|
|
|
|
|
|
by DalekBaldwin
2153 days ago
|
|
|
"This paper seems to be saying all the math Stephen Dolan did was self-important overkill, at least in hindsight." It shows that you can implement algorithms that give the same results as MLsub without following the algebra so closely, but those algorithms were still designed with MLsub as a reference. It would be difficult to just stumble on a system like Simple-sub without that guidance. And Dolan's emphasis on the algebra of types still provides a guiding perspective for future work. If you want to add subtyping to a language with a more sophisticated type system, or add new features to a language that already has subtyping -- even if the existing subtyping system was written using MLsub or Simple-sub as a starting point -- you should probably take a long hard look at it from an algebraic point of view to make sure they interact the way you want, rather than call it a day after finding the simplest way to add the feature while still yielding a type lattice. |
|
|
Actually, I'm not sure it would be that hard (Simple-sub author here). If you look at the core of the algorithm closely, you'll see it's really not special: you create type variables, add constraints on them, propagate the constraints, and that's mostly it. In fact, it's perfectly in line all previous work on subtyping inference, going back at least to Pottier's 1998 thesis — that thesis already had many ingredients of MLsub. The three big things MLsub brought to the table, in my opinion, were: 1. the idea to coalesce constraint graphs into compact type expressions, which are easier to read and understand; 2. using the algebraic insight to develop an elegant and simple principality proof (but I'm not sure it's really worth it; AFAIK the proof sketch I provided would also work); and 3. to provide a simpler subsumption checking algorithm. Specifically in terms of pure type inference (so, ignoring points 2 and 3), it's possible to imagine making the leap to compact types without the algebra insight. But this is just speculation, and it's of course impossible to tell a posteriori.
> If you want to add subtyping to a language with a more sophisticated type system, or add new features to a language that already has subtyping
In that case I think Simple-sub is a good place to start, as it does not presuppose all the algebraic structure that MLsub does; Simple-sub shows that principal type inference really doesn't need much at all form the type system. Now, you're free to add more structure to your subtyping lattice if you want to be able to simplify types more, and if you want to make checking subsumption easier, but the choice is in your hands.
> you should probably take a long hard look at it from an algebraic point of view to make sure they interact the way you want
That's still definitely true!