<div dir="ltr"><div>That seems to be at odds with my example i.e. whether we type check before constraining to signature (accepting this example) or the other way around (accepting my example).</div><div><br></div><div>So maybe this should be considered a feature, not a bug of the type system?</div><div><br></div><div>Also, Poly/ML accepts both.</div></div><div class="gmail_extra"><br><div class="gmail_quote">On Wed, Nov 11, 2015 at 9:16 PM, Ramana Kumar <span dir="ltr"><<a href="mailto:Ramana.Kumar@cl.cam.ac.uk" target="_blank">Ramana.Kumar@cl.cam.ac.uk</a>></span> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><div dir="ltr"><div><div><div><div><div>Type annotations do not solve this problem.<br><br></div>Consider:<br><br></div>structure foo :> sig val f : int -> int; val g : unit end = struct<br></div>fun f x = x;<br>val g = f ();<br>end<br><br></div>This should type check, but adding annotations will make it fail.<br><br></div>(Example from discussion with Scott and Magnus.)<br></div><div class="HOEnZb"><div class="h5"><div class="gmail_extra"><br><div class="gmail_quote">On 5 October 2015 at 23:03, Michael Norrish <span dir="ltr"><<a href="mailto:Michael.Norrish@nicta.com.au" target="_blank">Michael.Norrish@nicta.com.au</a>></span> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">Some type annotations are parsed but the PtreeConversion process ignores them.<br>
<br>
Michael<br>
<div><div><br>
> On 5 Oct 2015, at 23:02, Scott Owens <<a href="mailto:S.A.Owens@kent.ac.uk" target="_blank">S.A.Owens@kent.ac.uk</a>> wrote:<br>
><br>
> 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>
><br>
>> On 2015/10/04, at 04:40, Yong Kiam <<a href="mailto:tanyongkiam@gmail.com" target="_blank">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>
>> _______________________________________________<br>
>> Users mailing list<br>
>> <a href="mailto:Users@cakeml.org" target="_blank">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" target="_blank">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>
</div></div>________________________________<br>
<br>
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.<br>
<div><div><br>
_______________________________________________<br>
Users mailing list<br>
<a href="mailto:Users@cakeml.org" target="_blank">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>
</div></div></blockquote></div><br></div>
</div></div><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>
<br></blockquote></div><br></div>