How to make Dialyzer more strict?

[OvermindDL1]

@stefanchrobot

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.

Yes, in fact it could even be done via a library, this is what my TypedElixir and MLElixir experiments do (in different ways).

(Wish I could get time to work on it some more, it’s so fun making such things!!)

@gon782

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.

Alpaca has promise, but it is more ‘pure’ in typing, like having OCaml compile to Javascript. It doesn’t have great integrations with Elixir and macro’s just don’t work at all, in addition it can’t use the types that the rest of the Beam more focuses on, as well as it doesn’t black box PID’s but instead tries to ‘type’ them (which seems inherently faulty on a BEAM language to me), etc… It is good as a more pure language, but not as something to interact with Elixir libraries.

@stefanchrobot

I’d rather have this in Elixir 2.x. The downside of a new language is the fragmentation of the community. What’s the point of a new language if you can’t get hired to work in it? It’s still tough to find a job in Elixir.

Elixir is expressive enough (though the syntax definitely has some warts, like a couple random n-arity ‘functions’ as one example…) to do it as a library though. ^.^
Then you can mix-and-match as you want!

@gon782

I work with both Erlang and Elixir, i.e. I work with the BEAM. Would I have issues trying to convince project leaders to let me use LFE? Yeah, but the value proposition of something like LFE isn’t as obvious as a statically typed language that could allow for far less cognitive load. The value of a language like that would be self-evident at some point and it’s a much easier comparison than external statically typed languages vs. Elixir as well.

It actually would be possible to make an LFE library that can make and consume Elixir macro’s though, unlike Alpaca.

You could type LFE as well via a library for it.

@gon782

because all the important things in Elixir are the important things for the BEAM in general.

Except Macro’s, Parse Transforms are indeed as powerful in erlang but just not as easy to use. Macro’s are where Elixir gets its power (a proper macro system in erlang would make choosing elixir over erlang far far harder with only the library ecosystem (because of elixir macros) being the deciding choice, I wish elixir was more erlang/beam compatible instead of making custom/new formats somehow…).

@gon782

Not for more strict type checking only, perhaps, but certainly for a better type system. If you want a decent language in terms of type system you should implement it in compiler passes and probably just output BEAM bytecode.

Precisely this. A good type system not only catches a lot of bugs (making entire classes of bugs just outright impossible), but it can also generate better code, make smaller and more expressive code constructs, and more!

@hypno

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?

As stated above, just strengthening it alone will make checks better, which is always good of course, but you don’t get the gain in code generation efficiency nor better code constructs. That is why both of my TypedElixir and MLElixir experiments tries to ‘use’ dialyzer specs as much as possible, but also expanded above and beyond those.

@hypno

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

Oh I wish I had the time! It would be so fun to do!