Functional Programming

Table of Contents

1 References

2 Expression

An expression can be reduced to an simpler equivalent form. We say an expression is canonical (or in normal form) if it cannot be further reduced.

The result of equality test is done by reducing the expressions to their canonical form, and testing whether the results are identical. If an expression does not have a canonical form, the result is undefined, represented by \(\bot\). In particular, function values have no canonical form.

The order of evaluation thus matters. Each reduction step replace a sub-term by an equivalent term. The term is called a redex, short for reducible expression. There are two reduction policies, innermost reduction and outermost reduction. Innermost reduction reduces the innermost redex, i.e. the one that contains no other redex. Outermost reduction reduces the one that is contained in no other redex.

Any term that is reduced must be reduced to head normal form. A term is in head normal form if it is not a redex, and it cannot become a redex by reducing any of its subterms. For example, (e1:e2) is in head normal form, because the (:) itself cannot be reduced. However, e1 and e2 might be reducible. It is a normal form only when e1 and e2 both are in normal form. By definition, every term in normal form is in head normal form, but not vice versa.

The evaluation order matters because of the termination. Sometimes, the outermost reduction will terminate while the inner most fail to do so. In fact, we have the following property:

For every term, if there exists any reduction order that terminates, then there is an outermost reduction that terminates.

Thus, outermost reduction is also called normal order reduction, because it is capable of reducing a term to its normal form whenever the term has such a form. It is also called lazy evaluation, because it does not reduce a term unless it is essential for finding the answer. By contract, the innermost reduction is called applicative order reduction, or eager evaluation.

Outermost reduction is essential for evaluating non-strict functions. But innermost and outermost reduction will yield the same answer when only strict functions are involved.

With that said for termination property, however, outermost may require more steps than innermost reduction. The reason is that, the outermost reduction might duplicate some inner expressions. One problem is called graph reduction, which ensures that the duplicated sub-terms are always linked together in the graph, and reduction of them will happen ones, for all the references of them. With graph reduction, we can say outermost reduction never performs more steps than innermost.

In summary, we shall use outermost graph reduction as the evaluation model, because

  1. it terminates whenever any reduction order terminates
  2. it requires no more steps than innermost order reduction

However, the outermost reduction might use more space than innermost. In this case, it might be desired to mix innermost order to achieve better space efficiency. There is a special function strict that fine-control the evaluation order. strict f e is reduced by first reducing e to head normal form, then applying f. The term e itself is evaluated as normal, using outermost order. With that, strict can be defined like below. We can easily have this: f = strict f iff f is a strict function.

strict f x = \bot, if x = \bot
           = f x,  otherwise

There are some ways to decide how to use strict to optimize the space occupation, but some takeaway: for functions such as (+) or (x), that are strict in both arguments, and can be computed in constant time and space, foldl' is more efficient. But for functions, such as (&) and (++), that are non-strict in some argument, foldr is often more efficient. (foldl' is a rewrite of foldl with strictness)

foldl' (op) a [] = a
foldl' (op) a (x:xs) = strict (foldl' (op)) (a op x) xs

3 What is a Function?

  • currying: replacing structured arguments by a sequence of simple ones. The function application operation associates to the left, i.e. f x y means ((f x) y).

3.1 Composition

Functional composition has the definition of

\[(f \circ g) x = f (g x)\]

and the type of it

\[(\circ) :: (\beta \rightarrow \gamma) \rightarrow (\alpha \rightarrow \beta) \rightarrow (\alpha \rightarrow \gamma)\]

functional composition is also associative, thus no need to put brackets

\[(f \circ g) \circ h = f \circ (g \circ h)\]

3.2 Strictness

The special value \(\bot\) is polymorphic: \(\bot\) is a value of every type. This means, any function can be applied to \(\bot\). If \(f \bot = \bot\), then \(f\) is said to be strict. Otherwise, it is non-strict. In other words, a function is strict if it is undefined whenever its argument is undefined.

In fact, a non-strict semantic is often preferable for functions, for several reasons:

  • it makes reasoning about equality easier
  • we can define new control structures by defining new functions

For example, we define a function three that takes anything and return the value 3. I.e.

three :: num -> num
three x = 3

Another example, the definition of cond

\[cond :: bool \rightarrow \alpha \rightarrow \alpha \rightarrow \alpha\]

cond p x y = x, if p
           = y, otherwise

Under strict semantics, \(cond\ True\ 0\ \bot = \bot\), under non-strict semantics, \(cond True 0 \bot = 0\). But in either case, cond is strict on its first argument. This also means, strictness is bundled with the function, and is applied on some arguments, not all.

The operational semantics of strict or non-strict functions is closely related to the reduction strategy. eager-evaluation reduces every expression to its simplest form, while lazy-evaluation does not care about the wellness of the expressions whose values are not required for the evaluation.

