OCaml type binding in recursive modules

Question

I am trying to build a sequence of recursive modules in ocaml. Here is a minimally simple example:

  module rec Foo : sig
    type t =
      | A of int
      | B of Foo.t
  end = struct
    type t =
      | A of int
      | B of Foo.t
  end       

  module rec Bar : sig
    open Foo
    type map_t = int -> Foo.t
    type t = { foo : map_t }
    val bar_of_foo : Foo.t -> t
  end = struct
    open Foo

    let rec bar_of_foo f = match f with
      | A a -> let ff (_:int) = a in 
               { Bar.foo = ff }
      | B b -> { foo = bar_of_foo b.foo } 
  end

Compilation fails in function bar_of_foo, in the match of A, with Error: unbound type constructor f.

I don't understand why this is happening - field foo is defined as having type map_t = int -> Foo.t, and f has signature int -> Foo.t.

I've also tried simply referring to record field foo as foo rather than Bar.foo (in the match case for B - that gives me an Errror: unbound record field foo error).

Any pointers or advice gratefully received.

Steve

(1) The innermost f (the outermost f being a parameter to bar_of_foo) has signature int -> int, since it uses a : int as its return value. I think it's a good idea to remove the name clash. (2) I fail to see recursive dependencies between Foo and Bar. I just see that Bar uses Foo, but not the other way around. — Anton Trunov
OK, so what I don't understand is how the typing is resolving in bar_of_foo. The first line: ` | A a -> let ff (_:int) = a in { Bar.foo = ff }` starts by matching with type A ( = Foo.A). And, the type of Foo.A is int. So I understand why the signature of ff is int -> int. But A is one of the variants of Foo.t, so why can bar_of_foo not have signature Foo.t -> int ? — Steve Gooberman-Hill

Anton Trunov Anton Trunov · Accepted Answer · 2016-05-25T15:05:16

Since bar_of_foo is a function it has type x -> y.
The type inference algorithm sees that you pattern-match the argument f on the constructors of Foo.t. This fact fixes x = Foo.t.
When you return {foo = ...} the system gets y = Bar.t (or just t in our context).
So, bar_of_foo : Foo.t -> Bar.t.

The following code compiles and it is similar to the code in the OP:

module Foo : sig
  type t =
  | A of int
  | B of t
  end = struct
  type t =
      | A of int
      | B of t
  end

module Bar : sig
  type map_t = int -> Foo.t
  type t = { foo : map_t }
  val bar_of_foo : Foo.t -> t
  end = struct
    open Foo

    type map_t = int -> Foo.t
    type t = { foo : map_t }

    let rec bar_of_foo f = match f with
      | A a -> { foo = fun (_:int) -> A a }
      | B b -> bar_of_foo b 
  end

A test:

open Foo
open Bar

let () =
  let bar = bar_of_foo (B (B (B (A 42)))) in
  match (bar.foo 0) with
    | A n -> print_int n; print_newline ()
    | B _ -> print_string "Impossible!\n"

And the output:

$ ocaml example.ml
$ 42

Note that the modules Foo and Bar are not mutually-recursive. Otherwise we would have to write

module rec Foo : sig
  ...
  end = struct
  ...
  end
and Bar : sig
  ...
  end = struct
    ... 
  end

OCaml type binding in recursive modules

2 Answers