(original) (raw)

{-# 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 Data.Coerce (coerce)

infixr 9 . infixr 1 >>>, <<<

class Category cat where

[id](Control.Category.html#id) :: [cat](#local-6989586621679608305) [a](#local-6989586621679608311) [a](#local-6989586621679608311)


[(.)](Control.Category.html#.) :: [cat](#local-6989586621679608305) [b](#local-6989586621679608310) [c](#local-6989586621679608309) -> [cat](#local-6989586621679608305) [a](#local-6989586621679608308) [b](#local-6989586621679608310) -> [cat](#local-6989586621679608305) [a](#local-6989586621679608308) [c](#local-6989586621679608309)

{-# 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 :: forall a. a -> a id = a -> a forall a. a -> a GHC.Base.id . :: forall b c a. (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 :: forall (a :: k). a :: a id = a :: a forall k (a :: k). a :: a Refl b :: c Refl . :: forall (b :: k) (c :: k) (a :: k). (b :: c) -> (a :: b) -> a :: c . a :: b Refl = a :: c forall k (a :: k). a :: a Refl

instance Category (:~~:) where id :: forall (a :: k). a :: a id = a :: a forall k (a :: k). a :: a HRefl b :: c HRefl . :: forall (b :: k) (c :: k) (a :: k). (b :: c) -> (a :: b) -> a :: c . a :: b HRefl = a :: c forall k (a :: k). a :: a HRefl

instance Category Coercion where id :: forall (a :: k). Coercion a a id = Coercion a a forall {k} (a :: k) (b :: k). Coercible a b => Coercion a b Coercion . :: forall (b :: k) (c :: k) (a :: k). Coercion b c -> Coercion a b -> Coercion a c (.) Coercion b c Coercion = Coercion a b -> Coercion a c coerce

(<<<) :: Category cat => 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 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 cat a b f >>> :: forall {k} (cat :: k -> k -> *) (a :: k) (b :: k) (c :: k). Category cat => cat a b -> cat b c -> cat a c >>> 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 {-# INLINE (>>>) #-}