読者です 読者をやめる 読者になる 読者になる

bitterharvest’s diary

A Bitter Harvestは小説の題名。作者は豪州のPeter Yeldham。苦闘の末に勝ちえた偏見からの解放は命との引換になったという悲しい物語

サーモンと玉ねぎ・ピーマンのクリーム煮

オーブン料理は簡単でよい。手間をかけずに調理できるのにもかかわらず、食卓に並べたときは高級感を醸し出してくれる。このギャップを料理人は楽しむことができる。経済的な言葉を用いれば、費用対効果に優れているということだろう。

でも、良いことばかりではなさそうだ。だんだん慣れてくるに従って、オーブン料理を敬遠するようになってきた。オーブン料理を作るときは、一つしかないスチームオーブンレンジを用いるが、このオーブンレンジは調理前も後も他の目的のために使うことができない。調理前は余熱のためなので我慢できるが、調理後の庫内の熱を冷ます時は面食らう場合が多い。オーブン料理ができた後で、レンジで温めたいと思うことが少なからずあるためだ。それも悪いことに、オーブン料理が出来上がるころに思いつくので始末に悪い。

スチームオーブンレンジの欠点を補ってくれるのがオーブントースターだ。庫内を温める必要もないし、冷ます必要もない。今回は、オーブントースターを用いて、新しい道具の利用法を開拓することにした。

デパ地下の食料品売り場で新鮮な生鮭を見つけた(2切れ購入し、等分に切った)。
f:id:bitterharvest:20170521094518j:plain
これを利用して「サーモンと玉ねぎ・ピーマンのクリーム煮」を作ることにした。サーモンと玉ねぎだけで作れるので、いたって簡単な料理である。今回は、ピーマンも加えたが、これは衝動的である。生鮭を手にした後に寄った野菜売り場で、ピーマンの安売りをしていた。一袋300円となっていたが、売り子のおばさんが袋に一杯詰めた後で、さらに5個付け加えた。袋からは完全にあふれていたが、これも一袋だからということで、甘い言葉に乗って、買ってしまった。あまりにも、たくさんのピーマンを手にしたので、これも用いることにした。

グラタン皿を二つ用意して、それぞれに。オリーブ油を小さじ1杯たらした。玉ねぎ1/4個を細切りにして、それをグラタン皿の底に敷いた。
f:id:bitterharvest:20170521094607j:plain
さらに、ピーマン1個を切って、グラタン皿に加えた。
f:id:bitterharvest:20170521094911j:plain
塩(それぞれに一つまみ)と胡椒(2,3振り)を振りかけた生鮭をグラタン皿に加えた。
f:id:bitterharvest:20170521095250j:plain
生クリーム(50mg)とサワークリーム(大匙3杯)を別の器でかき混ぜ、これに、塩、胡椒を加える。
f:id:bitterharvest:20170521095509j:plain
かき混ぜた生クリームとサワークリームを生鮭の上に加える。
f:id:bitterharvest:20170521095624j:plain
オーブントースターで12分間焼く。
f:id:bitterharvest:20170521095722j:plain
ディルを上にまぶす。
f:id:bitterharvest:20170521095814j:plain
さらに、レモンを加えて食卓に供する。
f:id:bitterharvest:20170521095927j:plain
魚臭さもなく、クリーム味を楽しむことができ、期待通り、コスト・パーフォーマンスのよい料理であった。

写像対象-カリー=ハワード同型対応

7.9 カリー=ハワード同型対応

世の中には、言い方は違っているのだが、同じことを言っているということが往々にしてある。

前回の記事で、型定理と圏論は一対一に対応づけできると説明したが、その例の一つである。さらに、もう一つ対応するものがある。それは、型定理と論理だ。

論理、型定理、圏論の関係を示すと以下のようになる。

意味 論理 型定理 圏論
真(true) \(True\) \(()\) (ユニット) 終対象
偽(false) \(False\) \(Void\) 始対象
論理積(conjunction) \(A \land B\) \((a,b)\) (デカルト積) \(A \times B\) (直積)
論理和(disjunction) \(A \lor B\) \(Either \ a \ b\) \(A + B\) (余積)
含意(implication) \(A \rightarrow B\) \(a \rightarrow b\) (関数型) \(B^A\) (指数対象)
含意除去(modus ponens) \((A \rightarrow B \land A) = B\) \((a \rightarrow b,a) = b\) \((B^A \times A) = B\)

この関係が成り立つので、プログラムの証明が可能になるが、それについてはいずれかの機会にしたいと思う。ここでは、論理、型定理、圏論の関係を示すに止めておき、次回は、自然変換(Natural Transformation)の話題に移行する。

注:\(a \rightarrow b\)はこれまでは説明しなかった。これは、すでに説明した写像対象\(A \rightarrow B\)を型に変えたものである。そして、関数の形をとっているので、関数型と呼ばれる。

写像対象-型定理(続き)

7.8 具体例

指数対象\(A^{B+C} = A^B \times A^C\)は、Haskellシグネチャで表すと、
\begin{eqnarray}
Either \ b \ c \rightarrow a \sim (b \rightarrow a, c \rightarrow a)
\end{eqnarray}
となることを前回の記事で説明した。

それでは、このシグネチャに基づいて具体例を提示することにしよう。

対象\(A,B,C\)をそれぞれ2個の文字の集まり\(\{A,B\}\)、3個の整数の集まり\(\{1,2,3\}\)、ブール値\(\{True,False\}\)としよう。

まず、左辺の
\begin{eqnarray}
Either \ b \ c \rightarrow a
\end{eqnarray}
を実現しよう。これは、\(A\)か\(B\)を入力し、\(C\)を出力する射の集まりを求めているので、次の32個の関数として実現することができる。

f1 a
  | a == Left 'A' = True 
  | a == Left 'B' = True 
  | a == Right 1  = True 
  | a == Right 2  = True 
  | a == Right 3  = True 
  | otherwise = error "not assigned"
f2 a
  | a == Left 'A' = True 
  | a == Left 'B' = True 
  | a == Right 1  = True 
  | a == Right 2  = True 
  | a == Right 3  = False 
  | otherwise = error "not assigned"
f3 a
  | a == Left 'A' = True 
  | a == Left 'B' = True 
  | a == Right 1  = True 
  | a == Right 2  = False 
  | a == Right 3  = True 
  | otherwise = error "not assigned"
f4 a
  | a == Left 'A' = True 
  | a == Left 'B' = True 
  | a == Right 1  = True 
  | a == Right 2  = False 
  | a == Right 3  = False 
  | otherwise = error "not assigned"
f5 a
  | a == Left 'A' = True 
  | a == Left 'B' = True 
  | a == Right 1  = False 
  | a == Right 2  = True 
  | a == Right 3  = True 
  | otherwise = error "not assigned"
f6 a
  | a == Left 'A' = True 
  | a == Left 'B' = True 
  | a == Right 1  = False 
  | a == Right 2  = True 
  | a == Right 3  = False 
  | otherwise = error "not assigned"
f7 a
  | a == Left 'A' = True 
  | a == Left 'B' = True 
  | a == Right 1  = False 
  | a == Right 2  = False 
  | a == Right 3  = True 
  | otherwise = error "not assigned"
f8 a
  | a == Left 'A' = True 
  | a == Left 'B' = True 
  | a == Right 1  = False 
  | a == Right 2  = False 
  | a == Right 3  = False 
  | otherwise = error "not assigned"
f9 a
  | a == Left 'A' = True 
  | a == Left 'B' = False 
  | a == Right 1  = True 
  | a == Right 2  = True 
  | a == Right 3  = True 
  | otherwise = error "not assigned"
f10 a
  | a == Left 'A' = True 
  | a == Left 'B' = False 
  | a == Right 1  = True 
  | a == Right 2  = True 
  | a == Right 3  = False 
  | otherwise = error "not assigned"
f11 a
  | a == Left 'A' = True 
  | a == Left 'B' = False 
  | a == Right 1  = True 
  | a == Right 2  = False 
  | a == Right 3  = True 
  | otherwise = error "not assigned"
f12 a
  | a == Left 'A' = True 
  | a == Left 'B' = False 
  | a == Right 1  = True 
  | a == Right 2  = False 
  | a == Right 3  = False 
  | otherwise = error "not assigned"
f13 a
  | a == Left 'A' = True 
  | a == Left 'B' = False 
  | a == Right 1  = False 
  | a == Right 2  = True 
  | a == Right 3  = True 
  | otherwise = error "not assigned"
f14 a
  | a == Left 'A' = True 
  | a == Left 'B' = False 
  | a == Right 1  = False 
  | a == Right 2  = True 
  | a == Right 3  = False 
  | otherwise = error "not assigned"
f15 a
  | a == Left 'A' = True 
  | a == Left 'B' = False 
  | a == Right 1  = False 
  | a == Right 2  = False 
  | a == Right 3  = True 
  | otherwise = error "not assigned"
f16 a
  | a == Left 'A' = True 
  | a == Left 'B' = False 
  | a == Right 1  = False 
  | a == Right 2  = False 
  | a == Right 3  = False 
  | otherwise = error "not assigned"
f17 a
  | a == Left 'A' = False 
  | a == Left 'B' = True 
  | a == Right 1  = True 
  | a == Right 2  = True 
  | a == Right 3  = True 
  | otherwise = error "not assigned"
f18 a
  | a == Left 'A' = False 
  | a == Left 'B' = True 
  | a == Right 1  = True 
  | a == Right 2  = True 
  | a == Right 3  = False 
  | otherwise = error "not assigned"
f19 a
  | a == Left 'A' = False 
  | a == Left 'B' = True 
  | a == Right 1  = True 
  | a == Right 2  = False 
  | a == Right 3  = True 
  | otherwise = error "not assigned"
f20 a
  | a == Left 'A' = False 
  | a == Left 'B' = True 
  | a == Right 1  = True 
  | a == Right 2  = False 
  | a == Right 3  = False 
  | otherwise = error "not assigned"
f21 a
  | a == Left 'A' = False 
  | a == Left 'B' = True 
  | a == Right 1  = False 
  | a == Right 2  = True 
  | a == Right 3  = True 
  | otherwise = error "not assigned"
f22 a
  | a == Left 'A' = False 
  | a == Left 'B' = True 
  | a == Right 1  = False 
  | a == Right 2  = True 
  | a == Right 3  = False 
  | otherwise = error "not assigned"
f23 a
  | a == Left 'A' = False 
  | a == Left 'B' = True 
  | a == Right 1  = False 
  | a == Right 2  = False 
  | a == Right 3  = True 
  | otherwise = error "not assigned"
