Sound Mutable and Const Types

SRL Technical Report SRL2008-03

Oct. 3rd 2008.

Swaroop Sridhar, Jonathan S. Shapiro, Scott F. Smith

Department of Computer Science

The Johns Hopkins University
3400 N.Charles Street. 224 NEB. Baltimore, MD 21218.

Abstract

Subsequent to the work presented in Sound and Complete Type Inference in BitC, we introduced by-reference parameters and discovered that the definition of mutability described in that report was insufficient. The language specification was updated to have a path-wise notion of mutability. At the same time, a const meta-constructor was introduced into the language to strip shallow mutability (up to the ref boundary) from existing types.

The following type rules reflect the modifications to the language associated with that change.

1

*B* Language grammar:

Identifiers

_x_ ::=

_y_ | _z_ | ...

Booleans

?b? ::=

true | false

Indices

i ::=

1 | 2 | !i

Opt. Const

_e_ ::=

_e_ | ⌊_e_⌋

Values

_v_ ::=

() | ?b? | λ_x_._e_ | (_v_, _v_) | ℓ

Syn. Value

υ ::=

_v_ | _x_ | l | (υ, υ)

Left Expr

_l_ ::=

_x_ | l | _e_^ | _l_.i

Expressions

_e_ ::=

υ | _e_ _e_ | _l_ := _e_ | if  _e_ then _e_ else _e_

  

 

 | dup(_e_) | _e_^ | (_e_, _e_) | _e_.i

  

 

 | letϰ _x_ = _e_ in _e_

Let-kinds

ϰ ::=

- | κ | ψ | ∀

Locations

?L? ::=

l | ℓ

Types grammar:

Type Variables

α ::=

α | β | γ | δ | ε | ...

M-Vars

ς ::=

α | Ψα

Types.1

ρ ::=

α | unit | bool | τ → τ | τ ✗ τ

  Ref/Pointer

 

 | ⇑τ

  Mutable, const

 

 | Ψρ | ⌊τ⌋

Types.2

ϱ ::=

ρ | α⇃ρ

Types

τ ::=

ϱ | ς↓ρ

Type Scheme

σ ::=

τ | ∀α*.τ\*D*

Poly. Constraints

?d? ::=

★ϰ_x_(τ)

Poly. Constraint Sets

*D* ::=

∅ | {?d?*} | *D* ∪ *D*

Grammar for Dynamic Semantics:

Stack

S ::=

∅ | S, l ↦ _v_

Heap

H ::=

∅ | H, ℓ ↦ _v_

Selection Path

?p? ::=

i | ?p?.?p?

lvalues

£ ::=

l | ℓ^ | l.?p? | ℓ^.?p?

Redex

*R* ::=

- | *R* _e_ | _v_ *R* | £ := *R*

  

 

 | if  *R* then _e_ else _e_ | *R*^

  

 

 | dup(*R*) | dup(⌊*R*⌋) | (*R*, _e_)

  

 

 | (_v_, *R*) | *R*.i | letϰ _x_ = *R* in _e_

Grammar for Static Semantics:

Unf. Constraints

?u? ::=

τ = τ | κ = ϰ | ?d?

Unf. Constraint Sets

*C* ::=

∅ | {?u?*} | *C* ∪ *C* | *C* ∪ *C*

Substitutions

θ ::=

〈〉 | [α ↣ τ] | [κ ↣ ϰ] | θ ∘ θ

Binding Environment

Γ ::=

∅ | Γ, _x_ ↦ σ

Store Typing

Σ ::=

∅ | Σ, ?L? ↦ τ

Definition 1: (Mutability Normalization in Composite Types)

*M*?(?τ?)? | ?Immut??(?τ?)? = ⊥
*M*?(?α?)? = ⊥
*M*?(?Ψα?)? = ⊥
*M*?(?Ψbool?)? = 〈〉
*M*?(?Ψunit?)? = 〈〉
*M*?(?Ψ(τ1 → τ2)?)? = 〈〉
*M*?(?Ψ⇑τ?)? = 〈〉
*M*?(?Ψ(τ1 ✗ τ2)?)? = *M*?(?τ1?)? ∘ *M*?(?τ2?)?
*M*?(?α⇃ρ?)? = [α ↣ Ψρ] ∘ *M*?(?Ψρ?)?
*M*?(?Ψα↓ρ?)? = 〈〉
*M*?(?α↓ρ?)? = [α ↣ Ψβ] |  ⊧new β

