[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