CODEWITHSUNDEEP
moduleocamlfunctor
Del
Del

Reputation: 1319

How does one state that a module implements an interface so that a type in the signature is the same as another type?

I am creating monads in OCaml and need to compose them, so I created transformers. I implemented the regular monad in terms of the transformer with the Identity monad:

module type MONAD = sig
  type 'a m
  val (>>=) : 'a m -> ('a -> 'b m) -> 'b m
  val return : 'a -> 'a m
end

module Identity : MONAD = struct
  type 'a m = 'a
  let (>>=) m f = f m
  let return x = x
end

module OptionT (M : MONAD) : MONAD with type 'a m := ('a option) M.m = struct
  type 'a m = ('a option) M.m
  let (>>=) m f = M.(>>=) m (fun option ->
    match option with
    | Some x -> f x
    | None -> M.return None)
  let return x = M.return @@ Some x
end

module Option = OptionT(Identity)

However, I can't do this:

open Option
let _ = (Some 1) >>= (fun x -> Some (x + 1))

The errors are:

(Some 1)

This expression has type 'a option
    but an expression was expected of type 'b option Identity.m

Some (x + 1)

This expression has type 'a option
    but an expression was expected of type 'b option Identity.m

If I try to fix the error with module Identity : MONAD with type 'a m = 'a I get an error at module Option = OptionT(Identity) that states that

The type `m' is required but not provided

It seems that now, 'a has replaced 'a m in the signature.

Doing

module Option : MONAD with type 'a m := 'a option = struct
  type 'a m = 'a option
    let (>>=) m f =
      match m with
      | Some x -> f x
      | None -> None
  let return x = Some x
end

works just fine.

How do I tell the compiler that a module implements a signature so that a type declared in the signature is the same as another type, while still keeping the signature's original type declaration?

Upvotes: 1

Views: 110

Answers (2)

octachron
octachron

Reputation: 18912

It seems that now, 'a has replaced 'a m in the signature.

This the effect of destructive substitution, when you write

module Identity : MONAD with type 'a m := 'a

you are asking the compiler to substitute all instance of 'a m by 'a. Contrarily, standard with constraint adds a type equality to the module type

 module Identity : MONAD with type 'a m = 'a

Looking at your various examples, it seems that you have confused the two, and are using destructive substitution when you meant to add a type constraint:

module OptionT(X:Monad) : MONAD with type 'a m = 'a = …
(* or *) module Option : MONAD with type 'a m = 'a option = …

and not 

module OptionT(X:Monad) : MONAD with type 'a m := 'a = …
(* nor *) module Option : MONAD with type 'a m := 'a option = …

Upvotes: 5

Étienne Millon
Étienne Millon

Reputation: 3028

This expression has type 'a option but an expression was expected of type 'b option Identity.m

And indeed, the compiler does not know anything about Identity except that its signature is MONAD. (: MONAD) is not something that merely helps the compiler, it hides all information about Identity except that its signature is MONAD.

So, you can add a type equality for that

module Identity : MONAD with type 'a m = 'a = ...

and it works.

Upvotes: 0

Related Questions