程序代写代做代考 Java data structure Haskell ocaml concurrency compiler Motivation Polymorphism Implementation Parametricity

Motivation Polymorphism Implementation Parametricity
Polymorphism
Christine Rizkallah
CSE, UNSW Term 3 2020
1

Motivation
Polymorphism Implementation Parametricity
Where we’re at
Syntax Foundations 􏰁
Concrete/Abstract Syntax, Ambiguity, HOAS, Binding, Variables, Substitution
Semantics Foundations 􏰁
Static Semantics, Dynamic Semantics (Small-Step/Big-Step), (Assignment 0) Abstract Machines, Environments (Assignment 1)
Features
Algebraic Data Types 􏰁
Polymorphism
Polymorphic Type Inference (Assignment 2) Overloading
Subtyping
Modules
Concurrency
2

Motivation Polymorphism Implementation Parametricity
A Swap Function
Consider the humble swap function in Haskell:
swap :: (t1, t2) → (t2, t1)
swap (a, b) = (b, a)
In our MinHS with algebraic data types from last lecture, we can’t define this function.
3

Motivation Polymorphism Implementation Parametricity
Monomorphic
In MinHS, we’re stuck copy-pasting our function over and over for every different type we want to use it with:
recfun swap1 :: ((Int × Bool) → (Bool × Int)) p = (snd p,fst p)
recfun swap2 :: ((Bool × Int) → (Int × Bool)) p = (snd p,fst p)
recfun swap3 :: ((Bool × Bool) → (Bool × Bool)) p = (snd p,fst p)
···
This is an acceptable state of affairs for some domain-specific languages, but not for general purpose programming.
4

Motivation Polymorphism
Implementation Parametricity
Solutions
We want some way to specify that we don’t care what the types of the tuple elements are.
swap :: (∀a b. (a × b) → (b × a))
This is called parametric polymorphism (or just polymorphism in functional programming circles). In Java and some other languages, this is called generics and polymorphism refers to something else. Don’t be confused.
5

Motivation Polymorphism
Implementation Parametricity
How it works
There are two main components to parametric polymorphism:
1 Type abstraction is the ability to define functions regardless of specific types (like
the swap example before).In MinHS, we will write using type expressions like so: (the literature uses Λ)
swap = type a. type b.
recfun swap :: (a × b) → (b × a) p = (snd p,fst p)
7

Motivation Polymorphism
Implementation
Parametricity
Analogies
The reason they’re called type abstraction and application is that they behave analogously to λ-calculus.
We have a β-reduction principle, but for types:
(type a. e)@τ 􏰀→β (e[a := τ])
Example (Identity Function)
(typea.recfunf ::(a→a)x=x)@Int3
11

Motivation Polymorphism
Implementation
Parametricity
Analogies
The reason they’re called type abstraction and application is that they behave analogously to λ-calculus.
We have a β-reduction principle, but for types:
(type a. e)@τ 􏰀→β (e[a := τ]) Example (Identity Function)
(typea.recfunf ::(a→a)x=x)@Int3 􏰀→ (recfunf ::(Int→Int)x=x)3
12

Motivation Polymorphism
Implementation
Parametricity
Analogies
The reason they’re called type abstraction and application is that they behave analogously to λ-calculus.
We have a β-reduction principle, but for types:
(type a. e)@τ 􏰀→β (e[a := τ]) Example (Identity Function)
(typea.recfunf ::(a→a)x=x)@Int3 􏰀→ (recfunf ::(Int→Int)x=x)3
􏰀→ 3
This means that type expressions can be thought of as functions from types to values.
13

Motivation Polymorphism Implementation Parametricity
What is the type of this?
Type Variables
(typea.recfunf ::(a→a)x=x)
14

Motivation Polymorphism Implementation Parametricity
What is the type of this?
∀a. a → a Types can mention type variables now1.
1Technically, they already could with recursive types.
Type Variables
(typea.recfunf ::(a→a)x=x)
15

Motivation Polymorphism Implementation Parametricity
What is the type of this?
∀a. a → a Types can mention type variables now1.
If id : ∀a.a → a, what is the type of id@Int? 1Technically, they already could with recursive types.
Type Variables
(typea.recfunf ::(a→a)x=x)
16

Motivation Polymorphism Implementation Parametricity
What is the type of this?
Type Variables
(typea.recfunf ::(a→a)x=x)
∀a. a → a
Types can mention type variables now1.
If id : ∀a.a → a, what is the type of id@Int?
(a → a)[a := Int] = (Int → Int) 1Technically, they already could with recursive types.
17

Motivation Polymorphism Implementation Parametricity
Typing Rules Sketch
We would like rules that look something like this:
Γ⊢e:τ
Γ ⊢ type a. e : ∀a. τ
Γ ⊢ e : ∀a. τ
Γ ⊢ e@ρ : τ[a := ρ]
But these rules don’t account for what type variables are available or in scope.
18

