I'm currently actively working on a typechecking system for elixir (three packages: https://github.com/ityonemo/selectrix for compile-time interface, ../mavis for type logic, and ../mavis_inference for performing type inference on compiled code).
The chief difficulties I am running into are:
1) How to do intersections on functions and maps (this is in the article):
f(integer) -> integer is not usable as f(any) -> integer
2) not all of the erlang bytecode instructions are well documented
3) I still haven't figured out how to deal with circular dependencies at the module level.
Erlang makes this easy in these ways:
1) compiled module structure is simple and the way branching works makes the mechanics of type inference trivial.
2) erlangs concurrency makes dealing with, for example in-module dependencies trivial
3) there are only a handful of types in erlang so, aside from functions, their subtyping relationships are very straightforward.
Elixir makes this easy in these ways:
1) Typechecking structs can be more straightforward than records.
2) Writing a composable type logic (mavis) is super easy with elixir's protocols
3) I built (and am refining) a very easy dsl that makes creating and testing logic for the beam opcodes less of a hair-tearing experience:
I'm going to shill Gradualizer[1] in here as well.
1. I think you have to see typing as helpful information. Like:
-spec add(integer(), integer()) -> integer().
add(A, B) -> A + B.
Technically, nothing prevents add from accepting number() or float(). It's too much specification.
2. I was surprised how much there actually is but also disappointed that a lot of errors were in until OTP 23. Gradualizer also overrides some definitions [2]
3. Haven't encountered a problem with this yet with gradualizer, would need to test.
Yeah, I had thought that development of Gradualizer had halted, glad to see it's not. Part of why I wanted to do Mavis is because I wanted to make it easy for developers to make their own custom overrides and ship it with their libraries, especially for Elixir protocols[0]. still haven't figured out how to architect that, but I have an idea.
> I think you have to see typing as helpful information
Indeed. Selectrix will allow you to chain your inference with fallbacks, so, maybe the first level is a fast cache, second level is checking files for user overrides, third level is dialyzer specs, fourth level is inference.
I think it should also be possible to create an addon module with Mavis that lets you type inbound messages for GenServers, given a set of constraints (all possible calls and casts are present in the module itself as an API)
[0] it's a big problem that in elixir, Enumerable protocol destroys typing information, so I want to make an typing override for Enumerable an "example" typing override system.
I think it did partially stopped. I'm the only one committing right now but some of the original devs will review PRs and are EXTREMELY helpful. Great bunch.
The sytnax and integration look great here, I like it.
Although not entirely the same Dialyzer always seemed to be strange and quirky in its design choices - in the same way other parts of Erlang syntax can be a bit odd sometimes. The kind of thing I assume inspired Elixir in the first place (although in general I like Erlang as a language, it’s small enough and my complaints are few - it just feels syntactically quirky sometimes).
But I never felt inspired to use Dialyzer largely for these reasons. Never seemed to “fit” the syntax entirely and made it quite ugly IMO.
Which is why I’m happy to see these modern attempts, they look much better.
Good luck with the project. It should be an excellent learning process regardless.
> 3) I still haven't figured out how to deal with circular dependencies at the module level.
That is usually dealt with by distinguishing between interface and implementation (cf. dependency inversion principle), which should eliminate the circularity. Disclaimer: I know very little about Erlang and Elixir.
You start with f having type 'a0 -> a1', and g having type 'a2 -> a3'.
Looking at the body of f you infer that a0 = a2 and a1 = Foo | a3, after the substitution f has type 'a0 -> Foo | a3' and g has type 'a0 -> a3'.
Looking at the body of g you infer that a0 = a0 (whew!) and a3 = Bar | (a3 | Foo). Now, the last one is tricky, and here is the point where you can easily get your type inference engine to diverge, but the (least) solution is given by a3 = Bar | Foo (because A = A | B iff A is a superset of B).
So, after the final substitution you have 'a0 -> Bar | Foo' for f and 'a0 -> Bar | Foo' for g, generalize 'a0' as appropriate.
The chief difficulties I am running into are:
1) How to do intersections on functions and maps (this is in the article):
f(integer) -> integer is not usable as f(any) -> integer
2) not all of the erlang bytecode instructions are well documented
3) I still haven't figured out how to deal with circular dependencies at the module level.
Erlang makes this easy in these ways:
1) compiled module structure is simple and the way branching works makes the mechanics of type inference trivial.
2) erlangs concurrency makes dealing with, for example in-module dependencies trivial
3) there are only a handful of types in erlang so, aside from functions, their subtyping relationships are very straightforward.
Elixir makes this easy in these ways:
1) Typechecking structs can be more straightforward than records.
2) Writing a composable type logic (mavis) is super easy with elixir's protocols
3) I built (and am refining) a very easy dsl that makes creating and testing logic for the beam opcodes less of a hair-tearing experience:
https://github.com/ityonemo/mavis_inference/blob/main/lib/ty...