[CakeML] Interaction of signature annotations and value restrictions

[Ramana Kumar]

Yes, you're right. It's about the modularity on which the value restriction
is applied (single declarations versus whole modules).

On 11 November 2015 at 15:31, Yong Kiam <tanyongkiam at gmail.com> wrote:

> I think this is related to how we can type this using unification
> variables:
>
> let
> fun f x = ref x
> val z = f [] in
> 5::(!z)
> end
>
> In my first example, it wasn't necessary that the type of f is
> constrained, as long as the type of z is constrained it ends up fine.
>
> Similarly,
>
> structure foo = struct fun f x = ref x val z = f [] val g = 5::(!z) end;
>
> type checks fine (but not in CakeML).
>
> So the problem is that we are treating a whole module declaration as
> though it were a "REPL" where we are expecting to run the module line by
> line without knowledge of future lines.
>
> Instead, the current uniqueness and most-general value restrictions should
> probably be applied after signatures are applied.
>
> I don't have a good idea about how to do this for the inferencer though, I
> guess the ungeneralized unification variables have to be kept around
> somehow...
>
>
>
> On Wed, Nov 11, 2015 at 10:33 PM, Ramana Kumar <Ramana.Kumar at cl.cam.ac.uk>
> wrote:
>
>> Accepting both examples is the right thing to do (and that is what the
>> SML definition says).
>>
>> Which means you can't check the signature before or after; the checking
>> must be interleaved somehow (or another strategy altogether).
>>
>>
>> On 11 November 2015 at 13:50, Yong Kiam <tanyongkiam at gmail.com> wrote:
>>
>>> 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).
>>>
>>> So maybe this should be considered a feature, not a bug of the type
>>> system?
>>>
>>> Also, Poly/ML accepts both.
>>>
>>> On Wed, Nov 11, 2015 at 9:16 PM, Ramana Kumar <Ramana.Kumar at cl.cam.ac.uk
>>> > wrote:
>>>
>>>> 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
>>>>>
>>>>
>>>>
>>>> _______________________________________________
>>>> 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/e5cb2b18/attachment-0001.html>