(define (member? elem ls)
    (if (null? ls)
        #f
        (if (= elem (car ls))
            #t
           (member? elem (cdr ls)))))

We can use boolean operators in order to get a simpler and clearer definition. Boolean operators are very helpful to define predicates.

Notice: the boolean operators or and and of Scheme are actually operators that can take an arbitrary number of expressions as arguments. The arguments are evaluated in sequence.
and returns #f as soon as the evaluation of an argument returns #f.
or returns #t as soon as the evaluation of an argument returns #t.

(define (member? elem ls)
   (and (not (null? ls))
        (or (= elem (car ls))
            (member? elem (cdr ls))))))
 

Exercise: write functions to sort a list using the different sorting algorithms you know.

   Now let's consider another example of recursion on the length of a list: a function summing up all the numbers present in a list of numbers.

(define (Sumlist ls)
     (if (null? ls)
         0
         (+ (car ls) (Sumlist (cdr ls)))))

Intuition: How did we manage to program this function? Well, first we provided its result ( 0 ) in case the input be the basic element of the domain (the empty list). Then, by assuming that our program works correctly on lists that are "smaller" than the input, (Sumlist (cdr ls)), we "built" the result for the generic input ls: (+ (car ls) (Sumlist (cdr ls))).
We considered (cdr ls) to be "smaller" than ls.
But why do we have to use "smaller" inputs for the recursive calls?
In order to guarantee the computation eventually stops. In fact we cannot go on forever calling the function on smaller and smaller elements. Sooner or later we reach the emptylist, on which the function is correctly defined.
The problem is how we can be sure that it is not possible to have an infinite sequence of smaller and smaller elements.
For the present function there is no problem, since a "smaller" input consists in a shorter list, and it is impossible to have an infinite sequence of shorter and shorter lists.
But we shall see that it is not always so simple....

So, we need
(1) to provide the result for the simplest elements of the domain;
(2) to provide the result for all the other possible "shapes" of the input using the assumption that the program works correctly on "smaller" arguments than the input.;
(3) to be sure that there exists no infinite sequence of smaller and smaller elements

Point (3) above can be formally proved by using the notion of well-founded precedence relation.
We do not study such a notion in the present very introductory notes.

   Let us write a function that sums up the number in a list using the constraint that the first argument of an addition must always be 1 (it is a weird and inefficient way to sum up the elements of a list, but in our examples we do not care about efficiency, we simply wish to practice with recursion.)

(define (Sumlistweird ls)
     (cond ((null? ls) 0)
           ((= (car ls) 0) (Sumlistweird (cdr ls)))
           (else (+ 1 
	            (Sumlistweird (cons (- (car ls) 1) 
		                        (cdr ls)))))))

Intuition: In this case we provided the value for the simplest element and for all the possible shapes of the input different from the emptylist:
(in an informal notation)
Sumlistweird emptylist = 0
Sumlistweird (cons 0 (cdr ls)) = Sumlist (cdr ls)
Sumlistweird (cons n (cdr ls)) = 1 + (Sumlist (cons (- n 1) (cdr ls)))

We assumed that Sumlistweird works correctly on "smaller" elements than ls. But now we are considering both (cdr ls) and (cons (- n 1) (cdr ls)) to be smaller than ls! Notwithstanding (cons (- n 1) (cdr ls)) has the same lenght as ls!
Actually this is not a problem, we need only to be sure that, according to this particular notion of "being smaller" there is no infinite sequence of smaller and smaller lists. The notion of well-founded precedence relation could help us to get a formal proof of that.

Recursion on nested lists

In Scheme lists are not homogeneus, so we can have anything in a list, also other lists.