Definition 2: (Normalization of Const Types)

*N*?(?α?)? = α
*N*?(?⌊α⌋?)? = ⌊α⌋
*N*?(?bool?)? = bool
*N*?(?⌊bool⌋?)? = bool
*N*?(?unit?)? = unit
*N*?(?⌊unit⌋?)? = unit
*N*?(?τ1 → τ2?)? = *N*?(?τ1?)? → *N*?(?τ2?)?
*N*?(?⌊τ1 → τ2⌋?)? = *N*?(?τ1?)? → *N*?(?τ2?)?
*N*?(?⇑τ?)? = ⇑*N*?(?τ?)?
*N*?(?⌊⇑τ⌋?)? = ⇑*N*?(?τ?)?
*N*?(?Ψτ?)? = Ψ*N*?(?τ?)?
*N*?(?⌊Ψτ⌋?)? = *N*?(?⌊τ⌋?)?
*N*?(?τ1 ✗ τ2?)? = *N*?(?τ1?)? ✗ *N*?(?τ2?)?
*N*?(?⌊τ1 ✗ τ2⌋?)? = ⌊*N*?(?τ1?)?⌋ ✗ ⌊*N*?(?τ2?)?⌋
*N*?(?α⇃ρ?)? = α⇃*N*?(?Ψρ?)?
*N*?(?⌊α⇃ρ⌋?)? = ⌊α⇃*N*?(?Ψρ?)?⌋
*N*?(?ς↓ρ?)? = ς↓*N*?(?ρ?)?
*N*?(?⌊ς↓ρ⌋?)? = ⌊ς↓*N*?(?ρ?)?⌋

Definition 3: (Notational convenience)

We write τ1 =▾ τ2 as shorthand for ▾(τ1) = ▾(τ2), τ1 =▽ τ2 for ▽(τ1) = ▽(τ2), and τ1 =∘ τ2 for ▽(τ1) = ▽(τ2)

Definition 4: (Const-ness Requirement)

*P*?(?_e_,  τ?)? = ?true?
*P*?(?⌊_e_⌋,  ⌊τ⌋?)? = ?true?
*P*?(?_e_,  ⌊τ⌋?)? (otherwise) = ?false?
*P*?(?_e_,  τ?)? = τ
*P*?(?⌊_e_⌋,  τ?)? = ⌊τ⌋

Rule

Pre-conditions

Evaluation Step

E-Rval

S(l) = _v_

S; H; l ⇒ S; H; _v_

E-#

S; H; _e_ ⇒ S′; H′; _e_′

S; H; *R*[_e_] ⇒ S′; H′; *R*[_e_′]

E-App

l ∉ dom(S)

S; H; λ_x_._e_ _v_ ⇒ S, l ↦ _v_; H; _e_[l/_x_]

E-If

?b?1 = true    ?b?2 = false

S; H; if  ?b?i then _e_1 else _e_2 ⇒ S; H; _e_i

E-.i

S; H; (_v_1, _v_2).i ⇒ S; H; _v_i

E-Dup

ℓ ∉ dom(H)

S; H; dup(_v_) ⇒ S; H, ℓ ↦ _v_; ℓ

EL-^#

S; H; _e_ ⇒ S′; H′; _e_′

S; H; _e_^ ⇛ S′; H′; _e_′^

E-^

H(ℓ) = _v_

S; H; ℓ^ ⇒ S; H; _v_

E-:=#

S; H; _l_ ⇛ S′; H′; _l_′

S; H; _l_ := _e_ ⇒ S′; H′; _l_′ := _e_

E-:=Stack

S, l ↦ _v_; H; l := _v_′ ⇒ S, l ↦ _v_′; H; ()

E-:=Heap

S; H, ℓ ↦ _v_; ℓ^ := _v_′ ⇒ S; H, ℓ ↦ _v_′; ()

E-:=S.p

_v_′!i = _v_!i    S, l ↦ _v_i; H; l.?p? := _v_′i

S, l ↦ (_v_1, _v_2); H; l.i.?p? := _v_′i

                    ⇒ S, l ↦ _v_′i; H; ()        

                         ⇒ S, l ↦ (_v_′1, _v_′2); H; ()

