First class module and existential type

Learning
1

After being lazy for some years, I decided to get a grasp of first class modules. So far so good but I’m currently stuck within my experiments mainly in relation to the way one can add typing constraints to such module values.

Writing a function apply of type ('a -> 'b) -> 'a -> 'b is done trivially as let apply f arg = f arg.

Suppose that it is not one function but a set of functions I want to give to apply. I can define a module and use first class modules.

module type MTYPE = sig type input type output val f: input -> output end
let apply1 m arg =
  let module M = (val m: MTYPE) in
  M.f arg

This code raise an error: The type constructor M.input would escape its scope. One possible solution is to use existential types:

let apply2 (type a b) m arg =
  let module M = (val m: MTYPE with type input = a and type output = b) in
  M.f arg

This code compiles and works great but it forces me to define the types input and output in the implementations though the typer computed them…

Q1: is there a way to do this without requiring the developer to define input and output? I would have liked to say:

let apply3 (type a b) m arg =
  let module M = (val m: sig val f: a -> b end) in
  M.f arg

but the compiler raises an error: invalid package type: only module type identifier and ‘with type’ constraints are supported.

Sticking with apply2, I now want the module argument to be a functor. For example, supposing:

module type PTYPE = sig type ('a,'b) ty end
module type MTYPE' = functor (P:PTYPE) -> MTYPE

module I: PTYPE =
  struct
    type ('a,'b) ty = ('a * 'b) list
  end

I would like to write:

let apply4 (type a b) m arg =
  let module M = (val m: functor (P:PTYPE) -> sig val f: a -> b end) (I) in
  M.f arg

which is still not possible so I tried:

let apply5 (type a b) m arg =
  let module M = (val m: MTYPE' with type input = a and type output = b) (I) in
  M.f arg

That does not work: Error: This module type is not a signature.

Q2: is there a way to link the input and output type of the functor to my existential types?

Thank you in advance

2

module type MTYPE’ = functor (P:PTYPE) → MTYPE
…
MTYPE’ with type input = a and type output = b

That won’t quite work. The existential is nested underneath the parameter (i.e. that functor type lets the functor choose different input and output for different P). Instead you want to move the existential outside of the functor:

module type MTYPE' = sig
  type a
  type b
  module F : functor (P : PTYPE) -> MTYPE with type input = a type output = b
end
...
MTYPE' with type a = a and type b = b
1 Like
3

Thanks that helped me to get to an acceptable understanding.

4

Continuing my experiments and with the help of the answer of lpw25, I arrived the following form of code:

open Printf
module type MTYPE = sig type input type output val f: input -> output end

type ('a,'b) func = (module MTYPE with type input = 'a and type output = 'b)

let apply (type a b) (m: (a,b) func) arg =
  let module M = (val m) in
  M.f arg

let create: type a b.(a -> b) -> (a,b) func = fun f ->
  let module M =
    struct
      type input = a
      type output = b
      let f = f
    end
  in (module M)

let () =
  printf "\na first test %s\n" (apply (create (fun x -> x)) "yes");
  printf "a second test %i\n" (apply (create List.length) ["yes";"again"])

This code answer to my question Q1… Where it is the existential of the function create that compute the types…

Interestingly, in this form the code extends rather directly to functors and answer to my question Q2:

module type PTYPE = sig type ('a,'b) ty end
module type MTYPE' =
  sig
    type a
    type b
    module F: functor (P:PTYPE) -> MTYPE with type input = a and type output = b
  end

type ('a,'b) func' = (module MTYPE' with type a = 'a and type b = 'b)

module I: PTYPE =
  struct
    type ('a,'b) ty = ('a * 'b) list
  end

let apply' (type a b) (m: (a,b) func') arg =
  let module M = (val m) in
  let module R = M.F (I) in
  R.f arg

let create': type c d.(c -> d) -> (c,d) func' = fun f ->
  let module M =
    struct
      type a = c
      type b = d
      module F (P:PTYPE) =
        struct
          type input = a
          type output = b
          let f = f
        end
    end
  in (module M)

let () =
  printf "\na first test %s\n" (apply' (create' (fun x -> x)) "yes");
  printf "a second test %i\n" (apply' (create' List.length) ["yes";"again"])

This could be helpful for others…

5

module F: functor (P:PTYPE) → sig include MTYPE with type input = a and type output = b end

This can be written as just:

module F: functor (P:PTYPE) -> MTYPE with type input = a and type output = b

(The unnecessary sig .. end probably came from a typo in my example which I have since corrected)

6

I also edited my to reflect it.
Thanks again

7

Following up on the exploration, I tried to write the following code

module type MTYPE = sig type arg type _ t val unpack: arg t -> arg val pack: arg -> arg t end

let apply (type a) m (f: a -> a) arg =
  let module M = (val m: MTYPE with type arg = a) in
  M.pack (f (M.unpack arg))

This code raises an error because the type constructor M.t would escape its scope. Easy, I though let’s define a second existential type:

let apply (type a b) m (f: a -> a) arg =
  let module M = (val m: MTYPE with type arg = a and type _ t = b) in
  M.pack (f (M.unpack arg))

But, that raises another error invalid package type: parametrized types are not supported.

Questions:

  • Is there any fundamental issue in supporting parameterized types or is it a matter of implementation?
  • Is there a way to get around this limitation?
8

Sorry for the slow reply. There are fundamental issues with supporting parametrized types in general. So something like val m: MTYPE with type arg = a and type 'a t = 'a list is definitely going to be a problem. I suspect that this particular case could be allowed – where the parameter of the type does not appear in the body – but no one has thought to add support for it or put the effort in to think through the implications and check it is definitely safe.