One-level nesting
Let us consider a function on lists of lists of numbers.
The following function returns the sum of all the numbers present in a list of lists of numbers. (We call lsls the argument, in order to recall that it is a list of lists (of numbers)).
Notice that in Scheme (caar exp) stands for (car (car exp)).
Moreover, (cdar exp) stands for (cdr (car exp), and so on.

(define (Sumlistlist lsls)
    (if (null? lsls)
        0
        (if (null? (car lsls))
            (Sumlistlist (cdr lsls))
            (+ (caar lsls) 
	       (Sumlistlist (cons (cdar lsls) 
	                           (cdr lsls)))))))

Useless to say that the above function could be defined far more easily by means of the functions Sumlist and map (do it as exercise).
But now we are not interested in the best ways to make sums, we are just playing with recursion in its various forms.

Now we write a "weird" version of Sumlistlist: a version where "+" can be used only with 1 as first argument.

(define (Sumlslsweird ls)
   (cond ((null? ls) 0)
         ((null? (car ls)) (Sumlslsweird (cdr ls)))
         ((= (caar ls) 0) (Sumlslsweird (cons (cdar ls) 
	                                      (cdr ls))))
         ( else (+ 1 
	        (Sumlslsweird (cons (cons (- (caar ls) 1) 
		                          (cdar ls)) 
                                    (cdr ls)))))))

This is an example of triple induction: on the length of the list, on the length of the first element and on the numerical value of the first number of the first element of the list.

Multiple levels of nesting
We consider now lists containing numerical elements or other lists at any level of nesting.

Let us define the function (actually a predicate) genmember?.
Such a function checks whether a number is in a list containing numbers at any level of nesting.

(define (genmember? elem ls)
    (if (null? ls)
         #f
        (if (list? (car ls))
            (or (genmember? elem (car ls))
                (genmember? elem (cdr ls)) )
            (or (eqv? elem (car ls))
                (genmember? elem (cdr ls))))))

    We write now a function that sums all the numbers present in the input (a list containing numerical elements or other lists at any level of nesting.)

(define (Gensumls llss)
    (if (null? llss)
        0
        (if (list? (car llss))
            (+ (Gensumls  (car llss))
               (Gensumls  (cdr llss)) )
            (+ (car llss) (Gensumls  (cdr llss))))))
 

Notice that the recursion is not on the level of nesting. In fact (cdr llss) could have the same level of nesting of llss.

   If somebody knows the game of the Hanoi towers, the program to solve it in the right way is the following.

(define (tower-of-hanoi n peg1 peg2 peg3)
   (if (= n 0)
       '()
       (append (tower-of-hanoi (- n 1) 
                               peg1 
			       peg3 
			       peg2)
               (cons (list peg1 peg3) 
                     (tower-of-hanoi (- n 1) 
		                     peg2 
				     peg1 
				     peg3)))))

In this definition of the tower the problem is defined by giving the number of disks and the name of the three pegs (that can be also be identified by a number); it is assumed that the first one is where all the disks are at the beginning. The third one is where the disks have to be moved to.

   Of course we can have recursion on all sort of inductively defined Data Types (trees for examples).

11.  Correctness proofs of functional programs

   A functional programming style has advantages that are common in any mathematical notation:

• There is consistency in the use of names: variables do not vary, they stand for a, perhaps not yet known, constant value throughout their scope.
• Thanks to the absence of side-effects, in FPLs the same expression always denotes the same value. This property is called referential transparency.

A definition like x = x + 1 would mean in an imperative language that x is incremented. In a functional language however this definition means that any occurrence of x can always be substituted by x + 1.
Clearly the initial expression x does not have a normal form: substitution will continue forever (some systems recognize such situations in certain simple cases and report an error message).

x → x+1 → (x+1)+1 → ...

Due to the referential transparency one is allowed to replace in any expression any occurrence of any left-hand side of a definition by its corresponding right-hand side and vice versa

Referential transparency makes it possible to use common mathematical techniques such as symbolic substitution and induction. With the help of these techniques a program can be transformed into a more efficient one or certain properties of a program, such as its correctness, can be proven.

The use of Induction principles for proving functional program properties

    Recursion is the basis of the computational and expressive power of functional programming languages. You can notice how its working principle is analogous to that used in mathematical proofs by induction.
In fact, in a recursive program the output is defined for the base elements and then, assuming the program correctly works for "simpler", "smaller" elements than the input, the output is defined for the generic input.
In a proof by mathematical induction the property is proven for the base case (usually 0) and then, assuming the property to hold for smaller numbers, we prove the property for the generic number.
Refresh your knowledge about proofs by mathematical induction.

You can notice that the principle of mathematical induction is a logical rule that sort of implicitely "expresses" also a model of calculation. It corresponds, in functional programming, to defining numerical functions by recursion like the following one:

 (define (fact n) 
     (if (= n 0) 
         1 
         (* n (fact (- n 1))))) 

the value of the function is given for n=0 and is calculated for n assuming that fact correctly works for n-1.

   The close correspondence betweeen recursive functions and the principles of induction, make it possible, for example, to use induction to formally prove properties of recursive programs.
It is natural to use the principle of mathematical induction if we wish to show that the factorial is total, i.e. that for all n (fact n) converges (i.e. that its evaluation eventually terminates)
We need:
1. to prove that (fact 0) converges
2. to prove that, for a generic k not equal to 0, (fact k) converges, using the inductive hypothesis that (fact (- k 1)) converges).

Let's consider the definition of factorial given above and let's prove the two points above:
1. if k=0 you evaluate the "then" part of the conditional, therefore the value of the expression that represents the factorial is 1, that is (fact 0) converges ;
2. if k >0 you evaluate the "else" part, hence the value of (fact k) is the value of the expression (* k (fact (- k 1))). Hence, by assuming that the evaluation of (fact (- k 1)) converges, the evaluation of whole expression (* k (fact (- k 1))) trivially converges.

   In order to prove properties of programs that works on more complex data structures thatn number, we need to use more powerful mathematical tools, for instance the principle of well-founded induction (that we do not treat here).

12.  Typed Languages

   The class of functional languages can be divided into two main groups: Strongly typed languages (usually referred to simply as typed languages) and Non strongly typed languages (usually referred to simply as untyped languages).
A type, in general, can be looked at as a partial specification of a program (a function) or of an expression. These partial specifications, according to the particular type system of the language considered, can be more or less detailed.

By means of types we can avoid errors like:

true + 3

in fact the interpreter knows that + takes a pair of numbers and returns a number, i.e. that its type is

+::  int x int → int

   A language is strongly typed whenever any function and any legal expression of the language has (or can be given) a type.

