-- | Finite spans as the residual-remembering rung of the equipment ladder.
--
-- A span @A ←s— X —t→ B@ is two functions out of a shared apex @X@.  In the
-- equipment-optics story the apex is the residual of the interface.  In
-- "Span" equipments that residual is remembered on the nose: composition is a
-- pullback of apexes, and an optic between spans is just an apex map
-- commuting with the legs.  In @circuits@ the same shape appears as
-- @Body t ch arr a b@, with the channel @ch@ playing the role of the apex.
module Circuit.Span
  ( Span (..),
    pairs,
    companion,
    conjoint,
    composeS,
    identityS,
    presentS,

    -- * 2-cells between spans
    refinesS,

    -- * Metric optics
    spanDistance,
  )
where

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

-- $setup
-- >>> import Circuit.Span
-- >>> import Control.Category (id)
-- >>> import Prelude hiding (id, (.))

-- | A finite span with apex @x@ hidden existentially.
--
-- The apex must be 'Eq' so that pullback composition is computable.  Unlike
-- the relation view, the apex is part of the value: two spans with the same
-- boundary relation but different apexes are different spans.  This is the
-- "residual remembered on the nose" rung of the ladder.
data Span a b = forall x. (Eq x) => Span [x] (x -> a) (x -> b)

-- | View a span as its list of boundary pairs.
--
-- Note that this deliberately forgets the apex, so two spans that are not
-- isomorphic can 'show' alike.  That is the Rel rung looking at a Span-rung
-- value, not an accident.
instance (Show a, Show b) => Show (Span a b) where
  show :: Span a b -> String
