FOP/ex10.2 - 大久保弘崇

10.5

合成

LHS = pure ((>>> h) × id) >>> app
= app . ((h .) × id)
LHS (f, x) = app ( ((h .) × id) (f, x) )
= app ( h.f, id x )
= (h.f) x
RHS = app >>> h
= h . app
RHS (f, x) = h (app (f, x)) = h (f x)

簡約

RHS = pure id = id
LHS = pure (mkPair × id) >>> app
= app . (mkPair × id)
LHS (a, b) = app ( (mkPair × id) (a, b) )
= app (mkPair a, id b)
= (mkPair a) b = (a, b)

外延性

LHS = mkPair f >>> app
= app . mkPair f
LHS x = app (mkPair f x) = app (f, x) = f x

10.6

app = pure (λ (A f, x) → fst (f x)) = pure fa とおく。すると = A (λb → (fa b, pure fa)) = A (λ (A f, x) → (fst (f x), app)) = A fa' とおく。
外延性 mkPair f >>> app = f
mkPair f = pure (λc → (f, c)) = pure f1 とおく。すると = A (λb → (f1 b, pure f1)) = A (λc → ((f, c), mkPair f) = A f1' とおく。
LHS = mkPair f >>> app = A f1' >>> A fa'
= A (λb → let { (c,f') = f1' b; (d,g') = fa' c; } in (d, f' >>> g') )
= A (λb → let { c = (f, b); f' = mkPair f; (d,g') = fa' (f, b); } in (d, f1' >>> g') )
ここで、fは実はAutoのarrowなので、f = A fi という形に表せるはず。よって続けると、
= A (λb → let { c = (f, b); f' = mkPair f; (d,g') = fa' (A fi, b); } in (d, f1' >>> g') )
= A (λb → let { c = (f, b); f' = mkPair f; d = fst (fi b); g' = app } in (fst (fi b), mkPair f >>> app) )
= A (λb → (fst (fi b), mkPair f >>> app))
このAの中にある関数の返す値のうち、左側は正しい。しかし右側は正しくない。状態遷移していないから。
正しいfは、
f = A fi = A (λb → fi b) = A (λb → (fst (fi b), snd (fi b)))

10.7

instance ArrowChoice NonDet where
  left (ND f) = ND lf where
    lf (Left b) = map Left (f b)
    lf (Right c) = [Right c]
 
instance ArrowChoice (State st) where
  left (ST f) = ST lf where
    lf (s, Left b) = let (s',d) = f (s,b); in (s', Left d)
    lf (s, Right c) = (s, Right c)
 
instance ArrowChoice StreamMap where
  left (SM f) = SM (\xs -> comb xs (f (lefty xs)))
 
lefty (Cons (Left x) xs) = Cons x (lefty xs)
lefty (Cons (Right x) xs) = lefty xs
comb (Cons (Left x) xs) (z:zs) = Cons (Left z) : comb xs zs
comb (Cons (Right y) xs) zs = Cons (Right y) : comb xs zs
 

型は合っているが、則を満たしているかは確認していない。
StreamMapについては afp-arrows を参考にした。

StreamMapに対する古い、おそらく誤っている解。LeftもRightも無限に来ることを前提にしている。

fork :: Stream (Either a b) -> Stream (a, b)
fork st = fork2 (fork1 st)
fork1 :: Stream (Either a b) -> (Stream a, Stream b)
fork1 (Cons b st) = let (stL, stR) = fork1 st in case b of
  Left l -> (Cons l stL, stR)
  Right r-> (stL, Cons r stR)
fork2 :: (Stream a, Stream b) -> Stream (a,b)
fork2 (Cons l stL, Cons r stR) = Cons (l, r) (fork2 (stL, stR))
 
unfork :: Stream (a, b) -> Stream (Either a b)
unfork (Cons (l,r) st) = Cons (Left l) $ Cons (Right r) (unfork st)
 
instance ArrowChoice StreamMap where
  left f = SM fork >>> first f >>> SM unfork
 

10.8

State

Autoなら状態を持つ実体が分散するから違うと判るが、
Stateは状態を追加で受け取るだけの純関数と言えるので、
どういう例を持ちだせばよいのか判らない。

StreamMap

反例を示す。

-- take k . apply stream
appSMtake (SM f) st k = take k (f st) where
  take 0 _ = []
  take k (Cons x xs) = x:take (k-1) xs
 
infixr `Cons`
 
ex108sm = (appSMtake lhs st0 8, appSMtake rhs st0 8) where
  st0 = st 0
  st k = Left k `Cons` Right (k+1) `Cons` st (k+2)
  lhs = (f ||| g) >>> h
  rhs = (f >>> h) ||| (g >>> h)
  f = SM id
  g = SM id
  h = SM h0 where h0 (Cons x xs) = Cons x (Cons x (h0 xs))
 

hによる2重化と|||によるunforkのタイミングが異なるために結果が変わる、
というのはあくまで自分のStreamMapのleftの定義に依存するので、これで正しいのか全然自信がない。

コメント