[Vaguely2178]

I was referring to Elixir's blog post on static types where the creator of Elixir José Valim wrote: "The Dialyzer project, implemented in Erlang and available for Elixir projects, chose to have no false positives. However, that implies certain bugs may not be caught. At this point in time, it seems the overall community would prefer a system that flags more potential bugs, even if it means more false positives." [1]

From my experience with TypeScript, you really want your type checker to be eager about complaining about type issues, which is why so many people turn on strict mode. In fact, occasionally I'll have to suppress a false positive error with a @ts-expect-error comment.

But even assuming Dialyzer is as good as TypeScript, have you found that the libraries you use actually have quality type definitions? The few times I've used a JS library without type definitions it ended up breaking type inference, and infecting the codebase with the any type, which renders the type checker basically useless. How has your experience been in regards to that with Elixir?

[1] https://elixir-lang.org/blog/2022/10/05/my-future-with-elixi....

[h0l0cube]

> have you found that the libraries you use actually have quality type definitions?

I have some experience with Typescript and it was way better than vanilla JavaScript. Typescript mappings we’re available for most libraries, though for a couple they were not up to date. Similarly for Elixir, the coverage for nearly all APIs is pretty good but also has some holes. In my experience it hasn’t been a big deal either. Any serious library developer puts types alongside their function signatures/implementation.

> The few times I've used a JS library without type definitions it ended up breaking type inference, and infecting the codebase with the any type, which renders the type checker basically useless. How has your experience been in regards to that with Elixir?

Being a functional language, Dialyzer can easily make inferences on untyped code based on ‘success typing’ (what Jose talks about), though it can make for some very obtuse and verbose warning messages. This inference is in addition to safety provided by typespecs which every Elixir library developer typically intermingles with their API surface.

If I would level criticisms at dialyzer it would be its sometimes difficult to read warnings, it’s speed (despite being multithreaded) and the race conditions in the VS Code plugin (which is looking for extra maintainers – if I had time I would help). For the weird warnings I find I just need to add extra typing to my code to narrow it down, which I should be doing anyway

[Vaguely2178]

> If I would level criticisms at dialyzer it would be its sometimes difficult to read warnings, it’s speed (despite being multithreaded) and the race conditions in the VS Code plugin (which is looking for extra maintainers – if I had time I would help).

One of the advantages of TypeScript is that VSCode is written in TypeScript, and both VSCode and TypeScript are developed by the same company, so there's a really nice synergy there. I imagine Kotlin users feel the same way using Jetbrains products, and Swift users feel the same way about XCode.

Dialyzer looks interesting, but I can't imagine giving up on the expressiveness of TypeScript. Some of the things you can do with generics, mapped types, intersection types, template literal types, conditional types, and utility types are almost mind boggling. It's difficult to reap all of the benefits of static analysis without some of these advanced type operators. The type manipulation section of the TS manual is really underrated.

Someone for example wrote an SQL parser in TypeScript that requires no runtime code [1]. It can infer the types of an SQL query's result based on an SQL string without any runtime code execution. There was a similar project where someone built a JSON parser entirely using the type system [2]. There's also an ongoing discussion on Github about the the fact that TypeScript's type system appears to be a Turing-complete language with some other cool examples [3]. My point is that the type system is incredibly expressive. You rarely run into an idiom that can't be typed effectively.

[1] https://github.com/codemix/ts-sql

[2] https://twitter.com/buildsghost/status/1301976526603206657

[3] https://github.com/microsoft/TypeScript/issues/14833

[h0l0cube]

The SQL stuff sounds cool, but Ecto is so expressive I don’t even need to resort to raw SQL like I do in other languages. Elixir typing can handle a subset of intersection type which is rather niche, and of course handles union types which are more prevalent. Genetics and inheritance are replaced with a more permissive style of polymorphism with Elixir behaviors and are also part of the typing system.

