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 c5ff346549e7 (Postfix) with ESMTPS id ED5925D4 for ; Sat, 18 Apr 2020 09:48:37 +0000 (UTC) X-IronPort-AV: E=Sophos;i="5.72,398,1580770800"; d="scan'208";a="445714617" Received: from sympa.inria.fr ([193.51.193.213]) by mail2-relais-roc.national.inria.fr with ESMTP; 18 Apr 2020 11:48:37 +0200 Received: by sympa.inria.fr (Postfix, from userid 20132) id 52D0F7F48D; Sat, 18 Apr 2020 11:48:34 +0200 (CEST) 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 90BFA7EEDF for ; Sat, 18 Apr 2020 11:48:29 +0200 (CEST) Authentication-Results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=asai@is.ocha.ac.jp; spf=Pass smtp.mailfrom=asai@is.ocha.ac.jp; spf=None smtp.helo=postmaster@web.is.ocha.ac.jp IronPort-PHdr: =?us-ascii?q?9a23=3AV7PZ2xxeq4GQxH/XCy+O+j09IxM/srCxBDY+r6Qd?= =?us-ascii?q?2+gUIJqq85mqBkHD//Il1AaPAdyGrakVwLCO++C4ACpcuMrH6ChDOLV3FDY7yu?= =?us-ascii?q?wu1zQ6B8CEDUCpZNXLVAcdWPp4aVl+4nugOlJUEsutL3fbo3m18CJAUk6nbVk9?= =?us-ascii?q?Kev6AJPdgNqq3O6u5ZLTfx9IhD2gar9uMRm6twrcutQWjId4JKs8zhTFrmVUd+?= =?us-ascii?q?9LwW9kOU+fkwzz68ut85Nv6Thct+4k+8VdTaj0YqM0QKBXAzghL207/tDguwPZ?= =?us-ascii?q?TQuI6HscU2EWnQRNDgPY8hz0XYr/vzXjuOZl1yaUIcP5TbYvWTS/9KhrUwPniD?= =?us-ascii?q?0GNzEi7m7ajNF7gb9BrxKgoxx/xJPUYJ2QOfFjcK7RYc8WSGxcVctKSSdPHp2z?= =?us-ascii?q?YJcOD+oZPOZXsY/9p0cVrRCjAQWgHf7jxiNUinPz26AxzuYvHhzc3AE4EdwAsG?= =?us-ascii?q?raosj2OqccXu+60LTHwjfYYvNKxTvw8pTEfgw9rf2SW797bMrfyVMoFwPAllie?= =?us-ascii?q?rJLqPzWU1usRs2ib7vdrWP60i2E9qgF6vz+iyd03iobTh4IY0VHE9T5jzIYyOd?= =?us-ascii?q?K4SFR0bcS+H5RMrS2aNZN2T9okTmp1uyg60qULtYO1cSUE0pgqxh7SZ+aGfoWH?= =?us-ascii?q?+B7vSfqdLS9liH57dr+znQi+/Ea8xuHmWcS4zkxGojdEn9TCsH0Gygbd5dKdSv?= =?us-ascii?q?Rn+0eswTaP2B7X6uFDOU01m7TUJIU7zr4xjZofq0PDETP2mErslqOZbFkr9vKq?= =?us-ascii?q?6+T/ernmp5mcOJFoigzmL6gjlMKyDf45PwUORWSW+Oux2Kf+8UHlWLlKi+c5kq?= =?us-ascii?q?jdsJDUP8Qboau5DhdP3YY48Rm/Diyr0NUDnXUdK1JKZBKHgJLzN17UPP/0F/W/?= =?us-ascii?q?g0y0nDdx2//GJqHhAonKLnXbjLjuZ7N960pFxAo3zNBf/I5UB6oaIPPzX0/xrM?= =?us-ascii?q?bXAgU4Mwyy2ebnCc9y2pkQWWKVUeelN/b9uFWS5+8ra9KHZIIPtSy1f/cs7eTv?= =?us-ascii?q?gHt/glQdcLOkx7MYbXm5GrJtJEDPMlT2hdJUMmoMvwE+TaTDk1SDGWpafH+zd6?= =?us-ascii?q?MnoDYwCIvgBIyFRJj70+/J5zuyApADPjMOMVuLC3q9MtzcA65QOhLXGddol3k/?= =?us-ascii?q?bZbkU5UojEz8tRS8zLFnJ6zd8WsarcC7jYkn16jojRg3sAdMIYGY2mCJQXtzmz?= =?us-ascii?q?pVFT4tmqd0oUU7w1zF07Aq2qUFR+wW3OtAV0IBDbCZz+F+DImjCB3MdJGIUxCh?= =?us-ascii?q?SdWvRzg6CNApkYcD?= X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: =?us-ascii?q?A0BWAgATzJpefQpAQYVmHgELHIFwC4NrM?= =?us-ascii?q?Y1JiAuZU4F7AggBAwEKAQEtAgQBAYREAoIPHAcBBDIHDgIQAQEFAQEBAgECAwQ?= =?us-ascii?q?BEwEBCxQIG4V3gjspAYMNAQEBAgESFRM5BgULC0Y0AQUBHAY1hWEfAaJQgQQ9j?= =?us-ascii?q?CcziHghgVYSgSaMU4IAhCE+iBKCLQSLCgeODZdXe4JOgmeUcAwdj1KMbahYg3M?= =?us-ascii?q?CCgcGDyOBNgGCCDMaCDA7gmpPGA2RZBeONDOBNSYTjXUBAQ?= X-IPAS-Result: =?us-ascii?q?A0BWAgATzJpefQpAQYVmHgELHIFwC4NrMY1JiAuZU4F7Agg?= =?us-ascii?q?BAwEKAQEtAgQBAYREAoIPHAcBBDIHDgIQAQEFAQEBAgECAwQBEwEBCxQIG4V3g?= =?us-ascii?q?jspAYMNAQEBAgESFRM5BgULC0Y0AQUBHAY1hWEfAaJQgQQ9jCcziHghgVYSgSa?= =?us-ascii?q?MU4IAhCE+iBKCLQSLCgeODZdXe4JOgmeUcAwdj1KMbahYg3MCCgcGDyOBNgGCC?= =?us-ascii?q?DMaCDA7gmpPGA2RZBeONDOBNSYTjXUBAQ?= X-IronPort-AV: E=Sophos;i="5.72,398,1580770800"; d="scan'208";a="445714607" X-MGA-submission: =?us-ascii?q?MDGaaiFMv4bIj0OX+U2XSeXx1l798vRfJs7VtO?= =?us-ascii?q?WjTXMHsnA3y2uRE5jvACKOVIL++w/IHFa396TIvgW64Qt/8/pKe3wJgN?= =?us-ascii?q?mUKdcgmNkfOA3Deob/I2fJpHWzQPaiNi759gjAssodkRNG+o5JxzU0sN?= =?us-ascii?q?IU1Lg72dr6+AkAPx3Zm+zZ8w=3D=3D?= Received: from web.is.ocha.ac.jp ([133.65.64.10]) by mail2-smtp-roc.national.inria.fr with ESMTP; 18 Apr 2020 11:48:26 +0200 Received: from mail-pl1-f199.google.com (mail-pl1-f199.google.com [209.85.214.199]) by web.is.ocha.ac.jp (Postfix) with ESMTP id 7D3B120044C38 for ; Sat, 18 Apr 2020 18:47:51 +0900 (JST) Received: by mail-pl1-f199.google.com with SMTP id l1so3912799pld.14 for ; Sat, 18 Apr 2020 02:47:51 -0700 (PDT) X-Google-DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=1e100.net; s=20161025; h=x-gm-message-state:date:from:to:cc:subject:message-id:references :mime-version:content-disposition:in-reply-to; bh=kC83YaCiOFxFzVedRISArVVonVUI3Ok7yvYT2rhL2D4=; b=oyCDMzT1kBpdD3hbksMxkuBg7CgoD2c8O3GrZW0Yu98WP/yhHI8FzW78Gqk7Hn+G3P G0wUF6C4/iMZ4zk9Dgby06dylSbXlnviri2WXNcOKH9PShvZ+wwPGEdivA8I1z1tAPE9 UlQx7b8ixYFdMklKCpjTPQwnCIPU45CttscdHdgqAjOuLjnv9SZXcoM9Uoz4cwtRjgIx +s0VknguCWnsYODBbXwZhtUfE71VbybEGNtQo5tUCJr1uTQIgpgw/2bYIVjDFfla/ISO HciLmoXFX/dL7XE3ykbliNwrPHGbLAaZX8wazqFlxIcF1THF6AiDhOPx61Nzuu7v0rSy TImg== X-Gm-Message-State: AGi0PuaNVGlI6IEPLO0TOgMcERH3i5zIagwiciIMndHq2g6c+aye6hb8 VBJL2tbRjg0IlBGIQQKTgYkssFBxiJc2fF6Wvt8BevjSevuTMk5n3oYp9rOMZuBglgxSh46VVyr xNqfVF1OaDs+e X-Received: by 2002:a17:902:44d:: with SMTP id 71mr7971220ple.123.1587203270769; Sat, 18 Apr 2020 02:47:50 -0700 (PDT) X-Google-Smtp-Source: APiQypLv7EXedUTIvip7IgRpo4BtpkhxFvo7EnDdxFYWdevw6pX9blYKTXDuQm8RcTBNfz7eTzlqKA== X-Received: by 2002:a17:902:44d:: with SMTP id 71mr7971205ple.123.1587203270497; Sat, 18 Apr 2020 02:47:50 -0700 (PDT) Received: from localhost (123.230.42.163.er.eaccess.ne.jp. [123.230.42.163]) by smtp.gmail.com with ESMTPSA id 3sm10923010pgh.75.2020.04.18.02.47.49 (version=TLS1_3 cipher=TLS_AES_256_GCM_SHA384 bits=256/256); Sat, 18 Apr 2020 02:47:49 -0700 (PDT) Date: Sat, 18 Apr 2020 18:47:36 +0900 From: Kenichi Asai To: Gabriel Scherer Cc: caml users Message-ID: <20200418094736.GA80393@pllab.is.ocha.ac.jp> References: <20200418022319.GA75735@pllab.is.ocha.ac.jp> MIME-Version: 1.0 Content-Type: text/plain; charset=us-ascii Content-Disposition: inline In-Reply-To: Subject: Re: [Caml-list] Locally abstract parameterized types? Reply-To: Kenichi Asai X-Loop: caml-list@inria.fr X-Sequence: 18104 Errors-to: caml-list-owner@inria.fr Precedence: list Precedence: bulk Sender: caml-list-request@inria.fr X-no-archive: yes List-Id: List-Archive: List-Help: List-Owner: List-Post: List-Subscribe: List-Unsubscribe: Thank you, Gabriel. > No, this is currently not supported. For this use-case you will have to use > modules, typically a functor (in some circumstances a first-class module > parameter may work as well, if the return type does not depend on the > parameter). Let me ask a possibly related question. I want to define types similar to the following: type 'v pair_t = {pair : 'a. 'a * ('a -> 'v t)} and 'v t = A of 'v pair_t | V of 'v but where the type 'a of the pair field should be existential, rather than universal. Since the above definition is universal, I get an error for the following definition: let test : bool t = A {pair = (3, fun x -> V true)} Error: This field value has type int * (int -> bool t) which is less general than 'a. 'a * ('a -> 'v t) To implement an existential type, we need to use modules. Let me try. If 'v pair_t does not depend on 'v t, for example, if the second element of the pair has type 'a -> 'v (rather than 'a -> 'v t), I could write as follows: module type Pair1_t = sig type a type v val pair : a * (a -> v) (* not a -> v t *) end type 'v t1 = A of (module Pair1_t with type v = 'v) | V of 'v Now I can define (3, fun x -> true) as follows: let test1 : bool t1 = let module Pair1 = struct type a = int type v = bool let pair = (3, fun x -> true) end in A (module Pair1) On the other hand, if pair_t did not have a type parameter, for example, if the parameter is fixed to bool, I could write as follows: module type Pair2_t = sig type a type t val pair : a * (a -> t) (* not a -> v t *) end type t2 = A of (module Pair2_t with type t = t2) | V of bool Now I can define (3, fun x -> V true) as follows: let test2 : t2 = let module Pair2 = struct type a = int type t = t2 let pair = (3, fun x -> V true) end in A (module Pair2) My question is if we can combine these two to achieve my original goal. I first write: module type Pair3_t = sig type a type v type 'a t val pair : a * (a -> v t) end and tried to define: type 'v t3 = A of (module Pair3_t with type v = 'v and type 'a t = 'a t3) | V of 'v but I got the following error: Error: invalid package type: parametrized types are not supported If mutual recursion between Pair3_t and t3 is allowed, that would also be OK. But if I try to connect the two definitons with "and", I get a syntax error. You mention a functor, which is suggestive. I tried to use a functor, but so far without success. Can I define my types using a functor? Thank you in advance. Sincerely, -- Kenichi Asai