[CakeML] Interaction of signature annotations and value restrictions

[Ramana Kumar]

I agree that type annotations would be nice. I made an issue for it:
https://github.com/CakeML/cakeml/issues/84.

I also agree that apart from type annotations, we should constrain to
signature before failing due to value restriction. Adding implicit type
annotations, as Yong Kiam suggested, might be an easy way to do that.

On 5 October 2015 at 23:00, 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.
>
> -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
>
> _______________________________________________
> Users mailing list
> Users at cakeml.org
> https://lists.cakeml.org/listinfo/users
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <https://lists.cakeml.org/pipermail/users/attachments/20151006/2d75ce6b/attachment.html>