This style of recursion in datatype definitions is called "non-regular": the recursive type 'a t
is reused at an instance foo t
where foo
is different from the single variable 'a
used in the definition. Another well-known example is the type of full binary trees (with exactly 2^n leaves):
type 'a full_tree =
| Leaf of 'a
| Node of ('a * 'a) full_tree
Recursive functions that operate these datatypes typically suffer from the monomorphic recursion restriction of languages with type inference. When you do type inference you have to make a guess at what the type of a recursive function may be, before type-checking its body (as it may be use inside). ML languages refine this guess by unification/inference, but only monomorphic types may be inferred. If your function makes polymorphic uses of itself (it calls itself recursively on a different type that what it took as input), this cannot be inferred (it is undecidable in the general case).
let rec depth = function
| Leaf _ -> 1
| Node t -> 1 + depth t
^
Error: This expression has type ('a * 'a) full_tree
but an expression was expected of type 'a full_tree
Since 3.12, OCaml allows to use an explicit polymorphic annotation of
the form 'a 'b . foo
, meaning forall 'a 'b. foo
:
let rec depth : 'a . 'a full_tree -> int = function
| Leaf _ -> 1
| Node t -> 1 + depth t
You could do the same in your example. However, I wasn't able to
compile the type after using the annotation you have in your module
signature, as it appear to be wrong (the 'a_t
are just weird). Here
is what I used to make it work:
let rec map : 'a 'b . ('a -> 'b) -> ('a Op1.t -> 'b Op1.t) ->
('a, 'a Op1.t) t -> ('b, 'b Op1.t) t
= fun f g n -> match n with
| Leaf (a, b) -> Leaf (f a, g b)
| Inner (a, x, y) -> Inner (f a, map f (Op1.map f) x, map f g y)