E-:=H.p

_v_′!i = _v_!i    S; H, ℓ ↦ _v_i; ℓ^.?p? := _v_′i

S; H, ℓ ↦ (_v_1, _v_2); ℓ^.i.?p? := _v_′i

                    ⇒ S; H, ℓ ↦ _v_′i; ()        

                         ⇒S; H, ℓ ↦ (_v_′1, _v_′2); ()

E-Let-M

l ∉ dom(S)

S; H; letψ _x_ = _v_1 in _e_2 ⇒ S, l ↦ _v_1; H; _e_2[l/_x_]

E-Let-P

S; H; let∀ _x_ = _v_1 in _e_2 ⇒ S; H; _e_2[_v_1/_x_]

Figure 1.

Small Step Operational Semantics

τ

△(τ)

▽(τ)

▴(τ)

▾(τ)

▽(τ)

*I*(τ)

{|τ|}

α

Ψα

α

Ψα

α

α

α

{α}

unit

Ψunit

unit

Ψunit

unit

unit

unit

∅

bool

Ψbool

bool

Ψbool

bool

bool

bool

∅

τ1 → τ2

Ψ(τ1 → τ2)

τ1 → τ2

Ψ(τ1 → τ2)

τ1 → τ2

τ1 → τ2

τ1 → τ2

{|τ1|} ∪ {|τ2|}

⇑τ

Ψ⇑τ

⇑τ

Ψ⇑τ

⇑τ

⇑τ

⇑*I*(τ)

{|τ|}

Ψρ

△(ρ)

▽(ρ)

▴(ρ)

▾(ρ)

▽(ρ)

*I*(ρ)

{|ρ|}

τ1 ✗ τ2

Ψ(△(τ1) ✗ △(τ2))

▽(τ1) ✗ ▽(τ2)

Ψ(τ1 ✗ τ2)

τ1 ✗ τ2

▽(τ1) ✗ ▽(τ2)

*I*(τ1) ✗ *I*(τ2)

{|τ1|} ∪ {|τ2|}

α⇃ρ

△(ρ)

▽(ρ)

▴(ρ)

▾(ρ)

▽(ρ)

*I*(ρ)

{α⇃ρ} ∪ {|ρ|}

ς↓ρ

△(ρ)

▽(ρ)

▴(ς)↓ρ

▾(ς)↓ρ

▽(ρ)

*I*(ρ)

{ς↓ρ} ∪ {|ρ|}

⌊τ⌋

△(τ)

⌊τ⌋

Ψ⌊τ⌋

⌊τ⌋

▽(τ)

⌊*I*(ρ)⌋

{|τ|}

τ

?Mut??(?τ?)?

?Immut??(?τ?)?

?Const??(?τ?)?

θ〈τ〉

α

?false?

?false?

?false?

τ if [α ↣ τ] ∊ θ, else α.

unit

?false?

?true?

?true?

unit

bool

?false?

?true?

?true?

bool

τ1 → τ2

?false?

?true?

?true?

θ〈τ1〉 → θ〈τ2〉

⇑τ

?Mut??(?τ?)?

?Immut??(?τ?)?

?true?

⇑θ〈τ〉

Ψρ

?true?

?false?

?false?

Ψθ〈ρ〉

τ1 ✗ τ2

?Mut??(?τ1?)? ∨ ?Mut??(?τ2?)?

?Immut??(?τ1?)? ∧ ?Immut??(?τ2?)?

?Const??(?τ1?)? ∧ ?Const??(?τ2?)?

θ〈τ1〉 ✗ θ〈τ2〉

α⇃ρ

?Mut??(?▾(ρ)?)?

?false?

?false?

α′⇃θ〈ρ〉 if θ〈α〉 = α′

ρ′ if θ〈α〉 = ρ′ ≠ α′

ς↓ρ

?Mut??(?ς?)? ∨ ?Mut??(?▽(ρ)?)?

?false?

?false?

ς′↓θ〈ρ〉 if θ〈ς〉 = ς′

ϱ if θ〈ς〉 = ϱ ≠ ς′

⌊τ⌋

?false?

?Immut??(?▽(τ)?)?

?true?

⌊θ〈τ〉⌋

τ

□(τ)

□(τ)

□(τ)

Ν(τ)

*M*?(?τ?)?

α

?false?

?false?

?false?

