Type theory MOC

let declaration

In formal type theory and the design of functional programming languages, let declarations are a syntactic augmentation for internally expressing a substitution in-term. Specifically, the instance of the substitution rule

Γ⊢𝑎:𝐴Γ,𝑥:𝐴⊢𝑏:𝐵Γ⊢𝑏[𝑎/𝑥]:𝐵[𝑎/𝑥](S)

is superseded by

Γ⊢𝑎:𝐴Γ,𝑥:𝐴,Δ⊢𝑏:𝐵Γ⊢let 𝑥←𝑎 in 𝑏:𝐵[𝑎/𝑥](let)

In the former, both the in-term and in-type substitution occur at the level of the metatheory, whereas in the latter the in-term substitution occurs in the theory itself. Note this is different to the Π-type which internalizes substitition in terms as a type, although Π types can be used to achieve similar things. To ensure metatheoretic substitution still agrees with substitution via a let declaration, we impose the judgemental equality

Γ⊢𝑎:𝐴Γ,𝑥:𝐴,Δ⊢𝑏:𝐵Γ⊢let 𝑥←𝑎 in 𝑏=𝑏[𝑎/𝑥]:𝐵[𝑎/𝑥](let𝛽)

Beyond syntactic nicety, let declarations can be used to formulate induction rules for a positive type independently from a Π-type, see e.g. Σ type.

---

tidy | en | SemBr