4 Type

  • Strong-typing: the type of an expression depends only on the type of its component expressions.
  • Type variable: typically represented in Greek letters \(\alpha\), \(\beta\), etc. Such type can be instantiated by substitute the type variable with specific type.
  • Polymorphic type: a type that contains type variables
  • Enumerated type: enumeration of possible values
  • Composite type: composite primitive type together to form new types
  • algebraic data type: is a form of composite type, containing product type and sum type
    • sum type: this is like C union, so it is also called a tagged union. It can take value of either the type, but not both.
    • product type: this is like a C structure with different fields. The value set of this type is the set-theoretic product, i.e., the Cartesian product of the set of the field type.
  • Abstract Type: types in which the values are prescribed, but the operations are not, are called concrete types. A type whose values are not defined, but operations are, is called abstract type.

4.1 Type inference

Three basic rules

  1. Application rule: if f x :: t, then x :: t' and f :: t' -> t for some new type t'
  2. Equality rule: if both the types x :: t and x :: t' can be deduced for a variable x, then t = t'.
  3. Function rule: If t -> u = t' -> u', then t = t', and u = u'

Often, the newly introduced types are named by numerical sub-notation.

For example, consider the composition operator

(.) f g x = f (g x)

The following script shows the inference steps:

f :: t1
g :: t2
x :: t3
f (g x) :: t4
(.) :: t1 -> t2 -> t3 -> t4
g x :: t5
f :: t5 -> t4
x :: t6
g :: t6 -> t5
t1 = t5 -> t4
t2 = t6 -> t5
t3 = t6
(.) :: (t5 -> t4) -> (t6 -> t5) -> t6 -> t4

Finally, we need to replace the types with type variables to make it generic:

\[(\circ) :: (\beta \rightarrow \gamma) \rightarrow (\alpha \rightarrow \beta) \rightarrow (\alpha \rightarrow \gamma)\]

4.2 List

List itself is defined as a recursive type.

\[list \alpha :: Nil | Cons \alpha (list \alpha)\]

Let list comprehension notation be [<expr> | <qualifier>; ...]. Qualifier can be boolean expression for predicates or generators. Later generators vary more quickly than their predecessors, and can depends on the variables introduced by earlier ones. With this, we can define many operators on lists:

(++) :: [a] -> [a] -> [a]
concat :: [[a]] -> [a]
concat xss = [x | xs <- xss; x <- xs]

Instead of using (++) for concating list, we can use (:) (pronounced 'cons') for specifying consing. One important reason to use (:) is that, every list can be expressed in terms of [] and (:) in exactly one way.

(:) :: a -> [a] -> [a]
x:xs = [x] ++ xs

We have the following operators on lists:

(#) :: [a] -> num
#(xs ++ ys) = #xs + #ys

hd :: [a] -> a
tl :: [a] -> [a]
hd ([x] ++ xs) = x
tl ([x] ++ xs) = xs

take n xs ++ drop n xs = xs

takewhile :: (a -> bool) -> [a]  -> [a]
zip :: ([a], [b]) -> [(a,b)]
(!) :: [a] -> num -> a # index

Map and filter can be defined by:

map :: (a -> b) -> [a] -> [b]
map f xs = [f x | x <- xs]
filter :: (a -> bool) -> [a] -> [a]
filter p xs = [x | x <- xs; p x]


foldr :: (a -> b -> b) -> b -> [a] -> b
foldl :: (b -> a -> b) -> b -> [a] -> b
sum = foldr (+) 0
product = foldr (x) 1
concat = foldr (++) []
and = foldr (&) True
or = foldr (|) False

foldr and foldl do rely on associative of the underlying operators to function correctly, and there are several duality theorems.

In big data literature, map and reduce are borrowed from functional programming. Map is just map, reduce has another familiar name called fold. The Map-reduce framework does not just borrow the name. Its contribution is scalability and fault-tolerance. In this case, map produces data by filtering, and emit the data, marshalling, and reduce does folding.

5 Recursion

Functions are often defined recursively. In this section, we see some of the list function definitions in recursion.

zip([], ys) = []
zip(x:xs, []) = []
zip(x:xs, y:ys) = (x,y):zip(xs,ys)
take 0 xs = []
take (n+1) [] = []
take (n+1) (x:xs) = x:take n xs

drop 0 xs = xs
drop (n+1) [] = []
drop (n+1) (x:xs) = drop n xs
hd(x:xs) = x
tl(x:xs) = xs
map f [] = []
map f (x:xs) = f x : map f xs
filter p [] = []
filter p (x:xs) = x : filter p xs, if p x
                = filter p xs,     otherwise