α

〈〉

unit

?true?

?true?

?true?

unit

〈〉

bool

?true?

?true?

?true?

bool

〈〉

τ1 → τ2

?true?

?true?

?true?

Ν(τ1) → Ν(τ2)

*M*?(?τ1?)? ∘ *M*?(?τ2?)?

⇑τ

□(τ)

?true?

?true?

⇑Ν(τ)

*M*?(?τ?)?

Ψρ

□(ρ)

□(ρ)

□(ρ)

ΨΝ(ρ)

*M*?(?ρ?)?

τ1 ✗ τ2

□(τ1) ∧ □(τ2)

□(τ1) ∧ □(τ2)

□(τ1) ∧ □(τ2)

Ν(τ1) ✗ Ν(τ2)

*M*?(?τ1?)? ∘ *M*?(?τ2?)?

α⇃ρ

□(ρ)

□(ρ)

?false?

α⇃Ν(ρ)

*M*?(?ρ?)?

ς↓ρ

□(ρ)

□(ρ)

?false?

ς↓Ν(ρ)

*M*?(?ρ?)? ∘ [α ↣ △(ρ)] if ς = Ψα

and □(ρ); *M*?(?ρ?)? otherwise

⌊τ⌋

□(τ)

□(τ)

?true?

▽(τ) if □(τ)

*M*?(?τ?)?

⌊τ⌋ otherwise

Meanings of Operators

△

Add mutability up to the ref/function boundary.

▽

Remove mutability up to the ref/function boundary.

▴

Add top-most mutability.

▾

Remove top-most mutability.

▽

Remove mutability and const up to the ref/function boundary.

*I*

Remove mutability deeply up to the function boundary.

{| |}

Constraint Collection

?Mut?

Is the type observably mutable?

?Immut?

Is the type effectively deeply immutable?

?Const?

Is the type effectively const?

θ〈 〉

Substitution.

□

Is the type concretizable? (i.e. can be made invariable

by a substitution only for mutability-variables?)

□

Is the type concretizable up to a reference boundary?

□

Is this type concrete enough to drop an enclosing const?

Ν

Partially normalized form of const types, when a const wrapper

can be dropped (ex: ⌊bool⌋ ≡ bool)

*M*

Produce a substitution to normalize ς↓ρ types.

(ex: Ψα↓bool ≡ Ψbool)

*M*

Produce a substitution to propagate mutability inwards into

composite types (or fail with an error).

*N*

Normalized form of const types, where const only appears around

variable or constrained types.

Figure 2.

Operations and Predicates on Types

S-Refl

τ ⊴: τ

   

S-Trans

τ0 ⊴: τ1    τ1 ⊴: τ2

τ0 ⊴: τ2

   

S-Mut

ρ ⊴: ρ′

Ψρ ⊴: Ψρ′

   

S-Pair

τ1 ⊴: τ′1    τ2 ⊴: τ′2

τ1 ✗ τ2 ⊴: τ′1 ✗ τ′2

   

S-MT1

▾(ρ) ⊴: τ

α⇃ρ ⊴: τ

   

S-MT2

τ ⊴: ▴(ρ)

τ ⊴: α⇃ρ

S-MF1

▽(ρ) ⊴: τ

α↓ρ ⊴: τ

   

S-MF2

α↓ρ ⊴: ρ′

Ψα↓ρ ⊴: Ψρ′

   

S-MF3

τ ⊴: △(ρ)

τ ⊴: ς↓ρ

   

S-Const1

τ ⊴: ▽(τ′)

τ ⊴: ⌊τ′⌋

   

S-Const2

▽(τ) ⊴: τ′

⌊τ⌋ ⊴: τ′

Figure 3.

Copy Coercion Rules

T-Unit

∅; Γ; Σ ⊢ () : unit

  

T-Bool

∅; Γ; Σ ⊢ ?b? : bool

  

T-Id

Γ(_x_) = ∀α*.τ\*D*    θ ⊪ {τ,  *D*}    dom(θ) = {α*}

θ〈*D*〉; Γ; Σ ⊢ _x_ : θ〈τ〉

T-Hloc

Σ(ℓ) = τ

∅; Γ; Σ ⊢ ℓ : ⇑τ

  

T-Sloc

Σ(l) = τ

∅; Γ; Σ ⊢ l : τ

  

