[000B] レコード型

レコード型は構造を記述するのに便利な型である。本書では、組み込み型としては単位型と対型を導入し、レコード型は記法として実現する。これは体系を単純なものに抑えるためである。

単位型は要素を丁度一つ持つ型である。

[000K] 規則

-単位型(unit type) $\mathbf {1}:\mathcal {U}(0)$ を構成できる。
-要素 $\mathord {\star }:\mathbf {1}$ を構成できる。
-要素 $a:\mathbf {1}$ に対し、 $a\equiv \mathord {\star }$ と定義される。

対型は要素の対を要素に持つ型である。

[000L] 規則

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

-対型(pair type) $\sum _{x:A}B(x):\mathcal {U}(i)$ を構成できる。
-要素 $$a:A$$ と $$b:B(a)$$ に対し、対(pair) $\mathord {\textnormal {\textsf {pair}}}(a,b):\sum _{x:A}B(x)$ を構成できる。
-要素 $c:\sum _{x:A}B(x)$ に対し、射影(projection) $\mathord {\textnormal {\textsf {proj}}}_{1}(c):A$ と $\mathord {\textnormal {\textsf {proj}}}_{2}(c):B(\mathord {\textnormal {\textsf {proj}}}_{1}(c))$ を構成できる。
-要素 $$a:A$$ と $$b:B(a)$$ に対し、 $\mathord {\textnormal {\textsf {proj}}}_{1}(\mathord {\textnormal {\textsf {pair}}}(a,b))\equiv a$ , $\mathord {\textnormal {\textsf {proj}}}_{2}(\mathord {\textnormal {\textsf {pair}}}(a,b))\equiv b$ と定義される。
-要素 $c:\sum _{x:A}B(x)$ に対し、 $c\equiv \mathord {\textnormal {\textsf {pair}}}(\mathord {\textnormal {\textsf {proj}}}_{1}(c),\mathord {\textnormal {\textsf {proj}}}_{2}(c))$ と定義される。

[000M] 定義

$$i$$ を階数、 $A,B:\mathcal {U}(i)$ を型とする。型 $A\times B:\mathcal {U}(i)$ を $\sum _{x:A}B$ と定義する。

[000N] 記法

- $\times$ は右結合の演算子である。例えば、 $A\times B\times C$ は $A\times (B\times C)$ と読む。
- $\sum _{x:A}$ の結合は弱い。例えば、 $\sum _{x:A}\sum _{y:B}C\times D$ は $\sum _{x:A}(\sum _{y:B}(C\times D))$ と読む。

対型を繰り返し使って得られる型の要素は何らかの構造だと考えられる。構造の成分に名前をつけるための記法を導入する。

[000O] 記法

記法 $\mathord {\textnormal {\textsf {Record}}}\mathopen {\{ \negmedspace |}x_{1}:A_{1},\dots ,x_{n}:A_{n}\mathclose {|\negmedspace \} }$ を次のように定める。

- $\mathord {\textnormal {\textsf {Record}}}\mathopen {\{ \negmedspace |}\mathclose {|\negmedspace \} }$ は $\mathbf {1}$ のこととする。
- $\mathord {\textnormal {\textsf {Record}}}\mathopen {\{ \negmedspace |}x_{1}:A_{1},\dots ,x_{n+1}:A_{n+1}\mathclose {|\negmedspace \} }$ は $\sum _{x_{1}:A_{1}}\mathord {\textnormal {\textsf {Record}}}\mathopen {\{ \negmedspace |}x_{2}:A_{2},\dots ,x_{n+1}:A_{n+1}\mathclose {|\negmedspace \} }$ のこととする。

この形の型をレコード型(record type)と呼ぶ。また、記法

\mathord {\textnormal {\textsf {record}}}\mathopen {\{ \negmedspace |}x_{1}\equiv a_{1},\dots ,x_{n}\equiv a_{n}\mathclose {|\negmedspace \} }

