I agree that each ML falls short in some ways--I think SML and OCaml are probably the best programming languages ever made, but there's definitely room for impr

I agree that each ML falls short in some ways--I think SML and OCaml are probably the best programming languages ever made, but there's definitely room for improvement. I dream of the "Next Great ML"; 1ML definitely looks interesting in this regard, though I am a bit skeptical of Rossberg's rhetoric on a number of issues. I use SML over OCaml mostly for cultural & political reasons; SML has a few areas ripe for improvement (some of which are addressed in OCaml, others not): 1. structure sharing in the Definition is so bad that pretty much all the implementations of "S"ML diverge from it in some way. Each implementation of structure sharing is frustrating in its own way. 2. would be nice to be able to do higher-kinded polymorphism, as in 1ML 3. would be nice to unify polymorphism as a mere mode-of-use of functors, as in 1ML (well, this was not invented in 1ML, as I first saw it in Dreyer/Harper/Chakravarty's "Modular Type Classes": http://www.mpi-sws.org/~dreyer/papers/mtc/main-long.pdf; http://www.mpi-sws.org/~dreyer/papers/mtc/main-long.pdf; it may go back as far as the Harper-Stone type theoretic semantics). Combined with higher-order functors (which I believe are proposed to be added to "Successor ML"), this would give a proper treatment to polymorphism at higher kinds. 4. we need to standardize on a package calculus; the ML Basis system as used in Mlton is pretty nice, as is the simpler system used in SML/NJ's "Compilation Manager". 5. modular type classes (analogous to coq's "canonical structures") should be added in order to alleviate the pain of explicitly instantiating functors, etc. We do NOT want "type class coherence" as in Haskell, which amounts to a piece of global state that essentially outlaws local reasoning. I call it the "Antimodularity Restriction", but the name hasn't caught on, as much as Haskell folks like to berate us over our "value restriction" (which is a non-problem, and very useful--though it would be better to reconstruct it in a less ad-hoc way, via the theory of polarization that comes from Girard, and was further developed in light of effects, refinements and polymorphism by Zeilberger in his dissertation). 6. I'd like to (at least) follow OCaml and add the ability to convert between module signatures & existential types; I'm not sure if I am sold on the 1ML approach, which goes quite a bit further than this, but I need to investigate it more. 7. Refinement types would be nice (but PLEASE---do not fix in advance some awful solver or something for this; contra the popular literature at the moment refinement types have NOTHING at all to do with solvers!).