日々の流転

λ. Applicative Programming with Effects by Conor McBride and Ross Paterson

Monad(Strong Monad)とArrowの間に位置する抽象化だとか、コンビネータのSとKを抽象化したものとかいう話は耳にしてたけど、期待していたよりも面白かった。以前に書いた行列のコードなんかは、これを使って整理できそうだ。

圏論の言葉でいうと Applicative は strong lax monoidal functor になっているということなのだが、(モナドでない)一般の関手の場合のstrengthの「standard equations」なんて知りませんから!(後で調べる)

<2007-03-04追記> standard equations は

と

の二つだろう </2007-03-04追記>

それから「Note that B and FC swap places in the above diagram: strong naturality implies commutativety with pure computations.」という部分を理解するのにちと苦労した。

あと、最後のexerciseの「fmap swap (pure x ★ u) = u ★ pure x」の証明が案外面倒だった。もっと短く出来ないかな。

[lemma]
pure (f . g) <*> x
= {- homomorphism -}
  pure (.) <*> pure f <*> pure g <*> x
= {- composition -}
  pure f <*> (pure g <*> x)

fmap swap (pure x ★ u)
= {- definition of ★ -}
  fmap swap (pure (,) <*> pure x <*> u)
= {- homomorphism -}
  fmap swap (pure ((,) x) <*> u)
= {- definition of fmap -} 
  pure swap <*> (pure ((,) x) <*> u)
= {- lemma -}
  pure (swap . ((,) x)) <*> u
= pure (\y -> swap (x,y)) <*> u
= pure (\y -> (y,x)) <*> u
= pure (\y -> (\f -> f x) ((,) y)) <*> u
= pure ((\f -> f x) . (,)) <*> u
= {- lemma -}
  pure (\f -> f x) <*> (pure (,) <*> u)
= {- interchange -}
  pure (,) <*> u <*> pure x
= {- definition of ★ -}
  u ★ pure x

いや、「The Monoidal laws and the above definition of pure imply that pure computations commute past effects: fmap swap (pure x ★ u) = u ★ pure x」と言っているのだから、Applicativeの性質からではなく strong lax monoidal functor の性質から示すべきか。むむむ……

<2007-03-04追記> strengthを明示的に使ってはいないが、こんな感じか。

fmap swap (pure x ★ u)
= {- definition of pure -}
  fmap swap (fmap (\_ -> x) unit ★ u)
= fmap swap (fmap (\_ -> x) unit ★ fmap id u)
= {- naturality of ★ -}
  fmap swap (fmap ((\_ -> x)×id) (unit ★ u))
= fmap ((\y -> (y,x)) . snd) (unit ★ u))
= {- left identity -}
  fmap (\y -> (y,x)) u
= {- right identity -}
  fmap ((\y -> (y,x)) . fst) (u ★ unit)
= fmap (id × (\_ -> x)) (u ★ unit)
= {- naturality of ★ -}
  fmap id u ★ fmap (\_ -> x) unit
= u ★ fmap (\_ -> x) unit
= {- definition of pure -}
  u ★ pure x

</2007-03-04追記>

あと、「pure f <*> x1 <*> x2 <*> … <*> xn」を「iI f x1 x2 … xn Ii」と書けるようにする方法は Idiomatica.lhs に詳しい。しかし、こういうこと考えるやつは頭おかしいと思う……

λ. 『伝わる・揺さぶる!文章を書く』 (山田 ズーニー 著)

を読んだ。