Hacker News Reader

Comment by virtualwhys | Hacker News Reader

Assuming the thesis is "easily" implementable, will a from scratch ML need to be created, or can existing ML based languages all benefit? i.e. implement in the compiler, and voila, subtyping + inference for all MLers.

View on HN

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-subty... (PDF)

That 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.

Yeah 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.

Yeah 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).

Reply on news.ycombinator.com