From mboxrd@z Thu Jan  1 00:00:00 1970
Return-Path: <garrigue@math.nagoya-u.ac.jp>
X-Spam-Checker-Version: SpamAssassin 3.1.3 (2006-06-01) on yquem.inria.fr
X-Spam-Level: 
X-Spam-Status: No, score=0.4 required=5.0 tests=AWL,DNS_FROM_RFC_ABUSE 
	autolearn=disabled version=3.1.3
X-Original-To: caml-list@yquem.inria.fr
Delivered-To: caml-list@yquem.inria.fr
Received: from mail3-relais-sop.national.inria.fr (mail3-relais-sop.national.inria.fr [192.134.164.104])
	by yquem.inria.fr (Postfix) with ESMTP id B8C43BC6B
	for <caml-list@yquem.inria.fr>; Fri, 21 Sep 2007 02:12:37 +0200 (CEST)
X-IronPort-Anti-Spam-Filtered: true
X-IronPort-Anti-Spam-Result: Ao8CAGup8kaCNhAB/2dsb2JhbAA
X-IronPort-AV: E=Sophos;i="4.20,280,1186351200"; 
   d="scan'208";a="2995123"
Received: from kurims.kurims.kyoto-u.ac.jp ([130.54.16.1])
  by mail3-smtp-sop.national.inria.fr with ESMTP; 21 Sep 2007 02:14:03 +0200
Received: from localhost (orion [130.54.16.5])
	by kurims.kurims.kyoto-u.ac.jp (8.13.8/8.13.8) with ESMTP id l8L0Dmvg025811;
	Fri, 21 Sep 2007 09:13:49 +0900 (JST)
Date: Fri, 21 Sep 2007 09:13:37 +0900 (JST)
Message-Id: <20070921.091337.134531783.garrigue@math.nagoya-u.ac.jp>
To: Christophe.Raffalli@univ-savoie.fr
Cc: caml-list@yquem.inria.fr
Subject: Re: [Caml-list] polymorphic variant
From: Jacques Garrigue <garrigue@math.nagoya-u.ac.jp>
In-Reply-To: <46F28C38.2080801@univ-savoie.fr>
References: <46F28C38.2080801@univ-savoie.fr>
X-Mailer: Mew version 4.2 on Emacs 22.1 / Mule 5.0 (SAKAKI)
Mime-Version: 1.0
Content-Type: Text/Plain; charset=us-ascii
Content-Transfer-Encoding: 7bit
X-Spam: no; 0.00; christophe:01 raffalli:01 christophe:01 raffalli:01 univ-savoie:01 val:01 val:01 ocaml:01 polymorphic:01 caml-list:01 functions:01 jambon:01 behaviour:01 variant:02 caml:02 

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