blog/posts-wip/record.md

---

title: records date: 2024-06-02 tags: ['quox (language)'] ...

n-ary products to replace pairs and boxes, since the nested case expressions for nested pairs are actually really annoying.

syntax

\newcommand\CEQ{\operatorname{::=}} \begin{aligned} A, B, s, t &\CEQ \dotsb \mid ꞌ[Δ] \mid [𝔇] & \text{terms} \ e, f &\operatorname{::=} \dotsb \mid e\mathord·ℓ & \text{eliminations} \ 𝔅 &\operatorname{::=} \dotsb \mid [ \overline{ℓ=x} ] ⇒ s & \text{case bodies} \[1em] ℓ &\operatorname{::=} x \mid n & \text{labels (n ∈ ℕ)} \[1em] Δ &\operatorname{::=} \overline{π· ℓ=x : A} & \text{telescopes} \ 𝔇 &\operatorname{::=} \overline{ℓ=s} & \text{list of bindings} \ ϕ &\operatorname{::=} \overline{x=e} & \text{substitutions} \ \end{aligned}

• this replaces the box syntax. pair syntax still exists but expands to this. this means that A \times B \times C and A \times (B \times C) are no longer equivalent. i guess that's fine but it is a change.
• overlined things are comma separated.
• in Δ, π is optional and defaults to 1 like everywhere else.
• the pair syntax (x_0, \dotsc, x_n) : (x_0 : A_0) \times \dotsb \times A_n is now an abbreviation for ꞌ[0=x_0, \dotsc, n=x_n] : [0=x_0: A_0, \dotsc, n: A_n].
• instead of \operatorname{\mathsf{fst}} e and \operatorname{\mathsf{snd}} e, it's now e\mathord.0 and e\mathord.1 (and e\mathord.2, …).
• "'[0. 0 : A]" looks bad. i know.
• a telescope Δ can be used as a context by ignoring the outer labels ℓ.

typing

telescope checking

:::rulebox

Γ ⊢ Δ

:::

\frac{}{Γ ⊢ •} \qquad \frac{ Γ ⊢ Δ \qquad Γ, Δ ⊢_0 A ⇐ ★ }{ Γ ⊢ Δ, π·ℓ = x : A }

binding list checking

:::rulebox

 Γ ⊢ σ·𝔇 ⇐ Δ ⊳ Σ 

:::

 \frac{}{Γ ⊢ σ·• ⇐ • ⊳ 𝟎} 

\frac{ Γ ⊢ σ·𝔇 ⇐ Δ ⊳ Σ_𝔇 \qquad Γ ⊢ ⌊σπ⌋ · s ⇐ A[𝔇:Δ] ⊳ Σ_s }{ Γ ⊢ σ· (𝔇, ℓ = s) ⇐ (Δ, π·ℓ = x : A) ⊳ Σ_𝔇 + πΣ_s }

:::rulebox

 𝔇 : Δ = ϕ 

:::

produce a substitution from a binding list and a telescope by distributing the type annotations

\begin{aligned} • : • &= • \ (𝔇, x = s) : (Δ, π·ℓ=x : A) &= (𝔇 : Δ), (x = s ∷ A) \end{aligned}