[Caml-list] Exhaustiveness, currying with GADTs

[Caml-list] Exhaustiveness, currying with GADTs

[Markus Weissmann]

Hello,

while playing around with GADTs, I came across two issues I don't understand: The exhaustiveness check and currying functions.
1.) I get a warning about my match (in function "componentwise") not being exhaustive, while imho it obviously is:

--------8<----------
  type d2
  type d3

  type _ t =
    | Vector2 : (float * float) -> d2 t
    | Vector3 : (float * float * float) -> d3 t

  let componentwise : type d . (float -> float -> float) -> d t -> d t -> d t = fun f v1 v2 ->
    match (v1, v2) with
    | (Vector2 (x1, y1), Vector2 (x2, y2)) -> Vector2 (f x1 x2, f y1  y1)
    | (Vector3 (x1, y1, z1), Vector3 (x2, y2, z2)) -> Vector3 (f x1 x2, f y1 y1, f z1 z2)
-------->8----------

2.) When I use "componentwise" for other functions, I cannot do this:

  let add = componentwise (+.)

("contains type variables that cannot be generalized")
Fair enough. But I also cannot do this:

  let add : type d . d t -> d t -> d t = componentwise (+.) 

("This definition has type 'd t -> 'd t -> 'd t which is less general than 'd0. 'd0 t -> 'd0 t -> 'd0 t")
Only the "full" version works:

  let add : type d . d t -> d t -> d t = fun v1 v2 -> componentwise (+.) v1 v2


I would be very happy if someone could shed some light especially on 1.).


Thanks & regards
-Markus

-- 
Markus Weißmann, M.Sc.
Technische Universität München
Institut für Informatik
Boltzmannstr. 3
D-85748 Garching
Germany
http://wwwknoll.in.tum.de/

Re: [Caml-list] Exhaustiveness, currying with GADTs

[Jacques Le Normand]

2) seems to be the value restriction. basically, only constructors,
composition of constructors and lambdas can generalize.

What warning are you getting for 1) ?

On Thu, Oct 11, 2012 at 10:30 AM, Markus Weissmann
<markus.weissmann@in.tum.de> wrote:
> Hello,
>
> while playing around with GADTs, I came across two issues I don't understand: The exhaustiveness check and currying functions.
> 1.) I get a warning about my match (in function "componentwise") not being exhaustive, while imho it obviously is:
>
> --------8<----------
>   type d2
>   type d3
>
>   type _ t =
>     | Vector2 : (float * float) -> d2 t
>     | Vector3 : (float * float * float) -> d3 t
>
>   let componentwise : type d . (float -> float -> float) -> d t -> d t -> d t = fun f v1 v2 ->
>     match (v1, v2) with
>     | (Vector2 (x1, y1), Vector2 (x2, y2)) -> Vector2 (f x1 x2, f y1  y1)
>     | (Vector3 (x1, y1, z1), Vector3 (x2, y2, z2)) -> Vector3 (f x1 x2, f y1 y1, f z1 z2)
> -------->8----------
>
> 2.) When I use "componentwise" for other functions, I cannot do this:
>
>   let add = componentwise (+.)
>
> ("contains type variables that cannot be generalized")
> Fair enough. But I also cannot do this:
>
>   let add : type d . d t -> d t -> d t = componentwise (+.)
>
> ("This definition has type 'd t -> 'd t -> 'd t which is less general than 'd0. 'd0 t -> 'd0 t -> 'd0 t")
> Only the "full" version works:
>
>   let add : type d . d t -> d t -> d t = fun v1 v2 -> componentwise (+.) v1 v2
>
>
> I would be very happy if someone could shed some light especially on 1.).
>
>
> Thanks & regards
> -Markus
>
> --
> Markus Weißmann, M.Sc.
> Technische Universität München
> Institut für Informatik
> Boltzmannstr. 3
> D-85748 Garching
> Germany
> http://wwwknoll.in.tum.de/
>
>
> --
> Caml-list mailing list.  Subscription management and archives:
> https://sympa.inria.fr/sympa/arc/caml-list
> Beginner's list: http://groups.yahoo.com/group/ocaml_beginners
> Bug reports: http://caml.inria.fr/bin/caml-bugs

Re: [Caml-list] Exhaustiveness, currying with GADTs

["Markus W. Weißmann"]

On 11 Oct 2012, at 21:04, Jacques Le Normand wrote:

> 2) seems to be the value restriction. basically, only constructors,
> composition of constructors and lambdas can generalize.
> 
> What warning are you getting for 1) ?
> 

File "min.ml", line 12, characters 4-187:
Warning 8: this pattern-matching is not exhaustive.
Here is an example of a value that is not matched:
(Vector3 (_, _, _), Vector2 _)


