I'm currently actively working on a typechecking system for elixir (three packages: <a href="https://github.com/ityonemo/selectrix" rel="nofollow">https://github.com/ityonemo/selectrix</a> for compile-time interface, ../mavis for type logic, and ../mavis_inference for performing type inference on compiled code).<p>The chief difficulties I am running into are:<p>1) How to do intersections on functions and maps (this is in the article):<p>f(integer) -> integer is not usable as f(any) -> integer<p>2) not all of the erlang bytecode instructions are well documented<p>3) I still haven't figured out how to deal with circular dependencies at the module level.<p>Erlang makes this easy in these ways:<p>1) compiled module structure is simple and the way branching works makes the mechanics of type inference trivial.<p>2) erlangs concurrency makes dealing with, for example in-module dependencies trivial<p>3) there are only a handful of types in erlang so, aside from functions, their subtyping relationships are very straightforward.<p>Elixir makes this easy in these ways:<p>1) Typechecking structs can be more straightforward than records.<p>2) Writing a composable type logic (mavis) is super easy with elixir's protocols<p>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:<p><a href="https://github.com/ityonemo/mavis_inference/blob/main/lib/type.inference/opcodes/gc_bif.ex" rel="nofollow">https://github.com/ityonemo/mavis_inference/blob/main/lib/ty...</a>
Interestingly enough, the article doesn't say anything about propagation of types, which is the crux of the type checking and what makes any typing system useful or useless, obnoxious or helpful. Consider the example from the article:<p><pre><code> % a good old list length counter
count(A=[_|_]) -> count(A, 0).
count([], C) -> C;
count([_|T], C) -> count(T, C+1).
</code></pre>
What is the type of count/2? Arguably, it's "(list, any | number) -> any | number", which means that count/1 has type "list -> any | number". Well, that's bloody pointless, isn't it? What you probably want is "(list, any) -> any | (list, number) -> number" for count/2, so you could give count/1 its useful type "list -> number", but intersection function types are notoriously difficult to infer or typecheck, even with manual annotations.
I'm watching Gleam[1] for my 'I want to learn Erlang but dont want to deal with having to do runtime type checks so I wish there was a Statically-Typed Erlang' dreams.<p>[1] <a href="https://gleam.run/news/gleam-v0.12-and-gleam-otp-v0.1-released/" rel="nofollow">https://gleam.run/news/gleam-v0.12-and-gleam-otp-v0.1-releas...</a>
Just in case anyone here missed or hasn't seen this news: Facebook is working on a statically typed Erlang. <a href="https://twitter.com/robertoaloi/status/1304085677252935681" rel="nofollow">https://twitter.com/robertoaloi/status/1304085677252935681</a>
I really want to like Erlang because the priorities and USP's of the language are super compelling for a lot of use-cases. I tried to kick the tires on it a couple years ago, and what I found is that the error messages were just so vexing, and it took a minute to understand what they meant, even in toy examples. Maybe it gets better with time, or there is tooling to help with this, but it seemed a bit behind the times with the standard which has been set by more modern programming languages.
> all sorts of pattern matching<p>Outside of the famous builtin process model/BEAM (plus the subsequent ‘crash first’ style design of programs which adds resiliency) the pattern matching is what makes Erlang one of the best languages and the one thing I wish every new language copied.<p>You kinda get it in Haskell and Rust with the maybe style pattern matching. Rust in particular makes good use of it.<p>But it’s one thing I miss the most not writing Erlang/Elixir for a living... so far. It makes functions and data handling into these clean trees instead of conditionals (not to start a language flamewar but boo Golangs conditional obsession which seems to be the polar opposite in many ways for error handling, or at least it used to be I haven’t tried it recently).<p>There’s a lot to like and learn from in Erlang. Static typing will give it wider adoption IMO. And I’m happy to see so many developers working on it.
I replied to your post on twitter but I highly recommend Gradualizer[1].<p>Discovered it last year and started using it. The refinement portion handles unions and guards very well. It's not perfect but I'm integrating it in our codebase with some interesting successes. I'm hoping more people use it on their codebase and can find any bugs they have with it so it can be improved further.<p>[1] <a href="https://github.com/josefs/Gradualizer" rel="nofollow">https://github.com/josefs/Gradualizer</a>
I'd recommend anyone who have troubles with outdatedness (?) of the Erlang, to try Elixir. It runs on Erlang virtual machine, very modern and pleasure to code in.