G6021 Comparative Programming
G6021 Comparative Programming
Copyright By PowCoder代写 加微信 powcoder
Part 4 – Types
Part 4 – Types G6021 Comparative Programming 1 / 63
Typed λ-calculus
There are many variants of the λ-calculus (applied λ-calculi).
Here we briefly outline the simply typed λ-calculus;
and a minimal functional programming language.
Definition:
Types: type variables: σ, τ ,… and function types: σ → τ
Typed terms: terms will now be annotated with types, which we
write as: t : σ (term t has type σ)
▶ If M : τ and x : σ, then λx .M : σ → τ
▶ If M : σ → τ and N : σ then MN : τ
Does this look familiar?
Exercise: What are the differences between “pure” and “typed”
λ-calculi?
Part 4 – Types G6021 Comparative Programming 2 / 63
Programming Concepts: week 10
Using Implications
– P implies Q
We can conclude
Should be called Implication Elimination – ImpElim
but Greeks got there first.
1 P implies (Q implies R) ⊢ (P and Q) implies R
2 (P and Q) implies R ⊢ P implies (Q implies R)
Part 4 – Types G6021 Comparative Programming 3 / 63
Properties
Can every λ-term be given a type?
Strong Normalisation?
Confluence?
Exercise (for “fun”)
Consider the linear λ-calculus: each variable can occur exactly once:
i.e. λx .x is linear, but λx .xx is not. Now answer the above questions
Part 4 – Types G6021 Comparative Programming 4 / 63
Extending the λ-calculus (PCF)
PCF: Programming language for Computable Functions.
A very simple functional programming language derived from the
λ-calculus:
Types: σ, τ ::= int | bool | σ → τ
Typed terms: Same as the typed λ-calculus, with the addition of
constants:
▶ n : int for n = 0,1,2, . . .
▶ true, false : bool
▶ succ,pred : int → int
▶ iszero : int → bool
▶ for each type σ, condσ : bool → σ → σ → σ,
▶ for each type σ, fixσ : (σ → σ) → σ
Exercise: Write these in Haskell.
Part 4 – Types G6021 Comparative Programming 5 / 63
succ 3 : int
condint(iszero(pred(pred 2)))1 : int → int
and factorial
f x = if x==0 then 1 else x * f(x-1)
which we can code as
fixint→int
λf int→int.λxint.condint(iszero x) 1
mult x(f (pred x))
Exercise: Define mult.
Part 4 – Types G6021 Comparative Programming 6 / 63
Where did that come from?
Here are several snap-shots of the transformation from Haskell to PCF:
f x = if x==0 then 1 else x*f(x-1)
f = \x -> if x==0 then 1 else x*f(x-1)
f = \x -> cond (x==0) 1 (x*f(x-1))
f = \x -> cond (iszero x) 1 (x*f(pred x))
What next? PCF does not have recursion…. Abstract that out:
F = \f -> \x -> cond (iszero x) 1 (x * f(pred x))
F is not recursive! But it does not compute factorial…
Exercise: What are these:
F (\x -> x)
Part 4 – Types G6021 Comparative Programming 7 / 63
F = \f -> \x -> cond (iszero x) 1 (x*f(pred x))
None of the above give the factorial function. What we need is a
function fact, because:
F fact = fact
We don’t have such a function… But we do have a way of finding it!
What we need is the fixpoint of F, which we write as fix F.
fact = fix F
So to compute the factorial of a number, say 3, we write:
Part 4 – Types G6021 Comparative Programming 8 / 63
Here are some snap-shots of the reduction of fix F 3 to
demonstrate how the computation works:
fix F 3 -> F (fix F) 3
-> (\x -> cond (iszero x) 1 (x*(fix F (pred x)))) 3
-> cond (iszero 3) 1 (3*(fix F (pred 3)))
-> cond False 1 (3*(fix F 2))
-> 3*(fix F 2)
Part 4 – Types G6021 Comparative Programming 9 / 63
What’s New?
true = λxy .x
false = λxy .y
n = λfx .f nx
succ = λabc.b(abc)
pred = λz.fix H z S I false
cond = λxyz.xyz
iszero = λn.n S I true
fix = (λxy .y(xxy))(λxy .y(xxy))
where I = λx .x , H and S are defined as:
H = λhx .iszero x 0 (succ(h(x false)))
S = λxy .y false x
Part 4 – Types G6021 Comparative Programming 10 / 63
Operational Semantics of PCF
(λxσ.M)N → M{x 7→ N}
fixσM → M(fixσM)
condσ true M N → M
condσ false M N → N
succ n → n + 1
pred (n + 1) → n pred 0 → 0
iszero 0 → true iszero (n + 1) → false
Part 4 – Types G6021 Comparative Programming 11 / 63
condσMN1N2 → condσM ′N1N2
succ M → succ M ′
pred M → pred M ′
iszero M → iszero M ′
Remark that:
The configurations are just terms.
Computation = evaluation = reduction:
M → N means M reduces (evaluates) to N.
A final value is an irreducible (fully evaluated) term.
Part 4 – Types G6021 Comparative Programming 12 / 63
Observations
Note that we do not have “reductions in every context”. Specifically, we
do not have:
λx .N → λx .N ′
Strategies
Which strategy is being used here?
How can we change it to another strategy?
Part 4 – Types G6021 Comparative Programming 13 / 63
Properties
Termination?
Subject Reduction: If M : σ and M → M ′ then M ′ : σ
If M terminates, then:
▶ if M : int then M →∗ n
▶ if M : bool then either M →∗ true or M →∗ false
Otherwise: non-terminating (but still preserves the type)
Part 4 – Types G6021 Comparative Programming 14 / 63
1 λ-calculus (pure, typed)
2 PCF: simple functional language
These languages are very primitive (as far as the programmer is
concerned)
However, they provide the basis of the functional paradigm
Many languages based on this:
Standard ML, CAML
Lisp, Scheme, . . .
Part 4 – Types G6021 Comparative Programming 15 / 63
Type systems and Type Reconstruction
Type systems have become one of the most important theoretical
developments in programming languages
Here we will examine several key issues:
Type reconstruction (and unification)
Polymorphic types
Overloading
Intersection types
(System F)
Part 4 – Types G6021 Comparative Programming 16 / 63
Proof Systems
We write Γ ⊢ M : A to mean that term M has type A using the context Γ
Γ, x : A ⊢ x : A
Γ, x : A ⊢ M : B
Γ ⊢ λx .M : A → B
Γ ⊢ M : A → B Γ ⊢ N : A
Γ ⊢ MN : B
Using these rules we can build derivations of typed terms
Part 4 – Types G6021 Comparative Programming 17 / 63
x : A ⊢ x : A
⊢ λx .x : A → A
x : A, y : B ⊢ x : A
x : A ⊢ λy .x : B → A
⊢ λx .λy .x : A → B → A
f : A → B, x : A ⊢ f : A → B f : A → B, x : A ⊢ x : A
f : A → B, x : A ⊢ fx : B
f : A → B ⊢ λx .fx : A → B
⊢ λf .λx .fx : (A → B) → A → B
Part 4 – Types G6021 Comparative Programming 18 / 63
Type Reconstruction
Given a term M, can we find its type?
The proof system suggests an algorithm:
If M is a variable, then look up the type in the context
If M = λx .M ′ is an abstraction, find the type of M ′ in the context
extended with x : A, then calculate the type of the result
If M is an application, find the type of the function, then the
argument, then calculate the type of the result
But how do we make the types fit?
E.g. M : A → B and N : C. Can we give a type for MN?
(Can we make A and C the “same” type?)
Part 4 – Types G6021 Comparative Programming 19 / 63
Polymorphism
A second question: can a term (program) have several types?
Example: P = λx .1 : A → int
Are both P true and P 3 possible?
It seems reasonable, but at what moment does type A become either
bool or int?
Part 4 – Types G6021 Comparative Programming 20 / 63
is a mechanism which allows us to write functions
which can process objects of different types. It is a very powerful
programing technique.
len [] = 0
len (_:t) = 1+len t
len :: (Num t1) => [t] -> t1
len [1,2,3]
len “G6021”
Part 4 – Types G6021 Comparative Programming 21 / 63
Another Example
map f [] = []
map f (h:t) = (f h): map f t
map :: (a -> b) -> [a] -> [b]
map (\x -> x+1) [2,3,4]
map (\x -> “X”) [\x -> x, \x -> x+1]
t, t1, a, b are type variables
len :: [t] -> Int means that len has type ∀t .[t ] → Int.
I.e. forall types t .
t is called a generic type
Part 4 – Types G6021 Comparative Programming 22 / 63
Generalisation and Specialisation
The final machinery that we need are ways of introducing (and
eliminating) the ∀.
Γ ⊢ M : ∀α.A
Γ ⊢ M : ∀α.A
Γ ⊢ M : [B/α]A
Note: α ̸∈ FV (Γ) for the GEN rule
Part 4 – Types G6021 Comparative Programming 23 / 63
Reconstructing Polymorphic types
We give an algorithm which will find “the most general type” of a term
If M has a type, then we will find it, otherwise fail
Exercise: what could “most general type” mean?
Substitution (of types)
Unification
Type reconstruction
Part 4 – Types G6021 Comparative Programming 24 / 63
Unification
There is an algorithm U , which given a pair of types either returns a
substitution V or fails; further:
If U(τ, τ ′) = V then V τ = V τ ′ (we say V unifies τ and τ ′).
If S unifies τ and τ ′ then U(τ, τ ′) returns some V and there is
another substitution R such that S = RV (most general unifier).
Moreover, V only involves variables in τ and τ ′. Example:
U(α → α, (β → β) → β → β) = [β → β/α]
Part 4 – Types G6021 Comparative Programming 25 / 63
Disagreement sets
The algorithm for unification is specified in terms of the notion of a
disagreement set. When unifying pairs of types we will have a
disagreement set that is either empty or cardinality 1.
D(τ, τ ′) = ∅ (if τ = τ ′)
= {(σ, σ′)}
where σ, σ′ are the first two subterms at which τ, τ ′ disagree, using
depth first comparison. Some examples are in order:
D(α → β, α → β) = ∅
D(σ → τ, α → β) = {(σ, α)}
D(int, α → β) = {(int, α → β)}
D((int → int) → int, α → β) = {(int → int, α)}
Part 4 – Types G6021 Comparative Programming 26 / 63
Unification
U(τ, τ ′) = iter(id, τ, τ ′)
iter(V , τ, τ ′) = V , if V τ = V τ ′
= iter([b/a]V , τ, τ ′), if a does not occur in b
= iter([a/b]V , τ, τ ′), if b does not occur in a
= FAIL, otherwise.
where {(a,b)} = D(V τ,V τ ′).
Part 4 – Types G6021 Comparative Programming 27 / 63
Reconstruction of Types
Using unification, and the proof system as a guide, the algorithm is a
function which takes a set of assumptions (Γ) and a term to be typed
(e), and returns two things: a substitution (T ) and the type of the
whole term (τ): T (Γ,e) = (T , τ)
1 T (Γ, x) = (id, τ) where τ = [β1/α1, . . . βn/αn]σ if
x : ∀α1 . . . ∀αn.σ ∈ Γ. Otherwise, τ = Γx
2 T (Γ,MN) = (USR,Uβ) where (R, ρ) = T (Γ,M),
(S, σ) = T (RΓ,N) and U = U(Sρ, σ → β) (β new)
3 T (Γ, λx .M) = (R,Rβ → τ) where (R, ρ) = T (Γ ∪ x : β,M) (β new)
4 T (Γ, let x = M in N) = (SR, τ) where (R, σ) = T (Γ,M),
(S, τ) = T (RΓ ∪ x : σ′,N), σ′ = ∀α1 . . . ∀αn.σ and
{α1, . . . , αn} = FV (σ)− FV (Γ)
Part 4 – Types G6021 Comparative Programming 28 / 63
Reconstruction of types in functional languages
We can add a number of extra rules for the built-in types. For example,
something like this:
Γ ⊢ n :: Integer Γ ⊢ True :: Bool Γ ⊢ False :: Bool
Γ ⊢ P :: Bool Γ ⊢ Q :: Bool
Γ ⊢ P&&Q :: Bool
Γ ⊢ P :: Int Γ ⊢ Q :: Int
Γ ⊢ P + Q :: Int
Γ ⊢ [] :: [a]
Γ ⊢ h :: a Γ ⊢ t :: [a]
Γ ⊢ h : t :: [a]
Type reconstruction can be extended in a straightforward way.
Question: What about user defined types?
Part 4 – Types G6021 Comparative Programming 29 / 63
Type checking versus type inference
Type checking refers to the process of checking that the types
declared in a program are compatible with the use of the functions
and variables.
Type inference (or type reconstruction) is the process of inferring
types for the elements of the program (where type declarations
might be present, optionally).
Part 4 – Types G6021 Comparative Programming 30 / 63
Other notions of type
Overloading: 1 + 4, 1.2 + 3.7,
“this ” + ” is a ” + “string”
Also known as ad hoc polymorphism.
Intersection types
Γ ⊢ M : (σ1 ∩ σ2)
Γ ⊢ M : σi
Γ ⊢ M : σ Γ ⊢ M : τ
Γ ⊢ M : σ ∩ τ
System F: types as terms, dependent types, etc.
Part 4 – Types G6021 Comparative Programming 31 / 63
Type classes in : same code executed
Overloaded: different code executed
Haskell has an intermediate notion: type classes:
len :: (Num t1) => [t] -> t1
▶ Num is a typeclass: all things like numbers. So, len takes a list of
anything (really anything) and produces a number of some kind (but
might be Int, Integer, etc.). Saying that the type is in this class
groups all these functions together.
▶ Another example: Eq class defines equality (==) and inequality (/=).
All the basic datatypes exported by the Prelude are instances of
Eq, and Eq may be derived for any datatype whose constituents are
also instances of Eq.
Not to be confused with classes in Java.
Part 4 – Types G6021 Comparative Programming 32 / 63
A < A (reflexivity)
A < B and B < C then A < C (transitivity)
a : A and A < B then a : B (subsumption)
We also add a “top” type ⊤, which is above everything else: A < ⊤
Can you give examples of these from Java?
Objects: A larger type is a subtype of a smaller type
Part 4 - Types G6021 Comparative Programming 33 / 63
Types of polymorphism
Parametric polymorphism: operates uniformly across different
Subtype polymorphism: operates through an inclusion relation.
Ad-hoc polymorphism is another name for overloading and is
about the use of the same name for different functions.
Part 4 - Types G6021 Comparative Programming 34 / 63
Object-Oriented Languages
Many modern programming languages are based around the
object model: Java, Eiffel, C++, Smalltalk, Self, etc.
Naive understanding: object = (pointer to a) record
Basic features: Object creation, Field selection, Field update, and
Method invocation
We could study an object calculus which allows us to understand the
basic elements of object-oriented programming in the same spirit as
the λ-calculus for functional programming.
However, we want to focus now on comparing the paradigms.
Question: Functions vs. objects?
Part 4 - Types G6021 Comparative Programming 35 / 63
Object Oriented Programming
public data: methods (member functions), public variables
private data: instance variables, hidden methods
Object-Oriented Program:
Send messages to objects
Object-Oriented Programming
Programming methodology: organise concepts into objects and
Concepts: encapsulate data, subtyping (extensions of
data-types), inheritance (reuse of implementation)
Part 4 - Types G6021 Comparative Programming 36 / 63
Four Basic Concepts
Dynamic Lookup - when a message is sent to an object, the
method executed is determined by the object implementation.
Different objects can respond differently to the same message.
The response is not based on the static property of the variable or
Abstraction - implementation details are hidden inside a program
unit and exposed via a specific interface. Usually a set of public
methods manipulate private data.
Subtyping - if object A has all the functionality of another object B,
we can use A in place of B in contexts expecting A. Subtyping
means that the subtype has at least as much functionality as the
base type.
Inheritance - reuse definition of one type of object when defining
another object.
Part 4 - Types G6021 Comparative Programming 37 / 63
Aside: delegation-based languages
In these languages, objects are defined directly from other objects by
adding methods and replacing methods (rather then from classes).
Part 4 - Types G6021 Comparative Programming 38 / 63
Dynamic Lookup
A method is selected dynamically (at run time) according to the
implementation of the object that receives the message: Different
objects may implement the same operation differently.
x.add(y) means send the message add(y) to the object x. If x is
an integer, then we may perform usual addition; if x is a string, then
concatenation; if x is a set, then we add the element y to the set, etc.
etc. Thus:
while(c) {
may perform a different operation each time we enter the loop.
Part 4 - Types G6021 Comparative Programming 39 / 63
Dynamic lookup, continued
In functional languages, x.add(y) would be written as add(x,y):
the meaning of the operation stays the same.
Exercise: does dynamic lookup = overloading ?
Answer: To some extent: however, overloading is a static concept: it is
the static type information that dictates which code is used.
Dynamic lookup is an important part of Java, C++ and Smalltalk. (It is
the default in Java and Smalltalk, in C++ only virtual member functions
are dynamic).
Part 4 - Types G6021 Comparative Programming 40 / 63
Abstraction (encapsulation)
Programmer has a detailed view of program
User has an abstract view
Encapsulation is a mechanism for separating these two views
SML has a notion of abstraction:
abstype Set with
empty : unit -> Set
isEmpty : Set -> boolean
add : int * Set -> Set
union : Set * Set -> Set
is … (* detailed implementation *)
in … (* program *) end
Part 4 – Types G6021 Comparative Programming 41 / 63
Abstraction (Haskell example)
module Stack (Stack,empty,isEmpty,push,top,pop)
empty :: Stack a
isEmpty :: Stack a -> Bool
push :: a -> Stack a -> Stack a
top :: Stack a -> a
pop :: Stack a -> (a,Stack a)
newtype Stack a = StackImpl [a]
empty = StackImpl []
isEmpty (StackImpl s) = null s
push x (StackImpl s) = StackImpl (x:s)
top (StackImpl s) = head s
pop (StackImpl (s:ss)) = (s,StackImpl ss)
Part 4 – Types G6021 Comparative Programming 42 / 63
Encapsulation
Guarantee invariants of data structure: only functions of the data
type have access to the internal representation of the data
Limited Reuse: cannot reuse code
Exercise: What is the essential difference between functional style
abstraction and OO abstraction?
Object-oriented languages allow encapsulation in an extensible form.
Part 4 – Types G6021 Comparative Programming 43 / 63
Subtyping and Inheritance
Interface: The external view of an object; messages accepted by
an object; the type
Subtyping: relation between interfaces
Implementation: internal representation of an object
Inheritance: relation between implementations
Part 4 – Types G6021 Comparative Programming 44 / 63
interface Point: x, y, move
interface ColouredPoint: x, y, move, colour, changeColour.
If interface A contains all of interface B, then A objects can also be
used as B objects.
ColouredPoint interface contains Point: ColouredPoint is a subtype of
Part 4 – Types G6021 Comparative Programming 45 / 63
Inheritance
Implementation mechanism
New objects may be defined by reusing implementations of other
class Point
float x,y; Point move(float dx, dy)
class ColouredPoint
float x,y; colour c; Point move(float dx, dy)
Point changeColour(colour newc)
Subtyping: ColouredPoints can be used in place of Points:
property used by the client
Inheritance: ColouredPoints can be implemented by reusing the
implementation of Point: property used by the programmer
Part 4 – Types G6021 Comparative Programming 46 / 63
Multiple Inheritance
A controversial aspect of Object-oriented programming
Should we be allowed to build a class by inheriting from more than
one base class?
Name clashes: if class C inherits from classes A and B, where A
and B have members of the same name, then we have a name
solutions:
▶ Implicit resolution: arbitrary way defined by the language
▶ Explicit resolution: programmer decides
▶ Disallow name clashes: programs are not allowed to contain name
Exercise: can you give an example of name clashes using a Java-like
Part 4 – Types G6021 Comparative Programming 47 / 63
Case Study: Java
Design Goals
Portability
Reliability
Simplicity
Efficient (secondary)
Almost everything in Java is an object; Does not allow multiple
inheritance; statically typed.
Part 4 – Types G6021 Comparative Programming 48 / 63
Java Classes and Objects
Syntax similar to C++
Objects: fields, methods
Dynamic lookup: similar behaviour to other languages, static
typing (more efficient than some other languages, e.g. Smalltalk)
Dynamic linking (slower than C++)
Part 4 – Types G6021 Comparative Programming 49 / 63
Terminology
Class, Object (as usual)
Field: data member
Method: data function
Static members: class fields and methods
this: self
Package: se
程序代写 CS代考 加微信: powcoder QQ: 1823890830 Email: powcoder@163.com