Functional Programming - Exhaustive Course Notes

Foundations of Functional Programming: General Introduction

• Importance of Diverse Programming Languages for Computer Scientists:

  • Expression of Ideas: Familiarity with various concepts allows for better expression of ideas during software development.

  • Project Suitability: Knowledge is required to select the most appropriate language for specific projects.

  • Adaptability: Learning conceptually different languages makes it easier to acquire new ones later.

  • Language Design: Computer scientists are often tasked with designing new languages, which must build on existing foundations.

• Comparison of Paradigms:

  • Imperative Programming:

  • Programs are sequences of instructions executed one after another.

  • They modify variable values in memory (side effects).

  • Closely linked to the "Von Neumann" architecture.

  • Examples: C (low-level efficiency, manual memory management), Java.

  • Declarative Programming:

  • Focuses on specifying what should be calculated rather than how.

  • The interpreter/compiler determines the execution path.

  • It is problem-oriented rather than machine-oriented.

  • Sub-divided into Functional and Logic programming.

• Case Study: Calculating List Length:

  • Java (Imperative):

  • Uses a while loop to iterate through memory pointers.

  • Side Effect: In the provided example, calculating length len(l) sets l.head = null, essentially emptying the list as a side effect. To avoid this, developers must manually manage memory/cloning.

  • Haskell (Functional):

  • Defined by recursive equations:

    • (A) If list is empty, length is $0$.

    • (B) If list is not empty ($x:xs$), length is $1 + len(xs)$.

  • Implementation:

    • len :: [a] -> Int (Type declaration)

    • len [] = 0 (Base case)

    • len (x:xs) = 1 + len xs (Recursive case)

  • Uses Pattern Matching to determine which equation to apply.

• Core Properties of Haskell:

  • No Loops: Control flow is managed via recursion.

  • Parametric Polymorphism: Functions (like len) work on lists of any type a. Systems guarantee data is not misinterpreted.

  • Referential Transparency: No side effects. Applying a function to the same arguments always yields the same result.

  • Automatic Memory Management: No explicit pointer manipulation or memory allocation/deallocation.

  • Functions as First-Class Citizens: Functions can be arguments or results of other functions (Higher-Order Functions).

  • Lazy Evaluation: Arguments are only evaluated if necessary for the result.

• Advantages of Functional Programming:

  • Programs are shorter, clearer, and easier to maintain.

  • Less error-prone, facilitating more reliable software and verification.

  • Faster development cycles and ideal for prototyping.

  • Better reusability and modularity.

• Course Overview:

  • Chapter 1: Introduction to Haskell syntax and techniques.

  • Chapter 2: Denotational Semantics (formal mathematical meaning of programs).

  • Chapter 3: Lambda Calculus ($\Lambda$-Calculus) as the fundamental base of all functional languages.

  • Chapter 4: Type checking and inference (Algorithm W).

Chapter 1: Introduction to the Haskell Programming Language

• Basic Structure:

  • A program is a sequence of Declarations.

  • Declarations must be left-aligned (Offside Rule).

  • Syntax is defined by context-free grammars.

  • Comments:

  • Block: {- Comment -}

  • Line: -- Comment

• Types and Function Declarations:

  • Type Declaration: square :: Int -> Int.

  • The first Int is the domain; the second is the codomain.

  • var1, ..., varn :: type defines types for multiple variables.

  • Function Declaration: square x = x * x.

  • Left side: Function name and parameters.

  • Right side: Expression defining the result.

  • Standard Libraries: Haskell loads "Prelude" by default, containing arithmetic operations (+, *, -, /), Boolean types (True, False), and logic (not, &&, ||).

• Program Execution and Term Rewriting:

  • Execution involves evaluating expressions via Term Replacement.

  • Redex (Reducible Expression): A sub-expression matching the left side of a defining equation.

  • Evaluation Steps:

  1. Find a redex.

  2. Replace it with the right side of the equation, substituting variables.

  • Evaluation Strategies:

  • Strict (Leftmost Innermost / Call-by-Value / Eager): Evaluates the leftmost innermost redex first.

  • Non-Strict (Leftmost Outermost / Call-by-Name): Evaluates the leftmost outermost redex. Arguments are passed unevaluated.

  • Lazy Evaluation: Non-strict evaluation that uses pointers to avoid redundant calculations of the same sub-term.

  • Result Invariance: If any strategy terminates, the result is identical regardless of the strategy (Church-Rosser property), though termination behavior varies.

