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
_______________________________________________
polyml mailing list
[email protected]
http://lists.inf.ed.ac.uk/mailman/listinfo/polyml