All languages have their own flavor, and their own pros and cons, and if the advanced types of Typescript work for you, then great! In my own experience, I have found Elixir and it’s typing capabilities to work well for me

[Vaguely2178]

> The SQL stuff sounds cool, but Ecto is so expressive I don’t even need to resort to raw SQL like I do in other languages.

The SQL example I linked to isn't something you'd use to interact with a database in production, for that you'd probably reach for an ORM like Prisma. I was just trying to demonstrate the level of type inference you can achieve with TS. Going from a pure string of SQL or JSON to a concrete type without actually executing any runtime code is pretty crazy.

> Elixir typing can handle a subset of intersection type which is rather niche

I personally use intersection types quite a bit. If union types are like the logical or operator, then intersection types are like the logical and operator. Being able to define a type that combines one type and another is not a niche workflow for me.

> In my own experience, I have found Elixir and it’s typing capabilities to work well for me

Can't argue with that! Everyone has their preferences.

[erszcz]

> Going from a pure string of SQL or JSON to a concrete type without actually executing any runtime code is pretty crazy.

Going from a JSON string to a type for it is actually one of the easier examples of inference I can imagine. JSON is a data description format in which all the base types are syntactically distinguishable, it has no variables, no arrows (i.e. functions), no generics. In the topic of type inference, you can't have a much easier example.

SQL is more complex, indeed, but still doesn't seem too crazy if you have access to table schemas. It's also a matter of whether triggers and stored procedures are taken into account, but I assume they're not.

There's a lot of prior art described in literature as well as practical programming implementations with much crazier, yet successfully working type inference.

[Vaguely2178]

I just want to make sure we're on the same page here. The JSON example I linked to isn't inferring the types of JSON that's already been parsed and deserialized, that would be trivially easy in any language (including TS). If I have an object that's been parsed from JSON, I can just use the typeof operator in TypeScript to infer the type of that object.

The example I linked to is taking a serialized JSON string, and parsing the literal characters in the string (characters like double quotes, commas, whitespace, etc) into a type, purely using type annotations. And the structure of that JSON can be of arbitrary nested depth.

All of this is accomplished using template literal types which allow you to make assertions about the contents of a string. In TypeScript you can assert more than just "this value should be a string". You can make detailed assertions about the structure of strings, and that's what allows these parser demos to exist.

When you combine these template literal types with recursive types, conditional types, and TypeScript's infer keyword you can do some pretty interesting type level programming.

Just to further demonstrate the point, there's an interpreter for the BF programming language, written entirely using TypeScript type annotations [1].

> There's a lot of prior art described in literature as well as practical programming implementations with much crazier, yet successfully working type inference.

Has any of this been demonstrated in Elixir?

[1] https://github.com/sno2/bf

[h0l0cube]

> Going from a pure string of SQL or JSON to a concrete type without actually executing any runtime code is pretty crazy.

Elixir/Erlang might already be able to do something like this with metaprogramming. It’s certainly possible to generate and run Elixir at compile time, and map types are already a good superset for JSON objects, so a compile time JSON to map could then provide an inferrable type. I think someone more savvy with Elixir would know more. I’d certainly not something that I’ve needed.

[erszcz]

> But even assuming Dialyzer is as good as TypeScript, have you found that the libraries you use actually have quality type definitions?

Strictly speaking, Dialyzer has two big benefits over more traditional type systems:

1. It doesn't require type definitions to be present, it can type check code having none at all.

2. "Dialyzer is never wrong", i.e. it never returns false positives, i.e. it's an underapproximating checker.

These are the design decisions taken by the tool authors. There's rationale behind them, though the experience of using checkers for other languages might not be 1-to-1 applicable because of that. These decisions come with downsides, of course, some of which are covered in this thread, so I won't repeat them, but in general they were taken deliberately due to characteristics of the language(s) (it was originally created for Erlang, not Elixir) and the state of type system theory at the time. Please bear in mind Dialyzer was created in 2006, some 6-7 years before TypeScript.