caml-list - the Caml user's mailing list
 help / color / mirror / Atom feed
From: Kenichi Asai <asai@is.ocha.ac.jp>
To: Gabriel Scherer <gabriel.scherer@gmail.com>
Cc: caml users <caml-list@inria.fr>
Subject: Re: [Caml-list] Locally abstract parameterized types?
Date: Sat, 18 Apr 2020 18:47:36 +0900	[thread overview]
Message-ID: <20200418094736.GA80393@pllab.is.ocha.ac.jp> (raw)
In-Reply-To: <CAPFanBHvrnTqq1q0Ony4yqGvZPr9odKw_orZoA5Lje6T_RDRCA@mail.gmail.com>

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

  reply	other threads:[~2020-04-18  9:48 UTC|newest]

Thread overview: 6+ messages / expand[flat|nested]  mbox.gz  Atom feed  top
2020-04-18  2:23 Kenichi Asai
2020-04-18  7:35 ` Gabriel Scherer
2020-04-18  9:47   ` Kenichi Asai [this message]
2020-04-18 10:01     ` Gabriel Scherer
2020-04-18 10:04     ` Jeremy Yallop
2020-04-18 11:00       ` Kenichi Asai

Reply instructions:

You may reply publicly to this message via plain-text email
using any one of the following methods:

* Save the following mbox file, import it into your mail client,
  and reply-to-all from there: mbox

  Avoid top-posting and favor interleaved quoting:
  https://en.wikipedia.org/wiki/Posting_style#Interleaved_style

* Reply using the --to, --cc, and --in-reply-to
  switches of git-send-email(1):

  git send-email \
    --in-reply-to=20200418094736.GA80393@pllab.is.ocha.ac.jp \
    --to=asai@is.ocha.ac.jp \
    --cc=caml-list@inria.fr \
    --cc=gabriel.scherer@gmail.com \
    /path/to/YOUR_REPLY

  https://kernel.org/pub/software/scm/git/docs/git-send-email.html

* If your mail client supports setting the In-Reply-To header
  via mailto: links, try the mailto: link
Be sure your reply has a Subject: header at the top and a blank line before the message body.
This is a public inbox, see mirroring instructions
for how to clone and mirror all data and code used for this inbox;
as well as URLs for NNTP newsgroup(s).