In (strongly) typed languages errors like the one shown above are detected by the Type Checker, before the program is "executed" (statically). In not (strongly) typed languages this sort of errors can be detected only at run-time, by the interpreter itself (the program's execution is stopped whenever an error is detected).

If a function in a typed language has a type int->bool, it means that the function (program) takes an integer as an argument and returns a boolean as result.

   Scheme is an untyped language. In fact, we could write the following legal function definition

(define (f x) ((if (fac (list x x)) 5 #t)))

(define (g x) ((if (> x 4) 5 #t)))

Typed languages, like Haskell, prevents us to write functions like f and g, since they realize statically, at the moment of their definition, that f and g cannot be typed.
Notice that this is a good thing for what concerns f, since in such a way the Type Checker prevents us to apply fac to a list.
For what concerns g, however, you can notice that even if the Type Checker cannot give a type to g, such a function is not "intrinsically" wrong. Its application does not cause any disaster, we simply do not know if the result would be a number or a boolean.

The above discussion shows that, on the one hand, typed languages prevents us to write functions, like f, that can cause some disaster during their application, and this is a good thing.
On the other hand they prevent us to write functions, like g, that are not intrinsically dangerous and that in same case could be useful.
In a nutshell: typed languages are safer, while untyped languages are more flexible. However, if I can choose between a typed and an untyped language... I prefer the first one!

13 The λ-calculus and computation theory

   The Lambda-calculus is the computational model the functional languages are based on.
It is a very simple mathematical formalism. In the theory of the λ-calculus one is enabled to formalize, study and investigate properties and notions common to all the functional languages, without being burdened by all the technicalities of actual languages, useless from a theoretical point of view.
In a sense, the λ-calculus it is a paradigmatic and extremely simple functional language.

The concepts the Lambda-calculus is based on are those that are fundamental in all functional programming languages:

variable         ( formalisable by   x, y ,z,…)
abstraction (anonymous function)    (formalisable by   λx.M   
                                                       where M is a term and x a variable)
application    (formalizable by  MN, where M and N are terms )

We have seen that these are indeed fundamental notions in functional programming. It seems, however, that there are other important notions: basic elements, basic operators and the possibility of giving names to expressions.
Even if it could appear very strange, this notions actually are not really fundamental ones: they can be derived from the first ones.
This means that our fucntional computational model can be based on the concepts of variable, functional abstracion and application alone.
Using the formalization of these three concepts we form the lambda-terms. These terms represent both programs and data in our computational model (whose strenght in fact strongly depends on the fact it does not distinguish between "programs" and "data".)

   The formal definition of the terms of the Lambda-calculus (lambda-terms) is given by the following grammar:

Λ ::= X | (ΛΛ) | λX.Λ

where Λ stands for the set of lambda-terms and X is a metavariable that ranges over the (numerable) set of variables (x, y, v, w, z, x2, x2,...)
Variable and application are well-known concepts, but what is abstraction?
Abstraction is needed to create anonymous functions (i.e. functions without a name). We have seen that being able to specify an anonymous function is very important in fucntional programming, but it is also important to be able to associate an identifier to an anonymous function. Nonetheless we can avoid to introduce in our model the notion of "giving a name to a function". You could ask: how is it possible to define a function like fac without being able to refer to it trought its name??? Believe me, it is possible!.

The term λx. M represents the anonymous function that, given an input x, returns the "value" of the body M.
Other notions, usually considered as primitive, like basic operators (+, *, -, ...) or natural numbers, are not strictly needed in our computational model (indeed they can actually be treated as derived concepts.)

Bracketing conventions

For readability sake, it is useful to abbreviate nested abstractions and applications as follows:

(λx₁.(λx₂. ... . (λx_n.M) ... )    is abbreviated by    (λx₁x₂ ... x_n.M)

( ... ((M₁M₂)M₃) ... M_n)    is abbreviated by    (M₁M₂M₃ ... M_n)

We also use the convention of dropping outermost parentheses and those enclosing the body of an abstraction.

Example:

(λx.(x (λy.(yx))))     can be written as     λx.x(λy.yx)

In an abstraction λx.P, the term P is said to be the scope of the abstraction.
In a term, the occurrence of a variable is said to be bound if it occurs in the scope of an abstraction (i.e. it represents the argument in the body of a function).
It is said to be free otherwise.

These two concepts can be formalized by the following definitions.

Definition of bound variable
We define BV(M), the set of the Bound Variables of M, by induction on the term as follows:

BV(x) = Φ (the emptyset)
BV(PQ) = BV(P) U BV(Q)
BV(λx.P) = {x} U BV(P)

Definition of free variable
We define FV(M), the set of the Free Variables of M, by induction on the term as follows:

FV(x) = {x}
FV(PQ) = FV(P) U FV(Q)
FV(λx.P) = FV(P) \ {x}

Substitution

The notation M [L / x] denotes the term M in which any free (i.e. not representing any argument of a function) occurrence of the variable x in M is replaced by the term L.

Definition of substitution (by induction on the structure of the term)
1. If M is a variable (M = y) then:

2. If M is an application (M = PQ) then:

3. If M is a lambda-abstraction (M = λy.P) then:

Notice that in a lambda abstraction a substitution is performed only if the variable to be substituted is free.

Great care is needed when performing a substitution, as the following example shows:

Example:

Both of the terms   (λx.z)    and    (λy.z)    obviously represent the constant function which returns z for any argument

Let us assume we wish to apply to both of these terms the substitution [x / z] (we replace x for the free variable z). If we do not take into account the fact that the variable x is free in the term x and bound in (λx.z) we get:

(λx.z) [x / z]  =>  λx.(z[x / z])  =>  λx.x     representing the identity function
(λy.z) [x / z]  =>  λy.(z[x/ z])  =>  λy.x     representing the function that returns always x

This is absurd, since both the initial terms are intended to denote the very same thing (a constant function returning z), but by applying the substitution we obtain two terms denoting very different things.

Hence a necessary condition in order the substitution M[L/x] be correctly performed is that free variables in L does not change status (i.e. become not free) after the substitution. More formally: FV(L) and BV(M) must be disjoint sets.
Such a problem is present in all the programming languages, also imperative ones.

Example:

Let us consider the following substitution:

(λz.x) [zw/x]

The free variable z in the term to be substituted would become bound after the substitution. This is meaningless. So, what it has to be done is to rename the bound variables in the term on which the substitution is performed, in order the condition stated above be satisfied:

(λq.x) [zw/x]

  now, by performing the substitution, we correctly get: (λq.zw)

The example above introduces and justifies the notion of alpha-convertibility

The notion of alpha-convertibility

A bound variable is used to represent where, in the body of a function, the argument of the function is used. In order to have a meaningful calculus, terms which differ just for the names of their bound variables have to be considered identical. We could introduce such a notion of identity in a very formal way, by defining the relation of α-convertibility. Here is an example of two terms in such a relation.

λz.z  =_α λx.x

We do not formally define here such a relation. For us it is sufficient to know that two terms are α-convertible whenever one can be obtained from the other by simply renaming the bound variables.
Obviously alpha convertibility mantains completely unaltered both the meaning of the term and how much this meaning is explicit. From now on, we shall implicitely  work on λ-terms modulo alpha conversion. This means that from now on two alpha convertible terms like λz.z and λx.x are for us the very same term.

Example:

(λz. ((λt. tz) z)) z

All the variables, except the rightmost z, are bound, hence we can rename them (apply α-conversion). The rightmost z, instead, is free. We cannot rename it without modifying the meaning of the whole term.

It is clear from the definition that the set of free variables of a term is invariant by α-conversion, the one of bound variables obviously not.

The formalization of the notion of computation in λ-calculus:  The Theory of β-reduction

   In a functional language to compute means to evaluate expressions, making the meaning of a given expression more and more explicit. Up to now we have formalized in the lambda-calculus the notions of programs and data (the terms in our case). Let us see now how to formalize the notion of computation. In particular, the notion of "basic computational step".
We have noticed in the introduction that in the evaluation of a term, if there is a function applied to an argument, this application is replaced by the body of the function in which the formal parameter is replaced by the actual argument.
So, if we call redex any term of the form (λx.M)N, and we call M[N/x] its contractum, to perform a basic computational step on a term P means that P contains a subterm which is a redex and that such a redex is replaced by its contractum (β-reduction is applied on the redex.)
The relation between redexes and their contracta is called notion of β-reduction, and it is represented as follows.

The notion of β-reduction

(λx.M) N →_β M [N/x]

A term P β-reduces in one-step to a term Q if  Q can be obtained out of P by replacing a subterm of P of the form (λx.M)N by M[N/x]
 

Example:

If we had the multiplication in our system, we could perform the following computations

(λx. x*x) 2  =>  2*2   =>  4

here the first step is a β-reduction; the second computation is the evaluation of the multiplication function. We shall see how this last computation can indeed be realized by means of a sequence of basic computational steps (and how also the number 2 and the function multiplication can be represented by λ-terms).

Strictly speaking, M → N means that M reduces to N by exactly one reduction step. Frequently, we are interested in whether M can be reduced to N by any number of steps.

we write    M —» N     if     M → M₁ → M₂ → ... → M_k ≡ N    (K ≥ 0)

It means that M reduces to N in zero or more reduction steps.

Example:

((λz.(zy))(λx.x)) —» y

Normalization and possibility of non termination

Definition
If a term contains no β-redex, it is said to be in normal form.
Example:

λxy.y and xyz   are in normal form.

A term is said to have a normal form if it can be reduced to a term in normal form.
Example:

(λx.x)y   is not in normal form, but it has the normal form  y

Definition:
A term M is normalizable (has a normal form, is weakly normalizable) if there exists a term Q in normal form such that

M —» Q

A term M is strongly normalizable, if there exists no infinite reduction path out of M. That is, any possible sequence of β-reductions eventually leads to a normal form. 
 

Example:

(λx.y)((λz.z)t)

is a term not in normal form, normalizable and strongly normalizable too. In fact, the only two possible reduction sequences are:

1. (λx.y)((λz.z) t) → y

2. (λx.y)((λz.z) t) → (λx.y) t) → y

To normalize a term means to apply reductions until a normal form (if any) is reached. Many λ-terms cannot be reduced to normal form. A term that has no normal form is

(λx.xx)(λx.xx)

This term is usually called Ω.

Although different reduction sequences cannot lead to different normal forms, they can produce completely differend outcomes: one could terminate while the other could "run" forever. Typically, if M has a normal form and admits an infinite reduction sequence, it contains a subterm L having no normal form, and L can be erased by some reductions. The reduction

(λy.a)Ω → a

reaches a normal form, by erasing the Ω. This corresponds to a call-by-name treatment of arguments: the argument is not reduced, but substituted 'as it is' into the body of the abstraction.
Attempting to normalize the argument generates a non terminating reduction sequence:

(λy.a)Ω →(λy.a)Ω → ...

Evaluating the argument before substituting it into the body correspons to a call-by-value treatment of function application. In this examples, a call-by-value strategy never reaches the normal form.

Some important results of β-reduction theory

   The normal order reduction strategy consists in reducing, at each step, the leftmost outermost β-redex. Leftmost means, for istance, to reduce L (if it is reducible) before N in a term LN. Outermost means, for instance, to reduce (λx.M) N before reducing M or N (if reducible). Normal order reduction is a call-by-name evaluation strategy.

Theorem (Standardization)
If a term has a normal form, it is always reached by applying the normal order reduction strategy.

Theorem (Confluence)
If we have terms M, M₁ and M₂ such that:

M —» M₁    and    M —» M₂

then there always exists a term L such that:

M₁ —» L    and    M₂ —» L

That is, in diagram form:

Corollary (Uniqueness of normal form)
If a term has a normal form, it is unique.

Proof:

Let us suppose to have a generic term M, and let us suppose it has two normal forms N and N'. It means that

M —» N    and    M —» N'

Let us now apply the Confluence theorem. Then there exists a term Q such that:

N —» Q    and    N' —» Q

But N and N' are in normal form, then they have not any redex. So, it necessarily means that

N —» Q   in 0 steps

and hence that N ≡ Q.
Analogously we can show that N' ≡ Q. It is then obvious that   N ≡ N'.

The above result is a very important one for programming languages, since it ensures that if we implement the same algorithm in Scheme and in Haskell, the functions we obtain give us the very same result (if any), even if Scheme and Haskell are functional languages that use very different reduction strategies.

In the syntax of the λ-calculus we have not considered primitive data types (the natural numbers, the booleans and so on), or primitive operations (addition, multiplication and so on), because they indeed do not  represent really primitive concepts. As a matter of fact, we can represent them by using the essential notions already formalized  in the λ-calculus, namely variable, application and abstraction.

The theory of β-conversion

It is possible to formalize the notion of computational equivalence of programs into the lambda calculus. This is done by introducing the relation of β-conversion among λ-terms, denoted by M =_β N
Informally, we could say that two terms are β-convertible when they "represent the same information": actually if one can be transformed into the other by performing zero or more β-reductions and β-expansions.
(A β-expansion being the inverse of a reduction:    P[Q/x] ← (λx.P)Q  ) .
We shall not treat the theory of β-conversion in our course.

Representing data types and functions on them

In the syntax of the λ-calculus we have not considered primitive data types (the natural numbers, the booleans and so on), or primitive operations (addition, multiplication and so on), because they indeed do not  represent really primitive concepts. As a matter of fact, we can represent them by using the essential notions already formalized  in the λ-calculus, namely variable, application and abstraction. We shall not show how to do it (even if it fairly simple and natural). Even more, it is possible to represent in the lambda-calculus any computable function.

Representing recursive functions

In the syntax of the λ-calculus there is no primitive operation that enables us to give names to lambda terms. However, that of giving  names to expressions seems to be an essential features of programming languages in order to define functions by recursion, like in Scheme

(define fact (lambda (x) (if (= x 0) 1 (* x (fact (- x 1))))))

or in Haskell

fact 0 = 1

fact n = n * fact (n-1)

Then, in order to define recursive functions, it would seem essential to be able to give names to expressions, so that we can recursively refer to them.
Surprisingly enough, however, that's not true at all! In fact, we can represent recursive functions in the lambda-calculus by using the few ingredients we have already at hand, exploiting the concept of fixed point.
The notion of fixed point can be represented in the lambda calculus through terms like

λf. (λx. f(xx)) (λx. f(xx))

factorial = λx. if (x=0) then 1 else (x*factorial(x-1))

λf. λx. if (x=0) then 1 else (x*f(x-1))

 Reduction strategies

One of the aspects that characterizes a functional programming language is the reduction strategy it uses. Informally a reduction strategy is a "policy" which chooses a β-redex , if any, among all the possible ones present in the term. It is possible to formalize a strategy as a function, even if we do not do it here.

Let us see, now, same classes of strategies.

Call-by-value strategies
These are all the strategies that never reduce a redex  when the argument  is not a value.
Of  course we need to precisely formalize what we intend for "value".
In the following example we consider a value to be a lambda term in normal form.

Example:

Let us suppose to have:

((λx.x)((λy.y) z)) ((λx.x)((λy.y) z))

A call-by-value strategy never reduce the term (λx.x)((λy.y) z) because the argument is not a value. In a call-by-value strategy , then, we can reduce only one of the redex underlined.

Scheme uses a specific call-by-value strategy, and a particular notion of value.
Informally, up to now we have considered as "values" the terms in normal form. For Scheme, instead, also a function is considered to be a value (an expression like λx.M, in Scheme, is a value).
Then, if we have

(λx.x) (λz.(λx.x) x)

The reduction strategy of Scheme first reduces the biggest redex (the whole term), since the argument is considered to be a value (a function is a value for Scheme). After the reduction the interpreter stops, since the term λz.((λx.x) x) is a value for Scheme and hence cannot be further evaluated.


Call-by-name strategies
These are all the strategies that reduce a redex without checking whether its argument is a value or not. One of its subclasses is the set of lazy strategies. Generally, in programming languages a strategy is lazy if it is call-by-name and reduces a redex only if it's strictly necessary to get the final value (this strategy is called call-by-need too). One possible call-by-name strategy is the leftmost-outermost one: it takes, in the set of the possible redex, the leftmost and outermost one.

Example:

Let us denote by I the identity function and let us consider the term:

(I (II)) ( I (II))

the leftmost-outermost strategy first  reduces the underlined redex.

We have seen before that the leftmost-outermost strategy is very important since, by the Standardization Theorem, if a term has a normal form, we get it by following such a strategy. The problem is that the number of reduction steps is sometimes greater then the strictly necessary ones.


If a language uses a call-by-value strategy, we have to be careful because if an expression has not normal form, the search could go on endlessly.

14 Types and Typed Lambda-Calculi

  Introduction to types

The functional programming languages can be typed or untyped. A typed one is, for example, Haskell, while an untyped language is Scheme. By introducing the notion of type in the λ-calculus we shall be able to study it in an abstract and simplified way.
We can look at types as predicates on programs or, better, as partial specifications about the behaviour of programs. In the programming practice the use of types is helpful to prevent a number of programming errors.

There are two different approaches to the use of types.

• the approach a' la Curry (the one used in Haskell)
• the approach a' la Church (the one used in Pascal)

In the Curry approach, we first write a program and then check whether it satisfies a given specification.
Instead, in the Church approach, types are included in the syntax of the language and, in a sense, represent some constraints we have to follow during the writing of our programs in order to avoid making particular errors.
In the approach a' la Curry, checking if a term M satisfies the specification represented by the type t,  it is usually  referred to as "assigning the type t to the term M".

   Type assignment 'a la Curry

In this approach we firsr write a program and then we check whether it satisfies the specification we had in mind. This means that we have two distinct sets:  programs and partial specifications.
If we wish to talk in a general and abstract way about types (a' la Curry) in functional programming languages we can proceed with the following formalization:

where φ is a meta-variable which ranges over a set of type variables (φ, φ', φ'', a, b, ... etc.).  In this formalization we have considered the simplest form of type (in fact these types are called simple types). Elements of T will be denoted by σ, τ , ρ, etc.
 

There arise now a whole bunch of questions we should answer:

1) How can we formally show that, given a program (a term) M and a specification (a type) σ, M satisfies the specification  σ? That is, how can we prove that M has type σ?

2) Is it decidable,  given a M and a σ, that M is of type σ? i.e., given a program (term) M and a specification (type) σ, is there any algorithm enabling us to check whether M satisfies σ?

3) How can we be sure that the type of a term actually provide a piece of information about the semantics of a term?

4) What is the intrinsic meaning of having type variables in our system? has the use of type variables some implication for our system?

5) Is it possible to "compare" types? i.e., is it possible to formalize the notion that a type represents a "more general" specification than another one?

6) Is there any relation among all the possible types we can assign to a term M? there exists the most general type among them? If so, can it be algorithmically found?

Let us start with question 1).
What we need to do is to devise a formal system whose judgments (typing judgements) are of the form

M : σ

and whose meaning is: the program M respects the specification σ  (formally, the term M has type σ).

If we think about it, however, we can notice that our typing judgments should provide some more information than simply M : σ.
In fact, let us consider the term  λx.yx. Which sort of specification is satisfied by such a program?
In case the input is of type φ, a type for λx.yx is definitely of the form

φ → something

But now, how can we found out what something could be, if we do not have any information about the free variable y? Our program (term) takes an input x and returns the result of the application of y to x. If we do not make any assumption about the type of the free variable y, we cannot say anything about the type of yx.
This means that the (typing) judgments we are looking for should indeed have the following shape:

B |— M:σ

where B (called a basis), provides informations about the types of the free variables of M.
The meaning of the typing judgment   B |—  M : σ  is then:
using the informations given by the basis B, the term M satisfies the specification σ
(i.e. M has type σ under the assumptions provided by the basis B; or, shortly, M has type σ in B.)

Formally B will be a set of pairs of the form :   variable : type

An example of basis is, for instance, B = {x : τ , z : ρ}

Let us introduce now the formal system enabling us to infer types for lambda-terms.

Definition (Curry type assignment system)

Axiom

(a variable x has type σ  if the statement x : σ is in B).

Inference rules

These rules allow to derive all the possible valid typing judgements.

• 
  This rule says that if, by using the assumptions in B, we can prove that M has type
  σ → τ and N has type σ, then we are assured that, in the basis B, the application MN has type τ. This rule is usually called (→E): "arrow elimination". This rule can be "read" also bottom-up, as follows: if we wish to prove that MN has type τ in B, then we need to prove that M has type σ → τ in B for some σ and that N has type σ in B.
•  

• 
  This rule says that if, by using the assumptions in  B and the further assumption "x has type σ", we can prove that M has type τ, then we we are assured that, in B,  λx.M has type σ → τ. This rule is called (→I) : "arrow introduction". Also this rule can be "read" bottom-up. Do it as exercise.

  A term M is called typeable if there exist a basis B and a type σ such that the judgment
B |— M : σ can be derived in the assignment system above.

The above formal system is the core of the type systems of languages like Haskell, ML and others. This is the main motivation for which we are studying it.

Remark:

In Haskell, before writing the definition of a function, we can declare what type our function is intended to have, for instance:

fact :: Int → Int

By doing that, after defining the function fact the Haskell interpreter can check whether our program fact satisfies the given specification. In particular, the interpreter tries to derive, in a formal system like the one defined before, the Haskell typing  judgement   fact :: Int →Int.
Note: In Haskell we have not the concept of basis, because in correct programs an identifier either is a bound variable or it has been previously associated to some value.

Example:

Let Ø be the empty set and let us consider the judgment

Ø |— λxy.x : σ → (τ → σ)

whose informal meaning is: by considering no assumption at all (the empty basis), the term λxy.x satisfies the specification σ → (τ → σ).
If we wish to formally prove that the above judgment is valid, we need to use the Curry type assignment system.
Let us start from the axiom:

By using (→I) two times, we get

Let us notice that in the last two steps we have discharged, from the basis we have started with, the assumptions for the bound variables of the term. In fact, a basis has to provide only informations about   free variables, since the informations about bound variables are already contained in the type of the term.

Example:

We want to prove that:

B = {f : σ → σ, x : σ} |— f (f (fx)) : σ

Starting from B, we use the axiom and the rules of our formal system:

We can go on and derive, from the derivation above, other judgments:

Remark:
There are programs that do not satisfy any specification, whatever be the basis B. For example, let us consider:

It is impossible to derive this judgment in our system, whatever basis B and type τ we choose. What is the implication of this simple observation? Well, typed languages restrict the set of programs we can write, but on the other hand the programs we can write are safer, i.e. they are guaranteed not to contain certain errors and to satisfy their partial specifications. We loose something of course, that is flexibility, the possibility of writing "tricky" and "sly" programs.
So, in typed languages:    less flexibility = more safeness.
 

There is a quite relevant property of typeable terms that concerns strong normalizability.

Theorem
    Any typeable term is strongly normalizable.

So, since self-application cannot be typed, it follows that the combinator Y cannot be typed. This implies that we cannot type any term representing a recursive algorithm. This is also why, whereas in Scheme, if we wished, we could define recursive programs using fixed-point combinators, in Haskell it is not possible.
Of course this is not a real drawback for Haskell, since it is not realistic to write actual recursive programs by means of fixed-point combinators. In Haskell recursion is obtained by the use of recursive equations (which corresponds to the possibility of giving names to expressions.)


Let us now discuss another relevant property of our type assignment system:  Subject reduction

Saying that M has type σ   (M : σ ) amounts to say that M represents a value of type σ. The types should not give information about the form of the terms (about their syntax, in general), but, instead, they should provide informations about their intrinsic meaning, their semantics.
Hence, if a term has a certain type, it is important to be sure that during its evaluation the term "maintains" the same type.
For example, if a term M represents a program that returns a number, types would be useless   if we could  reduce M to a term that represents a program which returns a list.
Fortunately we can prove the following

Theorem  (Subject reduction)
If in a basis B we can prove that M has type σ, that is

B |— M : σ

and if  M —» N, then we can also prove that

B |— N : σ

Thanks to this theorem we are sure that, if we check that a term M has a given type at the beginning of a computation, then we can forget about types during the computation, since all the terms that we obtain by reducing M can be given the very same type. This also implies that types are irrelevant, do not play any role, in the computational process.

 Let us note that the subject reduction property holds only for reductions and not for expansions. That is, if we have that

B |— N : σ     and     M —» N

it is not always true that

B |— M : σ

By means of the Subject reduction theorem we have also answered question 3).

Let us now try and answer  question 4). Question 2) has still to be answered, but it will be done using the answer for 6)