T-Lambda

*D*; Γ, _x_ ↦ τ1; Σ ⊢ _e_ : τ2    τ1 =∘ τ′1    τ2 =∘ τ′2    *P*?(?_x_,  τ1?)?

*D*; Γ; Σ ⊢ λ_x_._e_ : τ′1 → τ′2

T-App

*D*1; Γ; Σ ⊢ _e_1 ⊴: τa → τr    *D*2; Γ; Σ ⊢ _e_2 ⊴: ▽(τa)    △(τr) ⊴: τ

*D*1 ∪ *D*2; Γ; Σ ⊢ _e_1 _e_2 : τ

   

T-Set

*D*1; Γ; Σ ⊢ _l_ ⊴: Ψρ    *D*2; Γ; Σ ⊢ _e_ ⊴: ρ

*D*1 ∪ *D*2; Γ; Σ ⊢ _l_ := _e_ : unit

T-If

*D*1; Γ; Σ ⊢ _e_1 ⊴: bool    *D*2; Γ; Σ ⊢ _e_2 ⊴: τ    *D*3; Γ; Σ ⊢ _e_3 ⊴: τ    τ′ ⊴: τ

*D*1 ∪ *D*2 ∪ *D*3; Γ; Σ ⊢ if  _e_1 then _e_2 else _e_3 : τ′

   

T-Deref

*D*; Γ; Σ ⊢ _e_ ⊴: ⇑τ

*D*; Γ; Σ ⊢ _e_^ : τ

T-Pair

*D*1; Γ; Σ ⊢ _e_1 ⊴: τ1    *D*2; Γ; Σ ⊢ _e_2 ⊴: τ2    τ′1 ⊴: τ1    τ′2 ⊴: τ2

*D*1 ∪ *D*2; Γ; Σ ⊢ (_e_1, _e_2) : τ′1 ✗ τ′2

  

T-Sel

*D*; Γ; Σ ⊢ _e_ : τ    *N*?(?τ?)? =▾ τ1 ✗ τ2

*D*; Γ; Σ ⊢ _e_.i : τi

T-Dup

*D*; Γ; Σ ⊢ _e_ ⊴: τ    τ′ ⊴: τ    *P*?(?_e_,  τ′?)?

*D*; Γ; Σ ⊢ dup(_e_) : ⇑τ′

  

T-Let-M

*D*1; Γ; Σ ⊢ _e_1 ⊴: τ1    τ ⊴: τ1    *P*?(?_x_,  τ1?)?    *D*2; Γ, _x_ ↦ τ; Σ ⊢ _e_2 : τ2

*D*1 ∪ *D*2; Γ; Σ ⊢ (letψ _x_ = _e_1 in _e_2) : τ2

T-Let-MP

*D*1; Γ; Σ ⊢ υ ⊴: τ1    τ ⊴: τ1    *P*?(?_x_,  τ1?)?    *D* = *D*1 ∪ {★ϰ_x_(τ)}    {α*} = ?ftv?(τ,  *D*) ∖ ?ftv?(Γ,  Σ)

*D*2; Γ, _x_ ↦ ∀α*.τ\*D*; Σ ⊢ _e_ : τ2     ⊧new β*

*D*[β*/α*] ∪ *D*2; Γ; Σ ⊢ (letϰ _x_ = υ in _e_) : τ2


Figure 4.

Declarative Type Rules

I-Unit

Γ; Σ ⊢i () : unit | ∅

   

I-Bool

Γ; Σ ⊢i ?b? : bool | ∅

   

I-Id

Γ(_x_) = ∀α*.τ\*D*    θ = [α ↣ β]*     ⊧new β*

Γ; Σ ⊢i _x_ : θ〈τ〉 | θ〈*D*〉

I-Hloc

Σ(ℓ) = τ

Γ; Σ ⊢i ℓ : ⇑τ | ∅

   

I-Sloc

Σ(l) = τ

Γ; Σ ⊢i l : τ | ∅

   

I-Lambda

Γ, _x_ ↦ *P*?(?_x_,  β↓α?)?; Σ ⊢i _e_ : τ | *C*     ⊧new αββ′γγ′δ

Γ; Σ ⊢i λ_x_._e_ : β′↓α → γ′↓δ | *C* ∪ {τ = γ↓δ}

I-App

