Thread by @erszcz

Is type checking #Erlang hard? Or #Elixir, by the way? Let's think...

There are only structural types in Erlang. No types are compared for equality just based on their names. Not even records, as they're tuples, and tuples differ structurally by arity.

Apart from opaque types which by definition hide the structure. So they can only be nominal! And maybe also user-defined types (also known as user types), since these do have names... But at runtime types don't exist anymore, so it's the structure that matters. Always. Almost ;)

Wikipedia says that "a value of a variant type is usually created with a quasi-functional entity called a constructor."

In Erlang types are (almost) always structural and don't have constructors :( Which makes supporting ADT-like features, like checking for pattern exhaustiveness, require to build them on top of union types. Union types, as in...

Set-theoretic types. It's quite clear from the official docs that Erlang has union types.

It's not as obvious, but still there, that Erlang also has intersection types - they camouflage as multiple-clause specs.

If one squints really hard, they might even spot the negation types in the bushes: "The general form of map types is #{AssociationList}. The key types in AssociationList are allowed to overlap, and if they do, the leftmost association takes precedence."

So if typing Erlang is set-theoretic, and sets can be subsets or supersets of other sets, then can types be subtypes or supertypes of other types?

Of course they can! After all we wouldn't want to, and thankfully don't have to, treat integers and floats differently all the time like the #OCaml folks do ;)

With this comes aaaaall the fun with fun(ction)s, though! It goes something like this: fun F is a subtype of another fun G if it's contravariant with G in the argument type, but covariant in the returned type.

So what about the aforementioned maps? Should they be covariant or contravariant in keys and values respectively?

So Erlang is a functional language with all these maps, and folds, and other higher-order functions that take functions AND data as arguments. Which all would be useless without polymorphism.

After all, we wouldn't want to write a separate map_integers, map_floats, map_maps. These just have to be generic in the element/leaf type of the structure they traverse.

So it would be nice to type check these small functions we pass into the higher order functions, against the data we pass into these higher order functions. And against the specs of these higher-order functions.

But often it's convenient to write these small functions that we pass to the higher-order functions inline. But the Erlang syntax only allows type annotations (aka specs) on the top-level functions!

So if the Erlang syntax doesn't allow to type annotate our inline functions, we have to resolve to...

Local type inference also known as bidirectional type checking. Well, we need to know the types of these small inline functions, so there's only one way to get them - infer them.

That's quite a few keywords already and we haven't even considered type checking message passing or exception handling.

The latter might not even be reasonable as modern statically typed languages like Rust or Swift shun exceptions. The first doesn't have them at all. The second requires explicitly declaring throwing them.

So could've @rvirding and @joerl originally created Erlang with a dedicated type system if they REALLY wanted to in 1986? I don't know.

I know, though, that Haskell first appeared only in 1990 and OCaml in 1996.

I also know the only papers I could find which cover all the aforementioned features we need in a type system for Erlang are:

"Polymorphic Functions with Set-Theoretic Types", POPL 2014

"MLstruct: Principal Type Inference in a Boolean Algebra of Structural Types", OOPSLA2 2022

And then there's github.com/josefs/Gradual…, which kind of does almost everything mentioned above well enough to type check itself with almost no warnings. (You've been warned ;p) But it has no formal description, or proof, and not much docs yet. It just works!