FOP/ex10.3 - 大久保弘崇

10.9

newtype Except a b c = E (a b (Either String c))
instance ArrowChoice a => Arrow (Except a)
 

ミッション：
ArrowChoiceなアローaと型b,cがあるとき、
bから(Either String c)というアローをEで包むようなExcept aをArrowにする。
以降、アローaを、アローExcept aをと表す。またEither x y を x+y で表す。
つまりbcとbString+cは同じ意味である。

pure

pure :: (b→c) → (bc)
pure f は、fをaのコンテキストでpureでアローにして、結果をRightコンストラクタで包めばよい。

pure f = E (pure f >>> pure Right)
 

>>>

(>>>) :: (bc) → (cd) → (bd)
E f >>> E g は、まずfを計算し、その結果がRightならgを計算する。
f :: b String+c, g :: c String+d, right g :: x+c x+(String+d)
繋ぐとxはStringにunifyされる。最終結果を String+d に型合わせするための関数を追加してみる。

E f >>> E g = E (f >>> right g >>> pure destring) where
    destring (Left s) = Left s
    destring (Right (Left s)) = Left s
    destring (Right (Right v)) = Right v
 

型は合うし意味的にも正しいはずなのだが、destringという独自の関数では、次の問題の則を用いた証明が進められない。
mirrorやassocsumを用いて等価な計算を作ることができるのか、よくわからない。

first

first :: (bc) → ( (b,d)(c,d) )
first (E f)は、Leftに対してfを計算し、Rightに対してはなにもしない。しかし型は直観的ではない。
f :: bc すなわち f :: bString+c のとき
first (E f) の型は (b,d)String+(c,d) であり、(b,d)(String+c,d) ではない所が。
使える道具はaのfirstで、first f :: (b,d) (String+c,d) こちらは直観的。

first (E f) = E (first f >>> pure deright) where
    deright (Left s,d) = Left s
    deright (Right c,d) = Right (c,d)
 

証明のために、型合わせのための独自関数derightを汎用部品で構成する。
distr :: (Either a b,c) → Either (a,c) (b,c) を使えば、

first (E f) = E (first f >>> pure distr >>> left (pure fst) )
 

とできる。

10.10

上の定義と則から目標を証明できない限り、上の定義が正しいとはいえない。

コメント