Algebraic Subtyping

Language Design
1

I originally opened up an issue on the dotty repo to discuss this, and was asked to move the discussion here. I found this paper on Hacker News today and have read through a few chapters. For me, the lack of full type inference has always been a trade off that I’ve been willing to deal with in order to get the benefits of functional programming with subtype polymorphism. This paper discusses a type system that provides ML style parametric polymorphism, subtype polymorphism, fully decidable type subsumption, and it does it with full type inference.

The author is a member and contributor to the ocaml community and the paper strongly reflects this background but I find a lot of the ideas extremely interesting and would love to see how applicable they are to the DOT calculus and scala in general. In particular I’d love to see how his ideas on biunification fit in with the the DOT calculus, and whether dotty could potentially benefit from these ideas. Also, the paper mentions higher kinder types as future work and was wondering if the ideas used in dotty to build higher minded types on top of DOT could translate over. Feel free to discuss other aspects as they relate to scala as well :slight_smile:

2 Likes
2

Note that besides the thesis (which I haven’t tried to read yet), there is an implementation online at https://www.cl.cam.ac.uk/~sd601/mlsub/ as well as a preprint of a related paper published at POPL 17: https://www.cl.cam.ac.uk/~sd601/papers/mlsub-preprint.pdf

3

I am about 1/3rd through reading the thesis. I believe it’s very interesting, but not 100% applicable to Scala. In particular, recursive types are used pervasively in the thesis, and the principal types property depends on them. But they are not present in Scala or in DOT. DOT has a different sort of recursive type, which is restricted to records, and the recursion goes through the self reference this instead of the type itself.

There’s some doubt whether MLsub’s recursive types let too many programs pass the typechecker which would better be rejected. See Andreas Rossberg’s comment in http://lambda-the-ultimate.org/node/5393.

Leaving out recursive types, the other elements are indeed very close to DOT and Scala. Maybe we can learn something from the thesis for making our constraint solving and type inference better.

4 Likes