[CakeML] Interaction of signature annotations and value restrictions

[Yong Kiam]

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/84364991/attachment.html>