> On Thu, Oct 11, 2012 at 10:30 AM, Markus Weissmann
> <markus.weissmann@in.tum.de> wrote:
>> Hello,
>> 
>> while playing around with GADTs, I came across two issues I don't understand: The exhaustiveness check and currying functions.
>> 1.) I get a warning about my match (in function "componentwise") not being exhaustive, while imho it obviously is:
>> 
>> --------8<----------
>>  type d2
>>  type d3
>> 
>>  type _ t =
>>    | Vector2 : (float * float) -> d2 t
>>    | Vector3 : (float * float * float) -> d3 t
>> 
>>  let componentwise : type d . (float -> float -> float) -> d t -> d t -> d t = fun f v1 v2 ->
>>    match (v1, v2) with
>>    | (Vector2 (x1, y1), Vector2 (x2, y2)) -> Vector2 (f x1 x2, f y1  y1)
>>    | (Vector3 (x1, y1, z1), Vector3 (x2, y2, z2)) -> Vector3 (f x1 x2, f y1 y1, f z1 z2)
>> -------->8----------
>> 
>> 2.) When I use "componentwise" for other functions, I cannot do this:
>> 
>>  let add = componentwise (+.)
>> 
>> ("contains type variables that cannot be generalized")
>> Fair enough. But I also cannot do this:
>> 
>>  let add : type d . d t -> d t -> d t = componentwise (+.)
>> 
>> ("This definition has type 'd t -> 'd t -> 'd t which is less general than 'd0. 'd0 t -> 'd0 t -> 'd0 t")
>> Only the "full" version works:
>> 
>>  let add : type d . d t -> d t -> d t = fun v1 v2 -> componentwise (+.) v1 v2
>> 
>> 
>> I would be very happy if someone could shed some light especially on 1.).
>> 
>> 
>> Thanks & regards
>> -Markus
>> 
>> --
>> Markus Weißmann, M.Sc.
>> Technische Universität München
>> Institut für Informatik
>> Boltzmannstr. 3
>> D-85748 Garching
>> Germany
>> http://wwwknoll.in.tum.de/
>> 
>> 
>> --
>> Caml-list mailing list.  Subscription management and archives:
>> https://sympa.inria.fr/sympa/arc/caml-list
>> Beginner's list: http://groups.yahoo.com/group/ocaml_beginners
>> Bug reports: http://caml.inria.fr/bin/caml-bugs

-- 
Markus Weißmann, M.Sc.
Technische Universität München
Institut für Informatik
Boltzmannstr. 3
D-85748 Garching
Germany
Tel. +49 (89) 2 89-1 81 05
Mobil +49 151 58402057 (AUDI)
Fax +49 (89) 2 89-1 81 07
http://wwwknoll.in.tum.de/

Re: [Caml-list] Exhaustiveness, currying with GADTs

[Jacques Garrigue]

On 2012/10/12, at 2:30, Markus Weissmann <markus.weissmann@in.tum.de> wrote:

> Hello,
> 
> while playing around with GADTs, I came across two issues I don't understand: The exhaustiveness check and currying functions.
> 1.) I get a warning about my match (in function "componentwise") not being exhaustive, while imho it obviously is:
> 
> --------8<----------
>  type d2
>  type d3
> 
>  type _ t =
>    | Vector2 : (float * float) -> d2 t
>    | Vector3 : (float * float * float) -> d3 t
> 
>  let componentwise : type d . (float -> float -> float) -> d t -> d t -> d t = fun f v1 v2 ->
>    match (v1, v2) with
>    | (Vector2 (x1, y1), Vector2 (x2, y2)) -> Vector2 (f x1 x2, f y1  y1)
>    | (Vector3 (x1, y1, z1), Vector3 (x2, y2, z2)) -> Vector3 (f x1 x2, f y1 y1, f z1 z2)
> -------->8----------

If you put all your code in the same module, as you have just done here,
you don't get such a warning.
What you have probably done is defining the types in a module,
and then defined componentwise in another module.
What happens then is that the type system cannot guarantee anymore
that d2 and d3 are distinct: they are just abstract types that could
be aliases to each other.

Simple workaround: just write

type d2 = D2
type d3 = D3

Then d2 and d3 are no longer abstract, and they are clearly different.

> 2.) When I use "componentwise" for other functions, I cannot do this:
> 
>  let add = componentwise (+.)
> 
> ("contains type variables that cannot be generalized")
> Fair enough. But I also cannot do this:
> 
>  let add : type d . d t -> d t -> d t = componentwise (+.) 
> 
> ("This definition has type 'd t -> 'd t -> 'd t which is less general than 'd0. 'd0 t -> 'd0 t -> 'd0 t")
> Only the "full" version works:
> 
>  let add : type d . d t -> d t -> d t = fun v1 v2 -> componentwise (+.) v1 v2

As Jacques pointed out, this is just the value restriction at work.
The well known workaround is to eta-expand:

let add x = componentwise (+.) x


Jacques Garrigue

Re: [Caml-list] Exhaustiveness, currying with GADTs

["Markus W. Weißmann"]

On 12 Oct 2012, at 07:42, Jacques Garrigue wrote:

> On 2012/10/12, at 2:30, Markus Weissmann <markus.weissmann@in.tum.de> wrote:
> 
>> Hello,
>> 
>> while playing around with GADTs, I came across two issues I don't understand: The exhaustiveness check and currying functions.
>> 1.) I get a warning about my match (in function "componentwise") not being exhaustive, while imho it obviously is:
>> 
>> --------8<----------
>> type d2
>> type d3
>> 
>> type _ t =
>>   | Vector2 : (float * float) -> d2 t
>>   | Vector3 : (float * float * float) -> d3 t
>> 
>> let componentwise : type d . (float -> float -> float) -> d t -> d t -> d t = fun f v1 v2 ->
>>   match (v1, v2) with
>>   | (Vector2 (x1, y1), Vector2 (x2, y2)) -> Vector2 (f x1 x2, f y1  y1)
>>   | (Vector3 (x1, y1, z1), Vector3 (x2, y2, z2)) -> Vector3 (f x1 x2, f y1 y1, f z1 z2)
>> -------->8----------
> 
> If you put all your code in the same module, as you have just done here,
> you don't get such a warning.
> What you have probably done is defining the types in a module,
> and then defined componentwise in another module.
> What happens then is that the type system cannot guarantee anymore
> that d2 and d3 are distinct: they are just abstract types that could
> be aliases to each other.
> 

Thanks -- thats it!


regards

-Markus

-- 
Markus Weißmann, M.Sc.
Technische Universität München
Institut für Informatik
Boltzmannstr. 3
D-85748 Garching
Germany
http://wwwknoll.in.tum.de/