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
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
Phil,
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
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
On Sat, Jul 21, 2012 at 10:34 AM, Phil Clayton phil.clayton@lineone.net wrote:
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) tdoes 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.
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".
I was going to point out the same solution that Phil notes: that adding an explicit type ascription that sets the type of the "A.mkT 2" expression to "(unit, int) A.t" allows the program to be accepted by SML/NJ and Poly/ML.
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
On 23/07/12 12:51, David Matthews wrote:
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.
Thanks for the update. I haven't noticed much difference in the printed types. The only change worth mentioning is that
val it = (): unit
now prints as
val it = (): {}
which is worth alerting people to. For example, ProofPower build files pattern match on that response to remove them.
Phil
On 05/08/12 15:55, Phil Clayton wrote:
On 23/07/12 12:51, David Matthews wrote:
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.
Thanks for the update. I haven't noticed much difference in the printed types. The only change worth mentioning is that
val it = (): unit
now prints as
val it = (): {}
...
I probably spoke a bit too soon here. After more interactive use, it appears that records and tuples can be expanded one level in the types printed back. This can make types much harder to read which may be an issue for those using an interactive session to e.g. inspect expression types by evaluating fragments of code. With the example at the end, 5.4 prints back
val nearest = fn: point -> point list1 -> real * point
which is fairly self-explanatory, whereas r1581 prints back
val nearest = fn: real * real -> (real * real) * (real * real) list -> real * (real * real)
This can be worked around using additional type annotations but that doesn't help for inspecting already written code and some people may not be happy to add so many annotations. (Also, it seems that for function return types, the annotation must go on the rhs.)
Phil
(* Example *)
type 'a list1 = 'a * 'a list fun foldl1 f ((x, xs) : 'a list1) = foldl f x xs fun map1 f ((x, xs) : 'a list1) = (f x, map f xs)
type point = real * real
fun sq (x : real) = x * x
fun distance ((x1, y1) : point) ((x2, y2) : point) = Math.sqrt (sq (y2 - y1) + sq (x2 - x1));
fun nearest p ps1 = let fun nearest2 (i as (di, _), a as (da, _)) = if di < da then i else a fun addDistance q = (distance p q, q) in foldl1 nearest2 (map1 addDistance ps1) end ;
On 05/09/2012 14:27, Phil Clayton wrote:
I probably spoke a bit too soon here. After more interactive use, it appears that records and tuples can be expanded one level in the types printed back. This can make types much harder to read which may be an issue for those using an interactive session to e.g. inspect expression types by evaluating fragments of code. With the example at the end, 5.4 prints back
val nearest = fn: point -> point list1 -> real * point
which is fairly self-explanatory, whereas r1581 prints back
val nearest = fn: real * real -> (real * real) * (real * real) list -> real * (real
- real)
It really ought to be unwinding any type abbreviations into their right hand sides. Perhaps it is only applying it once rather than repeatedly but that needs to be fixed. The problem with the bug you reported is that it really requires that this be done before unification so fixing the bug necessarily messes up printing. The only way I can see to avoid this is somehow to mark those type abbreviations that discard one or more type variables i.e. where a type variable on the left does not occur on the right, and only force the unwrapping on those. This would have to be inherited by any other type abbreviation that used such a type abbreviation. e.g. type ('a, 'b) t = 'a type ('a, 'b) s = ('a, 'b) t
I can't see a way to fix the bug and still keep the old printing of types with abbreviations. The problem is that the language definition does not consider printing at all.
David
On 05/09/2012 18:07, David Matthews wrote:
On 05/09/2012 14:27, Phil Clayton wrote:
I probably spoke a bit too soon here. After more interactive use, it appears that records and tuples can be expanded one level in the types printed back. This can make types much harder to read which may be an issue for those using an interactive session to e.g. inspect expression types by evaluating fragments of code. With the example at the end, 5.4 prints back
val nearest = fn: point -> point list1 -> real * point
which is fairly self-explanatory, whereas r1581 prints back
val nearest = fn: real * real -> (real * real) * (real * real) list -> real * (real
- real)
I can't see a way to fix the bug and still keep the old printing of types with abbreviations. The problem is that the language definition does not consider printing at all.
Well, after thinking some more about it overnight I did realise there was an alternative fix for the bug that kept the old printing. I've committed this and now the old printing has been restored.
I was actually on the point of releasing 5.5 and I've already rebuilt the compilers. I can see that it would be preferable to include this latest change in the 5.5 release especially if you are processing the output automatically. I might just hold off a little bit longer.
David
On 06/09/12 11:19, David Matthews wrote:
On 05/09/2012 18:07, David Matthews wrote:
On 05/09/2012 14:27, Phil Clayton wrote:
I probably spoke a bit too soon here. After more interactive use, it appears that records and tuples can be expanded one level in the types printed back. This can make types much harder to read which may be an issue for those using an interactive session to e.g. inspect expression types by evaluating fragments of code. With the example at the end, 5.4 prints back
val nearest = fn: point -> point list1 -> real * point
which is fairly self-explanatory, whereas r1581 prints back
val nearest = fn: real * real -> (real * real) * (real * real) list -> real * (real
- real)
I can't see a way to fix the bug and still keep the old printing of types with abbreviations. The problem is that the language definition does not consider printing at all.
Well, after thinking some more about it overnight I did realise there was an alternative fix for the bug that kept the old printing. I've committed this and now the old printing has been restored.
Thanks for this. I have to say the old printing makes interactive work easier. Also, this update reduces time to compile the auto-generated libraries of function bindings - 7.2s vs 8.6s.
I was actually on the point of releasing 5.5 and I've already rebuilt the compilers. I can see that it would be preferable to include this latest change in the 5.5 release especially if you are processing the output automatically. I might just hold off a little bit longer.
And even if output isn't being processed automatically, the more succinct compiler output generally makes life easier. I'll continue with r1592 and see how it goes. I haven't found it to be worse than r1591 in any respect yet.
Phil
On 05/09/12 18:07, David Matthews wrote:
On 05/09/2012 14:27, Phil Clayton wrote:
I probably spoke a bit too soon here. After more interactive use, it appears that records and tuples can be expanded one level in the types printed back. ...
It really ought to be unwinding any type abbreviations into their right hand sides. Perhaps it is only applying it once rather than repeatedly but that needs to be fixed. ...
Interesting. So I think there is still an issue. The attached example test-3 has two levels of phantom type and is accepted by MLton and HaMLet but not Poly/ML - neither the latest r1592, nor its predecessors with the previous fix (including r1581 that I was testing).
This doesn't affect me. I just mentioned it in case it help guide you towards a particular solution.
Phil
On 06/09/2012 14:17, Phil Clayton wrote:
Interesting. So I think there is still an issue. The attached example test-3 has two levels of phantom type and is accepted by MLton and HaMLet but not Poly/ML - neither the latest r1592, nor its predecessors with the previous fix (including r1581 that I was testing).
This doesn't affect me. I just mentioned it in case it help guide you towards a particular solution.
Thanks. I was on the right lines; just hadn't gone far enough. The latest fix (1593) seems to work and I've included your example in the regression test. What set me thinking about this was trying an example: type 'a t = int; fun f (x: real t) y = x = y; This works in 5.4.1 even though it's actually very similar to the bugs you reported. If "real" was actually present on the right hand side of the abbreviation then "real t" would not be an equality type. Poly/ML was handling equality differently to other properties because of the need to handle "ref" specially for equality.
David
-
David.Matthews＠prolingua.co.uk -
matthew.fluet＠gmail.com -
phil.clayton＠lineone.net -
rda＠lemma-one.com