{-# LANGUAGE GADTs #-}
{-# LANGUAGE ScopedTypeVariables #-}

-- | Poly-indexed channel type.
--
-- A channel is indexed by a polynomial interface @p :: Poly@. The polynomial
-- describes both the observable position (output) and the direction space
-- (input). The channel carries no residual field; any residual policy is
-- supplied by a 'Circuit.Process.Process' at composition time.
--
-- This module starts with function-category @(->)@ evaluation. The type
-- @Channel arr p@ keeps @arr@ as a parameter so that future slices can add
-- @Kleisli@ evaluation helpers without changing the type.
module Circuit.Poly.Channel
  ( -- * Poly-indexed channel
    Channel (..),

    -- * Observation and interaction
    emitChannel,
    commitChannel,

    -- * Constructing channels
    idChannel,
    constChannel,
    mapChannel,
  )
where

import Circuit.Poly
  ( Dir,
    Eval (..),
    Mono,
    Morphism (..),
    Poly (..),
    applyLens,
    lens,
    runMorphism,
  )
import Circuit.System
  ( System,
    SystemEval (..),
    evalToSystem,
    fromEvalSystem,
    lensAsSystem,
    system,
    toEvalSystem,
  )
import Control.Category (id, (.))
import Data.Functor (void)
import Prelude hiding (id, (.))

-- $setup
-- >>> import Circuit.Poly (Mono, Morphism, lens, applyLens)
-- >>> import Circuit.System (System)

-- | A channel whose interface is the polynomial @p@.
--
-- Internally it is a Moore system with hidden state @s@. The state is
-- existentially quantified so that different channel constructors can use
-- different state types.
data Channel arr (p :: Poly) where
  Ch ::
    (SystemEval p) =>
    -- | Current state of the Moore machine.
    s ->
    -- | The system governing the channel interface.
    System arr s p ->
    Channel arr p

-- | Observe the current output of a @(->)@ channel.
--
-- The observation is an @Eval p ()@: a position together with a trivial
-- direction consumer. The position is the channel's current output; the
-- direction consumer is how a future input will advance the channel.
emitChannel :: Channel (->) p -> Eval p ()
emitChannel :: forall (p :: Poly). Channel (->) p -> Eval p ()
emitChannel (Ch s
s System (->) s p
sys) = Eval p s -> Eval p ()
forall (f :: * -> *) a. Functor f => f a -> f ()
void (System (->) s p -> s -> Eval p s
forall (p :: Poly) s.
SystemEval p =>
System (->) s p -> s -> Eval p s
toEvalSystem System (->) s p
sys s
s)

-- | Commit an input direction to a @(->)@ channel, advancing its state.
commitChannel :: Channel (->) p -> Dir p -> Channel (->) p
commitChannel :: forall (p :: Poly). Channel (->) p -> Dir p -> Channel (->) p
commitChannel (Ch s
s System (->) s p
sys) Dir p
d =
  let (Pos p
_pos, Dir p -> s
next) = Eval p s -> (Pos p, Dir p -> s)
forall x. Eval p x -> (Pos p, Dir p -> x)
forall (p :: Poly) x.
SystemEval p =>
Eval p x -> (Pos p, Dir p -> x)
evalToSystem (System (->) s p -> s -> Eval p s
forall (p :: Poly) s.
SystemEval p =>
System (->) s p -> s -> Eval p s
toEvalSystem System (->) s p
sys s
s)
   in s -> System (->) s p -> Channel (->) p
forall (p :: Poly) s (arr :: * -> * -> *).
SystemEval p =>
s -> System arr s p -> Channel arr p
Ch (Dir p -> s
next Dir p
d) System (->) s p
sys

-- | Identity channel on a monomial interface @Mono a a@.
--
-- Output is the current state; next state is the input direction.  An
-- initial state must be supplied because a Moore machine has no input
-- before the first commit.
idChannel :: a -> Channel (->) (Mono a a)
idChannel :: forall a. a -> Channel (->) (Mono a a)
idChannel a
s0 = a -> System (->) a (Mono a a) -> Channel (->) (Mono a a)
forall (p :: Poly) s (arr :: * -> * -> *).
SystemEval p =>
s -> System arr s p -> Channel arr p
Ch a
s0 (Morphism (Mono a a) (Mono a a) -> System (->) a (Mono a a)
forall s i o.
Morphism (Mono s s) (Mono i o) -> System (->) s (Mono i o)
lensAsSystem ((a -> a) -> (a -> a -> a) -> Morphism (Mono a a) (Mono a a)
forall a b db da.
(a -> b) -> (a -> db -> da) -> Morphism (Mono da a) (Mono db b)
lens a -> a
forall a. a -> a
forall {k} (cat :: k -> k -> *) (a :: k). Category cat => cat a a
id (\a
_ a
d -> a
d)))

-- | Constant-output channel on a monomial interface @Mono a b@.
--
-- Output is always @b@; the state is the constant value and is preserved
-- across commits (the input direction is ignored).
constChannel :: b -> Channel (->) (Mono a b)
constChannel :: forall b a. b -> Channel (->) (Mono a b)
constChannel b
b = b -> System (->) b (Mono a b) -> Channel (->) (Mono a b)
forall (p :: Poly) s (arr :: * -> * -> *).
SystemEval p =>
s -> System arr s p -> Channel arr p
Ch b
b (Morphism (Mono b b) (Mono a b) -> System (->) b (Mono a b)
forall s i o.
Morphism (Mono s s) (Mono i o) -> System (->) s (Mono i o)
lensAsSystem ((b -> b) -> (b -> a -> b) -> Morphism (Mono b b) (Mono a b)
forall a b db da.
(a -> b) -> (a -> db -> da) -> Morphism (Mono da a) (Mono db b)
lens (b -> b -> b
forall a b. a -> b -> a
const b
b) b -> a -> b
forall a b. a -> b -> a
const))

-- | Map a polynomial morphism over a @(->)@ channel.
--
-- The forward map transforms positions; the backward map transforms
-- directions. This is the functorial action of 'Circuit.Poly.Morphism' on
-- channels.
mapChannel ::
  (SystemEval p, SystemEval q) =>
  Morphism p q ->
  Channel (->) p ->
  Channel (->) q
mapChannel :: forall (p :: Poly) (q :: Poly).
(SystemEval p, SystemEval q) =>
Morphism p q -> Channel (->) p -> Channel (->) q
mapChannel Morphism p q
m (Ch s
s System (->) s p
sys) =
  s -> System (->) s q -> Channel (->) q
forall (p :: Poly) s (arr :: * -> * -> *).
SystemEval p =>
s -> System arr s p -> Channel arr p
Ch s
s (((s, Dir q) -> (s, Pos q)) -> System (->) s q
forall (arr :: * -> * -> *) s (p :: Poly).
arr (s, Dir p) (s, Pos p) -> System arr s p
system (s, Dir q) -> (s, Pos q)
step)
  where
    step :: (s, Dir q) -> (s, Pos q)
step (s
s', Dir q
d') =
      let tgtEval :: Eval q s
tgtEval = Morphism p q -> forall x. Eval p x -> Eval q x
forall (p :: Poly) (q :: Poly).
Morphism p q -> forall x. Eval p x -> Eval q x
runMorphism Morphism p q
m (System (->) s p -> s -> Eval p s
forall (p :: Poly) s.
SystemEval p =>
System (->) s p -> s -> Eval p s
toEvalSystem System (->) s p
sys s
s')
          (Pos q
pos, Dir q -> s
next) = Eval q s -> (Pos q, Dir q -> s)
forall x. Eval q x -> (Pos q, Dir q -> x)
forall (p :: Poly) x.
SystemEval p =>
Eval p x -> (Pos p, Dir p -> x)
evalToSystem Eval q s
tgtEval
       in (Dir q -> s
next Dir q
d', Pos q
pos)