Re: [Caml-list] Existential row types

[Leo White <lpw25@cam.ac.uk>]

Hi Alain,

There is a work-around, but it is quite convoluted:

  https://sympa.inria.fr/sympa/arc/caml-list/2012-10/msg00131.html

There is also a feature request for the feature you propose:

  http://caml.inria.fr/mantis/view.php?id=6137

Regards,

Leo

Alain Frisch <alain@frisch.fr> writes:

> Dear all,
>
> GADTs allow to restrict existential type variables to being an instance of a row type, as in:
>
> class type c = ...
>
> type s =
>   | EX: ((#c as 'a) -> unit) * (unit -> 'a) -> ex
>
>
> I'm wondering if it is possible to simulate such restricted existential quantification with first-class module and
> private row types.  Something like:
>
>
> module type S = sig
>   type t = private #c
>   val f: t -> unit
>   val g: unit -> t
> end
>
> let foo (type t_) (f : (#c as t_) -> unit) (g : unit -> t_) =
>   let module M = struct
>     type t = t_
>     let f = f
>     let g = g
>   end
>   in
>   (module M : S)
>
>
> This does not work, of course, because of the "... as t_".  Is there a local work-around?  If not, I'm wondering if if
> would be easy (and make sense) to introduce a form for introducing locally private row types:
>
>  let foo (type t_ = private #c) (f : t_ -> unit) (g : unit -> t_) = ...
>
>
>
> -- Alain