Essentials of Programming Languages

Lecture #2

Data Types

Building blocks for data types

• Products
• Sums
• Recursion
• Functions

​

Products

• Origin: cartesian product
• Standard case: pairs
• A x B = { (a, b) | a in A, b in B }
• General case: n-tuples
• A₁ x A₂ x ... x A_n = { (a₁,...,a_n) | a_i in A_i }
• Degenerate case: 0-tuples, the unit type
• * = { () }
• Operations on products
• construction: build a tuple
• elimination: projections / pattern matching
• No write operation on components

​

​

Closely Related: Records

• Records = products with named fields

​

{ f₁ : A₁, ..., f_n : A_n }

• f₁,...,f_n field names
• structs in C and C++ (readonly)
• elimination with record selectors "the dot notation"

​

r.f_i

​

​

Tuples in big-step semantics

e ::= ... | (e, ..., e) | proj n e

Exp = ... | Tuple (List Exp) | Proj Int Exp

Val = ... | VTuple (List Val)

​

eval r (Tuple e*) =

VTuple (eval* r e*) -- evaluate each e in e*

eval r (Proj i e) =

let (VTuple v*) = eval r e in

v* [i] -- i^th element of list

Call-by-name tuples / Lazy tuples

Val' = ... | VTuple r (List Exp)

​

eval' r (Tuple e*) =

VTuple r e*

eval' r (Proj i e) =

