Shape-Irrelevant Dependent Types and Unification Constraints

Or:

Why Pattern Inductive Families Need Not Store Their Indices

Andreas Abel, Christoph-Simon Senjak December 2012

TODO.

1. map and foldr for RVec and IVec

2. Write typing rules

1 Syntax

Grammar.

Ann ∋ ⋆ ::= : relevant
| ˆ:  shape-irrelevant
| ÷  irrelevant
Exp ∋ r, s, t, u,
S, T, U ::= 1  unit type
| ()  unit intro
| r=s | r ˆ=s | r s  intensional equalities
| T_{1} + T_{2}  disjoint sum
| inl t | inr t | case_{T} (r){ inl ⇒ s; inr ⇒ t } disjoint sum intro/elim
| (x⋆U) → T  dependent function type
| x | λxt | r s  lambda-calculus
| (x⋆U) × T  dependent pair type
| (t_{1}, t_{2}) | unpair_{T} (t){ (·, ·) ⇒ f }  pair intro/elim
| μT  inductive type
| in t | out r | rec_{T} t  inductive type intro/elim
| B_{(Δ ⊢p ._{=}t:T)}U  unification constraint
| split r  empty type elimination
| split r in Δ̂, x. t  constraint elimination
| Set  universe of small types
Cxt ∋ Γ, Δ  ::= ⋄ | Γ. x⋆T  contexts
Pat ∋ p, q  ::= x | inl p | inr p | (p_{1}, p_{2}) | in p  patterns
UP ∋ P, Q  ::= (Δ ⊢ p ≐ t : T)  unification problem

We let \underline{Δ} denote the list of the variables bound in Δ. Thus, \underline{⋄} = ⋄ and \underline{Δ. x⋆T} = \underline{Δ}, x. The variables \underline{P} bound by a unification problem are \underline{(Δ ⊢ p ≐ t : T)} = \underline{Δ}. Further, let FV(t) be the list of free variable occurrences in term t.

Substitutions σ are maps from variables to expressions. We require that the domain dom(σ) = {x | σ(x) ≠ x} is finite. We write id for the identity substitution and [u := x] for the singleton substitution σ with dom(σ) = {x} and σ(x) = u. Capture avoiding parallel substitution of σ in t is written as juxtaposition tσ.

Operations on relevance annotations and contexts Let the linear order more irrelevant ≤ on relevance annotations be given by : ≤ ˆ: ≤ ÷. Relevance composition is given by:

⋆_{1}⋆_{2} = max(⋆_{1}, ⋆_{2})

Relevance “exponentiation”.

