DiscreteCategory.hs

{-# LANGUAGE
  GADTs,
  RankNTypes,
  PolyKinds,
  DataKinds,
  ScopedTypeVariables,
  StandaloneKindSignatures
#-}
module DiscreteCategory where

import Data.Kind

newtype Const a b = Const { getConst :: a }

-- 図にあった「2」という圏は、対象を二つだけ {1,2} と持ち、
-- 射は各要素上の恒等射id_1とid_2だけを持つような圏です。
-- このように恒等射しか持たない圏を離散圏とよびます。

-- 離散圏は以下のように実装できます
data Discrete k (a :: k) (b :: k) where
    Refl :: Discrete k a a

-- | 離散圏Discrete Boolから(->)の関手
type FunctorFromBool :: (Bool -> Type) -> Constraint
class FunctorFromBool f where
    -- 実のところこの型クラスは不要
    -- "fmap"が以下のデフォルト実装以外にあり得ないため
    fmapFromBool
      :: forall (x :: Bool) (y :: Bool).
         Discrete Bool x y -> (f x -> f y)
    fmapFromBool Refl = id

-- FunctorFromBool間の自然変換
newtype NatTrans f g = NatTrans {
        runNatTrans :: forall x. (KnownBool x) => f x -> g x
    }

toNatTrans :: (f False -> g False) -> (f True -> g True) -> NatTrans f g
toNatTrans t1 t2 = NatTrans $ \fx -> case boolVal fx of
    SFalse -> t1 fx
    STrue  -> t2 fx

fromNatTrans :: NatTrans f g -> (f False -> g False, f True -> g True)
fromNatTrans (NatTrans tr) = (tr, tr)

-- KnownBoolは、kindがBoolの型変数に"パターンマッチ"をするためのトリック
-- この手法を強力に支援する「singletons」というライブラリもあります

data SBool x where
    SFalse :: SBool 'False
    STrue  :: SBool 'True

class KnownBool x where
    sBool :: SBool x

instance KnownBool 'False where
    sBool = SFalse
instance KnownBool 'True where
    sBool = STrue

boolVal :: KnownBool x => proxy x -> SBool x
boolVal _ = sBool