Programming Languages

(\lambda x. s) t reduces to…

s[t/x] (Substitute t for x inside s)

IfThenElse(tt, s, t) reduces to…

s (The "Then" branch)

IfThenElse(ff, s, t) reduces to…

t (The "Else" branch)

case(lft a, f, g) reduces to…

f a (Apply left handler)

case(rgt b, f, g) reduces to…

g b (Apply right handler)

fold(r, s, []) reduces to…

s (The base case value)

fold(r, s, h@t) reduces to…

r h (fold(r, s, t)) (Recursive step)

Y f (Fixed Point Combinator) reduces to…

f (Y f) (Unrolls recursion once)

fst(s, t) reduces to…

s

snd(s, t) reduces to…

t

Sum Type Syntax

A ⊔ B (Contains either type A or type B)

Constructor for Left Sum

lft(a) (where a is type A)

Constructor for Right Sum

rgt(b) (where b is type B)

Typing Rule: Case Statement

If r: A⊔B, f: A->C, and g: B->C, then case(r,f,g): C

Typing Rule: List Cons (@)

If s: A and t: [A], then s@t : [A]

Typing Rule: List Nil ([])

[] has type [A]

Typing Rule: Fold

If r: A->B->B, s: B, and t: [A], then fold(r,s,t): B

Typing Rule: Fixpoint (Y)

If t: A->A, then Y t : A

Typing Rule: Pairs

If s: A and t: B, then (s, t) : A x B

Typing Rule: Projections

If s: A x B, then fst(s): A and snd(s): B

Typing Rule: Ex Falso

If e: 0 (Empty), then exfalso(e): A (Any type)

Call-by-Value (CBV)

Evaluate arguments before substitution.

Call-by-Name (CBN)

Substitute arguments immediately (un-evaluated).