# Type checking and recursive types (Writing the Y combinator in Haskell/Ocaml)

When explaining the Y combinator in the context of Haskell, it's usually noted that the straight-forward implementation won't type-check in Haskell because of its recursive type.

For example, from Rosettacode:

The obvious definition of the Y combinator in Haskell canot be used because it contains an infinite recursive type (a = a -> b). Defining a data type (Mu) allows this recursion to be broken.

``````newtype Mu a = Roll { unroll :: Mu a -> a }

fix :: (a -> a) -> a
fix = \f -> (\x -> f (unroll x x)) \$ Roll (\x -> f (unroll x x))
``````

And indeed, the “obvious” definition does not type check:

``````λ> let fix f g = (\x -> \a -> f (x x) a) (\x -> \a -> f (x x) a) g

<interactive>:10:33:
Occurs check: cannot construct the infinite type:
t2 = t2 -> t0 -> t1
Expected type: t2 -> t0 -> t1
Actual type: (t2 -> t0 -> t1) -> t0 -> t1
In the first argument of `x', namely `x'
In the first argument of `f', namely `(x x)'
In the expression: f (x x) a

<interactive>:10:57:
Occurs check: cannot construct the infinite type:
t2 = t2 -> t0 -> t1
In the first argument of `x', namely `x'
In the first argument of `f', namely `(x x)'
In the expression: f (x x) a
(0.01 secs, 1033328 bytes)
``````

The same limitation exists in Ocaml:

``````utop # let fix f g = (fun x a -> f (x x) a) (fun x a -> f (x x) a) g;;
Error: This expression has type 'a -> 'b but an expression was expected of type 'a
The type variable 'a occurs inside 'a -> 'b
``````

However, in Ocaml, one can allow recursive types by passing in the `-rectypes` switch:

``````   -rectypes
Allow  arbitrary  recursive  types  during type-checking.  By default, only recursive
types where the recursion goes through an object type are supported.
``````

By using `-rectypes`, everything works:

``````utop # let fix f g = (fun x a -> f (x x) a) (fun x a -> f (x x) a) g;;
val fix : (('a -> 'b) -> 'a -> 'b) -> 'a -> 'b = <fun>
utop # let fact_improver partial n = if n = 0 then 1 else n*partial (n-1);;
val fact_improver : (int -> int) -> int -> int = <fun>
utop # (fix fact_improver) 5;;
- : int = 120
``````

Being curious about type systems and type inference, this raises some questions I'm still not able to answer.

• First, how does the type checker come up with the type `t2 = t2 -> t0 -> t1`? Having come up with that type, I guess the problem is that the type (`t2`) refers to itself on the right side?
• Second, and perhaps most interesting, what is the reason for the Haskell/Ocaml type systems to disallow this? I guess there is a good reason since Ocaml also will not allow it by default even if it can deal with recursive types if given the `-rectypes` switch.

If these are really big topics, I'd appreciate pointers to relevant literature.

First, the GHC error,

GHC is attempting to unify a few constraints with `x`, first, we use it as a function so

``````x :: a -> b
``````

Next we use it as a value to that function

``````x :: a
``````

And finally we unify it with the original argument expression so

``````x :: (a -> b) -> c -> d
``````

Now `x x` becomes an attempt to unify `t2 -> t1 -> t0`, however, We can't unify this since it would require unifying `t2`, the first argument of `x`, with `x`. Hence our error message.

Next, why not general recursive types. Well the first point worth noting is the difference between equi and iso recursive types,

• equi-recursive are what you'd expect `mu X . Type` is exactly equivalent to expanding or folding it arbitrarily.
• iso-recursive types provide a pair of operators, `fold` and `unfold` which fold and unfold the recursive definitions of types.

Now equi-recursive types sound ideal, but are absurdly hard to get right in complex types systems. It can actually make type checking undecidable. I'm not familiar with every detail of OCaml's type system but fully equirecursive types in Haskell can cause the typechecker to loop arbitrarily trying to unify types, by default, Haskell makes sure that type checking terminates. Further more, in Haskell, type synonyms are dumb, the most useful recursive types would be defined like `type T = T -> ()`, however are inlined almost immediately in Haskell, but you can't inline a recursive type, it's infinite! Therefore, recursive types in Haskell would demand a huge overhaul to how synonyms are handled, probably not worth the effort to put even as a language extension.

Iso-recursive types are a bit of a pain to use, you more or less have to explicitly tell the type checker how to fold and unfold your types, making your programs more complex to read and write.

However, this is very similar to what your doing with your `Mu` type. `Roll` is fold, and `unroll` is unfold. So actually, we do have iso-recursive types baked in. However, equi-recursive types are just too complex so systems like OCaml and Haskell force you to pass recurrences through type level fixpoints.

Now if this interests you, I'd recommend Types and Programming Languages. My copy is sitting open in my lap as I'm writing this to make sure I've got the right terminology :)

• In particular chapter 21 provides a good intuition for induction, coinduction, and recursive types Oct 28, 2013 at 2:46
• Thank you! This is really fascinating. I am currently reading TAPL, and I'm glad to hear this will be covered later in the book.
– beta
Oct 29, 2013 at 8:21
• @beta Yep, TAPL and it's big brother, Advanced Topics in Types and Programming Languages, are wonderful resources. Oct 29, 2013 at 17:33

In OCaml, you need to pass `-rectypes` as a parameter to the compiler (or enter `#rectypes;;` in the toplevel). Roughly speaking, this will turn off "occurs check" during unification. The situation `The type variable 'a occurs inside 'a -> 'b` will no longer be a problem. The type system will still be "correct" (sound, etc.), the infinite trees that arise as types are sometimes called "rational trees". The type system gets weaker, i.e. it becomes impossible to detect some programmer errors.

See my lecture on lambda-calculus (starting at slide 27) for more information on fixpoint operators with examples in OCaml.