圏論

リンク


圏論勉強会インデックス

第1回(動画スライド)


第2回(動画スライド)


第3回(動画スライド)


第4回(動画スライド)


第5回(動画スライド)


第6回(動画スライド)


第7回(動画スライド)


第8回(動画スライド)


第9回(動画スライド)


第10回(動画スライド)


第11回(動画スライド)


第12回(動画スライド)


第13回(動画スライド)


メモ書き

対象と射からなる構造、以下を満たす
      恒等射
      射の合成
  結合律
  単位元



Hask圏

  • 圏 Hask とその部分圏を扱う。
  • 対象は型である。
  • 射は関数である。
  • 型を取り別の型を返すものが型構成子である。         ⇒  対象関数 (ex. Maybe a)
  • 関数をとり別の関数を返すものが高階関数である。 ⇒ 射関数 (ex. fmap)



Monoid

  • 二項演算である
  • 二つの引数と戻り値は同圏である
  • 単位元が存在すること 
  • 結合的であること

加算、乗算は、自然数(0を含む)に対してモノイドである

Haskellにおける型クラス

class Monoid a where
        mempty  :: a
        mappend :: a -> a -> a
        mconcat :: [a] -> a
        mconcat = foldr mappend mempty

Functor

1つの圏から1つの圏への写像

「射」を写すのが射関数
「対象」を写すのが対象関数

Functor則

      1. T(id) = id'
      2. T(f . g) = T(f) . T(g)
1においては、idとid'はそれぞれの圏の恒等関数。
2 は準同型写像が備えるべき条件
2つの圏の構造の相同性があることがわかる。

HaskellにおけるFunctor

    • 射関数
class  Functor f  where
    fmap :: (a -> b) -> f a -> f b

射関数なので、圏論においては、以下の意味が近いのかな。

class  Functor f  where
    fmap :: (a -> b) -> (f a -> f b)

    • 対象関数
型構成子
    例) Maybe a

Applicative

HaskellにおけるApplicative
class Functor f => Applicative f where
    pure :: a -> f a
    (<*>) :: f (a -> b) -> f a -> f b
    (*>) :: f a -> f b -> f b
    (*>) = liftA2 (const id)
    (<*) :: f a -> f b -> f a
    (<*) = liftA2 const

f (a->b) の作り方

fmap で (+)関数を射関数で向こうの圏に写す
>
> let x = fmap (+) :: (Maybe Int -> Maybe (Int -> Int))
> :t x
x :: Maybe Int -> Maybe (Int -> Int)
>

対象関数で写した対象を適用する
> let y = x $ pure 1
> :t y
y :: Maybe (Int -> Int)
>

Utility Function

fmapをoperator化
(<$>) :: Functor f => (a -> b) -> f a -> f b
(<$>) = fmap

二項演算を向こう側に写す

liftA2 :: Applicative f => (a -> b -> c) -> f a -> f b -> f c

例えば足し算
> let x = liftA2 (+) :: (Maybe Int -> Maybe Int -> Maybe Int)
>

liftA3もあるよ

Applicativeは、こっち側から向こう側の操作をリモートコントロールするための便利な概念、ユーティティですね。
> liftA2 (+) (Just 1) (Just 2)
Just 3
> (+) <$> Just 1 <*> Just 2
Just 3
>

Monad


代数スタイルのモナドの定義

モナドは、自己関手T(射関数、対象関数) と 2つの自然変換 (単位元 η  と乗法 μ)  の3つ組のこと


拡張スタイルのモナドの定義

モナドは、自己関手T(対象関数) と 自然変換 (単位元 η) と 拡張 の3つ組のこと  (Kleisli Tripple)




Haskell におけるモナドの定義


 スタイル 自己関手 自然変換 拡張
 代数スタイル
 対象関数    型構成子 
 射関数 fmap
  単位元  return、pure
  乗法  join
 -
 拡張スタイル 対象関数  型構成子 単位元 return、pure  (=<<)
  • 単位元
Prelude Control.Monad> :t return
return :: Monad m => a -> m a
Prelude Control.Monad>
Prelude Control.Applicative> :t pure
pure :: Applicative f => a -> f a
Prelude Control.Applicative>

  • 乗法
Prelude Control.Monad> :t join
join :: Monad m => m (m a) -> m a
Prelude Control.Monad>

  • 拡張
Prelude Control.Monad> :t (=<<)
(=<<) :: Monad m => (a -> m b) -> m a -> m b
Prelude Control.Monad>

  • 拡張+適用 (おまけ)
Prelude Control.Monad> :t (>>=)
(>>=) :: Monad m => m a -> (a -> m b) -> m b
Prelude Control.Monad>


Monoid から Monad


「モナドは単なる自己関手の圏におけるモノイド対象だよ。何か問題でも?」
                                  フィリップ・ワドラー


MonadからKleisli 圏



自然変換 on Haskell

自然変換 on Haskell

