{-# LANGUAGE Trustworthy #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE NoImplicitPrelude #-}
{-# LANGUAGE PolyKinds #-}
{-# OPTIONS_GHC -Wno-inline-rule-shadowing #-}
module Control.Category where
import qualified GHC.Base (id,(.))
import Data.Type.Coercion
import Data.Type.Equality
import GHC.Prim (coerce)
infixr 9 .
infixr 1 >>>, <<<
class Category cat where
id :: cat a a
(.) :: cat b c -> cat a b -> cat a c
{-# RULES
"identity/left" forall p .
id . p = p
"identity/right" forall p .
p . id = p
"association" forall p q r .
(p . q) . r = p . (q . r)
#-}
instance Category (->) where
id :: a -> a
id = a -> a
forall a. a -> a
GHC.Base.id
. :: (b -> c) -> (a -> b) -> a -> c
(.) = (b -> c) -> (a -> b) -> a -> c
forall b c a. (b -> c) -> (a -> b) -> a -> c
(GHC.Base..)
instance Category (:~:) where
id :: a :~: a
id = a :~: a
forall k (a :: k). a :~: a
Refl
Refl . :: (b :~: c) -> (a :~: b) -> a :~: c
. Refl = a :~: c
forall k (a :: k). a :~: a
Refl
instance Category (:~~:) where
id :: a :~~: a
id = a :~~: a
forall k (a :: k). a :~~: a
HRefl
HRefl . :: (b :~~: c) -> (a :~~: b) -> a :~~: c
. HRefl = a :~~: c
forall k (a :: k). a :~~: a
HRefl
instance Category Coercion where
id :: Coercion a a
id = Coercion a a
forall k (a :: k) (b :: k). Coercible a b => Coercion a b
Coercion
. :: Coercion b c -> Coercion a b -> Coercion a c
(.) Coercion = Coercion a b -> Coercion a c
forall a b. Coercible a b => a -> b
coerce
(<<<) :: Category cat => cat b c -> cat a b -> cat a c
<<< :: cat b c -> cat a b -> cat a c
(<<<) = cat b c -> cat a b -> cat a c
forall k (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
(.)
(>>>) :: Category cat => cat a b -> cat b c -> cat a c
f :: cat a b
f >>> :: cat a b -> cat b c -> cat a c
>>> g :: cat b c
g = cat b c
g cat b c -> cat a b -> cat a c
forall k (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. cat a b
f