From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: Received: from mail2-relais-roc.national.inria.fr (mail2-relais-roc.national.inria.fr [192.134.164.83]) by sympa.inria.fr (Postfix) with ESMTPS id 6B81E7F6CB for ; Thu, 29 Jan 2015 03:02:00 +0100 (CET) Received-SPF: None (mail2-smtp-roc.national.inria.fr: no sender authenticity information available from domain of garrigue@math.nagoya-u.ac.jp) identity=pra; client-ip=133.6.130.5; receiver=mail2-smtp-roc.national.inria.fr; envelope-from="garrigue@math.nagoya-u.ac.jp"; x-sender="garrigue@math.nagoya-u.ac.jp"; x-conformance=sidf_compatible Received-SPF: None (mail2-smtp-roc.national.inria.fr: no sender authenticity information available from domain of garrigue@math.nagoya-u.ac.jp) identity=mailfrom; client-ip=133.6.130.5; receiver=mail2-smtp-roc.national.inria.fr; envelope-from="garrigue@math.nagoya-u.ac.jp"; x-sender="garrigue@math.nagoya-u.ac.jp"; x-conformance=sidf_compatible Received-SPF: None (mail2-smtp-roc.national.inria.fr: no sender authenticity information available from domain of postmaster@mailhost.math.nagoya-u.ac.jp) identity=helo; client-ip=133.6.130.5; receiver=mail2-smtp-roc.national.inria.fr; envelope-from="garrigue@math.nagoya-u.ac.jp"; x-sender="postmaster@mailhost.math.nagoya-u.ac.jp"; x-conformance=sidf_compatible X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: A0BRAQBPlMlUmQWCBoVag1hZgwHBUYV5AoFbAQEBAQERAQEBAQEICwsHFC6EDAEBAQMBIx0DATUBAQMLCxgCAhgOAgJXBog3B78gcIRoAowzhGoBAQEBAQEEAQEBAQEBAQETAQaBIY4kMweCaC6BE4oRikCDSpJGhB9ggkIBAQE X-IPAS-Result: A0BRAQBPlMlUmQWCBoVag1hZgwHBUYV5AoFbAQEBAQERAQEBAQEICwsHFC6EDAEBAQMBIx0DATUBAQMLCxgCAhgOAgJXBog3B78gcIRoAowzhGoBAQEBAQEEAQEBAQEBAQETAQaBIY4kMweCaC6BE4oRikCDSpJGhB9ggkIBAQE X-IronPort-AV: E=Sophos;i="5.09,484,1418079600"; d="scan'208";a="119098257" Received: from rabbit.math.nagoya-u.ac.jp (HELO mailhost.math.nagoya-u.ac.jp) ([133.6.130.5]) by mail2-smtp-roc.national.inria.fr with ESMTP; 29 Jan 2015 03:01:54 +0100 Received: from mailhost.math.nagoya-u.ac.jp (localhost [127.0.0.1]) by mailhost.math.nagoya-u.ac.jp (Postfix) with ESMTP id AAF3B6492; Thu, 29 Jan 2015 11:01:51 +0900 (JST) Received: from mailhost.math.nagoya-u.ac.jp (localhost [127.0.0.1]) by mailhost.math.nagoya-u.ac.jp (Postfix) with ESMTP id 4B44B4154; Thu, 29 Jan 2015 11:01:51 +0900 (JST) DKIM-Signature: v=1; a=rsa-sha1; c=relaxed; d=math.nagoya-u.ac.jp; h= subject:mime-version:content-type:from:in-reply-to:date:cc :content-transfer-encoding:message-id:references:to; s=alpha; bh=KlYsCOw5USvnhzM48/deMx5QJss=; b=VZyXk64Ert7os4bw0+08qYQeFU4E mvD+AYle1YasAiYK+WQ8XrFJ+4eRa9a+rn0r3jY0lmA5UCqtvEAaS+6xNtTfHwa4 Srncokpyo9BSFwQPrZNltYp2SWcnYOK3AAOlSoMfZR+1Zdu35Ue8+/Pf/kO8hA+x XqjAgVw4VZpsK3Q= DomainKey-Signature: a=rsa-sha1; h=Received:Subject:Mime-Version:Content-Type:From:In-Reply-To:Date:Cc:Content-Transfer-Encoding:Message-Id:References:To:X-Mailer; b=RXILaftI5WPUzsnJ7iIew4MdSyAwbPk7igFZ1v7haMYWJdwDJrmqQIWygKJz80qhvZgdPoBhsnXaR8KKPM5lcYIp77o3SDGGWkJYiGfT77v+0pe9G1xoHHZBTaGamI50Dr3SDBsnhKfTpU3PR+816pRp25ScBhxVRT97Lxad4SM=; c=nofws; d=math.nagoya-u.ac.jp; q=dns; s=alpha Received: from tanpopo.garrigue.jp (58x158x128x157.ap58.ftth.ucom.ne.jp [58.158.128.157]) by mailhost.math.nagoya-u.ac.jp (Postfix) with ESMTPSA id 1E21F414D; Thu, 29 Jan 2015 11:01:51 +0900 (JST) Mime-Version: 1.0 (Mac OS X Mail 8.1 \(1993\)) Content-Type: text/plain; charset=utf-8 From: Jacques Garrigue In-Reply-To: Date: Thu, 29 Jan 2015 11:02:03 +0900 Cc: OCaml Mailing List Content-Transfer-Encoding: quoted-printable Message-Id: References: To: =?utf-8?Q?Milan_Stanojevi=C4=87?= X-Mailer: Apple Mail (2.1993) Subject: Re: [Caml-list] first class module types with "with type" On 2015/01/29 08:39, Milan Stanojevi=C4=87 wrote: >=20 > My search foo is failing me, I'm pretty sure this was discussed before > but I can't find it. >=20 > Why is the following disallowed: > module type A =3D sig type 'a t end > type foo =3D { a : (module A with type 'a t =3D 'a list)} >=20 > File "z.ml", line 2, characters 29-30: > Error: Syntax error This is because ocaml does not have higher-order polymorphism in its core language. Namely, the type (module S with type t =3D texpr) can be seen as the type (texpr s) where type 'a s =3D (module S with type t =3D 'a) However, if t itself has a type parameter, we cannot turn it into a type variable (which would have to be higher-order). Technically, it would be possible to allow such equations, if we do not go through the above intermediate type s. That is, we would have to require that the type definition contains no free variables, in contrast with non-parameterized ones for which allowing free variables is essential. > But this is ok > module type A =3D sig type 'a t end > module type S =3D A with type 'a t =3D 'a list > type a =3D (module S) OCaml has higher-order polymorphism in the module language. This is what you are using in this case. Not that from the point of view of theoretical expressivity, there is no big difference between the two: since 4.02, equality on package types is structural, so that it will work even if you define S twice in different places. Jacques Garrigue=