{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}

-- | Local category hierarchy without object constraints.
--
-- 'Category' is local so morphisms can carry an associated object
-- constraint.  This version removes the constraint-family apparatus:
-- objects are unconstrained at the type level and legitimacy is an
-- audit concern rather than a discharge concern.
--
-- == Operator convention
--
-- The tip of the operator points in the direction of data flow.
--
-- * @|@ means /apply/ to a value: @('|>')@ feeds a value into a function
--   (forward application, like @&@), and @('<|')@ applies a function
--   to a value (backward application, like @'$'@).
-- * @.@ means /compose/ morphisms: @('.>')@ is forward composition and
--   @('.')@ is backward composition as usual.
module Circuit.Category
  ( Category (..),
    (.>),
    (|>),
    (<|),
    K (..),
    FunctionLike (..),
    Pointed (..),
  )
where

import Control.Monad ((<=<))
import Data.Kind (Type)
import Prelude hiding (id, (.))

-- | A category without object constraints.
--
-- @Ob arr a@ is gone; every object is mentionable.  Lawfulness is
-- checked by the axioma oracles rather than by type-level discharge.
class Category (arr :: k -> k -> Type) where
  -- | Identity morphism.
  id :: arr a a

  -- | Composition (right-to-left).
  (.) :: arr b c -> arr a b -> arr a c

-- | Forward composition. @f .> g = g . f@
(.>) :: (Category arr) => arr a b -> arr b c -> arr a c
arr a b
f .> :: forall {k} (arr :: k -> k -> *) (a :: k) (b :: k) (c :: k).
Category arr =>
arr a b -> arr b c -> arr a c
.> arr b c
g = arr b c
g arr b c -> arr a b -> arr a c
forall (b :: k) (c :: k) (a :: k). arr b c -> arr a b -> arr a c
forall k (arr :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category arr =>
arr b c -> arr a b -> arr a c
. arr a b
f
{-# INLINE (.>) #-}

-- | Forward application. @x |> f = f x@
(|>) :: a -> (a -> b) -> b
a
x |> :: forall a b. a -> (a -> b) -> b
|> a -> b
f = a -> b
f a
x
{-# INLINE (|>) #-}

infixl 1 |>

-- | Backward application. @f <| x = f x@
(<|) :: (a -> b) -> a -> b
a -> b
f <| :: forall a b. (a -> b) -> a -> b
<| a
x = a -> b
f a
x
{-# INLINE (<|) #-}

infixr 0 <|

-- | Unconstrained function category.
instance Category (->) where
  id :: forall a. a -> a
id a
x = a
x
  (b -> c
f . :: forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> b
g) a
x = b -> c
f (a -> b
g a
x)

-- | Kleisli arrows of a monad, named locally.
newtype K m a b = K {forall {k} (m :: k -> *) a (b :: k). K m a b -> a -> m b
runK :: a -> m b}

instance (Monad m) => Category (K m) where
  id :: forall a. K m a a
id = (a -> m a) -> K m a a
forall {k} (m :: k -> *) a (b :: k). (a -> m b) -> K m a b
K a -> m a
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure
  K b -> m c
f . :: forall b c a. K m b c -> K m a b -> K m a c
. K a -> m b
g = (a -> m c) -> K m a c
forall {k} (m :: k -> *) a (b :: k). (a -> m b) -> K m a b
K (b -> m c
f (b -> m c) -> (a -> m b) -> a -> m c
forall (m :: * -> *) b c a.
Monad m =>
(b -> m c) -> (a -> m b) -> a -> m c
<=< a -> m b
g)

-- | Categories that can embed pure functions as morphisms.
--
-- This is the canonical functor from the function category @(->)@ into
-- @arr@. It is useful for lifting decision procedures (e.g. bias in a
-- race) into arrows such as Kleisli categories.
class (Category arr) => FunctionLike arr where
  -- | Lift a pure function into the arrow.
  function :: (a -> b) -> arr a b

-- | Functions embed as themselves.
instance FunctionLike (->) where
  function :: forall a b. (a -> b) -> a -> b
function = (a -> b) -> a -> b
forall a. a -> a
forall k (arr :: k -> k -> *) (a :: k). Category arr => arr a a
id
  {-# INLINE function #-}

-- | Kleisli arrows embed pure functions by returning the result in the
-- monad.
instance (Monad m) => FunctionLike (K m) where
  function :: forall a b. (a -> b) -> K m a b
function a -> b
f = (a -> m b) -> K m a b
forall {k} (m :: k -> *) a (b :: k). (a -> m b) -> K m a b
K (b -> m b
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (b -> m b) -> (a -> b) -> a -> m b
forall b c a. (b -> c) -> (a -> b) -> a -> c
forall k (arr :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category arr =>
arr b c -> arr a b -> arr a c
. a -> b
f)

-- | A pointed object: an object with a distinguished element.
--
-- This class has no laws by construction — it merely names a chosen
-- element.  It is the structural requirement for the coproduct-unit poles
-- of 'Body Either': on a payload input the companion must produce a carrier
-- value, and there is no ambient state to use.  'Monoid' is over-strong for
-- this purpose, since only the identity element is needed.
class Pointed a where
  point :: a

-- | The singleton type is canonically pointed.
instance Pointed () where
  point :: ()
point = ()
  {-# INLINE point #-}

-- | 'Maybe' is canonically pointed at 'Nothing'.
instance Pointed (Maybe a) where
  point :: Maybe a
point = Maybe a
forall a. Maybe a
Nothing
  {-# INLINE point #-}

-- | Lists are canonically pointed at the empty list.
instance Pointed [a] where
  point :: [a]
point = []
  {-# INLINE point #-}