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 #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 --]

```
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 #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 --]

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

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