PS

Kind

定義

Kind

Type familyの集合:

$\mathbf{L} ^ {K} = K \rightarrow \mathbf{L} = \lbrace A \mid A: K \rightarrow \mathbf{L} \rbrace$

を $K$ から ${\mathbf{L}}$ へのkindという(と思う)。

Higher kind

特に、 $K$ もkindの場合、higher kindという。

$\mathbf{L} ^ {\mathbf{N} ^ {\mathbf{M}}} = \mathbf{N} ^ {\mathbf{M}} \rightarrow \mathbf{L} = (\mathbf{M} \rightarrow \mathbf{N}) \rightarrow \mathbf{L}$

Box

Haskellでは全てのkindの集合をboxというらしい。これを $\sqcup$ と書くことにする。

命題

- ただし、 $1$ はsingleton setとする。

これにより、型の集合もkindと言ってしまう。

$\mathbf{L} \in \sqcup \sim \mathbf{L} ^ {1} \in \sqcup$

参考文献