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 E3FC55D4 for ; Sat, 18 Apr 2020 10:05:22 +0000 (UTC) X-IronPort-AV: E=Sophos;i="5.72,398,1580770800"; d="scan'208";a="445715964" Received: from sympa.inria.fr ([193.51.193.213]) by mail2-relais-roc.national.inria.fr with ESMTP; 18 Apr 2020 12:05:21 +0200 Received: by sympa.inria.fr (Postfix, from userid 20132) id 542907F4C1; Sat, 18 Apr 2020 12:05:15 +0200 (CEST) Received: from mail3-relais-sop.national.inria.fr (mail3-relais-sop.national.inria.fr [192.134.164.104]) by sympa.inria.fr (Postfix) with ESMTPS id B2FC67EEDF for ; Sat, 18 Apr 2020 12:05:04 +0200 (CEST) Authentication-Results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=yallop@gmail.com; spf=Pass smtp.mailfrom=yallop@gmail.com; spf=None smtp.helo=postmaster@mail-il1-f179.google.com IronPort-PHdr: =?us-ascii?q?9a23=3A/z6MIRf3Tr6B0xa3Rv3mzlZmlGMj4u6mDksu8pMi?= =?us-ascii?q?zoh2WeGdxc2zZR7h7PlgxGXEQZ/co6odzbGJ4+a9ASQp2tWojjMrSNR0TRgLiM?= =?us-ascii?q?EbzUQLIfWuLgnFFsPsdDEwB89YVVVorDmROElRH9viNRWJ+iXhpRZbIBj0NBJ0?= =?us-ascii?q?K+LpAcaSyp3vj6Hhs6HUNiZFgju2YbI6BQ6/rE2Fv9IfgKNjMeA2wRvA5HJDPe?= =?us-ascii?q?ZOkzBGP1WWyjTx/Mq17dZS+iBUvOppo99JVaH9Z4w3SLVZCHItNGVjt56jjgXK?= =?us-ascii?q?UQbavihUaW4RiBcdRlGdtEimDKe0iTPzs69G4AffJdf/FOlmVjGr7qMtQxjt2n?= =?us-ascii?q?9eZmwJtVrPg8k1t5p15Reophhx2YnROdjHO/93f6ebdtQfFzMYA5RhEhdZC4b5?= =?us-ascii?q?VLMhSuoMOeEC8dv4rloK6Bq6XEyiXby+jDBPgXDy0Osx1OFzSQw=3D?= X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: =?us-ascii?q?A0CCBABl0Jpef7OmVdFmDhABCxyGFyqEH?= =?us-ascii?q?YN6iwKCEYoDdZBWCgEDAQwvBAEBhEQCgg8cBwEENBMCEAEBBQEBAQIBAgMEARM?= =?us-ascii?q?BAQkLCwgnhV8MgjsFASMBBoMGAQEBAQIBEhEEGQEbHQEDAQsGBQsNAgImAgIiA?= =?us-ascii?q?REBBQEcBhMIGoVPAQMOIKJWgQQ9ijN1fxYFAReDAQWEdgoZJw1lgTQCBxJ8Kow?= =?us-ascii?q?5GoIAgUeCWj6EToMSgl8EsXBHggeCZ4tAiTwdnD+sZA8jgUaBeTMaCBsVOzGCO?= =?us-ascii?q?FAYDZFYg3OKGD1EMI1dgVQBAQ?= X-IPAS-Result: =?us-ascii?q?A0CCBABl0Jpef7OmVdFmDhABCxyGFyqEHYN6iwKCEYoDdZB?= =?us-ascii?q?WCgEDAQwvBAEBhEQCgg8cBwEENBMCEAEBBQEBAQIBAgMEARMBAQkLCwgnhV8Mg?= =?us-ascii?q?jsFASMBBoMGAQEBAQIBEhEEGQEbHQEDAQsGBQsNAgImAgIiAREBBQEcBhMIGoV?= =?us-ascii?q?PAQMOIKJWgQQ9ijN1fxYFAReDAQWEdgoZJw1lgTQCBxJ8Kow5GoIAgUeCWj6ET?= =?us-ascii?q?oMSgl8EsXBHggeCZ4tAiTwdnD+sZA8jgUaBeTMaCBsVOzGCOFAYDZFYg3OKGD1?= =?us-ascii?q?EMI1dgVQBAQ?= X-IronPort-AV: E=Sophos;i="5.72,398,1580770800"; d="scan'208";a="346318385" X-MGA-submission: =?us-ascii?q?MDFFIRBUPiI8FoNPAVO3w/pXQBmay3xbmjxmH9?= =?us-ascii?q?rrCDZeE9CRncpUuGpojgK478TrANgMFcGLVjZkQJPR7/ZD/bB2WYlCJ8?= =?us-ascii?q?BM54+XmeKYWFQUergLdQ91zIm5prKMLYcv5YreAf6nU32caluOhIAQ4Y?= =?us-ascii?q?HkPhdsgt3RXqfzw30NtZgnCQ=3D=3D?= Received: from mail-il1-f179.google.com ([209.85.166.179]) by mail3-smtp-sop.national.inria.fr with ESMTP/TLS/AES256-GCM-SHA384; 18 Apr 2020 12:05:02 +0200 Received: by mail-il1-f179.google.com with SMTP id u5so4768363ilb.5 for ; Sat, 18 Apr 2020 03:05:02 -0700 (PDT) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20161025; h=mime-version:references:in-reply-to:from:date:message-id:subject:to :cc:content-transfer-encoding; bh=+sBPdyrBqPn4rigpU/4t9x+qrk4xWFqivnZ5niq6pUk=; b=O7RCe8DTvrP4x3kySxkEh5GQETiXjTCVJ2YvSeWowfjTtG4j3Ab4OSKxEiKAEdANEP 12aGhvQ0UzHarvses3DqwMCQBBz00NHfctOaqT/jPhWPe2idTe+6jqlXI6XkYriEx9l1 eHeh/lW4PVN1rdC10sx1oUr4MnKSXWSUslt564sGGcgAFDFtH2BahXHhAgd1lagfBWC7 040nsJFbe/JgmmQOA63s9j1zrCulXWmXBAJUZsp1qU6T9/DQLBBF9LAESUTaLDceVrcx dodjr8WO6p7Gx877BPtQ/daLXoFJ83LEPE6ivpn+J2TUXJS52G/wHw4CHd1+31l3gE01 O14Q== X-Google-DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=1e100.net; s=20161025; h=x-gm-message-state:mime-version:references:in-reply-to:from:date :message-id:subject:to:cc:content-transfer-encoding; bh=+sBPdyrBqPn4rigpU/4t9x+qrk4xWFqivnZ5niq6pUk=; b=CbXLOUPFKuxxR4DFQjkRHWk1kpoufaluHcIbvuI9uYWS8UDqgCQ2uUjWB3nvAR/bAX rSoz3HWniQbvsPEGelmQT9wXsVe0i2CJ9U/U5J7eLVQg/+tf2Rtl+O4aDgS7UCLj7fVq g7wlcaa6DIE8Kv9d+mfuzYPBsbmrJwZAy5cUxVWHKlYN0Bvq3zqBc4WCWTUwtIu38JlG P/6cqJabKUuxn9taMZddjvYFfdFeld1BldDSDNlQplPDnfSzjhVuckQK3mRDxGr4L/qX hdqrV5B/CBMzjxfR/plKK0SzKbW/bn2gvdIxMUNdvN1RIHspjMZG2w4tnuyPTUjVqZZT Kb2Q== X-Gm-Message-State: AGi0PuZASySSCEZEwm55Pre/eF/NVtGx/SpYTihA+5kuoCHLHLPBe36v yfwQiDgKFjSUnllgQFrlAGeWNMg4Pj/2r4TWmIIsr0QwwGU= X-Google-Smtp-Source: APiQypJ5fwJ1VkDU4iI21BLENodQEkvYAwLy2PiX0u+nZ3nNhfVQw0RHNtZOVrjr5xfOW0TpR6mp7hxym4lObF0m9mU= X-Received: by 2002:a92:1d4b:: with SMTP id d72mr7082657ild.14.1587204300979; Sat, 18 Apr 2020 03:05:00 -0700 (PDT) MIME-Version: 1.0 References: <20200418022319.GA75735@pllab.is.ocha.ac.jp> <20200418094736.GA80393@pllab.is.ocha.ac.jp> In-Reply-To: <20200418094736.GA80393@pllab.is.ocha.ac.jp> From: Jeremy Yallop Date: Sat, 18 Apr 2020 10:04:49 +0000 Message-ID: To: Kenichi Asai Cc: Gabriel Scherer , caml users Content-Type: text/plain; charset="UTF-8" Content-Transfer-Encoding: quoted-printable Subject: Re: [Caml-list] Locally abstract parameterized types? Reply-To: Jeremy Yallop X-Loop: caml-list@inria.fr X-Sequence: 18106 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: On Sat, 18 Apr 2020 at 09:49, Kenichi Asai wrote: > > 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 modul= e > > 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 =3D {pair : 'a. 'a * ('a -> 'v t)} > and 'v t =3D > A of 'v pair_t > | V of 'v > > but where the type 'a of the pair field should be existential, rather > than universal. Here's one fairly direct way to do that: type 'v pair_t =3D Pair : ('a * ('a -> 'v t)) -> 'v pair_t and 'v t =3D A of 'v pair_t | V of 'v let test : bool t =3D A (Pair (3, fun x -> V true)) But, since '=E2=88=83a.(a =C3=97 (a =E2=86=92 t))' is isomorphic to 'unit = =E2=86=92 t', you can write the example more simply, without universal or existential types: type 'v t =3D A of (unit -> 'v t) | V of 'v let a x f =3D A (fun () -> f x) let test : bool t =3D a 3 (fun x -> V true) (Of course, in your real code this scheme may be not be possible.) > My question is if we can combine these two to achieve my original > goal. I first write: > > module type Pair3_t =3D sig > type a > type v > type 'a t > val pair : a * (a -> v t) > end > > and tried to define: > > type 'v t3 =3D > A of (module Pair3_t with type v =3D 'v and type 'a t =3D 'a t3) > | V of 'v > > but I got the following error: > > Error: invalid package type: parametrized types are not supported Here's a slight variant of this idea that works by avoiding the parameterized type in Pair3_t: module type Pair3_t =3D sig type a type vt val pair : a * (a -> vt) end type 'v t =3D A of (module Pair3_t with type vt =3D 'v t) | V of 'v let test : bool t =3D A (module struct type a =3D int type vt =3D bool t let pair =3D (3, fun x -> V true) end) Kind regards, Jeremy