{-# LANGUAGE CPP #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE RankNTypes #-}
#if __GLASGOW_HASKELL__ >= 702
{-# LANGUAGE Trustworthy #-}
#endif
{-# LANGUAGE TypeFamilies #-}
module Data.Semigroupoid.Categorical (
Categorical(..),
runCategorical
) where
import Control.Category (Category (id, (.)))
import Data.Semigroupoid (Semigroupoid (o))
import Prelude ()
data Categorical s a b where
Id :: Categorical s a a
Embed :: s a b -> Categorical s a b
instance (Semigroupoid s) => Semigroupoid (Categorical s) where
Categorical s j k
Id o :: Categorical s j k -> Categorical s i j -> Categorical s i k
`o` Categorical s i j
y = Categorical s i j
Categorical s i k
y
Categorical s j k
x `o` Categorical s i j
Id = Categorical s j k
Categorical s i k
x
Embed s j k
x `o` Embed s i j
y = s i k -> Categorical s i k
forall (s :: * -> * -> *) a b. s a b -> Categorical s a b
Embed (s j k
x s j k -> s i j -> s i k
forall k (c :: k -> k -> *) (j :: k) (k :: k) (i :: k).
Semigroupoid c =>
c j k -> c i j -> c i k
`o` s i j
y)
instance (Semigroupoid s) => Category (Categorical s) where
id :: Categorical s a a
id = Categorical s a a
forall (s :: * -> * -> *) a. Categorical s a a
Id
. :: Categorical s b c -> Categorical s a b -> Categorical s a c
(.) = Categorical s b c -> Categorical s a b -> Categorical s a c
forall k (c :: k -> k -> *) (j :: k) (k :: k) (i :: k).
Semigroupoid c =>
c j k -> c i j -> c i k
o
runCategorical :: (a ~ b => r) -> (s a b -> r) -> Categorical s a b -> r
runCategorical :: ((a ~ b) => r) -> (s a b -> r) -> Categorical s a b -> r
runCategorical (a ~ b) => r
r s a b -> r
_ Categorical s a b
Id = r
(a ~ b) => r
r
runCategorical (a ~ b) => r
_ s a b -> r
f (Embed s a b
x) = s a b -> r
f s a b
x