を次のように定める。

- $\mathord {\textnormal {\textsf {record}}}\mathopen {\{ \negmedspace |}\mathclose {|\negmedspace \} }$ は $\mathord {\star }$ のこととする。
- $\mathord {\textnormal {\textsf {record}}}\mathopen {\{ \negmedspace |}x_{1}\equiv a_{1},\dots ,x_{n+1}\equiv a_{n+1}\mathclose {|\negmedspace \} }$ は $\mathord {\textnormal {\textsf {pair}}}(a_{1},\mathord {\textnormal {\textsf {record}}}\mathopen {\{ \negmedspace |}x_{2}\equiv a_{2},\dots ,x_{n+1}\equiv a_{n+1}\mathclose {|\negmedspace \} })$ のこととする。

これらの記法は、各

a_{i}

が

A_{i}[x_{1}\mapsto a_{1},\dots ,x_{i-1}\mapsto a_{i-1}]

の要素の時に

\mathord {\textnormal {\textsf {record}}}\mathopen {\{ \negmedspace |}x_{1}\equiv a_{1},\dots ,x_{n}\equiv a_{n}\mathclose {|\negmedspace \} }

が

\mathord {\textnormal {\textsf {Record}}}\mathopen {\{ \negmedspace |}x_{1}:A_{1},\dots ,x_{n}:A_{n}\mathclose {|\negmedspace \} }

の要素になるように設計されている。さらに、

a:\mathord {\textnormal {\textsf {Record}}}\mathopen {\{ \negmedspace |}x_{1}:A_{1},\dots ,x_{n}:A_{n}\mathclose {|\negmedspace \} }

を要素、

\(y\)

を

x_{1}

から

x_{n}

のいずれかとする時、記法

\(a.y\)

を次のように定める。

- $$y$$ が $x_{1}$ の時、 $a.x_{1}$ は $\mathord {\textnormal {\textsf {proj}}}_{1}(a)$ のこととする。
- $$y$$ が $x_{2}$ から $x_{n}$ のいずれかの時、 $$a.y$$ は $(\mathord {\textnormal {\textsf {proj}}}_{2}(a)).y$ のこととする。

この記法は

a.x_{i}:A_{i}[x_{1}\mapsto a.x_{1},\dots ,x_{i-1}\mapsto a.x_{i-1}]

となるように設計されている。また、

(\mathord {\textnormal {\textsf {record}}}\mathopen {\{ \negmedspace |}x_{1}\equiv a_{1},\dots ,x_{n}\equiv a_{n}\mathclose {|\negmedspace \} }).x_{i}\equiv a_{i}

であることと

a\equiv \mathord {\textnormal {\textsf {record}}}\mathopen {\{ \negmedspace |}x_{1}\equiv a.x_{1},\dots ,x_{n}\equiv a.x_{n}\mathclose {|\negmedspace \} }

であることを確かめられる。

[000W] 記法

大きなレコード型を定義する際には、文章内で $\mathord {\textnormal {\textsf {Record}}}\mathopen {\{ \negmedspace |}x_{1}:A_{1},\dots ,x_{n}:A_{n}\mathclose {|\negmedspace \} }$ と書く代わりに縦に並べて

- $x_{1}:A_{1}$
- $\vdots$
- $x_{n}:A_{n}$

と書くことがある。レコード型の要素を定義する際にも同様に縦に並べて書くことがある。

[001T] 例

$$i$$ を階数、 $A,B:\mathcal {U}(i)$ を型とする。型 $A\leftrightarrow B:\mathcal {U}(i)$ を $\mathord {\textnormal {\textsf {Record}}}\mathopen {\{ \negmedspace |}\mathord {\textnormal {\textsf {to}}}:A\to B,\mathord {\textnormal {\textsf {from}}}:B\to A\mathclose {|\negmedspace \} }$ と定義する。 $A\leftrightarrow B$ の要素がある時、 $$A$$ と $$B$$ は論理的に同値(logically equivalent)であると言う。反射律、対称律、推移律を次のように構成できる。

