Blog

Having established that the type of a `lambda`

is of the form
`D:->:R`

, typing an increment function is quite simple:

```
typeofM cont (lambda (x:TNum) in x + 1)
== TNum -> TNum
```

It follows directly that a `lambda`

taking another `lambda`

and
applying it to a value is similarly typed:

```
typeofM cont (lambda (f:Num -> Num) in (lambda (x:Num) in (f x)))
== (TNum -> TNum) -> TNum
```

The first argument to the expression is the `lambda`

to be applied
while the second is the number applied. It is thus quite natural to
have `lambda`

expressions passed to other `lambda`

expressions as
arguments. The application in the body of the `lambda`

applies the function
argument to a value. We have seen this before. Specifically, when we
looked at untyped recursion and the $\Omega$ and `Y`

.

Remember $\Omega$, a simple recursive function that does not terminate:

```
((lambda x in (x x)) (lambda x in (x x)))
```

Let’s add a type placeholder, call it `T->T`

, to the `lambda`

and
determine what a typed version of the $\Omega$ would look like:

```
((lambda (x:T->T) in (x x))(lambda (x:T->T) in (x x)))
```

Will this work? Remember that to determine the type of an `f a`

we find the type of `f`

. First, `f`

must be a function type. Then if `a`

has the same type as the domain of `f`

, `f a`

has the same type as
the range of `f`

.

Unfortunately, we will never find a type for `x x`

because the type of `x`

must be the domain type of `x`

. This is a problem. If
`x`

has type `T->T`

, then for `x x`

to have type `T`

, `x`

must
also have type `T`

. This will never work as `x`

would need to have
both type `T`

and `T->T`

. `T = T->T`

, something that is not possible in our type system and would break the datatype representation if it were.

What this means is $\Omega$ cannot have a type. By the same argument, `Y`

cannot have a type and neither can be written in our new language that includes function types. Worse yet, *no recursive function* can be directly written in our language with function types.

*Normalization* is a term used to talk about termination. We say that
a *normal form* is a term in a language that cannot be reduced by
evaluation. In our languages terms like `1`

, `true`

and ```
lambda x in
x + 1
```

are normal forms because `evalM`

simply returns their values
without reduction. We also define these normal forms to be *values*
representing acceptable evaluation results.

In all the languages we have written so far, values and
normal forms are the same. What if we removed the evaluation case for
`+`

implying that `1+1`

would not evaluate further? Now terms
involving `+`

join values as normal forms. Unlike values, `+`

terms
should reduce and not be treated as values. Normal forms that are not values are referred to as *stuck* values and represent errors in a language definition. It is always desirable to show that the only normal forms in a language are values.

Normalization is the property that evaluating any term in a language always terminates resulting in a value. No non-termination and no stuck terms. Evaluation always halts with a value.

As it turns out, normalization and typing are strongly related. In our latest language, function types ensure termination. We saw this when failing to find a type for $\Omega$, let’s generalize it to all function applications. Look at the types involved in this simple evaluation:

```
((lambda (x:TNum) in x+1) 3)
```

The type of the `lambda`

is `TNum -> TNum`

because the type of `x`

is `TNum`

and the type of `x+1`

assuming `x:TNum`

is also `TNum`

. The type of `3`

is `TNum`

. The type of the application is therefore `TNum`

- the domain of `TNum -> TNum`

that is smaller than the function type.

The type resulting from the application is always smaller than the type of `lambda`

. This is true because of the way application types are defined.
Specifically, given `f:D->R`

and `(f d)`

where `d:D`

, the result
will always be `R`

. The base types for numbers and booleans are the
smallest possible types. Like number and Boolean values, there is no
way to reduce them - they are the base cases for types. Thus, application
aways makes a type smaller and eventually will get to a base type.
Like subtracting 1 repeatedly from a number will eventually
result in 0. Given that’s the case, if we do repeatedly execute we
will always get to that smallest type which is always associated with
a value.

There are ins and outs to this normalization property. It is great to know that programs terminate in many cases. But it is not great to need to know how many times any iterative construct executes when writing programs. Furthermore, there are many programs we do not want to terminate. Think about operating systems or controllers as two examples. Clearly languages with function types allow this, we just need to figure out how.

