Category.hs

{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE TypeInType #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE QuantifiedConstraints #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE ExistentialQuantification #-}
{-# LANGUAGE NoImplicitPrelude #-}
{-# LANGUAGE ScopedTypeVariables #-}

module SubHask.Category
  (
  ) where

import Data.Kind (Type, Constraint)
import qualified Prelude as Prelude

class Category (cat :: k -> k -> Type) where
  type V cat (a :: k) :: Constraint
  id :: V cat a => cat a a

  infixr 9 .
  (.) :: cat b c -> cat a b -> cat a c

(>>>) :: Category cat => cat a b -> cat b c -> cat a c
a >>> b = b . a

(<<<) :: Category cat => cat b c -> cat a b -> cat a c
a <<< b = a . b

type Hask = (->)

instance Category (->) where
  type V (->) (a :: Type) = ()
  id = Prelude.id

  (.) = (Prelude..)

data CatT
  (cat  :: Type -> Type -> Type)
  (cat1 :: Type -> Type -> Type)
  (cat2 :: Type -> Type -> Type)
  = forall a b.
      ( V cat1 a
      , V cat2 a
      , V cat1 b
      , V cat2 b
      ) => CatT (cat1 a b `cat` cat2 a b)

instance Category cat => Category (CatT cat) where
  type V (CatT cat) cat1 = forall a b. (V cat1 a, V cat1 b, V cat (cat1 a b) )