Polymorphism, subtyping and type inference in MLsub -- Stephen Dolan - Alan Mycroft

Slightly off-topic, but if you're looking at lattices of types, are you familiar with Stephen Dolan's work adding subtyping to Hindley-Milner? Rough idea: given any two types `a` and `b`, rather than consulting the type hierarchy, we simply say that their meet and join are `a & b` and `a | b`. For example: select p v d = if p v then v else d Hindley-Milner would type this as select :: (a -> Bool) -> a -> a -> a But Dolan gives a more general type: select :: (a -> Bool) -> a -> b -> a | b Note that `|` is not the same as `Either`, rather, it means "an `a` or a `b`, but I'm not telling you which". But if your subtype hierarchy happens to have `a ≤ c` and `b ≤ c`, then you hav…

> Does anyone know if there are any implementations anywhere Yes, the type-checker used in the presentation is available online and on github. > any research into how they interact with type classes? Since the research is fairly new (there's also a POPL 2017 presentation), is presented using an OCaml-like language, and is implemented in OCaml, I'd guess not, at least not yet. What kind of extra difficulties are you worrying about, though? Isn't type-inference on an expression of type `C a => b` practically the same as if it had type `C a -> b` instead? Plus some extra work once a concrete `a` has been picked and instance search discovers new constraints, but that only occurs after `a`…