[CakeML] Interaction of signature annotations and value restrictions

[Yong Kiam]

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/1936b439/attachment.html>