f24 a
  | a == Left 'A' = False 
  | a == Left 'B' = True 
  | a == Right 1  = False 
  | a == Right 2  = False 
  | a == Right 3  = False 
  | otherwise = error "not assigned"
f25 a
  | a == Left 'A' = False 
  | a == Left 'B' = False 
  | a == Right 1  = True 
  | a == Right 2  = True 
  | a == Right 3  = True 
  | otherwise = error "not assigned"
f26 a
  | a == Left 'A' = False 
  | a == Left 'B' = False 
  | a == Right 1  = True 
  | a == Right 2  = True 
  | a == Right 3  = False 
  | otherwise = error "not assigned"
f27 a
  | a == Left 'A' = False 
  | a == Left 'B' = False 
  | a == Right 1  = True 
  | a == Right 2  = False 
  | a == Right 3  = True 
  | otherwise = error "not assigned"
f28 a
  | a == Left 'A' = False 
  | a == Left 'B' = False 
  | a == Right 1  = True 
  | a == Right 2  = False 
  | a == Right 3  = False 
  | otherwise = error "not assigned"
f29 a
  | a == Left 'A' = False 
  | a == Left 'B' = False 
  | a == Right 1  = False 
  | a == Right 2  = True 
  | a == Right 3  = True 
  | otherwise = error "not assigned"
f30 a
  | a == Left 'A' = False 
  | a == Left 'B' = False 
  | a == Right 1  = False 
  | a == Right 2  = True 
  | a == Right 3  = False 
  | otherwise = error "not assigned"
f31 a
  | a == Left 'A' = False 
  | a == Left 'B' = False 
  | a == Right 1  = False 
  | a == Right 2  = False 
  | a == Right 3  = True 
  | otherwise = error "not assigned"
f32 a
  | a == Left 'A' = False 
  | a == Left 'B' = False 
  | a == Right 1  = False 
  | a == Right 2  = False 
  | a == Right 3  = False 
  | otherwise = error "not assigned"

次に、右辺の
\begin{eqnarray}
(b \rightarrow a, c \rightarrow a)
\end{eqnarray}
を実現しよう。

まず、\(b \rightarrow a\)を実現しよう。これは次のようになる。

g1 a
  | a == 'A' = True
  | a == 'B' = True
  | otherwise = error "not assigned"
g2 a
  | a == 'A' = True
  | a == 'B' = False
  | otherwise = error "not assigned"
g3 a
  | a == 'A' = False
  | a == 'B' = True
  | otherwise = error "not assigned"
g4 a
  | a == 'A' = False
  | a == 'B' = False
  | otherwise = error "not assigned"

同様に、\(c \rightarrow a\)を実現すると、次のようになる。

h1 a
  | a == 1 = True
  | a == 2 = True
  | a == 3 = True
  | otherwise = error "not assigned"
h2 a
  | a == 1 = True
  | a == 2 = True
  | a == 3 = False
  | otherwise = error "not assigned"
h3 a
  | a == 1 = True
  | a == 2 = False
  | a == 3 = True
  | otherwise = error "not assigned"
h4 a
  | a == 1 = True
  | a == 2 = False
  | a == 3 = False
  | otherwise = error "not assigned"
h5 a
  | a == 1 = False
  | a == 2 = True
  | a == 3 = True
  | otherwise = error "not assigned"
h6 a
  | a == 1 = False
  | a == 2 = True
  | a == 3 = False
  | otherwise = error "not assigned"
h7 a
  | a == 1 = False
  | a == 2 = False
  | a == 3 = True
  | otherwise = error "not assigned"
h8 a
  | a == 1 = False
  | a == 2 = False
  | a == 3 = False
  | otherwise = error "not assigned"

右辺はこれらのデカルト積となるので、次の32個の関数として実現される。

p1 a b  = ((g1 a), (h1 b)) 
p2 a b  = ((g1 a), (h2 b)) 
p3 a b  = ((g1 a), (h3 b)) 
p4 a b  = ((g1 a), (h4 b)) 
p5 a b  = ((g1 a), (h5 b)) 
p6 a b  = ((g1 a), (h6 b)) 
p7 a b  = ((g1 a), (h7 b)) 
p8 a b  = ((g1 a), (h8 b)) 
p9 a b  = ((g2 a), (h1 b)) 
p10 a b = ((g2 a), (h2 b)) 
p11 a b = ((g2 a), (h3 b)) 
p12 a b = ((g2 a), (h4 b)) 
p13 a b = ((g2 a), (h5 b)) 
p14 a b = ((g2 a), (h6 b)) 
p15 a b = ((g2 a), (h7 b)) 
p16 a b = ((g2 a), (h8 b)) 
p17 a b = ((g3 a), (h1 b)) 
p18 a b = ((g3 a), (h2 b)) 
p19 a b = ((g3 a), (h3 b)) 
p20 a b = ((g3 a), (h4 b)) 
p21 a b = ((g3 a), (h5 b)) 
p22 a b = ((g3 a), (h6 b)) 
p23 a b = ((g3 a), (h7 b)) 
p24 a b = ((g3 a), (h8 b)) 
p25 a b = ((g4 a), (h1 b)) 
p26 a b = ((g4 a), (h2 b)) 
p27 a b = ((g4 a), (h3 b)) 
p28 a b = ((g4 a), (h4 b)) 
p29 a b = ((g4 a), (h5 b)) 
p30 a b = ((g4 a), (h6 b)) 
p31 a b = ((g4 a), (h7 b)) 
p32 a b = ((g4 a), (h8 b)) 

このように、左辺、右辺ともに32個の関数で実現され、これらの関数は1対1に対応させることができ、同型写像(Isomorphism)であることが分かる。

少しだけ、実行してみよう。

*Main> f27 (Left 'A')
False
*Main> f27 (Right 1)
True
*Main> p27 'A' 1
(False,True)

写像対象-型定理

7.7 型定理(Type Theory)

型定理という言葉に戸惑う人も多いことと思う。日本語版のウィキペディア型理論を検索するとあまりにも短い記述にがっかりするだろう。得られる情報も余りない。しかし、さすがに英語版の方には詳しく書いてある。その記述の中に、圏論との関係についての記述がある。その中で、ジョン・ベル(John Lane Bell)が「圏は、ある種の型定理と見なすことができる」と書いていると紹介されている。その紹介に続いて、対象を型に変更すれば、圏は型定理になるとも書かれている。

対象を型に変えるという表現はどこかで見たような気がしないだろうか。そう、圏論Haskellに変えるときに使っていた表現だ。なんてことはない。圏論の定理を型定理で解釈したほうが分かりやすい場合があることも経験的にわかっている。そこで、今回は、指数対象で成り立っている定理のいくつかについて、型定理での解釈を試みよう。

例を説明する前にこれまでの復習をしておこう。

\(A \Rightarrow B\)は、ドメイン\(A\)からコドメイン\(B\)への余すところのない、また、重複することのない射の集まり(集合)であった。そして、射の集まりは圏論では対象と見なすことができるので、これに特別な名前を与えて、写像対象と呼んだ。

\(A\)が\(m\)個の要素、\(B\)が\(n\)個の要素から成り立っているとき、射の総数は\(n^m\)である。

射の総数の表し方に似せて、写像対象\(A \Rightarrow B\)を\(B^A\)と書くことにする。\(B^A\)は指数対象と呼ばれる。指数対象が射の集まりであることに注意すると、二つの指数対象\(B^A\)と\(D^C\)が与えられた時、それぞれを構成している射の総数が同じである時、二つの指数対象には1対1の関係が成り立つ。この時、二つの指数対象は同型写像(Isomorphism)が成り立つという意味において同値であるといい、\(B^A = D^C\)と記述することとする。

また、Haskellでは対象は型(タイプ)として表される。指数対象\(B^A\)は型となるが、\(A\)も\(B\)も共に型である。Haskellでは型は小文字で記述されるので、\(a\),\(b\)と記述される。これは型変数とも呼ばれる。指数対象は射の集まりなので、Haskellではシグネチャで記述され、\(B^A\)は\(a \rightarrow b\)となる。

二つの指数対象\(B^A\)と\(D^C\)が同値の時、それぞれのシグネチャは1対1に対応するので、
\begin{eqnarray}
a \rightarrow b \sim c \rightarrow d
\end{eqnarray}
と記述することにする。

それでは例を示すことにしよう。

1) \(A^{B+C}=A^B \times A^C\)

圏論では\(A^{B+C}=A^B \times A^C\)が成り立つ。これを、型定理、即ち、Haskellで解釈してみよう。

\(B+C\)は型定理では\(Either \ b \ c\)である。左辺\(A^{B+C}\)は\(B+C\)を入力とし\(A\)を出力とする射の集まりなので、型定理では\(Either \ b \ c \rightarrow a\)となる。

\(A\)と\(B\)のデカルト積、即ち、\(A \times B\)は型定理では\((a,b)\)である。右辺\(A^B \times A^C\)は二つの射の集まり\(A^B\)と\(A^C\)のデカルト積なので、型定理では\((b \rightarrow a, c \rightarrow a)\)となる。

従って、\(A^{B+C}=(A^B \times A^C)\)は型定理では
\begin{eqnarray}
Either \ b \ c \rightarrow a \sim (b \rightarrow a, c \rightarrow a)
\end{eqnarray}
といっている。

2) \(A^{B^C}=A^{B \times C}\)

左辺\(A^{B^C}\)は、\(C\)という入力から、(\(B\)を入力とし\(A\)を出力とする)射を出力とするような射の集まりなので、型定理では\(c \rightarrow (b \rightarrow a)\)となる。

右辺\(A^{B \times C}\)は、\(B \times C\)という入力から、\(A\)を出力とする射の集まりなので、型定理では\((b,c) \rightarrow a\)となる。

従って、\(A^{B^C}=A^{B \times C}\)は型定理では
\begin{eqnarray}
c \rightarrow (b \rightarrow a) \sim (b,c) \rightarrow a
\end{eqnarray}
となる。これは変数を増やすアンカリー化と変数を減らすカリー化である。

3) \((A \times B)^C=A^C \times B^C\)

左辺\((A \times B)^C\)は、\(C\)という入力から、デカルト積\(A \times B\)を出力とする射の集まりなので、型定理では\(c \rightarrow (a,b)\)となる。

右辺\(A^C \times B^C\)は、\(C\)という入力から\(A\)を出力とする射と\(C\)という入力から\(B\)を出力とする射の集まりのデカルト積なので、型定理では\((c \rightarrow a, c \rightarrow b)\)となる。

