在Haskell中定義類別和類別規則

Question

我很開心通過將定義和規則直接轉換爲Haskell來學習分類理論。 Haskell當然不是Coq，但它可以幫助我獲得類別理論的直覺。我的問題是：下面是將一個類別定義合理地「翻譯」成Haskell？

{- 
    The following definition of a category is adapted from "Basic Category Theory" by Jaap van Oosten: 

    A category is given by a collection of objects and a collection of morphisms. 

    Each morphism has a domain and a codomain which are objects. 

    One writes f:X->Y (or X -f-> Y) if X is the domain of the morphism f, and Y its codomain. 

    One also writes X = dom(f) and Y = cod(f) 

    Given two morphisms f and g such that cod(f) = dom(g), the composition 
    of f and g, written (g f), is defined and has domain dom(f) and codomain cod(g): 
    (X -f-> Y -g-> Z) = (X -(g f)-> Z) 

    Composition is associative, that is: given f : X -> Y , g : Y -> Z and h : Z -> W, h (g f) = (h g) f 

    For every object X there is an identity morphism idX : X -> X, satisfying 
    (idX g) = g for every g : Y -> X and (f idX) = f for every f : X -> Y. 
-} 

module Code.CategoryTheory where 

--------------------------------------------------------------------- 

data Category o m = 
    Category 
    { 
    -- A category is given by a collection of objects and a collection of morphisms: 
    objects :: [o], 
    morphisms :: [m], 
    -- Each morphism has a domain and a codomain which are objects: 
    domain  :: m -> o, 
    codomain :: m -> o, 
    -- Given two morphisms f and g such that codomain f = domain g, 
    -- the composition of f and g, written (g f), is defined: 
    compose :: m -> m -> Maybe m, 
    -- For every object X there is an identity morphism idX : X -> X 
    identity :: o -> m 
    } 

--------------------------------------------------------------------- 

-- Check if (Category o m) is truly a category (category laws) 

is_category :: (Eq o,Eq m) => Category o m -> Bool 

is_category cat = 
    domains_are_objects   cat 
    && codomains_are_objects  cat 
    && composition_is_defined  cat 
    && composition_is_associative cat 
    && identity_is_identity  cat 

--------------------------------------------------------------------- 

-- Each morphism has a domain and a codomain which are objects: 

domains_are_objects :: Eq o => Category o m -> Bool 

domains_are_objects cat = 
    all (\m -> elem (domain cat m) (objects cat)) (morphisms cat) 

codomains_are_objects :: Eq o => Category o m -> Bool 

codomains_are_objects cat = 
    all (\m -> elem (codomain cat m) (objects cat)) (morphisms cat) 

--------------------------------------------------------------------- 

-- Given two morphisms f and g such that cod(f) = dom(g), 
-- the composition of f and g, written (g f), is defined 
-- and has domain dom(f) and codomain cod(g) 

composition_is_defined :: Eq o => Category o m -> Bool 

composition_is_defined cat = 
    go $ morphisms cat 
    where 
    go []  = True 
    go (m : mx) = all (go2 m) mx && go mx 

    go2 g f = 
     if domain cat g /= codomain cat f then 
     True 
     else 
     case compose cat g f of 
      Nothing -> False 
      Just gf -> domain cat gf == domain cat f && codomain cat gf == codomain cat g 

--------------------------------------------------------------------- 

-- Composition is associative, that is: 
-- given f:X->Y, g:Y->Z and h:Z->W, h (g f) = (h g) f 

composition_is_associative :: (Eq o,Eq m) => Category o m -> Bool 

composition_is_associative cat = 
    go $ morphisms cat 
    where 
    go []   = True 
    go (m : mx)  = go2 m mx && go mx 

    go2 _ []  = True 
    go2 f (g : mx) = all (go3 f g) mx && go2 f mx 

    go3 f g h = 
     if codomain cat f == domain cat g && codomain cat g == domain cat h then 
     case (compose cat g f, compose cat h g) of 
      (Just gf, Just hg) -> 
      case (compose cat h gf, compose cat hg f) of 
       (Just hgf0, Just hgf1) -> hgf0 == hgf1 
       _      -> False 
      _ -> False 
     else 
     True 

--------------------------------------------------------------------- 

-- For every object X there is an identity morphism idX : X -> X, satisfying 
-- (idX g) = g for every g : Y -> X -- and (f idX) = f for every f : X -> Y. 

identity_is_identity :: (Eq m,Eq o) => Category o m -> Bool 

identity_is_identity cat = 
    go $ objects cat 
    where 
    go []  = True 
    go (o:ox) = all (go2 o) (morphisms cat) && go ox 

    go2 o m = 
     if domain cat m == o then 
     case compose cat m (identity cat o) of 
      Nothing -> False 
      Just mo -> mo == m 
     else if codomain cat m == o then 
     case compose cat (identity cat o) m of 
      Nothing -> False 
      Just im -> im == m 
     else 
     True 

--------------------------------------------------------------------- 

instance (Show m,Show o) => Show (Category o m) where 
    show cat = "Category{objects=" ++ show (objects cat) ++ ",morphisms=" ++ show (morphisms cat) ++ "}" 

--------------------------------------------------------------------- 

testCategory :: Category String (String,String,String) 

testCategory = 
    Category 
    { 
    objects = ["A","B","C","D"], 
    morphisms = [("f","A","B"),("g","B","C"),("h","C","D"),("i","A","D")], 
    domain = \(_,a,_) -> a, 
    codomain = \(_,_,b) -> b, 
    compose = \(g,gd,gc) (f,fd,fc) -> 
      if fc /= gd then 
       Nothing 
      else if gd == gc then 
       Just (f,fd,fc) 
      else if fd == fc then 
       Just (g,gd,gc) 
      else 
       Just (g ++ "." ++ f,fd,gc), 
    identity = \o -> ("id" ++ show o, o, o) 
    } 

--------------------------------------------------------------------- 

main :: IO() 

main = do 
    putStrLn "Category Theory" 
    let cat = testCategory 
    putStrLn $ show cat 
    putStrLn $ "Is category: " ++ show (is_category cat) 

Answer 1

這似乎是在原始結構的翻譯不是傳球。但是您不能利用類型系統爲您檢查的任何。

數據類包（https://hackage.haskell.org/package/data-category）使用一個巧妙的方法做你的建設「上一級」和執行的態射等組成部分屬性...

核心是

class Category k where 
    src :: k a b -> Obj k a 
    tgt :: k a b -> Obj k b 
    (.) :: k b c -> k a b -> k a c 

type Obj k a = k a a 

在這裏，他只表示態射體及其組成，然後簡單地將對象捕獲爲這些對象上的身份態射。我發現這個庫在它的表達能力上非常強大。