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.

## Advertising

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.berthom...@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.matth...@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@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 > > > > _______________________________________________ > 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 _______________________________________________ polyml mailing list polyml@inf.ed.ac.uk http://lists.inf.ed.ac.uk/mailman/listinfo/polyml