Comment by tomp

1 day ago

I recommend anyone interested in this to check the work of Lionel Parreaux, in particular SimpleSub, which is equivalent to MLsub but substantially simpler.

As it turns out, Dolan's main contribution wasn't the algorithm (which is overly complex, as proven by Parreaux's simpler implementation), but the type language - the insight that most subtyping constraints can be removed and/or simplified to simple union and intersection types, assuming certain simplifications of the type system (namely: positive/negative types, and distributivity of union/intersection over function types).

https://lptk.github.io/programming/2020/03/26/demystifying-m...

https://dl.acm.org/doi/10.1145/3409006

Parreaux is continuing to work on this problem, and has since removed one of the assumptions/simplifications (positive/negative types) in his work on MLstruct