[Caml-list] GADT and local modules

[Caml-list] GADT and local modules

[Thomas Braibant]

Hi list,

I would like to find a way to name (or capture) the variables that are
existentially quantified in a GADT constructor, to put them inside a
module and apply a functor on the said module. Attached below is a
mockup of what I would like to have. (I can live without this coding
pattern, but I would like to know whether or not it is possible to
make it work, even if I suspect that the answer is no).

Best,
Thomas


type t = Pack : 'a * 'b list -> t

(* I want to unpack a t, and put its content in a module of signature S *)
module type S = sig
  type a
  type b
  val foo : (a * b) list
end

(* I want to apply the functor M on my module to produce a result,
whose type does not depend on the types in S.  I am using a functor as
a way to structure the computations that happen inside. I started with
a version without modules, which requires to write quite a few type
annotations... *)
module M (C:S) : sig val result : int end= struct

  include C

 (* Here I want bar to have type (a * b) list. Of course, I could have
bar s a function that takes two type variables as arguments, and a
list, and returns a list of the right type. *)
  let bar = List.rev foo
  let result = List.length bar

end

(* Here, I do not know of a way to retrieve the type variables
quantified in the GADT constructor Pack, to feed them in C *)
let f (t : t) =
  match t with
  | Pack l -> let module C = .... in M(C)

(* alternative with modules, which is not satisfying. *)

module type S = sig
  val t : t
end

module M (C:S) : sig val result : int end = struct

  include C

  (* Now, I can unpack the t locally in each function, but I cannot
     open the existential in the whole module, which is painful. *)

end

Re: [Caml-list] GADT and local modules

[Gabriel Scherer]

You will be familiar with the solution from the Coq world.

  match t with
   | Pack l ->
     begin fun (type a') (type b') l ->
       let module C = struct
         type a = a'
         type b = b'
         let foo = l
      end in
      let module R = M(C) in
      R.result
    end l

On Fri, May 23, 2014 at 10:15 AM, Thomas Braibant
<thomas.braibant@gmail.com> wrote:
> Hi list,
>
> I would like to find a way to name (or capture) the variables that are
> existentially quantified in a GADT constructor, to put them inside a
> module and apply a functor on the said module. Attached below is a
> mockup of what I would like to have. (I can live without this coding
> pattern, but I would like to know whether or not it is possible to
> make it work, even if I suspect that the answer is no).
>
> Best,
> Thomas
>
>
> type t = Pack : 'a * 'b list -> t
>
> (* I want to unpack a t, and put its content in a module of signature S *)
> module type S = sig
>   type a
>   type b
>   val foo : (a * b) list
> end
>
> (* I want to apply the functor M on my module to produce a result,
> whose type does not depend on the types in S.  I am using a functor as
> a way to structure the computations that happen inside. I started with
> a version without modules, which requires to write quite a few type
> annotations... *)
> module M (C:S) : sig val result : int end= struct
>
>   include C
>
>  (* Here I want bar to have type (a * b) list. Of course, I could have
> bar s a function that takes two type variables as arguments, and a
> list, and returns a list of the right type. *)
>   let bar = List.rev foo
>   let result = List.length bar
>
> end
>
> (* Here, I do not know of a way to retrieve the type variables
> quantified in the GADT constructor Pack, to feed them in C *)
> let f (t : t) =
>   match t with
>   | Pack l -> let module C = .... in M(C)
>
> (* alternative with modules, which is not satisfying. *)
>
> module type S = sig
>   val t : t
> end
>
> module M (C:S) : sig val result : int end = struct
>
>   include C
>
>   (* Now, I can unpack the t locally in each function, but I cannot
>      open the existential in the whole module, which is painful. *)
>
> end
>
> --
> Caml-list mailing list.  Subscription management and archives:
> https://sympa.inria.fr/sympa/arc/caml-list
> Beginner's list: http://groups.yahoo.com/group/ocaml_beginners
> Bug reports: http://caml.inria.fr/bin/caml-bugs

Re: [Caml-list] GADT and local modules

[Thomas Braibant]

Oh my. I would never have thought that I could use commutative cuts in
OCaml. I should have thought about this myself, given the time that I
spent playing with these.

For the interested reader, this solution is also called the convoy
pattern in Coq, and is described here
http://adam.chlipala.net/cpdt/html/MoreDep.html

Thanks a lot Gabriel.

On Fri, May 23, 2014 at 9:24 AM, Gabriel Scherer
<gabriel.scherer@gmail.com> wrote:
> You will be familiar with the solution from the Coq world.
>
>   match t with
>    | Pack l ->
>      begin fun (type a') (type b') l ->
>        let module C = struct
>          type a = a'
>          type b = b'
>          let foo = l
>       end in
>       let module R = M(C) in
>       R.result
>     end l
>
> On Fri, May 23, 2014 at 10:15 AM, Thomas Braibant
> <thomas.braibant@gmail.com> wrote:
>> Hi list,
>>
>> I would like to find a way to name (or capture) the variables that are
>> existentially quantified in a GADT constructor, to put them inside a
>> module and apply a functor on the said module. Attached below is a
>> mockup of what I would like to have. (I can live without this coding
>> pattern, but I would like to know whether or not it is possible to
>> make it work, even if I suspect that the answer is no).
>>
>> Best,
>> Thomas
>>
>>
>> type t = Pack : 'a * 'b list -> t
>>
>> (* I want to unpack a t, and put its content in a module of signature S *)
>> module type S = sig
>>   type a
>>   type b
>>   val foo : (a * b) list
>> end
>>
>> (* I want to apply the functor M on my module to produce a result,
>> whose type does not depend on the types in S.  I am using a functor as
>> a way to structure the computations that happen inside. I started with
>> a version without modules, which requires to write quite a few type
>> annotations... *)
>> module M (C:S) : sig val result : int end= struct
>>
>>   include C
>>
>>  (* Here I want bar to have type (a * b) list. Of course, I could have
>> bar s a function that takes two type variables as arguments, and a
>> list, and returns a list of the right type. *)
>>   let bar = List.rev foo
>>   let result = List.length bar
>>
>> end
>>
>> (* Here, I do not know of a way to retrieve the type variables
>> quantified in the GADT constructor Pack, to feed them in C *)
>> let f (t : t) =
>>   match t with
>>   | Pack l -> let module C = .... in M(C)
>>
>> (* alternative with modules, which is not satisfying. *)
>>
>> module type S = sig
>>   val t : t
>> end
>>
>> module M (C:S) : sig val result : int end = struct
>>
>>   include C
>>
>>   (* Now, I can unpack the t locally in each function, but I cannot
>>      open the existential in the whole module, which is painful. *)
>>
>> end
>>
>> --
>> Caml-list mailing list.  Subscription management and archives:
>> https://sympa.inria.fr/sympa/arc/caml-list
>> Beginner's list: http://groups.yahoo.com/group/ocaml_beginners
>> Bug reports: http://caml.inria.fr/bin/caml-bugs