Motivation Polymorphism Implementation Parametricity
Type Wellformedness
With variables in the picture, we need to check our types to make sure that they only refer to well-scoped variables.
t bound ∈ ∆
∆⊢t ok ∆⊢Intok ∆⊢Boolok
∆⊢τ1 ok ∆⊢τ2 ok ∆⊢τ1 ok ∆⊢τ2 ok
∆ ⊢ τ1 → τ2 ok
∆, a bound ⊢ τ ok ∆ ⊢ ∀a. τ ok
(etc.)
∆ ⊢ τ1 × τ2 ok
19

Motivation Polymorphism Implementation Parametricity
Typing Rules, Properly
We add a second context of type variables that are bound. a bound, ∆; Γ ⊢ e : τ
∆; Γ ⊢ type a. e : ∀a. τ ∆; Γ ⊢ e : ∀a. τ ∆ ⊢ ρ ok
∆;Γ ⊢ e@ρ : τ[a := ρ] (the other typing rules just pass ∆ through)
20

Motivation Polymorphism Implementation Parametricity
Dynamic Semantics
First we evaluate the LHS of a type application as much as possible:
e 􏰀→M e′ e@τ 􏰀→M e′@τ
21

Motivation Polymorphism Implementation Parametricity
Dynamic Semantics
First we evaluate the LHS of a type application as much as possible:
e 􏰀→M e′ e@τ 􏰀→M e′@τ
Then we apply our β-reduction principle:
(type a. e)@τ 􏰀→M e[a := τ]
22

Motivation Polymorphism Implementation Parametricity
23
Curry-Howard
Previously we noted the correspondence between types and logic:
×∧
+∨ →⇒ 1⊤
0⊥ ∀?

Motivation Polymorphism Implementation Parametricity
24
Curry-Howard
Previously we noted the correspondence between types and logic:
×∧
+∨ →⇒ 1⊤
0⊥ ∀∀

Motivation Polymorphism Implementation Parametricity
Curry-Howard
The type quantifier ∀ corresponds to a universal quantifier ∀, but it is not the same as the ∀ from first-order logic. What’s the difference?
First-order logic quantifiers range over a set of individuals or values, for example the natural numbers:
∀x. x + 1 > x
These quantifiers range over propositions (types) themselves. It is analogous to
second-order logic, not first-order:
∀A. ∀B. A ∧ B ⇒ B ∧ A
∀A. ∀B. A × B → B × A
The first-order quantifier has a type-theoretic analogue too (type indices), but this is not nearly as common as polymorphism.
26

Motivation Polymorphism
Implementation Parametricity
Generality
If we need a function of type Int → Int, a polymorphic function of type ∀a. a → a will do just fine, we can just instantiate the type variable to Int. But the reverse is not true. This gives rise to an ordering.
Generality
A type τ is more general than a type ρ, often written ρ ⊑ τ, if type variables in τ can be instantiated to give the type ρ.
28

Motivation Polymorphism Implementation Parametricity
Implementation Strategies
Our simple dynamic semantics belies a complex implementation headache.
While we can easily define functions that operate uniformly on multiple types, when this is compiled to machine code the results may differ depending on the size of the type in question.
There are two main approaches to solve this problem.
30

Motivation Polymorphism Implementation Parametricity
Template Instantiation
Key Idea
Automatically generate a monomorphic copy of each polymorphic functions based on the types applied to it.
31

Motivation Polymorphism Implementation Parametricity
Template Instantiation
Key Idea
Automatically generate a monomorphic copy of each polymorphic functions based on the types applied to it.
For example, if we defined our polymorphic swap function:
swap = type a. type b.
recfun swap :: (a × b) → (b × a)
p = (snd p,fst p)
Then a type application like swap@Int@Bool would be replaced statically by the
compiler with the monomorphic version:
swapIB = recfun swap :: (Int × Bool) → (Bool × Int) p = (snd p,fst p)
A new copy is made for each unique type application.
33

Motivation Polymorphism Implementation Parametricity
Evaluating Template Instatiation
34

Motivation Polymorphism Implementation Parametricity
Evaluating Template Instatiation
This approach has a number of advantages:
1 Little to no run-time cost
2 Simple mental model
3 Allows for custom specialisations (e.g. list of booleans into bit-vectors)
4 Easy to implement
However the downsides are just as numerous:
1 Large binary size if many instantiations are used
2 This can lead to long compilation times
3 Restricts the type system to statically instantiated type variables.
Languages that use Template Instantiation: Rust, C++, Cogent, some ML dialects
36

Motivation Polymorphism Implementation Parametricity
Polymorphic Recursion
Consider the following Haskell data type:
data Dims a = Step a (Dims [a]) | Epsilon
37

