Abstraction
Abstraction
Leo White
Jane Street
February 2017
1/ 88
Abstraction
▶ When faced with creating and maintaining a complex system,
the interactions of different components can be simplified by
hiding the details of each component’s implementation from
the rest of the system.
▶ Details of a component’s implementation are hidden by
protecting it with an interface.
▶ Abstraction is maintained by ensuring that the rest of the
system is invariant to changes of implementation that do not
affect the interface.
2/ 88
Abstraction in OCaml
3/ 88
Modules
4/ 88
Modules: structures
module IntSet = struct
type t = int list
let empty = []
let is_empty = function
| [] -> true
| _ -> false
let equal_member (x : int) (y : int) =
x = y
let rec mem x = function
| [] -> false
| y :: rest ->
if (equal_member x y) then true
else mem x rest
let add x t =
5/ 88
Modules: structures
if (mem x t) then t
else x :: t
let rec remove x = function
| [] -> []
| y :: rest ->
if (equal_member x y) then rest
else y :: (remove x rest)
let to_list t = t
end
6/ 88
Modules: structures
let one_two_three : IntSet.t =
IntSet.add 1
(IntSet.add 2
(IntSet.add 3 IntSet.empty))
7/ 88
Modules: structures
open IntSet
let one_two_three : t =
add 1 (add 2 (add 3 empty))
8/ 88
Modules: structures
let one_two_three : IntSet.t =
IntSet.(add 1 (add 2 (add 3 empty)))
9/ 88
Modules: structures
module IntSetPlus = struct
include IntSet
let singleton x = add x empty
end
10/ 88
Modules: signatures
sig
type t = int list
val empty : ‘a list
val is_empty : ‘a list -> bool
val equal_member : int -> int -> bool
val mem : int -> int list -> bool
val add : int -> int list -> int list
val remove : int -> int list -> int list
val to_list : ‘a -> ‘a
end
11/ 88
Modules: signatures
module IntSet : sig
type t = int list
val empty : int list
val is_empty : int list -> bool
val mem : int -> int list -> bool
val add : int -> int list -> int list
val remove : int -> int list -> int list
val to_list : int list -> int list
end = struct
…
end
12/ 88
Modules: signatures
module type IntSetS = sig
type t = int list
val empty : int list
val is_empty : int list -> bool
val mem : int -> int list -> bool
val add : int -> int list -> int list
val remove : int -> int list -> int list
val to_list : int list -> int list
end
module IntSet : IntSetS = struct
…
end
13/ 88
Modules: abstract types
let print_set (s : IntSet.t) : unit =
let rec loop = function
| x :: xs ->
print_int x;
print_string ” “;
loop xs
| [] -> ()
in
print_string “{ “;
loop s;
print_string “}”
14/ 88
Modules: abstract types
module type IntSetS : sig
type t
val empty : t
val is_empty : t -> bool
val mem : int -> t -> bool
val add : int -> t -> t
val remove : int -> t -> t
val to_list : t -> int list
end
module IntSet : IntSetS = struct
…
end
15/ 88
Modules: abstract types
# let print_set (s : IntSet.t) : unit =
let rec loop = function
| x :: xs ->
print_int x;
print_string ” “;
loop xs
| [] -> ()
in
print_string “{ “;
loop s;
print_string “}”;;
Characters 172-173:
loop s;
^
Error: This expression has type IntSet.t
but an expression was expected of type
int list
16/ 88
Invariants
17/ 88
Invariants
Abstraction has further implications beyond the ability to replace
one implementation with another:
Abstraction allows us to preserve invariants on types.
18/ 88
Invariants
module Positive : sig
type t
val zero : t
val succ : t -> t
val to_int : t -> int
end = struct
type t = int
let zero = 0
let succ x = x + 1
let to_int x = x
end
19/ 88
The meaning of types
The ability for types to represent invariants beyond their particular
data representation fundamentally changes the notion of what a
type is:
▶ In a language without abstraction (e.g. the simply typed
lambda calculus) types only represent particular data
representations.
▶ In a language with abstraction (e.g. System F) types can
represent arbitrary invariants on values.
20/ 88
Phantom types
21/ 88
Phantom types
module File : sig
type t
val open_readwrite : string -> t
val open_readonly : string -> t
val read : t -> string
val write : t -> string -> unit
end = struct
type t = int
let open_readwrite filename = …
let open_readonly filename = …
let read f = …
let write f s = …
end
22/ 88
Phantom types
# let f = File.open_readonly “foo” in
File.write f “bar”;;
Exception: Invalid_argument “write: file is read-only”.
23/ 88
Phantom types
module File : sig
type t
val open_readwrite : string -> t
val open_readonly : string -> t
val read : t -> string
val write : t -> string -> unit
end = struct
type t = int
let open_readwrite filename = …
let open_readonly filename = …
let read f = …
let write f s = …
end
24/ 88
Phantom types
module File : sig
type readonly
type readwrite
type ‘a t
val open_readwrite : string -> readwrite t
val open_readonly : string -> readonly t
val read : ‘a t -> string
val write : readwrite t -> string -> unit
end = struct
type readonly
type readwrite
type ‘a t = int
let open_readwrite filename = …
let open_readonly filename = …
let read f = …
let write f s = …
end
25/ 88
Phantom types
# let f = File.open_readonly “foo” in
File.write f “bar”;;
Characters 51-52:
File.write f “bar”;;
^
Error: This expression has type File.readonly File.t
but an expression was expected of type
File.readwrite File.t
Type File.readonly is not compatible with type
File.readwrite
26/ 88
The meaning of types (continued)
Just as abstraction allows types to represent more than just a
particular data representation, higher-kinded abstraction allows
types to represent an even wider set of concepts:
▶ Base-kinded abstraction restricts types to directly representing
invariants on values, with each type corresponding to
particular set of values.
▶ Higher-kinded abstraction allows types to represent more
general concepts without a direct correspondence to values.
27/ 88
Existential types in OCaml
28/ 88
Existential types in OCaml
Λ𝛼::*.𝜆p:Bool.𝜆x:𝛼.𝜆y:𝛼.
if p [𝛼] x y
Λ𝛼::*.Λ𝛽::*.𝜆p:Bool.𝜆x:𝛼.𝜆y:𝛽.
if p [∃𝛾.𝛾]
(pack 𝛼, x as ∃𝛾.𝛾)
(pack 𝛽, y as ∃𝛾.𝛾)
29/ 88
Existential types in OCaml
Λ𝛼::*.𝜆p:Bool.𝜆x:𝛼.𝜆y:𝛼.
if p [𝛼] x y
Λ𝛼::*.Λ𝛽::*.𝜆p:Bool.𝜆x:𝛼.𝜆y:𝛽.
if p [∃𝛾.𝛾]
(pack 𝛼, x as ∃𝛾.𝛾)
(pack 𝛽, y as ∃𝛾.𝛾)
29/ 88
Existential types in OCaml
fun p x y -> if p then x else y
∀𝛼::*. Bool → 𝛼 → 𝛼 → 𝛼
∀𝛼::*.∀𝛽::*. Bool → 𝛼 → 𝛽 → ∃𝛾::*.𝛾
30/ 88
Existential types in OCaml
(* ∃𝛼.𝛼 × (𝛼 → 𝛼) × (𝛼 → string) *)
type t =
E : ‘a * (‘a -> ‘a)* (‘a -> string) -> t
let ints =
E(0, (fun x -> x + 1), string_of_int)
let floats =
E(0.0, (fun x -> x +. 1.0), string_of_float)
let E(z, s, p) = ints in
p (s (s z))
31/ 88
Example: lightweight static capabilities
32/ 88
Example: lightweight static capabilities
module Array : sig
type ‘a t
val length : ‘a t -> int
val set : ‘a t -> int -> ‘a -> unit
val get : ‘a t -> int -> ‘a
end
33/ 88
Example: lightweight static capabilities
let search cmp arr v =
let rec look low high =
if high < low then None
else begin
let mid = (high + low)/2 in
let x = Array.get arr mid in
let res = cmp v x in
if res = 0 then Some mid
else if res < 0 then look low (mid - 1)
else look (mid + 1) high
end
in
look 0 (Array.length arr)
34/ 88
Example: lightweight static capabilities
# let arr = [|'a';'b';'c';'d'|];;
val arr : char array = [|'a'; 'b'; 'c'; 'd'|]
# let test1 = search compare arr 'c';;
val test1 : int option = Some 2
# let test2 = search compare arr 'a';;
val test2 : int option = Some 0
# let test3 = search compare arr 'x';;
Exception: Invalid_argument "index out of bounds".
35/ 88
Example: lightweight static capabilities
# let arr = [|'a';'b';'c';'d'|];;
val arr : char array = [|'a'; 'b'; 'c'; 'd'|]
# let test1 = search compare arr 'c';;
val test1 : int option = Some 2
# let test2 = search compare arr 'a';;
val test2 : int option = Some 0
# let test3 = search compare arr 'x';;
Exception: Invalid_argument "index out of bounds".
35/ 88
Example: lightweight static capabilities
# let arr = [|'a';'b';'c';'d'|];;
val arr : char array = [|'a'; 'b'; 'c'; 'd'|]
# let test1 = search compare arr 'c';;
val test1 : int option = Some 2
# let test2 = search compare arr 'a';;
val test2 : int option = Some 0
# let test3 = search compare arr 'x';;
Exception: Invalid_argument "index out of bounds".
35/ 88
Example: lightweight static capabilities
# let arr = [|'a';'b';'c';'d'|];;
val arr : char array = [|'a'; 'b'; 'c'; 'd'|]
# let test1 = search compare arr 'c';;
val test1 : int option = Some 2
# let test2 = search compare arr 'a';;
val test2 : int option = Some 0
# let test3 = search compare arr 'x';;
Exception: Invalid_argument "index out of bounds".
35/ 88
Example: lightweight static capabilities
l e t s e a r c h cmp a r r v =
l e t r e c l ook low h igh =
i f h igh < low then None
e l s e beg in
l e t mid = ( h igh + low ) /2 i n
l e t x = Array . ge t a r r mid i n
l e t r e s = cmp v x i n
i f r e s = 0 then Some mid
e l s e i f r e s < 0 then l ook low (mid −
1)
e l s e l ook (mid + 1) h igh
end
i n
l ook 0 (Array.length arr)
36/ 88
Example: lightweight static capabilities
l e t s e a r c h cmp a r r v =
l e t r e c l ook low h igh =
i f h igh < low then None
e l s e beg in
l e t mid = ( h igh + low ) /2 i n
l e t x = Array . ge t a r r mid i n
l e t r e s = cmp v x i n
i f r e s = 0 then Some mid
e l s e i f r e s < 0 then l ook low (mid −
1)
e l s e l ook (mid + 1) h igh
end
i n
l ook 0 ((Array.length arr) - 1)
37/ 88
Example: lightweight static capabilities
module Array : sig
type 'a t
val length : 'a t -> int
val set : ‘a t -> int -> ‘a -> unit
val get : ‘a t -> int -> ‘a
end
38/ 88
Example: lightweight static capabilities
module BArray : sig
type (‘s,’a) t
type ‘s index
val last : (‘s, ‘a) t -> ‘s index
val set : (‘s,’a) t -> ‘s index -> ‘a -> unit
val get : (‘s,’a) t -> ‘s index -> ‘a
end
39/ 88
Example: lightweight static capabilities
type ‘a brand =
| Brand : (‘s, ‘a) t -> ‘a brand
| Empty : ‘a brand
val brand : ‘a array -> ‘a brand
40/ 88
Example: lightweight static capabilities
# l e t Brand x = brand [ | ’ a ’ ; ’ b ’ ; ’ c ’ ; ’ d ’ | ] i n
l e t Brand y = brand [ | ’ a ’ ; ’ b ’ | ] i n
ge t y ( l a s t x ) ; ;
Characters 96-104:
get y (last x);;
^^^^^^^^
Error: This expression has type s#1 BArray.index
but an expression was expected of type s#2 BArray.index
Type s#1 is not compatible with type s#2
41/ 88
Example: lightweight static capabilities
val zero : ‘s index
val last : (‘s, ‘a) t -> ‘s index
val index : (‘s, ‘a) t -> int -> ‘s index option
val position : ‘s index -> int
val middle : ‘s index -> ‘s index -> ‘s index
val next : ‘s index -> ‘s index -> ‘s index option
val previous : ‘s index -> ‘s index ->
‘s index option
42/ 88
Example: lightweight static capabilities
struct
type (‘s,’a) t = ‘a array
type ‘a brand =
| Brand : (‘s, ‘a) t -> ‘a brand
| Empty : ‘a brand
let brand arr =
if Array.length arr > 0 then Brand arr
else Empty
type ‘s index = int
let index arr i =
if i >= 0 && i < Array.length arr then Some i
else None
let position idx = idx
let zero = 0
43/ 88
Example: lightweight static capabilities
let last arr = (Array.length arr) - 1
let middle idx1 idx2 = (idx1 + idx2)/2
let next idx limit =
let next = idx + 1 in
if next <= limit then Some next
else None
let previous limit idx =
let prev = idx - 1 in
if prev >= limit then Some prev
else None
let set = Array.set
let get = Array.get
end
44/ 88
Example: lightweight static capabilities
l e t b s ea r ch cmp a r r v =
l e t open BArray i n
l e t r e c l ook ba r r low h igh =
l e t mid = midd le low h igh i n
l e t x = get ba r r mid i n
l e t r e s = cmp v x i n
i f r e s = 0 then Some ( p o s i t i o n mid )
e l s e i f r e s < 0 then
match p r e v i o u s low mid wi th
| Some prev −> look ba r r low prev
| None −> None
e l s e
match next mid h igh wi th
| Some next −> look ba r r nex t h igh
| None −> None
i n
match brand a r r w i th
| Brand ba r r −> look ba r r z e r o ( l a s t b a r r )
| Empty −> None
45/ 88
Example: lightweight static capabilities
l e t s e t = Array . un sa f e_s e t
l e t ge t = Array . unsa f e_get
46/ 88
Abstraction in System F𝜔
47/ 88
Existential types
48/ 88
Existential types
NatSetImpl =
𝜆𝛼::*.
𝛼
× (𝛼 → Bool)
× (Nat → 𝛼 → Bool)
× (Nat → 𝛼 → 𝛼)
× (Nat → 𝛼 → 𝛼)
× (𝛼 → List Nat)
empty = Λ𝛼::*.𝜆s:NatSetImpl 𝛼.𝜋1 s
is_empty = Λ𝛼::*.𝜆s:NatSetImpl 𝛼.𝜋2 s
mem = Λ𝛼::*.𝜆s:NatSetImpl 𝛼.𝜋3 s
add = Λ𝛼::*.𝜆s:NatSetImpl 𝛼.𝜋4 s
remove = Λ𝛼::*.𝜆s:NatSetImpl 𝛼.𝜋5 s
to_list = Λ𝛼::*.𝜆s:NatSetImpl 𝛼.𝜋6 s
49/ 88
Existential types
nat_set_package =
pack List Nat,〈
nil [Nat],
isempty [Nat],
𝜆n:Nat.fold [Nat] [Bool]
(𝜆x:Nat.𝜆y:Bool.or y (equal_nat n x))
false,
cons [Nat],
𝜆n:Nat.fold [Nat] [List Nat]
(𝜆x:Nat.𝜆l:List Nat
if (equal_nat n x) [List Nat] l
(cons [Nat] x l))
(nil [Nat]),
𝜆l:List Nat.l 〉
as ∃𝛼::*.NatSetImpl 𝛼
50/ 88
Existential types
open nat_set_package as NatSet, nat_set
one_two_three =
(add [NatSet] nat_set) one
((add [NatSet] nat_set) two
((add [NatSet] nat_set) three
(empty [NatSet] nat_set)))
51/ 88
Existential types
Γ ⊢ 𝑀 ∶ 𝐴[𝛼 ∶= 𝐵] Γ ⊢ ∃𝛼∶∶𝐾.𝐴 ∶∶ ∗
∃-introΓ ⊢ pack 𝐵, 𝑀 as ∃𝛼∶∶𝐾.𝐴 ∶ ∃𝛼∶∶𝐾.𝐴
52/ 88
Relational abstraction
53/ 88
Relational abstraction
We can give a precise description of abstraction using relations
between types.
54/ 88
Definable relations
We define relations between types
𝜌 ∶∶= (𝑥 ∶ 𝐴, 𝑦 ∶ 𝐵).𝜙[𝑥, 𝑦]
where A and B are System F types, and 𝜙[𝑥, 𝑦] is a logical formula
involving 𝑥 and 𝑦.
55/ 88
Definable relations
Logical connectives:
𝜙 ∶∶= 𝜙 ∧ 𝜓 | 𝜙 ∨ 𝜓 | 𝜙 ⇒ 𝜓
Universal quantifications:
𝜙 ∶∶= ∀𝑥 ∶ 𝐴.𝜙 | ∀𝛼.𝜙 | ∀𝑅 ⊂ 𝐴 × 𝐵.𝜙
Existential quantifications:
𝜙 ∶∶= ∃𝑥 ∶ 𝐴.𝜙 | ∃𝛼.𝜙 | ∃𝑅 ⊂ 𝐴 × 𝐵.𝜙
Relations:
𝜙 ∶∶= 𝑅(𝑡, 𝑢)
Term equality:
𝜙 ∶∶= (𝑡 =𝐴 𝑢)
56/ 88
Changing implementations
type t
val empty : t
val is_empty : t -> bool
val mem : t -> int -> bool
val add : t -> int -> t
val if_empty : t -> ‘a -> ‘a -> ‘a
57/ 88
Changing implementations
type tlist = int list
let emptylist = []
let is_emptylist = function
| [] -> true
| _ -> false
let rec memlist x = function
| [] -> false
| y :: rest ->
if x = y then true
else memlist x rest
let addlist x t =
if (memlist x t) then t
else x :: t
58/ 88
Changing implementations
let if_emptylist t x y =
match t with
| [] -> x
| _ -> y
59/ 88
Changing implementations
type ttree =
| Empty
| Node of ttree * int * ttree
let emptytree = Empty
let is_emptytree = function
| Empty -> true
| _ -> false
let rec memtree x = function
| Empty -> false
| Node(l, y, r) ->
if x = y then true
else if x < y then memtree x l
else memtree x r
let rec addtree x t =
match t with
| Empty -> Node(Empty, x, Empty)
60/ 88
Changing implementations
| Node(l, y, r) as t ->
if x = y then t
else if x < y then Node(addtree x l, y, r)
else Node(l, y, addtree x r)
let if_emptytree t x y =
match t with
| Empty -> x
| _ -> y
61/ 88
Relations between types
type t list = i n t l i s t ∼
type t tree =
| Empty
| Node o f t tree * i n t * t tree
[] Empty
[1, 2]
[2, 1]
Node(Empty, 1, Node(Empty, 2, Empty)
Node(Node(Empty, 1, Empty), 2, Empty
𝜎
𝜎
𝜎
𝜎
𝜎
62/ 88
Relations between types
type t list = i n t l i s t ∼
type t tree =
| Empty
| Node o f t tree * i n t * t tree
[] Empty
[1, 2]
[2, 1]
Node(Empty, 1, Node(Empty, 2, Empty)
Node(Node(Empty, 1, Empty), 2, Empty
𝜎
𝜎
𝜎
𝜎
𝜎
62/ 88
Relations between types
type t list = i n t l i s t ∼
type t tree =
| Empty
| Node o f t tree * i n t * t tree
[] Empty
[1, 2]
[2, 1]
Node(Empty, 1, Node(Empty, 2, Empty)
Node(Node(Empty, 1, Empty), 2, Empty
𝜎
𝜎
𝜎
𝜎
𝜎
62/ 88
Relations between types
type t list = i n t l i s t ∼
type t tree =
| Empty
| Node o f t tree * i n t * t tree
[] Empty
[1, 2]
[2, 1]
Node(Empty, 1, Node(Empty, 2, Empty)
Node(Node(Empty, 1, Empty), 2, Empty
𝜎
𝜎
𝜎
𝜎
𝜎
62/ 88
Relations between values
l e t empty list = [ ] ∼ l e t emptytree = Empty
𝜎(emptylist, emptytree)
63/ 88
Relations between values
l e t empty list = [ ] ∼ l e t emptytree = Empty
𝜎(emptylist, emptytree)
63/ 88
Relations between values
l e t i s_empty list = fun c t i o n
| [ ] −> t r u e
| _ −> f a l s e ∼ l e t i s_empty tree = fun c t i o n
| Empty −> t r u e
| _ −> f a l s e
∀𝑥 ∶ 𝑡list. ∀𝑦 ∶ 𝑡tree.
𝜎(𝑥, 𝑦) ⇒ (is_emptylist 𝑥 = is_emptytree 𝑦)
64/ 88
Relations between values
l e t i s_empty list = fun c t i o n
| [ ] −> t r u e
| _ −> f a l s e ∼ l e t i s_empty tree = fun c t i o n
| Empty −> t r u e
| _ −> f a l s e
∀𝑥 ∶ 𝑡list. ∀𝑦 ∶ 𝑡tree.
𝜎(𝑥, 𝑦) ⇒ (is_emptylist 𝑥 = is_emptytree 𝑦)
64/ 88
Relations between values
l e t r e c memlist x = f u n c t i o n
| [ ] −> f a l s e
| y : : r e s t −>
i f x = y then t r u e
e l s e memlist x r e s t
∼
l e t r e c memtree x = f u n c t i o n
| Empty −> f a l s e
| Node ( l , y , r ) −>
i f x = y then t r u e
e l s e i f x < y then memtree x l
e l s e memtree x r
∀𝑥 ∶ 𝑡list. ∀𝑦 ∶ 𝑡tree. ∀𝑖 ∶ 𝐼𝑛𝑡. ∀𝑗 ∶ 𝐼𝑛𝑡.
𝜎(𝑥, 𝑦) ⇒ (𝑖 = 𝑗) ⇒ (memlist 𝑥 𝑖 = memtree 𝑦 𝑗)
65/ 88
Relations between values
l e t r e c memlist x = f u n c t i o n
| [ ] −> f a l s e
| y : : r e s t −>
i f x = y then t r u e
e l s e memlist x r e s t
∼
l e t r e c memtree x = f u n c t i o n
| Empty −> f a l s e
| Node ( l , y , r ) −>
i f x = y then t r u e
e l s e i f x < y then memtree x l
e l s e memtree x r
∀𝑥 ∶ 𝑡list. ∀𝑦 ∶ 𝑡tree. ∀𝑖 ∶ 𝐼𝑛𝑡. ∀𝑗 ∶ 𝐼𝑛𝑡.
𝜎(𝑥, 𝑦) ⇒ (𝑖 = 𝑗) ⇒ (memlist 𝑥 𝑖 = memtree 𝑦 𝑗)
65/ 88
Relations between values
l e t add list x t =
i f (memlist x t ) then t
e l s e x : : t
∼
l e t r e c addtree x t =
match t w i th
| Empty −> Node (Empty , x , Empty )
| Node ( l , y , r ) as t −>
i f x = y then t
e l s e i f x < y then
Node ( addtree x l , y , r )
e l s e
Node ( l , y , addtree x r )
∀𝑥 ∶ 𝑡list. ∀𝑦 ∶ 𝑡tree. ∀𝑖 ∶ 𝐼𝑛𝑡. ∀𝑗 ∶ 𝐼𝑛𝑡.
𝜎(𝑥, 𝑦) ⇒ (𝑖 = 𝑗) ⇒ 𝜎(addlist 𝑥 𝑖, addtree 𝑦 𝑗)
66/ 88
Relations between values
l e t add list x t =
i f (memlist x t ) then t
e l s e x : : t
∼
l e t r e c addtree x t =
match t w i th
| Empty −> Node (Empty , x , Empty )
| Node ( l , y , r ) as t −>
i f x = y then t
e l s e i f x < y then
Node ( addtree x l , y , r )
e l s e
Node ( l , y , addtree x r )
∀𝑥 ∶ 𝑡list. ∀𝑦 ∶ 𝑡tree. ∀𝑖 ∶ 𝐼𝑛𝑡. ∀𝑗 ∶ 𝐼𝑛𝑡.
𝜎(𝑥, 𝑦) ⇒ (𝑖 = 𝑗) ⇒ 𝜎(addlist 𝑥 𝑖, addtree 𝑦 𝑗)
66/ 88
Relations between values
l e t i f_empty list t x y =
match t w i th
| [ ] −> x
| _ −> y
∼
l e t i f_empty tree t x y =
match t w i th
| Empty −> x
| _ −> y
∀𝛾. ∀𝛿.
∀𝑥 ∶ 𝑡list. ∀𝑦 ∶ 𝑡tree. ∀𝑎 ∶ 𝛾. ∀𝑏 ∶ 𝛾. ∀𝑐 ∶ 𝛿. ∀𝑑 ∶ 𝛿.
𝜎(𝑥, 𝑦) ⇒ (𝑎 = 𝑐) ⇒ (𝑏 = 𝑑) ⇒
(if_emptylist 𝑥 𝑎 𝑏 = if_emptytree 𝑦 𝑐 𝑑)
67/ 88
Relations between values
l e t i f_empty list t x y =
match t w i th
| [ ] −> x
| _ −> y
∼
l e t i f_empty tree t x y =
match t w i th
| Empty −> x
| _ −> y
∀𝛾. ∀𝛿.
∀𝑥 ∶ 𝑡list. ∀𝑦 ∶ 𝑡tree. ∀𝑎 ∶ 𝛾. ∀𝑏 ∶ 𝛾. ∀𝑐 ∶ 𝛿. ∀𝑑 ∶ 𝛿.
𝜎(𝑥, 𝑦) ⇒ (𝑎 = 𝑐) ⇒ (𝑏 = 𝑑) ⇒
(if_emptylist 𝑥 𝑎 𝑏 = if_emptytree 𝑦 𝑐 𝑑)
67/ 88
Relations between values
Given t : tlist and s : ttree such that 𝜎(t, s):
i f_empty list t 5 6 ∼ i f_empty tree s 5 6
i f_empty list t t ( add list t 1)
∼
i f_empty tree s s ( addtree s 1)
i f_empty list t memlist memlist
∼
i f_empty tree t memtree memtree
68/ 88
Relations between values
Given t : tlist and s : ttree such that 𝜎(t, s):
i f_empty list t 5 6 ∼ i f_empty tree s 5 6
i f_empty list t t ( add list t 1)
∼
i f_empty tree s s ( addtree s 1)
i f_empty list t memlist memlist
∼
i f_empty tree t memtree memtree
68/ 88
Relations between values
Given t : tlist and s : ttree such that 𝜎(t, s):
i f_empty list t 5 6 ∼ i f_empty tree s 5 6
i f_empty list t t ( add list t 1)
∼
i f_empty tree s s ( addtree s 1)
i f_empty list t memlist memlist
∼
i f_empty tree t memtree memtree
68/ 88
Relations between values
l e t i f_empty list t x y =
match t w i th
| [ ] −> x
| _ −> y
∼
l e t i f_empty tree t x y =
match t w i th
| Empty −> x
| _ −> y
∀𝛾. ∀𝛿.
∀𝑥 ∶ 𝑡list. ∀𝑦 ∶ 𝑡tree. ∀𝑎 ∶ 𝛾. ∀𝑏 ∶ 𝛾. ∀𝑐 ∶ 𝛿. ∀𝑑 ∶ 𝛿.
𝜎(𝑥, 𝑦) ⇒ (𝑎 = 𝑐) ⇒ (𝑏 = 𝑑) ⇒
(if_emptylist 𝑥 𝑎 𝑏 = if_emptytree 𝑦 𝑐 𝑑)
69/ 88
Relations between values
l e t i f_empty list t x y =
match t w i th
| [ ] −> x
| _ −> y
∼
l e t i f_empty tree t x y =
match t w i th
| Empty −> x
| _ −> y
∀𝛾. ∀𝛿. ∀𝜌 ⊂ 𝛾 × 𝛿.
∀𝑥 ∶ 𝑡list. ∀𝑦 ∶ 𝑡tree. ∀𝑎 ∶ 𝛾. ∀𝑏 ∶ 𝛾. ∀𝑐 ∶ 𝛿. ∀𝑑 ∶ 𝛿.
𝜎(𝑥, 𝑦) ⇒ 𝜌(𝑎, 𝑐) ⇒ 𝜌(𝑏, 𝑑) ⇒
𝜌(if_emptylist 𝑥 𝑎 𝑏, if_emptytree 𝑦 𝑐 𝑑)
69/ 88
Relations between values
val empty:
t 𝜎(emptylist, emptytree)
val is_empty:
t -> bool
∀𝑥 ∶ 𝑡list. ∀𝑦 ∶ 𝑡tree.
𝜎(𝑥, 𝑦) ⇒(is_emptylist 𝑥 = is_emptytree 𝑦)
val mem:
t -> int -> bool
∀𝑥 ∶ 𝑡list. ∀𝑦 ∶ 𝑡tree. ∀𝑖 ∶ 𝐼𝑛𝑡. ∀𝑗 ∶ 𝐼𝑛𝑡.
𝜎(𝑥, 𝑦) ⇒(𝑖 =𝑗) ⇒
(memlist 𝑥 𝑖 = memtree 𝑦 𝑗)
val add:
t -> int -> t
∀𝑥 ∶ 𝑡list. ∀𝑦 ∶ 𝑡tree. ∀𝑖 ∶ 𝐼𝑛𝑡. ∀𝑗 ∶ 𝐼𝑛𝑡.
𝜎(𝑥, 𝑦) ⇒(𝑖 =𝑗) ⇒
𝜎(addlist 𝑥 𝑖, addtree 𝑦 𝑗)
val if_empty:
t -> ‘a -> ‘a -> ‘a
∀𝛾. ∀𝛿. ∀𝜌 ⊂ 𝛾 × 𝛿.
∀𝑥 ∶ 𝑡list. ∀𝑦 ∶ 𝑡tree. ∀𝑎 ∶ 𝛾. ∀𝑏 ∶ 𝛾. ∀𝑐 ∶ 𝛿. ∀𝑑 ∶ 𝛿.
𝜎(𝑥, 𝑦) ⇒𝜌(𝑎, 𝑐) ⇒𝜌(𝑏, 𝑑) ⇒
𝜌(if_emptylist 𝑥 𝑎 𝑏, if_emptytree 𝑦 𝑐 𝑑)
70/ 88
Relations between values
val empty:
t 𝜎(emptylist, emptytree)
val is_empty:
t -> bool
∀𝑥 ∶ 𝑡list. ∀𝑦 ∶ 𝑡tree.
𝜎(𝑥, 𝑦) ⇒(is_emptylist 𝑥 = is_emptytree 𝑦)
val mem:
t -> int -> bool
∀𝑥 ∶ 𝑡list. ∀𝑦 ∶ 𝑡tree. ∀𝑖 ∶ 𝐼𝑛𝑡. ∀𝑗 ∶ 𝐼𝑛𝑡.
𝜎(𝑥, 𝑦) ⇒(𝑖 =𝑗) ⇒
(memlist 𝑥 𝑖 = memtree 𝑦 𝑗)
val add:
t -> int -> t
∀𝑥 ∶ 𝑡list. ∀𝑦 ∶ 𝑡tree. ∀𝑖 ∶ 𝐼𝑛𝑡. ∀𝑗 ∶ 𝐼𝑛𝑡.
𝜎(𝑥, 𝑦) ⇒(𝑖 =𝑗) ⇒
𝜎(addlist 𝑥 𝑖, addtree 𝑦 𝑗)
val if_empty:
t -> ‘a -> ‘a -> ‘a
∀𝛾. ∀𝛿. ∀𝜌 ⊂ 𝛾 × 𝛿.
∀𝑥 ∶ 𝑡list. ∀𝑦 ∶ 𝑡tree. ∀𝑎 ∶ 𝛾. ∀𝑏 ∶ 𝛾. ∀𝑐 ∶ 𝛿. ∀𝑑 ∶ 𝛿.
𝜎(𝑥, 𝑦) ⇒𝜌(𝑎, 𝑐) ⇒𝜌(𝑏, 𝑑) ⇒
𝜌(if_emptylist 𝑥 𝑎 𝑏, if_emptytree 𝑦 𝑐 𝑑)
70/ 88
Relations between values
val empty:
t 𝜎(emptylist, emptytree)
val is_empty:
t -> bool
∀𝑥 ∶ 𝑡list. ∀𝑦 ∶ 𝑡tree.
𝜎(𝑥, 𝑦) ⇒(is_emptylist 𝑥 = is_emptytree 𝑦)
val mem:
t -> int -> bool
∀𝑥 ∶ 𝑡list. ∀𝑦 ∶ 𝑡tree. ∀𝑖 ∶ 𝐼𝑛𝑡. ∀𝑗 ∶ 𝐼𝑛𝑡.
𝜎(𝑥, 𝑦) ⇒(𝑖 =𝑗) ⇒
(memlist 𝑥 𝑖 = memtree 𝑦 𝑗)
val add:
t -> int -> t
∀𝑥 ∶ 𝑡list. ∀𝑦 ∶ 𝑡tree. ∀𝑖 ∶ 𝐼𝑛𝑡. ∀𝑗 ∶ 𝐼𝑛𝑡.
𝜎(𝑥, 𝑦) ⇒(𝑖 =𝑗) ⇒
𝜎(addlist 𝑥 𝑖, addtree 𝑦 𝑗)
val if_empty:
t -> ‘a -> ‘a -> ‘a
∀𝛾. ∀𝛿. ∀𝜌 ⊂ 𝛾 × 𝛿.
∀𝑥 ∶ 𝑡list. ∀𝑦 ∶ 𝑡tree. ∀𝑎 ∶ 𝛾. ∀𝑏 ∶ 𝛾. ∀𝑐 ∶ 𝛿. ∀𝑑 ∶ 𝛿.
𝜎(𝑥, 𝑦) ⇒𝜌(𝑎, 𝑐) ⇒𝜌(𝑏, 𝑑) ⇒
𝜌(if_emptylist 𝑥 𝑎 𝑏, if_emptytree 𝑦 𝑐 𝑑)
70/ 88
Relations between values
val empty:
t 𝜎(emptylist, emptytree)
val is_empty:
t -> bool
∀𝑥 ∶ 𝑡list. ∀𝑦 ∶ 𝑡tree.
𝜎(𝑥, 𝑦) ⇒(is_emptylist 𝑥 = is_emptytree 𝑦)
val mem:
t -> int -> bool
∀𝑥 ∶ 𝑡list. ∀𝑦 ∶ 𝑡tree. ∀𝑖 ∶ 𝐼𝑛𝑡. ∀𝑗 ∶ 𝐼𝑛𝑡.
𝜎(𝑥, 𝑦) ⇒(𝑖 =𝑗) ⇒
(memlist 𝑥 𝑖 = memtree 𝑦 𝑗)
val add:
t -> int -> t
∀𝑥 ∶ 𝑡list. ∀𝑦 ∶ 𝑡tree. ∀𝑖 ∶ 𝐼𝑛𝑡. ∀𝑗 ∶ 𝐼𝑛𝑡.
𝜎(𝑥, 𝑦) ⇒(𝑖 =𝑗) ⇒
𝜎(addlist 𝑥 𝑖, addtree 𝑦 𝑗)
val if_empty:
t -> ‘a -> ‘a -> ‘a
∀𝛾. ∀𝛿. ∀𝜌 ⊂ 𝛾 × 𝛿.
∀𝑥 ∶ 𝑡list. ∀𝑦 ∶ 𝑡tree. ∀𝑎 ∶ 𝛾. ∀𝑏 ∶ 𝛾. ∀𝑐 ∶ 𝛿. ∀𝑑 ∶ 𝛿.
𝜎(𝑥, 𝑦) ⇒𝜌(𝑎, 𝑐) ⇒𝜌(𝑏, 𝑑) ⇒
𝜌(if_emptylist 𝑥 𝑎 𝑏, if_emptytree 𝑦 𝑐 𝑑)
70/ 88
Relations between values
val empty:
t 𝜎(emptylist, emptytree)
val is_empty:
t -> bool
∀𝑥 ∶ 𝑡list. ∀𝑦 ∶ 𝑡tree.
𝜎(𝑥, 𝑦) ⇒(is_emptylist 𝑥 = is_emptytree 𝑦)
val mem:
t -> int -> bool
∀𝑥 ∶ 𝑡list. ∀𝑦 ∶ 𝑡tree. ∀𝑖 ∶ 𝐼𝑛𝑡. ∀𝑗 ∶ 𝐼𝑛𝑡.
𝜎(𝑥, 𝑦) ⇒(𝑖 =𝑗) ⇒
(memlist 𝑥 𝑖 = memtree 𝑦 𝑗)
val add:
t -> int -> t
∀𝑥 ∶ 𝑡list. ∀𝑦 ∶ 𝑡tree. ∀𝑖 ∶ 𝐼𝑛𝑡. ∀𝑗 ∶ 𝐼𝑛𝑡.
𝜎(𝑥, 𝑦) ⇒(𝑖 =𝑗) ⇒
𝜎(addlist 𝑥 𝑖, addtree 𝑦 𝑗)
val if_empty:
t -> ‘a -> ‘a -> ‘a
∀𝛾. ∀𝛿. ∀𝜌 ⊂ 𝛾 × 𝛿.
∀𝑥 ∶ 𝑡list. ∀𝑦 ∶ 𝑡tree. ∀𝑎 ∶ 𝛾. ∀𝑏 ∶ 𝛾. ∀𝑐 ∶ 𝛿. ∀𝑑 ∶ 𝛿.
𝜎(𝑥, 𝑦) ⇒𝜌(𝑎, 𝑐) ⇒𝜌(𝑏, 𝑑) ⇒
𝜌(if_emptylist 𝑥 𝑎 𝑏, if_emptytree 𝑦 𝑐 𝑑)
70/ 88
The relational interpretation
Given:
▶ type 𝑇 with free variables ⃗⃗ ⃗⃗𝛼 = 𝛼1, … , 𝛼𝑛
▶ relations ⃗𝜌 = 𝜌1 ⊂ 𝐴1 × 𝐵1, … , 𝜌𝑛 ⊂ 𝐴𝑛 × 𝐵𝑛
We define the relation:
J𝑇 K[ ⃗𝜌] ⊂ 𝑇 [ ⃗⃗ ⃗⃗ ⃗⃗𝐴] × 𝑇 [ ⃗⃗⃗ ⃗⃗𝐵]
71/ 88
Relational interpretation: free variables
If 𝑇 is 𝛼𝑖 then J𝑇 K[ ⃗𝜌] = 𝜌𝑖
72/ 88
Relational interpretation: products
If 𝑇 is 𝑇 ′ × 𝑇 ″ then
J𝑇 K[ ⃗𝜌] = (𝑥 ∶ 𝑇 [ ⃗⃗ ⃗⃗ ⃗⃗𝐴], 𝑦 ∶ 𝑇 [ ⃗⃗⃗ ⃗⃗𝐵]).J𝑇 ′K[ ⃗𝜌](𝑓𝑠𝑡(𝑥), 𝑓𝑠𝑡(𝑦))
∧ J𝑇 ″K[ ⃗𝜌](𝑠𝑛𝑑(𝑥), 𝑠𝑛𝑑(𝑦))
73/ 88
Relational interpretation: sums
If 𝑇 is 𝑇 ′ + 𝑇 ″ then
J𝑇 K[ ⃗𝜌] = (𝑥 ∶ 𝑇 [ ⃗⃗ ⃗⃗ ⃗⃗𝐴], 𝑦 ∶ 𝑇 [ ⃗⃗⃗ ⃗⃗𝐵]).
∃𝑢′ ∶ 𝑇 ′[ ⃗⃗ ⃗⃗ ⃗⃗𝐴]. ∃𝑣′ ∶ 𝑇 ′[ ⃗⃗⃗ ⃗⃗𝐵].
𝑥 = 𝑖𝑛𝑙(𝑢′) ∧ 𝑦 = 𝑖𝑛𝑙(𝑣′)
∧ J𝑇 ′K[ ⃗𝜌](𝑢′, 𝑣′)
∨
∃𝑢″ ∶ 𝑇 ″[ ⃗⃗ ⃗⃗ ⃗⃗𝐴]. ∃𝑣″ ∶ 𝑇 ″[ ⃗⃗⃗ ⃗⃗𝐵].
𝑥 = 𝑖𝑛𝑟(𝑢″) ∧ 𝑦 = 𝑖𝑛𝑟(𝑣″)
∧ J𝑇 ″K[ ⃗𝜌](𝑢″, 𝑣″)
74/ 88
Relational interpretation: functions
If 𝑇 is 𝑇 ′ → 𝑇 ″ then
J𝑇 K[ ⃗𝜌] = (𝑓 ∶ 𝑇 [ ⃗⃗ ⃗⃗ ⃗⃗𝐴], 𝑔 ∶ 𝑇 [ ⃗⃗⃗ ⃗⃗𝐵]).
∀𝑢 ∶ 𝑇 ′[ ⃗⃗ ⃗⃗ ⃗⃗𝐴]. ∀𝑣 ∶ 𝑇 ′[ ⃗⃗⃗ ⃗⃗𝐵].J𝑇 ′K[ ⃗𝜌](𝑢, 𝑣) ⇒ J𝑇 ″K[ ⃗𝜌](𝑓 𝑢, 𝑔 𝑣)
75/ 88
Relational interpretation: univerals
If 𝑇 is ∀𝛽.𝑇 ′ then
J𝑇 K[ ⃗𝜌] = (𝑥 ∶ 𝑇 [ ⃗⃗ ⃗⃗ ⃗⃗𝐴], 𝑦 ∶ 𝑇 [ ⃗⃗⃗ ⃗⃗𝐵]).
∀𝛾. ∀𝛿. ∀𝜌′ ⊂ 𝛾 × 𝛿.J𝑇 ′K[ ⃗𝜌, 𝜌′](𝑥[𝛾], 𝑦[𝛿])
76/ 88
Relational interpretation: existentials
If 𝑇 is ∃𝛽.𝑇 ′ then
J𝑇 K[ ⃗𝜌] = (𝑥 ∶ 𝑇 [ ⃗⃗ ⃗⃗ ⃗⃗𝐴], 𝑦 ∶ 𝑇 [ ⃗⃗⃗ ⃗⃗𝐵]).
∃𝛾. ∃𝛿. ∃𝜌′ ⊂ 𝛾 × 𝛿.
∃𝑢 ∶ 𝑇 ′[ ⃗⃗ ⃗⃗ ⃗⃗𝐴, 𝛾]. ∃𝑣 ∶ 𝑇 ′[ ⃗⃗⃗ ⃗⃗𝐵, 𝛿].
𝑥 = pack 𝛾, 𝑢 as 𝑇 [ ⃗⃗ ⃗⃗ ⃗⃗𝐴]
∧ 𝑦 = pack 𝛿, 𝑣 as 𝑇 [ ⃗⃗⃗ ⃗⃗𝐵]
∧ J𝑇 ′K[ ⃗𝜌, 𝜌′](𝑢, 𝑣)
77/ 88
Relations between values
val empty:
t 𝜎(emptylist, emptytree)
val is_empty:
t -> bool
∀𝑥 ∶ 𝑡list. ∀𝑦 ∶ 𝑡tree.
𝜎(𝑥, 𝑦) ⇒ (is_emptylist 𝑥 = is_emptytree 𝑦)
val mem:
t -> int -> bool
∀𝑥 ∶ 𝑡list. ∀𝑦 ∶ 𝑡tree. ∀𝑖 ∶ 𝐼𝑛𝑡. ∀𝑗 ∶ 𝐼𝑛𝑡.
𝜎(𝑥, 𝑦) ⇒ (𝑖 = 𝑗) ⇒
(memlist 𝑥 𝑖 = memtree 𝑦 𝑗)
val add:
t -> int -> t
∀𝑥 ∶ 𝑡list. ∀𝑦 ∶ 𝑡tree. ∀𝑖 ∶ 𝐼𝑛𝑡. ∀𝑗 ∶ 𝐼𝑛𝑡.
𝜎(𝑥, 𝑦) ⇒ (𝑖 = 𝑗) ⇒
𝜎(addlist 𝑥 𝑖, addtree 𝑦 𝑗)
val if_empty:
t -> ‘a -> ‘a -> ‘a
∀𝛾. ∀𝛿. ∀𝜌 ⊂ 𝛾 × 𝛿.
∀𝑥 ∶ 𝑡list. ∀𝑦 ∶ 𝑡tree. ∀𝑎 ∶ 𝛾. ∀𝑏 ∶ 𝛾. ∀𝑐 ∶ 𝛿. ∀𝑑 ∶ 𝛿.
𝜎(𝑥, 𝑦) ⇒ 𝜌(𝑎, 𝑐) ⇒ 𝜌(𝑏, 𝑑) ⇒
𝜌(if_emptylist 𝑥 𝑎 𝑏, if_emptytree 𝑦 𝑐 𝑑)
78/ 88
Relations between values
val empty:
t J𝛼K[𝜎](emptylist, emptytree)
val is_empty:
t -> bool
∀𝑥 ∶ 𝑡list. ∀𝑦 ∶ 𝑡tree.
𝜎(𝑥, 𝑦) ⇒ (is_emptylist 𝑥 = is_emptytree 𝑦)
val mem:
t -> int -> bool
∀𝑥 ∶ 𝑡list. ∀𝑦 ∶ 𝑡tree. ∀𝑖 ∶ 𝐼𝑛𝑡. ∀𝑗 ∶ 𝐼𝑛𝑡.
𝜎(𝑥, 𝑦) ⇒ (𝑖 = 𝑗) ⇒
(memlist 𝑥 𝑖 = memtree 𝑦 𝑗)
val add:
t -> int -> t
∀𝑥 ∶ 𝑡list. ∀𝑦 ∶ 𝑡tree. ∀𝑖 ∶ 𝐼𝑛𝑡. ∀𝑗 ∶ 𝐼𝑛𝑡.
𝜎(𝑥, 𝑦) ⇒ (𝑖 = 𝑗) ⇒
𝜎(addlist 𝑥 𝑖, addtree 𝑦 𝑗)
val if_empty:
t -> ‘a -> ‘a -> ‘a
∀𝛾. ∀𝛿. ∀𝜌 ⊂ 𝛾 × 𝛿.
∀𝑥 ∶ 𝑡list. ∀𝑦 ∶ 𝑡tree. ∀𝑎 ∶ 𝛾. ∀𝑏 ∶ 𝛾. ∀𝑐 ∶ 𝛿. ∀𝑑 ∶ 𝛿.
𝜎(𝑥, 𝑦) ⇒ 𝜌(𝑎, 𝑐) ⇒ 𝜌(𝑏, 𝑑) ⇒
𝜌(if_emptylist 𝑥 𝑎 𝑏, if_emptytree 𝑦 𝑐 𝑑)
78/ 88
Relations between values
val empty:
t J𝛼K[𝜎](emptylist, emptytree)
val is_empty:
t -> bool J𝛼 → 𝛾K[𝜎, =Bool](is_emptylist, is_emptytree)
val mem:
t -> int -> bool
∀𝑥 ∶ 𝑡list. ∀𝑦 ∶ 𝑡tree. ∀𝑖 ∶ 𝐼𝑛𝑡. ∀𝑗 ∶ 𝐼𝑛𝑡.
𝜎(𝑥, 𝑦) ⇒ (𝑖 = 𝑗) ⇒
(memlist 𝑥 𝑖 = memtree 𝑦 𝑗)
val add:
t -> int -> t
∀𝑥 ∶ 𝑡list. ∀𝑦 ∶ 𝑡tree. ∀𝑖 ∶ 𝐼𝑛𝑡. ∀𝑗 ∶ 𝐼𝑛𝑡.
𝜎(𝑥, 𝑦) ⇒ (𝑖 = 𝑗) ⇒
𝜎(addlist 𝑥 𝑖, addtree 𝑦 𝑗)
val if_empty:
t -> ‘a -> ‘a -> ‘a
∀𝛾. ∀𝛿. ∀𝜌 ⊂ 𝛾 × 𝛿.
∀𝑥 ∶ 𝑡list. ∀𝑦 ∶ 𝑡tree. ∀𝑎 ∶ 𝛾. ∀𝑏 ∶ 𝛾. ∀𝑐 ∶ 𝛿. ∀𝑑 ∶ 𝛿.
𝜎(𝑥, 𝑦) ⇒ 𝜌(𝑎, 𝑐) ⇒ 𝜌(𝑏, 𝑑) ⇒
𝜌(if_emptylist 𝑥 𝑎 𝑏, if_emptytree 𝑦 𝑐 𝑑)
78/ 88
Relations between values
val empty:
t J𝛼K[𝜎](emptylist, emptytree)
val is_empty:
t -> bool J𝛼 → 𝛾K[𝜎, =Bool](is_emptylist, is_emptytree)
val mem:
t -> int -> bool J𝛼 → 𝛽 → 𝛾K[𝜎, =Int, =Bool](memlist, memtree)
val add:
t -> int -> t
∀𝑥 ∶ 𝑡list. ∀𝑦 ∶ 𝑡tree. ∀𝑖 ∶ 𝐼𝑛𝑡. ∀𝑗 ∶ 𝐼𝑛𝑡.
𝜎(𝑥, 𝑦) ⇒ (𝑖 = 𝑗) ⇒
𝜎(addlist 𝑥 𝑖, addtree 𝑦 𝑗)
val if_empty:
t -> ‘a -> ‘a -> ‘a
∀𝛾. ∀𝛿. ∀𝜌 ⊂ 𝛾 × 𝛿.
∀𝑥 ∶ 𝑡list. ∀𝑦 ∶ 𝑡tree. ∀𝑎 ∶ 𝛾. ∀𝑏 ∶ 𝛾. ∀𝑐 ∶ 𝛿. ∀𝑑 ∶ 𝛿.
𝜎(𝑥, 𝑦) ⇒ 𝜌(𝑎, 𝑐) ⇒ 𝜌(𝑏, 𝑑) ⇒
𝜌(if_emptylist 𝑥 𝑎 𝑏, if_emptytree 𝑦 𝑐 𝑑)
78/ 88
Relations between values
val empty:
t J𝛼K[𝜎](emptylist, emptytree)
val is_empty:
t -> bool J𝛼 → 𝛾K[𝜎, =Bool](is_emptylist, is_emptytree)
val mem:
t -> int -> bool J𝛼 → 𝛽 → 𝛾K[𝜎, =Int, =Bool](memlist, memtree)
val add:
t -> int -> t J𝛼 → 𝛽 → 𝛼K[𝜎, =Int](addlist, addtree)
val if_empty:
t -> ‘a -> ‘a -> ‘a
∀𝛾. ∀𝛿. ∀𝜌 ⊂ 𝛾 × 𝛿.
∀𝑥 ∶ 𝑡list. ∀𝑦 ∶ 𝑡tree. ∀𝑎 ∶ 𝛾. ∀𝑏 ∶ 𝛾. ∀𝑐 ∶ 𝛿. ∀𝑑 ∶ 𝛿.
𝜎(𝑥, 𝑦) ⇒ 𝜌(𝑎, 𝑐) ⇒ 𝜌(𝑏, 𝑑) ⇒
𝜌(if_emptylist 𝑥 𝑎 𝑏, if_emptytree 𝑦 𝑐 𝑑)
78/ 88
Relations between values
val empty:
t J𝛼K[𝜎](emptylist, emptytree)
val is_empty:
t -> bool J𝛼 → 𝛾K[𝜎, =Bool](is_emptylist, is_emptytree)
val mem:
t -> int -> bool J𝛼 → 𝛽 → 𝛾K[𝜎, =Int, =Bool](memlist, memtree)
val add:
t -> int -> t J𝛼 → 𝛽 → 𝛼K[𝜎, =Int](addlist, addtree)
val if_empty:
t -> ‘a -> ‘a -> ‘a J∀𝛿. 𝛼 → 𝛿 → 𝛿 → 𝛿K[𝜎](if_emptylist, if_emptytree)
78/ 88
Relations between values
J𝛼
× (𝛼 → 𝛾)
× (𝛼 → 𝛽 → 𝛾)
× (𝛼 → 𝛽 → 𝛼)
× (∀𝛿. 𝛼 → 𝛿 → 𝛿 → 𝛿)K[𝜎, =Int, =Bool](setlist, settree)
79/ 88
Relational abstraction
Given a type 𝑇 with free variables 𝛼, 𝛽1, … , 𝛽𝑛:
∀𝐵1. … ∀𝐵𝑛. ∀𝑥 ∶ (∃𝛼.𝑇 [𝛼, 𝐵1, … , 𝐵𝑛]). ∀𝑦 ∶ (∃𝛼.𝑇 [𝛼, 𝐵1, … , 𝐵𝑛]).
𝑥 = 𝑦 ⇔
∃𝛾. ∃𝛿. ∃𝜎 ⊂ 𝛾 × 𝛿.
∃𝑢 ∶ 𝑇 [𝛾, 𝐵1, … 𝐵𝑛]. ∃𝑣 ∶ 𝑇 [𝛿, 𝐵1, … 𝐵𝑛].
𝑥 = pack 𝛾, 𝑢 as ∃𝛼.𝑇 [𝛼, 𝐵1, … , 𝐵𝑛]
∧ 𝑦 = pack 𝛿, 𝑣 as ∃𝛼.𝑇 [𝛼, 𝐵1, … , 𝐵𝑛]
∧ J𝑇 K[𝜎, =𝐵1 , … , =𝐵𝑛 ](𝑢, 𝑣)
80/ 88
Relational abstraction
If there is a relation between the implementation types of two
values with existential type, and their implementations behave the
same with respect to this relation, then the two values are equal.
81/ 88
Invariants
82/ 88
Invariants
Represent an invariant 𝜙[𝑥] on a type 𝛾 as a relation 𝜌 ⊂ 𝛾 × 𝛾:
𝜌(𝑥 ∶ 𝛾, 𝑦 ∶ 𝛾) = (𝑥 = 𝑦) ∧ 𝜙[𝑥]
83/ 88
Invariants
Given a type 𝑇 with free variable 𝛼:
∀𝑓 ∶ (∀𝛼.𝑇 [𝛼] → 𝛼).
∀𝛾. ∀𝜌 ⊂ 𝛾 × 𝛾. ∀𝑥 ∶ 𝑇 [𝛾].J𝑇 K[𝜌](𝑥, 𝑥) ⇒ 𝜌(𝑓[𝛾] 𝑥, 𝑓[𝛾] 𝑥)
84/ 88
Invariants
Note that:
open (pack 𝛾, 𝑢 as ∃𝛼. 𝑇 [𝛼]) as 𝑥, 𝛼 in 𝑡
=
(Λ𝛼. 𝜆𝑥 ∶ 𝑇 [𝛼]. 𝑡)[𝛾] 𝑢
So:
∀𝜌 ⊂ 𝛾 × 𝛾. J𝑇 K[𝜌](𝑢, 𝑢) ⇒
𝜌(
open (pack 𝛾, 𝑢as ∃𝛼. 𝑇 [𝛼]) as 𝑥, 𝛼in 𝑡,
open (pack 𝛾, 𝑢as ∃𝛼. 𝑇 [𝛼]) as 𝑥, 𝛼in 𝑡
)
85/ 88
Identity extension
86/ 88
Identity extension
Given a type 𝑇 with free variables 𝛼1, … , 𝛼𝑛:
∀𝐴1. … ∀𝐴𝑛. ∀𝑥 ∶ 𝑇 [𝐴1, … , 𝐴𝑛]. ∀𝑦 ∶ 𝑇 [𝐴1, … , 𝐴𝑛].
(𝑥 =𝑇[𝐴1,…,𝐴𝑛] 𝑦) ⇔ J𝑇 K[=𝐴1 , … , =𝐴𝑛 ](𝑥, 𝑦)
87/ 88
Next time
Parametricity
88/ 88