show = [(a, b)] -> String
forall a. Show a => a -> String
show ([(a, b)] -> String)
-> (Span a b -> [(a, b)]) -> Span a b -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
forall {k} (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. Span a b -> [(a, b)]
forall a b. Span a b -> [(a, b)]
pairs

-- | Forget the apex and return the boundary pairs.
pairs :: Span a b -> [(a, b)]
pairs :: forall a b. Span a b -> [(a, b)]
pairs (Span [x]
xs x -> a
s x -> b
t) = [(x -> a
s x
x, x -> b
t x
x) | x
x <- [x]
xs]

-- | The companion of a function: its graph read forward.
--
-- @companion xs f@ is the span @A ←id— A —f→ B@.
companion :: (Eq a) => [a] -> (a -> b) -> Span a b
companion :: forall a b. Eq a => [a] -> (a -> b) -> Span a b
companion [a]
xs a -> b
f = [a] -> (a -> a) -> (a -> b) -> Span a b
forall a b x. Eq x => [x] -> (x -> a) -> (x -> b) -> Span a b
Span [a]
xs a -> a
forall a. a -> a
forall {k} (cat :: k -> k -> *) (a :: k). Category cat => cat a a
id a -> b
f

-- | The conjoint of a function: its graph read backward.
--
-- @conjoint xs f@ is the span @B ←f— A —id→ A@.
conjoint :: (Eq a) => [a] -> (a -> b) -> Span b a
conjoint :: forall a b. Eq a => [a] -> (a -> b) -> Span b a
conjoint [a]
xs a -> b
f = [a] -> (a -> b) -> (a -> a) -> Span b a
forall a b x. Eq x => [x] -> (x -> a) -> (x -> b) -> Span a b
Span [a]
xs a -> b
f a -> a
forall a. a -> a
forall {k} (cat :: k -> k -> *) (a :: k). Category cat => cat a a
id

-- | Pullback composition of spans.  The new apex is the set of pairs that
-- agree on the shared boundary.
composeS :: (Eq b) => Span b c -> Span a b -> Span a c
composeS :: forall b c a. Eq b => Span b c -> Span a b -> Span a c
composeS (Span [x]
ys x -> b
h x -> c
k) (Span [x]
xs x -> a
f x -> b
g) =
  [(x, x)] -> ((x, x) -> a) -> ((x, x) -> c) -> Span a c
forall a b x. Eq x => [x] -> (x -> a) -> (x -> b) -> Span a b
Span [(x
x, x
y) | x
x <- [x]
xs, x
y <- [x]
ys, x -> b
g x
x b -> b -> Bool
forall a. Eq a => a -> a -> Bool
== x -> b
h x
y] (\(x
x, x
_) -> x -> a
f x
x) (\(x
_, x
y) -> x -> c
k x
y)

-- | The identity span on a finite type, given by its enumeration.
identityS :: (Eq a) => [a] -> Span a a
identityS :: forall a. Eq a => [a] -> Span a a
identityS [a]
xs = [a] -> (a -> a) -> Span a a
forall a b. Eq a => [a] -> (a -> b) -> Span a b
companion [a]
xs a -> a
forall a. a -> a
forall {k} (cat :: k -> k -> *) (a :: k). Category cat => cat a a
id

-- | Present a span as its own two legs: @⟨s,t⟩ = s* ⊙ t_*@.
--
-- The result has the same boundary pairs as the original, but its apex is
-- the diagonal pulled back along identity — the same span up to apex
-- isomorphism, never up to quotient.
presentS :: Span a b -> Span a b
presentS :: forall a b. Span a b -> Span a b
presentS (Span [x]
xs x -> a
s x -> b
t) = Span x b -> Span a x -> Span a b
forall b c a. Eq b => Span b c -> Span a b -> Span a c
composeS ([x] -> (x -> b) -> Span x b
forall a b. Eq a => [a] -> (a -> b) -> Span a b
companion [x]
xs x -> b
t) ([x] -> (x -> a) -> Span a x
forall a b. Eq a => [a] -> (a -> b) -> Span b a
conjoint [x]
xs x -> a
s)

-- | Does a span 2-cell from the first span to the second exist?
--
-- A 2-cell is an apex map @h@ with @a . h = s@ and @b . h = t@.  Over finite
-- enumerations such an @h@ exists exactly when every boundary pair of the
-- source occurs in the target, so existence is decidable from the 'pairs'
-- view alone — no access to the apexes required.
--
-- This is the existence statement; checking a /given/ witness needs the
-- apexes and lives with the caller that built them.  The gap between the two
-- is the ladder: @refinesS@ is what the Rel rung can see, and it is strictly
-- less than the Span rung, which distinguishes non-isomorphic apexes with the
-- same pairs.
--
-- >>> let p = Span [1 :: Int, 2] id id :: Span Int Int
-- >>> let q = Span [1 :: Int, 2, 3] id id :: Span Int Int
-- >>> (refinesS p q, refinesS q p)
-- (True,False)
refinesS :: (Eq a, Eq b) => Span a b -> Span a b -> Bool
refinesS :: forall a b. (Eq a, Eq b) => Span a b -> Span a b -> Bool
refinesS Span a b
p Span a b
q = ((a, b) -> Bool) -> [(a, b)] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all ((a, b) -> [(a, b)] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` Span a b -> [(a, b)]
forall a b. Span a b -> [(a, b)]
pairs Span a b
q) (Span a b -> [(a, b)]
forall a b. Span a b -> [(a, b)]
pairs Span a b
p)

-- | Directed Hausdorff distance between two spans over a common boundary:
--
-- @
--   d((s,t),(a,b)) = sup_x inf_y [ d(s x, a y) + d(b y, t x) ]
-- @
--
-- The @sup@ ranges over the /domain/ apex and the @inf@ over the /codomain/
-- apex.  Those are not two spellings of the same thing: in
-- @([0,∞], ≥)@-enrichment limits are suprema and colimits are infima, so the
-- @sup@ is the end and the @inf@ is the coend.  This function is therefore
-- the general @∫_x ∫^y@ shape made concrete, not merely a metric analogue of
-- it — which is also why it cannot be written in a bare semiring: for the
-- tropical scalar the @inf@ is the semiring addition but the @sup@ belongs to
-- the dual semiring.
--
-- The two units are the degenerate cases and must be supplied:
--
-- * @bot@ is the value of a @sup@ over an empty domain apex (@0@ for a
--   tropical scalar) — a span with no apex points is distance @bot@ from
--   anything;
-- * @top@ is the value of an @inf@ over an empty codomain apex (@+∞@) —
--   nothing can be approximated by a span with no apex points.
--
-- Passing them explicitly is what keeps this total; folding with 'maximum'
-- and 'minimum' would throw on either empty enumeration.
--
-- >>> let dist x y = abs (fromIntegral x - fromIntegral y) :: Double
-- >>> let sA = Span [0 :: Int, 1] id id
-- >>> let sB = Span [0 :: Int] id id
-- >>> spanDistance 0 (1 / 0) (+) dist dist sA sA
-- 0.0
-- >>> spanDistance 0 (1 / 0) (+) dist dist sA sB
-- 2.0
--
-- The empty codomain apex is total, not an exception:
--
-- >>> spanDistance 0 (1 / 0) (+) dist dist sA (Span ([] :: [Int]) id id)
-- Infinity
spanDistance ::
  (Ord d) =>
  -- | @bot@: the supremum over an empty domain apex.
  d ->
  -- | @top@: the infimum over an empty codomain apex.
  d ->
  -- | Addition of the forward and backward costs.
  (d -> d -> d) ->
  -- | Distance on the left boundary.
  (a -> a -> d) ->
  -- | Distance on the right boundary.
  (b -> b -> d) ->
  Span a b ->
  Span a b ->
  d
spanDistance :: forall d a b.
Ord d =>
d
-> d
-> (d -> d -> d)
-> (a -> a -> d)
-> (b -> b -> d)
-> Span a b
-> Span a b
-> d
spanDistance d
bot d
top d -> d -> d
add a -> a -> d
da b -> b -> d
db (Span [x]
xs x -> a
s1 x -> b
t1) (Span [x]
ys x -> a
s2 x -> b
t2) =
  (d -> d -> d) -> d -> [d] -> d
forall a b. (a -> b -> b) -> b -> [a] -> b
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr
    d -> d -> d
forall a. Ord a => a -> a -> a
max
    d
bot
    [ (d -> d -> d) -> d -> [d] -> d
forall a b. (a -> b -> b) -> b -> [a] -> b
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr d -> d -> d
forall a. Ord a => a -> a -> a
min d
top [d -> d -> d
add (a -> a -> d
da (x -> a
s1 x
x) (x -> a
s2 x
y)) (b -> b -> d
db (x -> b
t2 x
y) (x -> b
t1 x
x)) | x
y <- [x]
ys]
    | x
x <- [x]
xs
    ]