[CakeML] Interaction of signature annotations and value restrictions

[Michael Norrish]

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.