Literature and references on polymorphism / constraint solving applicable to Erlang

[erszcz]

For some time now I've been researching the literature and sometimes it feels a little bit like playing bingo ;) These are the relevant keywords describing features of the type system that, I think, we need in order to type check Erlang:

• subtyping - to model flexibility of a primarily dynamic language
• polymorphism - to express maps, folds etc; higher-order functions in general
• set-theoretic types - to express Erlang's first class union types and limited intersection types aka multiple-clause specs ("ad-hoc polymorphism", specifically "function overloading")
• local type inference / bidirectional typing - global inference for Erlang is undecidable, so we have to reach for local methods

All in all, I've identified only three papers (having looked through far more) which seem to present type systems capturing all of the above features:

1. Polymorphic Functions with Set-Theoretic Types by Castagna, Nguyen, Xu, Abate
2. Polymorphic set-theoretic types for functional languages by Thomas Petrucciani, but it's a PhD thesis under Castagna, so it covers a very similar approach
3. MLstruct: Principal Type Inference in a Boolean Algebra of Structural Types by Lionel Parreaux

The first two are a bit disheartening due to the volume and complexity of the presented theory and, to be frank, I haven't read them in detail yet. They seem to be spot on with regard to the features they target, though. There's also a fresh PhD project by Guillaume Duboc lead by Giuseppe Castagna on applying this theory to create a type system for Elixir, but no published results yet. Another factor in favour of this model is that there are reference implementations available:

• http://www.pps.univ-paris-diderot.fr/~gc/misc/polyduce.tar.gz
• https://gitlab.math.univ-paris-diderot.fr/cduce/cduce

MLstruct, on the other hand, seems to be significantly lighter, but according to the author, it's not completely applicable to Erlang without introducing modifications. Fortunately, it also comes with a reference implementation and even with MLscript - an online demo of a language based on this type system.

All these publications are quite fresh, i.e. the oldest one is from 2019. It really seems a type system for Erlang is on the edge of the current research in the field 😅

@josefs @zuiderkwast do you have an opinion on the papers mentioned above? Which model, do you think, is better suited to Erlang? Or maybe there are other, more relevant, papers that I've not stumbled upon?

[zuiderkwast]

Polymorphic Functions with Set-Theoretic Types (part 1 and 2) doesn't mention "gradual typing". Does this mean they only study fully statically typed languages here?

I liked this paper about gradual typing + set-theoretic types: Gradual Typing with Union and Intersection Types (Castagna, Lanvin) https://www.irif.fr/~gc/papers/icfp17.pdf -- with the limitation that it doesn't solve polymorphism (IIRC) -- sort of similar to what we already have.

I also liked (though hard to grasp) this one: Gradual typing: a new perspective (Castagna, Lanvin, Petrucciani, Siek) https://dl.acm.org/doi/10.1145/3290329 -- which uses a semantic approach rather than a syntactic one and solves polymorphism for set-theoretic types, but not subtyping...

[erszcz]

Some news based on findings from #503 and #504.

Having spent some time dogfooding the constraint solver, I see some limitations of the current implementation. In general, the limitations show up when dealing with intersection or union types.

#503 shows that constraints generated based on a function intersection type lead to conflicts and type checking errors. Constraints from multiple patterns are applied to a single type variable, whereas in fact the type var stands for a type which would be handled by a single specific clause of the function.

e643a0f shows a problem of pattern matching a union type in a negative position, i.e. as a return value, generating conflicting constraints. Strictly speaking, the problem is that each type var of the union is assigned constraints from both pattern clauses of the case expression, whereas in fact each of them is expected to match only one of the patterns.

[bieniusa]

We are also working on a set-theoretic type checker for Erlang; first publication out here: https://arxiv.org/abs/2302.12783 (published at IFL 2022).

Ping me for more information 😊

[zuiderkwast]

Very cool @bieniusa! I skimmed through the paper. The semantic approach seems promising. Will you release the implementation as open source? Then maybe some of us can even contribute something like maps or other missing pieces.

Also nice to see comparisons with gradualizer and the test suites in the paper.

@josefs: pinging you in case you haven't seen this.

[bieniusa]

Thanks for your interest! We are in the final steps of getting the repos online here: https://github.com/orgs/etylizer/repositories

They should be available within the next 1-2 weeks.
Contributions would be great! The experience will be a bumpy bit initially, but we really want to get it to a state where it is usable for the community.

[erszcz]

@bieniusa
Great paper! I think it's a really gentle and nice to grok introduction into the theory so directly applicable to Erlang 🚀

They should be available within the next 1-2 weeks.

I'd be really keen on experimenting with this new type checker. Is there any update on this? I see there's still only the feature-matrix repo available at https://github.com/orgs/etylizer/repositories.

Contributions would be great! The experience will be a bit initially, but we really want to get it to a state where it is usable for the community.

With the recent changes in Gradualizer we're finally able to successfully type check the project itself. With this in mind, I imagine it might be a long road ahead for etylizer to get to that state. Given these two projects are quite closely related -- strictly speaking, I think Gradualizer is "the first adaption of set theoretic types to a dynamically typed programming language widely used in industry", it's just not described in scientific literature (EDIT: upon a closer look at the set-theoretic model and algorithms it's rather clear Gradualizer is not a direct implementation) -- maybe Gradualizer's code base could serve as the ground for applying said theory and carrying on further research? I imagine it could bring benefit to the community earlier than developing a new tool from scratch. What do you think?

[bieniusa]

The etylizer repos are now publically visible: https://github.com/orgs/etylizer/repositories
Sorry for the delay - it is mid of teaching term for us and it was pretty hectic.
We carefully updated the issues to show where we are and where we are heading towards.
If anything is unclear, don't hesitate to ping us via issues and discussions.
Looking forward to your opinions and suggestions!

[ilya-klyuchnikov]

@bieniusa

We are also working on a set-theoretic type checker for Erlang; first publication out here: https://arxiv.org/abs/2302.12783

The paper claims:

This article introduces etylizer, a static typechecker
for Erlang. To our knowledge, etylizer is the first adaption of settheoretic types to a dynamically typed programming language
widely used in industry.

Which may not be correct - see eg https://luau-lang.org/2022/10/31/luau-semantic-subtyping.html - Roblox/luau has an order of magnitude more users than Erlang.

[bieniusa]

We had our paper submitted and presented to IFL‘22 which was actually in August 2022. The publication process of IFL has been taking a while due to post-conference proceedings.

We saw the blog post later - really nice and impactful work indeed!

[erszcz]

Roblox/luau has an order of magnitude more users than Erlang.

@ilya-klyuchnikov Hmm, actually what's the source of this information? My super quick and naive comparison of GH stars for Roblox/luau and erlang/otp suggests exactly the opposite. Or do you mean end users of products based on the respective platforms? lua/lua is the same order of magnitude as erlang/otp, but still fewer in absolute terms.