トップ «前の日記(2006-12-06) 最新 次の日記(2006-12-08)» 月表示 編集

日々の流転


2006-12-07 [長年日記]

λ. 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 は
\xymatrix{ I\otimes TA \ar[r]^\tau \ar[dr]_{l} & T(I\otimes A) \ar[d]^{T(l)} \\ & TA }

\xymatrix{ (A\otimes B)\otimes TC \ar[rr]^\tau \ar[d]_\alpha && T((A\otimes B)\otimes C) \ar[d]^{T(\alpha)}\\ A\otimes (B\otimes TC) \ar[r]_{\mathrm{id}\otimes\tau} & A\otimes T(B\otimes C) \ar[r]_\tau & T(A\otimes (B\otimes C)) }
の二つだろう </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 に詳しい。しかし、こういうこと考えるやつは頭おかしいと思う……

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

伝わる・揺さぶる!文章を書く (PHP新書)(山田 ズーニー) を読んだ。

Tags:
本日のツッコミ(全4件) [ツッコミを入れる]
ψ たけを (2007-03-02 20:00)

教えてくん質問で恐縮ですが、strong monad ってどういうのを言うんでしょう?

ψ さかい (2007-03-02 23:49)

一般に strong ??? というのは適当な条件(coherence condition)を満たす自然変換 τ_{X,Y}: X□TY→T(X□Y) が存在する ??? のことで、モナドの場合には λ_A: 1□A→A, α_{A,B,C}: (A□B)□C→A□(B□C) を自然変換として以下の条件になります。<br><br>(1) T λ_A ・ τ_{1,A} = λ_TA<br>(2) T α_{A,B,C} ・τ_{A□B,C} = τ_{A,B□C} ・ (id_A □ τ_{B,C}) ・ α_{A,B,TC}<br>(3) τ_{A,B} ・ (id_A □ η_B) = η_{A□B}<br>(4) τ_{A,B} ・ (id_A □ μ_B) = μ_{A□B} ・ T τ_{A,B} ・ τ_{A,TB}<br><br>また、Haskellでは<br> t :: Monad m => (a, m b) -> m (a, b)<br> t (a,m) = m >>= \b -> return (a,b)<br>と定義することにより、Monadクラスのインスタンスは全て strong monad になります。

ψ たけを (2007-03-04 17:44)

丁寧な回答ありがとうです。ぐは、むずいー。<br>strong monoidal functor というのが Mac Lane の本に載ってますけど、あれも strong ??? の一種だと思っていいんですかね、そうすると。

ψ さかい (2007-03-04 20:13)

> 丁寧な回答ありがとうです。ぐは、むずいー。<br><br>条件の細部はあまり気にする必要ないと思います。<br>結局のところ、τが既存の他の操作と整合的であることを言っているだけなので。<br><br>> strong monoidal functor というのが Mac Lane の本に載ってますけど、あれも strong ??? の一種だと思っていいんですかね、そうすると。<br><br>↓のやつですね。<br><br>| F_0: e'→F(e)<br>| F_2(a,b): F(a)□F(b)→F(a□b)<br>| ……<br>| A monoidal functor is said to be ((*strong*)) when F_0 and all the F_2(a,b) are isomorphisms.<br><br>これは違うと思います。<br>やっぱり「一般に strong ??? というのは〜」というのは一般化しすぎでした……(汗<br># ちなみに、τは tensorial strength と呼ばれるのですが、他にも functorial strength とかもあったりします。