- $\mathord {\textnormal {\textsf {record}}}\mathopen {\{ \negmedspace |}\mathord {\textnormal {\textsf {to}}}\equiv \mathord {\textnormal {\textsf {id}}},\mathord {\textnormal {\textsf {from}}}\equiv \mathord {\textnormal {\textsf {id}}}\mathclose {|\negmedspace \} }:A\leftrightarrow A$
- $\lambda e.\mathord {\textnormal {\textsf {record}}}\mathopen {\{ \negmedspace |}\mathord {\textnormal {\textsf {to}}}\equiv e.\mathord {\textnormal {\textsf {from}}},\mathord {\textnormal {\textsf {from}}}\equiv e.\mathord {\textnormal {\textsf {to}}}\mathclose {|\negmedspace \} }:(A\leftrightarrow B)\to (B\leftrightarrow A)$
- $\lambda (e,f).\mathord {\textnormal {\textsf {record}}}\mathopen {\{ \negmedspace |}\mathord {\textnormal {\textsf {to}}}\equiv f.\mathord {\textnormal {\textsf {to}}}\circ e.\mathord {\textnormal {\textsf {to}}},\mathord {\textnormal {\textsf {from}}}\equiv e.\mathord {\textnormal {\textsf {from}}}\circ f.\mathord {\textnormal {\textsf {from}}}\mathclose {|\negmedspace \} }:(A\leftrightarrow B)\to (B\leftrightarrow C)\to (A\leftrightarrow C)$

[001U] 演習

$$i$$ を階数、 $A_{1},A_{2},A_{3}:\mathcal {U}(i)$ を型とする。関数 $f:A_{1}\to A_{2}$ と $g:A_{2}\to A_{3}$ と $h:A_{3}\to A_{1}$ がある時、各 $A_{n}$ と $A_{m}$ は論理的に同値であることを確かめよ。

[008A] 例

$$i$$ を階数とする。型 $\mathcal {U}_{\bullet }(i):\mathcal {U}(\mathord {\textnormal {\textsf {succ}}}(i))$ を次のレコード型と定義する。

- $\mathord {\textnormal {\textsf {Carrier}}}:\mathcal {U}(i)$
- $\mathord {\textnormal {\textsf {point}}}:\mathord {\textnormal {\textsf {Carrier}}}$

\mathcal {U}_{\bullet }(i)

の要素を(階数

\(i\)

の)点付き型(pointed type)と呼ぶ。

[008B] 例

$$i$$ を階数とする。型 $\mathord {\textnormal {\textsf {Magma}}}(i):\mathcal {U}(\mathord {\textnormal {\textsf {succ}}}(i))$ を次のレコード型と定義する。

- $\mathord {\textnormal {\textsf {Carrier}}}:\mathcal {U}(i)$
- $\mathord {\textnormal {\textsf {op}}}:\mathord {\textnormal {\textsf {Carrier}}}\to \mathord {\textnormal {\textsf {Carrier}}}\to \mathord {\textnormal {\textsf {Carrier}}}$

\mathord {\textnormal {\textsf {Magma}}}(i)

の要素をマグマ(magma)と呼ぶ。

[008A]と[008B]で名前の衝突がある( $\mathord {\textnormal {\textsf {Carrier}}}$ )が、型によってどの構造について話しているのか分かるので混乱は無いだろう。

[008C] 例

$$i$$ を階数とする。型 $\mathord {\textnormal {\textsf {ReflGraph}}}(i):\mathcal {U}(\mathord {\textnormal {\textsf {succ}}}(i))$ を次のレコード型と定義する。

