{-# LANGUAGE InstanceSigs #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeAbstractions #-}
{-# LANGUAGE TypeFamilies #-}
{-# OPTIONS_GHC -Wno-orphans #-}

-- | Layer instance for 'FreeAgent': unit / run / bind into any category.
--
-- Mirrors 'Circuit.Free' so free agent terms obey the same β/η laws as the
-- circuits free-category layer.
module Free.Agent.Layer
  ( runFreeAgent,
    bindFreeAgent,
  )
where

import Circuit.Category (Category (..))
import Circuit.Layer (Layer (..), (:~>))
import Data.Kind (Type)
import Free.Agent.Syntax (FreeAgent (..))
import Prelude hiding (id, (.))

-- $setup
-- >>> import Free.Agent.Syntax
-- >>> import Free.Agent.Layer
-- >>> import Prelude hiding (id, (.))

-- | 'FreeAgent' is a free category, so it is a 'Layer' over any base arrow.
-- 'runFreeAgent' and 'bindFreeAgent' are the two folds.
instance Layer FreeAgent where
  type Law FreeAgent arr' = Category arr'
  type Run FreeAgent arr = Category arr
  type Bind FreeAgent arr = ()
  unit :: forall (arr :: * -> * -> *). Category arr => arr :~> FreeAgent arr
unit = arr x y -> FreeAgent arr x y
forall {k} (arr :: k -> k -> *) (a :: k) (b :: k).
arr a b -> FreeAgent arr a b
Lift
  bind ::
    forall arr' arr a b.
    (Law FreeAgent arr') =>
    (arr :~> arr') ->
    FreeAgent arr a b ->
    arr' a b
  bind :: forall (arr' :: * -> * -> *) (arr :: * -> * -> *) a b.
Law FreeAgent arr' =>
(arr :~> arr') -> FreeAgent arr a b -> arr' a b
bind arr :~> arr'
h (Lift arr a b
f) = arr a b -> arr' a b
arr :~> arr'
h arr a b
f
  bind arr :~> arr'
h (Compose @_ @_ FreeAgent arr b1 b
g FreeAgent arr a b1
f) = (arr :~> arr') -> FreeAgent arr b1 b -> arr' b1 b
forall (arr' :: * -> * -> *) (arr :: * -> * -> *) a b.
(Law FreeAgent arr', Bind FreeAgent arr) =>
(arr :~> arr') -> FreeAgent arr a b -> arr' a b
forall (f :: (* -> * -> *) -> * -> * -> *) (arr' :: * -> * -> *)
       (arr :: * -> * -> *) a b.
(Layer f, Law f arr', Bind f arr) =>
(arr :~> arr') -> f arr a b -> arr' a b
bind arr x y -> arr' x y
arr :~> arr'
h FreeAgent arr b1 b
g arr' b1 b -> arr' a b1 -> arr' a b
forall b c a. 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 :~> arr') -> FreeAgent arr a b1 -> arr' a b1
forall (arr' :: * -> * -> *) (arr :: * -> * -> *) a b.
(Law FreeAgent arr', Bind FreeAgent arr) =>
(arr :~> arr') -> FreeAgent arr a b -> arr' a b
forall (f :: (* -> * -> *) -> * -> * -> *) (arr' :: * -> * -> *)
       (arr :: * -> * -> *) a b.
(Layer f, Law f arr', Bind f arr) =>
(arr :~> arr') -> f arr a b -> arr' a b
bind arr x y -> arr' x y
arr :~> arr'
h FreeAgent arr a b1
f

-- | Fold a free agent term back into its base category.
runFreeAgent ::
  forall (arr :: Type -> Type -> Type) a b.
  (Category arr) =>
  FreeAgent arr a b ->
  arr a b
runFreeAgent :: forall (arr :: * -> * -> *) a b.
Category arr =>
FreeAgent arr a b -> arr a b
runFreeAgent (Lift arr a b
f) = arr a b
f
runFreeAgent (Compose FreeAgent arr b1 b
g FreeAgent arr a b1
f) = FreeAgent arr b1 b -> arr b1 b
forall (arr :: * -> * -> *) a b.
Category arr =>
FreeAgent arr a b -> arr a b
runFreeAgent FreeAgent arr b1 b
g arr b1 b -> arr a b1 -> arr a b
forall b c a. 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
. FreeAgent arr a b1 -> arr a b1
forall (arr :: * -> * -> *) a b.
Category arr =>
FreeAgent arr a b -> arr a b
runFreeAgent FreeAgent arr a b1
f

-- | Fold a free agent term into any target category.
bindFreeAgent ::
  forall (arr' :: Type -> Type -> Type) (arr :: Type -> Type -> Type) a b.
  (Category arr') =>
  (arr :~> arr') ->
  FreeAgent arr a b ->
  arr' a b
bindFreeAgent :: forall (arr' :: * -> * -> *) (arr :: * -> * -> *) a b.
Category arr' =>
(arr :~> arr') -> FreeAgent arr a b -> arr' a b
bindFreeAgent = (arr :~> arr') -> FreeAgent arr a b -> arr' a b
forall (arr' :: * -> * -> *) (arr :: * -> * -> *) a b.
(Law FreeAgent arr', Bind FreeAgent arr) =>
(arr :~> arr') -> FreeAgent arr a b -> arr' a b
forall (f :: (* -> * -> *) -> * -> * -> *) (arr' :: * -> * -> *)
       (arr :: * -> * -> *) a b.
(Layer f, Law f arr', Bind f arr) =>
(arr :~> arr') -> f arr a b -> arr' a b
bind