Types.md

Type System

Composition $$ (Q;R):(A\sim C) \qquad\text{where } \begin{cases} Q: (A\sim B)\ R: (B\sim C) \end{cases} $$

$$ [Q,R]:(\lang A, C\rang\sim \lang B,D\rang) \qquad\text{where } \begin{cases} Q: (A\sim B)\\ R:(C\sim D) \end{cases} $$

Converse $$ R: \lang x\rang \sim \lang y\rang \qquad R^{-1}:\lang y\rang \sim \lang x\rang $$

$$ \begin{align*} (R^{-1})^{-1} &= R\\ (Q ; R)^{-1} &= R^{-1} ; Q^{-1}\\ [Q, R]^{-1} &= [Q^{-1}, R^{-1}]\\ R ; R^{-1} &\neq id &\text{(in general)} \end{align*} $$

Binary Tree btree $$ \begin{align*} \text{(operator) } & R : \lang x, x\rang \sim x\ \text{(base case) } &\text{btree}1 = R\ \text{(assume) } &\text{btree}n : \lang x\rang{2^n} \sim x\ \text{(inductive case) } &\text{btree}{n+1} = \underbrace{\text{half}{m=2^n}}{\lang x\rang_{2^{n+1}}\sim\lang\lang x \rang_{2^n}, \lang x \rang_{2^n}\rang} ; \underbrace{[\text{btree}_{n}, R, \text{btree}n, R]}{\sim \lang x, x \rang} ; R \end{align*} $$

(Transpose) Conjugate $$ \begin{align*} R \text{ \ } [P, Q] &= [P, Q]^{-1} ; R ; [P, Q] \ R \text{ \\ } [P, Q] &= [Q, P]^{-1} ; R ; [P, Q]

\end{align*} $$

$$ \begin{align*} R \text{ \\ } (\text{fst } Q) &= (\text{snd }Q^{-1}) ; R; \text{fst } Q

\end{align*} $$

Triangular $\Delta$ $$ \begin{align*} \Delta_n, R &= [R^0, R^1, R^2, \dots, R^{n-1}] \ \Delta_n^\sim, R &= [R^{n-1}, \dots, R^2, R^1, R^0] \end{align*} $$

**Repeated Parallel Composition ** map n R $$ R : \lang x \rang \sim \lang y\rang \ \text{map } n , R : \lang x \rang_n\sim\lang y\rang_n = [R]_n $$

$$ \begin{align*}

\text{(base case) } & \text{map } 0, R = []

\ \text{(assume) } &\text{map } n , R : \lang xs\rang \sim \lang ys \rang

\ \text{(inductive case) } & \text{map } (n+1),R

= \underbrace{(\text{apl }(n+1))^{-1}}{\lang x, xs \rang\sim\lang x, \lang xs \rang \rang} ; \underbrace{[ R, \text{map } n]}{\lang x, \lang xs\rang\rang\sim\lang y, \lang ys\rang\rang}; \underbrace{\text{apl }(n+1)}_{\sim\lang y, ys\rang}

\end{align*} $$

Beside & Below <-> & <|> $$ P : \lang x_P, y_P\rang \sim\lang y'_P, x'_P\rang\ Q: \lang x_Q, y_Q \rang \sim \lang y'_Q, x'_Q\rang

\ P \lrarr Q : \lang x_P, \lang y_P, y_Q\rang \rang \sim \lang \lang y'_P, y'_Q\rang, x'_Q\rang \qquad \text{where } y'_P = x_Q \ P \updownarrow Q : \lang\lang x_P, x_Q\rang, y_Q\rang\sim\lang y'_P, \lang x'_P, x'_Q\rang\rang \qquad \text{where } y'_Q = y_P $$ Laws: $$ (A\lrarr B)\updownarrow(C\lrarr D) = (A\updownarrow C) \lrarr (B \updownarrow D) $$ Row row n R $$ \begin{align*} \text{(operator) } &R : \lang x, y\rang \sim \lang y', x'\rang \

\text{(base case) } & \text{row } 1, R : & \lang x, \lang y\rang\rang \sim \lang \lang y'\rang, x'\rang &= \text{snd } [-]^{-1}; R; \text{fst }[-] & \ \text{(assume) } & \text{row } n , R : & \lang x, \lang ys\rang\rang \sim \lang \lang y's\rang, x'\rang \ & R\lrarr (\text{row } n , R) : & \sim\lang x, \lang y, \lang ys \rang\rang\rang \ \text{(inductive case) } & \text{row } (n+1), R : & \lang x, \lang y, ys \rang\rang \sim \lang \lang y', y's\rang, x'\rang &= \underbrace{\text{snd }(\text{apl }n)^{-1}}{\sim\lang x, \lang y, \lang ys\rang \rang\rang } ; \underbrace{(R\lrarr \text{row } n)}{\lang x, \lang y, \lang ys\rang\rang\rang\sim\lang\lang y', \lang y's\rang\rang, x'\rang} ; \text{fst } (\text{apl } n)

\end{align*} $$

$$ R : \lang x, y\rang \sim \lang y', x'\rang \\ \text{row }n , R : \lang x, \lang y \rang_n\rang \sim\lang\lang y'\rang_n, x'\rang \\ \text{col }n, R: \lang \lang x\rang_n, y\rang\sim\lang y',\lang x'\rang\rang \\ \text{grid } m, n, R : \lang\lang x\rang_m, \lang y\rang_n\rang \sim \lang\lang y'\rang_n, \lang x'\rang_m\rang $$

$$ \text{col }n , R = (\text{row }n, R^{-1})^{-1}\\ \text{grid }m , n, R = \text{row } m, (\text{col},n, R) = \text{col},n, (\text{row } m, R) $$