PS

Type family

定義 Dependent type

Type family

型族のこと。つまり、全ての型の集合を $\mathbb{\ast}$ とすると

$\mathbf{L} \subseteq \mathbb{\ast}$
$A : K \rightarrow \mathbf{L}$

なる関数のこと。族の記法を使うと

$(A_a \in \mathbf{L})_{a \in K}$

特に断らない場合は、添字集合 $K$ は $\mathbb{\ast}$ の部分集合とする。

Dependent type family

Dependent type familyとは、添字集合が型になっているtype familyのこと。つまり、

$V \in \mathbb{\ast}$
$\mathbf{L} \subseteq \mathbb{\ast}$
$A : V \rightarrow \mathbf{L}$

なる関数のこと。族の記法を使うと

$(A _ x \in \mathbf{L}) _ {x \in V}$

つまり、termから型への関数である。関数適用 $A(x)$ をdependent typeという。

Singleton type family

Singleton type familyとは、次のようなdependent type familyのこと。

$(\lbrace x \rbrace \in \mathbb{\ast} ) _ {x \in V}$

つまり、 $x$ ただ一つをtermとする型を返す関数のこと。関数適用 $\lbrace x \rbrace$ をsingleton typeという。

$1(x) = \lbrace x \rbrace$

とすると

$V \cong ^ {1} 1(V)$
$x \in T \Rightarrow 1(x) \subseteq T$

参考文献