Recursion in Haskell and LC

When we speak of recursion for Haskell, we can define fix point like this:

Prelude> let fix f = f (fix f)
Prelude> :t fix
fix :: (t -> t) -> t

We can see from its type that it is well defined, i.e. the argument should be a function that takes a t and returns a t.

So now consider we have factorial defined as:
Prelude> let fact n = if n == 0 then 1 else n * fact(n-1)

So we can use it like:
Prelude> (fix (\x -> fact)) 4

This is great!

So, regarding lambda calculus, recursion is defined as:
Y := λg.(λx.g (x x)) (λx.g (x x))

But, if we tried to do that in Haskell, we’d get something like:

Prelude> \g -> (\x -> g (x x)) (\x -> g (x x))
    Occurs check: cannot construct the infinite type: t1 = t1 -> t0
    In the first argument of `x', namely `x'
    In the first argument of `g', namely `(x x)'
    In the expression: g (x x)

So this is Haskell warning us about infinite types. And why does that recursion definition work with lambda calculus?

Well, the reason is that lambda calculus is untyped (unless we are talking about typed lambda calculus, which we aren’t :-)), and Haskell is typed.

So in the world of typed languages, that lambda expression is not possible.
Consider x :: a -> a for some choice of a. To apply x to something, that something must have type a. So, to apply to x, x :: a. But that means a == a->a.

But hey, we still have fixed point combinators!


Leave a Reply

Fill in your details below or click an icon to log in: Logo

You are commenting using your account. Log Out / Change )

Twitter picture

You are commenting using your Twitter account. Log Out / Change )

Facebook photo

You are commenting using your Facebook account. Log Out / Change )

Google+ photo

You are commenting using your Google+ account. Log Out / Change )

Connecting to %s