[Caml-list] Existential row types

[Caml-list] Existential row types

[Alain Frisch]

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

Re: [Caml-list] Existential row types

[Leo White]

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

Re: [Caml-list] Existential row types

[Alain Frisch]

Hi Leo,

On 7/15/2014 6:11 PM, Leo White wrote:
 > There is a work-around, but it is quite convoluted:
 >
 >    https://sympa.inria.fr/sympa/arc/caml-list/2012-10/msg00131.html

Very clever trick. Thanks!

One can actually use the GADT only to carry the constraint and pass the 
value argument(s) separately.  This means the GADT definition remains 
very simple even if we need to add many fields:


=============================================================
class type c = object end

module type SIG =
sig
   type t = private #c
   val f: t -> unit
   val g: unit -> t
end

type 'a aux = Aux: (#c as 'a) aux

let create f g =
   let helper (type u) (Aux : u aux) f g =
     (module struct
        type t = u
        let f = f
        let g = g
      end : SIG)
   in
   helper Aux f g

(* or even: *)

let create f g =
   let module Aux = struct type 'a t = E: (#c as 'a) t end in
   begin fun (type u) (Aux.E : u Aux.t) f g ->
     (module struct
        type t = u
        let f = f
        let g = g
      end : SIG)
   end Aux.E f g
=============================================================



-- Alain