従って、\((A \times B)^C=A^C \times B^C\)は型定理では
\begin{eqnarray}
c \rightarrow (a,b) \sim (c \rightarrow a, c \rightarrow b)
\end{eqnarray}
となる。

前回説明したものについても、もう一度、挙げておこう。

4) \(A^0=1\)

左辺\(A^0\)は、\(0\)という入力から\(1\)を出力とする射の集まりである。型定理では、\(0\)は\(Void\)なので、左辺は\(Void \rightarrow a\)となる。

右辺は\(1\)である。型定理では、\(1\)はユニット\(()\)なので、右辺は\(()\)となる。

従って、\(A^0=1\)は型定理では
\begin{eqnarray}
Void \rightarrow a \sim ()
\end{eqnarray}
となる。これは、それぞれの集まりが1であることから、この関係が成り立つことが分かる。

5) \(A^1=A\)

左辺\(A^1\)は、\(1\)という入力から積\(A\)を出力とする射の集まりなので、型定理では\(() \rightarrow a\)となる。

右辺は\(A\)である。型定理では\(a\)となる。

従って、\(A^1=A\)は型定理では
\begin{eqnarray}
() \rightarrow a \sim a
\end{eqnarray}
となる。これは、それぞれの集まりが\(A\)の要素数であることから、この関係が成り立つことが分かる。

6) \(1^A=1\)

左辺\(1^A\)は、\(A\)という入力から積\(1\)を出力とする射の集まりなので、型定理では\(a \rightarrow ()\)となる。これは、終対象への写像であり、写像の総数は1である。

右辺は\(1\)である。型定理では\(()\)となる。

従って、\(1^A=1\)は型定理では
\begin{eqnarray}
a \rightarrow () \sim ()
\end{eqnarray}
となる。これは、それぞれの集まりが\(1\)であることから、この関係が成り立つことが分かる。

最後に型定理とプログラミングの関係を説明した本を紹介しておこう。Benjamin C. PierceのTypes and Programming Languagesがよいと思う(日本語訳も出ているようだ)。彼は、コンピュータ科学の人たちに向けて圏論の本も書いている。
f:id:bitterharvest:20170510203727j:plain

また、最近のホットな話題はホモトピータイプ定理(Hotomopy Type Theory)である。型の概念をさらに抽象化した数学の一分野で、いずれは、コンピュータ科学に大きな影響を及ぼすだろうと期待している。
f:id:bitterharvest:20170511072554p:plain

写像対象-指数対象

7.6 指数対象

写像対象には別の表現法がある。また、こちらの方がよく知られてもいる。それは指数対象と呼ばれる。

対象\(A\)から対象\(B\)への射の集まり\(A \Rightarrow B\)を写像対象と呼んだ。同じように射の集まりなのだが、ドメイン\(A\)を肩に、コドメイン\(B\)をその下に、即ち、\(B^A\)と記述したものを、指数対象という。写像対象と指数対象は記述の仕方が異なるだけで、意味するところは同じである。しかし、指数対象の形で記述すると、何となく馴染みやすい。これは、指数という概念を中学生の時に学ぶので、熟知しているためだ。都合のよいことに、指数対象は指数と概念を共有している。その例を示そう。

ドメイン\(A\)を変えたときに、その指数対象には射がいくつ存在するかを考えてみよう。\(B^A\)は\(A\)から\(B\)への射の集まり(集合)を表している。\(A\)を定めたとき、あるいは\(B\)を定めたとき、その射の集合がどれだけの要素からなりなっているかを考えることにしよう。その時、\(A\)と\(B\)はそれぞれその要素数を表していると考えて解釈する。

まず、ドメイン\(A\)が始対象の時を考えてみよう。Haskellでは始対象は\(Void\)と記述される。これは、ただ一つの関数\(absurd\)という関数を有していた。\(absurd :: Void -> b\)である。Haskellで確認してみる。

Prelude> import Data.Void
Prelude Data.Void> :t absurd
absurd :: Void -> a

始対象は要素を持たないので、その要素数を0である。従って、指数関数が有する射の数は\(B^0\)となる。また、射の数は1個であったので、\(B^0=1\)となる。これは、指数の定義と同じである。

ドメイン\(A\)が要素を一つだけ持つ場合を考えてみよう。これは、Haskellではユニット(Unit)と呼ばれ、\(()\)と記述される。\(()\)からコドメイン\(B\)への射は下図のようになる。
f:id:bitterharvest:20170505083030p:plain
これらの射は定数関数と呼べれるが、その数は\(B\)の要素の数となる。\(A\)の要素は一つなので1とする。そこで、指数関数が有する射の数は\(B^1\)となる。また、射の数は\(B\)個であったので、\(B^1=B\)となる。これも、指数の概念と同じである。

ドメイン\(A\)が要素を二つだけ持つ場合を考えてみよう。これは、ブール値\(\{True, False \}\)となる。このため、指数関数が有する射の数は\(B^2\)となる。射の数は\(B \times B\)個なので、\(B^2=B \times B\)となる。これも、指数の概念と同じである。
一般に、ドメイン\(A\)が要素を\(n\)個持つときは、\(B^n=\prod_{i=1}^{n}B=B \times B \times...B\)となる。

それでは、コドメインの方を変えてみよう。コドメイン空集合の時は、射を定義することができないので、\(0^A=0\)となる。やはり、指数の概念と同じである。

ドメインが一つの要素の時、即ち、終対象、Haskellではユニットの時は、下図のように、関数は一つである。
f:id:bitterharvest:20170505084656p:plain
これから、\(1^A=1\)となる。やはり、指数の概念と同じである。

この章では、数学的な厳密さを追わずに、要素数が同じということで説明したが、次の章ではもう少し数学的な概念を用いて同値であるということを明確にする。

写像対象-Haskellで表現する

7.3 写像対象とは

ここでは写像対象を定義することにしよう。前回の記事写像対象を説明するための図として下図を提示した。
f:id:bitterharvest:20170428074146p:plain
上図で、\(Z\)は最善の表現であるとすると、これは\(A\)から\(B\)への可能な写像を重なることなくすべてを含むような関数の集合であった。これは、\(A\)と\(B\)が定まれば一意に決まるので、\(A \Rightarrow B\)と表すことにしよう。\(A \Rightarrow B\)を縦方向に、\(A\)を横方向にして、その中央には、\((A \Rightarrow B) \times A\)の値を計算する関数を定義する(先の記事ではこれを表で表したが、より、一般的にするため関数とした)。この関数は一意的に定まるので\(eval\)で表す。即ち、上記の図で、\(Z\)は\(A \Rightarrow B\)で表し、\(g\)を\(eval\)で表す。そして、\(Z\)と\(g\)が空席になったので、\(Z’\)は\(Z\)で\(g’\)は\(g\)で書き換えると、下記の互換図を得る。
f:id:bitterharvest:20170503144407p:plain
この図で、\(A \Rightarrow B\)は関数の集合である。このため、これは対象とみなすことができる。そこで、これを関数対象と呼ぶことにする。なお、上の図が股間図であることから、\(g\)には次のことが成り立つことが分かる。
\begin{eqnarray}
g = eval \circ (h \times id)
\end{eqnarray}
である。

そこで、上記の互換図を圏として表しておこう。
①対象:\(A\), \(B\), \(Z\), \(A \Rightarrow B\), \(Z \times A\), \((A \Rightarrow B) \times A\)
②射:\(h\), \(h \times id\), \(g\), \(eval\)
ドメイン、コドメイン:\(h : Z\rightarrow A \Rightarrow B\), \(h \times id : Z \times A \rightarrow (A \Rightarrow B) \times A \), \(g : Z \times A \rightarrow B\), \(eval : (A \Rightarrow B) \times A \rightarrow B\)
④恒等射:\(id_A\), \(id_B\), \(id_Z\), \(id_{A \Rightarrow B}\), \(id_{Z \times A}\), \(id_{(A \Rightarrow B) \times A}\)
⑤結合:\(g=eval \circ (h \times id)\)
また、結合律、単位律が成り立っていることは明らかである。

これで、\(A\)から\(B\)への関数の集合を写像対象として圏として表すことができた。

7.4 Haskellで表すための準備