• Advanced Declarations:

  • Conditional Equations (Guards):

  • maxi(x, y) | x >= y = x | otherwise = y

  • Currying: Named after Haskell B. Curry. Converting a function with a tuple of arguments into a sequence of functions with single arguments.

  • plus :: Int -> Int -> Int is equivalent to plus :: Int -> (Int -> Int).

  • Allows Partial Application: plus 1 results in a successor function.

  • Local Declarations:

  • where block: Follows a right side; values calculated once and shared.

  • let ... in ...: Expression-level local binding.

  • Offside Rule: Determined by the indent of the first symbol in a declaration block.

• Infix Operators:

  • Operators consist of special characters. Constructor operators (like :) start with a colon.

  • Any prefix function can be infix using backquotes: 2 `plus` 3.

  • Any infix operator can be prefix using parentheses: (+) 2 3.

  • Properties:

  • Associativity: infixl (left), infixr (right), or infix (none).

  • Binding Priority: Integer from $0$ to $9$ ($9$ is highest). Default is $9$.

Chapter 1.1.2 - 1.1.4: Expressions, Patterns, and Types

• Expression Types:

  • var (variables), constr (constructors starting with uppercase), integer, float, char ('a'), string ("hallo", synonymous with [Char]).

  • Lists: [1,2,3] is shorthand for 1:(2:(3:[])).

  • Tuples: (10, False). Elements can have different types. Empty tuple () has type ().

  • Conditionals: if exp1 then exp2 else exp3 (requires exp1 :: Bool).

  • Case Distinction: case exp of {pat1 -> exp1; ...}.

  • Lambda Abstraction: \pat1 ... patn -> exp. Represents anonymous functions.

• Patterns:

  • Used for decomposing objects via matching.

  • Linearity: A variable can appear only once in a pattern to ensure deterministic evaluation.

  • Pattern Types:

  • Variable: Matches anything, binds it.

  • Joker (_): Matches anything, no binding.

  • Constants: Matches exact values (Int, Char, etc.).

  • Constructors: (Cons x xs) matches a non-empty list.

  • As-Patterns: var@pat (binds var to the entire matched structure).

  • Tupel/List Patterns: (p1, p2), [p1, p2, p3].

• Types & Polymorphism:

  • Parametric Polymorphism: Functions use type variables (e.g., id :: a -> a) to work regardless of concrete types.

  • Ad-hoc Polymorphism: Overloading. The same symbol behaves differently based on type.

  • Type Definitions:

  • type Name = Typ (Type synonym/abbreviation).

  • data Name vars = C1 t1 ... | C2 t1 ... (Algebraic data type).

  • Example: data List a = Nil | Cons a (List a).

• Type Classes:

  • Sets of types that implement specific methods.

  • Common Classes:

  • Eq: Requires (==) and (/=).

  • Ord: Requires comparison such as (<), (<=).

  • Show: Requires show :: a -> String.

  • Num: Requires arithmetics like (+), (*), (-).

  • Contexts: Eq a => [a] -> Bool restricts the type variable a to members of class Eq.

  • Instancing: instance Eq Int where (==) = primEqInt.

  • Deriving: deriving (Eq, Show) automatically generates standard implementations.

Chapter 1.2: Higher-Order Functions

• Definition: Functions that take functions as arguments or return them as results.

• Function Composition (.):

  • Defined as: (.) :: (b -> c) -> (a -> b) -> (a -> c).

  • f . g = \x -> f (g x).

• Curry and Uncurry:

  • curry :: ((a,b) -> c) -> (a -> b -> c).

  • uncurry :: (a -> b -> c) -> ((a,b) -> c).

