PS

Haskell category

定義 Category

Haskell category

Haskell category*1:

$\mathcal{Hask}$

を次のように定義できる:

$\mathcal{Hask} _ 0 = \lbrace a \mid a \text{ is a Haskell type} \rbrace$
$\mathcal{Hask} _ 1 = \lbrace f \mid f \text{ is a Haskell function} \rbrace$
$\text{dom}(f:: a \rightarrow b) = a$
$\text{cod}(f:: a \rightarrow b) = b$
$g \circ f = g . f$
$\text{id} _ a = id :: a \rightarrow a$

厳密にはundefined :: forall a. aの扱いが難しいらしい。

Bottom

${} \forall a \in \mathcal{Hask} _ 0, a \ne \emptyset$

ならば、選択公理により

$\prod \mathcal{Hask} _ 0 \ne \emptyset$

ここで

$\prod \mathcal{Hask} _ 0 \big( \equiv \prod {} _ {a \in \mathcal{Hask} _ 0 } a \equiv \forall _ {a \in \mathcal{Hask} _ 0 } a \big)$

をbottom typeと言い*2、その中から元を一つ選んで $\bot$ (bottom) とする。

- $\Leftrightarrow {} \forall a \in \mathcal{Hask} _ 0, \bot _ a \in a$

公理的集合論では、bottom typeは型にならない(と思う)。

参考文献

*1:という用語があるかがまず怪しい。

*2:大変怪しい。