ここで、対象\(Z\)から関数対象\(A \Rightarrow B\)への射(\(h\)をHaskellシグネチャを用いて表すことを考えよう。Haskellでは対象は型(Type)タイプで、射は関数で表す。シグネチャは関数に入力される型と出力される型を示す。
型が分かっているときは大文字で表される型名を用いる(例えば、整数という型であればInt)。また、型がその関数が利用される環境によって決まるときは小文字の型変数を用いる。例えば、2入力、1出力の関数\(f\)のシグネチャは\(f :: (a, b) \rightarrow c\)で表される。ここで、\(a,b\)が入力、\(c\)が出力である。しかし、入力あるいは出力の中で、型が同じものについては、同じ型変数を用いる。例えば、上記で、2入力、1出力とも同じ型の場合には\(f :: (a, a) \rightarrow a\)とかく。

Haskellでは、関数は関数を入力とすることもできる。今、\(f\)が、1入力1出力の関数を入力するとき、\((a \rightarrow b) \rightarrow a \rightarrow c\)となる。この時、\((a \rightarrow b) \)は入力される関数となり、その次の\(a\)はこの関数への入力である。そして、最後の\(c\)は\(f\)の出力である。なお、型が同じ場合には型変数も同じにするのは前と同じである。

簡単な例を示そう。次のプログラムでは、関数\(dbl\)は関数\(f\)によって得られた値を倍にする。

dbl :: (Num b) => (a -> b) -> a -> b
dbl f a = f a * 2

実行してみよう。

Prelude> :load "dbl.hs"
[1 of 1] Compiling Main             ( dbl.hs, interpreted )
Ok, modules loaded: Main.
*Main> dbl length "abc"
6
*Main> dbl sin 5
-1.917848549326277
*Main> dbl sqrt 4
4.0

ある実数の2乗を出力する関数\(f\)を定義してみよう。

f :: Floating a => (a -> a)
f = \x -> x ** 2

これを実行してみよう。

Prelude> :load "outputFunction.hs"
[1 of 1] Compiling Main             ( outputFunction.hs, interpreted )
Ok, modules loaded: Main.
*Main> f 2
4.0
*Main> f 5
25.0
*Main> f 3.4
11.559999999999999
*Main> f (-2.6)
6.760000000000001

二つの数を入力し、その積をを出力する関数\(g\)を定義してみよう。

g :: Num a => ((a, a) -> a)
g = \ (x, y) -> x * y

これを実行してみよう。

*Main> g (3,4)
12
*Main> g (3.5, 7.8)
27.3
*Main> g (-3.6, -2.5)
9.0

このように、関数の入出力で関数を用いているとき、入出力で用いられている関数は写像対象である。

7.5 写像対象をHaskellで表す

関数の入出力に関数を用いることを学んだので、写像対象の互換図に現れた射\(h\),\(g\)をHaskellシグネチャで表すと次のようになる。

h :: z -> (a -> b)
g :: (z,a) -> b

それでは、関数対象\(A \Rightarrow B\)を定義してみよう。ここでは、前回の記事で説明した例を用いる。例では、\(A\)は\(\{1,2,3\}\)は\(B\)は\(\{T,F\}\)であった。そこで、写像対象\(A \Rightarrow B\)は\(A\)から\(B\)への関数をすべて定義すればよいので、Haskellで表すと次のようになる。

f0 = \a -> case a of 
             1 -> True  
             2 -> True 
             3 -> True
             _ -> error "Not Assigned."
f1 = \a -> case a of 
             1 -> True  
             2 -> True 
             3 -> False
             _ -> error "Not Assigned."
f2 = \a -> case a of 
             1 -> True  
             2 -> False 
             3 -> True
             _ -> error "Not Assigned."
f3 = \a -> case a of 
             1 -> True  
             2 -> False 
             3 -> False
             _ -> error "Not Assigned."
f4 = \a -> case a of 
             1 -> False  
             2 -> True 
             3 -> True
             _ -> error "Not Assigned."
f5 = \a -> case a of 
             1 -> False  
             2 -> True 
             3 -> False
             _ -> error "Not Assigned."
f6 = \a -> case a of 
             1 -> False  
             2 -> False 
             3 -> True
             _ -> error "Not Assigned."
f7 = \a -> case a of 
             1 -> False  
             2 -> False 
             3 -> False
             _ -> error "Not Assigned."

次に、\(Z\)を定義しよう。これは、前回の例では以下の関数を表すものであった(但し、\(Z'\)は\(Z\)に変えてある)。
f:id:bitterharvest:20170504211155p:plain
そこで、対象\(Z\)は関数の名前の集合としよう。即ち、\(Z=\{“f’0”, “f’1”, “f’2”, “f’3”, “f’4”, “f’5”, “f’6”\}\)
次に、\(H:Z \rightarrow (A \Rightarrow B) \)を定義しよう。次のようになる。

h = \z -> case z of
             "f'0" -> f0
             "f'1" -> f1
             "f'2" -> f2
             "f'3" -> f3
             "f'4" -> f4
             "f'5" -> f4
             "f'6" -> f6
             _     -> error "Not Assigned."

さらに、\(g : Z \times A -> B\)を定義しよう。\(g = eval \circ (h \times id)\)より、次のようになる。

g (z, a) = eval (h z, a)
eval (f, a) = f a

互換図をHaskellで表すと次のようになる。
f:id:bitterharvest:20170503145058p:plain
それでは実行してみよう。

Prelude> :load "fObject.hs"
[1 of 1] Compiling Main             ( fObject.hs, interpreted )
Ok, modules loaded: Main.
*Main> g ("f'0", 1)
True
*Main> g ("f'0", 2)
True
*Main> g ("f'0", 3)
True
*Main> g ("f'1", 1)
True
*Main> g ("f'1", 2)
True
*Main> g ("f'1", 3)
False
*Main> g ("f'1", 4)
*** Exception: Not Assigned.
CallStack (from HasCallStack):
  error, called at fObject.hs:10:19 in main:Main
*Main> g ("f'2", 3)
True
*Main> g ("f'3", 1)
True
*Main> g ("f'4", 1)
False
*Main> g ("f'7", 2)
*** Exception: Not Assigned.
CallStack (from HasCallStack):
  error, called at fObject.hs:50:19 in main:Main

思い通りに機能していることが分かった。

7.5 カリー化とアンカリー化

入出力に関数を用いることを学んだが、関数は一般に\(n\)変数である。そこで、\(n\)変数の関数をそれより一つ少ない変数の関数に次のように変えることをカリー化という。即ち、最初の変数を変数とする関数の戻り値を関数として、これが残りの変数を受けて元の関数と同じ値を返すようにすることをカリー化という。いま、\(f : A_0 \times A_1 \times, ..,\times A_n \rightarrow B\) とした時、\(g : A_0 \rightarrow h\), \(h : A_1 \times A_2 \times, ..,\times A_n \rightarrow B\)となるとき、\(h\)は\(f\)をカリー化した関数と呼ばれる。 また、その逆はアンカリー化という。
カリー化とアンカリー化の例として、ここでは、2変数の関数を1変数の関数に、1変数の関数を2変数の関数に、変えることを考えよう。これを、再帰的に利用すれば、カリー化とアンカリー化を一般化できる。定義に従えば、カリー化\(curry'\)とアンカリー化\(uncurry'\)の関数は次のように定義できる。

curry' :: ((a, b) -> c) -> (a -> (b -> c))
curry' f = \ a -> (\ b -> f(a,b)) 

uncurry' :: (a -> (b -> c)) -> ((a, b) -> c)
uncurry' f = \ (a,b) -> (f a) b

\(curry'\)の定義は次のようになっている。入力が2変数\((a,b)\)出力が\(c\)である関数は、入力\(a\)を受けて、入力が\(b\)で出力が\(c\)の関数を出力する。

それでは、利用してみよう。長方形の面積を求める2入力の\(area\)という関数を定義する。そして、カリー化したときのシグネチャを求めてみよう。

Prelude> :load "curry.hs"
[1 of 1] Compiling Main             ( curry.hs, interpreted )
Ok, modules loaded: Main.
*Main> area (a,b) = a * b
*Main> :t curry area
curry area :: Num c => c -> c -> c

カリー化した時のシグネチャは \(Num c => c -> c -> c\)となっている。これは、実は\(Num c => c -> (c -> c)\)と同じである。後者の\(Num c => c -> (c -> c)\)では、最初のタイプ\(c\)の入力を与えると、関数\((c -> c)\)を得る。この関数はタイプ\(c\)の入力を与えると出力\(c\)を得ることを意味する。前者の\(Num c => c -> c -> c\)では、タイプ\(c\)の入力を与えた後で、タイプ\(c\)の入力を与えるとタイプ\(c\)の出力を得ることを意味する。従って、全者と後者は同じである。従って、期待通りにカリー化されていることが分かる。そこで、計算を実行してみよう。

*Main> area (3,4)
12
*Main> curry area 3 4
12

カリー化は、ざっくばらんにいうと、多変数の入力をバラバラにして入力することとなる。

それでは、アンカリー化についても調べてみよう。同じように、面積を求める関数area'を次のように定義する。

*Main> area' a b = a * b
*Main> :t uncurry area'
uncurry area' :: Num c => (c, c) -> c

\(area'\)の定義は、\(area' a b\) は\(area' a\)を実行して関数を得て、この関数に\(b\)を与えて面積を求めることと同じである。即ち、次のように定義しても同じである。

*Main> (area' a) b = a * b

\(area'\)をアンカリー化すると、\((c,c) -> c\)の2入力関数が得られることが分かる。

そこで、これを実行する。

*Main> area' 3 4
12
*Main> uncurry area' (3,4)
12

期待通りになっていることが分かる。

伊豆箱根鉄道駿豆線沿いの遺跡を訪ねる

伊豆箱根鉄道駿豆線東海道線三島駅から伊豆市修善寺までの19.8Kmを結び、車窓からは富士山を楽しむことができるローカル線だ。歴史的遺産が多く楽しむことができる。今回はこの路線の近くにある古い遺跡を訪れた。

三島市の中心にあるのが伊豆国分寺である。三島駅の隣の三島広小路駅から3分の近さだ。門は新しく、寺の表札も鮮やかだ。
f:id:bitterharvest:20170503211142j:plain
本堂も最近建て替えられたのか綺麗だ。
f:id:bitterharvest:20170503211238j:plain
時代はさかのぼるが、741年に聖武天皇が全国に国分僧寺国分尼寺を建立するように命を出した。伊豆国でも二つの寺が建てられた。僧寺は現在の国分寺の地に建てられたが、現在では、塔跡しか残っていない。本堂の裏に塔の跡がある。
f:id:bitterharvest:20170503211725j:plain
f:id:bitterharvest:20170503211804j:plain

伊豆仁田駅から東へ2km、歩いて25分のところに粕谷(かしや)横穴群がある。静岡県内では最大規模の横穴墓群で、300基あったのではと予想されている。横穴群は函南町の粕谷公園の中にある。子供たちの絶好の遊び場になっていたが、時折、横穴群を目当てに訪れる旅行者も見受けられた。
f:id:bitterharvest:20170503213036j:plain
6世紀から8世紀の200年間にわたって使われたそうだ。後半期には新たに墓は造られず、前からあった墓に追葬が行われたそうである。最後の頃には火葬骨を納めた例もあったとのことである。

墓の内部(玄室)は次のようになっていた。
f:id:bitterharvest:20170503213731j:plain
墓の手前(墓前域)と玄室の間は閉塞石で閉じられていたそうである。墓前域では亡くなった人の霊を慰めるために供養祭が行われたと予想されている。それを示すように、墓前域からはたくさんの土器が出土している。

また、住居跡は見つかっていないそうだが、モデル展示として弥生時代の住居跡や倉庫が展示されていた。
f:id:bitterharvest:20170503214521j:plain
f:id:bitterharvest:20170503214549j:plain

さらには埴輪もモデル展示されていた。
f:id:bitterharvest:20170503214640j:plain

最後は、駿豆線の終点の修善寺駅から旧中伊豆町の方へ4.2Km、歩くと1時間程度かかると思われるところに上白岩遺跡がある。ここは、4000年前の縄文時代中期から後期にかけての遺跡である。ここからは、縄文時代後期を中心とする大規模な配石遺構が発見された。その中に、環状配列の遺構がある。20単位ほどの環状・組石状の小配列が鎖のように連続して並べてあって、直径15mの環状になっている。
次の写真は環状配列である。
f:id:bitterharvest:20170503223839j:plain
別の角度から見ると次のようになる。
f:id:bitterharvest:20170503224023j:plain
組石の写真である。
f:id:bitterharvest:20170503224056j:plain
後ろの方には土壙の跡もある。
f:id:bitterharvest:20170503224312j:plain
環状列石の周りには土壙があり、さらにその外側に住居跡がある。
f:id:bitterharvest:20170503224203j:plain
近くには、長野県の井戸尻遺跡を参考に縄文時代の竪穴住居が復元されていた。
f:id:bitterharvest:20170503224544j:plain
f:id:bitterharvest:20170503224606j:plain
建物の内部には炉があった。
f:id:bitterharvest:20170503224647j:plain
遺跡の全体は次のようになっている。手前二つが住居跡。最後部が環状列石、その手前が組石である。
f:id:bitterharvest:20170503224813j:plain
近くに資料館があったので立ちよる。
入り口近くに、縄文時代の竪穴住居の模型があった。
f:id:bitterharvest:20170503225133j:plain
その横には環状列石の模型もあった。
f:id:bitterharvest:20170503231433j:plain
さらに進むと遺構で発見された縄文時代の土器が展示されていた。
f:id:bitterharvest:20170503225259j:plain
f:id:bitterharvest:20170503225317j:plain
顔面把手も展示されていた。
f:id:bitterharvest:20170503225426j:plain
耳飾りなどの装飾品も飾られていた。
f:id:bitterharvest:20170503225536j:plain
世界最古に属する土器片もあった。
f:id:bitterharvest:20170503225628j:plain
何か怪しい石棒も片隅に置かれていた。
f:id:bitterharvest:20170503225729j:plain

ゴールデンウィークの前半にこれらの遺跡を訪ねた。天気にも恵まれ、富士山の眺望や、柔らかい緑に覆われた里山などが目を楽しませてくれた。

今回は訪問しなかったが、駿豆線に沿って、源頼朝の配流地や、北条氏ゆかりの地、江戸後期の代官であった江川家跡、世界遺産に指定された韮山反射炉などがある。いくつかは既に見学したが、北条氏ゆかりの場所は訪問していないので、次の機会にはぜひ訪れたいと思っている。

写像対象―入門

しばらく休みを頂いたが、この間、古代史の関係の書物を読み漁った。特に、松木武彦さんの本が気に入った。
『美の考古学:古代人は何に魅せられてきたか』と『旧石器・縄文・弥生・古墳時代 列島創世記」を、また、共著だが『弥生時代って、どんな時代だったのか?』を楽しく読むことができた。日本列島の古代を知ろうとすると、中国に残されているわずかなものを除くと全く文字資料がないため、考古学的な遺跡を頼りに解明するしかない。しかし、どこそこでどのような土器が発見されたとか、どのようなタイプの墓が発見されたのかということを述べるだけでは、この時代に人々がどのように生活していたのかを伝えてはくれない。そこで、松木さんは認知考古学を導入することで、この時代の人がどのように考えて、土器や住居や墓を作ったのかを説明してくれる。無機的な世界に息吹を与えてくれ、歴史を楽しく知ることができる。
f:id:bitterharvest:20170426103102j:plain
認知考古学の系統を手繰っていくと、英国のスティーブ・ミズン(Steven Mithen)というレディング大学(University of Reading)の教授にたどり着く。彼は『心の先史時代(The Prehistory of the Mind)』、『氷河期以降(After the Ice: A Global Human History)』という本を書いている。前者はまだ読んでいないのでその内容は説明できないが、後者の本では紀元前2万年から5千年までの時代を変わったスタイルで描いている。ラボック君に世界中を旅をさせ、見聞きしたことを伝えるという手法で歴史を語らせる。もちろん、縄文時代の日本列島も訪問する。最初に降り立つのは、桜島近くの上野原遺跡だ。歯が一本もない少し年老いた女性が縄文土器を作り出す様子などを説明してくれる。上野原遺跡で発見された土器などを元に認知考古学を用いてその当時の生活を描き出してくれる。点と点のつながりでしかなかった古代の遺物がビジュアルにつながり読む人を楽しませてくれる。
f:id:bitterharvest:20170426102608j:plain
英国には別のアプローチをとる考古学者もいる。コリン・レンフルー(Colin Renfrew)だ。彼はケンブリッジ大学の教授を務めた。『先史時代と心の進化(Prehistory: The Making of the Human Mind)』、『考古学―理論・方法・実践 (Archaeology: Theories, Methods, and Practice)』を著作している。人類の進歩には2段階あって、遺伝子が進化した時代と、共通の知識の蓄積により変化した時代とがあると説明している。人類がアフリカを出る6万年前には、遺伝子的な進化は終了し、現代人と同じ遺伝子を有していたと述べている。アフリカを出た後、それぞれの地域によって異なる文化を築いたのは、共通知識の蓄積の仕方が異なったためだと説明している。
f:id:bitterharvest:20170426102428j:plain
認知考古学の助けを借りて文字がなかった時代を読み解くという方法は、圏論での関手を利用してある圏から別の圏を覗くいう方法と重なり合い、興味深かった。

他にもうひとつ面白い本があったのでそれも紹介しておこう。ここ数十年の考古学の研究の新しい流れの中で、最新技術が考古学に応用されている。その結果、これまでとは異なる見解が多く示されこともある。特に、放射性炭素14年代測定法やDNAの解読などの寄与は大きい。斎藤成也の『日本列島人の歴史』は、中学生・高校生でも楽に読めるように書かれている良書である。現代から古代の方に歴史を逆にたどっていき、最後に彼が主張する「三段階渡来モデル」の説明がある。DNAの解析結果をベースとしているので、説得力のある理論だと思う。
f:id:bitterharvest:20170426103953j:plain

これらの理論に圏論を応用できないかと考えているのだが、まだ、そこまでの準備はできていない。さて、前振りが長くなったが、これから、圏論の中でも面白い分野に属する写像対象(Functional Object, Map Object)について説明しよう。写像対象は指数対象(Exponential Object)とも呼ばれる。

7.1 集合と関数

ここから読み始める人もいると思うので、これまでの説明を前提にしないでも、理解できるように説明する。圏は、5つの構成要件と2つの条件により定義されている。その中で、重要な構成要件は対象(Objects))と射(MorphismsまたはArrows)の二つである。集合(Sets)と関数(Functions)を圏として表そうとすると、集合を対象として表すことができ、関数は射として表すことができる。

ここからしばらくは、圏論の世界を離れて集合と関数の世界で話をすることにしよう。

集合と関数の関係は次のように決められている。関数\(f\)はある集合\(A\)からある集合\(B\)への方向性のある対応関係を与える。そして、一つの制約がある。それは、\(A\)の全ての要素\(a\)に対して、\(B\)のある要素\(b\)が対応しなければならない。但し、\(B\)の全ての要素\(b\)に対しては対応する\(A\)の要素がなくても構わない。即ち、関数\(f:A \rightarrow B\)は次の条件を満足するものである。
\begin{eqnarray}
\forall a \in A, \exists b \in B, b = f(a)
\end{eqnarray}

\(A\)から\(B\)への関数を定義することができる(この時、\(A\)をドメイン、\(B\)をコドメインと呼ぶ)。例えば、\(A\)は\(\{1,2,3\}\)という3つの数字の集まりで、\(B\)は\(\{T,F\}\)はブール値であるとすると、可能な関数は下図に示すように8つである。
f:id:bitterharvest:20170427092305p:plain
また、

7.2 関数の集合

集合と関数を圏として表す時の最も自然な方法は、集合を対象に、関数を射とすることである。先ほどの例では、圏\(\mathcal{C}\)において、対象の集まり(対象の類)\(ob(\mathcal{C})\)は\(\{A,B\}\)であり、射の集まり(射の類)\(hom(\mathcal{C})\)は\(\{f_0,f_1,f_2,f_3,f_4,f_5,f_6,f_7\}\)である。圏として完成させるためには、この後の作業として、恒等射(\(id_A:A \rightarrow A,id_B:B \rightarrow B\))、射の合成(\(\circ\))を定め、結合律、単位律(\(id_A \circ f_i = f_i,f_i \circ id_B=f_i\)である。但し、\(i=0..7\))が成り立つようにすればよい。

集合と関数を圏として表す方法は一つではない。先の例で、\(A\)から\(B\)への関数を数え上げた。\(A\)から\(B\)への関数の集まりを集合と見なすと対象にできるのではと考えても不思議ではない。そこで、関数の集まりを\(Z=\{f_0,f_1,f_2,f_3,f_4,f_5,f_6,f_7\}\)とし、以下のように縦方向に\(Z\)を横方向を\(A\)を配置し、交わったところを\(B\)即ち\(b=f_i(a)\)となるようにして、表を作成してみよう。
f:id:bitterharvest:20170427130235p:plain
どこかで見たような表ではないだろうか。そう、デカルト積だ。デカルト積は圏として表すことができる。それは圏の積と呼ばれる。積の圏では、二つの対象が存在し、さらにその二つの対象の積も対象になる。今説明している例では、\(A\)と\(Z\)とさらにその積の\(Z \times A\)である。

積の圏はさらに\(Z \times A\)と性質を同じにする対象\(C\)を有する。数学的な説明でないが、\(Z \times A\)は最善の表現であり\(C\)はそれより劣った表現である。\(Z \times A\)はしばしば極限といわれる。極限とは何を表しているのだろう。\(\times\)は論理積を意味するときがある。\(Z \land A\)と考えると\(A\)と\(Z\)の共通部分だ。最善な共通部分とは、余すところなく共通部分を拾ったものだろう。それより劣る表現は共通部分の一部分を表したものだろう。あるいは、共通部分を二重に表現したものも劣る表現であろう(これはすぐ後で説明するが共通部分への写像が選択になるので最善とは言えなくなる)。このようなことを考えると、\(A\)と\(Z\)が整数である時、\(\times\)が共通に含まれる素数ということを表しているものと理解すると、最善な表現は最大公約数となる。そして、積の圏の場合には、\(\times\)は\(A\)から\(B\)への写像を表しているので、最善の表現は無駄のない余すことのない写像の集まりになるだろう。このように理解して次に進もう。


数学的な厳密さを用いて説明しよう(下図参照)。積の圏で\(Z \times A\)が最善の表現であるとは、どのような\(C\)を持ってきたとしても、\(C\)から\(Z \times A\)への変換\(u\)は一意に定まり、\(C\)から\(Z\)への変換は\(p'=p \circ u\)で、\(C\)から\(A\)への変換は\(q'=q \circ u\)で与えられることをいう。但し、\(p:Z \times A \rightarrow Z, q:Z \times A \rightarrow A\)である。
f:id:bitterharvest:20170428074913p:plain

次に、\(Z \times A\)と性質を同じにする対象\(C\)について話を進めよう。先の例では、\(A\)から\(B\)への写像を重複させるまたすべて含むような関数の集まりを求めた。そこで、今回は、\(A\)から\(B\)への写像をすべて含まなくてもよいし、重複してもよいということにしよう。このような関数の集まりを\(Z'\)とする。例えば、下図のようなものを作成したとする。
f:id:bitterharvest:20170427131216p:plain
この関数の集まりを\(Z'=\{f'_0,f'_1,f'_2,f'_3,f'_4,f'_5,f'_6\}\)としよう。表を作成すると次のようになる。
f:id:bitterharvest:20170427131253p:plain

この例で、\(Z'\)から\(Z\)へは次のように変換することができる。
\begin{eqnarray}
f'_0 \rightarrow f_0 \\
f'_1 \rightarrow f_1 \\
f'_2 \rightarrow f_2 \\
f'_3 \rightarrow f_3 \\
f'_4 \rightarrow f_4 \\
f'_5 \rightarrow f_4 \\
f'_6 \rightarrow f_6 \\
\end{eqnarray}

この例に限ることなく、一般にどのような関数の集まり\(Z'\)が与えられたとしても、\(Z'\)から\(Z\)への写像\(h\)を一意に定めることができる。即ち、\(Z' \times A\)から\(Z \times A\)への写像\(u=(h \times id)\)を一意に定めることができる。
f:id:bitterharvest:20170428074949p:plain

\(Z\)は特別な存在であった。即ち、これは\(A\)から\(B\)への写像を重複することなくすべてを含むような集まりであった。そしてどのような\(A\)から\(B\)への関数の集まりを持ってきたとしても\(Z'\)から\(Z\)への写像\(h\)を一意に定めることができる。積の圏では、先にも述べたが、このようなものを極限という。Milewskiの言葉を借りれば最善な表現(Best Representation)である。

しかし、互換図を見て分かると思うが、恒等射\(id\)が多すぎてあまり面白くはない。そこで、次の節で述べる関数対象を扱えるようにするために、ドメインを対象として組込み、次の互換図を用意する。
f:id:bitterharvest:20170428074146p:plain
この図で、\(Z'\)が\(Z\)より劣る表現である時、\(Z'\)から\(Z\)へ一意に定まる関数\(h\)が存在する。また、いかなる\(Z'\)に対しても、\(Z'\)から\(Z\)へ一意に定まる関数が存在するとき、\(Z\)は最善の表現と呼ぶことにする。\(Z'\)が\(Z\)より劣る表現のとき、\(Z' \times A\)から\(Z \times A\)へ一意の関数\((h \times id)\)が存在する。そして、\(Z' \times A\)から\(B\)への関数を\(g'\)とし、\(Z \times A\)から\(B\)への関数を\(g\)としたとき、\(g'=g \circ (h \times id)\)である。

これで、関数の集合\(Z\)を対象として扱う準備ができたので、次はその役割について説明しよう。

サラダたまねぎでコース料理を楽しむ

春の訪れとともに、水俣の復興に協力されている方から、新玉葱が送られてくる。これは「サラダたまねぎ」という名前で売られている。その名の通り瑞々しさが売り物だ。水俣の特産品を紹介しているブログには、「サラダたまねぎは、早い時期に収穫する(極早生)品種で、温暖な水俣・芦北地方を中心に栽培されている限定品」と書かれている。

さらにブログを手繰っていくと、「安心に対するこだわり方」というコーナーに出会う。ここには、栽培基準が紹介されている。どのような農薬がどの程度使われたかが記載されている。無農薬ではないが、極力、農薬を極力使わないようにしたいという姿勢に感激する。

頭書に「水俣病を経験した水俣だからこそ、安心して食ベていただくために事実を表示しています」と書かれている。水俣病は、1950年代から60年代に発生した公害で、有機水銀食物連鎖により人の体内に摂取されたことにより生じる疾病である。1973年の認定患者は、新潟の罹患者も含めると、3000人にも及ぶ。現時点でも完全には解決しているとは言えないとても悲惨な事件である。

さて、水俣にまつわる話はこのくらいにして、サラダたまねぎを活かしてコースの料理に挑戦してみた。前菜は「シーチキンをトッピングしたサラダたまねぎステーキ」、スープは「丸ごとサラダたまねぎスープ」、主菜は「あじの塩焼き」である。

そして、白ワイン。産地は南豪州のマクラーレン・ベール、生産者はダーレンベルグ、品種はヴィオニエとマルサンヌだ。かつてオーストラリアに住んでいた時に頻繁に訪れたワイナリーだ。横浜君嶋屋のブログを見ると、「ヴィオニエは豊かな香りと果実味の中にエスニックな一面を持ち合わせた個性派。なめらかで厚みがあり、魚貝系のグリルやカレー風味ソースなどのエスニック系味付けの料理にもおすすめ。マルサンヌは緻密ながら比較的穏やかな味わいで魚料理と好相性、特にあんこう鍋などの和食と合わせると目から鱗のマリアージュ」と書いてある。今日の料理に合いそうだ。
f:id:bitterharvest:20170401102059j:plain
それぞれの料理は作り方は単純なのだが、コース料理として食膳に供するためには、うまく手順を考えないとパニック状態になる。最初にスープの作成に取り掛かる。これは出来上がった後でも弱火で温めておける。

「丸ごとサラダたまねぎスープ」の料理に使用した材料は、サラダたまねぎ2個、コンソメ2袋、黒コショウ、水1000ccだ。二人分だ。
f:id:bitterharvest:20170401101759j:plain
また、庭にあるパセリも使用した。
f:id:bitterharvest:20170401101844j:plain
今回は、3品を同時に料理したため、料理を作成しているときの写真を撮る暇がない。文章だけで勘弁して欲しい。
鍋に水、表面の皮をむいたサラダたまねぎ、コンソメを入れて蓋をし、強火にして沸騰させる。その後、水があふれてこないように中火あるいは弱火にして、30分ほど煮る。これで終わりである。あとは出番が来るまで、冷めないように弱火で温め続ける。

「丸ごとサラダたまねぎスープ」の料理に使用した材料は、サラダたまねぎ1個、シーチキン2缶、マヨネーズ、モッツァレラチーズ、塩、胡椒である。
f:id:bitterharvest:20170401103227j:plain
サラダたまねぎを4等分に輪切りする。シーチキンは油を切った後、マヨネーズを加えて混ぜる。マヨネーズの量は味を見ながら調整する。フライパンにオリーブオイルをひき、輪切りにしたたまねぎの両面を、塩・胡椒をして、少し焦げる程度に焼く。そのあと、フライパンから取り出し、マヨネーズと混ぜたシーチキンをのせる。さらに、モッツァレラチーズを表面が隠れる程度に乗せる。オーブントースターでチーズをとろけさせるために10分ほど温める。出来上がった時が、食卓に供する時間となる。

あじは、多くの場合下ごしらえしてあるので、塩をまぶしてそのまま焼けばよい。しかし、今回、味を購入した店は安売りが売り物のお店なので下ごしらえをしてくれない。そこで、内臓を取り出し、ぜいごと呼ばれるかたいうろこを取る。その後、塩をまぶしてグリルで焼く。残念ながら写真はない。

前菜はこのような感じ。
f:id:bitterharvest:20170401105942j:plain

そして、スープは次のよう。黒胡椒をまぶし、パセリを加えて食卓に供した。
f:id:bitterharvest:20170401105758j:plain

最後は主菜。残念だが写真はない。想像の世界だ。

サラダたまねぎ満載のコース料理であった。準備している段階で、サラダたまねぎの量が多すぎるかなと懸念したが、前菜もスープも新鮮で瑞々しいサラダたまねぎを堪能することができた。不要な懸念であった。

神奈川県中央部の勝坂遺跡公園を訪ねる

相模線にゆられて縄文の遺跡を訪ねた。これは横浜から出ている相模本線ではない。JRだ。神奈川県の中央部を縦断するように、東海道線茅ヶ崎駅横浜線橋本駅の間を結んでいるローカル線だ。東京の近郊には珍しい単線運転でもある。

往きは小田急線の海老名駅で乗り換えた。小田急線の駅とJRの駅との間は連絡橋で接続されており、丹沢山塊の景色を楽しみながら渡ることができる。小田急側の駅は大きな駅で町の中心を担っていることを実感させてくれるが、JR側の駅は何とも萎びている。鉄道マニアは既に承知のことと思うが、JR線に沿ってもう一本線路が引かれている。相模本線の方から延びてきて厚木の駅までJR線と並走する。かつて、相模線は相鉄の所有であったが戦時中に国鉄に買収された。並走している線は、これを反映する歴史的な名残なのだろう。

今回、訪れたのは勝坂遺跡公園である。この遺跡は国指定の史跡になっている。最寄り駅は下溝駅である。とはいっても都心の感覚での最寄り駅ではない。田舎の感覚でとらえないと大変なことになる。電車を降りて撮った写真が以下である。
f:id:bitterharvest:20170317150807j:plain
駅員さんももちろんいない。駅を出て振り返っての写真。とてもそっけない。
f:id:bitterharvest:20170317151113j:plain
ここは相模台地の西側であり、さらにその西側を相模川が流れている。川の向こう側に見えるのが丹沢山塊である(下の写真の右側の大きな建物はヤマト運輸の厚木ゲートウェイ)。
f:id:bitterharvest:20170317151551j:plain
f:id:bitterharvest:20170317151631j:plain
相模線に沿って造られている県道46号線を南下する。道の山側にだけ幅の狭い歩道がついている。トラックの交通量が多く歩道を歩いていてもこすられそうな感じがして心地よくない。20分近く歩いたところで、勝坂遺跡公園の駐車場への案内に出会う。駐車場の脇に沿って遺跡に入る道が作られている。幅の狭い山道のようなところを進んでいく。途中には、春の訪れを知らせてくれるかのように、花大根の群れが紫色の可憐な花を咲かせていた。
f:id:bitterharvest:20170317152928j:plain
f:id:bitterharvest:20170317153103j:plain

山道を抜け台地に出ると、走り回る子供たちの大きな歓声が迎えてくれた。遠くに竪穴住居らしきものが見える何もない大きな公園だ。

近くに遺跡があったので、取り敢えずカメラに納める。敷石住居跡だ。
f:id:bitterharvest:20170317154608j:plain
温暖な気候に恵まれた縄文時代は中期末(4500年前)になると冷涼化する。これとともに、竪穴住居の構造が大きく変わり、石を敷いた住居が出現する。写真は敷き詰められた石である。石を温めることで、部屋の温度を上げたのであろう。

縄文時代は前期から中期にかけては、温暖な気候に恵まれていた。当時の生活様式は採取狩猟である。しかし、一般的な採取狩猟民とは異なり、縄文の人たちは定住生活を送っていた。森を開いて住むための空間をつくり、また、住居の周りにはドングリやクリやクルミの木を植樹して、定住しやすい環境を作っていた。住居の周りに作られた林は二次林と呼ばれるが、勝坂遺跡公園にもそれがあった。緑に生い茂っていれば想像できるのだろうが、この時期、葉が落ちてしまって隙間だらけで寂しいけれども次の写真である。
f:id:bitterharvest:20170317163039j:plain
そうこうしているうちに、公園の一番隅にある竪穴住居にたどり着いた。二つほどあったが、一つは笹で他の一つは土で屋根が葺かれていた。笹で作られた竪穴住居は4700年前ごろに作られたものの復元である。入口付近は、
f:id:bitterharvest:20170317165018j:plain
中に入ってみる。内部の壁は木で作られている。豪勢だ。また、少し奥まったところに炉が設けられている。お決まりのパターンだ。温度計と湿度計があるがもちろん当時はない。
f:id:bitterharvest:20170317165458j:plain
建物を支えている柱だ。この当時は石斧しかないので、作るのは大変だったろうと思う。f:id:bitterharvest:20170317165613j:plain
外に出て全景を取る。
f:id:bitterharvest:20170317165744j:plain
次は屋根が土で葺かれた竪穴住居だ。入口の写真を一枚。家というよりもなんとなく土で盛られた墓に入っていくような気分になる。
f:id:bitterharvest:20170317170010j:plain
炉の上に、燻製でも作るのだろうか吊るし棚があった。
f:id:bitterharvest:20170317170212j:plain
内から入口の方を見ると、
f:id:bitterharvest:20170317170327j:plain
二つの住居を一緒に撮る。
f:id:bitterharvest:20170317170500j:plain
建物跡も近くにある。
f:id:bitterharvest:20170317170618j:plain

少し離れたところに中村家住宅があることを案内で知ったのでそこに向かう。この建物は、国登録有形文化財に指定されている。幕末期の和洋折衷の珍しい建物だ。当初は三階建てだったが関東大震災後に三階部分を取り除いたそうだ。
f:id:bitterharvest:20170317171011j:plain
中村家と勝坂遺跡には因縁がある。大正15年に休暇で帰省していた学生の清水二郎が、この家の当主中村忠亮が所有する畑で散在する多数の土器を発見し、それを考古学者の大山柏(維新の元勲の大山巌は父)に標本として渡したことが、この遺跡発見の発端となった。

中村家から少し離れたところに、勝坂式土器発見の地があった。また、勝坂遺跡は相模川の小さな支流の鳩川沿いの谷戸に形成されたとのことであった。

最初に来た公園に戻り管理棟を訪れた。小さな会議ができるかなと思えるぐらいの空間であったが、そこには復元だが大山柏発掘の土器が展示されていた。
f:id:bitterharvest:20170317172812j:plain
また、この遺跡で発見された土器は、勝坂式土器と呼ばれ、中部・関東地方の縄文時代中期の指標となった。
f:id:bitterharvest:20170317173039j:plain
縄文土器は、この後の弥生式土器や古墳時代の土器と比べると重厚感にあふれている。松木武彦さんは『進化考古学の大冒険』のなかで、なぜ形は変わるのかについて説明している。それによれば、縄文時代には祭祀と調理具・食器の両方で使われたため豪華であったが、弥生時代になると後者のためだけに使われるようになり実用的な形になったと認知心理学を用いて説明している。

帰りは相模線の風景をもう少し満喫したかったので、海老名の方には戻らず、相模線をそのまま乗り継いで橋本駅に向かった。春がそこまで来ていることを知らせてくれるのどかな一日を相模の地で楽しむことができた。

プログラマーのための圏論(中)

プログラマのための圏論』は(上)の後の部分をまとめ(中)にしてPDFファイルにしました。参考にしてください。なお、(上)のホームページはこちら

関手ープロファンクタ

6.10 プロファンクタ

1)双関手の復習

プロファンクタの話をする前に、双関手を再度勉強しておこう。関手と反関手は矢印が逆向きであるという関係を有していたが、双関手とプロファンクタも同じような関係にある。

Haskellでは双関手はData.Bifunctorで定義されている。それによれば、

Prelude Data.Bifunctor> :i Bifunctor
class Bifunctor (p :: * -> * -> *) where
  bimap :: (a -> b) -> (c -> d) -> p a c -> p b d
  first :: (a -> b) -> p a c -> p b c
  second :: (b -> c) -> p a b -> p a c

このうち、\(bimap\)を図で表すと次のようになる。
f:id:bitterharvest:20170306154429p:plain

この図から分かるように、二つの対象がそれぞれの対象に対して与えられた射によって計算が行われる。双関手は\(Either\)と\( (,) \)などのデータ型に対して用意されている。

\(bimap\)はこれらのデータ型に対しては次のように定義されている。

instance Bifunctor (,) where
  bimap f g ~(a, b) = (f a, g b)

instance Bifunctor Either where
  bimap f _ (Left a) = Left (f a)
  bimap _ g (Right b) = Right (g b)

双関手になれるために少し実行してみよう。二つの関数を必要とするので、これを定義する。左側は3倍する関数としよう。また、右側は文字の長さを計算する関数としよう。

Prelude> import Data.Bifunctor
Prelude Data.Bifunctor> a =  a = bimap (*3) length

これを利用してみる。まず、タプルに対してだ。

Prelude> import Data.Bifunctor
Prelude Data.Bifunctor> a = ((*3), length)
Prelude Data.Bifunctor> a (5, "Bifunctor")
(15,9)

次は\(Either\)に対してである。

Prelude Data.Bifunctor> a (Left 5)
Left 15
Prelude Data.Bifunctor> a (Right "Either is used as a bifunctor.")
Right 30

2)プロファンクタ

プロファンクタの型クラスは次のように定義される。

class Profunctor f where
    dimap :: (a -> b) -> (c -> d) -> f b c -> f a d

図で示すと
f:id:bitterharvest:20170306154021p:plain
となる。

双関手の時の図と比較すると、\(a\)と\(b\)とが逆になっているのが分かる。今、関数\(\rightarrow\)をプロファンクタのインスタンスとすると、\(f\)のところを関数に変えればよいので、\(dimap\)は次のようになる。

instance Profunctor (->) where
  dimap :: (a -> b) -> (c -> d) -> (b -> c) -> (a -> d)
  dimap f g h = g.h.f

となる。

少し利用してみよう。

*Main Data.Bifunctor> a = dimap length odd (`div` 2)
*Main Data.Bifunctor> a "Do you like Profunctor?"
True

長かったが、関手の説明はこれで一応終了である。

関手―反関手

6.9 反関手

以前に、Readerと呼ばれる関手について説明したことがある。二つの射を得て一つの射を出力するという分かりにくい関手だったのではと想像している。圏論は、射を中心にして考えるので、射を射の入力や出力として利用するのは自然なのだが、値で慣れている場合には頭の切り替えが必要になり、分かりにくいことと思う。

そこで、Readerの復習をした後で、反関手の話をしよう。

1)射を関手にする―復習

具体的な例を用いて、前に説明したファンクタ\(Reader\)を再度考えてみる。そのため、次の問題を考えてみよう。

【問題】苗字という概念がなかったある地域\(\mathcal{C}\)で名前の文字数をカウントする関数\(f\)が用いられていたとしよう。この地域と交流のあった別の地域\(\mathcal{D}\)に、様々な技術移転が生じ、文字数をカウントする関数も他のものと一緒に移転された。しかし、\(\mathcal{D}\)での名前は氏や階級などが一緒になった複雑な構造をなしていた。数学の得意な人がいろいろと考えて、複雑な構造の名前から「名」の部分を取り出す関数\(g\)を考え出した。\(\mathcal{D}\)での名前から名の部分の文字数を得るためにはどうしたらよいかを関手を用いて説明しなさいというのがこの問題である。

それぞれの地域を圏とし、それぞれの圏の構成を下図に示す。
f:id:bitterharvest:20170305160623p:plain
\(\mathcal{C}\)では、名前を対象\(A\)で文字数を対象\(B\)で表わした。また、名前から文字数に変換する射はそのまま\(f\)である。\(\mathcal{C}\)の対象と射は関手\(F\)によって\(\mathcal{D}\)に移される。即ち、\(\mathcal{C}\)の\(A,B\)は\(F(A),F(B)\)に移され、\(f\)は\(F(f)\)に移されている。

複雑な構造の名前の対象は\(F(R)\)で表した(これは、\(\mathcal{C}\)の対象\(R\)を\(\mathcal{D}\)に移したと読める。このように意図しているのだが、\(\mathcal{C}\)にはもしかすると\(R\)は存在しないかもしれない。この問題の場合には明らかに存在しないのだ。従って、ここでは、この国の名前は\(F(R)\)であるという程度に考えて欲しい。\(F\)がついている理由はHaskellのプログラムになった時に分かる)。(同じ理由から)複雑な名前から名に変換する射を\(F(g)\)とした。ここで、求めたいのが、\(F(R)\)から\(F(B)\)への写像である。これは次のようになる。
f:id:bitterharvest:20170305160646p:plain

圏でのこの関係をHaskellで記述すると次のようになる。
f:id:bitterharvest:20170306094934p:plain
具体的にプログラムで記述すると、

{-# LANGUAGE InstanceSigs #-}
newtype Reader r a = Reader { getName :: r -> a }

instance Functor (Reader r) where
  fmap :: (a -> b) -> Reader r a -> Reader r b
  fmap f (Reader g) = Reader (f.g)

first :: (a,a,a) -> a
first (a,_,_) = a

count :: Reader (String, String, String) Int
count = fmap (length :: String -> Int) (Reader first)

smap =[("Takuya","Omi","Kimura"),("Goro","Muraji","Inagaki"),("Hiroaki","Tomonomiyakko","Nakai"),("Singo","Agatanusi","Katori")]

このプログラムで\(count\)が\(Reader \ r \ r\)即ち\(F(r)\)から\(Reader \ r \ b\)即ち\(F(b)\)への射を出力してくれる。そこで、データ型(\(Reader \ r \ a\))で定義されているフィールド\(getName\)を利用して射\(r \rightarrow a\)を取り出す。ここで取り出される射は\(r\)から\(b\)への関数である。

これに、複雑な構造の名前(といっても、ここでは、ファーストネームと氏姓制度での地位とラストネームからなるトリプルだが)を入力に与えると、その文字数を与えてくれる。なお、名を散りだす関数は\(first\)である。これは、トリプルの最初の要素を取り出す。

最初の実行例は個人名を与えたものである。\(count\)は\(F(r)\)から\(F(b)\)への射を与える。これに、\(getName\)を施すと\(r\)から\(b\)への射\(length.first)\)を与える。これに("Mike", "Omuraji", "Brooks")という名前を与えてるとファーストネームの文字数が出力される(因みに、友人のMike Brooksは現在は学長だ。「大連」より偉いかもしれない)。少し、複雑だがこのプログラムはこのようになっている。

次は、あるグループを構成していた人たちの名前を入力とした。<$>もファンクタの一種だが、配列での適応を可能にしてくれる。

*Main> getName count ("Mike","Omuraji","Brooks")
4
*Main> getName count <$> smap
[6,4,7,5]
*Main> getEven even' "Taro"
True
*Main> getEven even' <$> smap'
[True,True,False,False]

データ型\(Reader\)は関数を表現しているので、関数型(Function Type)とも呼ばれる。

圏での表現を書き換えると下図のように表すこともできる。
f:id:bitterharvest:20170305160721p:plain
この図から、\(\mathcal{C} \times \mathcal{D}=\mathcal{D}\)であることから、デカルト積になっていることもわかる。

2)反関手

それでは先ほどの文字数を求める問題にもう一度戻ることにしよう。

【問題】さらに別の地域\(E\)があって、そこでは文字数が偶数であるかどうかを判断していたとする。

取り敢えず\(C,E\)を圏にして図を示すことにしよう。
f:id:bitterharvest:20170305160738p:plain
ここで、\(f\)は\(A\)から\(B\)に写像する。それにもかかわらず、矢印の方向は\(F(B)\)から\(F(A)\)である。同様に\(g\)は\(B\)から\(C\)に写像するが、矢印の方向は\(F(C)\)から\(F(B)\)である。このように、ドメイン側の圏\(C\)の全ての射に対して、コドメイン側の圏\(E\)ではその方向が逆になるものを反関手(\(Contravariant\)あるいは\(Cofunctor\))と呼ぶ。

方向が逆向きになることを説明する。今回も前回と同じように、射を利用して、関手を張ることとする。前回は\(Reader\)という関手であった。これは\( new type \)を利用してデータ型を定義したが、その時のデータ型は\(Reader \ r \ a = Reader \ r \rightarrow a\)であった。
その時、\(r\)の方は固定して\(a\)の方が変われるようにした。\(Reader \ r \ a\)は、\(r\)を入力とし、\(a\)を出力とすると考えることができる。従って、データ型の\(Reader \ r \ a\)とフィールドで定義した\(r \rightarrow a\)とは方向が同じと見なせる。

次に、これから説明しようとするものは、反関手\(Writer \ c\)で張られる。後で示すが、そのデータ型は、\(Writer \ c \ a = Writer \ a \rightarrow c\)である。これは、前者\(Reader\)が射の入力を固定したのに対し、後者\(Writer \)は射の出力を固定するためである。このため、\(Writer \ c \ a\)は\(c\)を入力とし、\(a\)を出力とするようにふるまう。これに対して\(Writer \ a \rightarrow c\)は逆である。このため、方向はお互いに逆になる。

さて、本題に移ろう。ここで求めたいのは、\(F(C)\)から\(F(A)\)への射である。下図のようになる。
f:id:bitterharvest:20170305160757p:plain

Haskellでの表記に変えると以下のようになる。
f:id:bitterharvest:20170305160813p:plain

プログラムは以下のようになる。

{-# LANGUAGE InstanceSigs #-}
class Contravariant f where 
  contramap :: (a -> b) -> f b -> f a

newtype Writer c a = Writer { getEven :: a -> c }

instance Contravariant (Writer c) where
  contramap :: (a -> b) -> Writer c b -> Writer c a
  contramap f (Writer g) = Writer (g.f)

even' = contramap (length :: String -> Int) (Writer even)

smap' =["Takuya","Goro","Hiroaki","Singo"]

前と同じように実行してみよう。予想通りの動きになっている。

*Main> getEven even' "Taro"
True
*Main> getEven even' <$> smap'
[True,True,False,False]

\(Reader\)の場合と同じようにこれも圏の積になるが、反関手なので、\(C^{op} \times E \rightarrow E \)と記す。\(\mathcal{C}^{op}\)は\(\mathcal{C}\)の全ての矢印を逆にした圏を表す。

次回はいよいよ関手の最後、プロファンクタのお出ましだ。

秦野市桜土手古墳公園

小田急線を利用して秦野市にある古墳を見に行った。最寄り駅は渋沢である。北口に出てまっすぐに丹沢の方に向かって歩く。島津製作所日産自動車などの工場街の中にあるのが桜土手古墳公園だ。
f:id:bitterharvest:20170303163122j:plain

中に入るとすぐにこんもりと盛り上がった小さな丘がある。古墳だ。
f:id:bitterharvest:20170303163313j:plain
近づいてみるとこのような説明書きがある。
f:id:bitterharvest:20170303163407j:plain

それぞれの古墳について築造された時期が記されていなかったが、ウィキペディアで調べてみると、7世紀後半を中心に6世紀末から8世紀初頭に作られたとのことだ。35基の古墳が確認されているそうで、公園内にはそのうちの6基が保存されている。

展示館に古墳時代ジオラマがあった。すべてが円墳である。
f:id:bitterharvest:20170303164343j:plain

公園の中は古墳を取り巻くように散歩道が作られているのでそれに沿って歩く。古墳の中には木が生えているものもある。
f:id:bitterharvest:20170303165924j:plain
この古墳には次のような説明があった。径が15.6mあるそうだ。
f:id:bitterharvest:20170303170015j:plain

しばらく行くと復元された古墳に出会う。
f:id:bitterharvest:20170303170159j:plain
1号古墳を復元したものだ。周りは葺石で覆われ、そして、2段になっている。お墓は横穴式石室である。石室の入り口は
f:id:bitterharvest:20170303170742j:plain
石室の中から外側を覗くと
f:id:bitterharvest:20170303170848j:plain
公園事務所の人が掃除をしている姿も見ることができる。
横穴式の石室の説明は、
f:id:bitterharvest:20170303171049j:plain

石室の中ではなく墳丘の上部から、割られた大きな須恵器の甕が発見されたそうである。埋葬儀式のときに割られたものと考えられている。
f:id:bitterharvest:20170303171345j:plain
手前の大きな甕がそれである。穴が空いている部分が、割るために何かをぶつけた場所と考えられている。死者がもたらす災いから免れるために甕を割ったのであろうかなどと葬祭儀式の意義を見つけながら眺めた。

お墓を作っている場面を想定したジオラマもあった。
f:id:bitterharvest:20170303171634j:plain

墓の復元にはフォークリフトなどを用いて30日程度かかったそうである。当時の人たちはどれだけの日数をかけたのであろうか。また、築造中の事故も多かったのではなどと思いを巡らしながら、お腹もすいてきたこともあって古墳公園を後にした。

関手―余積をファンクタで実現する

6.8 余積をファンクタで実現する

前回の記事では関手を利用しての積と余積を定義する中で\(Identity\)を用いたが、その詳しい説明はしなかった。そこで、ここでは、まず、データ型\(Identity\)の定義から話を始めよう。関手\(Identity\)の互換図は下図のようになる。
f:id:bitterharvest:20170303080859p:plain
これを参考にしてHaskellで\(Identity\)のデータ型とファンクタを実現すると次のようになる。

data Identity a = Identity a deriving (Eq, Show, Read) 

instance Functor Identity where
  fmap f (Identity a) = Identity (f a)

終対象への写像に似ている関数で、一つの値\(c\)に写像する定数関数\(const\)と呼ばれるものがある。これを下図のように関手として利用してみよう。
f:id:bitterharvest:20170306141445p:plain
\(Const\)のデータ型とファンクタは次のようになる。

data Const c a = Const c deriving (Eq, Show, Read)

instance Functor (Const c) where
  fmap f (Const c) = Const c

少し利用してみよう。

*Main> a = Identity 4
*Main> fmap (*3) a
Identity 12
*Main> fmap (+6) a
Identity 10
*Main> b = Const 3
*Main> fmap (*3) b
Const 3
*Main> fmap (+6) b
Const 3

今得た二つの互換図を左右を逆にして重ねてみよう。
f:id:bitterharvest:20170306141459p:plain
この互換図は定数\(Const \ c\)と値\(Identity \ a\)との余積と見ることができる。しかも、余積はファンクタとしての\(Identity\)と\(Const\)により実現されている。

それでは、\(Const \ c\)を\( ( ) \)で置き換えてみよう。
f:id:bitterharvest:20170306141520p:plain
これも余積である。Haskellは余積を\(Either\)で表していたので、これは\(Either \ (Const \ ()) \ (Identity \ a)\)と書くことができる。

これは何かに似ていないだろうか。\(Maybe\)は値を持たないか値を持つかのいずれかであった。値を持たない場合には\(Nothing\)で表し、持つ場合には\(Just \ a\)で表した。そこで、これを今得た\(Either\)に当てはめてみよう。\(Nothing\)を\(Const \ ( )\)と、\(Just \ a\)を\(Identity \ a\)と考えてみよう。相互に表現法が違うだけで同じものであることが分かる。そこで、\(Either \ (Const \ ()) \ (Identity \ a)\)をタイプを用いて次のように\(Maybe'\)で言い換えてみる。

type Maybe' a = Either (Const () a) (Identity a)

少し利用してみよう。変数のデータ型を定めながらの利用になるが以下の様である。

*Main> a = Identity (3 :: Integer)
*Main> b = Right a :: Maybe' Integer
*Main> c = Const () :: Const () Integer
*Main> d = Left c :: Maybe' Integer
*Main> :t a
a :: Identity Integer
*Main> a
Identity 3
*Main> b
Right (Identity 3)
*Main> c
Const ()
*Main> d
Left (Const ())
*Main> :t a
a :: Identity Integer
*Main> :t b
b :: Maybe' Integer
*Main> :t c
c :: Const () Integer
*Main> :t d
d :: Maybe' Integer
*Main> :i a
a :: Identity Integer 	-- Defined at <interactive>:9:1
*Main> :i b
b :: Maybe' Integer 	-- Defined at <interactive>:10:1
*Main> :i c
c :: Const () Integer 	-- Defined at <interactive>:11:1
*Main> :i d
d :: Maybe' Integer 	-- Defined at <interactive>:12:1

このことからも、\(Maybe\)と\(Either\)は同じ概念を表していることが分かる。沢山のファンクタについて説明してきたが、次は反関手の話をする。