[Caml-list] Locally abstract parameterized types?

[Caml-list] Locally abstract parameterized types?

[Kenichi Asai]

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

Re: [Caml-list] Locally abstract parameterized types?

[Gabriel Scherer]

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

Re: [Caml-list] Locally abstract parameterized types?

[Kenichi Asai]

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

Re: [Caml-list] Locally abstract parameterized types?

[Gabriel Scherer]

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

Re: [Caml-list] Locally abstract parameterized types?

[Jeremy Yallop]

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

Re: [Caml-list] Locally abstract parameterized types?

[Kenichi Asai]

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