[CakeML] Interaction of signature annotations and value restrictions

[Ramana Kumar]

Type annotations do not solve this problem.

Consider:

structure foo :> sig val f : int -> int; val g : unit end = struct
fun f x = x;
val g = f ();
end

This should type check, but adding annotations will make it fail.

(Example from discussion with Scott and Magnus.)

On 5 October 2015 at 23:03, Michael Norrish <Michael.Norrish at nicta.com.au>
wrote:

> Some type annotations are parsed but the PtreeConversion process ignores
> them.
>
> Michael
>
> > On 5 Oct 2015, at 23:02, 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
>
> ________________________________
>
> The information in this e-mail may be confidential and subject to legal
> professional privilege and/or copyright. National ICT Australia Limited
> accepts no liability for any damage caused by this email or its attachments.
>
> _______________________________________________
> 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/20151111/b92506fc/attachment.html>