Hask圏の関手圏と自然同型

関手圏$ \mathrm{Hask}^\mathrm{Hask}

https://gyazo.com/ed63c9f1f22dfd89cfcaa9a8e9f192c9

自然同型

上図の他のものを見る

https://gyazo.com/7441c21aae3cb8637a7495d14753aeb4

code:hs

alpha :: Maybe a -> Either () a

alpha Nothing = Left ()

alpha (Just x) = Right x

beta :: Either () a -> Maybe a

beta (Left ()) = Nothing

beta (Right x) = Just x

betaはalphaの逆射になっている

code:hs

beta.alpha == id_maybe

alpha.beta == id_either

alpha、betaは多相的な関数なので、自然変換である

これらは同型である自然変換なので、Maybe, Eitherにおける自然同型である

「自然同型」というものが、「2つの関手が本質的に同じ」であることを示すのであれば、上の議論から

Maybe aとEither () aは本質的に何の違いもない、ということが言える

aにIntを代入するなら

正規の値の方は例えば

code:hs

Just 100

Right 100

失敗の値の方は

code:hs

Nothing

Left ()

と、なる

これらを同じものとみなせば、関手自体を全く同じものと見なすことができる

参考