polymorphic variant

polymorphic variant

[Christophe Raffalli]

[-- Attachment #1.1: Type: text/plain, Size: 1312 bytes --]

Can someone explain to me why the two following functions are typed so
differently:

---------------
        Objective Caml version 3.10.0

# let f = function
      `T, y -> y
    | x, `T -> x
    | `F, `F -> `F
    | `F, _ -> `F
;;
Warning U: this match case is unused.
val f : [ `F | `T ] * [ `F | `T ] -> [ `F | `T ] = <fun>

# let g = function
    `T, y -> y
  | x, `T -> `F
  | `F, `F -> `F
  | `F, _ -> `F
;;
val g : [< `F | `T ] * ([> `F | `T ] as 'a) -> 'a = <fun>

-------

The decision to close the second column seems to depend upon the right hand side of the pattern, which seems excluded by Jacques Garrigue's paper about deep pattern matching ... According to this paper, the second function is strangely typed. What is implemented in OCaml ?

Regards,
-- 
Christophe Raffalli
Universite de Savoie
Batiment Le Chablais, bureau 21
73376 Le Bourget-du-Lac Cedex

tel: (33) 4 79 75 81 03
fax: (33) 4 79 75 87 42
mail: Christophe.Raffalli@univ-savoie.fr
www: http://www.lama.univ-savoie.fr/~RAFFALLI
---------------------------------------------
IMPORTANT: this mail is signed using PGP/MIME
At least Enigmail/Mozilla, mutt or evolution 
can check this signature. The public key is
stored on www.keyserver.net
---------------------------------------------


[-- Attachment #1.2: Christophe.Raffalli.vcf --]
[-- Type: text/x-vcard, Size: 310 bytes --]

begin:vcard
fn:Christophe Raffalli
n:Raffalli;Christophe
org:LAMA (UMR 5127)
email;internet:christophe.raffalli@univ-savoie.fr
title;quoted-printable:Ma=C3=AEtre de conf=C3=A9rences
tel;work:+33 4 79 75 81 03
note:http://www.lama.univ-savoie.fr/~raffalli
x-mozilla-html:TRUE
version:2.1
end:vcard


[-- Attachment #2: OpenPGP digital signature --]
[-- Type: application/pgp-signature, Size: 249 bytes --]

Re: [Caml-list] polymorphic variant

[Martin Jambon]

On Thu, 20 Sep 2007, Christophe Raffalli wrote:

> Can someone explain to me why the two following functions are typed so
> differently:
>
> ---------------
>        Objective Caml version 3.10.0
>
> # let f = function
>      `T, y -> y
>    | x, `T -> x
>    | `F, `F -> `F
>    | `F, _ -> `F
> ;;
> Warning U: this match case is unused.
> val f : [ `F | `T ] * [ `F | `T ] -> [ `F | `T ] = <fun>
>
> # let g = function
>    `T, y -> y
>  | x, `T -> `F
>  | `F, `F -> `F
>  | `F, _ -> `F
> ;;
> val g : [< `F | `T ] * ([> `F | `T ] as 'a) -> 'a = <fun>
>
> -------
>
> The decision to close the second column seems to depend upon the right hand side of the pattern, which seems excluded by Jacques Garrigue's paper about deep pattern matching ... According to this paper, the second function is strangely typed. What is implemented in OCaml ?


The difference lies in the pattern: if you use a catch-all such as a 
lowercase identifier, the type of the bound variable will be the same as 
the argument that you are matching.

In the following, x and y will have the same type:
match x with
   y -> y


but here x and y have possibly different types:

match x with
  (`A | `B) as y -> y

(x could be of type [ `A ], which is incompatible with the type of y)


It can be conveniently replaced by the following shortcut:

type ab = [ `A | `B ]

match x with
  #ab as y -> y


Martin

--
http://martin.jambon.free.fr

Re: [Caml-list] polymorphic variant

[Jacques Garrigue]

From: Christophe Raffalli <Christophe.Raffalli@univ-savoie.fr>
> Can someone explain to me why the two following functions are typed so
> differently:
> 
> ---------------
>         Objective Caml version 3.10.0
> 
> # let f = function
>       `T, y -> y
>     | x, `T -> x
>     | `F, `F -> `F
>     | `F, _ -> `F
> ;;
> Warning U: this match case is unused.
> val f : [ `F | `T ] * [ `F | `T ] -> [ `F | `T ] = <fun>
> 
> # let g = function
>     `T, y -> y
>   | x, `T -> `F
>   | `F, `F -> `F
>   | `F, _ -> `F
> ;;
> val g : [< `F | `T ] * ([> `F | `T ] as 'a) -> 'a = <fun>
> 
> -------
> 
> The decision to close the second column seems to depend upon the
> right hand side of the pattern, which seems excluded by Jacques
> Garrigue's paper about deep pattern matching ... According to this
> paper, the second function is strangely typed. What is implemented
> in OCaml ?

It is implemented, and correctly I believe.
The above behaviour was correctly explained by Martin Jambon, but I'll
add some detail:
The type of f is actually an instance of the type of g, where the
first and second columns of the pattern were unified. The reason for
that is that in f the 1st line returns the 2nd column, and the 2nd
line the first column. Since the return type has to be unique, this
unifies x and y, i.e. the 1st and 2nd columns.

I hope this clarifies the situation.

Jacques Garrigue

Re: [Caml-list] polymorphic variant

[Christophe Raffalli]

[-- Attachment #1.1: Type: text/plain, Size: 2228 bytes --]

Jacques Garrigue a écrit :
> From: Christophe Raffalli <Christophe.Raffalli@univ-savoie.fr>
>   
>> Can someone explain to me why the two following functions are typed so
>> differently:
>>
>> ---------------
>>         Objective Caml version 3.10.0
>>
>> # let f = function
>>       `T, y -> y
>>     | x, `T -> x
>>     | `F, `F -> `F
>>     | `F, _ -> `F
>> ;;
>> Warning U: this match case is unused.
>> val f : [ `F | `T ] * [ `F | `T ] -> [ `F | `T ] = <fun>
>>
>> # let g = function
>>     `T, y -> y
>>   | x, `T -> `F
>>   | `F, `F -> `F
>>   | `F, _ -> `F
>> ;;
>> val g : [< `F | `T ] * ([> `F | `T ] as 'a) -> 'a = <fun>
>>
>> -------
>>
>> The decision to close the second column seems to depend upon the
>> right hand side of the pattern, which seems excluded by Jacques
>> Garrigue's paper about deep pattern matching ... According to this
>> paper, the second function is strangely typed. What is implemented
>> in OCaml ?
>>     
>
> It is implemented, and correctly I believe.
> The above behaviour was correctly explained by Martin Jambon, but I'll
> add some detail:
> The type of f is actually an instance of the type of g, where the
> first and second columns of the pattern were unified. The reason for
> that is that in f the 1st line returns the 2nd column, and the 2nd
> line the first column. Since the return type has to be unique, this
> unifies x and y, i.e. the 1st and 2nd columns.
>
> I hope this clarifies the situation.
>
> Jacques Garrigue
>   
OK, I understand. But I would prefer if the decision to close or not the
pattern (and therefore
make the last case useless) did not depend upon the right members ...

Cheers,

-- 
Christophe Raffalli
Universite de Savoie
Batiment Le Chablais, bureau 21
73376 Le Bourget-du-Lac Cedex

tel: (33) 4 79 75 81 03
fax: (33) 4 79 75 87 42
mail: Christophe.Raffalli@univ-savoie.fr
www: http://www.lama.univ-savoie.fr/~RAFFALLI
---------------------------------------------
IMPORTANT: this mail is signed using PGP/MIME
At least Enigmail/Mozilla, mutt or evolution 
can check this signature. The public key is
stored on www.keyserver.net
---------------------------------------------


[-- Attachment #1.2: Christophe.Raffalli.vcf --]
[-- Type: text/x-vcard, Size: 310 bytes --]

begin:vcard
fn:Christophe Raffalli
n:Raffalli;Christophe
org:LAMA (UMR 5127)
email;internet:christophe.raffalli@univ-savoie.fr
title;quoted-printable:Ma=C3=AEtre de conf=C3=A9rences
tel;work:+33 4 79 75 81 03
note:http://www.lama.univ-savoie.fr/~raffalli
x-mozilla-html:TRUE
version:2.1
end:vcard


[-- Attachment #2: OpenPGP digital signature --]
[-- Type: application/pgp-signature, Size: 249 bytes --]

Re: [Caml-list] polymorphic variant

[Jacques Garrigue]

From: Christophe Raffalli <Christophe.Raffalli@univ-savoie.fr>
> > The above behaviour was correctly explained by Martin Jambon, but I'll
> > add some detail:
> > The type of f is actually an instance of the type of g, where the
> > first and second columns of the pattern were unified. The reason for
> > that is that in f the 1st line returns the 2nd column, and the 2nd
> > line the first column. Since the return type has to be unique, this
> > unifies x and y, i.e. the 1st and 2nd columns.
> >
> > I hope this clarifies the situation.
> >
> > Jacques Garrigue
> >   
> OK, I understand. But I would prefer if the decision to close or not the
> pattern (and therefore
> make the last case useless) did not depend upon the right members ...

So actually you didn't understand :-)
The point here is that the typing for the pattern matching is
determined completely independently of the right members. This is only
afterwards that some extra unifications may happen, as is always the
case with type inference. This is not a "decision", but a natural
consequence of the type system.
The warning about the useless case is actually a clever trick: rather
than immediately checking for useless cases after checking the pattern
matching, it waits for the whole expression to be typed, in order to
be more accurate.

In some way what you are saying is a bit like:

# let f (x : [> `A]) (y : [> `B]) = ignore [x;y] ;;
val f : ([> `A | `B ] as 'a) -> 'a -> unit = <fun>

Why are the types for x and y unified, I'd much prefere them to be
independent...

By the way, as Martin Jambon explained, you can protect you variables
against type propagation with the "as" syntax.

# let f (`A as x) (`B as y) = [x;y];;
val f : [< `A ] -> [< `B ] -> [> `A | `B ] list = <fun>


Jacques Garrigue