Status: Discontinued
Typed Erlang Experiment - using Ocaml for type-checking.
The idea was to transform Erlang to OCaml and leverage OCaml's Hindley-Milner type inference instead of relying solely on Dialyzer. Erlang atoms were mapped to OCaml polymorphic variants. The initial goal was not to generate runnable OCaml code, just enough to do the type-checking.
The landscape has changed dramatically since this project started:
- Erlang OTP 28 (mid-2025) shipped a built-in set-theoretic type checker as a compiler pass. It uses
-spec/-typeannotations, runs automatically, and will keep improving in OTP 29+. This is the official blessed solution. - Elixir 1.17+ (2024-2025) shipped built-in type checking using the same set-theoretic foundation (same researcher — Guillaume Duboc). It infers types without requiring annotations for most code.
- eqWAlizer (WhatsApp/Meta) is a production-grade gradual type checker for Erlang, open-sourced since 2022.
- Gleam 1.0 shipped in 2024 — a fully HM-typed language on BEAM with Erlang/Elixir FFI.
Dialyzer is nice, but I wanted to try a more standard Hindley-Milner type inference approach. http://okmij.org/ftp/ML/generalization.html
It had been tried before:
In order to do that, I needed to restrict Erlang, for example the bang operator ! needs to know the module(s) it sends the message to.
Instead of implementing type-checking myself, version 1 transforms Erlang to an OCaml program and lets the OCaml compiler do the verification. Erlang atoms are mapped to OCaml polymorphic variants, https://realworldocaml.org/v1/en/html/variants.html#polymorphic-variants
The OCaml type-checker is complex: http://okmij.org/ftp/ML/generalization.html