Higher-Ranked Exception Types
Ruud Koot
May 13, 2014
1 The λ∪ -calculus
Types
τ ∈ Ty
P
| τ1 → τ2
::=
(base type)
(function type)
Terms
t ∈ Tm
::=
|
|
|
|
|
Values
x, y, ...
(variable)
λx : τ.t
(abstraction)
t1 t2
(application)
∅
{c}
t1 ∪ t2
(empty)
(singleton)
(union)
Values v are terms of the form
λx1 : τ1 . · · · λxi : τi .{c1 } ∪ (· · · ∪ ({c j } ∪ ( x1 v11 · · · v1m ∪ (· · · ∪ xk vk1 · · · vkn ))))
Environments
Γ ∈ Env ::=
1.1
· | Γ, x : τ
Typing relation
Γ, x : τ ` x : τ
[T-Var]
Γ`∅:P
Γ, x : τ1 ` t : τ2
[T-Abs]
Γ ` λx : τ1 .t : τ1 → τ2
[T-Empty]
1.2
Semantics
1.3
Reduction relation
Γ ` {c} : P
[T-Con]
Γ ` t1 : τ1 → τ2 Γ ` t2 : τ1
[T-App]
Γ ` t1 t2 : τ2
Γ ` t1 : τ Γ ` t2 : τ
[T-Union]
Γ ` t1 ∪ t2 : τ
Definition 1. Let ≺ be a strict total order on Con ∪ Var, with c ≺ x for all c ∈ Con and x ∈ Var.
1
(λx : τ.t1 ) t2 −→ [t2 /x ] t1
(β-reduction)
(t1 ∪ t2 ) t3 −→ t1 t3 ∪ t2 t3
(λx : τ.t1 ) ∪ (λx : τ.t2 ) −→ λx : τ. (t1 ∪ t2 )
x t1 · · · tn ∪ x 0 t10 · · · t0n −→ x t1 ∪ t10 · · · tn ∪ t0n
(congruences)
(t1 ∪ t2 ) ∪ t3 −→ t1 ∪ (t2 ∪ t3 )
(associativity)
∅ ∪ t −→ t
(unit)
t ∪ ∅ −→ t
x ∪ x −→ x
x ∪ ( x ∪ t) −→ x ∪ t
(idempotence)
{c} ∪ {c} −→ {c}
{c} ∪ ({c} ∪ t) −→ {c} ∪ t
x t1 · · · tn ∪ {c} −→ {c} ∪ x t1 · · · tn
(1)
x t1 · · · tn ∪ ({c} ∪ t) −→ {c} ∪ ( x t1 · · · tn ∪ t)
x
x t1 · · · tn ∪ x 0 t10 · · · t0n
t1 · · · tn ∪ x 0 t10 · · · t0n ∪ t
0
−→
−→
x 0 t10 · · · t0n
x 0 t10 · · · t0n
0
∪ x t1 · · · t n
∪ ( x t1 · · · t n ∪ t )
{c} ∪ {c } −→ {c } ∪ {c}
{c} ∪ {c0 } ∪ t −→ {c0 } ∪ ({c} ∪ t)
(2)
0
(3)
0
(4)
0
(5)
0
(6)
if x ≺ x
if x ≺ x
if c ≺ c
if c ≺ c
Conjecture 1. The reduction relation −→ preserves meaning.
Conjecture 2. The reduction relation −→ is strongly normalizing.
Conjecture 3. The reduction relation −→ is locally confluent.
Corollary 1. The reduction relation −→ is confluent.
Proof. Follows from SN, LC and Newman’s Lemma.
Corollary 2. The λ∪ -calculus has unique normal forms.
Corollary 3. Equality of λ∪ -terms can be decided by normalization.
2 Completion
κ ∈ Kind
::=
exn
| κ1 ⇒ κ2
χ ∈ Exn
::=
e
| λe : κ.χ
τb ∈ ExnTy
∀e :: κ.b
τ
| bc
ool
| [τb throws χ]
| τb1 throws χ1 → τb2 throws χ2
::=
The completion procedure as a set of inference rules:
The completion procedure as an algorithm:
complete :: Env × Ty → ExnTy × Exn × Env
complete ei :: κi bool =
let e be fresh
in hbc
ool; e ei ; e :: κi ⇒ exni
2
(exception)
(exception operator)
(exception variables)
(exception abstraction)
(exception quantification)
(boolean type)
(list type)
(function type)
ei :: κi ` bool : bc
ool & e ei . e :: κi ⇒exn
[C-Bool]
ei :: κi ` τ : τb & χ . e j :: κ j
[C-List]
ei :: κi ` [τ ] : [τb throws χ] & e ei . e :: κi ⇒exn, e j :: κ j
` τ1 : τb1 & χ1 . e j :: κ j ei :: κi , e j :: κ j ` τ2 : τb2 & χ2 . e j :: κ j
[C-Arr]
ei :: κi ` τ1 → τ2 : ∀e j :: κ j . (τb1 throws χ1 → τb2 throws χ2 ) & e ei . e :: κ j ⇒exn, ek :: κk
Figure 1: Type completion (Γ ` τ : τb & χ . Γ0 )
3