Lets revisit our original problem by going back and revisiting factorial:

```
bind fact = (lambda x in (if (isZero x) then 1 else x * (fact x-1)))
```

If this is dynamically scoped it executes recursively just fine. But
when static scoping and types come into play, things go downhill fast.
Here is a basic definition of `fact`

that will not execute if
statically scoped:

```
bind fact = (lambda (x:TNum) in (if (isZero x) then 1 else x * (fact x-1)))
```

Because `fact`

is not in scope, technically there is also no type for this
expression. If we can get `fact`

in scope, maybe this will
work. We need `fact`

to be in its closure’s environment. That’s a fancy way of saying `fact`

needs to know about itself. Let’s look at the
closure resulting from evaluating the `lambda`

defining `fact`

:

```
(ClosureV "x" TNum (if (isZero x) then 1 else x * (fact x-1)) [])
```

Let’s see if it works by applying the closure to 0:

```
((ClosureV "x" TNum (if (isZero x) then 1 else x * (fact x-1)) []) 0) []
== (if (isZero 0) then 1 else x * (fact x-1)) []
== 1
```

Remember that when we execute an application, the environment from the
closure replaces the local environment. That environment here is
empty, thus the recursive reference to `fact`

is not in the closure’s
environment. `fact 0`

works only because the recursive call to
`fact`

never occurs. `fact 0`

is the base case and its value can be
calculated directly. Still can’t find a type for `fact`

, but we’ll
worry about that later.

Unfortunately, any value other that `0`

triggers the recursive call
where `fact`

must be found in the environment. Looking at `fact 1`

demonstrates the problem immediately:

```
((ClosureV "x" TNum (if (isZero x) then 1 else x * (fact x-1)) []) 1) env
== evalM (if (isZero 1) then 1 else 1 * (fact 0)) []
== 1 * (fact 0) []
== error on lookup of fact in []
```

The actual value of `env`

is immaterial here because we’re using
static scoping. The empty environment in the closure is where we look
for the definition of `fact`

.

The easiest fix is to simply add `fact`

to its closure’s environment.
We know the definition of `fact`

when it is defined, so we can simply
add it to it’s own closure. That should do the trick because the
lookup of `fact`

will find it. Let’s give it a try:

```
(ClosureV "x" TNum (if x=0 then 1 else x * (fact x-1))
[(fact,(ClosureV "x" TNum (if ...) []))])
```

There are two closures here. The outer closure is what we will
evaluate during the initial application and the inner closure defines the value of `fact`

in the outer closure’s environment. Now `fact`

will work for `0`

as it did before and should work for other values as well. Let’s give it
a shot for `1`

:

```
((ClosureV "x" TNum (if (isZero x) then 1 else x * (fact x-1))
[(fact,(ClosureV "x" TNum (if ...) []))]) 1) env
== (if (isZero x) then 1 else x * (fact x-1) [(x,1),(fact,(ClosureV "x" TNum (if ...) []))]
== (if (isZero 1) then 1 else 1 * (fact 0)) [(x,1),(fact,(ClosureV "x" TNum (if ...) []))]
== evalM 1 * (fact 0) [(x,1),(fact,(ClosureV "x" TNum (if ...) []))]
== 1 * ((lambda x in (if (isZero x) then 1 else x * (fact x-1)) []) 0)
[(fact,(ClosureV "x" TNum (if ...) []))]
== 1 * (if (isZero x) then 1 else x * (fact x-1)) [(x,0)]
== 1 * 1
```

Good for now, but look at the last application where `fact`

is no longer in
the environment. What happened? The environment of the *inner*
closure becomes the new environment when it is applied. This means
`fact 2`

will fail when the `if`

evaluates and tries to apply
fact. We have a fix for that! Let’s just add the closure again - add
the closure to the environment of the closure in the closures’
environment: (Say that fast 5 times)

```
(ClosureV "x" (if x=0 then 1 else x * (fact x-1))
[(fact,(ClosureV "x" (if ...)
[(fact,(ClosureV "x" (if ...) [(x,??)])),(x,??)])
```

Bingo. Now the closure in the environment for the closure knows about
the closure. Now we can call `fact`

