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

Reply via email to