Definition  (Type substitution)
Let T be the set of simple types:

  a) the type substitution (φ ρ) : T → T, where φ is a type-variable and ρ is a type, is inductively defined by:

 (φ ρ) φ = ρ
(φ ρ) φ' = φ', if φ' ≠ φ
(φ ρ) σ → τ = ((φ ρ) σ) → ((φ ρ) τ)

The above definition formalizes the notion of "substituting a type variable by a type inside a type"

  b) We can compose type substitution, that is, if S₁, S₂ are type substitutions, then so is S₁oS₂, where:

S₁oS₂ σ = S₁ (S₂ σ)

  c)  A type substitution can also be applied to a basis:   SB = {x : Sτ | x : τ is in B}

  d) A type substitution can also be applied to pairs of basis and type (it will be useful later on)

        S <B, σ> = <SB, Sσ>
 

Note: The notion of substitution for types is much simpler than the one for terms, since in simple types we do not have bound type-variables.

Note: The above definition of type susbtitution is tailored in order to be used for the principal pair algorithm that we shall describe below. In fact it is not possible to describe a type substitution transforming φ→ψ into ψ→φ. This is not a problem, since such a type substitution will never be needed in the principar pair algorithm.

Example:  if we apply the type substitution (φ σ) to the type φ → (τ→ φ), and if τ does not contain φ, we obtain the type    σ → (τ→ σ)

