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

Reply via email to