Presented by Pinglei Guo for UCSC CMPS253 on 11/07/2017
NOTE: the title and order of some sections are modfied to emphasize specific content
We use a more Java-style pseudo code instead of lambda-calculus to have named function and multi arguments
The style we should use
(* NOTE: from [2], rewrite in a mix of OCaml and lambda-calculus, won't compile *)
let sphere = {center={x=1, y=2, z=3}, radius=2} in
let circle = sphere in
(lambda c:{center: {x: Nat, y:Nat}, radius: Nat}. c.center={x=0, y=0}) circle
sphere.center.z
The style we actually use (similar to [2])
/* {center: {x:Nat, y:Nat}, radius: Nat} -> Unit */
function move_to_origin(c: {center: {x:Nat, y:Nat}, radius: Nat}) : Unit {
c.center = {x=0, y=0}
}
var sphere = {center={x=1, y=2, z=3}, radius=2}
move_to_origin(sphere)
sphere.center.z
Recall the typing rule for function application
$$\frac{\Gamma \vdash t_1 : T_{11} \rightarrow T_{12} \quad \Gamma \vdash t_2 : T_{11}}{\Gamma \vdash t_1 \ t_2 : T_{12}} \quad\quad \textbf{(T-APP)}$$This is a well typed term
$$(\lambda \text{r:{x:Nat}. r.x) {x=0}}$$This is not typable, but it looks reasonable
$$(\lambda \text{r:{x:Nat}. r.x) {x=0,y=1}}$$However, passing {x=0,y=1} to ($\lambda$ r:{x:Nat}. r.x) should yield 0, the function only needs field x and don't care other fields in record. So we extend our rule to allow this kind of operation, where a more informative type ({x:Nat, y:Nat}) is used in the place of a less informative one ({x:Nat}).
We can use {x=0, y=1} in palace of {x=0}, we say {x:Nat, y:Nat} is a subtype, written <: of {x:Nat}. It's sub because the number of records of the subtype is less. [3]
Foramally, S is a subtype of T written S <: T, mean any term of type S can safely be used in a context where a term of type T is expected
$$\frac{\Gamma \vdash t : S \quad S <: T}{\Gamma \vdash t : T} \quad\quad \textbf{(T-SUB)}$$Intuitively, our subtype relation also have reflexivity and transitivity
$$ S <: S \quad \textbf{(S-REFL)}$$$$\frac{S <:U \quad U <: T}{S <: T} \quad\quad \textbf{(S-TRANS)}$$Question
Anything strange about our T-SUB rule compared w/ other typing rules when syntax is considered?
Syntax
t :: = x variable
lambda x:T. t abstraction (function)
t t application (function call)Typing rules
$$\frac{x:T \in \Gamma}{\Gamma \vdash x : T} \quad\quad \textbf{(T-VAR)}$$$$\frac{\Gamma,x:T_1 \vdash t_2:T_2}{\Gamma \vdash \lambda x:T_1. t_2:T_1 \rightarrow T_2} \quad\quad \textbf{(T-ABS)}$$$$\frac{\Gamma \vdash t_1 : T_{11} \rightarrow T_{12} \quad \Gamma \vdash t_2 : T_{11}}{\Gamma \vdash t_1 \ t_2 : T_{12}} \quad\quad \textbf{(T-APP)}$$$$\frac{\Gamma \vdash t : S \quad S <: T}{\Gamma \vdash t : T} \quad\quad \textbf{(T-SUB)}$$This will be answered in Chapter 16
We formalize {x=0, y=1} <: {x=0} as width subtyping rule
$$\{l_i:T_i^{i \in 1..n+k}\} <: \{l_i:T_i^{i \in 1..n}\} \quad \textbf{(S-RCDWIDTH)}$$It might looks counter intuitive that the "smaller" type (subtype) actually has more fields. That is because more fields in the record type means more restriction and a smaller set it can cover, the following euler diargam shows this relation, {x:Nat, y:Nat, z:Nat} <: {x:Nat, y:Nat} <: {x:Nat} and {x:Nat, y:Nat} <: {y:Nat}
The "smaller" record type has more fields because there are less records of this type
Question
If we specialize record to tuple, how many circle would left in above diagram?
In S-RcdWidth, we require each field has identitical type, however, this restriction can be loosen, they can have subtype relation, this gives us the depth subtyping rule
$$\frac{\text{for each } i \quad S_i <: T_i}{\{l_i:S_i^{i \in 1..n}\} <: \{l_i:T_i^{i \in 1..n}\}} \quad\quad \textbf{(S-RCDDEPTH)}$$We can combine S-RcdWidth and S-RcdDepth together
$$\frac{ \text{\{ x: Nat, y: Nat, z: Nat\}} <: \text{\{x: Nat, y: Nat\}} \quad \text{\{radius: Nat\}} <: \text{\{radius: Nat\}} } {\text{\{center: {x: Nat, y: Nat, z: Nat}, radius: Nat\}} <: \text{\{center: {x: Nat, y: Nat}, radius: Nat\}} }$$Question
If we allow mutable record, what would happen? [2]
/* {center: {x:Nat, y:Nat}, radius: Nat} -> Unit */
function move_to_origin(c: {center: {x:Nat, y:Nat}, radius: Nat}) : Unit {
c.center = {x=0, y=0}
}
var sphere = {center={x=1, y=2, z=3}, radius=2}
move_to_origin(sphere)
sphere.center.z // 3?
This will be answered in 15.5
The order of fields in record type does not have impact on safety because our projection is insensitive to it, so we have the last rule for record S-RcdPerm
$$\{l_i:T_i^{i \in 1..n+k}\} <: \{l_i:T_i^{i \in 1..n}\} \quad \textbf{(S-RCDWIDTH)}$$$$\frac{\text{for each } i \quad S_i <: T_i}{\{l_i:S_i^{i \in 1..n}\} <: \{l_i:T_i^{i \in 1..n}\}} \quad\quad \textbf{(S-RCDDEPTH)}$$$$\frac{\{k_j:S_j^{j\in 1..n}\} \text{ is a permuatation of } \{l_i:T_i^{i\in 1..n}\}} {\{k_j:S_j^{j\in 1..n}\} <: \{l_i:T_i^{i\in 1..n}\}} \quad\quad \textbf{(S-RCDPERM)}$$In fact, record subtyping is not widely adopted, OCaml is using row-variable polymorphism for records [1].
Variants is similar to record in some sense, record is a combination of many types, variant is also a combination of many types, but it can only be one of them at given time. Intuitively we have depth and permutation rule for variants.
$$\frac{\text{for each } i \quad S_i <: T_i}{\{l_i:S_i^{i \in 1..n}\} <: \{l_i:T_i^{i \in 1..n}\}} \quad\quad \textbf{(S-RCDDEPTH)}$$$$\frac{\text{for each } i \quad S_i <: T_i}{\langle l_i:S_i^{i \in 1..n}\rangle <: \langle l_i:T_i^{i \in 1..n}\rangle} \quad\quad \textbf{(S-VARIANTDEPTH)}$$$$\frac{\{k_j:S_j^{j\in 1..n}\} \text{ is a permuatation of } \{l_i:T_i^{i\in 1..n}\}} {\{k_j:S_j^{j\in 1..n}\} <: \{l_i:T_i^{i\in 1..n}\}} \quad\quad \textbf{(S-RCDPERM)}$$$$\frac{\langle k_j:S_j^{j\in 1..n}\rangle \text{ is a permuatation of } \langle l_i:T_i^{i\in 1..n}\rangle} {\langle k_j:S_j^{j\in 1..n}\rangle <: \langle l_i:T_i^{i\in 1..n}\rangle} \quad \textbf{(S-VARIANTPERM)}$$But what about width rule?
$$\{l_i:T_i^{i \in 1..n+k}\} <: \{l_i:T_i^{i \in 1..n}\} \quad \textbf{(S-RCDWIDTH)}$$Why the opposite in record and variants?
In a high order language, function can be argument to other function. Recall our subtyping rule, t does not have to be a variable term.
$$\frac{\Gamma \vdash t : S \quad S <: T}{\Gamma \vdash t : T} \quad\quad \textbf{(T-SUB)}$$The text book says we should use this one for function type
$$\frac{T_1 <: S_1 \quad S_2 <: T_2}{S_1 \rightarrow S_2 <: T_1 \rightarrow T_2} \quad\quad (\textbf{S-ARROW})$$But there are total 4 combination, what about the other 3?
$$\frac{S_1 <: T_1 \quad S_2 <: T_2}{S_1 \rightarrow S_2 <: T_1 \rightarrow T_2} \quad\quad (\textbf{S-ARROW-1})$$$$\frac{T_1 <: S_1 \quad T_2 <: S_2}{S_1 \rightarrow S_2 <: T_1 \rightarrow T_2} \quad\quad (\textbf{S-ARROW-2})$$$$\frac{S_1 <: T_1 \quad T_2 <: S_2}{S_1 \rightarrow S_2 <: T_1 \rightarrow T_2} \quad\quad (\textbf{S-ARROW-3})$$Note on the left side of $\rightarrow$, the relation is contravariant while on the right side, the relation is covariant, which is pretty counter intuitive. One might expect the left side (arugment) is convariant. Possible source of confusion are:
Let's look at a concrete example before we dive into this rule.
Assume we have a game called Game of the Type, you are the main character John Calculus, you want to travel to the north safely, you can use the following transportation for one time and walk all the rest
Following is the Pseudo-Code, the implementation is written in python and use dict to represent record.
/*
* Game of the Type - The Journey of John Calculus
*/
var start = {x:0, y:0} // your home
var end = {x:101, y:505} // the wall
function train(p:{y:Nat}) : {y:Nat} {
return {y=p.y+50}
}
function walk(p:{x:Nat, y:Nat}) : {x:Nat, y:Nat} {
return {x=p.x+1, y=p.y+5}
}
function dragon(p:{x:Nat, y:Nat, z:Nat}) : {x:Nat, y:Nat, z:Nat} {
return {x=p.x+10, y=p.y+50, z=p.z+1}
}
function travel(transport:{x:Nat, y:Nat} -> {x:Nat, y:Nat}, s:{x:Nat, y:Nat}) : Unit {
p := transport(s)
p := walk(p)
print(p)
}
Case-0, walk all the way (exact same type)
$$S_1 = T_1 = \text{\{x:Nat, y:Nat\}}= S_2 = T_2$$
In [4]:
# {x:Nat, y:Nat} -> {x:Nat, y:Nat}
def walk(p):
return {'x': p['x']+1, 'y': p['y']+5}
# ({x:Nat, y:Nat} -> {x:Nat, y:Nat}) -> {x:Nat, y:Nat} -> Unit
def travel(transport, s):
p = transport(s)
p = walk(p)
print('{} and walk, now I am at {}'.format(transport.__name__, p))
travel(walk, {'x': 0, 'y': 0})
Case-1, dragon, covariant for both argument and return value
$$S_1 = S_2 = \text{\{x:Nat, y:Nat, z:Nat\}} <: \text{\{x:Nat, y:Nat}\} = T_1 = T_2$$$$\frac{S_1 <: T_1 \quad S_2 <: T_2}{S_1 \rightarrow S_2 <: T_1 \rightarrow T_2} \quad\quad (\textbf{S-ARROW-1})$$
In [5]:
# {x:Nat, y:Nat, z:Nat} -> {x:Nat, y:Nat, z:Nat}
def dragon(p):
return {'x': p['x']+10, 'y': p['y']+50, 'z': p['z']+1}
In [6]:
travel(dragon, {'x': 0, 'y': 0})
In fact, covariant for both argument and return value sometimes does work
In [7]:
start = {'x': 0, 'y': 0}
# {x:Nat, y:Nat, z:Nat} <: {x:Nat, y:Nat}
new_start = {'x': start['x'], 'y': start['y'], 'z': 0}
travel(dragon, new_start)
But our type system need to be sound, not might work when special input is provided
Case-2, train, contravariant for both argument and return value
$$T_1 = T_2 = \text{\{x:Nat, y:Nat\}} <: \text{\{y:Nat}\} = S_1 = S_2$$$$\frac{T_1 <: S_1 \quad T_2 <: S_2}{S_1 \rightarrow S_2 <: T_1 \rightarrow T_2} \quad\quad (\textbf{S-ARROW-2})$$
In [8]:
# {y:Nat} -> {y:Nat}
def train(p):
return {'y': p['y']+50}
In [9]:
travel(train, {'x': 0, 'y': 0})
Case-3, dragon_train, covariant for argument and contravariant for return value
$$ \text{\{x:Nat, y:Nat, z:Nat\}} = S_1 <: T_1 = \text{\{x:Nat, y:Nat\}} = T_2 <: S_2 = \text{\{y:Nat\}}$$$$\frac{S_1 <: T_1 \quad T_2 <: S_2}{S_1 \rightarrow S_2 <: T_1 \rightarrow T_2} \quad\quad (\textbf{S-ARROW-3})$$
In [11]:
# {x:Nat, y:Nat, z:Nat} -> {y:Nat}
def dragon_train(p):
p = {'x': p['x'], 'y': p['y'], 'z': 0}
return train(dragon(p))
In [12]:
travel(dragon_train, {'x': 0, 'y': 0})
Case-4, train_dragon, contravariant for argument and covariant for return value
$$ \text{\{x:Nat, y:Nat, z:Nat\}} = S_2 <: T_2 = \text{\{x:Nat, y:Nat\}} = T_1 <: S_1 = \text{\{y:Nat\}}$$$$\frac{T_1 <: S_1 \quad S_2 <: T_2}{S_1 \rightarrow S_2 <: T_1 \rightarrow T_2} \quad\quad (\textbf{S-ARROW})$$
In [13]:
# {y:Nat} -> {x:Nat, y:Nat, z:Nat}
def train_dragon(p):
x = p['x']
p = train(p)
p = {'x': x, 'y': p['y'], 'z': 0} # get off the train and get on the dragon
return dragon(p)
In [14]:
travel(train_dragon, {'x': 0, 'y': 0})
In conclusion, you can replace a function w/ its subtype because the subtype
Case-1 covariant in both argument and return value $S_1 <: T_1$ and $S_2 <: T_2$
Case-2 contravariant in both argument and return value $T_1 <: S_1$ and $T_2 <: S_2$
Case-3 covariant in argument and contravariant in return value $S_1 <: T_1$ and $T_2 <: S_2$
S-Arrow, contravariant in argument and covariant in return value $T_1 <: S_1$ and $S_2 <: T_2$
Top
Bot
null in Java [5]public void DownCast(Set<String> s) {
HashSet<String> hs = (HashSet<String>) s;
}
We need a more practical (algorithmic) rule that is equivalent to our current declarative subtyping rule
Thus we got the algorithmic subtyping after we have proved its relationship w/ the declarative one
(no more latex, just compy and paste)
Based on this algorithmic rule, we can write a pseudo implementation
function subtype(S:Ty, T:Ty) : Bool {
// anytype is subtype of Top
if T == Top then
true
// S-Arrow
else if S = S1 -> S2 && T = T1 -> T2 then
// contravariant in argument and covariant in result
subtype(T1, S1) && subtype(S2, T2)
// Record
else if S is record && T is record then
for l in S.fields()
T.contains(l) && subtype(S[l], T[l])
// Variants
else if S is variant && T is variant then
for l in T.fields()
S.contains(l) && subtype(S[l], T[l])
else
false
}
Question Anything wrong in our pseudo code?
Books
Courses
Meetup
Miscellaneous