程序代写代做代考 compiler Haskell algorithm flex concurrency case study C c++ data structure Java G6021 Comparative Programming

G6021 Comparative Programming
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 σ)
􏰀x:σ
􏰀 IfM:τandx:σ,thenλx.M:σ→τ 􏰀 IfM:σ→τandN:σthenMN:τ
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
Modus Ponens:
From
– P implies Q
– and P
We can conclude Q is true
Should be called Implication Elimination – ImpElim but Greeks got there first.
Exercises
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 again.
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
􏰀 foreachtypeσ,condσ :bool→σ→σ→σ,
􏰀 foreachtypeσ,fixσ :(σ→σ)→σ
Exercise: Write these in Haskell.
Part 4 – Types
G6021 Comparative Programming
5/63

Examples
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
fix 􏰄λfint→int.λxint.cond (iszero x) 1􏰂mult x(f(pred x))􏰃􏰅
int→int int 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(iszerox)1(x*f(predx)) F is not recursive! But it does not compute factorial…
Exercise: What are these:
F (\x -> x)
F succ
F pred
Part 4 – Types
G6021 Comparative Programming
7/63

Fixpoints
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:
fix F 3
Part 4 – Types
G6021 Comparative Programming
8/63

Example
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 = false = n = succ = pred = cond = iszero = fix =
λxy.x
λxy.y
λfx.fnx λabc.b(abc) λz.fixHzSIfalse λxyz .xyz
λn.n S I true
(λ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.yfalsex
Part 4 – Types
G6021 Comparative Programming
10/63

Operational Semantics of PCF
(λxσ.M)N → M{x 􏰁→ N}
fixσM → M(fixσM)
condσ trueM N →M
condσ false M N → N
succ n → n + 1
pred(n+1)→n pred0→0
iszero 0 → true iszero (n + 1) → false
Part 4 – Types
G6021 Comparative Programming
11/63

Rules
M → M′ condσMN1N2 → condσM′N1N2
M → M′ succM →succM′
M → M′
iszero M → iszero M′
M → M′ predM →predM′
M → M′ MN → M′N
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:
N → N′ N → N′ MN → MN′ λ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?
SubjectReduction:IfM:σandM→M′ thenM′ :σ If M terminates, then:
􏰀 ifM :intthenM →∗ n
􏰀 ifM :booltheneitherM →∗ trueorM →∗ false
Otherwise: non-terminating (but still preserves the type)
Part 4 – Types
G6021 Comparative Programming
14/63

Summary
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 Haskell
Clean
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
WewriteΓ⊢M :AtomeanthattermM hastypeAusingthecontextΓ
Γ, x : A ⊢ x : A
Γ,x:A⊢M:B Γ⊢M:A→B Γ⊢N:A Γ⊢λx.M :A→B Γ⊢MN :B
Using these rules we can build derivations of typed terms
Part 4 – Types
G6021 Comparative Programming
17/63

Examples
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

Polymorphism
Polymorphism is a mechanism which allows us to write functions which can process objects of different types. It is a very powerful programing technique.
Examples:
len [] = 0
len (_:t) = 1+len t
len :: (Num t1) => [t] -> t1
len [1,2,3] 3
len “G6021” 5
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]
[3,4,5]
map (\x -> “X”) [\x -> x, \x -> x+1]
[“X”,”X”]
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
(GEN )
Γ⊢M :∀α.A
Note: α ̸∈ FV (Γ) for the GEN rule
Γ⊢M :∀α.A
(SPEC )
Γ⊢M :[B/α]A
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?
Machinery
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:
IfU(τ,τ′)=V thenVτ =Vτ′ (wesayV 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,α → β)
D((int → int) → int,α → β)
= ∅
= {(σ,α)}
= {(int,α → β)}
= {(int → int,α)}
Part 4 – Types
G6021 Comparative Programming
26/63

Unification
where
iter(V,τ,τ′)
U(τ,τ′) = iter(id,τ,τ′)
= 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(Γ,letx = M inN)=(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 :: Int Γ ⊢ Q :: Int
Γ ⊢ P&&Q :: Bool Γ ⊢ P + Q :: Int Γ⊢h::a Γ⊢t ::[a]
Γ ⊢ [] :: [a]
Type reconstruction can be extended in a straightforward way.
Question: What about user defined types?
Γ⊢h:t ::[a]
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 :σ
Γ⊢M :τ
Γ ⊢ M : σi Γ ⊢ M : σ ∩ τ System F: types as terms, dependent types, etc.
Part 4 – Types
G6021 Comparative Programming
31/63

Type classes in Haskell
Polymorphic: 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

Subtypes
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 types. 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 Objects: 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 classes 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 pointer. 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 Examples: Dylan Self 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. Example: 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) { ... x.add(y) ... } 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)
where
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

Subtyping
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 Point
Part 4 – Types
G6021 Comparative Programming
45/63

Inheritance
Implementation mechanism
New objects may be defined by reusing implementations of other objects
Example:
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?
Problems:
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
clash. solutions:
􏰀 Implicit resolution: arbitrary way defined by the language
􏰀 Explicit resolution: programmer decides
􏰀 Disallow name clashes: programs are not allowed to contain name
clashes
Exercise: can you give an example of name clashes using a Java-like syntax?
Part 4 – Types
G6021 Comparative Programming
47/63

Case Study: Java
Design Goals
Portability
Reliability
Safety
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: set of classes in a shared namespace
Native method: method written in another language (often C)
Part 4 – Types
G6021 Comparative Programming
50/63

Java Encapsulation
Every field belongs to a class; every class is part of some package
Visibility
Four distinctions: public, private, protected, package Method can refer to:
􏰀 private members of class it belongs to
􏰀 non-private members of all classes in the same package
􏰀 protected members of superclasses (in different packages)
􏰀 public members of classes in visible packages
Part 4 – Types
G6021 Comparative Programming
51/63

Inheritance
Similar to other languages (C++, Smalltalk)
Subclass inherits from superclass: but only single inheritance Some additional features:
􏰀 final classes and methods
􏰀 use of super in constructors (subclass constructor must call the
super constructor – compiler will add it anyway! Note that if the superclass does not have a constructor with same number of arguments, then we get a compilation error!!)
Part 4 – Types
G6021 Comparative Programming
52/63

Class Object
In Java, every class extends another class: superclass is Object if no other class is named.
Class Object has a number of methods:
getClass
toString
equals
hashCode
Clone
wait, notify, notifyAll (used with concurrency) finalize
Part 4 – Types
G6021 Comparative Programming
53/63

Types
Primitive types (not objects): int, bool, etc. Reference types: classes, interfaces, arrays Type conversion:
Casts checked at run-time (may raise Exception)
if A < B and B x then can cast x to A. Subtyping subclass produces subtype; single inheritance implies tree structure of subclasses However, an interface can have multiple subtypes (multiple subtyping) Part 4 - Types G6021 Comparative Programming 54/63 Generic Programming Exercise: Does Java support parametric polymorphism? Class Object is the supertype of all types: allows subtype polymorphism Early versions of Java did not allow templates (parametric polymorphism) Note that we can use Object to write generic data-structures (for instance lists), but what are the problems with this? Part 4 - Types G6021 Comparative Programming 55/63 Templates We write: class Stack { void push(Object o){ ... } Object pop() { ... } ... But would like to write: class Stack {
void push (A a){ … }
A pop() { … }
…
This was considered one of the main shortfalls of Java. Many proposals put forward, but is now “standard”.
Part 4 – Types
G6021 Comparative Programming
56/63