PS

Singletons

Dependent type Haskell

vs. dependent types

一般に、dependent type family:

$a \in \mathbb{*}$
$(A _ v \in \mathbb{\ast}) _ {v \in a}$

を実装するのは難しい(らしい)。一方、singleton type family:

$(1 _ v \in \mathbb{\ast}) _ {v \in a} = ( \lbrace v \rbrace) _ {v}$

の実装はなんとかなるので、

$a \cong ^ {1} 1 _ a = \lbrace 1 _ v \mid v \in a \rbrace$

を満たすことから、

$A _ v = \tilde{A} _ {1 _ v}$

という関係のもと、

$\mathbb{\ast} ^ a \cong \mathbb{\ast} ^ {1 _ a}$

Promotion

Haskellはすごいことになっており

$v \in a \in \mathbb{\ast}$

というデータ型があると、コンパイラが型とkind:

- $\sqcup$ は全てのkindの集合

を自動で作るdatatype promotionという機能がある。

Singletons library

さらに、singletons libraryというのがあって

$(\text{Sing}('v) ) _ {v \in a} = ( \lbrace \text{S}v \rbrace ) _ {v}$

なるsingleton type familyを作ってくれる。

その他の重要そうな関数の定義:

$\text{sing} :: \text{Sing}('v) = \text{S}v$
$\text{fromSing}(\text{S}v) = v$
$\text{Demote}('v) = a$

参考文献