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 ESMTP id A924A5D4 for ; Sat, 18 Apr 2020 10:01:50 +0000 (UTC) X-IronPort-AV: E=Sophos;i="5.72,398,1580770800"; d="scan'208,217";a="445715536" Received: from sympa.inria.fr ([193.51.193.213]) by mail2-relais-roc.national.inria.fr with ESMTP; 18 Apr 2020 12:01:49 +0200 Received: by sympa.inria.fr (Postfix, from userid 20132) id 716D87F486; Sat, 18 Apr 2020 12:01:49 +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 1A2217EEDF for ; Sat, 18 Apr 2020 12:01:44 +0200 (CEST) Authentication-Results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=gabriel.scherer@gmail.com; spf=Pass smtp.mailfrom=gabriel.scherer@gmail.com; spf=None smtp.helo=postmaster@mail-qk1-f169.google.com IronPort-PHdr: =?us-ascii?q?9a23=3Au5FP7x+cbRxfNP9uRHKM819IXTAuvvDOBiVQ1KB9?= =?us-ascii?q?0+gcTK2v8tzYMVDF4r011RmSAtWdtqoMotGVmp6jcFRI2YyGvnEGfc4EfD4+ou?= =?us-ascii?q?JSoTYdBtWYA1bwNv/gYn9yNs1DUFh44yPzahANS47WLmffqXyq7DMUBg63dU8s?= =?us-ascii?q?fry0ScbuiJGU2uaz8J3SKyxTjTv1NbppJRSerB6XscIWiM1rIeAz0k2ajGFPfr?= =?us-ascii?q?F5zGlyJF+X1y335sqq8YQrpytZsegg+soGSq76cr41V5RXCT0nNyY+48i95kqL?= =?us-ascii?q?dheG+nZJCjZeqRFPGQWQqUiiBs6s4Bu/jfJ03WyhBeOzTb0wXm78vaJiSRutkS?= =?us-ascii?q?RecjBgrjCRhct3g6ZW5hmmok4nmtKGUMSuLPN7O5jlU5YCX2MYB5ReUiVABsW3?= =?us-ascii?q?aI5dV7NQb9YdlJH0oh41lTX7AACtAO31zToR3y352KQ716IqFgSUhQE=3D?= X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: =?us-ascii?q?A0B9BgBAz5pef6neVdFmDhABCxyGFyqEH?= =?us-ascii?q?YEcgl6LAoIRigN1jm+BZwoBAwEMLwQBAYREAoIPHAcBBDQTAhABAQUBAQECAQI?= =?us-ascii?q?DBAETAQEJCwsIJ4VfDII7BQEjAQaDBwEBAQIBEhEEGQEbFwYBAwELBgMCCzcCA?= =?us-ascii?q?iIBEQEFARwGEwgahU8BAw4gk0uPEIEEPYsofxYFAReDAQWEeQoZJw1iA4E0Agc?= =?us-ascii?q?SgSaMOQ+BTD+BR4JaPoQUg0yCXwSwdXsHgkd9BJZiHZw/qFiEDA8jgUaBeTMaI?= =?us-ascii?q?1AxgjhQGA2RWAwXg1CKGD9CMI1dgVQBAQ?= X-IPAS-Result: =?us-ascii?q?A0B9BgBAz5pef6neVdFmDhABCxyGFyqEHYEcgl6LAoIRigN?= =?us-ascii?q?1jm+BZwoBAwEMLwQBAYREAoIPHAcBBDQTAhABAQUBAQECAQIDBAETAQEJCwsIJ?= =?us-ascii?q?4VfDII7BQEjAQaDBwEBAQIBEhEEGQEbFwYBAwELBgMCCzcCAiIBEQEFARwGEwg?= =?us-ascii?q?ahU8BAw4gk0uPEIEEPYsofxYFAReDAQWEeQoZJw1iA4E0AgcSgSaMOQ+BTD+BR?= =?us-ascii?q?4JaPoQUg0yCXwSwdXsHgkd9BJZiHZw/qFiEDA8jgUaBeTMaI1AxgjhQGA2RWAw?= =?us-ascii?q?Xg1CKGD9CMI1dgVQBAQ?= X-IronPort-AV: E=Sophos;i="5.72,398,1580770800"; d="scan'208,217";a="346318144" X-MGA-submission: =?us-ascii?q?MDEXcXiZYTvEiuAZ7PgBY84WHRLCFpR7cV5YWw?= =?us-ascii?q?ipOGg3JHNWXkdPb0VeA+0ajkvV+LjT6gGoZx9fJNPRu543UDonyOtizZ?= =?us-ascii?q?aKVemJRCBUsgc9gZmhnY/S01VUhBS7cQQYAmjGJkIl5wHyBLbiFqgkuK?= =?us-ascii?q?TecVHICNXiJYRjIGiZICLdQQ=3D=3D?= Received: from mail-qk1-f169.google.com ([209.85.222.169]) by mail3-smtp-sop.national.inria.fr with ESMTP/TLS/AES256-GCM-SHA384; 18 Apr 2020 12:01:42 +0200 Received: by mail-qk1-f169.google.com with SMTP id 20so5177285qkl.10 for ; Sat, 18 Apr 2020 03:01:42 -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; bh=yviKRh7GnhDoQ7JmmUcxZHCfmO+FtKgwaIVywg3KTW8=; b=lz4nzoho0tr8S+Vz4nbWnfgD5hRx6IpNy47iJx5uJpIY0hHhzF4r4HMmg2U6z+XSEe gFrn6B0HLzvBxorDbPtqpOyUMLhIK5MsybPHSv60lkD2Xx/v9w2v1LgtU3yeYcslNeau tpU0+KMbvc9KFOFyJY1t5aBgD91mHrFEJHRsQCNIzeAB1+sViUR0CFYybPJuM7sYVIen WztFxslUafL/F2l3ppEU3wz1mXaS938TawX+6L3K7EkVyCnOrvXg/wPHpKkFejPbMwcA H+WcRHxK6iyWjDAG1Qy/YiMPXppU62Altoq2DqDNJFdOWNzMFi+phLYQJoce01pKVsxG j7BQ== 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; bh=yviKRh7GnhDoQ7JmmUcxZHCfmO+FtKgwaIVywg3KTW8=; b=m61Jto4l0ddrxRWrJQytnVBkYjO865D80FjgQ3BRLXB/QjU1xkd8DcEAizRShFfcwA GweeU0vySqPJgMI0FlqjmPkIIgSA8M2g+UYb6wcOm1jT9QBPCdH7aBPveguDAsUpX2Ei afg5McTMpoAmzu7l7GVyIvp27OylxBG+d/c5/LyfaZH61zpk92LSAO5+fuKCfsMb7x8w Z1+2o1SRBvUXXnl0+t34GDa9FtaffStAB40dl//Sgipxo/RFcZX7Hcx8ha4qVvPXo7bP +8XwckxZTx8OSzqBkqyAfyPBRRwE1xA2qp2tRzctGm6o9ULz7U51LVYHr6fc093iKA4Y 6sFg== X-Gm-Message-State: AGi0Puau5HWVYR1fgv8W71L2muxWZuJFwY4zXv8NfkhPzcO3DI6FRa9R CHgNxAE98yuzXIaXhrp5n8MOW6m/DW7MyCiD+0KCGVx5XX8= X-Google-Smtp-Source: APiQypKqLUEb0z46/wQEMmR0NHnTyoq0JAN65fnboBF6qnLR1o7b6P/l3x+y82iXjmgINaYl0m267e0OpZbzpWSMNV4= X-Received: by 2002:a37:a45:: with SMTP id 66mr7113492qkk.395.1587204101557; Sat, 18 Apr 2020 03:01:41 -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: Gabriel Scherer Date: Sat, 18 Apr 2020 12:01:01 +0200 Message-ID: To: Kenichi Asai Cc: caml users Content-Type: multipart/alternative; boundary="000000000000a8d1d105a38dc0ef" Subject: Re: [Caml-list] Locally abstract parameterized types? Reply-To: Gabriel Scherer X-Loop: caml-list@inria.fr X-Sequence: 18105 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: --000000000000a8d1d105a38dc0ef Content-Type: text/plain; charset="UTF-8" Dear Kenichi, You can have existentials with GADTs: type _ t = | A : 'a * ('a -> 'v t) -> 'v t | V : 'v -> 'v t let test : bool t = A (3, fun x -> V true) (Another approach, simpler than modules, is to use a double universal encoding: (exists a. T[a]) becomes (forall b. (forall a. T[a] -> b) -> b) ) On Sat, Apr 18, 2020 at 11:47 AM Kenichi Asai wrote: > 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 > --000000000000a8d1d105a38dc0ef Content-Type: text/html; charset="UTF-8" Content-Transfer-Encoding: quoted-printable
Dear Kenichi,

