From: Jeremy Yallop <yallop@gmail.com>
To: Kenichi Asai <asai@is.ocha.ac.jp>
Cc: Gabriel Scherer <gabriel.scherer@gmail.com>,
caml users <caml-list@inria.fr>
Subject: Re: [Caml-list] Locally abstract parameterized types?
Date: Sat, 18 Apr 2020 10:04:49 +0000 [thread overview]
Message-ID: <CAAxsn=HCuWJz1mgGEKaGSay9tCZUAXW8fTXzCP5Vx2nKNFMQww@mail.gmail.com> (raw)
In-Reply-To: <20200418094736.GA80393@pllab.is.ocha.ac.jp>
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
next prev parent reply other threads:[~2020-04-18 10:05 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
2020-04-18 10:01 ` Gabriel Scherer
2020-04-18 10:04 ` Jeremy Yallop [this message]
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='CAAxsn=HCuWJz1mgGEKaGSay9tCZUAXW8fTXzCP5Vx2nKNFMQww@mail.gmail.com' \
--to=yallop@gmail.com \
--cc=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