Monad
Menu
Monad とは?
Haskell では IO や、Error を表す返り値、Exception などで Monad が頻繁に使われている。IO などを表すデータ構造 (= Functor ) を定義して、Functor に作用する自然変換を通して、そのデータ構造を操作するのが Monad である。このデータ構造は文脈と呼ばれることもある。
もともと圏論の概念であり、少々複雑であるが、折角なので、ちゃんと数学的な定義を理解しよう。
Functor T と二つの自然変換からなる Monad
Monad から作られる Kleisli Category
を理解する。Monad のプログラミングは、Kleisli Category の射(普通のデータを受け取って、Monad を返す関数)を定義して、Monad の自然変換で合成していくことになる。
Monad を自分で定義するには、Monad の自然変換を自分で定義すれば良い。
Monad の Functor T によって、以下のような機能を持つ計算を定義することができる。(x は集合の直積、+ は排他的和)
| 最も単純な計算 | T(A) = A | ||||||
| 部分計算 | T(A) = A + ⊥ (⊥は未定義値) | ||||||
| 非決定的な計算 | T(A) = A2 | ||||||
| 副作用のある計算 | T(A) = (A x S)s (Sは状態の集合)| 例外のある計算 | A + E (E は例外の集合) | 継続のある計算 | R R A R は計算結果 | 計算量を持つ計算 | A x N (N は計算量) | |
部分計算
計算には例外が付きものである。例外として未定値を返せる計算を考えよう。この時に、返す値は、通常返される値と、未定値のSum型になる。型変数を持つデータ構造は Functor だったのを思い出して、
data maybe {c : Level} (A : Set c) : Set c where
just : A → maybe A
nothing : maybe A
Maybe : Functor Sets Sets
Maybe = record {
FObj = λ a → maybe a
; FMap = λ {a} {b} f → fmap f
; isFunctor = record {
identity = extensionality {zero} ( λ x → ? )
; distr = extensionality {zero} ( λ x → ? )
}
} where
fmap : { a b : Obj Sets } ( f : a → b ) → maybe a → maybe b
fmap f ( just x ) = just (f x)
fmap f nothing = nothing
just 1 とかが返ってくればok。ダメなら nothing が返る。例えば、割り算ならば、
div : ℕ → ℕ → maybe ℕ
div _ Zero = nothing
div Zero _ = just Zero
div (suc n) m = just ( f1 (ℕ.suc n) m m )
where
f1 : ℕ → ℕ → ℕ → ℕ
f1 Zero _ _ = Zero
f1 (suc n) Zero _ = Zero -- can't happen
f1 (suc n) (suc Zero) m = ℕ.suc ( f1 n m m )
f1 (suc n) (suc m') m = f1 n m' m
maybetest1 = div 3 0
maybetest2 = div 10 3
などと定義する。
Maybe に引き続く計算
div が nothing を返すのは良いが、引き続く計算 f : a → b は入力が nothing なら nothing
入力が just x なら x を入力として、just y
を返して欲しい。そういう f' : Maybe a → Maybe b を定義しても良いが、f を使って書けた方が良い。
div の結果に FMap で + 2 を作用させると、
maybetest3 : ℕ → ℕ → maybe ℕ
maybetest3 x y = FMap Maybe (λ x → x + 2) ( div x y )
として調子が良い。割り算を続ける時は、
maybetest4 : ℕ → ℕ → maybe (maybe ℕ )
maybetest4 x y = FMap Maybe (λ x → div 2 x ) ( div x y )
これはうれしくない。maybe (maybe ℕ ) ではなくて、maybe ℕ になって欲しい。もちろん、
m : {a : Set} → maybe (maybe a ) → maybe a
m nothing = nothing
m (just nothing) = nothing
m (just (just x)) = just x
として、
maybetest6 : ℕ → ℕ → maybe ℕ
maybetest6 x y = m ( FMap Maybe (λ x → div 2 x ) ( div x y ) )
とすると具合が良い。
maybe は Functor だったが、m はnest した Functor から1重のFunctorへの変換になる。これを自然変換と呼ぶのだった。
一般的に Monad T を返す関数 g : a → T b があった時に、その結果 T b に f : b → T c を作用させるには、
g の結果に f を FMap して、m を作用させる
とすれば良い。つまり Monad を返す関数 fとgの結合は
f . g = m ( ( FMap Maybe f ) g )
によって定義される。
普通の関数 h は
h' = λ x → just (h x)
とすると Monad を返す関数になる。
Monad と Monad が作る圏
圏(category)は、集合である関数の型を対象とし、射を関数とする構造体で、射の結合 o に対して、単位元idがあり、左単位元 id a o f = f 右単位元 f o id a = f 結合法則 (f o g ) o h = f o (g o h )
が成り立つものだった。上の Monad を返す射に対する結合がこの三つの法則を満たせば、Monadを返す射は圏になる。
この圏をKleisli圏という。
その前に、Monad をAgdaで定義しよう。Kleisli 圏を作るためにいくつかの規則が必要になる。
Monad とは、Functor T と二つの自然変換η,μの三つ組 (T,η,μ) で、以下の性質を満たすものである。
record IsMonad {l : Level} { C : Category {l} } (T : Functor C C) ( η : NTrans idFunctor T ) ( μ : NTrans (T ● T) T )
: Set (suc l) where
field
assoc : {a : Obj C} → C [ TMap μ a o TMap μ ( FObj T a ) ] ≡ C [ TMap μ a o FMap T (TMap μ a) ]
unity1 : {a : Obj C} → C [ TMap μ a o TMap η ( FObj T a ) ] ≡ id C (FObj T a)
unity2 : {a : Obj C} → C [ TMap μ a o (FMap T (TMap η a ))] ≡ id C (FObj T a)
record Monad {l : Level} { C : Category {l} } (T : Functor C C) : Set (suc l) where
field
η : NTrans idFunctor T
μ : NTrans (T ● T) T
isMonad : IsMonad T η μ
T ● T はFunctorの結合で、TTともT^2とも書く。
T: C -> C T は AからAへのFunctor
η: 1_C -> T ηは、a から T a への自然変換
μ: T^C -> T μは T T a から T a への自然変換
さらに、Unity Law と呼ばる
μ○Tη = 1_T = μ○ηTと、Association Law と呼ばれる可換図を満たす。
μ○μT = μ○Tμこの結合○は、普通の関数の結合である。
T( η(a)) が Functor T による射 η(a) の変換。η(a) が a から T a を返す Functor (データ構造 )であることを思い出すと、 T( η(a)) は、
T (T a)
という形をしたものである。
μ(b) は、 T (T a) という形をしたものを受け取って、T a という形のものを返す。(FObj T a、Maybe なら maybe a)μ○Tη =は、その組み合わせ
μ(b) T( η(a) )
である。自然変換の引数は型であり Generic のような役割になっている。引数TがFunctorなので、TにはGenericで型を与える必要がある。( μ(b) の型は何か? Monad Maybe だったら型は?) Tμ はFMap T (TMap μ a)の省略系である(その型は何か?)。
Monadの自然変換μ
μ : TT → T
TTは (T(T(a)) のこと。Functor が二つネストしている。これを T a に変換するのが、μ。maybe で使った m である。この時に、
μ(a)
TT(a) -------> T(a)
| |
TT(f)| |T(f)
| |
v μ(b) v
TT(b)---------->T(b)
が可換である必要がある。μの引数は型変数。
assoc : {a : Obj C} → C [ TMap μ a o TMap μ ( FObj T a ) ] ≡ C [ TMap μ a o FMap T (TMap μ a) ]
Monadの自然変換η
ηは 1 → T 、元の a とか b の属する圏A上の1つまり、同じデータ型を返すFunctorから、T へのデータ変換。まどろっこしいが、要するに a とか b から Ta とかTbを 作れば良い。
η(a)
a ------------> T(a)
| |
f| |T(f)
| |
v η(b) v
b ------------->T(b)
という可換性が要求される 。
unity1 : {a : Obj C} → C [ TMap μ a o TMap η ( FObj T a ) ] ≡ id C (FObj T a)
unity2 : {a : Obj C} → C [ TMap μ a o (FMap T (TMap η a ))] ≡ id C (FObj T a)
T(a) は型。η(a) はconstructor。T(a) と同じ気もするが、T(a) は型であって値ではない。η(a) は、射、つまり型aから型Taを返す関数なので、実際に値が決まる。
MaybeMonad では η(a)は just x と定義する。普通の関数からMaybeMonadの射を作る時に使う。
Monadの射は勝手なTを返して良い。Tにはメタ計算を表すいろんなパラメータがあるので、それを勝手に指定できる自由度がある。
Monad の射の結合
Monad T が作る Kleisli圏の対象は、Setsの対象をそのまま使う。射は a → T b という形の関数である。これを record で定義する。
record KleisliHom { c : Level} { A : Category {c} } { T : Functor A A } (a : Obj A) (b : Obj A)
: Set c where
field
KMap : Hom A a ( FObj T b )
(record にしなくても別に良いらしい)
f : a → b
g : b → c
に対して、 関数の結合 g○ f は、 f ○ g : a → c
Kleisli圏の射の結合*は
f : a → T b
g : b → T c
に対して、
f * g = μ(c)○T(g)f
Sets なら
x : a があったときに f(x) は T b を返す
T(g)( f(x)) は、T ( T c )を返す
μ ○ T(g)( f(x)) は、T ( T c )をうけ取って T c を返す
とする。これは join と呼ばれる。μは、TT → T で、f と g が創りだした 二つのTを一つにするのだった。
join : { a b c : Obj C } → Hom b (FObj T c) → Hom a (FObj T b ) → Hom a (FObj T c )
join {a} {b} {c} f g = record { KMap = ( C [ TMap (Monad.μ M) c o C [ FMap T ( KMap f ) o KMap g ] ] ) }
ここで C [ x o y ] は、圏Cで射 x と cを結合すると言う構文である。今の場合は Sets なので、普通の関数の結合となる。
η の単位元としての性質は、
η(b) * f = f f * η(a) = fを示せば良い。
結合則は、
f * (g * h) = μ(c)○T(f)((μ(b)○T(g)h)
(f * g) * h = μ(c)○T(μ(b)○T(f))(μ(b)○(T(g)h))
が等しいことを証明すれば良い。
TMap (Monad.μ M) d o ( FMap T (KMap f) o ( TMap (Monad.μ M) c o ( FMap T (KMap g) o KMap h ) ) ) )
h T g μ c
a ---→ T b -----------------→ T T c -------------------------→ T c
| | |
| | |
| | T T f NAT μ | T f
| | |
| v μ (T d) v
| distr T T T T d -------------------------→ T T d
| | |
| | |
| | T μ d Monad-assoc | μ d
| | |
| v v
+------------------→ T T d -------------------------→ T d
T (μ d・T f・g) μ d
TMap (Monad.μ M) d o ( FMap T (( TMap (Monad.μ M) d o ( FMap T (KMap f) ・ KMap g ) ) ) o KMap h ) )
Maybe で f g h と具体的に入力を与えた場合に、可換図のノードの値を計算してみよ。
Monad の構文
Haskell の Monad では様々な構文が用意されている。
f * g = μ(c)○T(g)f
join f g
で定義される。これを、Haskell では、
g >>= f
と書く。方向が逆だが、gの方が先に計算されるので、この方が良い。
ηは return と書く。
infixl 1 >>, >>=
class Monad m where
(>>=) :: m a -> (a -> m b) -> m b
return :: a -> m a
instance Monad (T1 a) where
return a = eta a
(>>=) = \t \f -> mu (fmap f t)
という風に定義されている。m は Functor である。
join は自然変換μを使わずに、>>= を直接定義すると Haskell では効率が良い。
instance Monad (Maybe a) where
return x = just x
nothing >>= _ = nothing
just x >>= k = k x
良く使われる形は、
g >>= (\x → ... x ... )
だが、これを
do
x <- g
... x ...
と書く構文がHaskellには用意されている。Monad T は T を返す必要があるので、
return a
つまり、η : 1 → T が返す T を返すのが普通。例えば、fをMonadを返さない普通の関数だとして、
do
x <- g
return (f x)
となる。gが返すのはMonadで、f x は通常の値を返す。return がそれを (η : 1 → T)を用いてTに変換している。
fが直接Tを返すなら、
do
x <- g
f x
で良い。do の構文は複数の Monad を返す関数を含めると、それぞれに join を働かせるようになっている。なので、putStr を複数回呼び出すこともできる。
この Manod が何かは、f x が返す Monad の型で決まる。Monad は class で plymoriphic に定義されているので、 do が選択する μ は、f の返す値に寄って変わる。
Agda は monomorphic なので、Monad の型を明示する(あるいは暗黙の引数で示す)必要がある。
Applicative
二つの引数の普通の関数、例えば、
_+_ : ℕ → ℕ → ℕ
は、結果だけを maybe ℕ にしても、 ℕ → maybe ℕ の形にならない。
( ℕ x ℕ ) → maybe ℕ
にしても良いが、ℕ → ( ℕ → ℕ ) という Curry 化できる利点が失われてしまう。
ℕ → maybe ( ℕ → maybe ℕ )
という形にできると良い。
record Applicative ( F : Functor (Sets ) (Sets ) )
: Set (suc zero) where
field
pure : {a : Obj Sets} → Hom Sets a ( FObj F a )
_<*>_ : {a b : Obj Sets} → FObj F ( a → b ) → FObj F a → FObj F b
MaybeApplicative : Applicative Maybe
MaybeApplicative = record {
pure = \ x -> just x
; _<*>_ = _<*>_
} where
_<*>_ : {a b : Obj Sets} → FObj Maybe (a → b) → FObj Maybe a → FObj Maybe b
nothing <*> x = nothing
(just f) <*> x = (FMap Maybe f) x
maybetest7 = (just (λ x y → x + y ) <*> just 3 ) <*> just 7
where
_<*>_ = Applicative._<*>_ MaybeApplicative
Haskell では Monad は Applicative であることが要請される。( return + <*> return 3 <*> return 7 など使われる)
Sets上のApplicativeはMonadから構成するとができる。
_<*>_ : {a b : Obj Sets} → FObj T ( a → b ) → FObj T a → FObj T b
_<*>_ {a} {b} f x = ( TMap (μ m ) b ) ( (FMap T (λ k → FMap T k x )) f )
しかし、<*>はMonadFunctorに対して再帰的に定義する方が簡単かつHaskell的に効率的である。
Applicative でKelisli圏を構成するには直積 ℕ x ℕ がFとUでisomorphicに保存される必要がある。そのための法則がある(が結構面倒)。
圏CとKleisli圏の関係
Haskell では基本的に Sets が使われる。このSetsとKleilisi 圏の二つの圏がある。これらは関手により、相互に対応している。
Sets 上の射 (Hom Sets a (T b)), f : a → T b
が
Kleisli圏上の射 KleisliHom a b, record { KMap = f }
に自明に対応する。しかし、実際にこの二つの圏の間のFunctorを構成するのは少し面倒である。
U : ( T : Functor Sets Sets ) → { m : Monad T } → Functor (Kleisli Sets T m) Sets
U T {m} = record {
FObj = FObj T
; FMap = λ {a} {b} f x → TMap ( μ m ) b ( FMap T ( KMap f ) x )
; isFunctor = record { identity = IsMonad.unity2 (isMonad m) ; distr = ? }
F : ( T : Functor Sets Sets ) → {m : Monad T} → Functor Sets ( Kleisli Sets T m)
F T {m} = record {
FObj = λ a → a ; FMap = λ {a} {b} f → record { KMap = λ x → TMap (η m) b (f x) }
; isFunctor = record { identity = refl ; distr = ? }
(? を埋めてFunctorを完成させよ)
この時に
T = U ● F
となる(これを示せ)。これは Monad のResolution と呼ばれる。Uで行ってFで戻ってきても、同じ射に戻るわけではない。もしそうなら、二つの圏は同一になてしまう。その代わりに別な対応がある。
この対応は、
Hom K (F a) b ≈ Hom Sets a ( U b )
と書かれる。単に1対1対応ではなくて、isomorphic に対応するという意味である。以下の可換図が成立すると言う意味になる。
Hom C F(a) b ←---→ Hom D a U(b) Hom C F (a) b ←---→ Hom D a U(b)
| | | |
Ff| f| |f |Uf
| | | |
↓ ↓ ↓ ↓
Hom C F(f(a)) b ←---→ Hom D (f a) U(b) Hom C F(a) f(b) ←---→ Hom D a U(f(b))
f : b → T c , g : a → b があった時に、
f o g : a → T c
となる。先に、f, g を相手の圏に送ってから結合させるのと、結合してから相手の圏に送るのとつじつまがあっている必要がある。
もう一つ、 f : b → c , g : a → T b があった時に、
T f o g : a → T c
でも同じような対応が必要になる。 ←---→ は右向き、左向きの二つの写像(left, right)を含み、それぞれを合成すると元に戻る必要がある。 ( left o right = id , right o left = id )
この時にUとFは随伴関手であると言われる。随伴関手があると、Monadを構成することもできる(Agdaで証明するのもそれほど難しくない)。
Monad の例
Monoid Monad
ここではListをMonoid として使う。計算の履歴を取ったりするのに便利なMonad。
data T1 m a = T [m] a
deriving (Show)
instance Functor T1 where
fmap f ( T m a ) = T m ( f a )
ηは eta 、μ は mu として定義する
eta a = T [] a
mu (T m (T m' a)) = T (m ++ m') a
これを class して定義すると、
class Monad1 t where
eta :: a -> t a
mu :: t ( t a ) -> t a
となる。Monad のηとμの定義とぴったり対応している。
eta と mu が自然変換であることを確認する必要がある。そして、Monad 則が成立しているかどうかを調べる。
List のAgdaでの定義を思い出そう。
data List {l : Level} (A : Set l ) : Set l where
[] : List A
_::_ : A → List A → List A
append : { A : Set } → List A → List A → List A
append [] x = x
append (x :: y ) z = x :: append y z
T1 の定義は Haskell とほぼ同じ。
data T1 (M : Set ) (A : Set ) : Set where
T : List M → A → T1 M A
しかし、これをFunctorにする必要がある。
FunctorT1 : (M : Set ) → Functor Sets Sets
FunctorT1 M = record {
FObj = λ x → T1 M x
; FMap = λ {a} {b} f → fmap f
; isFunctor = record {
identity = λ {A} → extensionality {zero} ( λ x → ? x )
; distr = λ{a} {b} {c} {f} {g} → extensionality {zero} ( λ x → ? f g x )
}
} where
fmap : {a b : Obj Sets} (f : a → b ) → T1 M a → T1 M b
fmap f (T m x) = T m (f x)
ここで、
extensionality : {a b : Set } → {f g : a → b } → ∀(x : a) → → f x ≡ g x → f ≡ g
が仮定されている。
(? を埋めて、Functor を完成させよ)
Monadの定義は以下のようになる。list の結合法則を前もって証明しておこう。
list-assoc : { a : Set } → ( x y z : List a ) → append (append x y ) z ≡ append x ( append y z )
list-assoc [] [] _ = refl
list-assoc [] (h :: y) z = refl
list-assoc (h :: x ) y z = cong ( λ z → h :: z ) ( list-assoc x y z )
T1Monad : (M : Set) → Monad (FunctorT1 M)
T1Monad M = record {
η = record { TMap = λ a x → T [] x ; isNTrans = record { commute = refl } }
; μ = record { TMap = λ a x → mu a x ; isNTrans = record { commute = extensionality {zero} ( λ tt → mu-commute tt ) } }
; isMonad = record {
assoc = extensionality {zero} ( λ m → assoc m )
; unity1 = extensionality {zero} ( λ m → ? m )
; unity2 = extensionality {zero} ( λ m → ? m )
}} where
mu : (a : Obj Sets) (x : T1 M ( T1 M a ) ) → (T1 M a )
mu a (T m (T m' x) ) = T (append m m') x
mu-commute : {a b : Obj Sets} {f : a → b } ( tt : T1 M ( T1 M a ) )
→ (Sets [ FMap (FunctorT1 M) f o (λ x → mu a x) ]) tt ≡ (Sets [ (λ x → mu b x) o FMap (FunctorT1 M ● FunctorT1 M) f ]) tt
mu-commute {a} {b} {f} (T m (T m' x) ) = let open ≡-Reasoning in begin
(Sets [ FMap (FunctorT1 M) f o mu a ]) (T m (T m' x))
≡⟨ ? ⟩
(Sets [ mu b o FMap (FunctorT1 M ● FunctorT1 M) f ]) (T m (T m' x))
∎
assoc : {a : Obj Sets } ( m : T1 M ( T1 M ( T1 M a )))
→ (Sets [ (λ x → mu a x) o (λ x → mu (FObj (FunctorT1 M) a) x) ]) m ≡ (Sets [ (λ x → mu a x) o FMap (FunctorT1 M) (λ x → mu a x) ]) m
assoc {a} ( T m ( T m' ( T m'' x ) ) ) = let open ≡-Reasoning in begin
T (append (append m m') m'') x
≡⟨ cong ( λ z → T z x ) ( list-assoc m m' m'' ) ⟩
T (append m (append m' m'')) x
∎
(? を埋めて、証明を完成させよ)
{-# TERMINATING #-}
fact : ℕ → T1 ℕ ℕ
fact Zero = T [] 1
fact (suc Zero) = T [] 1
fact (suc n) = KleisliHom.KMap ( KT [ record { KMap = λ x → T ( x :: [] ) ( x * n ) } o record { KMap = fact } ] ) n
fact' : ℕ → T1 ℕ ℕ
fact' Zero = T [] 1
fact' (suc Zero) = T [] 1
fact' (suc n) = (TMap (Monad.μ (T1Monad ℕ)) ℕ ( FMap (FunctorT1 ℕ) ( λ x → T ( x :: [] ) ( x * n )) ( fact' n ) ) )
fact'' : ℕ → T1 ℕ ℕ
fact'' Zero = T [] 1
fact'' (suc Zero) = T [] 1
fact'' (suc n) = ( fact'' n ) >>= ( λ x → T ( x :: [] ) ( x * n ))
where
_>>=_ : {a b : Obj Sets } -> T1 ℕ a -> ( a -> T1 ℕ b ) -> T1 ℕ b
(T [] x >>= g ) = (g x)
(T (h :: t) x >>= g ) with (T t x >>= g )
... | T gt gx = T ( h :: gt ) gx
list monad
monoid と似ているが、List の扱いが違う。複数の値を返す時に使う。非決定的な計算とか。
ListMonad : Monad ListFunctor
ListMonad = record {
η = record { TMap = λ a x → x :: [] ; isNTrans = record { commute = ? } }
; μ = record { TMap = λ a x → mu a x ; isNTrans = record { commute = extensionality {zero} ( λ ll → mu-commute ll ) } }
; isMonad = record {
assoc = λ {a} → extensionality {zero} ( λ m → ? m )
; unity1 = extensionality {zero} ( λ m → ? m )
; unity2 = extensionality {zero} ( λ m → ? m )
}
} where
mu : (a : Obj Sets) ( x : List ( List a ) ) → List a
mu a [] = []
mu a (h :: t ) = append h ( mu a t )
mu-commute : {a b : Obj Sets} {f : Hom Sets a b} → ( x : List ( List a ) )
→ (Sets [ FMap ListFunctor f o (λ x → mu a x) ]) x ≡ (Sets [ (λ x → mu b x) o FMap (ListFunctor ● ListFunctor) f ]) x
mu-commute [] = ?
IO Monad
Haskell では Monad はIOに使われる。これはどうのように作れば良いのだろうか?
open import Data.Char
data IOTeletype (a : Set ) : Set where
GetChar : (Char -> IOTeletype a) -> IOTeletype a
PutChar : Char -> (IOTeletype a) -> IOTeletype a
ReturnTeletype : a -> IOTeletype a
IOTeletype はListのような再帰的な構造を持っていて、出力したCharをListのように持っている。GetCharには入力したCharを消費する関数が必要である。
まず、これをFunctor にする必要がある。
IOT : Functor Sets Sets
IOT = record {
FObj = λ x → IOTeletype x
; FMap = fmap
; isFunctor = record {
identity = extensionality {zero} {zero} ( λ x → ? x )
; distr = λ {a} {b} {c} {f} {g} → extensionality {zero} ( λ x → ? x f g )
}
} where
fmap : {A B : Obj Sets} → Hom Sets A B → Hom Sets (IOTeletype A) (IOTeletype B)
fmap k (GetChar f) = GetChar ( \c -> fmap k (f c ) )
fmap k (PutChar c f) = PutChar c (fmap k f )
fmap k (ReturnTeletype x) = ReturnTeletype ( k x )
fmap が再帰的に定義されていることに注目しよう。Monadは基本的に、このように構成される。(?を埋めて証明を完成させよ)
IOMonad : Monad IOT
IOMonad = record {
η = record { TMap = λ a x → ReturnTeletype x ; isNTrans = record { commute = ? } }
; μ = record { TMap = λ a x → mu {a} x ; isNTrans = record { commute = \ {a} {b} {f} -> extensionality {zero} ( λ m → ? )}}
; isMonad = record {
assoc = extensionality {zero} ( λ m → ? m )
; unity1 = extensionality {zero} ( λ m → ? m )
; unity2 = extensionality {zero} ( λ m → ? m )
}
} where
mu : {a : Obj Sets } -> IOTeletype ( IOTeletype a ) -> IOTeletype a
mu (GetChar f) = GetChar ( \ c -> mu ( f c) )
mu (PutChar c f) = PutChar c ( mu f )
mu (ReturnTeletype x) = x
Monad の mu も fmap と同じように作られている。
return : {a : Obj Sets } -> a -> IOTeletype a
return = ReturnTeletype
_>>=_ : {a b : Obj Sets } -> IOTeletype a -> ( a -> IOTeletype b ) -> IOTeletype b
(GetChar f) >>= g = GetChar (\c -> (f c >>= g))
(PutChar c f) >>= g = PutChar c (f >>= g)
(ReturnTeletype x) >>= g = g x
とすると、Haskellの構文に近くなる。
IO Monad には、入力を用意して、出力を表示する driver (runTT) が必要になる。
open import Data.List
open import Data.Product
getChar1 : IOTeletype Char
getChar1 = GetChar ( ReturnTeletype )
putChar1 : Char -> IOTeletype Char
putChar1 c = PutChar c (ReturnTeletype c )
runTT : {a : Obj Sets } -> (IOTeletype a ) -> ( In : List Char ) -> (Out : List Char ) -> ( a × List Char )
runTT (ReturnTeletype x) In out = ( x , out )
runTT (PutChar c f) cs h = runTT f cs ( h ++ (c ∷ []) )
runTT (GetChar f) (h ∷ t) cs = runTT (f h) t cs
runTT (GetChar f) [] cs = runTT (f '\0' ) [] cs
{-# TERMINATING #-}
getl : IOTeletype (List Char )
getl = getChar1 >>= \ c -> getl1 c
where
getl1 : Char -> IOTeletype (List Char)
getl1 '\n' = return []
getl1 c = getl >>= ( \ l -> return ( c ∷ l ) )
runn : List Char × List Char
runn = runTT getl ( 't' ∷ 'e' ∷ 's' ∷ 't' ∷ '\n' ∷ [] ) []
test3 : IOTeletype ( Char -> Char -> Char -> List Char )
test3 = return ( \ x y z -> ( x ∷ y ∷ z ∷ [] ) )
testapp : IOTeletype (List Char)
testapp = ((test3 <*> getChar1 ) <*> getChar1 ) <*> getChar1
where
_<*>_ : {a b : Obj Sets} → FObj IOT ( a → b ) → FObj IOT a → FObj IOT b
_<*>_ = Applicative._<*>_ IOApplicative
runa : List Char × List Char
runa = runTT testapp ( 't' ∷ 'e' ∷ 's' ∷ 't' ∷ '\n' ∷ [] ) []
(Data.String を使って書き直してみよ)
IO Monad の例題 (Haskell 上で同様のことを実現してみよ)
Hakell の IO Monad をSimulate する