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.1 required=5.0 tests=AWL autolearn=disabled version=3.1.3 X-Original-To: caml-list@yquem.inria.fr Delivered-To: caml-list@yquem.inria.fr Received: from mail1-relais-roc.national.inria.fr (mail1-relais-roc.national.inria.fr [192.134.164.82]) by yquem.inria.fr (Postfix) with ESMTP id E8D90BC6B for ; Fri, 21 Sep 2007 08:06:24 +0200 (CEST) X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: AgAAANr88kbUGyocimdsb2JhbACOGgEBAQgEBg8RBw X-IronPort-AV: E=Sophos;i="4.20,280,1186351200"; d="asc'?vcf'?scan'208";a="1140011" Received: from smtp2-g19.free.fr ([212.27.42.28]) by mail1-smtp-roc.national.inria.fr with ESMTP; 21 Sep 2007 08:07:53 +0200 Received: from smtp2-g19.free.fr (localhost.localdomain [127.0.0.1]) by smtp2-g19.free.fr (Postfix) with ESMTP id 4482098FB4; Fri, 21 Sep 2007 08:07:53 +0200 (CEST) Received: from Tocksi.local (unknown [82.254.20.237]) by smtp2-g19.free.fr (Postfix) with ESMTP id DBAB67535; Fri, 21 Sep 2007 08:07:52 +0200 (CEST) Message-ID: <46F35FB3.6060304@univ-savoie.fr> Date: Fri, 21 Sep 2007 08:07:47 +0200 From: Christophe Raffalli User-Agent: Thunderbird 2.0.0.6 (Macintosh/20070728) MIME-Version: 1.0 To: Jacques Garrigue Cc: caml-list@yquem.inria.fr Subject: Re: [Caml-list] polymorphic variant References: <46F28C38.2080801@univ-savoie.fr> <20070921.091337.134531783.garrigue@math.nagoya-u.ac.jp> In-Reply-To: <20070921.091337.134531783.garrigue@math.nagoya-u.ac.jp> X-Enigmail-Version: 0.95.3 Content-Type: multipart/signed; micalg=pgp-sha1; protocol="application/pgp-signature"; boundary="------------enig35C18C2937FB10D6CB202351" X-Spam: no; 0.00; christophe:01 raffalli:01 christophe:01 raffalli:01 univ-savoie:01 univ-savoie:01 val:01 val:01 ocaml:01 cheers:01 chablais:01 73376:01 polymorphic:01 lama:01 caml-list:01 X-Attachments: cset="utf-8" name="Christophe.Raffalli.vcf" name="Christophe.Raffalli.vcf" type="application/pgp-signature" name="signature.asc" name="signature.asc" This is an OpenPGP/MIME signed message (RFC 2440 and 3156) --------------enig35C18C2937FB10D6CB202351 Content-Type: multipart/mixed; boundary="------------070909050707020804060808" This is a multi-part message in MIME format. --------------070909050707020804060808 Content-Type: text/plain; charset=ISO-8859-1 Content-Transfer-Encoding: quoted-printable Jacques Garrigue a =E9crit : > From: Christophe Raffalli > =20 >> Can someone explain to me why the two following functions are typed so= >> differently: >> >> --------------- >> Objective Caml version 3.10.0 >> >> # let f =3D 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 ] =3D >> >> # let g =3D function >> `T, y -> y >> | x, `T -> `F >> | `F, `F -> `F >> | `F, _ -> `F >> ;; >> val g : [< `F | `T ] * ([> `F | `T ] as 'a) -> 'a =3D >> >> ------- >> >> 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 ? >> =20 > > 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 > =20 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, --=20 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=20 can check this signature. The public key is stored on www.keyserver.net --------------------------------------------- --------------070909050707020804060808 Content-Type: text/x-vcard; charset=utf-8; name="Christophe.Raffalli.vcf" Content-Transfer-Encoding: quoted-printable Content-Disposition: attachment; filename="Christophe.Raffalli.vcf" begin:vcard fn:Christophe Raffalli n:Raffalli;Christophe org:LAMA (UMR 5127) email;internet:christophe.raffalli@univ-savoie.fr title;quoted-printable:Ma=3DC3=3DAEtre de conf=3DC3=3DA9rences 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 --------------070909050707020804060808-- --------------enig35C18C2937FB10D6CB202351 Content-Type: application/pgp-signature; name="signature.asc" Content-Description: OpenPGP digital signature Content-Disposition: attachment; filename="signature.asc" -----BEGIN PGP SIGNATURE----- Version: GnuPG v1.4.7 (Darwin) Comment: Using GnuPG with Mozilla - http://enigmail.mozdev.org iD8DBQFG81+3i9jr/RgYAS4RAi9hAKCdiP2tso4945ZyahPHskD3m8KJXwCg3dQn wggZl1Pkgn5HHSgOxkvhEqw= =yfSh -----END PGP SIGNATURE----- --------------enig35C18C2937FB10D6CB202351--