[CakeML] Interaction of signature annotations and value restrictions
tanyongkiam at gmail.com
Sun Oct 4 03:40:11 UTC 2015
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
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
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.
-------------- next part --------------
An HTML attachment was scrubbed...
More information about the Users