Erlang type system efforts

What’s going on with the Erlang typing efforts ?
Last I heard, Whatsapp had an internal project which was subsequently shelved.

Are there any other ongoing projects other than the Elixir ones (Typecheck, Norm etc…) ?

4 Likes

While I don’t know of any active attempts to type check Erlang or Elixir code, there are several active statically typed languages on the BEAM

6 Likes

There is a repository that tries to keep track of all the BEAM languages, including statically typed ones, and additional typing efforts for existing languages: GitHub - llaisdy/beam_languages: Languages, and about languages, on the BEAM

I’m sure this is even not all of them! (I need to dig through my stars on GitHub and send PRs to add a few more)

The languages @lpil listed are probably the most mature of the statically-typed ones, and used in production

5 Likes

This might be the “internal project” by WhatsApp GitHub - WhatsApp/erlt: Early prototype of ErlT, an experimental Erlang dialect with first-class support for static typing.
Alas I did not see it much discussed after it was released (and immediately archived on github).

3 Likes

I believe @alavrik was the lead for that project but it was dropped - perhaps Anton or @max-au might be able to shed some light as to why :blush:

There were a few threads about it:

I was going to link to @Qqwy’s TypeCheck but you’ve already mentioned it.

Aside from that and in terms of a full language, currently Gleam looks like it might be the best fit as Louis is keen on BEAM/Erlang/Elixir interop from what I gather from his posts :smiley:

1 Like

@AstonJ thanks for the ping. I am no longer with WhatsApp, so I can’t comment on the current state of the internal project for Erlang static typechecker. I very much hope that the project is going well. I believe that typechecker is essential for a large team that strives to stay efficient while working on a critical internet-scale service.

I also hope that we will eventually see some benefits of this project for the wider Erlang open-source community.

While I was at WhatsApp, we experimented with using Hindley-Milner for an Erlang-like language. We built an experimental Erlang dialect called ErlT: GitHub - WhatsApp/erlt: Early prototype of ErlT, an experimental Erlang dialect with first-class support for static typing. Eventually, we decided not to pursue this experiment further and open sourced it.

6 Likes

Thanks for the info Anton :blush:

Is that a separate project to ErlT? ErlT has been archived so I guess it’s not something the WhatsApp team will be working on themselves (perhaps you could take over it?)

Were there any technical reasons for this or was it just something the team/WhatsApp lost interest in? (No problem if you’re not allowed to share details.)

1 Like

Anyone can of course pick up the effort since it’s open source.

2 Likes

GitHub introduced a new feature so I made a “erlang and static types” list of my GitHub stars: https://github.com/stars/michallepicki/lists/erlang-and-static-types
edit: The star lists feature requires logging in to GitHub, otherwise shows a 404 error.

3 Likes

Wow. Its mind boggling how many man hours have gone into this.

Wonder what the Erlang folks were trying with this…
erlang-labs/typer: Erlang/OTP (github.com)

3 Likes

Doesn’t look like Gradualizer has been linked to here yet GitHub - josefs/Gradualizer: A Gradual type system for Erlang

4 Likes

Its the first on the list

3 Likes

30 posts were split to a new topic: Static Typing vs Dynamic Typing (split thread)

I often wonder why the erlang-labs github repo score so high on google… it is a dead organization that we used to experiment with breaking Erlang/OTP into multiple repositories.

The repo that you are linking to is Erlang -- typer, which is a tool to automatically annotate Erlang code with type annotations based on what dialyzer figures out.

6 Likes

Hi all, just a quick note to say I agree with Peer that it’s important to highlight the shortcomings of things like static typing but I also agree with Louis that a dedicated or linked thread for that may be best (a bit like our What do you think should be in OTP? and What do you think should not be in OTP? threads).

It’s also completely normal for threads to develop forks like this and so what we usually do is when it seems necessary we split them into dedicated thread/s. When I get a moment I’ll do that here and post a link back to that thread (I’ll also do a bit of general clean up so the threads can get back on track).

I’m going to move this thread to the moderation queue for now, then once it has been sorted out will move it back to the main forum. Thanks for your patience and understanding.

Edit: done - here’s the link to the split thread: Static Typing discussion (split thread)

2 Likes

I hope I’m not uncovering some not fully fleshed out plans, but here is a new effort related to CDuce and Elixir: Giuseppe Castagna: Master project description on “Set-theoretic types for the Elixir programming language”.

I slightly worry about the structural type checker performance, but I’m sure there are ways to make it fast enough (as shown e.g. by Typescript). And similarly with pretty printing “big” types, e.g. in error messages.

But I think this is very exciting news!

4 Likes