on 0, 1, and 2. But not 3. Do
you see why?

The innermost closure can never have `fact`

in its
environment because it is, in effect, the base case. Any number of
nested closures you choose can always be exceeded by 1. Build 10 and
`fact`

will fail for 11, build 100 and it fails for 101 and so forth.
No matter how deep the nesting, eventually the recurse call to `fact`

fails. We cannot pre-seed a closure’s environment to contain copies of itself.

In the immortal words of Dr. Seuss, “it’s turtles all the way down”. No matter how many turtles we add there is always one at the bottom we can try to jump under. We cannot write $\Omega$ this way nor can we write Y. We cannot use closure magic. The only option left is adding a new construct to our language with a different execution behavior.

The fix is adding a *fixed point* operator with concrete syntax ```
fix
t
```

, to our statically scoped language. Instead of using the language
to write a fixed point construct like Y, we will build the fixed point
into the language directly and take advantage of controlling
evaluation more precisely.

The inference rule defining the general recursive fixed point structure is:

\[\frac{[g\mapsto (\ffix (\llambda g\; b))]\; b \eval v}{\ffix \llambda g\; b \eval v}\]Evaluating `fix`

uses substitution to replace the function associated with recursion with `fix`

over that same function.

First note that $g$ is *not* the argument to the factorial function. $g$ is
the function that is called in the recursive case. Evaluating `fix`

does not perform one step of the recursion, but instead sets up what
will replace the recursive call. `fix`

is not recursive.

```
evalM env (Fix f) = do { (ClosureV i b e) <- (evalM env f) ;
evalM e (subst i (Fix (Lambda i b)) b) }
```

To better understand how the `fix`

operation works, let’s evaluate
factorial of `3`

using our new operation. First, let’s define `fact`

,
the function we will use to implement factorial:

```
bind fact = (lambda g in
(lambda x in
(if x=0 then 1 else x * (g x-1)))) in ...
```

`fact`

is no longer recursive. It takes a parameter that will be
the function that it will call in the recursive case. When given that
paraneter, `fact`

returns something that looks a great deal like
factorial. Let’s do a quick thought experiment to see what `fact`

would look like if it were called on itself:

```
((lambda g in (lambda x in (if x=0 then 1 else x * (g x-1)))) fact)
== (lambda x in (if x=0 then 1 else x * (fact x-1))))
```

That looks exactly like what we want, but it won’t work until we use
`fix`

to perform the instantiation of `fact`

. After evaluating `fact`

and pulling the resulting closure apart, we have the following
definitions that get used in the evaluation:

```
i = g
b = (lambda x in (if x=0 then 1 else x * (g x-1))
e = []
```

The parameter defined by the `fact`

`lambda`

expression is `g`

. Thus,
the argument name in the closure is `g`

. The body of the `fact`

`lambda`

is what we think of as factorial with the recursive call
replaced by a call to `g`

. The environment is empty because there is
nothing defined when we defined the `fact`

`lambda`

. Let’s start the
evaluation by applying the fixed point of `fact`

to `3`

:

```
((fix fact) 3)
```

Note that we are not applying `fact`

to `3`

, but instead applying the
fixed point of `fact`

to `3`

. To
evaluate the application we evaluate `(fix fact)`

and apply the
resulting value to `3`

. Let’s evaluate `(fix fact)`

using the
definition from above by replacing `g`

