[CakeML] Interaction of signature annotations and value restrictions

[Ramana Kumar]

Accepting both examples is the right thing to do (and that is what the SML
definition says).

Which means you can't check the signature before or after; the checking
must be interleaved somehow (or another strategy altogether).

On 11 November 2015 at 13:50, Yong Kiam <tanyongkiam at gmail.com> wrote:

> That seems to be at odds with my example i.e. whether we type check before
> constraining to signature (accepting this example) or the other way around
> (accepting my example).
>
> So maybe this should be considered a feature, not a bug of the type system?
>
> Also, Poly/ML accepts both.
>
> On Wed, Nov 11, 2015 at 9:16 PM, Ramana Kumar <Ramana.Kumar at cl.cam.ac.uk>
> wrote:
>
>> Type annotations do not solve this problem.
>>
>> Consider:
>>
>> structure foo :> sig val f : int -> int; val g : unit end = struct
>> fun f x = x;
>> val g = f ();
>> end
>>
>> This should type check, but adding annotations will make it fail.
>>
>> (Example from discussion with Scott and Magnus.)
>>
>> On 5 October 2015 at 23:03, Michael Norrish <Michael.Norrish at nicta.com.au
>> > wrote:
>>
>>> Some type annotations are parsed but the PtreeConversion process ignores
>>> them.
>>>
>>> Michael
>>>
>>> > On 5 Oct 2015, at 23:02, Scott Owens <S.A.Owens at kent.ac.uk> wrote:
>>> >
>>> > I tried out the example on Moscow ML and MLton where it works, and on
>>> SML/NJ where you get a type error. I agree that it would be nice to get
>>> this example to work, or at least to have type annotations so that the
>>> programmer could put annotations in the structure themselves. I think I
>>> know how to add type annotations, but it hasn’t ever become high-priority.
>>> >
>>> > -Scott
>>> >
>>> >> On 2015/10/04, at 04:40, Yong Kiam <tanyongkiam at gmail.com> wrote:
>>> >>
>>> >> Hi all,
>>> >>
>>> >> Here's an interesting bug/feature of CakeML's type system due to the
>>> way signatures are handled (and the value restriction):
>>> >>
>>> >> Consider:
>>> >>
>>> >> structure foo :> sig val f : int list -> int list ref val z:int list
>>> ref end =
>>> >> struct fun f x = ref x val z = f [] end
>>> >>
>>> >> Without the signature, the declaration val z = f [] violates the
>>> value restriction and doesn't type check.
>>> >>
>>> >> This makes the declaration of foo a type error in the current CakeML
>>> type system implementation because we first type check the structure before
>>> constraining it with the signature.
>>> >>
>>> >> This is accepted in Poly/ML (not sure about other ML implementations):
>>> >>> structure foo :> sig val f : int list -> int list ref val z:int list
>>> ref end = struct fun f x = ref x val z = f [] end;
>>> >> structure foo : sig val f : int list -> int list ref val z : int list
>>> ref end
>>> >>
>>> >> There might be an easy fix if we have type annotations: convert the
>>> annotations in signatures to actual annotations on the structure's values
>>> before type checking.
>>> >>
>>> >> _______________________________________________
>>> >> Users mailing list
>>> >> Users at cakeml.org
>>> >> https://lists.cakeml.org/listinfo/users
>>> >
>>> > _______________________________________________
>>> > Users mailing list
>>> > Users at cakeml.org
>>> > https://lists.cakeml.org/listinfo/users
>>>
>>> ________________________________
>>>
>>> The information in this e-mail may be confidential and subject to legal
>>> professional privilege and/or copyright. National ICT Australia Limited
>>> accepts no liability for any damage caused by this email or its attachments.
>>>
>>> _______________________________________________
>>> Users mailing list
>>> Users at cakeml.org
>>> https://lists.cakeml.org/listinfo/users
>>>
>>
>>
>> _______________________________________________
>> Users mailing list
>> Users at cakeml.org
>> https://lists.cakeml.org/listinfo/users
>>
>>
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <https://lists.cakeml.org/pipermail/users/attachments/20151111/931f31f6/attachment-0001.html>