CategoriesAndCS

Categories and Computer Science

  Slides and other references

• What is Category Theory(219)

  Haskell

I am sure you have already GHC(compiler) and GHCI(interpreter). If it is not the case, you should consult with Google or something and install the required software.

  もっとも単純な例と第１回課題

以下のプログラムは対象がAのみ、identityを除いて矢がalphaのみの圏である。ファイル名は"ex4-1.hs"とする。

-- a category ex4-1
-- with one object o_a and one arrow alpha other than the identity

-- type synonym for String
type Object = String

-- The Arrow type has two data constructors
data Arrow = Arrow String Object Object | Id Object
  deriving (Eq, Show)

-- The dom function takes an arrow as argument and returns the domain of the arrow.
dom :: Arrow -> Object
dom (Arrow st o1 o2) = o1
dom (Id o1) = o1

-- The codom function takes an arrow as argument and returns the codomain of the arrow.
codom :: Arrow -> Object
codom (Arrow st o1 o2) = o2
codom (Id o1) = o1

-- "cat" is short for "concatenate."  
-- The cat function takes two arrows as arguments and returns their composition.
cat :: Arrow -> Arrow -> Maybe Arrow
cat (Id o1) (Id o2) 
  | o1 == o2 = Just (Id o1)
  | otherwise = Nothing
cat (Arrow st o1 o2) (Id o3) 
  | o1 == o3 = Just (Arrow st o1 o2)
  | otherwise = Nothing
cat (Id o3) (Arrow st o1 o2)  
  | o2 == o3 = Just (Arrow st o1 o2)
  | otherwise = Nothing
cat g f
  |  dom g /= codom f  =  Nothing  -- Removing this guard does not affect the result. Then, what for?
  |  otherwise         =  lookup (g, f) compTable

unsafeCat :: Arrow -> Arrow -> Arrow
unsafeCat (Id o1) (Id o2) 
  | o1 == o2 = (Id o1)
  | otherwise = error "cannot compose"
unsafeCat (Arrow st o1 o2) (Id o3) 
  | o1 == o3 =  (Arrow st o1 o2)
  | otherwise = error "cannot compose"
unsafeCat (Id o3) (Arrow st o1 o2)  
  | o2 == o3 =  (Arrow st o1 o2)
  | otherwise = error "cannot compose"
unsafeCat g f
  |  dom g /= codom f  =  error "cannot compose"
  |  otherwise         =  case (lookup (g, f) compTable) of
                          Nothing    -> error "cannot compose"
                          Just value -> value


-- Define object o_a
o_a :: Object
o_a = "A"

-- Define arrow alpha
alpha = Arrow "alpha" o_a o_a

-- Define the composition table for this category
compTable :: [((Arrow, Arrow), Arrow)]
compTable = [((alpha,alpha), Id o_a)]

-- this category consists of ..
objs = [o_a]   -- The list of all objects
arrows = [(Id o_a), alpha]   -- The list of all arrows

-- generate the complete list of test cases for closedness
test_pairs = [ (f, g) | f <- arrows, g <- arrows, dom f == codom g]

-- The following two functions are to test closedness 
---- map (uncurry cat) test_pairs
---- elem Nothing $ map (uncurry cat) test_pairs

-- generate the complete list of test cases for associativity
test_triples = [ (f, g, h) | f <- arrows, g <- arrows, h <- arrows, dom f == codom g, dom g == codom h]

-- test for each triple
assoc_test :: (Arrow, Arrow, Arrow) -> Bool
assoc_test (f, g, h) = (unsafeCat (unsafeCat f g) h)==(unsafeCat f (unsafeCat g h))
-- To avoid using unsafe version of Cat, we have to deal with Maybe monad directly

-- The following two functions are to test associativity 
---- map assoc_test test_triples
---- elem False $ map assoc_test test_triples

閉じているかテスト

ghciを起動して

:load ex4-1

を実行後

map (uncurry cat) test_pairs

を実行してみよ。さらに、

elem Nothing $ map (uncurry cat) test_pairs

の結果がTrueならOK。

結合律をテスト

map assoc_test test_triples

elem False $ map assoc_test test_triples

Falseが返ればOK。

課題

1. ex4-1.hs を読みこなす
2. unsafeCat を使わずに Maybe monad を直に使う方法に直す(Optional)