• 野生のHaskller(27♂)
• 東京都近郊に生息・現NEET
  　
• クルージング(スケボー)
• SOUND VOLTEX(音ゲー)
• リトルノア（スマフォゲー）
  　
• ゆずこ（ゆゆ式）可愛い
• ヲ級ちゃん可愛い
• 艦これやってない

以下の全単射の存在を示す定理
米田関手（後述）と呼ばれる関手が充満忠実である事を証明する

マックレーン「圏論の基礎」による証明
「以下の可換図式によって示される」

米田の補題の証明には、以下の前提が必要

αは自然変換なので
「圏論の基礎」で示されていた以下の図式は可換

左辺に1rを作用

右辺に1rを作用

αd(f)=Kf(αr1r)は∀f:r->dで成り立つ
よってαr1rが定まればαが定まる

αとαr1rは、米田の補題の左辺と右辺
ここまでの説明は片方の集合から
もう片方が完全に定まる事を示していた

よって、以下の集合間に全単射が存在する事が証明される

この補題は、以下のように定義された
米田関手が充満忠実である事を証明する

米田関手の双対として、
米田埋め込みという充満忠実な関手がある。
これは任意の圏をSetに移せるため有用・・・だそうだ。

newtype Yoneda f x
= Yoneda { runYoneda :: forall b. (x -> b) -> f b }

Yoneda型は以下のようにしてFunctorにすることで、
米田の補題により、任意のFunctor f と同値になる。

instance Functor (Yoneda f) where
fmap f (Yoneda m) = Yoneda $ \k -> m (k . f)

たとえば、Yoneda Maybe a は
Functorとして完全に Maybe a 型に代用する事が出来る。

Yoneda型が任意のFunctorの代用になる事を確認するため、
簡単な関数を定義しておこう。

lowerYoneda :: Yoneda f a -> f a
lowerYoneda (Yoneda m) = m id

liftYoneda :: Functor f => f a -> Yoneda f a
liftYoneda v = Yoneda $ \k -> fmap k v

その上で、以下のコードを実行する事で
Yoneda型を仲介しても結果は変わらない事が確認できる。

ndigits :: Functor f => f Int -> f Int
ndigits = fmap length . fmap show

main :: IO ()
main = do
-- Just 114514
print . ndigits $ Just 114514
print . lowerYoneda . ndigits . liftYoneda $ Just 114514
-- Nothing
print . ndigits $ Nothing
print . lowerYoneda . ndigits . liftYoneda $ Nothing

Yoneda型を構成する際にmapの計算を組み込めれば、
元になる型がFunctorのインスタンスになっている必要はない。
関手が存在するかどうかは、型そのものの性質だからである。

data MyMaybe a = MyJust a | MyNothing
deriving (Show, Read, Eq, Ord)

yonedaMM :: MyMaybe a -> Yoneda MyMaybe a
yonedaMM (MyJust x) = Yoneda $ \k -> MyJust (k x)
yonedaMM MyNothing = Yoneda $ \_ -> MyNothing

main :: IO ()
main = do
print . lowerYoneda . fmap (*2) . yonedaMM $ MyJust 114514
print . lowerYoneda . fmap (*2) . yonedaMM $ MyNothing

改めて、Yonedaのfmapの実装を見てみよう。
mapした際に行われるのは基本的に関数操作である。

instance Functor (Yoneda f) where
fmap f (Yoneda m) = Yoneda $ \k -> m (k . f)

データへの直接的な操作はオーバーヘッドになり兼ねない。
つまりYonedaは、Functorに対する大きな操作の、
パフォーマンス対策ツールになり得る。

米田の補題の双対として「余米田の補題」があり、
余米田の補題は、以下のようにHaskell上で実装される。

data CoYoneda f x = forall b. CoYoneda (b -> x) (f b)

instance Functor (CoYoneda f) where
fmap f (CoYoneda g v) = CoYoneda (f . g) v

CoYonedaは概ね、Yonedaと同等の機能を持つ。

liftCoYoneda :: f a -> CoYoneda f a
liftCoYoneda = CoYoneda id

lowerCoYoneda :: Functor f => CoYoneda f a -> f a
lowerCoYoneda (CoYoneda f x) = fmap f x

main :: IO ()
main = do
print . lowerCoYoneda . ndigits . liftCoYoneda $ Just 114514
print . lowerCoYoneda . ndigits . liftCoYoneda $ Nothing

YonedaとCoYonedaの双対性は、
lift, lower関数の型定義に明確に現れる。

liftYoneda :: Functor f => f a -> Yoneda f a
liftCoYoneda :: f a -> CoYoneda f a

lowerYoneda :: Yoneda f a -> f a
lowerCoYoneda :: Functor f => CoYoneda f a -> f a

Yonedaはliftの際にmap操作が決定しなくてはいけない、
対して、CoYonedaはlowerで決定する。

Yonedaの場合と同様、lowerの際にmapの計算を組み込めれば、
その型自体がFunctorのインスタンスである必要はない。

coyonedaMM :: CoYoneda MyMaybe a -> MyMaybe a
coyonedaMM (CoYoneda f (MyJust x)) = MyJust $ f x
coyonedaMM (CoYoneda _ _) = MyNothing

