Recursion

For a function to be recursive, it has to "know it's own name". i.e. the definition of a function must be known to itself.

Dynamically Scoped Recursion

This works fine with dynamically scoped recursion. This is because all variables are added to the global environment and the function is able to recall its own definition.

Statically Scoped Recursion

This has to be done differently depending on if immediate or deferred substitution is used.

If immediate substitution is used, then the Omega Combinator and the Y-Combinator must be used to create recursive functions.

Warning

This method does not allow for functions to be typed. This is because an infinitely long type must be created to account for all the function calls of the Y-combinator.

If deferred substitution is used, the definition of a function can be put into the closure's environment. But again the closure will become too large.

Fix Point Operator

Instead we use fix a fixed point operator

When evaluated, fix will substitute its function argument into itself before evaluation

bind f = (lambda g in 
            (lambda x in 
                if x = 0 then 1 else x * (g (x-1)))) in
((fix f) 2) -- Replace g in the body of f with (fix f), then evaluate

Extending FBAE

eval e (Fix f) = do { (ClosureV g b e') <- eval e f;
                      eval e' (subst g (Fix (Lambda g b)) b)
                     }

The type of fix has the same domain and range as the function applied to fix. This means the type of fix when running the type checker is just the range.

Definitions

Omega Combinator

This is the most basic combinator in lambda calculus it spawns copies of itself by passing a copy or reference to itself as a parameter.

bind o = lambda x in (x x) in
    (o o)

Y-Combinator

This allows for

Recursion without a function name
Recursion in static scoping

bind Y = (lambda f in (lambda x in f (x x))
                      (lambda x in f (x x))))
in (Y F)

f is the function being called recursively
F is the function we're applying recursively

Note

F is not an identifier

F = (lambda g in (lambda z in if z=0 then z else z + (g (z-1))))

bind F = (lambda g in (lambda z in if z=0 then z else z + (g (z-1)))) in 
    bind Y = (lambda f (lambda x in F (x x))
                       (lambda x in F (x x))))
    in (Y F)

Typing Functions

Type checking finds errors all at once as opposed to runtime error checking which finds errors as they occur and only once.

i.e. type checking is symbolic evaluation.

Traditional type checking gives a variable a type

Type derivation calculates the type of an expression.

Type checking and evaluation occurs at two different times. Thus we can't know what the input to a lambda will evaluate to.

The type of a function is similar to a "promise". i.e. If you feed a function a specific type, it will give some other type back.

T->T

homogenous function??

where

T ::= TNum | TBool | T -> T

Note

This is a recursive defition. It essentially means there are an infinite number of types that can be created, but each of those types have to be finite.

If every operation you perform will reduce the size of a finite type to 1, which is just a value.

D->R

D: domain type
R: range type

Quote

"Function types are theorems, functions are proofs" - P. Alexander

Finding D and R

$τ$ = [] derives bind x=1 in x+1 is of some type TNum

$τ$ is a list of identifiers and their types in scope. This is called the context.
TNum is the type of the body of the bind, and what the bind returns.
G |- t:T is a read "gamma derives that t is of type T" and is called a type judgement

Haskell

typeof c (Lambda x d t) = do { r <- typeof (x,d):c t;
                               return (d:->:r)
                              }