--- a/presen/agda-prog.ind	Thu Jan 09 19:02:04 2014 +0900
+++ b/presen/agda-prog.ind	Sat Jan 11 00:52:00 2014 +0900
@@ -6,7 +6,11 @@
 
 証明支援系の歴史は古い ( HOL, Coq, Agda も新しくない )
 
-Monadって何?
+Haskell が流行ってるようだが…
+
+     Monadって何?
+
+--Monadって何?
 
 Monad を解説しているサイトは多いが、多くは皮相的
 
@@ -14,24 +18,167 @@
 
 →　だったら、Monad を証明支援系を使って理解すれば良いんじゃないの?
 
---プログラムの検証の二つの方法
+とりあえず、目標は Monad の合成則
+
+--圏
+
+Category とは、集合であるオブジェクト A と、オブジェクト間の写像である射 f の組。
+    id(A) とは、A の要素を同じ要素に写像する射で必ず存在する 
+
+f: A->B, g: B->C に対して、射の合成がある。
+    g ○ f : A->C
+
+合成則
+
+    h ○ (g ○ f )  = (h ○ g) ○ f )
+
+A->A への単位射がある。同じ値を同じ値に返す射。
+    id_a : A->A
+
+これだけ。(あとは、Functor, Natural Transformation, Adjunction, Monad ... )
+
+--圏と関数型プログラミング
+
+射が関数 ( = 関数型プログラミングのプログラム)
+
+対象が型 ( 射は、型→型の写像)
+
+これだけ。(あとは、Functor, Natural Transformation, Adjunction, Monad ... )
+
+--圏としての型
+
+例えば Integer は、Integer から Integer への関数がある。これを射と考える。
+
+関数の合成則は成立しているし、単射もある。
+
+型は圏でもある。
+
+--Functor
 
-    モデル検証
-    証明
+Functor F とは、Category C から D への写像
+対象AをDの対象B対応させる写像をFObjとする。
+射の対応が、以下を満たす時に、F はFunctor と言う。
+
+    (1) C の射 f:A->B を Dの射 F(f):F(A)->F(B) に割り当てる (FMap)
+    (2) id(F(A)) = F(id(A))
+    (3) f: A->B, g: B->C に対して、
+        F(g) ○ F(f) : F(g○f)
+
+Functor は対象の写像FObjと、射の写像FMapの二つを持つ。
+
+--Constructor としての Functor
+
+Integer と List はどちらも圏であり、
+Integer から List を作る Constructor は、
+Category から Category への Functor に相当する。
+
+つまり、Haskell の data はFunctor になる。
+
+    data List a = (::) a (List a)
+           |      []
 
--- モデル検証
+   data Nodes a = Node (Nodes a) (Nodes a)
+       |       Leaf a
+
+List や Node を Functor のFObj(対象の射)として考えることができる。
+
+--FMap
+
+Functor は射の写像も持っている必要があり、fmap として(自分で)定義する。
+
+     class Functor f where
+        fmap :: (a->b) -> f a -> f b
+
+    fmap f (Leaf a ) =  Leaf (f a)
+    fmap f (Node  a b ) =  Node (fmap f a) (fmap f b)
+
+
+fmap は要素の関数 g: a->b を List や Node の関数へ変換している。
+この時、f は List や Node の要素を操作する関数。
+
+            T(f)
+      T ------------> T
 
-    可能な実行をすべて試す 
-　　論理の言葉で言えば、充足可能性を調べる
-    バグを探す、検索空間が膨大、比較的大きなものに対処できる
-    扱う問題の規模に探索時間が依存する
+は T の要素に f を作用させると考えて良い。
+
+--Natural Transformation (自然変換)
+
+Node から List への変換を考える。これは、Functor から Functor への射になる。
+
+例えば、flatten ( 木を深さ順にリストにする) は、そういう射の例である。
+
+Node の要素をIntegerからStringに変換するには show が使える。( show 1 = '1' )
+
+ここで、
+
+   flattern ( List.fmap show aNode ) = Node.fmap show ( flattern  aNode )
+
+これを可換(commute)という。可換なFunctorからFunctorへの射をNatural Transformation
+とう。
+
+<center><img src="fig/flatten.jpg"></center>
+
+--Natural Transformation
+
+Functor で可換を書くと、
+
+<center><img src="fig/nat.jpg"></center>
+
+ここで、F,G は、データ型。F(a)/F(b)) は FObj 。F(f) / G(f) は FMap。
+
+t は自然変換(引数は要素の型)
+
+--Monad
+
+Monad とは、Functor T と二つの自然変換η,μの三つ組　 (T,η,μ) で、
+以下の性質を満たすものである。
+
+    T: A -> A             T は AからAへのFunctor
+    η: 1_A -> T            ηは、a から T a への自然変換
+    μ: T^2 -> T            μは T T a から T a への自然変換
+
+さらに、Unity Law と呼ばる
 
---証明
+   μ○Tη = 1_T = μ○ηT 
+
+と、Association Law　と呼ばれる以下の可換図を満たす。
+
+<center><img src="fig/nat.jpg"></center>
+
+--Kleisli 圏
+
+上の Monad で、 a から T b への射を 新しい Kleisli 圏の射と考える。
+
+この射の合成を、
+
+  f : b -> T(c)
+  g : c -> T(d)
+  g * f = μ(d)T(g)f    
+
+として定義する。
+
+Monad の合成則 (g * f ) * h = g * ( f * h ) が成立する。
 
-    プログラムがどういう性質を満たすかを論理式で記述する
-    推論規則を使って、公理と仮定から性質を導く
-    非常に難しく、証明の長さも長い
-    扱う問題の規模に証明時間が依存する
+--Haskell での Monad
+
+T はFunctorだからデータ型。メタデータだと思って良い。計算の詳細に関する
+メタなデータと、元のデータを含むデータ型。
+
+Haskell Monad はメタデータを追加して返す関数。 Reflection に相当する。
+
+<center><img src="fig/Kleisli.jpg"></center>
+
+
+例えば、IO Monad は、入出力するデータをメタデータとして返す。
+
+--Monad の合成
+
+メタデータの変化は自然変換 μ で決まる。
+
+<center><img src="fig/join.jpg"></center>
+
+合成則の証明は煩雑
+
 
 --Curry Howard 対応