Re: [polyml] Equality Type Parameter in Datatype Declaration

2016-09-17 Thread Bernard Berthomieu 

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:(_, []) t
 expression: (_, []) 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




___
polyml mailing list
polyml@inf.ed.ac.uk
http://lists.inf.ed.ac.uk/mailman/listinfo/polyml

Re: [polyml] Equality Type Parameter in Datatype Declaration

2016-09-17 Thread Bernard Berthomieu 

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

Re: [polyml] Equality Type Parameter in Datatype Declaration

2016-09-16 Thread David Matthews 

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

Re: [polyml] Equality Type Parameter in Datatype Declaration

2016-09-16 Thread Rob Arthan 

> On 16 Sep 2016, at 20:59, Bernard Berthomieu  
> 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.

___
polyml mailing list
polyml@inf.ed.ac.uk
http://lists.inf.ed.ac.uk/mailman/listinfo/polyml

Re: [polyml] Equality Type Parameter in Datatype Declaration

2016-09-16 Thread Bernard Berthomieu 

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

Re: [polyml] Equality Type Parameter in Datatype Declaration

2016-09-16 Thread David Matthews 

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

Re: [polyml] Equality Type Parameter in Datatype Declaration

2016-09-16 Thread Rob Arthan 

David,

> On 16 Sep 2016, at 19:19, David Matthews  
> 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

Re: [polyml] Equality Type Parameter in Datatype Declaration

2016-09-16 Thread David Matthews 

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

[polyml] Equality Type Parameter in Datatype Declaration

2016-09-16 Thread Tjark Weber 
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


___
polyml mailing list
polyml@inf.ed.ac.uk
http://lists.inf.ed.ac.uk/mailman/listinfo/polyml