[CakeML] Interaction of signature annotations and value restrictions
Yong Kiam
tanyongkiam at gmail.com
Sun Oct 4 03:40:11 UTC 2015
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.
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <https://lists.cakeml.org/pipermail/users/attachments/20151004/89696e2f/attachment.html>
More information about the Users
mailing list