1.6 KiB
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}
:::