4 ms·
Unfortunately, it is never as easy as "just" putting in a new type system to a preexisting compiler. In the case of ML and Haskell in particular, we are kind of
by ezyang 10y ago
Unfortunately, it is never as easy as "just" putting in a new type system to a preexisting compiler. In the case of ML and Haskell in particular, we are kind of crazy about GADTs, and GADTs and subtyping are known to interact in complex ways. See for example http://gallium.inria.fr/~remy/gadts/Scherer-Remy:gadts-subtyping@inria2012.pdf http://gallium.inria.fr/~remy/gadts/Scherer-Remy:gadts-subty... (PDF)
- virtualwhys 10y agoThat was my intuition. The instant win scenario for ML based languages is quite appealing from this side of the fence (Scala) where it's not all roses wrt to type inference and subtyping. Maybe even, gasp, SML can rise from the ashes and bring Rob Harper's dream to fruition (which seems to be that developers stop using Haskell); that or someone implements Rossberg's 1ML, or the theory backing this thesis. All the MLs, including Haskell, have pretty significant tradeoffs, would be great if there was really 1 ML to rule them all.
- Ericson2314 10y agoYeah 1ML is what really benefits from this: You really want subtyping for modules to handle library evolution, and 1ML means if you want it for modules ya better have it everywhere.
- Jweb_Guru 10y agoYeah IIRC width subtyping for modules was the only thing they didn't have complete inference for if you didn't use large types, so this is a huge win. Though I'm nearing the end of the thesis and I'm afraid there may be some things about 1ML that don't jive with this (1ML elaborate to full Fω and gives you explicit access to existentials and higher kinds, which are possibly difficult to unify with the work here).