main :: IO ()
main = do
print . coyonedaMM . fmap (*2) . liftCoYoneda $ MyJust 114514
print . coyonedaMM . fmap (*2) . liftCoYoneda $ MyNothing

対角自然変換（くさび）とは、
以下の割り当てを行う関数の事である。

エンドとは、あるe:Xと、くさびω:e->Sの組であり、
以下の規則を満たし、図式を可換にするもの。

また、エンドの対象e自体も述語の汎用でエンドと呼ばれ、
積分記号を用いて以下のように記述される。

エンドの双対コエンドは、
あるd:Xと、くさびζ:d->Sの組であり、

エンドと同様、d自体もコエンドと呼ばれ、
積分記号を用いて以下のように記述される。

米田の補題はエンドを用いて、
以下のように定義する事も可能で・・・

余米田の補題はコエンドを用いて、
以下のように定義される・・・のだそうだ。

Freeと呼ばれる型は以下のように定義され、
FunctorおよびMonadのインスタンスとなる

data Free f r = Free (f (Free f r)) | Pure r

instance Functor f => Functor (Free f) where
fmap f x = x >>= return . f

instance Functor f => Monad (Free f) where
return = Pure
Free x >>= f = Free $ fmap (>>= f) x
Pure x >>= f = f x

liftF関数を使い
Functorインスタンスのデータコンストラクタを元に、
Freeモナドのモナドアクションを生成できる。

liftF :: Functor f => f r -> Free f r
liftF cmd = Free (fmap Pure cmd)

-----

just :: a -> Free Maybe a
just = liftF . Just

nothing :: Free Maybe a
nothing = liftF Nothing

このようにして作成されたFree Maybeモナドは
実質的に、Freeモナドと同様に記述する事ができ・・・

sample1 :: Free Maybe Int
sample1 = do
x <- just 10
y <- just 20
return $ x + y

sample2 :: Free Maybe Int
sample2 = do
x <- just 10
y <- nothing
return $ x + y

retract関数を使い、
Maybeモナドと同様の結果を得る事が出来る。

main :: IO ()
main = do
print . retract $ sample1 -- Just 30
print . retract $ sample2 -- Nothing

このように、Freeモナドは任意のモナドの代用となる。

liftF関数は任意のFunctorを元に、
Freeのモナドアクションを生成する。

data MyMaybe a = MyJust a | MyNothing
deriving (Show, Read, Eq, Ord, Functor)

just :: a -> Free MyMaybe a
just = liftF . MyJust

nothing :: Free MyMaybe a
nothing = liftF MyNothing

Freeから内包した型を引き剥がす関数を定義できれば、
その型がMonad型クラスのインスタンスである必要はない。

runFreeMaybe :: Free MyMaybe a -> MyMaybe a
runFreeMaybe (Free (MyJust x)) = runFreeMaybe x
runFreeMaybe (Free _) = MyNothing
runFreeMaybe (Pure a) = MyJust a

これはYonedaがそうであったように、
Monadの存在は、ある型の性質に過ぎないからである。

FreeとCoYoneda、二つを組み合わせて、
任意の型を一気にMonadとして扱えるようにする。

これが、Operationalモナドの基本的なアイディアである。

newtype Program f a
= Program { toFree :: Free (CoYoneda f) a }

instance Monad (Program f) where
return = Program . return
x >>= f = Program $ toFree x >>= toFree . f

Operationalを利用してDSLを作成する場合、
まず最初にGADTsを用いて必要なAPIを羅列する。

ここでProgram型と組み合わせたtype宣言をしておくと良い。

data IntIOBase a where
PutInt :: Int -> IntIOBase ()
GetInt :: IntIOBase Int
PrintInt :: IntIOBase ()

type IntIO = Program IntIOBase

データコンストラクタをモナドアクションにするには、
singleton関数を利用すると良い。

singleton :: f a -> Program f a
singleton = Program . liftF . liftCoYoneda

putInt :: Int -> IntIO ()
putInt = singleton . PutInt

getInt :: IntIO Int
getInt = singleton GetInt

printInt :: IntIO ()
printInt = singleton PrintInt

各アクションが具体的に何を行うか、まだ指定していない。

しかし、Program型はモナドなので、この時点でdo記法によって、
プログラムを記述する事が可能になっている。

sample :: IntIO ()
sample = do
printInt
putInt 100
printInt
putInt 200
printInt

DSLを実行する関数の構築には、interpret関数を用いると良い。

第一引数には、
DSLを他の具体的なモナドに翻訳する関数を指定する。

interpret :: forall instr m b. Monad m =>
(forall a. instr a -> m a) -> Program instr b -> m b
interpret g (Program (Free (CoYoneda f x)))
= g x >>= interpret g . Program . f
interpret _ (Program (Pure a)) = return a

以下は、interpret関数の具体的な使用例である。

runIntIO :: IntIO a -> Int -> IO a
runIntIO t i = evalStateT (interpret advent t) i
where
advent :: IntIOBase a -> StateT Int IO a
advent (PutInt x) = put x
advent GetInt = get
advent PrintInt = get >>= liftIO . print