メモ

{-# LANGUAGE GADTs #-}

data Ident a where
    Ident :: a -> Ident a

instance Functor Ident where
    -- fmap :: (a -> b) -> Ident a -> Ident b
    fmap f (Ident a) = Ident (f a)

in1 :: Ident () -> ()
in1 = const ()

in2 :: Ident Bool -> Bool
in2 (Ident a) = a

hom1 :: () -> Bool
hom1 = const True

hom2 :: () -> Bool
hom2 = const False

f1 :: Ident () -> (Bool,Bool)
f1 x = (hom1 . in1 $ x,in2 . (fmap hom1) $ x)

f2 :: Ident () -> (Bool,Bool)
f2 x = (hom2 . in1 $ x,in2 . (fmap hom2) $ x)

Unit-Typeは、恒等関手に関するAlgebra(I-alg)と更にその忘却関手UIに対するconeにはならないですよねぇ・・・。ならないんですかね・・・？

話の流れとしては、今個人的ブームの
"Build,Augment and Destroy,Universally"(すぷりんが : http://www.springerlink.com/content/2m8ev9wwmwveljjk/)
という論文に関する話です。

この論文の中で、build関数の型が

build : (∀x.(F x → x) → C → x) → C → μF

ここでCは、関手FのF-algebraがあり、その忘却関手UFのconeになるもの

として与えられます。

しかしながら、Haskellの有名なfold/build fusion ruleのbulid( 参考 : http://haskell.org/ghc/docs/6.12.1/html/libraries/base-4.2.0.0/src/GHC-Base.html#foldr )は

foldr    :: (a -> b -> b) -> b -> [a] -> b

build   :: forall a. (forall b. (a -> b -> b) -> b -> b) -> [a]

(a -> b -> b) -> bが(F x → x)相当で、[a]がμF相当

で明らかにCが消えているわけです。Cに自明なconeを割当ててあげると多分良いのかしらーって事で、そういう時はunitとかだよなー。

でもunitをCとして取る為には、unitが任意の関手FのF-algと、忘却関手UFを取った時にconeにならないといけないはずで、そうすると恒等関手でもいけるべき！！ → でもいけてないっぽい。

というのが一連の流れ。