data-category-0.2.0: Data/Category.hs

{-# LANGUAGE TypeOperators, TypeFamilies, GADTs, RankNTypes #-}
-----------------------------------------------------------------------------
-- |
-- Module      :  Data.Category
-- Copyright   :  (c) Sjoerd Visscher 2010
-- License     :  BSD-style (see the file LICENSE)
--
-- Maintainer  :  sjoerd@w3future.com
-- Stability   :  experimental
-- Portability :  non-portable
-----------------------------------------------------------------------------
module Data.Category (
  
  -- * Category
    Category(..)
  , Obj(..)
  
  -- * Opposite category
  , Op(..)
    
) where

import Prelude (($))
import qualified Prelude


-- | An instance of @Category (~>)@ declares the arrow @(~>)@ as a category.
class Category (~>) where
  
  data Obj (~>) :: * -> *

  src :: a ~> b -> Obj (~>) a
  tgt :: a ~> b -> Obj (~>) b

  id  :: Obj (~>) a -> a ~> a
  (.) :: b ~> c -> a ~> b -> a ~> c


-- | The category with Haskell types as objects and Haskell functions as arrows.
instance Category (->) where
  
  data Obj (->) a = HaskO
  
  src _ = HaskO
  tgt _ = HaskO
  
  id _  = Prelude.id  
  (.)   = (Prelude..)    


data Op :: (* -> * -> *) -> * -> * -> * where
  Op :: (a ~> b) -> Op (~>) b a

-- | @Op (~>)@ is opposite category of the category @(~>)@.
instance Category (~>) => Category (Op (~>)) where
  
  data Obj (Op (~>)) a = OpObj (Obj (~>) a)
  
  src (Op a)      = OpObj $ tgt a
  tgt (Op a)      = OpObj $ src a
  
  id (OpObj x)    = Op $ id x
  (Op a) . (Op b) = Op $ b . a