let (VTuple r' e*) = eval' r e in

eval' r' (e* [i])

​

​

​

Tuples in Small-step semantics

e ::= ... | (e,...,e) | proj i e

v ::= ... | (v,...,v)

• Reduction rules

introduction: no reduction rules, but context

elimination: reduction rules & context

​

proj i (v₁,..., v_i, ..., v_n) --> v_i

​

S ::= ... | (v₁...,v_i, [ ], e, ...) | proj i [ ]

Sums

• Origin: disjoint union
• Standard case: binary sum
• A + B = { (1,a) | a in A } U { (2,b) | b in B }
• General case
• A₁ + ... + A_n = { (i, a) | a in A_i }
• Degenerate case: nullary sum, empty type
• void (Scala)
• Operations on sums
• introduction: injections, e.g., inl : A -> A+B
• elimination: case distinction

​

​

Closely related: Variants

• Variant = Sum with named alternatives

​

c_i e

​

• c_i is constructor for i^th alternative
• Simple case: enumerations

​

c₁ * + c₂ * + ...

​

​

​

Sums in big-step semantics

e ::= ... | in_i e | case e of ... in_i x => e_i ...

Exp = ... | Inj Int Exp | Case Exp (List Match)

Match = Match Int Ident Exp

Val = ...| VInj Int Val

​

eval r (Inj i e) =

VInj i (eval r e)

eval r (Case e m*) =

let (VInj i v) = eval r e in

let (Match i x e') = m*[i] in

eval (put r x v) e'

Lazy sum

Val' = ... | VInj i Closure

​

eval' r (Inj i e) =

VInj i (Clos r e)

eval' r (Case e m*) =

let (VInj i c) = eval' r e in

let (Match i x e_i) = m*[i] in

-- either evaluate c to v at this point

-- or change the environment to bind variables to closures

eval' (put r x v) e'

​

Encoding of Boolean

Boolean = * + *

false = inr ()

true = inl ()

​

if e1 e2 e3 =

case e1 of | inl() => e2 | inr() => e3

Recursive data structures

• Natural numbers, lists and trees

​

Nat = * + Nat

IntList = * + Int x IntList

BinTree = Int + BinTree x BinTree

​

• With variants

​

Nat = Zero + Succ Nat

IntList = Nil * + Cons (Int x IntList)

BinTree = Leaf Int + Node (BinTree x BinTree)

​

Evaluation of variants

• Introduction: constructor application

​

e ::= ... | c e*

Exp = ... | Con Ident (List Exp)

​

Val = ... | VCon Ident (List Val)

​

eval r (Con c e*) =

VCon c (eval* r e*)

​

Evaluation of variants II

• Elimination: pattern match expression
• Concise notation for case distinction and projection
• Pattern
• Expression consisting of constructors, variables, and wildcards
• Linear: each variable used at most once
• Pattern match expression

e ::= ... | case e of p₁ => e₁ ; ... ; p_n => e_n

p ::= _ | x | c p*

Exp = Case Exp (List (Pat x Exp))

Pat = PWild | PVar Ident | PCon Ident (List Pat)

​

Pattern Matching

• Pattern matching produces a binding from a pattern and a value (or fails)
• Wildcard pattern: matches every value, no binding
• Variable pattern: matches every value and binds variable to value
• Constructor pattern: matched value must start with same constructor, subvalues are matched against the subpatterns, the resulting bindings are combined
• Failure to match a constructor propagates

Pattern Matching II

match : Pat -> Val -> String + Env

match PWild v =

Inr empty

match (PVar x) v =

Inr [ x := v ]

match (PCon c p*) (VCon d v*) | c == d =

let r* = match* p* v* in

combine r* -- merge bindings if disjoint, otherwise fail (linearity)

match _ _ =

Inl "pattern match failure"

Pattern Matching III

• Selecting a matching branch
• sequentially check for matching patterns
• first matching pattern determines the outcome

​

select : List (Pat x Exp) -> Val -> String + Env * Exp

select [] v =

inl "no suitable branch"

select ((p, e) : m*) v =

case (match p v) of

Inl s => select m* v

Inr r => Inr (r, e)

Evaluation of variants III

eval r (Case e m*) =

let v = eval r e in

case (select m* v) of

Inl message =>

error message

Inr (r', e') =>

let r'' = override r r' in

eval r'' e'

Recursive functions

e ::= ... | rec f(x) . e

Exp = ... | Rec Ident Ident Exp

Val = ... | VRec Env Ident Ident Exp

​

eval r (Rec f x e) =

VRec r f x e

eval r (App e1 e2) =

let fv@(VRec r' f x e) = eval r e1 in

let v = eval r e2 in

eval (put (put r' x v) f fv) e

Observations

• recurring problem: by-name / by-value semantics depends on the metalanguage
• many primitives (product, sum, recursion)

​

Looking for a foundational metalanguage

• with as few primitives as possible
• with facilities to fix the evaluation order

Foundation: lambda calculus

• Minimalist programming language
• Syntax

e ::= x | \x.e | e e

​

• Semantics
• traditionally given by a (small-step) reduction relation
• different from previous evaluation-step relations
• Standard Reference: Hendrik P. Barendregt. The Lambda Calculus --- Its Syntax and Semantics. North-Holland. 1984.

​

Free and Bound Variables

​

FV(x) = { x }

FV(\x.e) = FV(e) \ { x }

FV(e1 e2) = FV(e1) U FV(e2)

​

BV(x) = { }

BV(\x.e) = BV(e) U { x }

BV(e1 e2) = BV(e1) U BV(e2)

Semantics of Lambda Calculus

• all rely on capture-avoiding substitution
• alpha conversion

\x.e -alpha-> \y.e[ x:=y ] if y not in FV(e)

​

• beta reduction

(\x.e1) e2 -beta-> e1[ x := e2 ]

​

• eta reduction

(\x.e x) -eta-> e if x not in FV(e)

Semantics of Lambda Calculus II

• difference to evaluation: rules can be applied anywhere in an expression
• more precisely define =R=> by
• if e -R-> e' then e =R=> e'
• if e =R=> e' then C[e] =R=> C[e']
• where contexts C are defined by

​

C ::= [] e | e [] | \x.[]

​

Semantics of Lambda Calculus III

• Let the relation =R=>* be the reflexive transitive closure of =R=>
• e =R=>* e
• e =R=> e' and e' =R=>* e'' implies e =R=>* e''
• Let the relation <=R=> be the symmetric closure of =R=>
• e =R=> e' implies e <=R=> e'
• e' =R=> e implies e <=R=> e'

​

Normal Form

A lambda expression is in (beta) normal form if no reduction applies.

​

e in normal form

if exists no e' such that e =beta=> e'

​

n is a normal form of e

if e =beta=>* n and n is normal form

Normal Form II

There are terms that have no normal form

​

(\x. x x) (\x. x x)

-beta->

(\x. x x) (\x. x x)

​

Theorem (Church-Rosser)

Suppose that e1 <=beta=>* e2.

Then there exists e' such that

e1 =beta=>* e' and

e2 =beta=>* e'

​

Corollary

A lambda expression has at most one normal form.

​

Modeling data types

• Lambda calculus is a calculus of pure functions
• but all standard data types can be modeled
• Booleans and sums
• Products
• Recursion

​

Booleans

• need lambda expressions that simulate true, false, and the conditional
• true = \x.\y.x
• false = \x.\y.y
• cond = \b.\t.\f.b t f

​

cond true e1 e2 = ...

​

Pairs

• need lambda expressions for introducing and eliminating pairs
• pair = \x.\y.\p. p x y
• fst = \p. p (\x.\y. x)
• snd = \p. p (\x.\y. y)

​

fst (pair e1 e2) = ...

Numbers: Church Numerals

• Idea: represent the natural number n by a function that computes n-fold function composition
• zero = \f.\x.x
• succ = \n.\f.\x. f (n x)
• ifzero = \n.\x.\y. n (\z.y) x

​

ifzero (succ n) e1 e2 = ...

Recursion (Fixpoint Theorem)

Every lambda expression has a fixpoint.

That is, for each f there is an e such that

f e <=beta=>* e

Proof (Fixpoint Theorem)

Let e = Y f where

Y = \f . (\x.(f x x)) (\x.(f x x))

​

​

Wrapup

• natural numbers
• pairs and projections
• booleans
• recursion

sufficient to simulate Kleene’s theory of recursive functions,

which in turn is sufficient to simulate Turing machines.

Hence, lambda calculus is a universal computing device (Turing equivalent)

Reduction Strategies

How to find the normal form of an expression?

Normal order reduction

each reduction step chooses the leftmost outermost redex

C ::= \x.e | [ ] e

​

Normalization theorem

If e ==>* n, then e ==>*_no n

Reduction vs. Evaluation

Programming languages

• do not reduce to normal form
• do not evaluate open expressions (with freee variables)

They stop reducing at values

v ::= \x.e

more generally weak head normal forms (that may contain free variables)

Call-by-name and call-by-value

• Different reduction strategies
• Call-by-name evaluation context
• E_n ::= [ ] e
• W_n ::= \x.e | A_n
• A_n ::= x | A_n e
• Call-by-value evaluation context
• E_v ::= [ ] e | v [ ]
• W_v ::= \x.e | A_v
• A_v ::= x | A_v W_v
• Colored parts not relevant for closed expressions

Controlling Evaluation

• Observation: Interpreted language dependent on evaluation strategy of the metalanguage
• How can this be amended?
• Use a different formal system (small-step operational semantics)
• Encode the evaluation strategy in the expression itself ==> transform expression to continuation-passing style

​

Continuation-passing style (CPS)

• Specific syntactic form of lambda expression (programs)
• Interpretation of CPS-expressions does not depend on the evaluation strategy of the metalanguage
• There are transformations from lambda expressions to CPS-expressions that encode an evaluation strategy into the expression

Continuation-Passing Style

Basic idea

• Every function and expression obtains an additional argument, a continuation
• Every function / expression returns its result by passing it to its continuation
• ​

Example (CPS)

• Original Function

fact n =

if n=0 then 1

else n * fact (n-1)

• Transformed Function

factc n k =

if n=0 then k 1

else factc (n-1) (\v. k (n*v))

CPS Interpreter

Scope:

• arithmetic expressions,
• conditional,
• functions (call-by-value)

​

Exp = Var Ident | Lam Ident Exp | App Exp Exp

| Cond Exp Exp Exp | Const Int | Add Exp Exp

Val = VInt Int | VBool Bool | VClos Ident Exp Env

​

The interpreter takes a continuation argument

Cont = Val -> Val

CPS Interpreter II

evalc : Env -> Exp -> Cont -> Val

evalc r (Var x) k =

k (get r x)

evalc r (Lam x e) k =

k (VClos x e r)

evalc r (App e1 e2) k =

evalc r e1 (\v1.

evalc r e2 (\v2.

match v1 with

(VClos x' e' r') =>

evalc (put r' x' v2) e' k))

CPS Interpreter III

evalc r (Cond e1 e2 e3) k =

evalc r e1 (\v1.

match v1 with

VBool b =>

if b then evalc r e2 k

else evalc r e3 k)

​

CPS Interpreter IV

evalc r (Const i) k =

k (VInt i)

evalc r (Add e1 e2) k =

evalc r e1 (\v1.

evalc r e2 (\v2.

match (v1, v2) with

(VInt i1, VInt i2) =>

k (VInt (i1+i2))))

​

Alternative: CPS Transformation

Instead of writing the interpreter in CPS:

• Use the simple interpreter
• Transform the program to CPS
• call-by-value transformation
• call-by-name transformation

​

Call-by-value CPS transformation

CV[[ x ]] = \k. k x

​

CV[[ \x.e ]] = \k. k (\x. CV[[ e ]])

​

CV[[ e1 e2 ]] = \k. CV[[ e1 ]] (\v1.

CV[[ e2 ]] (\v2.

v1 v2 k

​

"Fischer/Plotkin call-by-value CPS transformation"

Properties of Call-by-value CPS

1. Indifference

CV[[ e ]](\x.x) =v=>* w iff

CV[[ e ]](\x.x) =n=>* w'

where w = w'

2. Simulation

e =v=>* \x.e' (using call-by-value evaluation)

iff

CV[[ e ]](\x.x) =v=>* \x. CV[[ e' ]]

Call-by-name CPS transformation

CN[[ x ]] = x

​

CN[[ \x.e ]] = \k. k (\x. CN[[ e ]])

​

CN[[ e1 e2 ]] = \k. CN[[ e1 ]] (\v1.

v1 (CN [[e2]]) k