- $\mathord {\textnormal {\textsf {Vertex}}}:\mathcal {U}(i)$
- $\mathord {\textnormal {\textsf {Edge}}}:\mathord {\textnormal {\textsf {Vertex}}}\to \mathord {\textnormal {\textsf {Vertex}}}\to \mathcal {U}(i)$
- $\mathord {\textnormal {\textsf {refl}}}:\prod _{x:\mathord {\textnormal {\textsf {Vertex}}}}\mathord {\textnormal {\textsf {Edge}}}(x,x)$

\mathord {\textnormal {\textsf {ReflGraph}}}(i)

の要素を反射的グラフ(reflexive graph)と呼ぶ。

対型に関する基本的な関数をいくつか定義する。

[0014] 例

$$i$$ を階数、 $A:\mathcal {U}(i)$ を型、 $B:A\to \mathcal {U}(i)$ を型の族、 $C:\prod _{x:A}B(x)\to \mathcal {U}(i)$ を型の族とする。

-関数 $f:\prod _{z:\sum _{x:A}B(x)}C(\mathord {\textnormal {\textsf {proj}}}_{1}(z),\mathord {\textnormal {\textsf {proj}}}_{2}(z))$ に対し、カリー化(currying) $\mathord {\textnormal {\textsf {curry}}}(f):\prod _{x:A}\prod _{y:B(x)}C(x,y)$ を $\lambda (x,y).f(\mathord {\textnormal {\textsf {pair}}}(x,y))$ と定義する。
-関数 $g:\prod _{x:A}\prod _{y:B(x)}C(x,y)$ に対し、逆カリー化(uncurrying) $\mathord {\textnormal {\textsf {uncurry}}}(g):\prod _{z:\sum _{x:A}B(x)}C(\mathord {\textnormal {\textsf {proj}}}_{1}(z),\mathord {\textnormal {\textsf {proj}}}_{2}(z))$ を $\lambda z.g(\mathord {\textnormal {\textsf {proj}}}_{1}(z),\mathord {\textnormal {\textsf {proj}}}_{2}(z))$ と定義する。

[0015] 演習

[0014]において、 $\mathord {\textnormal {\textsf {uncurry}}}(\mathord {\textnormal {\textsf {curry}}}(f))\equiv f$ と $\mathord {\textnormal {\textsf {curry}}}(\mathord {\textnormal {\textsf {uncurry}}}(g))\equiv g$ を確かめよ。

[0016] 例

$$i$$ を階数、 $A:\mathcal {U}(i)$ を型、 $B:A\to \mathcal {U}(i)$ を型の族、 $C:\prod _{x:A}B(x)\to \mathcal {U}(i)$ を型の族とする。

-関数 $\mathord {\textnormal {\textsf {assoc}}}(C):(\sum _{z:\sum _{x:A}B(x)}C(\mathord {\textnormal {\textsf {proj}}}_{1}(z),\mathord {\textnormal {\textsf {proj}}}_{2}(z)))\to (\sum _{x:A}\sum _{y:B(x)}C(x,y))$ を $\lambda w.\mathord {\textnormal {\textsf {pair}}}(\mathord {\textnormal {\textsf {proj}}}_{1}(\mathord {\textnormal {\textsf {proj}}}_{1}(w)),\mathord {\textnormal {\textsf {pair}}}(\mathord {\textnormal {\textsf {proj}}}_{2}(\mathord {\textnormal {\textsf {proj}}}_{1}(w)),\mathord {\textnormal {\textsf {proj}}}_{2}(w)))$ と定義する。
-関数 $\mathord {\textnormal {\textsf {assoc}}}^{-1}(C):(\sum _{x:A}\sum _{y:B(x)}C(x,y))\to (\sum _{z:\sum _{x:A}B(x)}C(\mathord {\textnormal {\textsf {proj}}}_{1}(z),\mathord {\textnormal {\textsf {proj}}}_{2}(z)))$ を $\lambda w.\mathord {\textnormal {\textsf {pair}}}(\mathord {\textnormal {\textsf {pair}}}(\mathord {\textnormal {\textsf {proj}}}_{1}(w),\mathord {\textnormal {\textsf {proj}}}_{1}(\mathord {\textnormal {\textsf {proj}}}_{2}(w))),\mathord {\textnormal {\textsf {proj}}}_{2}(\mathord {\textnormal {\textsf {proj}}}_{2}(w)))$ と定義する。

