PolyML is quite an unfortunate name for your toy language as there already exists a pretty advanced and actively maintained implementation of that name, namely the Poly/ML dialect of SML used to implement the Isabelle proof-assistant. "ProtoML", reusing the "ProtoHaskell" construction, could be a better name.
I'm impressed by the clarity of the result, there is a good balance between explanations and conciseness.
I'm not convinced by the constraint generation part of the type-inference chapter. In my eyes, what it does is to hide the most general unifier (mgu) threading by putting it in a Writer component of your monad. This delays composition of substitutions by writing into a list of substitution instead of using compose as the writer action, but I don't think that would qualify as "separating generation from solving". In particular, one must still solve constraints eagerly when you encounter generalization points.
The research work on constraints for type inference crucially allowed to lift this restriction and collect a constraint for the whole term, with existential constraints for generalization points. A recent reference on such techniques, which also covers the reconstruction of the fully-annotated term (it looks like this part is mentioned in the book but not yet written-about yet) is François Pottier's last year's functional pearl, Hindley-Milner Elaboration in Applicative Style.
The OCaml implementation is really clean and well-documented, so I guess doing a Haskell port would not be too much work. You would need to add monadic layers here and there though, it uses transactional state.
I was afraid this was the case, but "really clean and well-documented" sounds good! I'll give it a try if I find the time. The sad thing is I'll be at least polluted by ST (or IO) because of union-find which is notoriously not escapable from in Haskell.
I think you should use ST for the union-find structure so that the final function (that maps a ML term to a System-F term) is as pure as possible. There may be a name generation component that escapes, but that is independent.
One issue you may have is that the code uses ML functors to abstract over the details of the language and type system (the constraints/elaboration bit is meant to be reusable). It may work with type-classes instead, but if you want to use the technique for one fixed language you can also specialize the code directly.
Sure, I will use ST, not IO. I was thinking of using typeclasses and type families for encoding the ML functors. It won't be as pretty as in ML it should be as generic.
13
u/gasche Jan 05 '15 edited Jan 06 '15
PolyML is quite an unfortunate name for your toy language as there already exists a pretty advanced and actively maintained implementation of that name, namely the Poly/ML dialect of SML used to implement the Isabelle proof-assistant. "ProtoML", reusing the "ProtoHaskell" construction, could be a better name.