{-# LANGUAGE GADTs #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeAbstractions #-}
{-# LANGUAGE TypeFamilies #-}

-- | Free category over a base arrow, named for the agent seat.
--
-- Same shape as 'Circuit.Free.Free': 'Lift' embeds a base arrow, 'Compose'
-- sequences free morphisms. Package role ABOVE circuits-agent — reify seats
-- and pipelines here, then fold into 'Circuit.Agent.Agent' or 'Circuit.Agent.Shard'.
module Free.Agent.Syntax
  ( FreeAgent (..),
  )
where

import Circuit.Category (Category (..))
import Prelude hiding (id, (.))

-- | Free category over a base arrow @arr@.
--
-- * 'Lift' — embed a base arrow.
-- * 'Compose' — sequential composition (right-to-left as in 'Category').
data FreeAgent arr a b where
  -- | Embed a base arrow as a single generator.
  Lift :: arr a b -> FreeAgent arr a b
  -- | Sequence two free morphisms (right-to-left, matching 'Category' composition).
  Compose :: FreeAgent arr b c -> FreeAgent arr a b -> FreeAgent arr a c

instance (Category arr) => Category (FreeAgent arr) where
  id :: forall (a :: k). FreeAgent arr a a
id = arr a a -> FreeAgent arr a a
forall {k} (arr :: k -> k -> *) (a :: k) (b :: k).
arr a b -> FreeAgent arr a b
Lift arr a a
forall (a :: k). arr a a
forall k (arr :: k -> k -> *) (a :: k). Category arr => arr a a
id
  . :: forall (b :: k) (c :: k) (a :: k).
FreeAgent arr b c -> FreeAgent arr a b -> FreeAgent arr a c
(.) = FreeAgent arr b c -> FreeAgent arr a b -> FreeAgent arr a c
forall {k} (arr :: k -> k -> *) (b :: k) (c :: k) (a :: k).
FreeAgent arr b c -> FreeAgent arr a b -> FreeAgent arr a c
Compose