FOP/ex10.1 - 大久保弘崇

10.1

instance Arrow (Reader s) where
  pure f = R (\ (_, b) -> f b)
  R f >>> R g = R (\ (s,i) -> g (s, f (s,i))
  first (R f) = R ( (f × id) . unassoc)
 
instance Arrow Writer where
  pure f = W (\ b -> ([], f b))
  W f >>> W g = W (\ b ->
    let (s1, o1) = f b
        (s2, o2) = g o1
    in  (s1 ++ s2, o2)
  first (W f) = W (assoc . (f × id))
 

10.2

型を合わせることを第一に考えて、概ね以下のような実装になるだろう。

instance Arrow ListMap where
  pure = LM . map
  LM f >>> LM g = LM (g.f)
  first (LM f) = LM (\ids -> let { (is, ds) = unzip ids; } in zip (f is) ds)
 

ここで直感的には、
ListMapはpureな関数から作る必要はないため、そのようなときに
ListMapの関数は[i]の要素それぞれをどう[o]に対応させているか不明になる。
これが[(i,d)]→[(o,d)]になったとき、dをどうしてよいかは明らかでない。

appLM (LM f) = f -- 計算を発動させる
LM reverse `appLM` [(1, 'a'), (2, 'b'), (3, 'c')]
LM (foldr (\x->(x:).(x:)) []) `appLM` [(1, 'a'), (2, 'b'), (3, 'c')]
 

などを考えてみよ。

もう少し厳密に考える。
f = LM (repeat.head) とする。
firstは則を満たさなければならない。単位(unit)則を上の例のような有限長のリストに適用することを考えると、
左辺はsndのおかげで止まるが、右辺は先にsndが外されてしまうために無限長になってしまい、等しくならない。

本当に厳密に考えるには、「どのようなfirstを持ってきても、則を満たさない反例が出現する」ことを証明しないといけないが、
問題文に「証明せよ」と書かれていないのはこの程度の説明でよいというニュアンスと読む。

10.3

instance Arrow StreamMap where
  pure f = SM (mapStream f)
  SM f >>> SM g = SM (g . f)
  first (SM f) = SM (zipStream . (f × id) . unzipStream)
 
mapStream :: (a -> b) -> Stream a -> Stream b
mapStream f (Cons x xs) = Cons (f x) (mapStream f xs)
zipStream :: (Stream a, Stream b) -> Stream (a, b)
zipStream (Cons x xs, Cons y ys) = Cons (x, y) (zipStream (xs, ys))
unzipStream :: Stream (a, b) -> (Stream a, Stream b)
unzipStream (Cons (x, y) xys) = (Cons x xs, Cons y ys) where (xs, ys) = unzipStream xys
 

http://www.soi.city.ac.uk/~ross/talks/fop.pdf を参考にした。
後はこの定義が「恒等性」「結合性」「関手恒等性」「関手合成」「拡張」「関手」「交換」「単位」「結合」の各lawを満たすことを証明するだけでよい。

10.4

2引数関手fuの満たすべきlawは、idA = pure id として、以下の2つ。
Identity: fu idA idA == idA
Composition: fu (f >>> g) (h >>> k) == fu f h >>> fu g k
は左は考えている圏、右は関数圏で固定される「いびつな」関手。

identity

{定義}
{拡張}
{関手}
{関手合成}
{idの性質、拡張}
{×は2引数関手なのでIdentityを満たす}

Composition

{定義}
{関手}

{定義}
{結合性と交換}
first f と first g は同じになったので、残りだけを考える

{関手合成}
{×は2引数関手なのでCompositionを満たす}
{idの性質、h,kは関数圏の関手なのでその>>>の定義}

コメント