CODEWITHSUNDEEP
ocaml
Mike Shulman
Mike Shulman

Reputation: 167

Parametrically polymorphic modules

Here is a simple OCaml module type for a monad:

module type Monad = sig
  type 'a t
  val return : 'a -> 'a t
  val bind : 'a t -> ('a -> 'b t) -> 'b t
end

I can instantiate this with any particular monad, such as the reader monad for some type r:

module Reader_monad : Monad = struct
  type 'a t = r -> 'a
  let return a = fun _ -> a
  let bind o f = fun x -> f (o x) x
end

And I can parametrize it over the type r by using a functor:

module type Readable = sig type r end
module Reader (R : Readable) : Monad = struct
  type 'a t = R.r -> 'a
  let return a = fun _ -> a
  let bind o f = fun x -> f (o x) x
end

However, the latter approach requires that I instantiate different instances of the functor for different types r. Is there any way to define a "parametrically polymorphic" module of type Monad that would give parametrically polymorphic functions like return : 'a -> ('r -> 'a)?

I think can get more or less what I want with a separate module type for "families of monads":

module type Monad_family = sig
  type ('c, 'a) t
  val return : 'a -> ('c, 'a) t
  val bind : ('c, 'a) t -> ('a -> ('c, 'b) t) -> ('c, 'b) t
end

module Reader_family : Monad_family = struct
  type ('c, 'a) t = 'c -> 'a
  let return a = fun _ -> a
  let bind o f = fun x -> f (o x) x
end

But if I have a substantial library of general facts about monads, this would require modifying it everywhere manually to use families. And then some monads are parametrized by a pair of types (although I suppose that could be encoded by a product type), etc. So I would rather avoid having to do it this way.

If this isn't directly possible, is there at least a way to instantiate the module Reader locally inside a parametrically polymorphic function? I thought I might be able to do this with first-class modules, but my naive attempt

let module M = Reader(val (module struct type r = int end) : Readable) in M.return "hello";;

produces the error message

Error: This expression has type string M.t
       but an expression was expected of type 'a
       The type constructor M.t would escape its scope

which I don't understand. Isn't the type M.t equal to int -> string?

Upvotes: 0

Views: 328

Answers (1)

Kevin Ji
Kevin Ji

Reputation: 10489

I think this is the same issue as The type constructor "..." would escape its scope when using first class modules, where the module M doesn't live long enough. If you instead wrote

# module M = Reader(struct type r = int end);;
# M.return "hello";;
- : string M.t = <fun>

then this would work fine.

Separately, the Reader functor loses some type equalities that you might want. You can restore them by defining it as such:

module Reader (R : Readable) : Monad with type 'a t = R.r -> 'a = struct
  type 'a t = R.r -> 'a
  let return a = fun _ -> a
  let bind o f = fun x -> f (o x) x
end

Upvotes: 1

Related Questions