Fix and recursion (Solutions) Wider Theory edit this chapter

The `fix` function is a particularly weird-looking function when you first see it. However, it is useful for one main theoretical reason: introducing it into the (typed) lambda calculus as a primitive allows you to define recursive functions.

Introducing `fix`

Let's have the definition of `fix` before we go any further:

```fix :: (a -> a) -> a
fix f = let x = f x in x
```

This immediately seems quite magical. Surely `fix f` will yield an infinite application stream of `f`s: `f (f (f (... )))`? The resolution to this is our good friend, lazy evaluation. Essentially, this sequence of applications of `f` will converge to a value if (and only if) `f` is a lazy function. Let's see some examples:

Example: `fix` examples

```Prelude> :m Control.Monad.Fix
*** Exception: stack overflow
"hello"
[1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,...
```

We first import the `Control.Monad.Fix` module to bring `fix` into scope (this is also available in the `Data.Function`). Then we try some examples. Since the definition of `fix` is so simple, let's expand our examples to explain what happens:

```  fix (2+)
= 2 + (fix (2+))
= 2 + (2 + fix (2+))
= 4 + (fix (2+))
= 4 + (2 + fix (2+))
= 6 + fix (2+)
= ...
```

It's clear that this will never converge to any value. Let's expand the next example:

```  fix (const "hello")
= const "hello" (fix (const "hello"))
= "hello"
```

This is quite different: we can see after one expansion of the definition of `fix` that because `const` ignores its second argument, the evaluation concludes. The evaluation for the last example is a little different, but we can proceed similarly:

```  fix (1:)
= 1 : fix (1:)
= 1 : (1 : fix (1:))
= 1 : (1 : (1 : fix (1:)))
```

Although this similarly looks like it'll never converge to a value, keep in mind that when you type `fix (1:)` into GHCi, what it's really doing is applying `show` to that. So we should look at how `show (fix (1:))` evaluates (for simplicity, we'll pretend `show` on lists doesn't put commas between items):

```  show (fix (1:))
= "[" ++ map show (fix (1:)) ++ "]"
= "[" ++ map show (1 : fix (1:)) ++ "]"
= "[" ++ "1" ++ map show (fix (1:)) ++ "]"
= "[" ++ "1" ++ "1" ++ map show (fix (1:)) ++ "]"
```

So although the `map show (fix (1:))` will never terminate, it does produce output: GHCi can print the beginning of the string, `"[" ++ "1" ++ "1"`, and continue to print more as `map show (fix (1:))` produces more. This is lazy evaluation at work: the printing function doesn't need to consume its entire input string before beginning to print, it does so as soon as it can start.

Exercises

What, if anything, will the following expressions converge to?

• `fix ("hello"++)`
• `fix (\x -> cycle (1:x))`
• `fix reverse`
• `fix id`
• `fix (\x -> take 2 \$ cycle (1:x))`

`fix` and fixed points

