From mboxrd@z Thu Jan 1 00:00:00 1970 X-Sympa-To: caml-list@inria.fr Received: from mail3-relais-sop.national.inria.fr (mail3-relais-sop.national.inria.fr [192.134.164.104]) by walapai.inria.fr (8.13.6/8.13.6) with ESMTP id p4BFlhZf019361 for ; Wed, 11 May 2011 17:47:43 +0200 X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: AlwCALCuyk3BMH5JmWdsb2JhbAAvl2uNchQBAQEBAQgLCwcUJYhwv3OGEASUF4o8 X-IronPort-AV: E=Sophos;i="4.64,353,1301868000"; d="asc'?scan'208";a="82961672" Received: from dsi-mta-out.univ-savoie.fr ([193.48.126.73]) by mail3-smtp-sop.national.inria.fr with ESMTP; 11 May 2011 17:47:37 +0200 Received: from localhost (localhost [127.0.0.1]) by dsi-mta-out.univ-savoie.fr (Postfix) with ESMTP id A326726381 for ; Wed, 11 May 2011 17:47:37 +0200 (CEST) X-Virus-Scanned: Debian amavisd-new at dsi-mta-out Received: from dsi-mta-out.univ-savoie.fr ([127.0.0.1]) by localhost (dsi-mta-out.univ-savoie.fr [127.0.0.1]) (amavisd-new, port 10024) with ESMTP id SWMXmycgBFPC for ; Wed, 11 May 2011 17:47:37 +0200 (CEST) Received: from dsi-mail-msa1.univ-savoie.fr (dsi-mail-msa1.univ-savoie.fr [193.48.126.83]) by dsi-mta-out.univ-savoie.fr (Postfix) with ESMTP id 8BBED26237 for ; Wed, 11 May 2011 17:47:37 +0200 (CEST) Received: from localhost (localhost [127.0.0.1]) by dsi-mail-msa1.univ-savoie.fr (Postfix) with ESMTP id 863E11C068; Wed, 11 May 2011 17:47:37 +0200 (CEST) X-Virus-Scanned: Debian amavisd-new at dsi-mail-msa1 Received: from dsi-mail-msa1.univ-savoie.fr ([127.0.0.1]) by localhost (dsi-mail-msa1.univ-savoie.fr [127.0.0.1]) (amavisd-new, port 10024) with ESMTP id 9TU4cgRSLZJE; Wed, 11 May 2011 17:47:37 +0200 (CEST) Received: from [193.48.123.45] (d45.lama.univ-savoie.fr [193.48.123.45]) by dsi-mail-msa1.univ-savoie.fr (Postfix) with ESMTPS id 6E6EA1C063; Wed, 11 May 2011 17:47:37 +0200 (CEST) Message-ID: <4DCAAF94.8010206@univ-savoie.fr> Date: Wed, 11 May 2011 17:47:32 +0200 From: Christophe Raffalli User-Agent: Mozilla/5.0 (X11; U; Linux x86_64; en-US; rv:1.9.2.17) Gecko/20110424 Lightning/1.0b2 Thunderbird/3.1.10 MIME-Version: 1.0 To: caml-list@inria.fr References: <719085.83949.qm@web111512.mail.gq1.yahoo.com> <35C81D78-50FE-47D2-93E2-F48FF4AEED3F@math.nagoya-u.ac.jp> In-Reply-To: <35C81D78-50FE-47D2-93E2-F48FF4AEED3F@math.nagoya-u.ac.jp> X-Enigmail-Version: 1.1.2 Content-Type: multipart/signed; micalg=pgp-sha1; protocol="application/pgp-signature"; boundary="------------enigAC8AA83939C29D33234B6D85" X-Validation-by: craff73@gmail.com Subject: Re: [Caml-list] Difference between [ `A ] and [< `A ] This is an OpenPGP/MIME signed message (RFC 2440 and 3156) --------------enigAC8AA83939C29D33234B6D85 Content-Type: text/plain; charset=ISO-8859-1 Content-Transfer-Encoding: quoted-printable > For instance, [< `A of int] and [< `A of bool] are unifiable, giving [< = `A of int & bool], OK ... this means you can write (I tested in 3.11.2) : # type ('a,'b,'c) inter =3D [< `A of 'b & 'c] as 'a;; type ('a, 'b, 'c) inter =3D 'a constraint 'a =3D [< `A of 'b & 'c ] which seems to be a type isomorphic to the intersection type of 'b and 'c .= .. does this mean we can play with intersection type in OCaml (using some type= cast because intersection type is undecidable ...) In other word : can we encode system D in OCaml ? Cheers, Christophe --=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 can check this signature. The public key is stored on www.keyserver.net --------------------------------------------- --------------enigAC8AA83939C29D33234B6D85 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.10 (GNU/Linux) Comment: Using GnuPG with Mozilla - http://enigmail.mozdev.org/ iEYEARECAAYFAk3Kr5QACgkQi9jr/RgYAS7EVgCgzXGiwnbPEULDqxfjX5KhOCtY eB4An0uqlnJiNEhFMF/8EFp9Fbz36lEy =hLco -----END PGP SIGNATURE----- --------------enigAC8AA83939C29D33234B6D85--