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.smlMLton 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