Faith, Evolution, and Programming

Languages
Philip Wadler
University of Edinburgh
Evolution
Multiculturalism
Static vs. Dynamic Typing
Part I. Church: The origins of faith

Part II. Haskell: Type Classes

Part III. Java: Generics

Part IV. Links: Reconciliation

 Part I

Church: The origins of faith

Gerhard Gentzen (1909–1945)
Gerhard Gentzen (1935) — Natural Deduction
Gerhard Gentzen (1935) — Natural Deduction
[A]x
·· A⊃B A
· ⊃-E
B B
⊃-Ix
A⊃B

A B A&B A&B
&-I &-E0 &-E1
A&B A B
Simplifying a proof
[B & A]z [B & A]z
&-E1 &-E0
A B
&-I
A&B [B]y [A]x
⊃-Iz &-I
(B & A) ⊃ (A & B) B&A
⊃-E
A&B
Simplifying a proof
[B & A]z [B & A]z
&-E1 &-E0
A B
&-I y x
A&B [B] [A]
⊃-Iz &-I
(B & A) ⊃ (A & B) B&A
⊃-E
A&B
⇓
[B]y [A]x [B]y [A]x
&-I &-I
B&A B&A
&-E1 &-E0
A B
&-I
A&B
Simplifying a proof
[B & A]z [B & A]z
&-E1 &-E0
A B
&-I y x
A&B [B] [A]
⊃-Iz &-I
(B & A) ⊃ (A & B) B&A
⊃-E
A&B
⇓
[B]y [A]x [B]y [A]x
&-I &-I
B&A B&A
&-E1 &-E0
A B
&-I
A&B
⇓
[A]x [B]y
&-I
A&B
Alonzo Church (1903–1995)
Alonzo Church (1932) — Lambda calculus
Alonzo Church (1940) — Typed λ-calculus
[x : A]x
·· s:A⊃B t:A
· ⊃-E
u:B st : B
⊃-Ix
λx. u : A ⊃ B

t:A u:B s:A&B s:A&B

&-I &-E0 &-E1
ht, ui : A & B s0 : A s1 : B
Simplifying a program
[z : B & A]z [z : B & A]z
&-E1 &-E0
z1 : A z0 : B
&-I y x
hz1 , z0 i : A & B [y : B] [x : A]
⊃-Iz &-I
λz. hz1 , z0 i : (B & A) ⊃ (A & B) hy, xi : B & A
⊃-E
(λz. hz1 , z0 i) hy, xi : A & B
Simplifying a program
[z : B & A]z [z : B & A]z
&-E1 &-E0
z1 : A z0 : B
&-I y x
hz1 , z0 i : A & B [y : B] [x : A]
⊃-Iz &-I
λz. hz1 , z0 i : (B & A) ⊃ (A & B) hy, xi : B & A
⊃-E
(λz. hz1 , z0 i) hy, xi : A & B
⇓
[y : B]y [x : A]x [y : B]y [x : A]x
&-I &-I
hy, xi : B & A hy, xi : B & A
&-E1 &-E0
hy, xi1 : A hy, xi0 : B
&-I
hhy, xi1 , hy, xi0 i : A & B
Simplifying a program
[z : B & A]z [z : B & A]z
&-E1 &-E0
z1 : A z0 : B
&-I y x
hz1 , z0 i : A & B [y : B] [x : A]
⊃-Iz &-I
λz. hz1 , z0 i : (B & A) ⊃ (A & B) hy, xi : B & A
⊃-E
(λz. hz1 , z0 i) hy, xi : A & B
⇓
[y : B]y [x : A]x [y : B]y [x : A]x
&-I &-I
hy, xi : B & A hy, xi : B & A
&-E1 &-E0
hy, xi1 : A hy, xi0 : B
&-I
hhy, xi1 , hy, xi0 i : A & B
⇓
[x : A]x [y : B]y
&-I
hx, yi : A & B
William Howard (1980) — Curry-Howard Isomorphism
Curry-Howard

Hindley-Milner

Girard-Reynolds
 Part II

Haskell: Type Classes

Type classes
class Ord a where
(<) :: a -> a -> Bool

instance Ord Int where

(<) = primitiveLessInt

instance Ord Char where

(<) = primitiveLessChar

max :: (Ord a) => a -> a -> a

max x y = if x < y then y else x

maximum :: (Ord a) => [a] -> a

