Monad

3年前のソフトウェア工学の授業で、Haskell の Monad をいじって敗れ去ったことがあって。いや、使い方はなんとなくわかる。

> getChar

とかすると、入力待ちになって c とか入れると c とか表示されるけど、

> let x = getChar

かすると、何も起きなくて、

> x

とかすると、その時点で入力待ちになって x を打つたびに違う物が返るとか。振る舞いは謎だし、構文も、

    getll = do 
        c <-getChar1
        if c=='\n' 
            then return []
            else do
                 l <- getll
                 return (c:l)

とか、ちょっと許してくださいという感じです。do ってなんだよ。do って。

getChar1 >>= \c -> return c

とかになると、いったいなんなのという感じ。まぁ、Haskell だからなぁ。

でも、今回は Category 特に Kleisli Category 勉強しまくったのでわかりました。

    Functor はデータ構造 F(a) は Fというデータ構造を作る
    F(f) は、fmap f のこと

で、Monad は Functor つまり、単なるデータ構造なわけ。

そして、Kleisli Category では、射は、

f : a -> F (a)

つまり、Functor である Monad を常に返す関数ってことね。return とかは単位元な Monad を返す。
で、>>== は、射の結合 g○f = μ(d)T(g)f を表す。なので、常に、

\c -> F ( f c )

というような形をしているのか。なるほど。

ただ、「だからなんなの?」ってのは、ちょっと残っていて、Kleisli Category は随伴関手とかもあるので、そっちに絡めて証明がなんたらとかやるんだろうなとは思いましたが、そこから先に突っ込むのは学部の授業では、ちょっとね。学生も Agda の証明には面食らっているようなので、その辺りをいじめると面白かったりするのだが。いや、それなりに楽しみました。

今朝もうっかり3時まで資料作ってましたが、さすがに前みたいに体調崩すということはなくなったみたい。ソフトウェア工学の授業も、やろうと思ったことはだいたいできたし。