At first glance, the `fix` function may appear odd and useless . However, there is a theoretical reason for its existence: introducing it into the (typed) lambda calculus as a primitive allows you to define recursive functions.

## Introducing `fix`

`fix` is simply defined as:

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

Doesn't that seem ... magical? You might be wondering: surely `fix f` will cause an infinite series of nested applications of `f`s: `x = f x = f (f x) = f (f (f ( ... )))`? The resolution here is lazy evaluation. Essentially, this infinite sequence of applications of `f` will be avoided if (and only if) `f` is a lazy function. Let's see some examples:

Example: `fix` examples

```Prelude> :m Control.Monad.Fix
Prelude Control.Monad.Fix> fix (2+)  -- Example 1
*** Exception: stack overflow
Prelude Control.Monad.Fix> fix (const "hello")  -- Example 2
"hello"
Prelude Control.Monad.Fix> fix (1:)  -- Example 3
[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` (which is also exported by the `Data.Function` module) into scope. Then we try three examples. Let us try to see what actually examples in the first example:

```  -- fix f = let {x = f x} in x
fix (2+)
= let {x = 2 + x} in x
= let {x = 2 + x} in 2 + x
= let {x = 2 + x} in 2 + (2 + x)
= let {x = 2 + x} in 2 + (2 + (2 + x))
= let {x = 2 + x} in 2 + (2 + (2 + (2 + x)))
= ...
```

The first example uses `(+)` which is an eager function; it needs the value of `x` before it can compute ... the value of `x`. Therefore this calculation will never stop. Let us now look at the second example:

```  fix (const "hello")
= let {x = const "hello" x} in x
= "hello"
```

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

```  fix (1:)
= let {x = 1 : x} in x
= let {x = 1 : x} in 1 : x
```

Here `1 : x` is already in weak head normal form (`(:)` is a lazy data constructor), so the expansion stops. This actually creates a cyclic structure. Each time new element of this list is requested by a consumer function, `x`'s definition is consulted, and it is already known to be `1 : x`.

Thus, requesting elements from this list one by one will return `1`s one after another while requested, without limit. So `take 10 (fix (1:))` will produce a list of ten `1`s, but trying to print them all by typing `fix (1:)` into GHCi causes the infinite stream of `1`s to be printed.

Well actually it causes the evaluation of `show (fix (1:)) = "[" ++ intercalate "," (map show (fix (1:))) ++ "]"`, and although the `map show (fix (1:))` will never terminate, it does produce its output incrementally, piece by piece, one `"1"` at a time:

```  "[" ++ intercalate "," (map show (fix (1:))) ++ "]"
= "[" ++ intercalate "," (map show (let {x = 1 : x} in x)) ++ "]"
= "[" ++ intercalate "," (map show (let {x = 1 : x} in 1 : x)) ++ "]"
= "[" ++ "1" ++ "," ++ intercalate "," (map show (let {x = 1 : x} in x)) ++ "]"
= "[1," ++ intercalate "," (map show (let {x = 1 : x} in 1 : x)) ++ "]"
= "[1," ++ "1" ++ "," ++ intercalate "," (map show (let {x = 1 : x} in x)) ++ "]"
= "[1,1," ++ intercalate "," (map show (let {x = 1 : x} in 1 : x)) ++ "]"
= "[1,1," ++ "1" ++ "," ++ intercalate "," (map show (let {x = 1 : x} in x)) ++ "]"
= "[1,1,1," ++ intercalate "," (map show (let {x = 1 : x} in 1 : x)) ++ "]"
= ...
```

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.

Lastly, iteratively calculating an approximation of a square root of a number,

```  -- fix f = let {x = f x} in x
fix (\next guess tol val -> if abs(guess^2-val) < tol then guess else
next ((guess + val / guess) / 2.0) tol val) 2.0 0.0001 25.0
= (let {next = (\next guess tol val -> if abs(guess^2-val) < tol then guess else
next ((guess + val / guess) / 2.0) tol val) next}
in next) 2.0 0.0001 25.0
= let  {next guess tol val =  if abs(guess^2-val) < tol then guess else
next ((guess + val / guess) / 2.0) tol val}
in  next  2.0 0.0001 25.0
= 5.000000000016778
```
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.) For the two aforementioned examples 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 have already come across examples of `fix`, chances are they were 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)
```

This is the same function as in the first example above, except that we gave a name to the anonymous function so that we're computing `fix fact' 5` now. `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 m then 1 else m * 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)

```newtype Stream a = Stream (Nu ((,) a)) -- exists b . (b, b -> (a, b))
newtype 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.