{-# LANGUAGE TypeFamilies, GADTs, RankNTypes, PolyKinds, NoImplicitPrelude #-}
-----------------------------------------------------------------------------
-- |
-- Module      :  Data.Category
-- License     :  BSD-style (see the file LICENSE)
--
-- Maintainer  :  sjoerd@w3future.com
-- Stability   :  experimental
-- Portability :  non-portable
-----------------------------------------------------------------------------
module Data.Category (

  -- * Category
    Category(..)
  , Obj
  , Kind

  -- * Opposite category
  , Op(..)

) where

infixr 8 .


-- | Whenever objects are required at value level, they are represented by their identity arrows.
type Obj k a = k a a

-- | An instance of @Category k@ declares the arrow @k@ as a 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


-- | The category with Haskell types as objects and Haskell functions as arrows.
instance Category (->) where

  src :: (a -> b) -> Obj (->) a
src a -> b
_ = \a
x -> a
x
  tgt :: (a -> b) -> Obj (->) b
tgt a -> b
_ = \b
x -> b
x

  b -> c
f . :: (b -> c) -> (a -> b) -> a -> c
. a -> b
g = \a
x -> b -> c
f (a -> b
g a
x)


newtype Op k a b = Op { Op k a b -> k b a
unOp :: k b a }

-- | @Op k@ is opposite category of the category @k@.
instance Category k => Category (Op k) where

  src :: Op k a b -> Obj (Op k) a
src (Op k b a
a)      = k a a -> Obj (Op k) a
forall k k (k :: k -> k -> *) (a :: k) (b :: k). k b a -> Op k a b
Op (k b a -> k a a
forall k (k :: k -> k -> *) (a :: k) (b :: k).
Category k =>
k a b -> Obj k b
tgt k b a
a)
  tgt :: Op k a b -> Obj (Op k) b
tgt (Op k b a
a)      = k b b -> Obj (Op k) b
forall k k (k :: k -> k -> *) (a :: k) (b :: k). k b a -> Op k a b
Op (k b a -> k b b
forall k (k :: k -> k -> *) (a :: k) (b :: k).
Category k =>
k a b -> Obj k a
src k b a
a)

  (Op k c b
a) . :: Op k b c -> Op k a b -> Op k a c
. (Op k b a
b) = k c a -> Op k a c
forall k k (k :: k -> k -> *) (a :: k) (b :: k). k b a -> Op k a b
Op (k b a
b k b a -> k c b -> k c a
forall k (k :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category k =>
k b c -> k a b -> k a c
. k c b
a)

type Kind (cat :: k -> k -> *) = k