A fixed point of a function `f` is a value `a` such that `f a == a`. For example, `0` is a fixed point of the function `(* 3)` since `0 * 3 == 0`. This is where the name of `fix` comes from: it finds the least-defined fixed point of a function. (We'll come to what "least defined" means in a minute.) Notice that for both of our examples above that converge, this is readily seen:

```const "hello" "hello" -> "hello"
(1:) [1,1,..]         -> [1,1,...]
```

And since there's no number `x` such that `2+x == x`, it also makes sense that `fix (2+)` diverges.

Exercises
For each of the functions `f` in the above exercises for which you decided that `fix f` converges, verify that `fix f` finds a fixed point.

In fact, it's obvious from the definition of `fix` that it finds a fixed point. All we need to do is write the equation for `fix` the other way around:

```f (fix f) = fix f
```

Which is precisely the definition of a fixed point! So it seems that `fix` should always find a fixed point. But sometimes `fix` seems to fail at this, as sometimes it diverges. We can repair this property, however, if we bring in some denotational semantics. Every Haskell type actually includes a special value called bottom, written `⊥`. So the values with type, for example, `Int` include, in fact, `⊥` as well as `1, 2, 3` etc.. Divergent computations are denoted by a value of `⊥`, i.e., we have that `fix (2+) = ⊥`.

The special value `undefined` is also denoted by this `⊥`. Now we can understand how `fix` finds fixed points of functions like `(2+)`:

Example: Fixed points of `(2+)`

```Prelude> (2+) undefined
*** Exception: Prelude.undefined
```

So feeding `undefined` (i.e., `⊥`) to `(2+)` gives us `undefined` back. So `⊥` is a fixed point of `(2+)`!

In the case of `(2+)`, it is the only fixed point. However, there are other functions `f` with several fixed points for which `fix f` still diverges: `fix (*3)` diverges, but we remarked above that `0` is a fixed point of that function. This is where the "least-defined" clause comes in. Types in Haskell have a partial order on them called definedness. In any type, `⊥` is the least-defined value (hence the name "bottom"). For simple types like `Int`, the only pairs in the partial order are `⊥ ≤ 1`, `⊥ ≤ 2` and so on. We do not have `m ≤ n` for any non-bottom `Int`s `m`, `n`. Similar comments apply to other simple types like `Bool` and `()`. For "layered" values such as lists or `Maybe`, the picture is more complicated, and we refer to the chapter on denotational semantics.

So since `⊥` is the least-defined value for all types and `fix` finds the least-defined fixed point, if `f ⊥ = ⊥`, we will have `fix f = ⊥` (and the converse is also true). If you've read the denotational semantics article, you will recognise this as the criterion for a strict function: `fix f` diverges if and only if `f` is strict.

Recursion

If you've come across examples of `fix` on the internet, or on the #haskell IRC channel, the chances are that you've seen examples involving `fix` and recursion. Here's a classic example:

Example: Encoding recursion with `fix`

```Prelude> let fact n = if n == 0 then 1 else n * fact (n-1) in fact 5
120
Prelude> fix (\rec n -> if n == 0 then 1 else n * rec (n-1)) 5
120
```

Here we have used `fix` to "encode" the factorial function: note that (if we regard `fix` as a language primitive) our second definition of `fact` doesn't involve recursion at all. In a language like the typed lambda calculus that doesn't feature recursion, we can introduce `fix` in to write recursive functions in this way. Here are some more examples:

Example: More `fix` examples

```Prelude> fix (\rec f l -> if null l then [] else f (head l) : rec f (tail l)) (+1) [1..3]
[2,3,4]
Prelude> map (fix (\rec n -> if n == 1 || n == 2 then 1 else rec (n-1) + rec (n-2))) [1..10]
[1,1,2,3,5,8,13,21,34,55]
```

So how does this work? Let's first approach it from a denotational point of view with our `fact` function. For brevity let's define:

```fact' rec n = if n == 0 then 1 else n * rec (n-1)
```

So that we're computing `fix fact' 5`. `fix` will find a fixed point of `fact'`, i.e. the function `f` such that `f == fact' f`. But let's expand what this means:

```f = fact' f
= \n -> if n == 0 then 1 else n * f (n-1)
```

All we did was substitute `rec` for `f` in the definition of `fact'`. But this looks exactly like a recursive definition of a factorial function! `fix` feeds `fact'` itself as its first parameter in order to create a recursive function out of a higher-order function.

We can also consider things from a more operational point of view. Let's actually expand the definition of `fix fact'`:

```  fix fact'
= fact' (fix fact')
= (\rec n -> if n == 0 then 1 else n * rec (n-1)) (fix fact')
= \n -> if n == 0 then 1 else n * fix fact' (n-1)
= \n -> if n == 0 then 1 else n * fact' (fix fact') (n-1)
= \n -> if n == 0 then 1
else n * (\rec n' -> if n' == 0 then 1 else n' * rec (n'-1)) (fix fact') (n-1)
= \n -> if n == 0 then 1
else n * (if n-1 == 0 then 1 else (n-1) * fix fact' (n-2))
= \n -> if n == 0 then 1
else n * (if n-1 == 0 then 1
else (n-1) * (if n-2 == 0 then 1
else (n-2) * fix fact' (n-3)))
= ...
```

Notice that the use of `fix` allows us to keep "unravelling" the definition of `fact'`: every time we hit the `else` clause, we product another copy of `fact'` via the evaluation rule `fix fact' = fact' (fix fact')`, which functions as the next call in the recursion chain. Eventually we hit the `then` clause and bottom out of this chain.

Exercises
1. Expand the other two examples we gave above in this sense. You may need a lot of paper for the Fibonacci example!
2. Write non-recursive versions of `filter` and `foldr`.

The typed lambda calculus

In this section we'll expand upon a point mentioned a few times in the previous section: how `fix` allows us to encode recursion in the typed lambda calculus. It presumes you've already met the typed lambda calculus. Recall that in the lambda calculus, there is no `let` clause or top-level bindings. Every program is a simple tree of lambda abstractions, applications and literals. Let's say we want to write a `fact` function. Assuming we have a type called `Nat` for the natural numbers, we'd start out something like the following:

```λn:Nat. if iszero n then 1 else n * <blank> (n-1)
```

The problem is, how do we fill in the `<blank>`? We don't have a name for our function, so we can't call it recursively. The only way to bind names to terms is to use a lambda abstraction, so let's give that a go:

```(λf:Nat→Nat. λn:Nat. if iszero n then 1 else n * f (n-1))
(λm:Nat. if iszero m then 1 else m * <blank> (m-1))
```

This expands to:

```λn:Nat. if iszero n then 1
else n * (if iszero n-1 then 1 else (n-1) * <blank> (n-2))
```

We still have a `<blank>`. We could try to add one more layer in:

```(λf:Nat→Nat. λn:Nat. if iszero n then 1 else n * f (n-1)
((λg:Nat→Nat. λm:Nat. if iszero n' then 1 else n' * g (m-1))
(λp:Nat. if iszero p then 1 else p * <blank> (p-1))))

->

λn:Nat. if iszero n then 1
else n * (if iszero n-1 then 1
else (n-1) * (if iszero n-2 then 1 else (n-2) * <blank> (n-3)))
```

It's pretty clear we're never going to be able to get rid of this `<blank>`, no matter how many levels of naming we add in. Never, that is, unless we use `fix`, which, in essence, provides an object from which we can always unravel one more layer of recursion and still have what we started off:

```fix (λf:Nat→Nat. λn:Nat. if iszero n then 1 else n * f (n-1))
```

This is a perfect factorial function in the typed lambda calculus plus `fix`.

`fix` is actually slightly more interesting than that in the context of the typed lambda calculus: if we introduce it into the language, then every type becomes inhabited, because given some concrete type `T`, the following expression has type `T`:

```fix (λx:T. x)
```

This, in Haskell-speak, is `fix id`, which is denotationally `⊥`. So we see that as soon as we introduce `fix` to the typed lambda calculus, the property that every well-typed term reduces to a value is lost.

Fix as a data type

It is also possible to make a fix data type in Haskell.

There are three ways of defining it.

```newtype Fix f=Fix (f (Fix f))
```

or using the RankNTypes extension

```newtype Mu f=Mu (forall a.(f a->a)->a)
data Nu f=forall a.Nu a (a->f a)
```

Mu and Nu help generalize folds, unfolds and refolds.

```fold :: (f a -> a) -> Mu f -> a
fold g (Mu f)=f g
unfold :: (a -> f a) -> a -> Nu f
unfold f x=Nu x f
refold :: (a -> f a) -> (g a-> a) -> Mu f -> Nu g
refold f g=unfold g . fold f
```

Mu and Nu are restricted versions of Fix. Mu is used for making inductive noninfinite data and Nu is used for making coinductive infinite data. Eg)

```newpoint Stream a=Stream (Nu ((,) a)) -- forsome b. (b,b->(a,b))
newpoint Void a=Void (Mu ((,) a)) -- forall b.((a,b)->b)->b
```

Unlike the fix point function the fix point types do not lead to bottom. In the following code Bot is perfectly defined. It is equivalent to the unit type ().

```newtype Id a=Id a
newtype Bot=Bot (Fix Id) -- equals          newtype Bot=Bot Bot
-- There is only one allowable term. Bot \$ Bot \$ Bot \$ Bot ..,
```

The Fix data type cannot model all forms of recursion. Take for instance this nonregular data type.

```data Node a=Two a a|Three a a a
data FingerTree a=U a|Up (FingerTree (Node a))
```

It is not easy to implement this using Fix.

 Fix and recursion Solutions to exercises Wider Theory Denotational semantics  >> Equational reasoning  >> Program derivation  >> Category theory  >> The Curry–Howard isomorphism  >> fix and recursion edit this chapter Haskell edit book structure