The reason for this is that dialyzer was added afterwards to a very dynamically typed language, then Erlang and now Elixir, with the requirement that it was not allowed to change the language. At all! So it does what it can. You will find that it doen’t just type a function but type checks a function and the calls made to it together to see if they agree.

Also in some ways dialyzer basically ignores a function spec when type checking so you don’t really need one to get the type checking. If you give one it will check that it is consistent with what it can work out about the function and it will use it when reporting type errors, which can be very useful. Actually same with type defs. Though both are extremely useful for documentation.

The compiler always ignores type specs except for some basic syntax checks.

Depressing no?

Did you try the overspecs/underspecs flags? Erlang -- dialyzer

Dialyzer is fine for the trade-offs it chose to make. Having something more strict most likely means rejecting code that is completely valid today. Or in the best case scenario, forcing types to be explicit and not relying on inference.

@tmbb is correct here. There aren’t low hanging fruits when it comes to types. Adding a type system involves many compromises and the compromises you are willing to make change a lot when the language already exists.

If you want to have type inference, then many Elixir idioms will no longer be supported. Elixir code is based on unions (it returns {:ok, _} | :error) and intersections (different clauses of a function) and those are very expensive for an inference engine.

We could add requirements, such as obligatory typing of inputs, but that doesn’t solve the problem that we have both typed and non-typed code and we should likely check the values at the boundaries, adding runtime cost.

If you want to keep the language the same and support all of the existing idioms and also not worry about conversion costs: that’s Dialyzer.

Long story short: we could have other type systems but you need to start from scratch and you will have to compromise in many ways.

Apologies but I did not mean that Clojure Spec is the future. It is unlikely we will have something like Clojure Spec in Elixir per-se, especially because we have typespecs and guards and adding a third option is going to bring only marginal gains. If somebody wants to explore something like Clojure Spec as a package, then please do!

Question is: can this be improved in the future? TypeScript is doing a similar thing for JavaScript. On the bright side, the coverage of different use cases is increasing while keeping the compilation time fast. The bad thing is that IMO the type system is kind of exploding with complexity.

Seems like Elixir could add opt-in strict type checking.

Maybe Elixir could just be what it is and other languages on the BEAM can build a foundation much more suited to this kind of thing. I would rather have something designed from the get-go to be strict than trying to bolt it onto Elixir/Erlang.

What I mean is that I think you’ll see better results trying to design for something like this much earlier and languages like Alpaca are probably a better bet in this regard. If the people who really want a strongly, statically typed on the BEAM (myself included) simply tried to help with Alpaca, maybe we could end up with something that could even become our BEAM language of choice.

I’m not an expert on types but we already have type declaration syntax that the community actively using in Elixir. The problem is how Dialyzer interprets them (too loose). Maybe a stupid question but can’t we just build source code level (Elixir AST) analyzer as a hex package (archive?) that reads source code like Code.string_to_quoted |> Macro.expand, and uses the type specs AST to match them against the source code AST?

We are very interested of stricter typing in our company and are willing to put a remarkable bounty on this project, if it is viable option ofcourse