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.
[1] https://github.com/josefs/Gradualizer [2] https://github.com/josefs/Gradualizer/blob/master/priv/prelu...
> 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.
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.
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.
This the question that needs resolution:
f = (x) => (...) ? Foo : g(x)
g = (x) => (...) ? Bar : f(x)
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...