I think it’s possible to go much farther than that. One attractive solution is to build a bolt-on solution on top of compiler hooks. That way you could have static type inference as a library. Those who wish to have it can use it; those who do not need not use it.
This old thread could be a useful read http://erlang.org/pipermail/erlang-questions/2008-October/thread.html#39245.
I know I’m coming back here after a long time, but the idea has stuck.
@ityonemo could you elaborate on this idea?
I was using typescript as a reference implementation because it seems to have similar constraints. Typescript is a layer on top of Javascript, is structurally typed (like Elixir), has amazing editor & code completion support, and deals with a language underneath that is dynamically typed.
Imagining a world where we throw away dialyzer specs and replace them with a type system layer similar to Typescript.
Actually I think the could would be simpler than Typescript because Elixir is a simpler language.
1 Like
yeah, I’m bullish on a “much better dialyzer”. I did just clear two things off of my stack, so one more to get to before continuing work on my type system. The state i’m at is that I have taken more of a “scientist’s approach” instead of a “mathematician’s approach”. What this means is instead of trying to shoehorn erlang VM into an existing theoretical typesystem, start from a theory of how the VM works, and build a typesystem around it using basic math, and set theory. I’ll be picking up my work on Mavis and Selectrix soon!
4 Likes
Excellent! I think it could also be a useful exercise to brainstorm developer experience. But suppose that’s a separate challenge?
One idea would be to see how a subset of typescript might map to elixir. For example the following are not exactly the same, but have equivalents in Elixir
- Interfaces
- Union types
- Guard clauses
Another thing worth looking at is JSDoc because it allows documenting types separately in the same way typespecs do.
Both will certainly have drawbacks but I think we may learn something from them.
Something inspired by interfaces and union types could cover quite a large amount of what Elixir typespecs do.
Types:
https://hexdocs.pm/mavis/Type.html
I’m in the middle of refactoring this. I realized I was doing lists and functions wrong.
inference:
Implements a DSL e.g. (mavis_inference/bifs.ex at main · ityonemo/mavis_inference · GitHub) that lets you define what types are accepted and rejected in both directions across an opcode, so you can do a bidirectional sift and infer which types are usable and which types are rejected.
There’s still some bugs and I need to write a sanity check to make sure that if you backpropagate, the type union is strictly smaller than the forward pass (because right now it’s infinite-looping on quite a bit of code).
Anyways if this stuff is interesting to you, i’m happy to accept help!
2 Likes