Γ; Σ ⊢i _e_1 : τ1 | *C*1    Γ; Σ ⊢i _e_2 : τ2 | *C*2     ⊧new αββ′γγ′δε

Γ; Σ ⊢i _e_1 _e_2 : ε↓γ | *C*1 ∪ *C*2 ∪ {τ1 = α↓(β′↓β → γ′↓γ),  τ2 = δ↓β}

   

I-Deref

Γ; Σ ⊢i _e_ : τ | *C*     ⊧new αβ

Γ; Σ ⊢i _e_^ : α | *C* ∪ {τ = β↓⇑α}

I-If

Γ; Σ ⊢i _e_1 : τ1 | *C*1    Γ; Σ ⊢i _e_2 : τ2 | *C*2    Γ; Σ ⊢i _e_3 : τ3 | *C*3     ⊧new αβγδε

Γ; Σ ⊢i if  _e_1 then _e_2 else _e_3 : ε↓γ | *C*1 ∪ *C*2 ∪ *C*3 ∪ {τ1 = α↓bool,  τ2 = β↓γ,  τ3 = δ↓γ}


I-Set

Γ; Σ ⊢i _l_ : τ1 | *C*1    Γ; Σ ⊢i _e_ : τ2 | *C*2     ⊧new αβγ

Γ; Σ ⊢i _l_ := _e_ : unit | *C*1 ∪ *C*2 ∪ {τ1 = (Ψα)↓β,  τ2 = γ↓β}

   

I-Dup

Γ; Σ ⊢i _e_ : τ | *C*    τ′ = *P*?(?_e_,  α↓β?)?     ⊧new αβγ

Γ; Σ ⊢i dup(_e_) : ⇑τ′ | *C* ∪ {τ = γ↓β}

I-Pair

Γ; Σ ⊢i _e_1 : τ1 | *C*1    Γ; Σ ⊢i _e_2 : τ2 | *C*2     ⊧new αα′ββ′γδ

Γ; Σ ⊢i (_e_1, _e_2) : α↓γ ✗ β↓δ | *C*1 ∪ *C*2 ∪ {τ1 = α′↓γ,  τ2 = β′↓δ}

   

I-Sel

Γ; Σ ⊢i _e_ : τ | *C*    τ1 = α↓β    τ2 = γ↓δ     ⊧new αβγδε

Γ; Σ ⊢i _e_.i : τi | *C* ∪ {τ = ε⇃(τ1 ✗ τ2)}

I-Let-Exp

Γ; Σ ⊢i _e_1 : τ1 | *C*1    _e_1 ≠ υ    Γ, _x_ ↦ *P*?(?_x_,  α↓β?)?; Σ ⊢i _e_2 : τ2 | *C*2     ⊧new αβγκ

Γ; Σ ⊢i letκ _x_ = _e_1 in _e_2 : τ2 | *C*1 ∪ {τ1 = γ↓β,  κ = ψ} ∪ *C*2


I-Let-Val

Γ; Σ ⊢i υ : τ1 | *C*1    *C*′1 = *C*1 ∪ {τ1 = γ↓β}    *U*(*C*′1) = (*D*u, θ)    *D* = *D*u ∪ {★κ_x_(τ)}

τ = *P*?(?_x_,  θ〈δ↓β〉?)?    {α*} = ?ftv?(τ,  *D*) ∖ ?ftv?(θ〈Γ〉,  θ〈Σ〉)    Γ, _x_ ↦ ∀α*.τ\*D*; Σ ⊢i _e_ : τ2 | *C*2     ⊧new βγδε*κ

Γ; Σ ⊢i letκ _x_ = υ in _e_ : τ2 | *C*′1[ε*/α*] ∪ *C*2


Figure 5.

Type Inference Algorithm





