Type checking and recursive types (Writing the Y combinator in Haskell/Ocaml)
Posted
by
beta
on Programmers
See other posts from Programmers
or by beta
Published on 2013-10-27T20:43:44Z
Indexed on
2013/10/27
22:00 UTC
Read the original article
Hit count: 355
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.
© Programmers or respective owner