How can I instantiate a functor module type at a particular input module?

Learning
1

I have read many posts here about modules but the following still isn’t clear to me. If Foo is a module of type FOO, and BAR is a module type for a functor that accepts some Foo:FOO and defines something else, how can I get the “something else”? In other words how do I say that some module Bar has type BAR Foo? In code:

module type FOO =
  sig
    type t
    val x : t
  end

module type BAR =
  functor (Foo:FOO) ->
  sig
    val y : Foo.t
  end

module Foo : FOO =
  struct
    type t = bool
    let x = true
  end


(** Doesn't work  *)
module Bar : BAR Foo =
  struct
    let y = Foo.x
  end


(** Doesn't work *)
module type BAR_At_Foo = BAR (Foo)

How can I, or why can’t I, do this?

My understanding of the module system is such that I think this is completely reasonable and doesn’t pose any problems whatsoever–it is approximately like instantiating a dependent product type at a particular value, all of which is known at compile time. So please disabuse me of this idea if I’m being naïve.

In anticipation of questions: My use case is that Foo is some configuration module that defines some types and Bar:BAR is a module that provides functionality whose types depend on the types from Foo. My library accepts a Foo:FOO and Bar:BAR(Foo) and returns something very complicated. I am aware that I could merge Foo and Bar into one massive module, or better yet a record, but I’m very interested in understanding this from a dependent types perspective.

(I hope the answer is not that I’ve encoded some obvious undecidability that I’m blindly overlooking.)

2

Nevermind. I looked at this paper


particularly sections 2.3 and 2.4. This is more subtle than I realized when dealing with nested modules.

1 Like
3

What you want is a function from module to module type. Let’s recap:

input output construct
value value functions
type type Type constructors ('a t)
modules modules Functors
module type module type Missing!
value/type value/type Dependent arrows (see the lambda cube)
value/module value/module First class modules
module/module type module/module type What you want

Fortunately, modules can contain pretty much anything, which allows us to be a bit creative! Here’s a version of your code that uses the fact that modules can contains module types to compute on module types.

module type FOO =
  sig
    type t
    val x : t
  end

module BAR (Foo:FOO) = struct
  module type T = sig
    val y : Foo.t
  end
end

module Foo : FOO =
  struct
    type t = bool
    let x = true
  end

module Bar : BAR(Foo).T =
  struct
    let y = Foo.x
  end

module type BAR_At_Foo = BAR(Foo).T

In the end, there is no technical reason not to have Dependent Functors in the language, and as you can see, it’s pretty easy to encode already. Since it’s so easy, there is no strong incentive to add yet another “sort of functions”.

There would be extremely good reasons to allow mixing normal polymorphism and module parameterization, but that’s another story …

5 Likes