You can have e= xistentials with GADTs:

=C2=A0 type _ t =3D
=C2= =A0 | A : 'a * ('a -> 'v t) -> 'v t
=C2=A0 | V : &= #39;v -> 'v t

=C2=A0 let test : bool t =3D A (3, fun x -> = V true)

(Another approach, simpler than modules, i= s to use a double universal encoding:
=C2=A0 (exists a. T[a])
becomes
=C2=A0 (forall b. (forall a. T[a] -> b) -> b= )
)



On Sat, Apr 18, 2020= at 11:47 AM Kenichi Asai <asai@is= .ocha.ac.jp> wrote:
Thank you, Gabriel.

> No, this is currently not supported. For this use-case you will have t= o use
> modules, typically a functor (in some circumstances a first-class modu= le
> parameter may work as well, if the return type does not depend on the<= br> > parameter).

Let me ask a possibly related question.=C2=A0 I want to define types
similar to the following:

type 'v pair_t =3D {pair : 'a. 'a * ('a -> 'v t)} and 'v t =3D
=C2=A0 A of 'v pair_t
| V of 'v

but where the type 'a of the pair field should be existential, rather than universal.=C2=A0 Since the above definition is universal, I get an
error for the following definition:

let test : bool t =3D A {pair =3D (3, fun x -> V true)}

