Hi,
Is the following behavior (of Poly/ML 5.6) intended?
datatype ''a t = C of ''a;
datatype 'a t = C of ''b
Moreover, Poly/ML rejects a following
C 1.0;
while SML/NJ accepts it.
Best, Tjark
On 16/09/2016 16:12, Tjark Weber wrote:
Hi,
Is the following behavior (of Poly/ML 5.6) intended?
datatype ''a t = C of ''a;
datatype 'a t = C of ''b
I'll look at the printing here. There was a change in 5.5 that seems to have broken it.
Moreover, Poly/ML rejects a following
C 1.0;
while SML/NJ accepts it.
I've checked hamlet and mlton and they both reject it so I think in this case Poly/ML is right and SML/NJ is wrong. I can't point to the bit of the definition that says that, though.
Regards, David
David,
On 16 Sep 2016, at 19:19, David Matthews <David.Matthews at prolingua.co.uk> wrote:
I've checked hamlet and mlton and they both reject it so I think in this case Poly/ML is right and SML/NJ is wrong. I can't point to the bit of the definition that says that, though.
It's in Appendix C: "Of [the type names listed in the initial static basis] all except exn and real admit equality".
Regards,
Rob.
Rob, Actually what I was trying to find was the bit that says that the equality attribute in a type variable used as a datatype parameter should be honoured where it isn't when used as a type parameter.
type ''a t = ''a * ''a;
type 'a t = 'a * 'a
(1.0, 2.0): real t;
val it = (1.0, 2.0): real t
datatype ''a t = C of ''a;
datatype 'a t = C of ''b <<<< This prints wrongly
C 1.0;
poly: : error: Type error in function application. Function: C : ''a -> ''a t Argument: 1.0 : real Reason: Can't unify ''a to real (Requires equality type) Found near C 1.0 Static Errors
I'm sure I looked into this a long time ago and a check with hamlet agrees with Poly/ML so I'm confident it's right; I just haven't been able to find the reference.
Regards, David
On 16/09/2016 20:18, Rob Arthan wrote:
David,
On 16 Sep 2016, at 19:19, David Matthews <David.Matthews at prolingua.co.uk> wrote:
I've checked hamlet and mlton and they both reject it so I think in this case Poly/ML is right and SML/NJ is wrong. I can't point to the bit of the definition that says that, though.
It's in Appendix C: "Of [the type names listed in the initial static basis] all except exn and real admit equality".
Regards,
Rob.
polyml mailing list polyml at inf.ed.ac.uk http://lists.inf.ed.ac.uk/mailman/listinfo/polyml
Hello,
Besides any printing/elaboration problem with polyml 5.6:
In polyml 5.5:
datatype ''a t = C of ''a;
datatype ''a t = C of ''a
C 1.0;
Error-Type error in function application. Function: C : ''a -> ''a t Argument: 1.0 : real Reason: Can't unify ''a to real (Requires equality type) Found near C 1.0 Static Errors
In sml-nj 110.77:
- datatype ''a t = C of ''a; datatype 'a t = C of 'a - C 1.0; val it = C 1.0 : real t
polyml interprets the type variable ''a in the declaration of t as an equality type, while sml-nj interprets it as a regular type variable.
I like the treatment of polyML :-), but I guess it is not standard:
The "definition" (http://sml-family.org/sml97-defn.pdf) says, page 19: "... In particular, the equality attribute has no significance in a bound variable of a type function; for example ... "
So, unless I'm mistaken, sml-nj is right.
Bernard.
On 9/16/16 9:41 PM, David Matthews wrote:
Rob, Actually what I was trying to find was the bit that says that the equality attribute in a type variable used as a datatype parameter should be honoured where it isn't when used as a type parameter.
type ''a t = ''a * ''a;
type 'a t = 'a * 'a
(1.0, 2.0): real t;
val it = (1.0, 2.0): real t
datatype ''a t = C of ''a;
datatype 'a t = C of ''b <<<< This prints wrongly
C 1.0;
poly: : error: Type error in function application. Function: C : ''a -> ''a t Argument: 1.0 : real Reason: Can't unify ''a to real (Requires equality type) Found near C 1.0 Static Errors
I'm sure I looked into this a long time ago and a check with hamlet agrees with Poly/ML so I'm confident it's right; I just haven't been able to find the reference.
Regards, David
On 16/09/2016 20:18, Rob Arthan wrote:
David,
On 16 Sep 2016, at 19:19, David Matthews <David.Matthews at prolingua.co.uk> wrote:
I've checked hamlet and mlton and they both reject it so I think in this case Poly/ML is right and SML/NJ is wrong. I can't point to the bit of the definition that says that, though.
It's in Appendix C: "Of [the type names listed in the initial static basis] all except exn and real admit equality".
Regards,
Rob.
polyml mailing list polyml at inf.ed.ac.uk http://lists.inf.ed.ac.uk/mailman/listinfo/polyml
polyml mailing list polyml at inf.ed.ac.uk http://lists.inf.ed.ac.uk/mailman/listinfo/polyml
On 16 Sep 2016, at 20:59, Bernard Berthomieu <Bernard.Berthomieu at laas.fr> wrote:
... I like the treatment of polyML :-), but I guess it is not standard:
The "definition" (http://sml-family.org/sml97-defn.pdf) says, page 19: "... In particular, the equality attribute has no significance in a bound variable of a type function; for example ... "
So, unless I'm mistaken, sml-nj is right.
That's interesting. The text you quote is pretty clear, but how is it consistent with the static semantics of constructor bindings on p29, which I read as saying that in Tjark's example: datatype ''a t = C of ''a, C gets type ''a -> ''a t?
Regards,
Rob.
Bernard, That refers to a "type function" not a datatype binding. type ''a t = ''a * ''a creates a type function and indeed Poly/ML ignores the equality attribute in that case. A datatype binding creates a new "type name" and that is dealt with elsewhere.
The fact that both mlton and hamlet behave the same way as Poly/ML makes me feel confident that it is SML/NJ that is wrong. Hamlet is based very closely on the semantics so it's usually the best way of checking out these sorts of questions.
Regards, David
On 16/09/2016 20:59, Bernard Berthomieu wrote:
Hello,
Besides any printing/elaboration problem with polyml 5.6:
In polyml 5.5:
datatype ''a t = C of ''a;
datatype ''a t = C of ''a
C 1.0;
Error-Type error in function application. Function: C : ''a -> ''a t Argument: 1.0 : real Reason: Can't unify ''a to real (Requires equality type) Found near C 1.0 Static Errors
In sml-nj 110.77:
- datatype ''a t = C of ''a;
datatype 'a t = C of 'a
- C 1.0;
val it = C 1.0 : real t
polyml interprets the type variable ''a in the declaration of t as an equality type, while sml-nj interprets it as a regular type variable.
I like the treatment of polyML :-), but I guess it is not standard:
The "definition" (http://sml-family.org/sml97-defn.pdf) says, page 19: "... In particular, the equality attribute has no significance in a bound variable of a type function; for example ... "
So, unless I'm mistaken, sml-nj is right.
Bernard.
On 9/16/16 9:41 PM, David Matthews wrote:
Rob, Actually what I was trying to find was the bit that says that the equality attribute in a type variable used as a datatype parameter should be honoured where it isn't when used as a type parameter.
type ''a t = ''a * ''a;
type 'a t = 'a * 'a
(1.0, 2.0): real t;
val it = (1.0, 2.0): real t
datatype ''a t = C of ''a;
datatype 'a t = C of ''b <<<< This prints wrongly
C 1.0;
poly: : error: Type error in function application. Function: C : ''a -> ''a t Argument: 1.0 : real Reason: Can't unify ''a to real (Requires equality type) Found near C 1.0 Static Errors
I'm sure I looked into this a long time ago and a check with hamlet agrees with Poly/ML so I'm confident it's right; I just haven't been able to find the reference.
Regards, David
On 16/09/2016 20:18, Rob Arthan wrote:
David,
On 16 Sep 2016, at 19:19, David Matthews <David.Matthews at prolingua.co.uk> wrote:
I've checked hamlet and mlton and they both reject it so I think in this case Poly/ML is right and SML/NJ is wrong. I can't point to the bit of the definition that says that, though.
It's in Appendix C: "Of [the type names listed in the initial static basis] all except exn and real admit equality".
Regards,
Rob.
polyml mailing list polyml at inf.ed.ac.uk http://lists.inf.ed.ac.uk/mailman/listinfo/polyml
polyml mailing list polyml at inf.ed.ac.uk http://lists.inf.ed.ac.uk/mailman/listinfo/polyml
David,
Yes, you are right; p19 applies to type functions (abbreviations), not to type constructors introduced by datatype. My understanding was that both obeyed the same rule, but I guess it is not the case (can't find anything about it in the book ..). mlton also rejects (C 1.0), by the way.
BB.
On 9/16/16 10:25 PM, David Matthews wrote:
Bernard, That refers to a "type function" not a datatype binding. type ''a t = ''a * ''a creates a type function and indeed Poly/ML ignores the equality attribute in that case. A datatype binding creates a new "type name" and that is dealt with elsewhere.
The fact that both mlton and hamlet behave the same way as Poly/ML makes me feel confident that it is SML/NJ that is wrong. Hamlet is based very closely on the semantics so it's usually the best way of checking out these sorts of questions.
Regards, David
On 16/09/2016 20:59, Bernard Berthomieu wrote:
Hello,
Besides any printing/elaboration problem with polyml 5.6:
In polyml 5.5:
datatype ''a t = C of ''a;
datatype ''a t = C of ''a
C 1.0;
Error-Type error in function application. Function: C : ''a -> ''a t Argument: 1.0 : real Reason: Can't unify ''a to real (Requires equality type) Found near C 1.0 Static Errors
In sml-nj 110.77:
- datatype ''a t = C of ''a;
datatype 'a t = C of 'a
- C 1.0;
val it = C 1.0 : real t
polyml interprets the type variable ''a in the declaration of t as an equality type, while sml-nj interprets it as a regular type variable.
I like the treatment of polyML :-), but I guess it is not standard:
The "definition" (http://sml-family.org/sml97-defn.pdf) says, page 19: "... In particular, the equality attribute has no significance in a bound variable of a type function; for example ... "
So, unless I'm mistaken, sml-nj is right.
Bernard.
On 9/16/16 9:41 PM, David Matthews wrote:
Rob, Actually what I was trying to find was the bit that says that the equality attribute in a type variable used as a datatype parameter should be honoured where it isn't when used as a type parameter.
type ''a t = ''a * ''a;
type 'a t = 'a * 'a
(1.0, 2.0): real t;
val it = (1.0, 2.0): real t
datatype ''a t = C of ''a;
datatype 'a t = C of ''b <<<< This prints wrongly
C 1.0;
poly: : error: Type error in function application. Function: C : ''a -> ''a t Argument: 1.0 : real Reason: Can't unify ''a to real (Requires equality type) Found near C 1.0 Static Errors
I'm sure I looked into this a long time ago and a check with hamlet agrees with Poly/ML so I'm confident it's right; I just haven't been able to find the reference.
Regards, David
On 16/09/2016 20:18, Rob Arthan wrote:
David,
On 16 Sep 2016, at 19:19, David Matthews <David.Matthews at prolingua.co.uk> wrote:
I've checked hamlet and mlton and they both reject it so I think in this case Poly/ML is right and SML/NJ is wrong. I can't point to the bit of the definition that says that, though.
It's in Appendix C: "Of [the type names listed in the initial static basis] all except exn and real admit equality".
Regards,
Rob.
polyml mailing list polyml at inf.ed.ac.uk http://lists.inf.ed.ac.uk/mailman/listinfo/polyml
polyml mailing list polyml at inf.ed.ac.uk http://lists.inf.ed.ac.uk/mailman/listinfo/polyml
Hello,
Funnily (where my belief came from ?), the page about equality type variables on mlton.org (http://mlton.org/EqualityTypeVariable) says that they play no special role in either type bindings or datatype bindings, contradicting the compiler ...
BB.
On 9/16/16 10:42 PM, Bernard Berthomieu wrote:
David,
Yes, you are right; p19 applies to type functions (abbreviations), not to type constructors introduced by datatype. My understanding was that both obeyed the same rule, but I guess it is not the case (can't find anything about it in the book ..). mlton also rejects (C 1.0), by the way.
BB.
On 9/16/16 10:25 PM, David Matthews wrote:
Bernard, That refers to a "type function" not a datatype binding. type ''a t = ''a * ''a creates a type function and indeed Poly/ML ignores the equality attribute in that case. A datatype binding creates a new "type name" and that is dealt with elsewhere.
The fact that both mlton and hamlet behave the same way as Poly/ML makes me feel confident that it is SML/NJ that is wrong. Hamlet is based very closely on the semantics so it's usually the best way of checking out these sorts of questions.
Regards, David
On 16/09/2016 20:59, Bernard Berthomieu wrote:
Hello,
Besides any printing/elaboration problem with polyml 5.6:
In polyml 5.5:
datatype ''a t = C of ''a;
datatype ''a t = C of ''a
C 1.0;
Error-Type error in function application. Function: C : ''a -> ''a t Argument: 1.0 : real Reason: Can't unify ''a to real (Requires equality type) Found near C 1.0 Static Errors
In sml-nj 110.77:
- datatype ''a t = C of ''a;
datatype 'a t = C of 'a
- C 1.0;
val it = C 1.0 : real t
polyml interprets the type variable ''a in the declaration of t as an equality type, while sml-nj interprets it as a regular type variable.
I like the treatment of polyML :-), but I guess it is not standard:
The "definition" (http://sml-family.org/sml97-defn.pdf) says, page 19: "... In particular, the equality attribute has no significance in a bound variable of a type function; for example ... "
So, unless I'm mistaken, sml-nj is right.
Bernard.
On 9/16/16 9:41 PM, David Matthews wrote:
Rob, Actually what I was trying to find was the bit that says that the equality attribute in a type variable used as a datatype parameter should be honoured where it isn't when used as a type parameter.
type ''a t = ''a * ''a;
type 'a t = 'a * 'a
(1.0, 2.0): real t;
val it = (1.0, 2.0): real t
datatype ''a t = C of ''a;
datatype 'a t = C of ''b <<<< This prints wrongly
C 1.0;
poly: : error: Type error in function application. Function: C : ''a -> ''a t Argument: 1.0 : real Reason: Can't unify ''a to real (Requires equality type) Found near C 1.0 Static Errors
I'm sure I looked into this a long time ago and a check with hamlet agrees with Poly/ML so I'm confident it's right; I just haven't been able to find the reference.
Regards, David
On 16/09/2016 20:18, Rob Arthan wrote:
David,
On 16 Sep 2016, at 19:19, David Matthews <David.Matthews at prolingua.co.uk> wrote:
I've checked hamlet and mlton and they both reject it so I think in this case Poly/ML is right and SML/NJ is wrong. I can't point to the bit of the definition that says that, though.
It's in Appendix C: "Of [the type names listed in the initial static basis] all except exn and real admit equality".
Regards,
Rob.
polyml mailing list polyml at inf.ed.ac.uk http://lists.inf.ed.ac.uk/mailman/listinfo/polyml
polyml mailing list polyml at inf.ed.ac.uk http://lists.inf.ed.ac.uk/mailman/listinfo/polyml
polyml mailing list polyml at inf.ed.ac.uk http://lists.inf.ed.ac.uk/mailman/listinfo/polyml
I think that the reasoning is that the type function induced by a datatype (which maps the type variables to the fresh type name) is ignorant of equality type variables, but the type schemes induced by the constructors do respect equality type variables.
Thus, with
datatype ('a, ''b) t = A of 'a | B of ''b
both
fun f (x: (int, real) t) = x
and
val l : ((int, real) t) list = []
type check (with MLton), since "(int, real) t" can always be successfully elaborated.
As noted previously,
val t1 = B 1.0
does not type check, because the type scheme of C cannot be instantiated with "real", a non-equality type.
At first, I was surprised by the following
val t2 : (int, real) t = A 1
which does not type check; in MLton, we report:
Pattern and expression disagree. pattern: (_, [<non-equality>]) t expression: (_, [<equality>]) t in: t2: (int, real) t = A 1
But, this is fine --- the type annotation on the pattern successfully elaborates, but type inference of the expression (constructor A applied to 1) yields "(int, ''B) t" for some fresh unification type variable ''B and this unification type variable is an equality type variable and cannot be unified with "real".
-Matthew
On Sat, Sep 17, 2016 at 4:43 AM, Bernard Berthomieu <Bernard.Berthomieu at laas.fr> wrote:
Hello,
Funnily (where my belief came from ?), the page about equality type variables on mlton.org (http://mlton.org/EqualityTypeVariable) says that they play no special role in either type bindings or datatype bindings, contradicting the compiler ...
BB.
On 9/16/16 10:42 PM, Bernard Berthomieu wrote:
David,
Yes, you are right; p19 applies to type functions (abbreviations), not to type constructors introduced by datatype. My understanding was that both obeyed the same rule, but I guess it is not the case (can't find anything about it in the book ..). mlton also rejects (C 1.0), by the way.
BB.
On 9/16/16 10:25 PM, David Matthews wrote:
Bernard, That refers to a "type function" not a datatype binding. type ''a t = ''a * ''a creates a type function and indeed Poly/ML ignores the equality attribute in that case. A datatype binding creates a new "type name" and that is dealt with elsewhere.
The fact that both mlton and hamlet behave the same way as Poly/ML makes me feel confident that it is SML/NJ that is wrong. Hamlet is based very closely on the semantics so it's usually the best way of checking out these sorts of questions.
Regards, David
On 16/09/2016 20:59, Bernard Berthomieu wrote:
Hello,
Besides any printing/elaboration problem with polyml 5.6:
In polyml 5.5:
datatype ''a t = C of ''a;
datatype ''a t = C of ''a
C 1.0;
Error-Type error in function application. Function: C : ''a -> ''a t Argument: 1.0 : real Reason: Can't unify ''a to real (Requires equality type) Found near C 1.0 Static Errors
In sml-nj 110.77:
- datatype ''a t = C of ''a;
datatype 'a t = C of 'a
- C 1.0;
val it = C 1.0 : real t
polyml interprets the type variable ''a in the declaration of t as an equality type, while sml-nj interprets it as a regular type variable.
I like the treatment of polyML :-), but I guess it is not standard:
The "definition" (http://sml-family.org/sml97-defn.pdf) says, page 19: "... In particular, the equality attribute has no significance in a bound variable of a type function; for example ... "
So, unless I'm mistaken, sml-nj is right.
Bernard.
On 9/16/16 9:41 PM, David Matthews wrote:
Rob, Actually what I was trying to find was the bit that says that the equality attribute in a type variable used as a datatype parameter should be honoured where it isn't when used as a type parameter.
type ''a t = ''a * ''a;
type 'a t = 'a * 'a
(1.0, 2.0): real t;
val it = (1.0, 2.0): real t
datatype ''a t = C of ''a;
datatype 'a t = C of ''b <<<< This prints wrongly
C 1.0;
poly: : error: Type error in function application. Function: C : ''a -> ''a t Argument: 1.0 : real Reason: Can't unify ''a to real (Requires equality type) Found near C 1.0 Static Errors
I'm sure I looked into this a long time ago and a check with hamlet agrees with Poly/ML so I'm confident it's right; I just haven't been able to find the reference.
Regards, David
On 16/09/2016 20:18, Rob Arthan wrote:
David,
On 16 Sep 2016, at 19:19, David Matthews <David.Matthews at prolingua.co.uk> wrote:
I've checked hamlet and mlton and they both reject it so I think in this case Poly/ML is right and SML/NJ is wrong. I can't point to the bit of the definition that says that, though.
It's in Appendix C: "Of [the type names listed in the initial static basis] all except exn and real admit equality".
Regards,
Rob.
polyml mailing list polyml at inf.ed.ac.uk http://lists.inf.ed.ac.uk/mailman/listinfo/polyml
polyml mailing list polyml at inf.ed.ac.uk http://lists.inf.ed.ac.uk/mailman/listinfo/polyml
polyml mailing list polyml at inf.ed.ac.uk http://lists.inf.ed.ac.uk/mailman/listinfo/polyml
polyml mailing list polyml at inf.ed.ac.uk http://lists.inf.ed.ac.uk/mailman/listinfo/polyml
Many thanks Matthew for the clarification. Subtle :-)
Since datatype declarations declare both a type operator and constructors, I think the explanation deserves to appear in http://mlton.org/EqualityTypeVariable, last part. The last two declarations declare identical type operators, but not identical constructors, right ?
Bernard.
On 9/17/16 1:42 PM, Matthew Fluet wrote:
I think that the reasoning is that the type function induced by a datatype (which maps the type variables to the fresh type name) is ignorant of equality type variables, but the type schemes induced by the constructors do respect equality type variables.
Thus, with
datatype ('a, ''b) t = A of 'a | B of ''b
both
fun f (x: (int, real) t) = x
and
val l : ((int, real) t) list = []
type check (with MLton), since "(int, real) t" can always be successfully elaborated.
As noted previously,
val t1 = B 1.0
does not type check, because the type scheme of C cannot be instantiated with "real", a non-equality type.
At first, I was surprised by the following
val t2 : (int, real) t = A 1
which does not type check; in MLton, we report:
Pattern and expression disagree. pattern: (_, [<non-equality>]) t expression: (_, [<equality>]) t in: t2: (int, real) t = A 1
But, this is fine --- the type annotation on the pattern successfully elaborates, but type inference of the expression (constructor A applied to 1) yields "(int, ''B) t" for some fresh unification type variable ''B and this unification type variable is an equality type variable and cannot be unified with "real".
-Matthew
-
Bernard.Berthomieu＠laas.fr -
David.Matthews＠prolingua.co.uk -
matthew.fluet＠gmail.com -
robarthan1＠googlemail.com -
tjark.weber＠it.uu.se