• Standard Recursion Patterns:

  • Map: Applies a function to every element of a structure.

  • map :: (a -> b) -> [a] -> [b].

  • map f [] = [], map f (x:xs) = f x : map f xs.

  • ZipWith: Combines two lists using a binary function.

  • zipWith f (x:xs) (y:ys) = f x y : zipWith f xs ys.

  • Filter: Removes elements that do not satisfy a predicate.

  • filter :: (a -> Bool) -> [a] -> [a].

  • Fold (Reduction): Replaces constructors with functions and initial values.

  • foldr :: (a -> b -> b) -> b -> [a] -> b.

  • foldr f e (x:xs) = f x (foldr f e xs).

  • Example: sum = foldr (+) 0.

• List Comprehension:

  • Syntax: [ exp | qual1, ..., qualn ].

  • Qualifiers are generators (var <- list) or guards (Boolean expressions).

  • Translation:

  • [exp | var <- exp', Q] = concat (map (\var -> [exp | Q]) exp').

  • [exp | guard, Q] = if guard then [exp | Q] else [].

  • Quicksort Implementation:

  • qsort [] = []

  • qsort (x:xs) = qsort [y | y <- xs, y < x] ++ [x] ++ qsort [y | y <- xs, y >= x].

Chapter 1.3 - 1.4: Lazy Evaluation and Monads

• Programming with Lazy Evaluation:

  • Non-strictness allows for Infinite Data Objects.

  • from x = x : from (x+1) results in [x, x+1, ...].

  • take n can be used to extract finite parts from infinite structures.

  • Sieve of Eratosthenes: Calculating infinite prime numbers by iteratively filtering multiples of the first list element.

  • Cyclic Objects: ones = 1 : ones creates a self-referencing list in memory.

  • Hamming Problem: Generating a sorted list of numbers whose prime factors are only $2, 3, 5$.

  • Linear complexity $O(n)$ achieved using un-evaluated list pointers and the mer (merge) function.

• The IO Monad:

  • To preserve Referential Transparency, side effects are encapsulated in the IO a type.

  • IO a represents an action that, when executed, yields a value of type a.

  • Primitive Actions:

  • putChar :: Char -> IO () (Output).

  • getChar :: IO Char (Input).

  • return :: a -> IO a (Encapsulate a value in a trivial action).

  • Combinators:

  • (>>) :: IO a -> IO b -> IO b (Sequencing, ignore first result).

  • (>>=) :: IO a -> (a -> IO b) -> IO b ("Bind", pass result to next action).

  • Do-Notation: Syntactic sugar for bind chains.

  • do { x <- p ; q } translates to p >>= \x -> q.

• General Monads:

  • Monad Laws:

  1. p >>= return = p (Right Identity).

  2. return x >>= f = f x (Left Identity).

  3. (p >>= f) >>= g = p >>= (\x -> f x >>= g) (Associativity).

  • Evaluator Example (Modularity):

  • Identity Monad (Value): For simple evaluation.

  • Maybe Monad: For error handling (division by zero results in Nothing).

  • State Monad (ST): To count evaluation steps (States).

  • Combination Monad (STE): Handling both state and exceptions.

Chapter 2: Semantics of Functional Programs

• Approach:

  • Denotational Semantics: Maps each expression to a mathematical object (the "meaning").

  • Operational Semantics: Defines meaning via the steps an abstract machine takes during evaluation.

• Complete Partial Orders (CPOs):

  • Bottom ($\perp$): Represents the "undefined" value or non-terminating calculation.

  • Partial Order ($\sqsubseteq$): Ordered by information content (degree of definition).

  • x \nsqsubseteq y means $x$ is less defined than or equal to $y$.

  • Flat Domains: E.g., $ZZ_{\perp} = \{\perp, 0, 1, -1, ...\}$. Only $\perp$ is below other values.

  • Product Domains: $(d_1, ..., d_n) \sqsubseteq (d'_1, ..., d'_n)$ iff $d_i \sqsubseteq d'_i$ for all $i$.

  • Function Domains: $f \sqsubseteq g$ iff $f(d) \sqsubseteq g(d)$ for all $d$.

  • CPO Requirements:

  1. Smallest element $\perp$ exists.

  2. For every Chain (sequence $d_1 \sqsubseteq d_2 \sqsubseteq ...$), a Least Upper Bound (LUB) $\sqcup S$ exists.