\begin{aligned}÷^{⊕} & = & ˆ: \\ ⋆^{⊕} & = & ⋆ & for ⋆ ≠ ÷ \end{aligned}  \begin{aligned}ˆ:^{⊖} & = & ÷ \\ ⋆^{⊖} & = & ⋆ & for ⋆ ≠ ˆ: \end{aligned}  ⋆_{1}^{⋆^{2}} = \{ \begin{matrix}: & if ⋆_{1} ≤ ⋆_{2} \\ ⋆_{1} & otherwise \end{matrix}

These operations are idempotent. −^{⊕} and ⋆_{0}^{−} are antitone, −^{⊖} and −^{⋆} are monotone. The operation −^{⊕} means going to the type world (and shape equality) and the inverse operation −^{⊖} means going to the term world (and exact equality). Further laws:

1. (⋆_{1}^{⋆^{2}})^{⋆^{3}} = ⋆_{1}^{(⋆_{2}⋆_{3})}. (Proof: If ⋆_{1} = : or ÷ ∈ {⋆_{2}, ⋆_{3}} then the result is : on both sides. Relevance level : ∈ {⋆_{2}, ⋆_{3}} is ignored in composition and is neutral as exponent. In the remaining case, ⋆_{2} = ⋆_{3} = ˆ:, and we conclude by idempotency.)

2. ⋆_{1}^{⊕} ≤ ⋆_{2} iff ⋆_{1} ≤ ⋆_{2}^{⊖} (Galois connection) iff ⋆_{1} ≤ ⋆_{2} or ⋆_{1} = ÷ and ⋆_{2} = ˆ:.

3. (⋆^{⊖})^{⊕} = ⋆^{⊕} and (⋆^{⊕})^{⊖} = ⋆^{⊖}.

4. (⋆^{⊕}_{1})^{⋆^{2}} = ⋆_{1}^{⋆^{2}^{⊖}}, in particular, (⋆^{⊕})^{ˆ:} = ⋆^{ˆ:^{⊖}} = ⋆^{÷} = :.

These operations are lifted to contexts Γ by applying them to the relevance operations of all bindings of Γ, the relevant (x:U), shape-irrelevant (x ˆ: U), and irrelevant (x ÷ U) ones. Resurrection Γ^{⊕} turns all irrelevant bindings x÷T into shape-irrelevant x ˆ: T ones. Operation Γ^{:} returns just Γ, Γ^{ˆ:} makes all shape-irrelevant bindings relevant, and Γ^{÷} makes all bindings relevant. We can extend relevance composition to include the symbols ⊕ and ⊖; let o ::= ⋆ | ⊕ | ⊖. Relevance : remains the neutral element of composition, and ÷ the dominant element. Altogether, we get a noncommutative operation with the following laws:

1. : o = o: = o and ÷ o = o ÷ = ÷.

2. ⊕⊖ = ⊖ and ⊖⊕ = ⊕.

3. ⊖ˆ: = ⊖ and ˆ:⊖ = ˆ:.

4. ⊕ˆ: = ÷, but Γ^{ˆ:⊕} is a new context operation, a kind of “decrement”, making shape-irrelevant assumptions relevant, and irrelevant ones shape-irrelevant.

We extend the relevance ordering by ÷ ≥ ⊕ ≥ : ≥ ⊖. Note that ⊕ and ˆ: are incomparable. We have ∀⋆(⋆^{o} ≤ ⋆^{o′}) iff o ≥ o′. It does not make sense to extend exponentiation to o^{o′}, since while the exponent may be an arbitrary context operation, the base must be a relevance level.

2 Declarative Presentation

Judgements.

Γ ⊢ T  T is a wellformed type in context Γ
Γ ⊢ t : T  t has type T in context Γ
Γ ⊢ T = T′ T and T′ are equal types in context Γ
Γ ⊢ t = t′ : T t and t’ are equal terms of type T in context Γ

Derived Judgements.

Δ ⊢_{Γ} p : T  p is a wellformed pattern of type T with pattern variables Δ
Γ ⊢ P  P is a well-formed unification problem in context Γ
Γ ⊢ P ⚡  unification problem P is unsolvable
Γ ⊢ P ↘ Γ′ ⊢ σ; τ unification problem P has most general solution σ, τ

Pattern typing.

Δ ⊢_{Γ} p : T :⟺ Γ ⊢ T and Γ. Δ ⊢ p : T and FV(p) = \underline{Δ}

Well-formed unification problems.

\frac{Γ ⊢ T  Γ^{ˆ:} ⊢ t : T  Γ ⊢ Δ  Δ^{ˆ:} ⊢_{Γˆ :} p : T}{Γ ⊢ (Δ ⊢ p ≐ t : T)}

Typing. Invariant: Γ ⊢ t : T implies Γ^{⊕} ⊢ T. Basic types.

\overline{Γ ⊢ 1}  \overline{Γ ⊢ () : 1}  \frac{Γ ⊢ t ∗ 1}{Γ ⊢ t = () ∗ T}

\frac{Γ ⊢ A  Γ ⊢ B}{Γ ⊢ A + B}  \frac{Γ ⊢ x : A  Γ ⊢ A  Γ ⊢ B}{Γ ⊢ (inl x) : (A + B)}  \frac{Γ ⊢ x : A  Γ ⊢ A  Γ ⊢ B}{Γ ⊢ (inr x) : (B + A)}

\frac{Γ ⊢ r : (A + B)  Γ ⊢ s : A → C  Γ ⊢ t : B → C}{Γ ⊢ (case_{C}(r)\{ inl ⇒ s; inr ⇒ t \}) : C}

\frac{Γ.x ∗ A ⊢ B}{Γ ⊢ (x ∗ A) × B}  \frac{Γ.x ∗ A ⊢ y : B}{Γ ⊢ (x, y) : ((x ∗ A) × B)}

\frac{Γ ⊢ t : (x ∗ A) × B Γ ⊢ f : (z ∗ A) → B[x := z] → C}{Γ ⊢ (unpair_{C}(t)\{ (·, ·) ⇒ f \}) : C}

Term equality.

\frac{Γ ⊢ t : T}{Γ ⊢ t = t : T}  \frac{Γ ⊢ p[x := t] : Q[x := t]  Γ ⊢ t = s : T}{Γ ⊢ p[x := s] : Q[x := s]} s, t free for x in p, Q

\frac{Γ ⊢ s = t : T}{Γ ⊢ t = s : T}  \frac{Γ ⊢ t : T}{Γ ⊢ s = t : T} s =_{βη} t

Type equality.

\frac{Γ ⊢ T}{Γ ⊢ T = T}  \frac{Γ ⊢ T [x := t]  Γ ⊢ t = u : V}{Γ ⊢ T [x := t] = T [x := u]} t, u free for x in T

\frac{Γ ⊢ x : T Γ ⊢ T = U}{Γ ⊢ x : U}

Functions.

\frac{Γ ⊢ U Γ. x⋆^{⊕}U ⊢ T}{Γ ⊢ (x⋆U) → T}

instances: \frac{Γ ⊢ U  Γ. x:U ⊢ T}{Γ ⊢ (x:U) → T}  \frac{Γ ⊢ U  Γ. x ˆ: U ⊢ T}{Γ ⊢ (xˆ:U) → T}  \frac{Γ ⊢ U  Γ. x ˆ: U ⊢ T}{Γ ⊢ (x÷U) → T}
\frac{(x ⋆ U) ∈ Γ}{Γ ⊢ x : U} ⋆ = :  \frac{Γ. x⋆U ⊢ t : T}{Γ ⊢ λxt : (x⋆U) → T}  \frac{Γ ⊢ r : (x⋆U) → T  Γ^{⋆} ⊢ u : U}{Γ ⊢ r u : T [u := x]}

Unification constraints.

\frac{Γ ⊢ (Δ ⊢ p ≐ t : T) Γ. Δ ⊢ U}{Γ ⊢ B_{(Δ ⊢p ._{=}t:T)}U}

\frac{Γ ⊢ P ↘ Γ′ ⊢ σ; τ Γ′ ⊢ u[τ] : U[τ, σ]}{Γ ⊢ u : B_{P} U}

\frac{Γ ⊢ r : B_{P} S Γ^{⊕} ⊢ P ⚡}{Γ ⊢ split r : U}

\frac{Γ ⊢ r : B_{P} S  Γ^{⊕} ⊢ P ↘ Γ′ ⊢ σ; τ  Γ′, x:S[τ, σ] ⊢ u[τ, σ] : U[τ]}{Γ ⊢ split r in \underline{P} , x. u : U}

Recursion.

\frac{Γ ⊢ t : F (μF) t⃗}{Γ ⊢ in t : μF t⃗} \frac{Γ ⊢ r : μF t⃗}{Γ ⊢ out r : F (μF) t⃗}
Γ. Δ. x:μF \underline{Δ} ⊢ C[\underline{Δ}, x]
Γ ⊢ f : (y⃗ : Δ. y : F ((Δ. x:μF \underline{Δ}y⃗) × C[\underline{Δ}, x])) → C[y⃗, in y]
Γ ⊢ rec_{\underline{Δ},x.C[\underline{Δ},x]} f : (Δ. x:μF \underline{Δ}) → C[\underline{Δ}, x]

Relevance-relative typing. Γ ⊢ t ⋆ T iff Γ^{⋆} ⊢ t : T.

Substitution typing. Γ ⊢ σ : Δ iff Γ ⊢ σ(x) ⋆ T for all (x ⋆ T) ∈ Δ. Lemma 1 (Substitution) If Γ ⊢ σ : Δ and Δ ⊢ t : T then Γ ⊢ tσ : T σ. Lemma 2 (Substitution promotion)

1. ⊕⋆_{0}^{⊕} ≥ ⋆_{0} and ⋆⋆_{0}^{⋆} ≥ ⋆_{0}.

2. If Γ ⊢ σ : Δ then Γ^{⊕} ⊢ σ : Δ^{⊕} and Γ^{⋆} ⊢ σ : Δ^{⋆}. Example 1 (Booleans)

Bool  : Set
Bool  := 1 + 1
false, true : Bool
false  := inl ()
true  := inr ()

Example 2 (Empty type)

0  : Set
0  := B_{(⋄ ⊢true ._{=}false:Bool)}1
abort_{A:Set} : 0 → A
abort_{A} r := split r

Example 3 (Option type)

Maybe  : Set → Set
Maybe  : λA. 1 + A
nothing_{A:Set}  : Maybe A
nothing_{A}  := inl ()
just_{A:Set}  : A → Maybe A
just_{A} x  := inr x
maybe_{A:Set,C[x:Maybe A]} : C[nothing] → ((y:A) → C[just y]) → (x:Maybe A) → C[x]
maybe_{A,C[x]}  := λn. λj. λx. case(x){ inl ⇒ λ . n; inr ⇒ j }

Example 4 (Natural numbers)

Nat : Set
Nat := μ Maybe
zero : Nat
zero := in nothing
suc : Nat → Nat
suc x := in (just x)

Specialized recursor for natural numbers:

natrec_{C[x:Nat]} : C[zero] → ((x:Nat) → C[x] → C[suc x]) → (x:Nat) → C[x]
natrec_{C}  := λz. λs. rec_{C} …

Example 5 (Recursive vectors)

RVec  : Set → Nat → Set
RVec  := λA. natrec _{.Set} 1 (λ . λX. A × X)
rnil_{A:Set}  : RVec A zero
rnil_{A}  := ()
rcons_{A:Set}  : (n:Nat) → A → RVec A n → RVec A (suc n)
rcons_{A} n x xs := (x, xs)

Example 6 (Inductive vectors, equality encoding)

IVec  : Set → Nat ˆ→ Set
IVec  := λA. μ λX : Nat ˆ→ Set. λn ˆ: Nat. (n ≡ zero) + (mˆ:Nat) × (n ≡ suc m) × A × X m
inil_{A:Set}  : IVec A zero
inil_{A}  := in (inl refl)
icons_{A:Set}  : (nˆ:Nat) → A → IVec A n → IVec A (suc n)
icons_{A} n x xs := in (inr (m, (refl, (x, xs))))

Example 7 (Inductive vectors, constraint encoding)

IVec  : Set → Nat ˆ→ Set
IVec  := λA. μ λX : Nat ˆ→ Set. λn ˆ: Nat.
( B_{(⋄ ⊢zero ._{=}n:Nat)}1) + ( B_{(mˆ:Nat ⊢suc m ._{=}n:Nat)}A × X m)
inil_{A:Set}  : IVec A zero
inil_{A}  := in (inl ())
icons_{A:Set}  : (n÷Nat) → A → IVec A n → IVec A (suc n)
icons_{A} n x xs := in (inr (x, xs))

Excerpts of typing derivations: Case IVec. Let Γ = A : Set. X:Nat ˆ→ Set. n ˆ: Nat.

m : Nat ⊢_{Γˆ :} suc m : Nat Γ^{ˆ:} ⊢ n : Nat

Γ ⊢ (m ˆ: Nat ⊢ suc m ≐ n : Nat)

Γ^{ˆ:}. m:Nat ⊢ m : Nat
Γ. m ˆ: Nat ⊢ X m
Γ. m ˆ: Nat ⊢ A × X m

Γ ⊢ B_{(mˆ:Nat ⊢suc m ._{=}n:Nat)}A × X m

Case icons. Let Γ = A:Set. n÷Nat. x:A. xs :IVec A n.

m ˆ: Nat ⊢_{Γ}^{a} m ≐ n : Nat ↘ Γ ⊢ id; [n/m]

m ˆ: Nat ⊢_{Γ}^{a} suc m ≐ suc n : Nat ↘ Γ ⊢ id; [n/m]

Γ ⊢ xs : IVec A n
Γ ⊢ (x, xs) : A × IVec A n
Γ ⊢ (x, xs) : ( B_{(mˆ:Nat ⊢suc m ._{=}suc n:Nat)}A × IVec A m)

3 Algorithmic Presentation

Judgements.

Γ ⊢^{a} T  T is a wellformed type in context Γ
Γ ⊢^{a} t ⇇ T  t checks against type T in context Γ
Γ ⊢^{a} r ⇉ T  r has inferred type T in context Γ
Γ ⊢^{a} P  P is a well-formed unification problem in context Γ
Δ ⊢_{Γ}^{a} p ⚡ t : T  unification of expression t and pattern p fails
Δ ⊢_{Γ}^{a} p ≐ t : T ↘ Γ′ ⊢ σ; τ expression t unifies with pattern p under m.g.u. σ, τ

Unification. Δ ⊢_{Γ}^{a} p ≐ t : T ↘ Γ′ ⊢ τ; σ

Algorithm for unification. Concatenation of pairs of substitutions are meant component-wise, concatenation with ⚡ yields ⚡. z is always a new variable which has not been used yet, q and r are placeholders for either (·, ·), or for in inl inr ignoring the second argument.

x ↘^{?} y = ([x := z], [y := z])
x ↘^{?} q(t, u) = ([x := q(t, u)[x := z]], [x := z])
q(t, u) ↘^{?} x = \{ \begin{matrix}(τ, σ) & for x ↘^{?} q(t, u) = (σ, τ) \\ ⚡ & for x ↘^{?} q(t, u) =⚡ \end{matrix}
q(t, u) ↘^{?} r(v, w) = \{ \begin{matrix}(t ↘^{?} v) ∘ (u ↘^{?} w) & for q = r \\ ⚡ & otherwise \end{matrix}

Invariants: If Γ^{⊕} ⊢ T and Γ^{⊕} ⊢ Δ and Γ^{⊕}^{ˆ:} ⊢ t : T and Δ^{ˆ:} ⊢_{Γ^{⊕}}ˆ : p : T then Γ′ ⊢ τ : Γ and Γ′^{⊕} ⊢ σ : Δτ and Γ′^{⊕}^{ˆ:} ⊢ pσ = tτ : T τ. Remember that Γ^{⊕}^{ˆ:} = Γ^{÷}.

Δ ⊢_{Γ}^{a} x ≐ t : T ↘ Γ ⊢ id; ⟨t⟩x Δ ⊢_{Γ. y⋆T,Γ′}^{a} p ≐ y : T ↘ Γ. Δ. Γ′ ⊢ ⟨p⟩y; id

References

[AS12] Andreas Abel and Gabriel Scherer. On irrelevance and algorithmic equality in predicative type theory. Logical Meth. in Comput. Sci., 8(1:29):1–36, 2012. TYPES’10 special issue.