[CakeML] Interaction of signature annotations and value restrictions
Michael.Norrish at nicta.com.au
Mon Oct 5 22:03:14 UTC 2015
Some type annotations are parsed but the PtreeConversion process ignores them.
> 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.
>> 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):
>> 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
> Users mailing list
> Users at cakeml.org
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.
More information about the Users