-- | Parameterised morphisms: @(p, a) -> b@.
--
-- @Para p@ is the constant-state slice of @Loop (,)@ — it threads a read-only
-- parameter through a composition chain.  Composition threads the same
-- parameter to both morphisms; 'id' discards it.
--
-- === Law oracles (see circuits-learn-axioma)
--
-- 1. 'Category' associativity: @(h '.' g) '.' f == h '.' (g '.' f)@
-- 2. @Para@ composition is @Loop (,)@ constant-state: threading a constant
--    parameter through a loop yields the same result as the para composition.
module Circuit.Learn.Para
  ( -- * Type
    Para (..),

    -- * Running
    runPara,
    liftPara,
    forgetPara,
  )
where

import Control.Arrow (Arrow (..), ArrowLoop (..))
import Control.Category (Category (..))
import Data.Profunctor (Costrong (..), Profunctor (..), Strong (..))
import Prelude hiding (id, (.))

-- | Parameterised morphism: @(p, a) -> b@.
newtype Para p a b = Para {forall p a b. Para p a b -> (p, a) -> b
unPara :: (p, a) -> b}

-- | Run with explicit parameter.
runPara :: Para p a b -> p -> a -> b
runPara :: forall p a b. Para p a b -> p -> a -> b
runPara (Para (p, a) -> b
f) p
p a
a = (p, a) -> b
f (p
p, a
a)

instance Category (Para p) where
  id :: forall a. Para p a a
id = ((p, a) -> a) -> Para p a a
forall p a b. ((p, a) -> b) -> Para p a b
Para (p, a) -> a
forall a b. (a, b) -> b
snd
  Para (p, b) -> c
g . :: forall b c a. Para p b c -> Para p a b -> Para p a c
. Para (p, a) -> b
f = ((p, a) -> c) -> Para p a c
forall p a b. ((p, a) -> b) -> Para p a b
Para (((p, a) -> c) -> Para p a c) -> ((p, a) -> c) -> Para p a c
forall a b. (a -> b) -> a -> b
$ \(p
p, a
a) -> (p, b) -> c
g (p
p, (p, a) -> b
f (p
p, a
a))

instance Arrow (Para p) where
  arr :: forall b c. (b -> c) -> Para p b c
arr b -> c
f = ((p, b) -> c) -> Para p b c
forall p a b. ((p, a) -> b) -> Para p a b
Para (((p, b) -> c) -> Para p b c) -> ((p, b) -> c) -> Para p b c
forall a b. (a -> b) -> a -> b
$ \(p
_, b
a) -> b -> c
f b
a
  first :: forall b c d. Para p b c -> Para p (b, d) (c, d)
first (Para (p, b) -> c
f) = ((p, (b, d)) -> (c, d)) -> Para p (b, d) (c, d)
forall p a b. ((p, a) -> b) -> Para p a b
Para (((p, (b, d)) -> (c, d)) -> Para p (b, d) (c, d))
-> ((p, (b, d)) -> (c, d)) -> Para p (b, d) (c, d)
forall a b. (a -> b) -> a -> b
$ \(p
p, (b
a, d
c)) -> ((p, b) -> c
f (p
p, b
a), d
c)

instance ArrowLoop (Para p) where
  loop :: forall b d c. Para p (b, d) (c, d) -> Para p b c
loop (Para (p, (b, d)) -> (c, d)
f) = ((p, b) -> c) -> Para p b c
forall p a b. ((p, a) -> b) -> Para p a b
Para (((p, b) -> c) -> Para p b c) -> ((p, b) -> c) -> Para p b c
forall a b. (a -> b) -> a -> b
$ \(p
p, b
a) ->
    let (c
b, d
c) = (p, (b, d)) -> (c, d)
f (p
p, (b
a, d
c)) in c
b

instance Profunctor (Para p) where
  dimap :: forall a b c d. (a -> b) -> (c -> d) -> Para p b c -> Para p a d
dimap a -> b
f c -> d
g (Para (p, b) -> c
m) = ((p, a) -> d) -> Para p a d
forall p a b. ((p, a) -> b) -> Para p a b
Para (((p, a) -> d) -> Para p a d) -> ((p, a) -> d) -> Para p a d
forall a b. (a -> b) -> a -> b
$ \(p
p, a
a) -> c -> d
g ((p, b) -> c
m (p
p, a -> b
f a
a))

instance Strong (Para p) where
  first' :: forall a b c. Para p a b -> Para p (a, c) (b, c)
first' (Para (p, a) -> b
f) = ((p, (a, c)) -> (b, c)) -> Para p (a, c) (b, c)
forall p a b. ((p, a) -> b) -> Para p a b
Para (((p, (a, c)) -> (b, c)) -> Para p (a, c) (b, c))
-> ((p, (a, c)) -> (b, c)) -> Para p (a, c) (b, c)
forall a b. (a -> b) -> a -> b
$ \(p
p, (a
a, c
c)) -> ((p, a) -> b
f (p
p, a
a), c
c)

instance Costrong (Para p) where
  unfirst :: forall a d b. Para p (a, d) (b, d) -> Para p a b
unfirst (Para (p, (a, d)) -> (b, d)
f) = ((p, a) -> b) -> Para p a b
forall p a b. ((p, a) -> b) -> Para p a b
Para (((p, a) -> b) -> Para p a b) -> ((p, a) -> b) -> Para p a b
forall a b. (a -> b) -> a -> b
$ \(p
p, a
a) ->
    let (b
b, d
c) = (p, (a, d)) -> (b, d)
f (p
p, (a
a, d
c)) in b
b

-- | Lift a plain function, ignoring the parameter.
liftPara :: (a -> b) -> Para p a b
liftPara :: forall a b p. (a -> b) -> Para p a b
liftPara a -> b
f = ((p, a) -> b) -> Para p a b
forall p a b. ((p, a) -> b) -> Para p a b
Para (((p, a) -> b) -> Para p a b) -> ((p, a) -> b) -> Para p a b
forall a b. (a -> b) -> a -> b
$ \(p
_, a
a) -> a -> b
f a
a

-- | Forget the parameter, recover plain function.
forgetPara :: p -> Para p a b -> a -> b
forgetPara :: forall p a b. p -> Para p a b -> a -> b
forgetPara p
p (Para (p, a) -> b
f) a
a = (p, a) -> b
f (p
p, a
a)