Motivation Polymorphism Implementation Parametricity
Polymorphic Recursion
Consider the following Haskell data type:
data Dims a = Step a (Dims [a]) | Epsilon This describes a list of matrices of increasing dimensionality, e.g:
Step 1 (Step [1, 2] (Step [[1, 2], [3, 4]] Epsilon)) :: Dims Int We can write a sum function like this:
sumDims :: ∀a. (a → Int) → Dims a → Int sumDims f Epsilon = 0
sumDimsf (Stepat)=(f a)+sumDims(sumf)t
39

Motivation Polymorphism
Implementation Parametricity
HM Types
Automatically generating a copy for each instantiation is great but can’t handle all polymorphic programs.
In practice a statically determined subset can be carved out by restricting what sort of programs can be written:
1 Only allow ∀ quantifiers on the outermost part of a type declaration (not inside functions or type constructors).
2 Recursive functions cannot call themselves with different type parameters.
This restriction is sometimes called Hindley-Milner polymorphism. This is also the subset for which type inference is both complete and tractable.
42

Motivation Polymorphism
Implementation Parametricity
Boxing
An alternative to our copy-paste-heavy template instantiation approach is to make all types represented the same way. Thus, a polymorphic function only requires one function in the generated code.
Typically this is done by boxing each type. That is, all data types are represented as a pointer to a data structure on the heap. If everything is a pointer, then all values use exactly 32 (or 64) bits of stack space.
The extra indirection has a run-time penalty, and it can make garbage collection more necessary, but it results in smaller binaries and unrestricted polymorphism. Languages that use boxing: Haskell, Java, C♯, OCaml
45

Motivation Polymorphism Implementation Parametricity
Constraining Implementations
How many possible implementations are there of a function of the following type?
Int → Int
46

Motivation Polymorphism Implementation Parametricity
Constraining Implementations
How many possible implementations are there of a function of the following type?
How about this type?
Int → Int
∀a. a → a
47

Motivation Polymorphism Implementation Parametricity
Constraining Implementations
How many possible implementations are there of a function of the following type?
Int → Int
How about this type?
∀a. a → a Polymorphic type signatures constrain implementations.
48

Motivation Polymorphism Implementation Parametricity
Parametricity
Definition
The principle of parametricity states that the result of polymorphic functions cannot depend on values of an abstracted type.
More formally, suppose I have a polymorphic function g that takes a type parameter. If run any arbitrary function f : τ → τ on some values of type τ, then run the function g@τ on the result, that will give the same results as running g@τ first, then f.
Example
foo :: ∀a. [a] → [a]
49

Motivation Polymorphism Implementation Parametricity
Definition
Parametricity
The principle of parametricity states that the result of polymorphic functions cannot depend on values of an abstracted type.
More formally, suppose I have a polymorphic function g that takes a type parameter. If run any arbitrary function f : τ → τ on some values of type τ, then run the function g@τ on the result, that will give the same results as running g@τ first, then f.
Example
foo :: ∀a. [a] → [a]
We know that every element of the output occurs in the input.
The parametricity theorem we get is, for all f :
foo ◦(map f) = (map f)◦foo
50

Motivation Polymorphism Implementation Parametricity
head :: ∀a. [a] → a What’s the parametricity theorems?
More Examples
51

Motivation Polymorphism Implementation Parametricity
head :: ∀a. [a] → a What’s the parametricity theorems?
More Examples
Example (Answer)
For any f :
f (head l) = head (map f l)
52

Motivation Polymorphism Implementation Parametricity
(++) :: ∀a. [a] → [a] → [a] What’s the parametricity theorem?
More Examples
53

Motivation Polymorphism Implementation Parametricity
(++) :: ∀a. [a] → [a] → [a]
What’s the parametricity theorem?
More Examples
Example (Answer)
mapf (a++b)=mapf a++mapf b
54

Motivation Polymorphism Implementation Parametricity
concat :: ∀a. [[a]] → [a] What’s the parametricity theorem?
More Examples
55

Motivation Polymorphism Implementation Parametricity
concat :: ∀a. [[a]] → [a]
What’s the parametricity theorem?
More Examples
Example (Answer)
map f (concat ls) = concat (map (map f ) ls)
56

Motivation Polymorphism Implementation Parametricity
Higher Order Functions
filter::∀a.(a→Bool) →[a]→[a] What’s the parametricity theorem?
57

Motivation Polymorphism Implementation Parametricity
Higher Order Functions
filter::∀a.(a→Bool) →[a]→[a] What’s the parametricity theorem?
Example (Answer)
filterp(mapf ls)=mapf (filter(p◦f)ls)
58

Motivation Polymorphism Implementation Parametricity
Parametricity Theorems
Follow a similar structure. In fact it can be mechanically derived, using the relational parametricity framework invented by John C. Reynolds, and popularised by Wadler in the famous paper, “Theorems for Free!”2.
Upshot: We can ask lambdabot on the Haskell IRC channel for these theorems.
2https://people.mpi-sws.org/~dreyer/tor/papers/wadler.pdf
59

Related Posts