maximum [x] = x
maximum (x:xs) = max x (maximum xs)

test :: Bool
test = maximum [0,1,2] == 2 &&
maximum "abc" == ’c’
Translation
data Ord a = Ord { less :: a -> a -> Bool }

ordInt :: Ord Int

ordInt = Ord { less = primitiveLessInt }

ordChar :: Ord Char

ordChar = Ord { less = primitiveLessChar }

max :: Ord a -> a -> a -> a

max d x y = if less d x y then y else x

maximum :: Ord a -> [a] -> a

maximum d [x] = x
maximum d (x:xs) = max d x (maximum d xs)

test :: Bool
test = maximum ordInt [0,1,2] == 2 &&
maximum ordChar "abc" == ’c’
Type classes, continued
instance Ord a => Ord [a] where
[] < [] = False
[] < y:ys = True
x:xs < [] = False
x:xs < y:ys | x < y = True
| y < x = False
| otherwise = xs < ys

test’ :: Bool
test’ = maximum ["zero","one","two"] == "zero" &&
maximum [[[0],[1]],[[0,1]]] == [[0,1]]
Translation, continued
ordList :: Ord a -> Ord [a]
ordList d = Ord { less = lt }
where
lt d [] [] = False
lt d [] (y:ys) = True
lt d (x:xs) [] = False
lt d (x:xs) (y:ys) | x < y = True
| y < x = False
| otherwise = lt d xs ys

test’ :: Bool
test’ = maximum d0 ["zero","one","two"] == "zero" &&
maximum d1 [[[0],[1]],[[0,1]]] == [[0,1]]
where
d0 = ordList ordChar
d1 = ordList (ordList ordInt)
 Part III

Java: Generics
Java generics
Lists in Java 4.0 and Java 5.0

in Java 4.0 in Java 5.0

integer list List List<Integer>

string list List List<String>

string list list List List<List<String>>

Lists in Java 4.0 and Java 5.0

in Java 4.0 in Java 5.0

integer list List List<Integer>

string list List List<String>

string list list List List<List<String>>

Lists in Java 4.0 and Java 5.0

in Java 4.0 in Java 5.0

integer list List List<Integer>

string list List List<String>

string list list List List<List<String>>

Lists in Java 4.0 and Java 5.0

in Java 4.0 in Java 5.0

integer list List List<Integer>

string list List List<String>

string list list List List<List<String>>

Lists in Java 4.0 and Java 5.0

in Java 4.0 in Java 5.0

integer list List List<Integer>

string list List List<String>

string list list List List<List<String>>

Legacy library with legacy client
class Stack {
private List list;
public Stack() { list = new ArrayList(); }
public boolean empty() { return list.size() == 0; }
public void push(Object elt) { list.add(elt); }
public Object pop() {
Object elt = list.remove(list.size()-1);
return elt;
}
}

class Client {
public static void main(String[] args) {
Stack stack = new Stack();
stack.push(new Integer(42));
int top = ((Integer)stack.pop()).intValue();
assert top == 42;
}
}
Generic library with generic client
class Stack<E> {
private List<E> list;
public Stack() { list = new ArrayList<E>(); }
public boolean empty() { return list.size() == 0; }
public void push(E elt) { list.add(elt); }
public E pop() {
E elt = list.remove(list.size()-1);
return elt;
}
}

class Client {
public static void main(String[] args) {
Stack<Integer> stack = new Stack<Integer>();
stack.push(42);
int top = stack.pop();
assert top == 42;
}
}
Generic library with legacy client
class Stack<E> {
private List<E> list;
public Stack() { list = new ArrayList<E>(); }
public boolean empty() { return list.size() == 0; }
public void push(E elt) { list.add(elt); }
public E pop() {
E elt = list.remove(list.size()-1);
return elt;
}
}

class Client {
public static void main(String[] args) {
Stack stack = new Stack(); // raw type
stack.push(new Integer(42));
int top = ((Integer)stack.pop()).intValue();
assert top == 42;
}
}
Legacy library with generic client—minimal changes
class Stack<E> {
private List list; // raw type
public Stack() { list = new ArrayList(); }
public boolean empty() { return list.size() == 0; }
public void push(E elt) { list.add(elt); }
public E pop() {
Object elt = list.remove(list.size()-1);
return (E)elt; // unchecked cast
}
}

