[SOLVED] 程序代写 G6021 Comparative Programming

G6021 Comparative Programming

G6021 Comparative Programming

Copyright By PowCoder代写加微信 assignmentchef

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 typePart 4 – Types G6021 Comparative Programming 33 / 63Types of polymorphismParametric polymorphism: operates uniformly across differentSubtype polymorphism: operates through an inclusion relation.Ad-hoc polymorphism is another name for overloading and isabout the use of the same name for different functions.Part 4 – Types G6021 Comparative Programming 34 / 63Object-Oriented LanguagesMany modern programming languages are based around theobject model: Java, Eiffel, C++, Smalltalk, Self, etc.Naive understanding: object = (pointer to a) recordBasic features: Object creation, Field selection, Field update, andMethod invocationWe could study an object calculus which allows us to understand thebasic elements of object-oriented programming in the same spirit asthe λ-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 / 63Object Oriented Programmingpublic data: methods (member functions), public variablesprivate data: instance variables, hidden methodsObject-Oriented Program:Send messages to objectsObject-Oriented ProgrammingProgramming methodology: organise concepts into objects andConcepts: encapsulate data, subtyping (extensions ofdata-types), inheritance (reuse of implementation)Part 4 – Types G6021 Comparative Programming 36 / 63Four Basic ConceptsDynamic Lookup – when a message is sent to an object, themethod 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 orAbstraction – implementation details are hidden inside a programunit and exposed via a specific interface. Usually a set of publicmethods 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. Subtypingmeans that the subtype has at least as much functionality as thebase type.Inheritance – reuse definition of one type of object when defininganother object.Part 4 – Types G6021 Comparative Programming 37 / 63Aside: delegation-based languagesIn these languages, objects are defined directly from other objects byadding methods and replacing methods (rather then from classes).Part 4 – Types G6021 Comparative Programming 38 / 63Dynamic LookupA method is selected dynamically (at run time) according to theimplementation of the object that receives the message: Differentobjects may implement the same operation differently.x.add(y) means send the message add(y) to the object x. If x isan integer, then we may perform usual addition; if x is a string, thenconcatenation; 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 / 63Dynamic lookup, continuedIn 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 isthe static type information that dictates which code is used.Dynamic lookup is an important part of Java, C++ and Smalltalk. (It isthe default in Java and Smalltalk, in C++ only virtual member functionsare dynamic).Part 4 – Types G6021 Comparative Programming 40 / 63Abstraction (encapsulation)Programmer has a detailed view of programUser has an abstract viewEncapsulation is a mechanism for separating these two viewsSML has a notion of abstraction:abstype Set withempty : 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代考加微信: assignmentchef QQ: 1823890830 Email: [email protected]