3 ms·
ML modules are great, but I'm not convinced that making them first-class (1ML) will be equally great. ML hits a sweet spot between automation (full type inferen
by catnaroek 9y ago
ML modules are great, but I'm not convinced that making them first-class (1ML) will be equally great. ML hits a sweet spot between automation (full type inference) and expressiveness that is only possible because the type language is first-order. This is IMO the point that most extensions on top of Hindley-Milner completely miss.
So, if anything, what I'd like to see is a dependently typed language whose type language is a first-order, computation-free (no non-constructor function application) subset of the value language.
- ratmice 9y agoThe 1ML papers discuss this, ML implementations in reality are already incomplete with regard to Hindley-Milner, a quote: "We show how Damas/Milner-style type inference can be integrated into such a language; it is incomplete, but only in ways that are already present in existing ML implementations."
- tomp 9y ago1ML is a conservative extension of HM - all valid ML programs are typable in 1ML without extra annotations. Furthermore, OCaml essentially already has first-class modules - just the syntax is much more awkward than is possible with 1ML.