How to map modules to a module type in OCaml?

3
votes

I want to define a module type that depends on other modules. I thought I could do it with a functor, but I believe functors are only mappings from modules to modules and it's not possible to use them to define mappings from a module to a module type.

Here's an example of what I'd like to do:

module type Field =
sig
  type t
  val add : t -> t -> t
  val mul : t -> t -> t
end

module type Func (F1 : Field) (F2 : Field) =
sig
  val eval : F1.t -> F2.t
end

module FuncField (F1 : Field) (F2 : Field) (F : Func F1 F2) =
struct
  let eval a = F.eval a
  let add a b = F2.add (F.eval a) (F.eval b)
  let mul a b = F2.mul (F.eval a) (F.eval b)
end

I have a Field module type, like the real and rational numbers for example, and I want to define the type of functions Func from one field to another, which is F1.t -> F2.t for any two given modules F1, F2. With those module types in place, I can then define FuncField, which takes F1, F2, F and basically augments F.eval with add and mul.

When I run the code, I get a generic Error: Syntax error in the line where I define Func. Is there a way to define something like this in OCaml?

I'm not sure if this requires dependent types, but I'm mildly familiar with Coq, which has dependent types, and it didn't complain when I defined an equivalent construct:

Module Type Field.
  Parameter T : Type.
  Parameter add : T -> T -> T.
  Parameter mul : T -> T -> T.
End Field.

Module Type Func (F1 : Field) (F2 : Field).
  Parameter eval : F1.T -> F2.T.
End Func.

Module FuncField (F1 : Field) (F2 : Field) (F : Func F1 F2).
  Definition eval a := F.eval a.
  Definition add a b := F2.add (F.eval a) (F.eval b).
  Definition mul a b := F2.mul (F.eval a) (F.eval b).
End FuncField.
2
ocaml

2 Answers

4
votes

Functors are functions from modules to modules. There is no such thing as a functor from module type to module type .... but you can cheat. :)

Unlike Coq, OCaml's modules are not fully dependent types, but they are "dependent enough" in this case. The idea is that modules can contain module types. Since we can't return a module type directly, we will simply return a module that contain one!

Your example become like that:

module type Field = sig
  type t
  val add : t -> t -> t
  val mul : t -> t -> t
end

module Func (F1 : Field) (F2 : Field) = struct
  module type T = sig
    val eval : F1.t -> F2.t
  end
end

module FuncField (F1 : Field) (F2 : Field) (F : Func(F1)(F2).T) = struct
  let eval a = F.eval a
  let add a b = F2.add (F.eval a) (F.eval b)
  let mul a b = F2.mul (F.eval a) (F.eval b)
end

Note the Func(F1)(F2).T syntax, which says "apply the functor, and out of the result, take the module type T". This combination of functor application + field access is only available in types (either normal ones or module types).

I don't remember where I found that trick first, but you can see it in action "in production" in tyxml (definition, usage).

1
votes

Going outside the box a little since it doesn't seem like you really need a functor to accomplish what you describe. Simple module constraints might suffice:

module type Field =
sig
  type t
  val add : t -> t -> t
  val mul : t -> t -> t
end

module type Func =
sig
  type t1
  type t2
  val eval : t1 -> t2
end

module FuncField (F1 : Field) (F2 : Field) (F : Func with type t1 = F1.t and type t2 = F2.t) =
struct
  let eval a = F.eval a
  let add a b = F2.add (F.eval a) (F.eval b)
  let mul a b = F2.mul (F.eval a) (F.eval b)
end