What does `A[spine]` mean?
hirrolot opened this issue · 2 comments
In 03-holes/Main.hs, I wonder how is Γ ⊢ rhs : A[spine] supposed to be understood (in the documentation of inverse). The notation X[something] wasn't introduced in the same file before, so I am a bit confused. I saw this notation being used in other places to mean "something may occur free in X" or to mean "X after substitution with something", but I am not sure what is meant in our case.
The notation is for applying a parallel substitution to something. So t[s] means replacing all free variables in t with corresponding terms in s.
The typing rule for substitution is: when Γ ⊢ t : A and s : Sub Δ Γ, then Δ ⊢ t[s] : A[s]. For example, given x : Nat ⊢ (x, suc zero) : Nat × Nat and (x ↦ zero) : Sub () (x : Nat) then () ⊢ (x, suc zero)[x ↦ zero) : Nat × Nat which is equal to () ⊢ (zero, suc zero) : Nat × Nat.
Instead of (x ↦ zero) : Sub () (x : Nat), we can use the notation () ⊢ (x ↦ zero) : (x : Nat), or in general Γ ⊢ s : Δ for Γ and Δ contexts and s being a mapping from vars to terms. This suggests a connection to term typing notation: while Γ ⊢ t : A is a single term in a context, Γ ⊢ s : Δ is a sequence of terms in a context, where types of the terms are given by Δ.
or in general
Γ ⊢ s : ΔforΓandΔcontexts and s being a mapping from vars to terms
Your example () ⊢ (x ↦ zero) : (x : Nat) is more like Δ ⊢ s : Γ.