<div dir="ltr"><div>I agree that type annotations would be nice. I made an issue for it: <a href="https://github.com/CakeML/cakeml/issues/84">https://github.com/CakeML/cakeml/issues/84</a>.<br><br></div>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.<br></div><div class="gmail_extra"><br><div class="gmail_quote">On 5 October 2015 at 23:00, Scott Owens <span dir="ltr"><<a href="mailto:S.A.Owens@kent.ac.uk" target="_blank">S.A.Owens@kent.ac.uk</a>></span> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">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.<br>
<br>
-Scott<br>
<div><div class="h5"><br>
> On 2015/10/04, at 04:40, Yong Kiam <<a href="mailto:tanyongkiam@gmail.com">tanyongkiam@gmail.com</a>> wrote:<br>
><br>
> Hi all,<br>
><br>
> Here's an interesting bug/feature of CakeML's type system due to the way signatures are handled (and the value restriction):<br>
><br>
> Consider:<br>
><br>
> structure foo :> sig val f : int list -> int list ref val z:int list ref end =<br>
> struct fun f x = ref x val z = f [] end<br>
><br>
> Without the signature, the declaration val z = f [] violates the value restriction and doesn't type check.<br>
><br>
> 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.<br>
><br>
> This is accepted in Poly/ML (not sure about other ML implementations):<br>
> > 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;<br>
> structure foo : sig val f : int list -> int list ref val z : int list ref end<br>
><br>
> 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.<br>
><br>
</div></div>> _______________________________________________<br>
> Users mailing list<br>
> <a href="mailto:Users@cakeml.org">Users@cakeml.org</a><br>
> <a href="https://lists.cakeml.org/listinfo/users" rel="noreferrer" target="_blank">https://lists.cakeml.org/listinfo/users</a><br>
<br>
_______________________________________________<br>
Users mailing list<br>
<a href="mailto:Users@cakeml.org">Users@cakeml.org</a><br>
<a href="https://lists.cakeml.org/listinfo/users" rel="noreferrer" target="_blank">https://lists.cakeml.org/listinfo/users</a><br>
</blockquote></div><br></div>