U-Empty *U*(∅) = (∅, 〈〉)
U-Refl *U*({τ = τ} ∪ *C*) = *U*(*C*)
U-Sym *U*({τ1 = τ2} ∪ *C*) = *U*({τ2 = τ1} ∪ *C*)
U-Var *U*({α = τ} ∪ *C*) | α ∉ τ = (*D*, θa ∘ θu) where θa = [α ↣ τ] and
*U*(Ν(θa〈*C*〉)) = (*D*, θu)
U-Fn *U*({τa → τr = τ′a → τ′r} ∪ *C*) = *U*(*C* ∪ {τa = τ′a,  τr = τ′r})
U-Ref *U*({⇑τ1 = ⇑τ2} ∪ *C*) = *U*(*C* ∪ {τ1 = τ2})
U-Mut *U*({Ψρ1 = Ψρ2} ∪ *C*) = (*D*, θu ∘ θm) where *M*?(?θu〈τ1〉?)? = θm and
*U*(*C* ∪ {ρ1 = ρ2}) = (*D*, θu)
U-Pair *U*({τ1 ✗ τ2 = τ′1 ✗ τ′2} ∪ *C*) = *U*(*C* ∪ {τ1 = τ′1,  τ2 = τ′2})
U-Const1 *U*({⌊τ1⌋ = ⌊τ2⌋} ∪ *C*) = *U*(*C* ∪ {τ1 =∘ τ2})
U-Const2 *U*({⌊τ1⌋ = τ2} ∪ *C*) = *U*(*C* ∪ {*N*?(?τ1?)? = τ2})
where *N*?(?τ1?)? ≠ τ1
U-Ct1 *U*({α⇃ρ1 = β⇃ρ2} ∪ *C*) = *U*(*C* ∪ {ρ1 =▾ ρ2,  α = β})
U-Ct2 *U*({α⇃ρ = ρ′} ∪ *C*) = *U*(*C* ∪ {ρ =▾ ρ′,  α = ρ′})
U-Ct3 *U*({α↓ρ1 = ς↓ρ2} ∪ *C*) = *U*(*C* ∪ {ρ1 =∘ ρ2,  α = ς})
U-Ct4 *U*({Ψα↓ρ1 = Ψβ↓ρ2} ∪ *C*) = *U*(*C* ∪ {ρ1 =∘ ρ2,  α = β})
U-Ct5 *U*({ς↓ρ = ϱ} ∪ *C*) = *U*(*C* ∪ {ρ =∘ ϱ,  ς = ϱ})
U-K *U*({κ = ϰ} ∪ *C*) = (*D*, θk ∘ θu) where θk = [κ ↣ ϰ] and
*U*(θk〈*C*〉) = (*D*, θu)
U-Om1 *U*({★ψ_x_(τ1),  ★ψ_x_(τ2)} ∪ *C*) = (*D* ∪ θ{★ψ_x_(τ1),  ★ψ_x_(τ2)}, θ) where
*U*(*C* ∪ {τ1 = τ2}) = (*D*, θ)
U-Op1 *U*({★∀_x_(τ)} ∪ *C*) | □(τ) = (*D* ∪ θ{★∀_x_(τ)}, θ) where
*U*(*C* ∪ {τ = *I*(τ)}) = (*D*, θ)
U-Om2 *U*({★κ_x_(τ)} ∪ *C*) | ?Mut??(?τ?)? = (*D*, θk ∘ θu) where θk = [κ ↣ ψ] and
*U*(θk〈{★κ_x_(τ)} ∪ *C*〉) = (*D*, θu)
U-Op2 *U*({★κ_x_(τ1),  ★κ_x_(τ2)} ∪ *C*) = (*D*, θk ∘ θu) where θk = [κ ↣ ∀] and
where *U*({τ1 = τ2} ∪ *C*) = ⊥ *U*(θk〈{★κ_x_(τ1),  ★κ_x_(τ2)} ∪ *C*〉) = (*D*, θu)
U-Error *U*(?c? ∪ *C*) | ?c? ∉ *C*v ∪ *C*s ∪ *C*p = ⊥
*C*v = ∀ α, ς, ρ, τ, τ′  | α ∉ τ′ . {τ = τ,  α = τ′,  τ′ = α,  α⇃ρ = τ,  τ = α⇃ρ,  ς↓ρ = τ,  τ = ς↓ρ}
*C*s = ∀ ρ, ρ′, τ, τ′, τ1, τ′1  . {τ → τ1 = τ′ → τ′1,  ⇑τ = ⇑τ′,  Ψρ = Ψρ′,  ⌊τ⌋ = ⌊τ′⌋}
*C*p = ∀ _x_, κ, ϰ, τ, τ′  | ¬?Mut??(?τ′?)? . {κ = ϰ,  ★ψ_x_(τ),  ★∀_x_(τ′),  ★κ_x_(τ)}

Figure 6.

Unification Algorithm