Re: [Caml-list] module types and polymorphic variants

[Jacques Garrigue <garrigue@kurims.kyoto-u.ac.jp>]

From: David Monniaux <David.Monniaux@ens.fr>
> I tried the following:
> 
> module type MT =
> sig
>   type t
>   val f: t->int
> end with type t = 'x constraint 'x = [> `A];;
> 
> ocaml gives me:
> module type MT = sig type t = [> `A] val f : t -> int end

This is already strange. Probably a bug: the definition of t should
not be accepted. Or is it ok because this is only an abstract
signature, not the signature of an actual module ?

> but this latter definition is NOT accepted by OCaml:
> "Unbound type parameter [..]"

That seems more reasonable :-)

> module N (M : MT) =
> struct
>   type t = [M.t | `B]
>   let f: t->int = function
>       `B -> 1
>     | x -> M.f x
> end;;
> 
> The functor definition is refused because
> "The type M.t is not a polymorphic variant type"
> 
> Is there a workaround?

Not that I know. Polymorphic variant extension only works for known
closed variant types, otherwise it would not be sound.

Note that all the above code would work if you defined type t = [ `A ]
to begin with, but this is probably not what you want.

# module type MT =
  sig
    type t = [ `A ]
    val f: t->int
  end;;
module type MT = sig type t = [ `A] val f : t -> int end
# module N (M : MT) =
  struct
    type t = [M.t | `B]
    let f: t->int = function
        `B -> 1
      | #M.t as x -> M.f x
  end;;
module N : functor (M : MT) -> sig type t = [ `A | `B] val f : t -> int end

For incremental extension of an unknown type, you must use a disjoint
sum. The coalesced sum provided by polymorphic variant extension will
not work.

module type MT = sig type t val f : t -> int end;;
module N (M : MT) =
  struct
    type t = [ `Inh of M.t | `B ]
    let f: t->int = function
        `B -> 1
      | `Inh x -> M.f x
  end;;

Theoretical thought: some other frameworks based on extensible rows
would allow what your write, but I'm starting to think that what they
provide is not coalesced sum, but rather a flattened form of disjoint
sum. Nice for some things, but harder to reason about for others.

Jacques Garrigue
-------------------
Bug reports: http://caml.inria.fr/bin/caml-bugs  FAQ: http://caml.inria.fr/FAQ/
To unsubscribe, mail caml-list-request@inria.fr  Archives: http://caml.inria.fr