Error: This field value has type int * (int -> bool t)
=C2=A0 =C2=A0 =C2=A0 =C2=A0which is less general than 'a. 'a * (= 9;a -> 'v t)

To implement an existential type, we need to use modules.=C2=A0 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 =3D sig
=C2=A0 type a
=C2=A0 type v
=C2=A0 val pair : a * (a -> v)=C2=A0 =C2=A0(* not a -> v t *)
end

type 'v t1 =3D
=C2=A0 A of (module Pair1_t with type v =3D 'v)
| V of 'v

Now I can define (3, fun x -> true) as follows:

let test1 : bool t1 =3D
=C2=A0 let module Pair1 =3D struct
=C2=A0 =C2=A0 type a =3D int
=C2=A0 =C2=A0 type v =3D bool
=C2=A0 =C2=A0 let pair =3D (3, fun x -> true)
=C2=A0 end in
=C2=A0 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 =3D sig
=C2=A0 type a
=C2=A0 type t
=C2=A0 val pair : a * (a -> t)=C2=A0 =C2=A0(* not a -> v t *)
end

type t2 =3D
=C2=A0 A of (module Pair2_t with type t =3D t2)
| V of bool

Now I can define (3, fun x -> V true) as follows:

let test2 : t2 =3D
=C2=A0 let module Pair2 =3D struct
=C2=A0 =C2=A0 type a =3D int
=C2=A0 =C2=A0 type t =3D t2
=C2=A0 =C2=A0 let pair =3D (3, fun x -> V true)
=C2=A0 end in
=C2=A0 A (module Pair2)

My question is if we can combine these two to achieve my original
goal.=C2=A0 I first write:

module type Pair3_t =3D sig
=C2=A0 type a
=C2=A0 type v
=C2=A0 type 'a t
=C2=A0 val pair : a * (a -> v t)
end

and tried to define:

type 'v t3 =3D
=C2=A0 A of (module Pair3_t with type v =3D 'v and type 'a t =3D &#= 39;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.=C2=A0 But if I try to connect the two definitons with "and"= ;, I get a
syntax error.

You mention a functor, which is suggestive.=C2=A0 I tried to use a
functor, but so far without success.=C2=A0 Can I define my types using a functor?

Thank you in advance.=C2=A0 Sincerely,

--
Kenichi Asai
--000000000000a8d1d105a38dc0ef--