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=1.3 required=5.0 tests=AWL,HTML_MESSAGE,SPF_NEUTRAL 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 3DD7EBBC4 for ; Thu, 16 Apr 2009 14:44:09 +0200 (CEST) X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: AkgDAO/E5knRVdqyimdsb2JhbACCJy+TED8BAQEKCQwHDwWpfpAVAQSDfYdl X-IronPort-AV: E=Sophos;i="4.38,431,1233529200"; d="scan'208";a="27789223" Received: from mail-bw0-f178.google.com ([209.85.218.178]) by mail1-smtp-roc.national.inria.fr with ESMTP; 16 Apr 2009 14:44:08 +0200 Received: by bwz26 with SMTP id 26so315764bwz.27 for ; Thu, 16 Apr 2009 05:44:08 -0700 (PDT) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=googlemail.com; s=gamma; h=domainkey-signature:mime-version:received:in-reply-to:references :date:message-id:subject:from:to:cc:content-type; bh=PvE2plP+G58Ji7kiJqjdGayAHzhzyaDRaP3PSUZpXgY=; b=ndEFWJLvikG7x3d+xZ3eMn63HnCjhM27XrhTS0Hf5OR3k4huYtYk5hWheheW06+RO4 MwIXCronbqM3pKgTgKamIgZLg+rR0aRgKPFc02Z5ozoCxTAQnpKhDHll7BAjzWw/F1Nr BjWDzyUxbMO81uy6FSoF9q3LKFzY0fDaFjLg4= DomainKey-Signature: a=rsa-sha1; c=nofws; d=googlemail.com; s=gamma; h=mime-version:in-reply-to:references:date:message-id:subject:from:to :cc:content-type; b=Xo1niODu+//wVC7/s3x7TY6zwZjDtDwpiD6tuoH3Ifa7INNGKN3yoEzzYNpD/iv2c+ N33lbTpTPSHlUFV5LTFAINahr7Pdo4kzyq3Yx5AnqEqHflHL25Vs6OEd83hjdoqSvHnK Iqutq+iQMzerN/SZBF8qVs4mjvqDekAba6wio= MIME-Version: 1.0 Received: by 10.223.108.196 with SMTP id g4mr396969fap.36.1239885848462; Thu, 16 Apr 2009 05:44:08 -0700 (PDT) In-Reply-To: <721f7f5a0904160531h5b31fd0djac95fe0d534737fe@mail.gmail.com> References: <721f7f5a0904150548o7351d50fm44aaf29b249b67f6@mail.gmail.com> <20090416.212314.107686494.garrigue@math.nagoya-u.ac.jp> <721f7f5a0904160531h5b31fd0djac95fe0d534737fe@mail.gmail.com> Date: Thu, 16 Apr 2009 14:44:08 +0200 Message-ID: <721f7f5a0904160544n3679c10ao870cc359af72c70e@mail.gmail.com> Subject: Re: [Caml-list] Typing of polymorphic variants From: Philippe Veber To: Jacques Garrigue Cc: caml-list@yquem.inria.fr Content-Type: multipart/alternative; boundary=001636c5aa418f44fa0467ab6b5f X-Spam: no; 0.00; variants:01 recursive:01 datatypes:01 recursion:01 datatype:01 abbreviation:01 abbreviation:01 datatype:01 recursive:01 datatypes:01 recursion:01 2009:98 2009:98 polymorphic:01 avoids:01 --001636c5aa418f44fa0467ab6b5f Content-Type: text/plain; charset=ISO-8859-1 Content-Transfer-Encoding: 7bit Just for the record, one possible workaround is the following : type ('a, 'b) gen_u = 'a * 'b type t = [`A | `B of (int,t) gen_u] type 'a u = 'a * t which avoids recursive definitions between type abbreviations. ph. 2009/4/16 Philippe Veber > > 2009/4/16 Jacques Garrigue > > From: Philippe Veber >> > I don't understand the following behaviour: >> > >> > Objective Caml version 3.11.0 >> > >> > # type t = [`A | `B of int u] and 'a u = 'a * t;; >> > Error: In the definition of t, type int u should be 'a u >> > # type t = A | B of int u and 'a u = 'a * t;; >> > type t = A | B of int u >> > and 'a u = 'a * t >> > >> > Anyone's got a simple explanation for this ? >> >> This is due to the difference between type abbreviations and >> datatypes. In your first example, you are defining two types >> abbreviations, and you are not allowed to instantiate a type you are >> defining in mutual recursion. In the second example, you are defining a >> datatype and a type abbreviation, and it is ok to instantiate the type >> abbreviation inside the datatype definition. >> >> The technical reason for this difference is the restriction to regular >> types in type abbreviations. It only applies when the definitions are >> mutually recursive, and do not go through any datatype definition. > > > Indeed, I noticed in other attempts that some definitions that would be > accepted in the form type t = ... type u = ... were rejected in the form > type t = ... and u = ... Now with your explanation it's clear why. Many > thanks ! > > ph. > > >> >> >> Jacques Garrigue >> > > --001636c5aa418f44fa0467ab6b5f Content-Type: text/html; charset=ISO-8859-1 Content-Transfer-Encoding: quoted-printable Just for the record, one possible workaround is the following :

type= ('a, 'b) gen_u =3D 'a * 'b
type t =3D [`A | `B of (int,= t) gen_u]
type 'a u =3D 'a * t

which avoids recursive def= initions between type abbreviations.

ph.



2009/4/16 Philippe Veber = <phil= ippe.veber@googlemail.com>

2009/4/16 Jacques Garrigue <garr= igue@math.nagoya-u.ac.jp>
From: Philippe Veber <philippe.veber@googlemail.com>
> I don't understand the following behavi= our:
>
> =A0 =A0 =A0 =A0 Objective Caml version 3.11.0
>
> # type t =3D [`A | `B of int u] and 'a u =3D 'a * t;;
> Error: In the definition of t, type int u should be 'a u
> # type t =3D A | B of int u and 'a u =3D 'a * t;;
> type t =3D A | B of int u
> and 'a u =3D 'a * t
>
> Anyone's got a simple explanation for this ?

This is due to the difference between type abbreviations and datatypes. In your first example, you are defining two types
abbreviations, and you are not allowed to instantiate a type you are
defining in mutual recursion. In the second example, you are defining a
datatype and a type abbreviation, and it is ok to instantiate the type
abbreviation inside the datatype definition.

The technical reason for this difference is the restriction to regular
types in type abbreviations. It only applies when the definitions are
mutually recursive, and do not go through any datatype definition.

Indeed, I noticed in other attempts that some defi= nitions that would be accepted in the form type t =3D ... type u =3D ... we= re rejected in the form type t =3D ... and u =3D ... Now with your explanat= ion it's clear why. Many thanks !

ph.
=A0


Jacques Garrigue


--001636c5aa418f44fa0467ab6b5f--