{-# LANGUAGE PatternSynonyms #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeFamilies #-}
{-# OPTIONS_GHC -Wno-pattern-namespace-specifier #-}

-- | Hyperfunctions: the final encoding of traced monoidal categories.
--
-- A @Hyper@ is completely determined by its dual. To get a @b@ you must
-- provide a continuation that can itself produce an @a@.
--
-- @Hyper@ is the function-category specialisation:
--
-- @
-- type Hyper = HyperA (->)
-- @
--
-- The two named targets are:
--
-- * @Hyper@ — arrows are plain functions and knots tie by Haskell laziness.
-- * @'HyperA' ('K' m)@ — arrows are Kleisli arrows and knots tie with 'mfix'.
--
-- They share the same newtype, but the constructors and eliminators are
-- specialised because the two bases have different notions of observation and
-- fixed point.
--
-- === doctests
--
-- >>> import Circuit.Hyper
-- >>> import Circuit.Channel (trace)
-- >>> import Circuit.Category (K (..))
-- >>> import Data.Functor.Identity (Identity (..))
--
-- >>> let body = liftK (K (\(xs, ()) -> Identity (0 : xs, take 3 xs)) :: K Identity ([Int], ()) ([Int], [Int]))
-- >>> runIdentity (observeK (trace body) ())
-- [0,0,0]
module Circuit.Hyper
  ( -- * Parameterised hyperfunctions
    HyperA (..),
    Hyper,
    pattern Hyper,

    -- * Function-category hyperfunctions
    lift,
    observe,
    base,
    push,
    runHyper,

    -- * Kleisli hyperfunctions
    liftK,
    observeK,
    baseK,
    pushK,
    runHyperK,

    -- * Either-loop state machine
    encodeEither,
    runEither,

    -- * Bridges from initial syntax
    encode,
    encodeK,
  )
where

import Circuit.Category (Category (..), K (..), (.>))
import Circuit.Channel (Channel (..), Strength (..), Traced (..))
import Circuit.Syntax (SigCompose (..), (:+:) (..))
import Circuit.Syntax qualified as Syn
import Circuit.Trace (SigYank (..), Trace)
import Control.Monad.Fix (MonadFix, mfix)
import Data.Functor.Identity (Identity (..))
import Prelude hiding (id, (.))

-- $setup
-- >>> import Prelude
-- >>> import Circuit.Hyper (observe, lift, runHyper, Hyper (..))
-- >>> let h = lift (+1) :: Hyper Int Int

-- * Hyperfunctions

-- | A hyperfunction from @a@ to @b@ over the base category @arr@.
newtype HyperA arr a b = HyperA
  { -- | Feed a continuation into the hyperfunction.
    forall {k} (arr :: * -> k -> *) (a :: k) (b :: k).
HyperA arr a b -> arr (HyperA arr b a) b
invoke :: arr (HyperA arr b a) b
  }

-- | The function-category hyperfunction.
type Hyper = HyperA (->)

-- | Bidirectional pattern for the function-category hyperfunction.
pattern Hyper :: (HyperA (->) b a -> b) -> Hyper a b
pattern $bHyper :: forall b a. (HyperA (->) b a -> b) -> Hyper a b
$mHyper :: forall {r} {b} {a}.
Hyper a b -> ((HyperA (->) b a -> b) -> r) -> ((# #) -> r) -> r
Hyper f = HyperA f

{-# COMPLETE Hyper :: Hyper #-}

-- * Function-category hyperfunctions

-- | Embed a plain function into a hyperfunction.
--
-- >>> observe (lift (+1)) 5
-- 6
lift :: (a -> b) -> Hyper a b
lift :: forall a b. (a -> b) -> Hyper a b
lift a -> b
f = (a -> b) -> Hyper a b -> Hyper a b
forall a b. (a -> b) -> Hyper a b -> Hyper a b
push a -> b
f ((a -> b) -> Hyper a b
forall a b. (a -> b) -> Hyper a b
lift a -> b
f)

-- | Extract a plain function from a hyperfunction.
--
-- >>> observe (lift reverse) "hello"
-- "olleh"
observe :: Hyper a b -> (a -> b)
observe :: forall a b. Hyper a b -> a -> b
observe Hyper a b
h a
a = Hyper a b -> HyperA (->) b a -> b
forall {k} (arr :: * -> k -> *) (a :: k) (b :: k).
HyperA arr a b -> arr (HyperA arr b a) b
invoke Hyper a b
h (a -> HyperA (->) b a
forall a b. a -> Hyper b a
base a
a)

-- | Ignores the input and returns a constant value.
--
-- >>> observe (base 42) undefined
-- 42
base :: a -> Hyper b a
base :: forall a b. a -> Hyper b a
base a
b = (HyperA (->) a b -> a) -> HyperA (->) b a
forall {k} (arr :: * -> k -> *) (a :: k) (b :: k).
arr (HyperA arr b a) b -> HyperA arr a b
HyperA ((HyperA (->) a b -> a) -> HyperA (->) b a)
-> (HyperA (->) a b -> a) -> HyperA (->) b a
forall a b. (a -> b) -> a -> b
$ \HyperA (->) a b
_ -> a
b

-- | Push a plain function onto a hyperfunction.
--
-- >>> observe (push (+1) (lift (*2))) 5
-- 6
push :: (a -> b) -> Hyper a b -> Hyper a b
push :: forall a b. (a -> b) -> Hyper a b -> Hyper a b
push a -> b
f Hyper a b
h = (HyperA (->) b a -> b) -> Hyper a b
forall {k} (arr :: * -> k -> *) (a :: k) (b :: k).
arr (HyperA arr b a) b -> HyperA arr a b
HyperA ((HyperA (->) b a -> b) -> Hyper a b)
-> (HyperA (->) b a -> b) -> Hyper a b
forall a b. (a -> b) -> a -> b
$ \HyperA (->) b a
k -> a -> b
f (HyperA (->) b a -> Hyper a b -> a
forall {k} (arr :: * -> k -> *) (a :: k) (b :: k).
HyperA arr a b -> arr (HyperA arr b a) b
invoke HyperA (->) b a
k Hyper a b
h)

-- | Close the self-referential loop.
--
-- >>> runHyper (Hyper $ \_ -> 42 :: Int)
-- 42
runHyper :: Hyper a a -> a
runHyper :: forall a. Hyper a a -> a
runHyper Hyper a a
h = let a :: a
a = Hyper a a -> Hyper a a -> a
forall {k} (arr :: * -> k -> *) (a :: k) (b :: k).
HyperA arr a b -> arr (HyperA arr b a) b
invoke Hyper a a
h (a -> Hyper a a
forall a b. a -> Hyper b a
base a
a) in a
a

-- * Kleisli hyperfunctions

-- | Embed a Kleisli arrow into a hyperfunction.
liftK :: (Monad m) => K m a b -> HyperA (K m) a b
liftK :: forall (m :: * -> *) a b. Monad m => K m a b -> HyperA (K m) a b
liftK K m a b
f = K m a b -> HyperA (K m) a b -> HyperA (K m) a b
forall (m :: * -> *) a b.
Monad m =>
K m a b -> HyperA (K m) a b -> HyperA (K m) a b
pushK K m a b
f (K m a b -> HyperA (K m) a b
forall (m :: * -> *) a b. Monad m => K m a b -> HyperA (K m) a b
liftK K m a b
f)

-- | Extract the underlying Kleisli arrow from a hyperfunction.
observeK :: (Monad m) => HyperA (K m) a b -> a -> m b
observeK :: forall (m :: * -> *) a b. Monad m => HyperA (K m) a b -> a -> m b
observeK HyperA (K m) a b
h a
a = K m (HyperA (K m) b a) b -> HyperA (K m) b a -> m b
forall {k} (m :: k -> *) a (b :: k). K m a b -> a -> m b
runK (HyperA (K m) a b -> K m (HyperA (K m) b a) b
forall {k} (arr :: * -> k -> *) (a :: k) (b :: k).
HyperA arr a b -> arr (HyperA arr b a) b
invoke HyperA (K m) a b
h) (a -> HyperA (K m) b a
forall (m :: * -> *) b a. Monad m => b -> HyperA (K m) a b
baseK a
a)

-- | A constant Kleisli hyperfunction.
baseK :: (Monad m) => b -> HyperA (K m) a b
baseK :: forall (m :: * -> *) b a. Monad m => b -> HyperA (K m) a b
baseK b
b = K m (HyperA (K m) b a) b -> HyperA (K m) a b
forall {k} (arr :: * -> k -> *) (a :: k) (b :: k).
arr (HyperA arr b a) b -> HyperA arr a b
HyperA (K m (HyperA (K m) b a) b -> HyperA (K m) a b)
-> K m (HyperA (K m) b a) b -> HyperA (K m) a b
forall a b. (a -> b) -> a -> b
$ (HyperA (K m) b a -> m b) -> K m (HyperA (K m) b a) b
forall {k} (m :: k -> *) a (b :: k). (a -> m b) -> K m a b
K ((HyperA (K m) b a -> m b) -> K m (HyperA (K m) b a) b)
-> (HyperA (K m) b a -> m b) -> K m (HyperA (K m) b a) b
forall a b. (a -> b) -> a -> b
$ \HyperA (K m) b a
_ -> b -> m b
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure b
b

-- | Push a Kleisli arrow onto a hyperfunction.
pushK :: (Monad m) => K m a b -> HyperA (K m) a b -> HyperA (K m) a b
pushK :: forall (m :: * -> *) a b.
Monad m =>
K m a b -> HyperA (K m) a b -> HyperA (K m) a b
pushK K m a b
f HyperA (K m) a b
h = K m (HyperA (K m) b a) b -> HyperA (K m) a b
forall {k} (arr :: * -> k -> *) (a :: k) (b :: k).
arr (HyperA arr b a) b -> HyperA arr a b
HyperA (K m (HyperA (K m) b a) b -> HyperA (K m) a b)
-> K m (HyperA (K m) b a) b -> HyperA (K m) a b
forall a b. (a -> b) -> a -> b
$ (HyperA (K m) b a -> m b) -> K m (HyperA (K m) b a) b
forall {k} (m :: k -> *) a (b :: k). (a -> m b) -> K m a b
K ((HyperA (K m) b a -> m b) -> K m (HyperA (K m) b a) b)
-> (HyperA (K m) b a -> m b) -> K m (HyperA (K m) b a) b
forall a b. (a -> b) -> a -> b
$ \HyperA (K m) b a
k -> do
  a_val <- K m (HyperA (K m) a b) a -> HyperA (K m) a b -> m a
forall {k} (m :: k -> *) a (b :: k). K m a b -> a -> m b
runK (HyperA (K m) b a -> K m (HyperA (K m) a b) a
forall {k} (arr :: * -> k -> *) (a :: k) (b :: k).
HyperA arr a b -> arr (HyperA arr b a) b
invoke HyperA (K m) b a
k) HyperA (K m) a b
h
  runK f a_val

-- | Close the self-referential loop using 'mfix'.
runHyperK :: (MonadFix m) => HyperA (K m) a a -> m a
runHyperK :: forall (m :: * -> *) a. MonadFix m => HyperA (K m) a a -> m a
runHyperK HyperA (K m) a a
h = (a -> m a) -> m a
forall a. (a -> m a) -> m a
forall (m :: * -> *) a. MonadFix m => (a -> m a) -> m a
mfix ((a -> m a) -> m a) -> (a -> m a) -> m a
forall a b. (a -> b) -> a -> b
$ \a
a -> K m (HyperA (K m) a a) a -> HyperA (K m) a a -> m a
forall {k} (m :: k -> *) a (b :: k). K m a b -> a -> m b
runK (HyperA (K m) a a -> K m (HyperA (K m) a a) a
forall {k} (arr :: * -> k -> *) (a :: k) (b :: k).
HyperA arr a b -> arr (HyperA arr b a) b
invoke HyperA (K m) a a
h) (a -> HyperA (K m) a a
forall (m :: * -> *) b a. Monad m => b -> HyperA (K m) a b
baseK a
a)

-- * Function-category instances

instance Category Hyper where
  id :: forall a. Hyper a a
id = (a -> a) -> Hyper a a
forall a b. (a -> b) -> Hyper a b
lift a -> a
forall a. a -> a
forall k (arr :: k -> k -> *) (a :: k). Category arr => arr a a
id
  Hyper b c
f . :: forall b c a. Hyper b c -> Hyper a b -> Hyper a c
. Hyper a b
g = (HyperA (->) c a -> c) -> HyperA (->) a c
forall {k} (arr :: * -> k -> *) (a :: k) (b :: k).
arr (HyperA arr b a) b -> HyperA arr a b
HyperA ((HyperA (->) c a -> c) -> HyperA (->) a c)
-> (HyperA (->) c a -> c) -> HyperA (->) a c
forall a b. (a -> b) -> a -> b
$ \HyperA (->) c a
k -> Hyper b c -> HyperA (->) c b -> c
forall {k} (arr :: * -> k -> *) (a :: k) (b :: k).
HyperA arr a b -> arr (HyperA arr b a) b
invoke Hyper b c
f (Hyper a b
g Hyper a b -> HyperA (->) c a -> HyperA (->) c b
forall b c a. Hyper b c -> Hyper a b -> Hyper a c
forall k (arr :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category arr =>
arr b c -> arr a b -> arr a c
. HyperA (->) c a
k)

instance Channel (,) Hyper where
  assoc :: forall a b c. Hyper ((a, b), c) (a, (b, c))
assoc = (((a, b), c) -> (a, (b, c))) -> Hyper ((a, b), c) (a, (b, c))
forall a b. (a -> b) -> Hyper a b
lift ((a, b), c) -> (a, (b, c))
forall a b c. ((a, b), c) -> (a, (b, c))
forall {k} (t :: k -> k -> k) (arr :: k -> k -> *) (a :: k)
       (b :: k) (c :: k).
Channel t arr =>
arr (t (t a b) c) (t a (t b c))
assoc
  assoc' :: forall a b c. Hyper (a, (b, c)) ((a, b), c)
assoc' = ((a, (b, c)) -> ((a, b), c)) -> Hyper (a, (b, c)) ((a, b), c)
forall a b. (a -> b) -> Hyper a b
lift (a, (b, c)) -> ((a, b), c)
forall a b c. (a, (b, c)) -> ((a, b), c)
forall {k} (t :: k -> k -> k) (arr :: k -> k -> *) (a :: k)
       (b :: k) (c :: k).
Channel t arr =>
arr (t a (t b c)) (t (t a b) c)
assoc'
  slide :: forall a b c. Hyper (a, (b, c)) (b, (a, c))
slide = ((a, (b, c)) -> (b, (a, c))) -> Hyper (a, (b, c)) (b, (a, c))
forall a b. (a -> b) -> Hyper a b
lift (a, (b, c)) -> (b, (a, c))
forall a b c. (a, (b, c)) -> (b, (a, c))
forall {k} (t :: k -> k -> k) (arr :: k -> k -> *) (a :: k)
       (b :: k) (c :: k).
Channel t arr =>
arr (t a (t b c)) (t b (t a c))
slide

instance Strength (,) Hyper where
  strength :: forall b c a. Hyper b c -> Hyper (a, b) (a, c)
strength Hyper b c
h = ((a, b) -> (a, c)) -> Hyper (a, b) (a, c)
forall a b. (a -> b) -> Hyper a b
lift (((a, b) -> (a, c)) -> Hyper (a, b) (a, c))
-> ((a, b) -> (a, c)) -> Hyper (a, b) (a, c)
forall a b. (a -> b) -> a -> b
$ \(a
a, b
b) -> (a
a, Hyper b c -> b -> c
forall a b. Hyper a b -> a -> b
observe Hyper b c
h b
b)

instance Traced (,) Hyper where
  trace :: forall a b c. Hyper (a, b) (a, c) -> Hyper b c
trace Hyper (a, b) (a, c)
body = (HyperA (->) c b -> c) -> HyperA (->) b c
forall {k} (arr :: * -> k -> *) (a :: k) (b :: k).
arr (HyperA arr b a) b -> HyperA arr a b
HyperA ((HyperA (->) c b -> c) -> HyperA (->) b c)
-> (HyperA (->) c b -> c) -> HyperA (->) b c
forall a b. (a -> b) -> a -> b
$ \HyperA (->) c b
k ->
    let pair :: (a, c)
pair = Hyper (a, b) (a, c) -> HyperA (->) (a, c) (a, b) -> (a, c)
forall {k} (arr :: * -> k -> *) (a :: k) (b :: k).
HyperA arr a b -> arr (HyperA arr b a) b
invoke Hyper (a, b) (a, c)
body HyperA (->) (a, c) (a, b)
cont
        cont :: HyperA (->) (a, c) (a, b)
cont = (Hyper (a, b) (a, c) -> (a, b)) -> HyperA (->) (a, c) (a, b)
forall {k} (arr :: * -> k -> *) (a :: k) (b :: k).
arr (HyperA arr b a) b -> HyperA arr a b
HyperA ((Hyper (a, b) (a, c) -> (a, b)) -> HyperA (->) (a, c) (a, b))
-> (Hyper (a, b) (a, c) -> (a, b)) -> HyperA (->) (a, c) (a, b)
forall a b. (a -> b) -> a -> b
$ \Hyper (a, b) (a, c)
_ -> ((a, c) -> a
forall a b. (a, b) -> a
fst (a, c)
pair, HyperA (->) c b -> c -> b
forall a b. Hyper a b -> a -> b
observe HyperA (->) c b
k ((a, c) -> c
forall a b. (a, b) -> b
snd (a, c)
pair))
     in (a, c) -> c
forall a b. (a, b) -> b
snd (a, c)
pair

-- * Kleisli instances

instance (Monad m) => Category (HyperA (K m)) where
  id :: forall a. HyperA (K m) a a
id = K m a a -> HyperA (K m) a a
forall (m :: * -> *) a b. Monad m => K m a b -> HyperA (K m) a b
liftK K m a a
forall a. K m a a
forall k (arr :: k -> k -> *) (a :: k). Category arr => arr a a
id
  HyperA (K m) b c
f . :: forall b c a.
HyperA (K m) b c -> HyperA (K m) a b -> HyperA (K m) a c
. HyperA (K m) a b
g = K m (HyperA (K m) c a) c -> HyperA (K m) a c
forall {k} (arr :: * -> k -> *) (a :: k) (b :: k).
arr (HyperA arr b a) b -> HyperA arr a b
HyperA (K m (HyperA (K m) c a) c -> HyperA (K m) a c)
-> K m (HyperA (K m) c a) c -> HyperA (K m) a c
forall a b. (a -> b) -> a -> b
$ (HyperA (K m) c a -> m c) -> K m (HyperA (K m) c a) c
forall {k} (m :: k -> *) a (b :: k). (a -> m b) -> K m a b
K ((HyperA (K m) c a -> m c) -> K m (HyperA (K m) c a) c)
-> (HyperA (K m) c a -> m c) -> K m (HyperA (K m) c a) c
forall a b. (a -> b) -> a -> b
$ \HyperA (K m) c a
k -> K m (HyperA (K m) c b) c -> HyperA (K m) c b -> m c
forall {k} (m :: k -> *) a (b :: k). K m a b -> a -> m b
runK (HyperA (K m) b c -> K m (HyperA (K m) c b) c
forall {k} (arr :: * -> k -> *) (a :: k) (b :: k).
HyperA arr a b -> arr (HyperA arr b a) b
invoke HyperA (K m) b c
f) (HyperA (K m) a b
g HyperA (K m) a b -> HyperA (K m) c a -> HyperA (K m) c b
forall b c a.
HyperA (K m) b c -> HyperA (K m) a b -> HyperA (K m) a c
forall k (arr :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category arr =>
arr b c -> arr a b -> arr a c
. HyperA (K m) c a
k)

instance (Monad m) => Channel (,) (HyperA (K m)) where
  assoc :: forall a b c. HyperA (K m) ((a, b), c) (a, (b, c))
assoc = K m ((a, b), c) (a, (b, c)) -> HyperA (K m) ((a, b), c) (a, (b, c))
forall (m :: * -> *) a b. Monad m => K m a b -> HyperA (K m) a b
liftK K m ((a, b), c) (a, (b, c))
forall a b c. K m ((a, b), c) (a, (b, c))
forall {k} (t :: k -> k -> k) (arr :: k -> k -> *) (a :: k)
       (b :: k) (c :: k).
Channel t arr =>
arr (t (t a b) c) (t a (t b c))
assoc
  assoc' :: forall a b c. HyperA (K m) (a, (b, c)) ((a, b), c)
assoc' = K m (a, (b, c)) ((a, b), c) -> HyperA (K m) (a, (b, c)) ((a, b), c)
forall (m :: * -> *) a b. Monad m => K m a b -> HyperA (K m) a b
liftK K m (a, (b, c)) ((a, b), c)
forall a b c. K m (a, (b, c)) ((a, b), c)
forall {k} (t :: k -> k -> k) (arr :: k -> k -> *) (a :: k)
       (b :: k) (c :: k).
Channel t arr =>
arr (t a (t b c)) (t (t a b) c)
assoc'
  slide :: forall a b c. HyperA (K m) (a, (b, c)) (b, (a, c))
slide = K m (a, (b, c)) (b, (a, c)) -> HyperA (K m) (a, (b, c)) (b, (a, c))
forall (m :: * -> *) a b. Monad m => K m a b -> HyperA (K m) a b
liftK K m (a, (b, c)) (b, (a, c))
forall a b c. K m (a, (b, c)) (b, (a, c))
forall {k} (t :: k -> k -> k) (arr :: k -> k -> *) (a :: k)
       (b :: k) (c :: k).
Channel t arr =>
arr (t a (t b c)) (t b (t a c))
slide

instance (Monad m) => Strength (,) (HyperA (K m)) where
  strength :: forall b c a. HyperA (K m) b c -> HyperA (K m) (a, b) (a, c)
strength HyperA (K m) b c
h = K m (a, b) (a, c) -> HyperA (K m) (a, b) (a, c)
forall (m :: * -> *) a b. Monad m => K m a b -> HyperA (K m) a b
liftK (K m (a, b) (a, c) -> HyperA (K m) (a, b) (a, c))
-> K m (a, b) (a, c) -> HyperA (K m) (a, b) (a, c)
forall a b. (a -> b) -> a -> b
$ ((a, b) -> m (a, c)) -> K m (a, b) (a, c)
forall {k} (m :: k -> *) a (b :: k). (a -> m b) -> K m a b
K (((a, b) -> m (a, c)) -> K m (a, b) (a, c))
-> ((a, b) -> m (a, c)) -> K m (a, b) (a, c)
forall a b. (a -> b) -> a -> b
$ \(a
a, b
b) -> (a
a,) (c -> (a, c)) -> m c -> m (a, c)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> HyperA (K m) b c -> b -> m c
forall (m :: * -> *) a b. Monad m => HyperA (K m) a b -> a -> m b
observeK HyperA (K m) b c
h b
b

instance (MonadFix m) => Traced (,) (HyperA (K m)) where
  trace :: forall a b c. HyperA (K m) (a, b) (a, c) -> HyperA (K m) b c
trace HyperA (K m) (a, b) (a, c)
body = K m (HyperA (K m) c b) c -> HyperA (K m) b c
forall {k} (arr :: * -> k -> *) (a :: k) (b :: k).
arr (HyperA arr b a) b -> HyperA arr a b
HyperA (K m (HyperA (K m) c b) c -> HyperA (K m) b c)
-> K m (HyperA (K m) c b) c -> HyperA (K m) b c
forall a b. (a -> b) -> a -> b
$ (HyperA (K m) c b -> m c) -> K m (HyperA (K m) c b) c
forall {k} (m :: k -> *) a (b :: k). (a -> m b) -> K m a b
K ((HyperA (K m) c b -> m c) -> K m (HyperA (K m) c b) c)
-> (HyperA (K m) c b -> m c) -> K m (HyperA (K m) c b) c
forall a b. (a -> b) -> a -> b
$ \HyperA (K m) c b
k -> do
    pair <- ((a, c) -> m (a, c)) -> m (a, c)
forall a. (a -> m a) -> m a
forall (m :: * -> *) a. MonadFix m => (a -> m a) -> m a
mfix (((a, c) -> m (a, c)) -> m (a, c))
-> ((a, c) -> m (a, c)) -> m (a, c)
forall a b. (a -> b) -> a -> b
$ \(a, c)
pair -> do
      let cont :: HyperA (K m) (a, c) (a, b)
cont =
            K m (HyperA (K m) (a, b) (a, c)) (a, b)
-> HyperA (K m) (a, c) (a, b)
forall {k} (arr :: * -> k -> *) (a :: k) (b :: k).
arr (HyperA arr b a) b -> HyperA arr a b
HyperA (K m (HyperA (K m) (a, b) (a, c)) (a, b)
 -> HyperA (K m) (a, c) (a, b))
-> K m (HyperA (K m) (a, b) (a, c)) (a, b)
-> HyperA (K m) (a, c) (a, b)
forall a b. (a -> b) -> a -> b
$ (HyperA (K m) (a, b) (a, c) -> m (a, b))
-> K m (HyperA (K m) (a, b) (a, c)) (a, b)
forall {k} (m :: k -> *) a (b :: k). (a -> m b) -> K m a b
K ((HyperA (K m) (a, b) (a, c) -> m (a, b))
 -> K m (HyperA (K m) (a, b) (a, c)) (a, b))
-> (HyperA (K m) (a, b) (a, c) -> m (a, b))
-> K m (HyperA (K m) (a, b) (a, c)) (a, b)
forall a b. (a -> b) -> a -> b
$ \HyperA (K m) (a, b) (a, c)
_ -> do
              b <- HyperA (K m) c b -> c -> m b
forall (m :: * -> *) a b. Monad m => HyperA (K m) a b -> a -> m b
observeK HyperA (K m) c b
k ((a, c) -> c
forall a b. (a, b) -> b
snd (a, c)
pair)
              pure (fst pair, b)
      K m (HyperA (K m) (a, c) (a, b)) (a, c)
-> HyperA (K m) (a, c) (a, b) -> m (a, c)
forall {k} (m :: k -> *) a (b :: k). K m a b -> a -> m b
runK (HyperA (K m) (a, b) (a, c)
-> K m (HyperA (K m) (a, c) (a, b)) (a, c)
forall {k} (arr :: * -> k -> *) (a :: k) (b :: k).
HyperA arr a b -> arr (HyperA arr b a) b
invoke HyperA (K m) (a, b) (a, c)
body) HyperA (K m) (a, c) (a, b)
cont
    pure (snd pair)

-- * Either-loop state machine

-- | Encode an Either-loop as a self-referential 'Hyper'.
--
-- Whereas 'encode' handles the @(,)@ tensor using @Hyper@'s own 'Traced'
-- instance, this preserves the Either-loop state in the function domain.
-- @Left a@ feeds back; @Right c@ terminates with output.
--
-- >>> :{
-- let step = \case
--       Right n | n < 3 -> Left (n + 1)
--       Right n         -> Right n
--       Left n  | n < 3 -> Left (n + 1)
--       Left n          -> Right n
-- :}
--
-- >>> runEither step (0 :: Int)
-- 3
encodeEither ::
  (Either a b -> Either a c) ->
  Hyper (Either a b -> c) (Either a b -> c)
encodeEither :: forall a b c.
(Either a b -> Either a c)
-> Hyper (Either a b -> c) (Either a b -> c)
encodeEither Either a b -> Either a c
f = Hyper (Either a b -> c) (Either a b -> c)
h
  where
    h :: Hyper (Either a b -> c) (Either a b -> c)
h =
      (Hyper (Either a b -> c) (Either a b -> c) -> Either a b -> c)
-> Hyper (Either a b -> c) (Either a b -> c)
forall b a. (HyperA (->) b a -> b) -> Hyper a b
Hyper
        ( \Hyper (Either a b -> c) (Either a b -> c)
k Either a b
s ->
            case Either a b -> Either a c
f Either a b
s of
              Right c
c -> c
c
              Left a
a -> Hyper (Either a b -> c) (Either a b -> c)
-> Hyper (Either a b -> c) (Either a b -> c) -> Either a b -> c
forall {k} (arr :: * -> k -> *) (a :: k) (b :: k).
HyperA arr a b -> arr (HyperA arr b a) b
invoke Hyper (Either a b -> c) (Either a b -> c)
k Hyper (Either a b -> c) (Either a b -> c)
h (a -> Either a b
forall a b. a -> Either a b
Left a
a)
        )

-- | Run an 'encodeEither'-encoded circuit from initial input @b@.
--
-- 'encodeEither' embeds the Either state machine into 'Hyper', 'runHyper'
-- ties the self-referential knot, and @Right b@ injects the initial state.
--
-- >>> :{
-- let step = \case
--       Right n | n < 3 -> Left (n + 1)
--       Right n         -> Right n
--       Left n  | n < 3 -> Left (n + 1)
--       Left n          -> Right n
-- :}
--
-- >>> runEither step (0 :: Int)
-- 3
runEither :: (Either a b -> Either a c) -> b -> c
runEither :: forall a b c. (Either a b -> Either a c) -> b -> c
runEither Either a b -> Either a c
f b
b = Hyper (Either a b -> c) (Either a b -> c) -> Either a b -> c
forall a. Hyper a a -> a
runHyper ((Either a b -> Either a c)
-> Hyper (Either a b -> c) (Either a b -> c)
forall a b c.
(Either a b -> Either a c)
-> Hyper (Either a b -> c) (Either a b -> c)
encodeEither Either a b -> Either a c
f) (b -> Either a b
forall a b. b -> Either a b
Right b
b)

-- * Bridges from initial syntax

-- | Encode a function-category 'Trace' into a 'Hyper'.
--
-- This is the unique traced functor from the initial syntax ('Trace')
-- to the final object ('Hyper'), satisfying the commuting triangle
-- @'observe' . 'encode' = 'Circuit.Syntax.eval'@.
--
-- 'base' constructors embed directly via 'lift'; 'Circuit.Trace.yank'
-- constructors become 'trace' over a hyperfunction.
--
-- >>> import qualified Circuit.Trace as Trace
-- >>> observe (encode (Trace.base (+1) :: Trace.Trace (,) (->) Int Int)) 5
-- 6
encode ::
  Trace (,) (->) a b ->
  Hyper a b
encode :: forall a b. Trace (,) (->) a b -> Hyper a b
encode (Syn.Lift a -> b
f) = (a -> b) -> Hyper a b
forall a b. (a -> b) -> Hyper a b
lift a -> b
f
encode (Syn.Op (L (SigCompose Syntax (SigCompose :+: SigYank (,)) (->) b1 b
g Syntax (SigCompose :+: SigYank (,)) (->) a b1
f))) = Syntax (SigCompose :+: SigYank (,)) (->) b1 b -> Hyper b1 b
forall a b. Trace (,) (->) a b -> Hyper a b
encode Syntax (SigCompose :+: SigYank (,)) (->) b1 b
g Hyper b1 b -> HyperA (->) a b1 -> Hyper a b
forall b c a. Hyper b c -> Hyper a b -> Hyper a c
forall k (arr :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category arr =>
arr b c -> arr a b -> arr a c
. Syntax (SigCompose :+: SigYank (,)) (->) a b1 -> HyperA (->) a b1
forall a b. Trace (,) (->) a b -> Hyper a b
encode Syntax (SigCompose :+: SigYank (,)) (->) a b1
f
encode (Syn.Op (R (Yank Syntax (SigCompose :+: SigYank (,)) (->) (s, a) (s, b)
body))) = HyperA (->) (s, a) (s, b) -> Hyper a b
forall a b c. Hyper (a, b) (a, c) -> Hyper b c
forall {k} (t :: k -> k -> k) (arr :: k -> k -> *) (a :: k)
       (b :: k) (c :: k).
Traced t arr =>
arr (t a b) (t a c) -> arr b c
trace (Syntax (SigCompose :+: SigYank (,)) (->) (s, a) (s, b)
-> HyperA (->) (s, a) (s, b)
forall a b. Trace (,) (->) a b -> Hyper a b
encode Syntax (SigCompose :+: SigYank (,)) (->) (s, a) (s, b)
body)

-- | Encode a Kleisli 'Trace' into a @'HyperA' ('K' m)@.
encodeK ::
  (MonadFix m) =>
  Trace (,) (K m) a b ->
  HyperA (K m) a b
encodeK :: forall (m :: * -> *) a b.
MonadFix m =>
Trace (,) (K m) a b -> HyperA (K m) a b
encodeK (Syn.Lift K m a b
f) = K m a b -> HyperA (K m) a b
forall (m :: * -> *) a b. Monad m => K m a b -> HyperA (K m) a b
liftK K m a b
f
encodeK (Syn.Op (L (SigCompose Syntax (SigCompose :+: SigYank (,)) (K m) b1 b
g Syntax (SigCompose :+: SigYank (,)) (K m) a b1
f))) = Syntax (SigCompose :+: SigYank (,)) (K m) b1 b -> HyperA (K m) b1 b
forall (m :: * -> *) a b.
MonadFix m =>
Trace (,) (K m) a b -> HyperA (K m) a b
encodeK Syntax (SigCompose :+: SigYank (,)) (K m) b1 b
g HyperA (K m) b1 b -> HyperA (K m) a b1 -> HyperA (K m) a b
forall b c a.
HyperA (K m) b c -> HyperA (K m) a b -> HyperA (K m) a c
forall k (arr :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category arr =>
arr b c -> arr a b -> arr a c
. Syntax (SigCompose :+: SigYank (,)) (K m) a b1 -> HyperA (K m) a b1
forall (m :: * -> *) a b.
MonadFix m =>
Trace (,) (K m) a b -> HyperA (K m) a b
encodeK Syntax (SigCompose :+: SigYank (,)) (K m) a b1
f
encodeK (Syn.Op (R (Yank Syntax (SigCompose :+: SigYank (,)) (K m) (s, a) (s, b)
body))) = HyperA (K m) (s, a) (s, b) -> HyperA (K m) a b
forall a b c. HyperA (K m) (a, b) (a, c) -> HyperA (K m) b c
forall {k} (t :: k -> k -> k) (arr :: k -> k -> *) (a :: k)
       (b :: k) (c :: k).
Traced t arr =>
arr (t a b) (t a c) -> arr b c
trace (Syntax (SigCompose :+: SigYank (,)) (K m) (s, a) (s, b)
-> HyperA (K m) (s, a) (s, b)
forall (m :: * -> *) a b.
MonadFix m =>
Trace (,) (K m) a b -> HyperA (K m) a b
encodeK Syntax (SigCompose :+: SigYank (,)) (K m) (s, a) (s, b)
body)