If for σ,τ there is a substitution S such that Sσ = τ, we say that τ is a (substitution) instance of σ.


The following lemma shows that if a term has a type, it has indeed infinitely many tipes. The Lemma will provide, at the same time, an answer to question 4).

Lemma (substitution lemma)
If using a basis B we can prove that a term M has a type σ, that is

B |— M : σ

then, for all possible substitutions S, we can also prove that:

S(B) |— M : S(σ)

Note: The above substitution lemma holds also for a more general definition of type substitution.

So the Substitution Lemma states that if a term satisfies a specification, then it satisfies infinitely many ones (because we can have infinitely many possible substitutions.)


Example:

It is easy to prove that

{x : φ → ψ} |— λy .xy : φ → ψ

The Substitution Lemma states that if we apply any substitution S, it is also true that

S({x : φ → ψ}) |— λy .xy : S(φ → ψ)

For example, by considering the substitution

(φ (φ' → φ)) o (ψ ξ)

it is true that

x : (φ' → φ) → ξ |— (λy .xy) : (φ' → φ) → ξ

Example:

If we have derived  

Ø |— λx.x : φ → φ

by the Substitution Lemma we are sure that also the following judgment is derivable

Ø |— λx.x : (ψ → φ) → (ψ → φ)

What we have just seen means that in our formal system we have polymorphic functions (a function is called polymorphic  if it can be correctly applied to objects of different types).
So, by using type variables, we have implicitly introduced a notion of polymorphism in our type assignment system.
Since this system is the core of the type system of Haskell, this implies that Haskell is a language with polymorphism. (In Haskell type variables have names like a, b, c etc.)

To state that the lambda term λx.x has type  a → a   is tantamount to say that λx.x is a polymorphic function, that is it can be uniformly applied to any element of any type T and it returns an element of type T. The type a → a is (implicitly) a polymorphic type since, being "a" a type-variable, it "represents" all the types with shape  T →  T.
This sort of polymorphism is called parametric polymorphism.  In particular, the parametric polymorphism of our system can be said to be implicit, since the fact that a term has many types it is not explicitly expressed in the syntax by means of particular operators on types, but it is expressed by results like the Substitution Lemma.
A possible syntax for explicit parametric polymorphism could be the following one:

λx.x : ∀φ.(φ → φ)

In this case the polymorphic behaviour of the term is explicitely described by the sintax.
(We shall deal later on with another sort of polymorphism: subtyping polymorphism. Besides, when studying the Type Classes in Haskell we shall deal with one more sort of polymorphism: overloading, a very restricted sort of polymorphism actually.)

We can now provide, using the notion of type substitution, an answer to question 5) by giving the following definition.

Definition (more general type)
Let τ and σ be two simple types.
τ is said to be more general than σ if there exists a substitution S such that   σ = S(τ).
That is if the latter can be obtained from the former by means of a type substitution.


We know that if a term M has a type, it has infinitely many ones. Now, it is also possible to prove that there exists a precise relation among all the types that a given term has (i.e. all the possible partial specifications of a program are, so to speak, connected to each other).
That would be an answer for question 6). Such an answer will also provide an answer for question 2) that up to now we have left unanswered.

   Principal pairs

Theorem
Given a term M, if M is typeable then it has a Principal Pair  <P, π>, where P is a basis and  π a type such that:

1) we can derive the following typing for M 

P |— M : π

2) Moreover, if we can derive

B |— M : σ

then there exists a substitution S such that B = S(P) (as a matter of fact B could be a superset of S(P)) and σ = S(π).
In other words, the principal pair represents the most generic typing possible for M. That is, any other basis and type that we can use to type M can be obtained from the principal pair.

This partially answer our question 6)


Example:

Let us consider the term:

λx.x

It has principal pair:

<Ø, φ → φ>

This means that any other typing for the identity  is a substitution instance of this principal pair.

The proof of the principal pair algorithm can be given by providing an algorithm that, given a term M, returns its principal pair, pp(M), and fails in case M be not typeable.
These completes the answer of our question 6).

  Before giving the formal description of the Principal Pair Algorithm (also called Hindley-Milner algorithm), let us first informally describe how it works.
The algorithm tries to type the given term in the most general way (that is to find the most general basis and the most general type for the term.) It tries to do that by using the rules of the assignment system, in a bottom-up way.