class Client {
public static void main(String[] args) {
Stack<Integer> stack = new Stack<Integer>();
stack.push(42);
int top = stack.pop();
assert top == 42;
}
}
Legacy library with generic client—stubs
class Stack<E> {
public Stack() { throw new StubException(); }
public boolean empty() { throw new StubException(); }
public void push(E elt) { throw new StubException(); }
public E pop() { throw new StubException(); }
}

class Client {
public static void main(String[] args) {
Stack<Integer> stack = new Stack<Integer>();
stack.push(42);
int top = stack.pop();
assert top == 42;
}
}

// compile with stub library, execute with legacy library

% javac -classpath stubs Client.java
% java -ea -classpath legacy Client
Comparison
interface Comparable<T> {
public int compareTo(T o);
}

Integer int0 = 0;
Integer int1 = 1;
assert int0.compareTo(int1) < 0;

String str0 = "zero";

String str1 = "one";
assert str0.compareTo(str1) > 0;

Number num0 = 0;
Number num1 = 1.0;
assert num0.compareTo(num1) < 0; // compile-time error
Maximum of a list
public static <T extends Comparable<T>>
T max(List<T> elts)
{
T candidate = elts.get(0);
for (T elt : elts) {
if (candidate.compareTo(elt) < 0) candidate = elt;
}
return candidate;
}

List<Integer> ints = Arrays.asList(0,1,2);

assert max(ints) == 2;

List<String> strs = Arrays.asList("zero","one","two");

assert max(strs).equals("zero");

List<Number> nums = Arrays.asList(0,1,2,3.14);

assert max(nums) == 3.14; // compile-time error
A fruity example
Permit comparison of apples with oranges
class Fruit implements Comparable<Fruit> {
... }
class Apple extends Fruit {
... }
class Orange extends Fruit {
... }

Prohibit comparison of apples with oranges

class Fruit {
... }
class Apple extends Fruit implements Comparable<Apple> {
... }
class Orange extends Fruit implements Comparable<Orange> {
... }
Comparing lists
class ComparableList<E extends Comparable<E>>
extends ArrayList<E> implements Comparable<List<E>>
{
public ComparableList(Iterable<E> list) {super(list)}
public int compareTo(List<E> that) {
int n1 = this.size();
int n2 = that.size();
for (int i = 0; i < Math.min(n1,n2); i++) {
int k = list1.get(i).compareTo(list2.get(i));
if (k != 0) return k;
}
return (n1 < n2) ? -1 : (n1 == n2) ? 0 : 1;
}
}

Cumbersome to use—probably better to use comparators

Maximum of a list of lists of lists of integers
ComparableList<ComparableList<Integer>> xss =
new ComparableList<ComparableList<Integer>>{{
add(new ComparableList<Integer>{{add(0)}});
add(new ComparableList<Integer>{{add(1)}});}};
ComparableList<ComparableList<Integer>> yss =
new ComparableList<ComparableList<Integer>>{{
add(new ComparableList<Integer>{{add(0);add(1);}})}};
List<ComparableList<ComparableList<Integer>>> xsss =
new List<ComparableList<ComparableList<Integer>>>{{
add(xss); add(yss);}};
assert max(xsss).equals(yss);
 Part IV

Links: Reconciliation
Links: Web Programming without Tiers

Browser
(HTML,XML,JavaScript)
6
form response
?
Server
(Java,Perl,PHP,Python)
6
query response
?
Database
(SQL,XQuery)
Links: Web Programming without Tiers

Browser
(Links)
6
call return
?
Server
(Links)
6
call return
?
Database
(Links)
 Hope — Burstall, MacQueen, and Sannella (1980)

Links — Cooper, Lindley, Wadler, and Yallop (2007)

Type classes, revisited
(+) :: Num a => a -> a -> a
1 :: Num a => a
2 :: Num a => a

1 + 1 == 2 :: Num a => Bool

-- ambiguous!

read :: Read a => String -> a

show :: Show a => a -> String

show . read :: (Read a, Show a) => String -> String

-- ambiguous!
Type classes, revisited
(+) :: Num a => a -> a -> a
1 :: Int
2 :: Int

1 + 1 == 2 :: Bool
-- unambiguous!

readInt :: String -> Int

show :: Show a => a -> String

show . readInt :: String -> String

-- unambiguous!
Static vs. Dynamic Typing
Multiculturalism
Evolution
Faith, Evolution, and Programming
Languages
Philip Wadler
University of Edinburgh