From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: X-Spam-Checker-Version: SpamAssassin 3.1.3 (2006-06-01) on yquem.inria.fr X-Spam-Level: X-Spam-Status: No, score=0.0 required=5.0 tests=none autolearn=disabled version=3.1.3 X-Original-To: caml-list@yquem.inria.fr Delivered-To: caml-list@yquem.inria.fr Received: from mail2-relais-roc.national.inria.fr (mail2-relais-roc.national.inria.fr [192.134.164.83]) by yquem.inria.fr (Postfix) with ESMTP id B53A5BC6B for ; Thu, 20 Sep 2007 18:58:00 +0200 (CEST) X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: AgAAAC1E8kZCbwQamGdsb2JhbACOFQEBAQEHBAQRGA X-IronPort-AV: E=Sophos;i="4.20,279,1186351200"; d="scan'208";a="1476403" Received: from out2.smtp.messagingengine.com ([66.111.4.26]) by mail2-smtp-roc.national.inria.fr with ESMTP; 20 Sep 2007 18:59:24 +0200 Received: from compute1.internal (compute1.internal [10.202.2.41]) by out1.messagingengine.com (Postfix) with ESMTP id 412CF2F087; Thu, 20 Sep 2007 12:59:23 -0400 (EDT) Received: from heartbeat1.messagingengine.com ([10.202.2.160]) by compute1.internal (MEProxy); Thu, 20 Sep 2007 12:59:23 -0400 X-Sasl-enc: sHGSWeecfA3FKaacSzC5OUi/S3iadqScCHN2qPmae/Rs 1190307562 Received: from [192.168.1.10] (AMontsouris-753-1-11-75.w90-2.abo.wanadoo.fr [90.2.135.75]) by mail.messagingengine.com (Postfix) with ESMTP id 4BB633E26; Thu, 20 Sep 2007 12:59:22 -0400 (EDT) Date: Thu, 20 Sep 2007 18:59:14 +0200 (CEST) From: Martin Jambon X-X-Sender: martin@martin.ec.wink.com To: Christophe Raffalli Cc: caml-list@yquem.inria.fr Subject: Re: [Caml-list] polymorphic variant In-Reply-To: <46F28C38.2080801@univ-savoie.fr> Message-ID: References: <46F28C38.2080801@univ-savoie.fr> MIME-Version: 1.0 Content-Type: TEXT/PLAIN; charset=US-ASCII; format=flowed X-Spam: no; 0.00; ens-lyon:01 christophe:01 raffalli:01 val:01 val:01 ocaml:01 catch-all:01 lowercase:01 2007,:98 polymorphic:01 wrote:01 incompatible:01 caml-list:01 functions:01 jambon:01 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 ] = > > # let g = function > `T, y -> y > | x, `T -> `F > | `F, `F -> `F > | `F, _ -> `F > ;; > val g : [< `F | `T ] * ([> `F | `T ] as 'a) -> 'a = > > ------- > > 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