As someone who worked with Elixir for the past couple years, and maintains multiple libraries in Elixir - nah not really. Static typing is the thing I'm missing with Elixir.

No matter how much pattern matching you do, and how many typespecs you add to get a better understanding of what's behind a variable, you'll still run into issues at runtime frequently that could have been avoided if it was statically typed.

Dialyzer is great but typespecs and pattern matching only get you so far. You'll always run into situations where the shape of data is not clear, and you have to open a REPL to do an IO.inspect somewhere

> You'll always run into situations where the shape of data is not clear

If you're using typespecs, then I think the deficiency is with tooling. I think the language servers (like ElixirLS) were quite buggy for a while, but it's getting better at code completion and inspection. But if the type has no spec then you're in the same situation as any gradually typed language.

If by "defiency is with tooling" you mean that `dialyzer` is bad, then yes. The current type checking facilities that it provides are too lax and also sometimes demonstrably actually incorrect even in the face of the simplest examples.

> incorrect even in the face of the simplest examples

I haven't found this in my experience. Most issues arise from a lack of typespeccing. If one were to rely on type inference, then, yes, it's not going to catch much. Specifying types is a requirement of a strictly-typed language, so to make a claim of deficiency with Dialyzer's type checking, you'd be comparing code that's fully specced with that of a strictly typed language.

The unavoidable problem is when using libraries that aren't properly typespecced, but that the same story as any gradually typed language (e.g., Typescript). The only solution here is to make a PR or a feature request to the product owners.

I've used dialyzer since 2015, it's not a question of "holding it wrong". I have an example of this that I literally demonstrated live in a talk online. It's very likely you haven't used dialyzer enough if you think it's actually correct 100% of the time even with type specs. Dialyzer is an exceedingly poor implementation of static type checking and not sufficient with any level of use.

I thought Dialyzer never raised false positives at the expense of false negatives, though perhaps your example is a false negative? I’ve only used it in the last 4 years. Is it possible the bugs have been fixed by now? Or is this just an inherent to this kind of type checking?

I don't think the implementation itself is at fault (I phrased that poorly in my previous post), but yes, I do think that the design of dialyzer makes it an (at times) faulty type checker. The unfortunate reality of a type checker that fails sometimes is that it makes it mostly useless because you can never trust that it'll do the job.

To be clear, I've had it fail in a function where I've literally specced that very function to return a `binary` but I'm returning an `integer` in one of the cases. This is a very shallow context but it can still fail. Now add more functions, maybe one more `case`. Dialyzer will just never keep up over a long enough time frame.

I think an entire rethink of type checking on the BEAM had to be done and that's why eqWalizer[0] was created and why Elixir is looking to add an actual sound, well-developed type checker. Gleam[1] I would assume is just a Hindley-Milner system so that's completely solid. `purerl`[2] is just PureScript for the BEAM so that's also Hindley-Milner, meaning it's solid. `purerl` has some performance issues caused by it compiling down to closures everywhere but if you can pay that cost it's actually pretty fantastic. With that said my bet for the best statically typed experience right now on the BEAM would be `gleam`.

0 - https://github.com/WhatsApp/eqwalizer

1 - https://gleam.run

2 - https://github.com/purerl/purerl

I miss static typing for two separate and quite opposite cases:

* trivial errors, that still cause a crash and waste my time ("foo(:yo, 7)" but was "foo(7, :yo)") - sometimes spotted by Dyalizer

* complex nested structures. In Java I never have surprises as to what foo.bar.baz is and I can use autocomplete reliably. Expressingthe same invariant in Elixir is something less straightforward

The fact that you _can_ open a REPL in production and inspect the data at runtime is huge.

Although few people use hotloading in code before, shapes of data can change from deployment to deployment.

That’s okay. I’d rather do that once in a while to keep all of elixir’s dynamic traits. The fact that you can open a REPL, and open one in prod, do language introspection, inspect data, query DBs with ecto, do hot code swapping is amazing.

Until we have something like Set Theoretical Types, I think this is the best of both worlds.

I'm building a static analyzer for Solidity in F# and the data shape of Solidity AST nodes overlaps frequently enough that explicitly specifying types is necessary just to get things to compile.

I can't imagine building something like this in a dynamically typed language. The way I see it, static typing is like writing inline unit tests to save yourself many, many headaches later.

types aren't a substitute for tests.

    let add : int -> int -> int = fun a b ->
      Random.self_init ();
      Random.int 100