Type checking and recursive types (Writing the Y combinator in Haskell/Ocaml)
- by beta
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 [1]:
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.
[1] http://rosettacode.org/wiki/Y_combinator#Haskell
