From: Jacques Garrigue <garrigue@math.nagoya-u.ac.jp>
To: Markus Mottl <markus.mottl@gmail.com>
Cc: OCaml List <caml-list@inria.fr>
Subject: Re: [Caml-list] Manifest types in module type inclusions
Date: Sun, 26 Dec 2010 14:56:28 +0900 [thread overview]
Message-ID: <1988FE07-0BE7-41C7-911A-FBC8DC9530EE@math.nagoya-u.ac.jp> (raw)
In-Reply-To: <AANLkTikyvcJNH2iQQQ9bSB4x0j1Y2egexHCKg-XiHDY0@mail.gmail.com>
On 2010/12/26, at 14:19, Markus Mottl wrote:
> please consider the following code:
>
> -------------------
> module M = struct type t = A | B end
>
> module X : sig
> (* type t = M.t = A | B *)
> include module type of M
> (* include module type of M with type t = M.t = A | B *)
> end = struct include M end
>
> let () = assert (M.A = X.A)
> -------------------
>
> This will fail, because M.A is not of the same type as X.A. But I
> would really like to make the types equivalent.
>
> Using the first commented out line instead of the module type
> inclusion will succeed, but then I would not be able to automatically
> include any functions potentially contained in module M. The last
> commented out line won't work, because one cannot establish a type
> equivalence via a manifest type definition after "with type". Even
> if, I don't think one could override anything else but an abstract
> type that way, and we are including a sum type here already.
>
> Does anybody have any suggestions for a workaround? I suspect this
> may be a missing feature.
Unfortunately there is no easy workaround using 3.12.0.
Intuitively at least the 3rd line should work, but a bug prevents this.
In 3.12.1, you should be able to write either the 3rd, or the
simpler following version:
include module type of M with type t = M.t
This should solve your problem.
Side note: the choice to make "include M" define "type t = A | B"
rather than "type t = M.t = A | B" was done to allow more implementations
(any module defining the same operations as M is allowed, rather
than modules sharing the same representation for types.)
But it resulted in not allowing the code you write here, which was
not intentional.
Jacques Garrigue
prev parent reply other threads:[~2010-12-26 5:56 UTC|newest]
Thread overview: 2+ messages / expand[flat|nested] mbox.gz Atom feed top
2010-12-26 5:19 Markus Mottl
2010-12-26 5:56 ` Jacques Garrigue [this message]
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=1988FE07-0BE7-41C7-911A-FBC8DC9530EE@math.nagoya-u.ac.jp \
--to=garrigue@math.nagoya-u.ac.jp \
--cc=caml-list@inria.fr \
--cc=markus.mottl@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