程序代写代做代考 Lambda Calculus ocaml Abstraction

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