On 21/07/2012 18:44, Matthew Fluet wrote:
I believe that both programs are valid SML programs. Both are accepted by HaMLet (http://www.mpi-sws.org/~rossberg/hamlet/), which is usually my goto for "who's right?" questions.
The value restriction does come into play, in that the result of "A.mkT 2" cannot be generalized and must have a monotype. But, if an implementation infers the correct monotype for "A.mkT 2" (namely, "(unit, int) A.t"), then the result can be given the type scheme "('a t, int) A.t" due to the equivalence of "'a t" and "unit".
This is an interesting problem. I've been looking into this, poring over the Definition of Standard ML and the Poly/ML implementation and trying to see what's going on. I'm fairly sure these are correct and I've now worked out a fix that I'm going to commit shortly.
It seems to come down to the difference between the type expressions written by the user and the type expressions used in the semantics. The simplest example I could make was type 'a t = int; val x : 'a t = 1+1; Note: 1+1 here is expansive. On the face of it this violates the value restriction that "x" cannot contain a type variable. Hamlet, though, accepts it and prints val x = 2 : int I think the reason this is valid is that type abbreviations are type functions so "t" is BigLambda 'a . int rather than ForAll 'a . int . Hence 'a t is simply "int" and doesn't contain any type variables.
What this implies for the implementation is that it needs to actively reduce any type abbreviations to their right hand sides before doing any unification and also when applying the value restriction. This then allows Phil's examples to work and also the simple example above. It does have the unfortunate side-effect that expressions with type abbreviations are not printed using the abbreviation in cases where it used to.
David