{-# LANGUAGE CPP #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE Trustworthy #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}

-----------------------------------------------------------------------------
-- |
-- Copyright   :  (C) 2021 Koz Ross
-- License     :  BSD-style (see the file LICENSE)
--
-- Maintainer  :  Koz Ross <koz.ross@retro-freedom.nz>
-- Stability   :  Experimental
-- Portability :  GHC only
--
-- Provides a way to attach an identity to any semigroupoid.
----------------------------------------------------------------------------
module Data.Semigroupoid.Categorical (
  Categorical(..),
  runCategorical
  ) where

import Control.Category (Category (id, (.)))
import Data.Semigroupoid (Semigroupoid (o))
#if __GLASGOW_HASKELL__ >= 904
import Data.Type.Equality (type (~))
#endif
import Prelude ()

-- | Attaches an identity.
--
-- @since 5.3.6
data Categorical s a b where
  Id :: Categorical s a a
  Embed :: s a b -> Categorical s a b

-- | @since 5.3.6
instance (Semigroupoid s) => Semigroupoid (Categorical s) where
  Categorical s j k1
Id o :: forall j k1 i.
Categorical s j k1 -> Categorical s i j -> Categorical s i k1
`o` Categorical s i j
y = Categorical s i j
Categorical s i k1
y
  Categorical s j k1
x `o` Categorical s i j
Id = Categorical s j k1
Categorical s i k1
x
  Embed s j k1
x `o` Embed s i j
y = s i k1 -> Categorical s i k1
forall (s :: * -> * -> *) a b. s a b -> Categorical s a b
Embed (s j k1
x s j k1 -> s i j -> s i k1
forall j k1 i. s j k1 -> s i j -> s i k1
forall {k} (c :: k -> k -> *) (j :: k) (k1 :: k) (i :: k).
Semigroupoid c =>
c j k1 -> c i j -> c i k1
`o` s i j
y)

-- | @since 5.3.6
instance (Semigroupoid s) => Category (Categorical s) where
  id :: forall a. Categorical s a a
id = Categorical s a a
forall (s :: * -> * -> *) a. Categorical s a a
Id
  . :: forall b c a.
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 b c a.
Categorical s b c -> Categorical s a b -> Categorical s a c
forall {k} (c :: k -> k -> *) (j :: k) (k1 :: k) (i :: k).
Semigroupoid c =>
c j k1 -> c i j -> c i k1
o

-- | @since 5.3.6
runCategorical :: (a ~ b => r) -> (s a b -> r) -> Categorical s a b -> r
runCategorical :: forall a b r (s :: * -> * -> *).
((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