[0017] 演習

[0016]において、 $\mathord {\textnormal {\textsf {assoc}}}^{-1}(C)\circ \mathord {\textnormal {\textsf {assoc}}}(C)\equiv \mathord {\textnormal {\textsf {id}}}$ と $\mathord {\textnormal {\textsf {assoc}}}(C)\circ \mathord {\textnormal {\textsf {assoc}}}^{-1}(C)\equiv \mathord {\textnormal {\textsf {id}}}$ を確かめよ。

[0018] 例

$$i$$ を階数、 $A,B:\mathcal {U}(i)$ を型とする。関数 $\mathord {\textnormal {\textsf {sym}}}(A,B):A\times B\to B\times A$ を $\lambda z.\mathord {\textnormal {\textsf {pair}}}(\mathord {\textnormal {\textsf {proj}}}_{2}(z),\mathord {\textnormal {\textsf {proj}}}_{1}(z))$ と定義する。

[0019] 演習

[0018]において、 $\mathord {\textnormal {\textsf {sym}}}(B,A)\circ \mathord {\textnormal {\textsf {sym}}}(A,B)\equiv \mathord {\textnormal {\textsf {id}}}$ であることを確かめよ。

[001A] 例

$$i$$ を階数、 $A:\mathcal {U}(i)$ を型、 $B:A\to \mathcal {U}(i)$ を型の族、 $C:\prod _{x:A}B(x)\to \mathcal {U}(i)$ を型の族とする。

-関数 $\mathord {\textnormal {\textsf {dist}}}(C):(\prod _{x:A}\sum _{y:B(x)}C(x,y))\to (\sum _{f:\prod _{x:A}B(x)}\prod _{x:A}C(x,f(x)))$ を $\lambda h.\mathord {\textnormal {\textsf {pair}}}(\lambda x.\mathord {\textnormal {\textsf {proj}}}_{1}(h(x)),\lambda x.\mathord {\textnormal {\textsf {proj}}}_{2}(h(x)))$ と定義する。
-関数 $\mathord {\textnormal {\textsf {dist}}}^{-1}(C):(\sum _{f:\prod _{x:A}B(x)}\prod _{x:A}C(x,f(x)))\to (\prod _{x:A}\sum _{y:B(x)}C(x,y))$ を $\lambda k.\lambda x.\mathord {\textnormal {\textsf {pair}}}(\mathord {\textnormal {\textsf {proj}}}_{1}(k(x)),\mathord {\textnormal {\textsf {proj}}}_{2}(k(x)))$ と定義する。

[001B] 演習

[001A]において、 $\mathord {\textnormal {\textsf {dist}}}^{-1}(C)\circ \mathord {\textnormal {\textsf {dist}}}(C)\equiv \mathord {\textnormal {\textsf {id}}}$ と $\mathord {\textnormal {\textsf {dist}}}(C)\circ \mathord {\textnormal {\textsf {dist}}}^{-1}(C)\equiv \mathord {\textnormal {\textsf {id}}}$ を確かめよ。

[002M] 演習

$$i$$ を階数、 $A:\mathcal {U}(i)$ を型とする。関数 $\mathord {\textnormal {\textsf {diag}}}(A):A\to A\times A$ であって、任意の $$a:A$$ に対して $\mathord {\textnormal {\textsf {proj}}}_{1}(\mathord {\textnormal {\textsf {diag}}}(A,a))\equiv a$ かつ $\mathord {\textnormal {\textsf {proj}}}_{2}(\mathord {\textnormal {\textsf {diag}}}(A,a))\equiv a$ となるものを構成せよ。