• Monotonicity and Continuity:

  • Monotonic: $d \sqsubseteq d' \implies f(d) \sqsubseteq f(d')$. Essential for computability.

  • Continuous: $f(\sqcup S) = \sqcup f(S)$. Boundary values match limits of approximations.

  • Haskell functions are interpreted as Continuous Functions over CPOs.

• Fixed Point Theory:

  • Recursion is modeled via fixed points. $f = \text{rhs}(f)$.

  • Tarski/Kleene Fixed Point Theorem: In a CPO, a continuous function $f: D \rightarrow D$ has a Least Fixed Point (LFP) defined as:

  • $lfp f = \sqcup \{ f^i(\perp) | i \in \mathbb{N} \}$.

• Domain Construction:

  • Lifting ($D_{\perp}$): Adds a new $\perp$ element below an existing set/domain.

  • Coalesced Sum ($\oplus$): Union of domains sharing the same $\perp$.

Chapter 3: Lambda Calculus ($\Lambda$-Calculus)

• Syntax ($\Lambda$):

  • Constants: $c \in C$.

  • Variables: $x \in V$.

  • Application: $(t_1 t_2)$.

  • Abstraction: $\lambda x. t$.

• Reduction Rules:

  • $\alpha$-Conversion: Renaming bound variables ($\lambda x.x \rightarrow \lambda y.y$).

  • $\beta$-Reduction: Executing function calls ($(\lambda x.t) r \rightarrow t[x/r]$).

  • $\delta$-Reduction: Rules for predefined constants (e.g., $plus\ 1\ 2 \rightarrow 3$).

  • Confluence (Church-Rosser): If a term can be reduced along different paths, those paths eventually converge. This ensures unique normal forms.

• Weak Head Normal Form (WHNF):

  • Evaluation in Haskell stops at WHNF to allow lazy evaluation.

  • A term is in WHNF if it is:

  1. A Lambda abstraction: $\lambda x. t$.

  2. A constructor application: $c\ t_1 ... t_n$.

  3. A variable application: $x\ t_1 ... t_n$.

• Fixed Point Combinators:

  • Used to represent recursion in the "pure" Lambda Calculus.

  • $\Theta$ (Turing Combinator): $\text{fix} = (\lambda xy. y(xxy)) (\lambda xy. y(xxy))$.

  • Property: $\text{fix}\ f \rightarrow f(\text{fix}\ f)$.

Chapter 4: Type Checking and Inference

• Type Schemes:

  • Polymorphic types are quantified: $\forall a. a \rightarrow a$.

  • Shallow Type Schemes: All quantifiers appear at the very beginning of the type.

• Unification:

  • Finding a substitution $\theta$ such that $\tau_1\theta = \tau_2\theta$.

  • Most General Unifier (MGU): The unique simplest unifier for two types.

• Algorithm W (Milner):

  • Input: Type assumption $A$ and Term $t$.

  • Logic:

  • Variables/Constants: Fetch from $A$, instantiate new variables for all quantifiers.

  • Abstraction ($\lambda x. t$): Assume $x::b$ ($b$ new), infer type of $t$, return function type.

  • Application ($t_1 t_2$): Infer types for both, then unify results with a new variable ($mgu(\tau_1, \tau_2 \rightarrow b)$).

• Polymorphic Recursion:

  • Occurs if a recursive function is called with a different type than declared.

  • Requires non-shallow type schemes or explicit type declarations; Haskell's inference often defaults to more specific types if declarations are missing.

• Haskell Implementation Overview:

  • Programs are translated from complex Haskell to simple Haskell, then to Lambda-Calculus terms.

  • The resulting terms are type-checked using Algorithm W before execution via WHNO (Weak Head Normal Order) reduction.

  • Static type checking ensures that no type errors occur at runtime (Safety Property).