---
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}
$$