[000A] 関数型

関数は型理論において最も基本的な概念である。関数の導入によって、仮定の下での対象をも型理論の対象にすることができ、これは型理論の表現力を飛躍的に向上させる。

[000H] 規則

$$i$$ を階数、 $A:\mathcal {U}(i)$ を型、 $B:\mathcal {U}(i)$ を仮定 $$x:A$$ の下での型とする。

-関数型(function type) $\prod _{x:A}B:\mathcal {U}(i)$ を構成できる。 $\prod _{x:A}B$ の要素を関数(function)と呼ぶ。
-仮定 $$x:A$$ の下での要素 $$b:B$$ に対し、ラムダ抽象(lambda abstraction) $\lambda x.b:\prod _{x:A}B$ を構成できる。
-要素 $f:\prod _{x:A}B$ と $$a:A$$ に対し、関数適用(function application) $f(a):B[x\mapsto a]$ を構成できる。
- $$b:B$$ を仮定 $$x:A$$ の下での要素、 $$a:A$$ を要素とする。このとき、 $(\lambda x.b)(a)\equiv b[x\mapsto a]$ と定義される。
-要素 $f:\prod _{x:A}B$ に対し、 $f\equiv \lambda x.f(x)$ と定義される。

関数型の導入により、仮定 $$x:A$$ の下での $$B$$ の要素と $\prod _{x:A}B$ 型の関数は同じように振る舞う。以降は仮定の下での要素の代わりに関数を使う。

$$B$$ が $$x:A$$ に依存しない場合は次のように略記する。

[000G] 定義

$$i$$ を階数、 $A,B:\mathcal {U}(i)$ を型とする。このとき、 $A\to B:\mathcal {U}(i)$ を $\prod _{x:A}B$ と定義する。

[000J] 記法

- $\to$ は右結合の演算子である。例えば、 $A\to B\to C$ は $A\to (B\to C)$ と読む。
- $\lambda x_{1}.\dots \lambda x_{n}.b$ は $\lambda (x_{1},\dots ,x_{n}).b$ と略記することがある。
- $f(a_{1})\dots (a_{n})$ は $f(a_{1},\dots ,a_{n})$ と略記することがある。
- $\prod _{x:A}$ の結合は弱い。例えば、 $\prod _{x:A}\prod _{y:B}C\to D$ は $\prod _{x:A}(\prod _{y:B}(C\to D))$ と読む。

引数が多い関数を適用する時、すべての引数を明示するのはいささか煩雑である。そこで、引数が他の引数の型から推論できる場合に省略できるようにする。

[000Q] 記法

$f:\prod _{\lbrace x:A\rbrace }\prod _{y:B}C$ のように引数を $\lbrace \phantom {x}\rbrace$ で囲った場合、その引数は暗黙的(implicit)であると約束する。つまり、要素 $$a:A$$ と $b:B[x\mapsto a]$ に対して、関数適用を $$f(a,b)$$ の代わりに $$a$$ を省略して $$f(b)$$ と書く。 $$B$$ の構成で $$x$$ を明示的に使う場合には実用上は曖昧性は無い。暗黙的な引数 $$a$$ だけを適用したい場合は $f\lbrace a\rbrace :\prod _{y:B[x\mapsto a]}C[x\mapsto a]$ と書く。

$A\to \mathcal {U}(i)$ 型の関数は $$A$$ で添字付けられた型の族と考えられる。

[000I] 用語

$$i$$ を階数、 $A:\mathcal {U}(i)$ を型とする。関数 $B:A\to \mathcal {U}(i)$ を $$A$$ 上の型の族(type family)と呼ぶ。

いくつかの簡単な関数の例を挙げる。

[0089] 記法

関数を定義するには次のいずれかような言い回しをする。

-関数 $f:\prod _{x:A}B(x)$ を $\lambda x.b$ と定義する。
-関数 $f:\prod _{x:A}B(x)$ を $f(x)\equiv b$ と定義する。
- $$x:A$$ を要素とする。要素 $$f(x):B(x)$$ を $$b$$ と定義する。

最後の記法において、

\(f\)

の引数のリストに現れない仮定は

\(f\)

の暗黙的引数([000J])と解釈する。

[0010] 例

$$i$$ を階数、 $A:\mathcal {U}(i)$ を型とする。恒等関数(identity function) $\mathord {\textnormal {\textsf {id}}}:A\to A$ を $\mathord {\textnormal {\textsf {id}}}(x)\equiv x$ と定義する。

[0011] 例

$$i$$ を階数、 $A,B,C:\mathcal {U}(i)$ を型、 $f:A\to B$ と $g:B\to C$ を関数とする。合成関数(composed function) $g\circ f:A\to C$ を $(g\circ f)(x)\equiv g(f(x))$ と定義する。

[0012] 演習

$$i$$ を階数、 $A,B,C,D:\mathcal {U}(i)$ を型、 $f:A\to B$ と $g:B\to C$ と $h:C\to D$ を関数とする。

1 $f\equiv f\circ \mathord {\textnormal {\textsf {id}}}$ であることを確かめよ。
2 $\mathord {\textnormal {\textsf {id}}}\circ f\equiv f$ であることを確かめよ。
3 $(h\circ g)\circ f\equiv h\circ (g\circ f)$ であることを確かめよ。

[0013] 例

$$i$$ を階数、 $A,B:\mathcal {U}(i)$ を型、 $C:A\to B\to \mathcal {U}(i)$ を型の族、 $f:\prod _{x:A}\prod _{y:B}C(x,y)$ を関数とする。関数 $\mathord {\textnormal {\textsf {swap}}}(f):\prod _{y:B}\prod _{x:A}C(x,y)$ を $\mathord {\textnormal {\textsf {swap}}}(f,y,x)\equiv f(x,y)$ と定義する。