---
title: quantity polymorphism (draft)
date: 2024-04-21
tags: [quox, computer]
...


im getting sick of writing `elim` and `elimω`, and `fold` and `foldω` and—

so let's call the quantity context, uh, $Ξ$. it's just a list of bound vars.
quantity arguments have to be full expressions though because arithmetic shows
up in the typing rules

## syntax

:::texdefs
$$ \newcommand\HL{\textcolor{blueviolet}} $$
:::


$$
\begin{aligned}
D &::=
  \cdots \mid \mathtt{def} \; \mathsf{a}_{\HL{\overline α}} : A = s
  & \text{declarations} \\
e &::=
  \cdots \mid \mathsf{a}_{\HL{\overline π}}^{ℓ}
  & \text{eliminations} \\
π, ρ &::=
  𝔮 \HL{\mid α \mid π + ρ \mid π \cdot ρ}
  & \HL{\text{quantity expressions}} \\[1em]
\HL{α, β} && \HL{\text{quantity variables}} \\
𝔮 &::=
  0 \mid 1 \mid ω
  & \text{quantity constants} \\
\HL{Ξ} &\mathrel{\HL{::=}}
  \HL{\cdot \mid Ξ, α}
  & \HL{\text{quantity contexts}}
\end{aligned}
$$

- a _quantity value_ $π̃$ in a context $Ξ$ is a polynomial with variables from
  $Ξ$ and coefficients from $\{0,1,ω\}$.


## typing

:::texdefs
$$
\newcommand\FracS[2]{\frac{\;#1\;}{\;#2\;}}
\newcommand\Many[1]{\begin{gathered}#1\end{gathered}}
\newcommand\Rule[3][]{\FracS{\Many{#2}}{\Many{#3}}\;\text{\small[#1]}}
\newenvironment{Rules}
  {\begin{gathered}\newcommand\nl{\\[1em]}}
  {\end{gathered}}
$$
:::

:::rulebox
$$
\newcommand\Syn\Rightarrow \newcommand\Chk\Leftarrow
\begin{gathered}
  \HL{Ξ \mid} Ψ \mid Γ \vdash σ \cdot s \Chk A \rhd Σ \\
  \HL{Ξ \mid} Ψ \mid Γ \vdash σ \cdot e \Syn A \rhd Σ
\end{gathered}
$$
:::