PS

If expression

圏論定義

いわゆるif文の圏論的表現。

Distributive category

$\mathcal{C}$ has finite products: $(\times, 1)$
$\mathcal{C}$ has finite coproducts: $(+, 0)$
$(A \times B) + (A \times C) \cong A \times (B + C)$

なるcategory $\mathcal{C}$ のこと。

以下、distributive category $\mathcal{C}$ について･･･

Predicate

$\mathtt{T} := \mathtt{F} := \mathbb{1}$
$p : A \to \mathtt{T} + \mathtt{F}$

Guard

$p ? := A \overset{\langle 1 _ A, p \rangle}{\to} A \times (\mathtt{T} + \mathtt{F}) \cong (A \times \mathtt{T} ) + (A \times \mathtt{F}) \overset{\pi _ A + \pi _ A}{\to} A + A$

If expression

$f : A \to B$
$g : A \to C$
$\operatorname{\mathtt{if}} p \operatorname{\mathtt{then}} f \operatorname{\mathtt{else}} g := A \overset{p?}{\to} A + A \overset{f + g}{\to} B + C$

参考文献

thesis.pdf