[CakeML] Interaction of signature annotations and value restrictions

[Scott Owens]

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