{-# LANGUAGE TypeFamilies, GADTs, RankNTypes, PolyKinds, LinearTypes, FlexibleInstances, 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(..)

  -- * `(->)`/Hask
  , obj

) where

import GHC.Exts
import Data.Kind (Type)

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


obj :: Obj (FUN m) a
obj :: forall (m :: Multiplicity) a. Obj (FUN m) a
obj a
x = a
x

-- | For @m ~ Many@: The category with Haskell types as objects and Haskell functions as arrows, i.e. @(->)@.
-- For @m ~ One@: The category with Haskell types as objects and Haskell linear functions as arrows, i.e. @(%1->)@.
instance Category (FUN m) where

  src :: forall a b. (a %m -> b) -> Obj (FUN m) a
src a %m -> b
_ = forall (m :: Multiplicity) a. Obj (FUN m) a
obj
  tgt :: forall a b. (a %m -> b) -> Obj (FUN m) b
tgt a %m -> b
_ = forall (m :: Multiplicity) a. Obj (FUN m) a
obj

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


newtype Op k a b = Op { forall {k} {k} (k :: k -> k -> *) (a :: k) (b :: k).
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 :: forall (a :: k) (b :: k). Op k a b -> Obj (Op k) a
src (Op k b a
a)      = forall {k} {k} (k :: k -> k -> *) (a :: k) (b :: k).
k b a -> Op k a b
Op (forall {k} (k :: k -> k -> *) (a :: k) (b :: k).
Category k =>
k a b -> Obj k b
tgt k b a
a)
  tgt :: forall (a :: k) (b :: k). Op k a b -> Obj (Op k) b
tgt (Op k b a
a)      = forall {k} {k} (k :: k -> k -> *) (a :: k) (b :: k).
k b a -> Op k a b
Op (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) . :: forall (b :: k) (c :: k) (a :: k). Op k b c -> Op k a b -> Op k a c
. (Op k b a
b) = forall {k} {k} (k :: k -> k -> *) (a :: k) (b :: k).
k b a -> Op k a b
Op (k b a
b 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)


-- | @Kind k@ is the kind of the objects of the category @k@.
type family Kind (k :: o -> o -> Type) :: Type where
  Kind (k :: o -> o -> Type) = o