*[Caml-list] Locally abstract parameterized types?@ 2020-04-18 2:24 Kenichi Asai2020-04-18 7:36 ` Gabriel Scherer 0 siblings, 1 reply; 6+ messages in thread From: Kenichi Asai @ 2020-04-18 2:24 UTC (permalink / raw) To: caml-list OCaml allows locally abstract types: let f (type t) x = ... Can the t take parameters as in 'a t? I want to have a locally abstract type that has type parameters. The manual says the t in (type t) must be {typeconstr-name}+ which expands to a sequence of lowercase-ident, so probably this is not allowed... -- Kenichi Asai ^ permalink raw reply [flat|nested] 6+ messages in thread

*Re: [Caml-list] Locally abstract parameterized types?2020-04-18 2:24 [Caml-list] Locally abstract parameterized types? Kenichi Asai@ 2020-04-18 7:36 ` Gabriel Scherer2020-04-18 9:48 ` Kenichi Asai 0 siblings, 1 reply; 6+ messages in thread From: Gabriel Scherer @ 2020-04-18 7:36 UTC (permalink / raw) To: Kenichi Asai; +Cc: caml users [-- Attachment #1: Type: text/plain, Size: 670 bytes --] Dear Kenichi, 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). On Sat, Apr 18, 2020 at 4:24 AM Kenichi Asai <asai@is.ocha.ac.jp> wrote: > OCaml allows locally abstract types: > > let f (type t) x = ... > > Can the t take parameters as in 'a t? I want to have a locally > abstract type that has type parameters. The manual says the t in > (type t) must be {typeconstr-name}+ which expands to a sequence of > lowercase-ident, so probably this is not allowed... > > -- > Kenichi Asai > [-- Attachment #2: Type: text/html, Size: 1028 bytes --] ^ permalink raw reply [flat|nested] 6+ messages in thread

*Re: [Caml-list] Locally abstract parameterized types?2020-04-18 7:36 ` Gabriel Scherer@ 2020-04-18 9:48 ` Kenichi Asai2020-04-18 10:01 ` Gabriel Scherer 2020-04-18 10:05 ` Jeremy Yallop 0 siblings, 2 replies; 6+ messages in thread From: Kenichi Asai @ 2020-04-18 9:48 UTC (permalink / raw) To: Gabriel Scherer; +Cc: caml users 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 ^ permalink raw reply [flat|nested] 6+ messages in thread

*Re: [Caml-list] Locally abstract parameterized types?2020-04-18 9:48 ` Kenichi Asai@ 2020-04-18 10:01 ` Gabriel Scherer2020-04-18 10:05 ` Jeremy Yallop 1 sibling, 0 replies; 6+ messages in thread From: Gabriel Scherer @ 2020-04-18 10:01 UTC (permalink / raw) To: Kenichi Asai; +Cc: caml users [-- Attachment #1: Type: text/plain, Size: 3167 bytes --] 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 <asai@is.ocha.ac.jp> 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 > [-- Attachment #2: Type: text/html, Size: 4222 bytes --] ^ permalink raw reply [flat|nested] 6+ messages in thread

*Re: [Caml-list] Locally abstract parameterized types?2020-04-18 9:48 ` Kenichi Asai 2020-04-18 10:01 ` Gabriel Scherer@ 2020-04-18 10:05 ` Jeremy Yallop2020-04-18 11:01 ` Kenichi Asai 1 sibling, 1 reply; 6+ messages in thread From: Jeremy Yallop @ 2020-04-18 10:05 UTC (permalink / raw) To: Kenichi Asai; +Cc: Gabriel Scherer, caml users On Sat, 18 Apr 2020 at 09:49, Kenichi Asai <asai@is.ocha.ac.jp> 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 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. Here's one fairly direct way to do that: type 'v pair_t = Pair : ('a * ('a -> 'v t)) -> 'v pair_t and 'v t = A of 'v pair_t | V of 'v let test : bool t = A (Pair (3, fun x -> V true)) But, since '∃a.(a × (a → t))' is isomorphic to 'unit → t', you can write the example more simply, without universal or existential types: type 'v t = A of (unit -> 'v t) | V of 'v let a x f = A (fun () -> f x) let test : bool t = 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 = 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 Here's a slight variant of this idea that works by avoiding the parameterized type in Pair3_t: module type Pair3_t = sig type a type vt val pair : a * (a -> vt) end type 'v t = A of (module Pair3_t with type vt = 'v t) | V of 'v let test : bool t = A (module struct type a = int type vt = bool t let pair = (3, fun x -> V true) end) Kind regards, Jeremy ^ permalink raw reply [flat|nested] 6+ messages in thread

*2020-04-18 10:05 ` Jeremy YallopRe: [Caml-list] Locally abstract parameterized types?@ 2020-04-18 11:01 ` Kenichi Asai0 siblings, 0 replies; 6+ messages in thread From: Kenichi Asai @ 2020-04-18 11:01 UTC (permalink / raw) To: Jeremy Yallop; +Cc: Gabriel Scherer, caml users Thank you, Gabriel and Jeremy. The GADT approach went well. I thought I considered GADTs, too, but it seems I did not pursue it enough. Thanks again. -- Kenichi Asai ^ permalink raw reply [flat|nested] 6+ messages in thread

end of thread, back to indexThread overview:6+ messages (download: mbox.gz / follow: Atom feed) -- links below jump to the message on this page -- 2020-04-18 2:24 [Caml-list] Locally abstract parameterized types? Kenichi Asai 2020-04-18 7:36 ` Gabriel Scherer 2020-04-18 9:48 ` Kenichi Asai 2020-04-18 10:01 ` Gabriel Scherer 2020-04-18 10:05 ` Jeremy Yallop 2020-04-18 11:01 ` Kenichi Asai

caml-list - the Caml user's mailing list Archives are clonable: git clone --mirror https://inbox.ocaml.org/caml-list AGPL code for this site: git clone https://public-inbox.org/ public-inbox