Rob,
That's immensely useful. I was miles away from value restriction.
There shouldn't be any value restriction issue here - there isn't
polymorphism where you may think there is. As you point out, entering
at the top level gives
val x = 2: (_a, int) t
and a warning about inventing type _a. However, inside structure B,
type inference should, given the signature constraint, constrain x to
have type
('a t, int) t
which is just
(unit, int) t
So, no polymorphic type and no value restriction issue. In fact, if we
add a type annotation in structure B to make this constraint explicit
structure B :> B =
struct
type 'a t = unit
val x = A.mkT 2 : (unit, int) t
end
then test-1.sml and test-2.sml are accepted by both Poly/ML and SML/NJ!
So I think Poly/ML and SML/NJ may have a type inference issue there.
Also, I note that using 'a t rather than unit in the type annotation as
follows:
val x = A.mkT 2 : ('a t, int) t
does not help either Poly/ML or SML/NJ, which may give some clue as to
where the issue is.
I am assuming that such type annotations shouldn't be necessary for a
program to type check but perhaps I am wrong to do so.
Phil
On 21/07/12 12:24, Rob Arthan wrote:
I don't think your test-1.sml is correct Standard ML. If you cut it right down
to:
type ('a, 'b) t = 'b;
fun mkT n = (n : ('a, int) t);
val x = mkT 2;
You will find that Poly/ML says:
Warning-The type of (x) contains a free type variable. Setting it to a unique
monotype.
val x = 2: (_a, int) t
and SML/NJ says:
Warning: type vars not generalized because of
value restriction are instantiated to dummy types (X1,X2,...)
val x = 2 : (?.X1,int) t
What is happening here is that if x is given it most general type based on the
right-hand side of the binding, then the binding is illegal so the compilers
are generating a dummy monomorphic type to let it get through.
If you try it with an explicit type constraint as in:
val y : ('a, int) t = mkT 2;
both compilers will correctly raise an error.
The problem is the so-called "value restriction" (see
http://users.cis.fiu.edu/~smithg/cop4555/valrestr.html). Since the right-hand side for
your value binding for x involves a function call, and its type contains a free type
variable, the value restriction disallows it. It seems when you wrap this up with the
type constraints in signatures and the bindings in structures, the problem shows up at a
different level and the error messages are a bit misleading, but the fundamental issue is
that ML won't give x defined as you have defined it a polymorphic type.
Tip: with problems like this, it is often helps to see what happens with fewer
signature constraints. Your example goes through with a warning if you remove
the signature constraint on structure B - and it is that warning that explains
why it can't work with the signature constraint.
Regards,
Rob.
(e.g., see http://users.cis.fiu.edu/~smithg/cop4555/valrestr.html)
On 21 Jul 2012, at 10:53, Phil Clayton wrote:
Apparently the plain text attachments didn't work for everyone (and they're not
very readable via the list archive) so here they are again, this time as a
binary blob.
Phil
On 20/07/12 14:49, Phil Clayton wrote:
I have been making use of phantom types (for encoding a
single-inheritance class hierarchy) and have encountered a case where
code accepted by MLton does not type check with Poly/ML. After
investigating, it appears that MLton, Poly/ML and SML/NJ all take
different views on what is a valid program!
Attached are two small examples with a slight difference where type
checking accepts/rejects as follows:
test-1.sml test-2.sml
MLton 20100608 accept accept
Poly/ML 5.4, latest reject accept
SML/NJ 110.73 reject reject
I don't know which of the above is consistent with the Definition yet.
(I would be very glad if test-1 is a legal program though!)
Phil
_______________________________________________
polyml mailing list
polyml@inf.ed.ac.uk
http://lists.inf.ed.ac.uk/mailman/listinfo/polyml
<tests.tar.gz>_______________________________________________
polyml mailing list
polyml@inf.ed.ac.uk
http://lists.inf.ed.ac.uk/mailman/listinfo/polyml
_______________________________________________
polyml mailing list
polyml@inf.ed.ac.uk
http://lists.inf.ed.ac.uk/mailman/listinfo/polyml