with `(fix (lambda g in b)):

```
== [g->(fix (lambda g in b))]b 3
== (lambda x in (if x=0 then 1 else x * ((fix (lambda g in b)) x-1) 3
```

Now we have something we understand. Specifically, application of a
`lambda`

to the term, `3`

. Substituting `3`

for x results in:

```
== if 3 = 0 then 1 else 3 * ((fix (lambda g in b)) 3-1)
== 3 * ((fix (lambda g in b)) 2)
```

We got exactly what we want! We started by applying the fixed point of the lambda to a value and we just got the same thing here. Exactly the same thing with the argument decremented by 1. Let’s keep going by applying the same steps again:

```
== 3 * [g->(fix (lambda g b))] b 2
== 3 * (lambda x in (if x=0 then 1 else x * ((fix (lambda g in b)) x-1) 2
== 3 * if 2 = 0 then 1 else 2 * ((fix (lambda g in b)) 2-1)
== 3 * 2 * ((fix (lambda g in b)) 1)
```

We are recursively executing just like we hoped we would. Now we just need to worrying about termination. Same steps again:

```
== 3 * 2 * ([g->(fix (lambda g b))] b 1)
== 3 * 2 * ((lambda x in (if x=0 then 1 else x * ((fix (lambda g in b)) x-1) 1)
== 3 * 2 * (if 1=0 then 1 else 1 * ((fix (lambda g in b)) 1-1))))
== 3 * 2 * 1 * ((fix (lambda g in b)) 0)
```

… and again:

```
== 3 * 2 * 1 * ((fix (lambda g in b)) 0)
== 3 * 2 * 1 * ([g->(fix (lambda g b))] b 0)
== 3 * 2 * 1 * ((lambda x in (if x=0 then 1 else x * ((fix (lambda g in b)) x-1) 0)
== 3 * 2 * 1 * if 0=0 then 1 else 0 * ((fix (lambda g in b)) -1)
```

This time the `if`

condition is true, so the function returns `1`

rather than evaluating the fixed point again. The result is exactly
what we would expect:

```
== 3 * 2 * 1 * 1
== 6
```

Finally evaluating the resulting product gives us `6`

as anticipated.
Our newly added `fix`

operation takes a properly formed function and
creates a recursive function. Let’s look back at the `fact`

function
given to `fix`

:

```
bind fact = (lambda g in (lambda x in (if x=0 then 1 else x * (g x-1)))) in
((fix fact) 3)
```

This looks exactly like our original `fact`

definition with a “hole”
for the recursive call. Where `fact`

appears in the initial
definition, the function `g`

from the outer `lambda`

appears. This is
the general form for any recursive construction we would like to
create. Specifically, create the recursive function and replace the
recursive instance with a variable created by an outer `lambda`

. This
will give you the value for the `g`

parameter in the fixpoint.

This entire discussion started with an attempt to create a statically
scoped, well-typed recursive construction. We could not find a type
for $\Omega$ or Y, we couldn’t hack closures, and finally resorted to
extending the core language to include a `fix`

operator. We now have
a statically scoped `fix`

expression that will create recursive
constructs for us.

What now is the type of `fix`

? Looking at how we created factorial from `fact`

gives is a great clue:

```
bind fact = (lambda g in (lambda x in (if x=0 then 1 else x * (g x-1)))) in
((fix fact) 3)
```

`fix fact`

gives us the actual factorial fucntion. The previous definition
could be rewritten as:

```
bind fact = (lambda g in (lambda x in (if x=0 then 1 else x * (g x-1)))) in
bind factorial = (fix fact) in
(factorial 3)
```

Looking at factorial this way, it should be clear the type of
`factorial`

must be `TNat->TNat`

. Given a number, factorial will
return another number. What then is the type of `fact`

? It takes a
value `g`

and returns a function that calls `g`

. So, the first argument to
`fact`

must be a function. The result must also be a function because
it is applied to a value. `fact`

takes a function and returns a
function. If we call `typeofM`

on just `fact`

we learn:

```
typeofM [] (lambda (ie:Nat->Nat) in
(lambda (x:Nat) in
(if (isZero x) then x else x + (ie (x-1))))
== (TNat :->: TNat) -> (TNat :->: TNat)
```

`fix`

takes `fact`

and creates `factorial`

. Instead of applying `fix`

to an argument like application, `fix`

skips the argument and environment
going straight to the substitution. Given a function like `fact`

,
`fix`

creates a recursive function from the body of `fact`

using the
function itself. Just like an application, the type of `fix`

is the range
of the input function:

The code for typing `fix`

follows directly from the inference rule:

```
typeofM cont (Fix t) = do { (d :->: r) <- typeofM cont t ;
return r }
```

Now we have a type for `fix`

. The factorial function defined using fix also has a type. The `lambda`

used to create factorial has the type:

```
(TNat :->: TNat) :->: (TNat :->: TNat)
```

Thus the type of `(fix fact)`

is the domain of `fact`

, or just `TNat :->: TNat`

. Exactly the type we expect for our factorial function.