随伴(Unit/Counit definition)

随伴(Unit/Counit definition)


モナド:随伴から導出

モナド:随伴から導出


自由モナド:自由モノイドから考察

自由モナド:自由モノイドから考察

自由モナド:自由モノイドから考察

自由モナド:自由モノイドから考察


自由モナド:自由モノイドから考察


図示:米田の補題

図示:米田の補題

Yoneda on Haskell

Yoneda on Haskell

CoYoneda on Haskell

CoYoneda on Haskell

Yoneda と CoYoneda

YonedaとCoYoneda

Free / CoYoneda / Operational on Haskell

  • Free版
import Control.Monad.Free

-- |
-- 例で使用するデータ型
--
data Exp a where
  Const :: a -> Exp a
  Add   :: Exp a -> Exp a -> Exp a
  deriving (Show)

-- |
-- インターフェース
--
data ExpF r a where
  ConstF :: r -> (Exp r -> a) -> ExpF r a
  AddF   :: Exp r -> Exp r -> (Exp r -> a) -> ExpF r a
  deriving (Functor)  -- ★ Functorの必要がある

-- |
-- Abstract Program
--
programF :: Free (ExpF Int) (Exp Int)
programF = do
  x <- constF 2
  y <- constF 3
  z <- addF x y
  return z

-- |
-- Lift
--
constF :: r -> Free (ExpF r) (Exp r)
constF x = Free $ ConstF x Pure

addF :: Exp r -> Exp r -> Free (ExpF r) (Exp r)
addF x y = Free $ AddF x y Pure

-- |
-- 忘却函手
--
forgetF :: Free (ExpF r) (Exp r) -> Exp r
forgetF (Pure x) = x
forgetF (Free (ConstF x cont)) = forgetF $ cont $ Const x
forgetF (Free (AddF x y cont)) = forgetF $ cont $ Add x y


  • CoYoneda版
-- |
-- 米田の双対(参照:category-extras)
--
data CoYoneda f x where
  CoYoneda :: (a -> x) -> f a -> CoYoneda f x

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

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

-- |
-- インターフェース
--
data ExpY n a where
  ConstY :: n -> (Exp n -> a) -> ExpY n a
  AddY   :: Exp r -> Exp r -> (Exp r -> a) -> ExpY r a
-- ★ Functorである必要なし

-- |
-- Abstract Program
--
programY :: Free (CoYoneda (ExpY Int)) (Exp Int)
programY = do
  x <- constY 2
  y <- constY 3
  z <- addY x y
  return z

-- |
-- Lift
--
constY :: n -> Free (CoYoneda (ExpY n)) (Exp n)
constY n = Free $ liftCoYoneda $ ConstY n Pure

addY :: Exp n -> Exp n -> Free (CoYoneda (ExpY n)) (Exp n)
addY x y = Free $ liftCoYoneda $ AddY x y Pure

-- |
-- 忘却函手
--
forgetY :: Free (CoYoneda (ExpY n)) (Exp n) -> Exp n
forgetY (Pure n) = n
forgetY (Free (CoYoneda f (ConstY n cont))) = forgetY $ f $ cont $ Const n
forgetY (Free (CoYoneda f (AddY x y cont))) = forgetY $ f $ cont $ Add x y


  • Operational版
import Control.Monad.Operational.Mini

-- |
--  インターフェース
--
data Exp n where
  Const :: n -> Exp n
  Add   :: Exp n -> Exp n -> Exp n
  deriving (Show)

data ExpO n where
  ConstO :: n -> ExpO (Exp n)
  AddO   :: Exp n -> Exp n -> ExpO (Exp n)

-- |
-- Abstract Program
--
programO :: (Num n) => ReifiedProgram ExpO (Exp n)
programO = do
  x <- constO 2
  y <- constO 4
  z <- addO x y
  return z

-- |
-- Lift
--
constO :: n -> ReifiedProgram ExpO (Exp n)
constO = singleton . ConstO

addO :: Exp n -> Exp n -> ReifiedProgram ExpO (Exp n)
addO a b = singleton $ AddO a b

-- |
-- 忘却函手
--
forgetO :: ReifiedProgram ExpO (Exp n) -> Exp n
forgetO (Return n) = n
forgetO (ConstO n :>>= cont) = forgetO . cont $ Const n
forgetO (AddO a b :>>= cont) = forgetO . cont $ Add a b


ghci> forgetO programO
Add (Const 2) (Const 4)

ghci>



      ą
      Aaa Zzz,
      2015/03/11 16:26
      ą
      Aaa Zzz,
      2015/03/11 16:39
      ą
      Aaa Zzz,
      2015/03/11 17:11
      ą
      Aaa Zzz,
      2015/03/13 18:11
      ą
      Aaa Zzz,
      2015/03/13 18:12
      ą
      Aaa Zzz,
      2015/03/13 18:12
      ą
      Aaa Zzz,
      2015/03/13 18:12
      Comments