{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE UndecidableInstances #-}

-- | The span fragment of polynomial functors.
--
-- The standard 'Circuit.Poly' encoding uses type families 'Pos' and 'Dir'.
-- 'Sum' has no 'Dir' row because directions over a sum are position-dependent,
-- and GHC cannot match on the result of a type family inside a GADT or type
-- family equation.
--
-- This module experiments with the alternative: represent a polynomial as a
-- span @Dir -> Pos@.  The position-dependency is carried by an explicit
-- projection function rather than by a dependent type family.  'Sum' becomes
-- the coproduct of spans, so it /does/ admit a netlist view in this encoding.
--
-- The cost is that correctness of the netlist view for 'Prod' becomes a fibre
-- condition: a direction function supplied to 'fromNetC' must return 'Nothing'
-- outside the fibre of the chosen position.  In the double-category picture
-- those fibre conditions are the lower-dimensional cells (companions,
-- conjoints, and the Beck–Chevalley cube).
--
-- The span fragment is the six constructors @CY@, @CConst@, @CExp@, @CSum@,
-- @CProd@ and @CTensor@.  'CComp' is included in the grammar but not in the
-- span fragment: it has a 'NetlistC' view, but no 'SpanC' projection.  See
-- 'loom/cube.md' for the research direction that 'CComp' belongs to.
--
-- The 'ETC' constructor is the netlist view inlined into the value; it is not
-- structural like 'ESC' or 'EPC'.  This makes tensor round-trips exact in the
-- spike, but it is an asymmetry of the encoding, not a mathematical fact about
-- tensors.
module Circuit.Poly.Span
  ( -- * Span descriptions
    Span (..),
    PosC,
    DirC,

    -- * Values
    EvalC (..),

    -- * Span projection (six span constructors)
    SpanC (..),
    onFibreC,

    -- * Netlist view (all seven constructors)
    NetlistC (..),
    netRoundTripC,

    -- * Sum / product distributivity
    prodSumDistrLC,
    prodSumDistrRC,
    distrPosLC,
    distrDirLC,

    -- * Composition product (outside the span fragment)
    nestedToCompC,
    compToNestedC,
    compAssocLC,
    compAssocRC,
  )
where

import Data.Bifunctor (bimap)
import Data.Kind (Type)
import Data.Maybe (fromMaybe)
import Data.Void (Void, absurd)
import Prelude

-- | Promoted description of a polynomial as a span @Dir -> Pos@.
--
-- Unlike 'Circuit.Poly.Poly', this grammar does not need a position-indexed
-- 'Dir' family; the projection is supplied by the 'SpanC' class at the term
-- level.
--
-- 'CComp' is in the grammar but outside the span fragment: it has a netlist
-- view, but no span projection.  See 'SpanC' and the module header.
data Span
  = CY
  | CConst Type
  | CExp Type
  | CSum Span Span
  | CProd Span Span
  | CTensor Span Span
  | CComp Span Span

-- | Position set of a span polynomial.
type family PosC (c :: Span) :: Type where
  PosC 'CY = ()
  PosC ('CConst a) = a
  PosC ('CExp a) = ()
  PosC ('CSum p q) = Either (PosC p) (PosC q)
  PosC ('CProd p q) = (PosC p, PosC q)
  PosC ('CTensor p q) = (PosC p, PosC q)
  PosC ('CComp p q) = (PosC p, DirC p -> PosC q)

-- | Total direction space of a span polynomial.
--
-- For 'CProd', the total direction space includes the /other/ position so that
-- the projection to the product of positions is a pure function.  In the
-- double-category picture this is the universal property of the product of
-- spans.
type family DirC (c :: Span) :: Type where
  DirC 'CY = ()
  DirC ('CConst a) = Void
  DirC ('CExp a) = a
  DirC ('CSum p q) = Either (DirC p) (DirC q)
  DirC ('CProd p q) = Either (DirC p, PosC q) (PosC p, DirC q)
  DirC ('CTensor p q) = (DirC p, DirC q)
  DirC ('CComp p q) = (DirC p, DirC q)

-- | Values of a span polynomial functor evaluated at @x@.
--
-- 'ETC' stores the tensor netlist directly: a pair of positions and a curried
-- direction function.  This is not structural like 'ESC' or 'EPC', and it makes
-- the tensor round-trip exact in the spike.  See the module header.
data EvalC (c :: Span) (x :: Type) where
  EYC :: x -> EvalC 'CY x
  EKC :: c -> EvalC ('CConst c) x
  EEC :: (a -> x) -> EvalC ('CExp a) x
  ESC :: Either (EvalC p x) (EvalC q x) -> EvalC ('CSum p q) x
  EPC :: (EvalC p x, EvalC q x) -> EvalC ('CProd p q) x
  ETC :: PosC p -> PosC q -> (DirC p -> DirC q -> x) -> EvalC ('CTensor p q) x
  ECC ::
    (PosC p, DirC p -> PosC q) ->
    ((DirC p, DirC q) -> x) ->
    EvalC ('CComp p q) x

instance Functor (EvalC c) where
  fmap :: forall a b. (a -> b) -> EvalC c a -> EvalC c b
fmap a -> b
f = \case
    EYC a
x -> b -> EvalC 'CY b
forall x. x -> EvalC 'CY x
EYC (a -> b
f a
x)
    EKC c
c -> c -> EvalC ('CConst c) b
forall p x. p -> EvalC ('CConst p) x
EKC c
c
    EEC a -> a
g -> (a -> b) -> EvalC ('CExp a) b
forall p x. (p -> x) -> EvalC ('CExp p) x
EEC (a -> b
f (a -> b) -> (a -> a) -> a -> b
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> a
g)
    ESC Either (EvalC p a) (EvalC q a)
e -> Either (EvalC p b) (EvalC q b) -> EvalC ('CSum p q) b
forall (p :: Span) x (q :: Span).
Either (EvalC p x) (EvalC q x) -> EvalC ('CSum p q) x
ESC ((EvalC p a -> EvalC p b)
-> (EvalC q a -> EvalC q b)
-> Either (EvalC p a) (EvalC q a)
-> Either (EvalC p b) (EvalC q b)
forall a b c d. (a -> b) -> (c -> d) -> Either a c -> Either b d
forall (p :: * -> * -> *) a b c d.
Bifunctor p =>
(a -> b) -> (c -> d) -> p a c -> p b d
bimap ((a -> b) -> EvalC p a -> EvalC p b
forall a b. (a -> b) -> EvalC p a -> EvalC p b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap a -> b
f) ((a -> b) -> EvalC q a -> EvalC q b
forall a b. (a -> b) -> EvalC q a -> EvalC q b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap a -> b
f) Either (EvalC p a) (EvalC q a)
e)
    EPC (EvalC p a
u, EvalC q a
v) -> (EvalC p b, EvalC q b) -> EvalC ('CProd p q) b
forall (p :: Span) x (q :: Span).
(EvalC p x, EvalC q x) -> EvalC ('CProd p q) x
EPC ((a -> b) -> EvalC p a -> EvalC p b
forall a b. (a -> b) -> EvalC p a -> EvalC p b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap a -> b
f EvalC p a
u, (a -> b) -> EvalC q a -> EvalC q b
forall a b. (a -> b) -> EvalC q a -> EvalC q b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap a -> b
f EvalC q a
v)
    ETC PosC p
i PosC q
j DirC p -> DirC q -> a
g -> PosC p
-> PosC q -> (DirC p -> DirC q -> b) -> EvalC ('CTensor p q) b
forall (p :: Span) (q :: Span) x.
PosC p
-> PosC q -> (DirC p -> DirC q -> x) -> EvalC ('CTensor p q) x
ETC PosC p
i PosC q
j (\DirC p
d DirC q
e -> a -> b
f (DirC p -> DirC q -> a
g DirC p
d DirC q
e))
    ECC (PosC p, DirC p -> PosC q)
pos (DirC p, DirC q) -> a
g -> (PosC p, DirC p -> PosC q)
-> ((DirC p, DirC q) -> b) -> EvalC ('CComp p q) b
forall (p :: Span) (q :: Span) x.
(PosC p, DirC p -> PosC q)
-> ((DirC p, DirC q) -> x) -> EvalC ('CComp p q) x
ECC (PosC p, DirC p -> PosC q)
pos (a -> b
f (a -> b) -> ((DirC p, DirC q) -> a) -> (DirC p, DirC q) -> b
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (DirC p, DirC q) -> a
g)

-- | Span polynomials: those constructors that admit a projection @Dir -> Pos@.
--
-- 'CComp' is deliberately /not/ an instance.  A single direction @(dp, dq)@
-- does not determine the hang map @'DirC' p -> 'PosC' q@, so there is no
-- function @'DirC' ('CComp' p q) -> 'PosC' ('CComp' p q)@ to write.  This is
-- a mathematical impossibility, not a Haskell limitation; it is documented at
-- the type level by the missing instance.
class SpanC (c :: Span) where
  projC :: DirC c -> PosC c

instance SpanC 'CY where
  projC :: DirC 'CY -> PosC 'CY
projC () = ()

instance SpanC ('CConst a) where
  projC :: DirC ('CConst a) -> PosC ('CConst a)
projC = Void -> a
DirC ('CConst a) -> PosC ('CConst a)
forall a. Void -> a
absurd

instance SpanC ('CExp a) where
  projC :: DirC ('CExp a) -> PosC ('CExp a)
projC DirC ('CExp a)
_ = ()

instance (SpanC p, SpanC q) => SpanC ('CSum p q) where
  projC :: DirC ('CSum p q) -> PosC ('CSum p q)
projC = (DirC p -> PosC p)
-> (DirC q -> PosC q)
-> Either (DirC p) (DirC q)
-> Either (PosC p) (PosC q)
forall a b c d. (a -> b) -> (c -> d) -> Either a c -> Either b d
forall (p :: * -> * -> *) a b c d.
Bifunctor p =>
(a -> b) -> (c -> d) -> p a c -> p b d
bimap (forall (c :: Span). SpanC c => DirC c -> PosC c
projC @p) (forall (c :: Span). SpanC c => DirC c -> PosC c
projC @q)

instance
  (SpanC p, SpanC q) =>
  SpanC ('CProd p q)
  where
  projC :: DirC ('CProd p q) -> PosC ('CProd p q)
projC = \case
    Left (DirC p
d, PosC q
j) -> (forall (c :: Span). SpanC c => DirC c -> PosC c
projC @p DirC p
d, PosC q
j)
    Right (PosC p
i, DirC q
e) -> (PosC p
i, forall (c :: Span). SpanC c => DirC c -> PosC c
projC @q DirC q
e)

instance (SpanC p, SpanC q) => SpanC ('CTensor p q) where
  projC :: DirC ('CTensor p q) -> PosC ('CTensor p q)
projC = (DirC p -> PosC p)
-> (DirC q -> PosC q) -> (DirC p, DirC q) -> (PosC p, PosC q)
forall a b c d. (a -> b) -> (c -> d) -> (a, c) -> (b, d)
forall (p :: * -> * -> *) a b c d.
Bifunctor p =>
(a -> b) -> (c -> d) -> p a c -> p b d
bimap (forall (c :: Span). SpanC c => DirC c -> PosC c
projC @p) (forall (c :: Span). SpanC c => DirC c -> PosC c
projC @q)

-- | Polynomials that admit a netlist view in the span encoding.
--
-- The netlist view is @EvalC p x ≅ (PosC p, DirC p -> Maybe x)@, where
-- 'Nothing' means "outside the fibre of the chosen position".
--
-- 'fromNetC' assumes the supplied function respects the fibre.  If it returns
-- 'Nothing' on a direction that is inside the fibre, 'fromNetC' raises an
-- internal error: that is the encoding's assertion of the Beck–Chevalley
-- condition, not user-facing junk.
--
-- Every constructor is an instance, including 'CComp', because a value of any
-- constructor can be stored together with its position and direction function.
-- 'CComp' is not a 'SpanC', so its netlist view is not a span netlist view.
class NetlistC (c :: Span) where
  toNetC :: EvalC c x -> (PosC c, DirC c -> Maybe x)
  fromNetC :: PosC c -> (DirC c -> Maybe x) -> EvalC c x

-- | Internal assertion: a direction that should be in the fibre must carry a
-- value.
expectJust :: Maybe a -> a
expectJust :: forall a. Maybe a -> a
expectJust = a -> Maybe a -> a
forall a. a -> Maybe a -> a
fromMaybe ([Char] -> a
forall a. HasCallStack => [Char] -> a
error [Char]
"Span.fromNetC: direction inside fibre returned Nothing")

instance NetlistC 'CY where
  toNetC :: forall x. EvalC 'CY x -> (PosC 'CY, DirC 'CY -> Maybe x)
toNetC (EYC x
x) = ((), \() -> x -> Maybe x
forall a. a -> Maybe a
Just x
x)
  fromNetC :: forall x. PosC 'CY -> (DirC 'CY -> Maybe x) -> EvalC 'CY x
fromNetC () DirC 'CY -> Maybe x
h = x -> EvalC 'CY x
forall x. x -> EvalC 'CY x
EYC (Maybe x -> x
forall a. Maybe a -> a
expectJust (DirC 'CY -> Maybe x
h ()))

instance NetlistC ('CConst a) where
  toNetC :: forall x.
EvalC ('CConst a) x
-> (PosC ('CConst a), DirC ('CConst a) -> Maybe x)
toNetC (EKC c
c) = (c
PosC ('CConst a)
c, Void -> Maybe x
DirC ('CConst a) -> Maybe x
forall a. Void -> a
absurd)
  fromNetC :: forall x.
PosC ('CConst a)
-> (DirC ('CConst a) -> Maybe x) -> EvalC ('CConst a) x
fromNetC PosC ('CConst a)
c DirC ('CConst a) -> Maybe x
_ = a -> EvalC ('CConst a) x
forall p x. p -> EvalC ('CConst p) x
EKC a
PosC ('CConst a)
c

instance NetlistC ('CExp a) where
  toNetC :: forall x.
EvalC ('CExp a) x -> (PosC ('CExp a), DirC ('CExp a) -> Maybe x)
toNetC (EEC a -> x
g) = ((), x -> Maybe x
forall a. a -> Maybe a
Just (x -> Maybe x) -> (a -> x) -> a -> Maybe x
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> x
g)
  fromNetC :: forall x.
PosC ('CExp a) -> (DirC ('CExp a) -> Maybe x) -> EvalC ('CExp a) x
fromNetC () DirC ('CExp a) -> Maybe x
h = (a -> x) -> EvalC ('CExp a) x
forall p x. (p -> x) -> EvalC ('CExp p) x
EEC (\a
a -> Maybe x -> x
forall a. Maybe a -> a
expectJust (DirC ('CExp a) -> Maybe x
h a
DirC ('CExp a)
a))

instance (NetlistC p, NetlistC q) => NetlistC ('CSum p q) where
  toNetC :: forall x.
EvalC ('CSum p q) x
-> (PosC ('CSum p q), DirC ('CSum p q) -> Maybe x)
toNetC (ESC (Left EvalC p x
u)) =
    let (PosC p
i, DirC p -> Maybe x
f) = EvalC p x -> (PosC p, DirC p -> Maybe x)
forall x. EvalC p x -> (PosC p, DirC p -> Maybe x)
forall (c :: Span) x.
NetlistC c =>
EvalC c x -> (PosC c, DirC c -> Maybe x)
toNetC EvalC p x
u
     in ( PosC p -> Either (PosC p) (PosC q)
forall a b. a -> Either a b
Left PosC p
PosC p
i,
          \case
            Left DirC p
d -> DirC p -> Maybe x
f DirC p
DirC p
d
            Right DirC q
_ -> Maybe x
forall a. Maybe a
Nothing
        )
  toNetC (ESC (Right EvalC q x
v)) =
    let (PosC q
j, DirC q -> Maybe x
g) = EvalC q x -> (PosC q, DirC q -> Maybe x)
forall x. EvalC q x -> (PosC q, DirC q -> Maybe x)
forall (c :: Span) x.
NetlistC c =>
EvalC c x -> (PosC c, DirC c -> Maybe x)
toNetC EvalC q x
v
     in ( PosC q -> Either (PosC p) (PosC q)
forall a b. b -> Either a b
Right PosC q
PosC q
j,
          \case
            Left DirC p
_ -> Maybe x
forall a. Maybe a
Nothing
            Right DirC q
e -> DirC q -> Maybe x
g DirC q
DirC q
e
        )

  fromNetC :: forall x.
PosC ('CSum p q)
-> (DirC ('CSum p q) -> Maybe x) -> EvalC ('CSum p q) x
fromNetC (Left PosC p
i) DirC ('CSum p q) -> Maybe x
h = Either (EvalC p x) (EvalC q x) -> EvalC ('CSum p q) x
forall (p :: Span) x (q :: Span).
Either (EvalC p x) (EvalC q x) -> EvalC ('CSum p q) x
ESC (EvalC p x -> Either (EvalC p x) (EvalC q x)
forall a b. a -> Either a b
Left (PosC p -> (DirC p -> Maybe x) -> EvalC p x
forall x. PosC p -> (DirC p -> Maybe x) -> EvalC p x
forall (c :: Span) x.
NetlistC c =>
PosC c -> (DirC c -> Maybe x) -> EvalC c x
fromNetC PosC p
i (\DirC p
d -> DirC ('CSum p q) -> Maybe x
h (DirC p -> Either (DirC p) (DirC q)
forall a b. a -> Either a b
Left DirC p
d))))
  fromNetC (Right PosC q
j) DirC ('CSum p q) -> Maybe x
h = Either (EvalC p x) (EvalC q x) -> EvalC ('CSum p q) x
forall (p :: Span) x (q :: Span).
Either (EvalC p x) (EvalC q x) -> EvalC ('CSum p q) x
ESC (EvalC q x -> Either (EvalC p x) (EvalC q x)
forall a b. b -> Either a b
Right (PosC q -> (DirC q -> Maybe x) -> EvalC q x
forall x. PosC q -> (DirC q -> Maybe x) -> EvalC q x
forall (c :: Span) x.
NetlistC c =>
PosC c -> (DirC c -> Maybe x) -> EvalC c x
fromNetC PosC q
j (\DirC q
e -> DirC ('CSum p q) -> Maybe x
h (DirC q -> Either (DirC p) (DirC q)
forall a b. b -> Either a b
Right DirC q
e))))

instance
  (NetlistC p, NetlistC q, Eq (PosC p), Eq (PosC q)) =>
  NetlistC ('CProd p q)
  where
  toNetC :: forall x.
EvalC ('CProd p q) x
-> (PosC ('CProd p q), DirC ('CProd p q) -> Maybe x)
toNetC (EPC (EvalC p x
u, EvalC q x
v)) =
    let (PosC p
i, DirC p -> Maybe x
f) = EvalC p x -> (PosC p, DirC p -> Maybe x)
forall x. EvalC p x -> (PosC p, DirC p -> Maybe x)
forall (c :: Span) x.
NetlistC c =>
EvalC c x -> (PosC c, DirC c -> Maybe x)
toNetC EvalC p x
u
        (PosC q
j, DirC q -> Maybe x
g) = EvalC q x -> (PosC q, DirC q -> Maybe x)
forall x. EvalC q x -> (PosC q, DirC q -> Maybe x)
forall (c :: Span) x.
NetlistC c =>
EvalC c x -> (PosC c, DirC c -> Maybe x)
toNetC EvalC q x
v
     in ( (PosC p
PosC p
i, PosC q
PosC q
j),
          \case
            Left (DirC p
d, PosC q
j') -> if PosC q
j' PosC q -> PosC q -> Bool
forall a. Eq a => a -> a -> Bool
== PosC q
PosC q
j then DirC p -> Maybe x
f DirC p
DirC p
d else Maybe x
forall a. Maybe a
Nothing
            Right (PosC p
i', DirC q
e) -> if PosC p
i' PosC p -> PosC p -> Bool
forall a. Eq a => a -> a -> Bool
== PosC p
PosC p
i then DirC q -> Maybe x
g DirC q
DirC q
e else Maybe x
forall a. Maybe a
Nothing
        )

  fromNetC :: forall x.
PosC ('CProd p q)
-> (DirC ('CProd p q) -> Maybe x) -> EvalC ('CProd p q) x
fromNetC (PosC p
i, PosC q
j) DirC ('CProd p q) -> Maybe x
h =
    (EvalC p x, EvalC q x) -> EvalC ('CProd p q) x
forall (p :: Span) x (q :: Span).
(EvalC p x, EvalC q x) -> EvalC ('CProd p q) x
EPC
      ( PosC p -> (DirC p -> Maybe x) -> EvalC p x
forall x. PosC p -> (DirC p -> Maybe x) -> EvalC p x
forall (c :: Span) x.
NetlistC c =>
PosC c -> (DirC c -> Maybe x) -> EvalC c x
fromNetC PosC p
i (\DirC p
d -> DirC ('CProd p q) -> Maybe x
h ((DirC p, PosC q) -> Either (DirC p, PosC q) (PosC p, DirC q)
forall a b. a -> Either a b
Left (DirC p
d, PosC q
j))),
        PosC q -> (DirC q -> Maybe x) -> EvalC q x
forall x. PosC q -> (DirC q -> Maybe x) -> EvalC q x
forall (c :: Span) x.
NetlistC c =>
PosC c -> (DirC c -> Maybe x) -> EvalC c x
fromNetC PosC q
j (\DirC q
e -> DirC ('CProd p q) -> Maybe x
h ((PosC p, DirC q) -> Either (DirC p, PosC q) (PosC p, DirC q)
forall a b. b -> Either a b
Right (PosC p
i, DirC q
e)))
      )

instance NetlistC ('CTensor p q) where
  toNetC :: forall x.
EvalC ('CTensor p q) x
-> (PosC ('CTensor p q), DirC ('CTensor p q) -> Maybe x)
toNetC (ETC PosC p
i PosC q
j DirC p -> DirC q -> x
g) = ((PosC p
PosC p
i, PosC q
PosC q
j), x -> Maybe x
forall a. a -> Maybe a
Just (x -> Maybe x)
-> ((DirC p, DirC q) -> x) -> (DirC p, DirC q) -> Maybe x
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (DirC p -> DirC q -> x) -> (DirC p, DirC q) -> x
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry DirC p -> DirC q -> x
DirC p -> DirC q -> x
g)
  fromNetC :: forall x.
PosC ('CTensor p q)
-> (DirC ('CTensor p q) -> Maybe x) -> EvalC ('CTensor p q) x
fromNetC (PosC p
i, PosC q
j) DirC ('CTensor p q) -> Maybe x
h = PosC p
-> PosC q -> (DirC p -> DirC q -> x) -> EvalC ('CTensor p q) x
forall (p :: Span) (q :: Span) x.
PosC p
-> PosC q -> (DirC p -> DirC q -> x) -> EvalC ('CTensor p q) x
ETC PosC p
i PosC q
j (\DirC p
d DirC q
e -> Maybe x -> x
forall a. Maybe a -> a
expectJust (DirC ('CTensor p q) -> Maybe x
h (DirC p
d, DirC q
e)))

instance NetlistC ('CComp p q) where
  toNetC :: forall x.
EvalC ('CComp p q) x
-> (PosC ('CComp p q), DirC ('CComp p q) -> Maybe x)
toNetC (ECC (PosC p, DirC p -> PosC q)
pos (DirC p, DirC q) -> x
g) = ((PosC p, DirC p -> PosC q)
PosC ('CComp p q)
pos, x -> Maybe x
forall a. a -> Maybe a
Just (x -> Maybe x)
-> ((DirC p, DirC q) -> x) -> (DirC p, DirC q) -> Maybe x
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (DirC p, DirC q) -> x
(DirC p, DirC q) -> x
g)
  fromNetC :: forall x.
PosC ('CComp p q)
-> (DirC ('CComp p q) -> Maybe x) -> EvalC ('CComp p q) x
fromNetC PosC ('CComp p q)
pos DirC ('CComp p q) -> Maybe x
h = (PosC p, DirC p -> PosC q)
-> ((DirC p, DirC q) -> x) -> EvalC ('CComp p q) x
forall (p :: Span) (q :: Span) x.
(PosC p, DirC p -> PosC q)
-> ((DirC p, DirC q) -> x) -> EvalC ('CComp p q) x
ECC (PosC p, DirC p -> PosC q)
PosC ('CComp p q)
pos (\(DirC p, DirC q)
de -> Maybe x -> x
forall a. Maybe a -> a
expectJust (DirC ('CComp p q) -> Maybe x
h (DirC p, DirC q)
DirC ('CComp p q)
de))

-- | Reassemble a value after taking it apart.
--
-- This is the executable form of the round-trip law
-- @'fromNetC' ('toNetC' v) ≡ v@.  It is exact for every constructor.  The
-- reverse direction @'toNetC' ('fromNetC' i h) ≡ (i, h)@ holds exactly when @h@
-- respects the fibre, and fails otherwise.
netRoundTripC :: (NetlistC c) => EvalC c x -> EvalC c x
netRoundTripC :: forall (c :: Span) x. NetlistC c => EvalC c x -> EvalC c x
netRoundTripC EvalC c x
v = (PosC c -> (DirC c -> Maybe x) -> EvalC c x)
-> (PosC c, DirC c -> Maybe x) -> EvalC c x
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry PosC c -> (DirC c -> Maybe x) -> EvalC c x
forall x. PosC c -> (DirC c -> Maybe x) -> EvalC c x
forall (c :: Span) x.
NetlistC c =>
PosC c -> (DirC c -> Maybe x) -> EvalC c x
fromNetC (EvalC c x -> (PosC c, DirC c -> Maybe x)
forall x. EvalC c x -> (PosC c, DirC c -> Maybe x)
forall (c :: Span) x.
NetlistC c =>
EvalC c x -> (PosC c, DirC c -> Maybe x)
toNetC EvalC c x
v)

-- | Test whether a direction lies in the fibre of a given position.
--
-- This is the lowest-dimensional fibre law, equivalent to the Beck–Chevalley
-- condition for the identity cell.
onFibreC :: forall c. (Eq (PosC c), SpanC c) => PosC c -> DirC c -> Bool
onFibreC :: forall (c :: Span).
(Eq (PosC c), SpanC c) =>
PosC c -> DirC c -> Bool
onFibreC PosC c
i DirC c
d = forall (c :: Span). SpanC c => DirC c -> PosC c
projC @c DirC c
d PosC c -> PosC c -> Bool
forall a. Eq a => a -> a -> Bool
== PosC c
i

-- ** Composition product isomorphisms

-- | Composition-product view of a nested span evaluation.
--
-- Correctness iso (right):
-- @'EvalC' p ('EvalC' q x) ≅ 'EvalC' ('CComp' p q) x@.
--
-- This is the span analogue of 'Circuit.Poly.nestedToComp', but it works
-- through the 'Maybe' netlist view.  Off-fibre directions in the outer
-- polynomial have no canonical @q@-position, so the hang map is only
-- defined on the fibre; this is the same cube boundary as the missing 'SpanC'
-- instance for 'CComp'.
nestedToCompC ::
  (NetlistC p, NetlistC q) =>
  EvalC p (EvalC q x) ->
  EvalC ('CComp p q) x
nestedToCompC :: forall (p :: Span) (q :: Span) x.
(NetlistC p, NetlistC q) =>
EvalC p (EvalC q x) -> EvalC ('CComp p q) x
nestedToCompC EvalC p (EvalC q x)
v =
  let (PosC p
i, DirC p -> Maybe (EvalC q x)
g) = EvalC p (EvalC q x) -> (PosC p, DirC p -> Maybe (EvalC q x))
forall x. EvalC p x -> (PosC p, DirC p -> Maybe x)
forall (c :: Span) x.
NetlistC c =>
EvalC c x -> (PosC c, DirC c -> Maybe x)
toNetC EvalC p (EvalC q x)
v
      cell :: DirC p -> (PosC q, DirC q -> Maybe x)
cell DirC p
dp = EvalC q x -> (PosC q, DirC q -> Maybe x)
forall x. EvalC q x -> (PosC q, DirC q -> Maybe x)
forall (c :: Span) x.
NetlistC c =>
EvalC c x -> (PosC c, DirC c -> Maybe x)
toNetC (Maybe (EvalC q x) -> EvalC q x
forall a. Maybe a -> a
expectJust (DirC p -> Maybe (EvalC q x)
g DirC p
dp))
      hang :: DirC p -> PosC q
hang DirC p
dp = (PosC q, DirC q -> Maybe x) -> PosC q
forall a b. (a, b) -> a
fst (DirC p -> (PosC q, DirC q -> Maybe x)
cell DirC p
dp)
   in (PosC p, DirC p -> PosC q)
-> ((DirC p, DirC q) -> x) -> EvalC ('CComp p q) x
forall (p :: Span) (q :: Span) x.
(PosC p, DirC p -> PosC q)
-> ((DirC p, DirC q) -> x) -> EvalC ('CComp p q) x
ECC (PosC p
i, DirC p -> PosC q
hang) (\(DirC p
dp, DirC q
dq) -> Maybe x -> x
forall a. Maybe a -> a
expectJust ((PosC q, DirC q -> Maybe x) -> DirC q -> Maybe x
forall a b. (a, b) -> b
snd (DirC p -> (PosC q, DirC q -> Maybe x)
cell DirC p
dp) DirC q
dq))

-- | Nested span evaluation from a composition-product value.
--
-- Correctness iso (left): inverse of 'nestedToCompC'.
compToNestedC ::
  (NetlistC p, NetlistC q) =>
  EvalC ('CComp p q) x ->
  EvalC p (EvalC q x)
compToNestedC :: forall (p :: Span) (q :: Span) x.
(NetlistC p, NetlistC q) =>
EvalC ('CComp p q) x -> EvalC p (EvalC q x)
compToNestedC (ECC (PosC p
i, DirC p -> PosC q
hang) (DirC p, DirC q) -> x
k) =
  PosC p -> (DirC p -> Maybe (EvalC q x)) -> EvalC p (EvalC q x)
forall x. PosC p -> (DirC p -> Maybe x) -> EvalC p x
forall (c :: Span) x.
NetlistC c =>
PosC c -> (DirC c -> Maybe x) -> EvalC c x
fromNetC PosC p
PosC p
i (\DirC p
dp -> EvalC q x -> Maybe (EvalC q x)
forall a. a -> Maybe a
Just (PosC q -> (DirC q -> Maybe x) -> EvalC q x
forall x. PosC q -> (DirC q -> Maybe x) -> EvalC q x
forall (c :: Span) x.
NetlistC c =>
PosC c -> (DirC c -> Maybe x) -> EvalC c x
fromNetC (DirC p -> PosC q
hang DirC p
DirC p
dp) (\DirC q
dq -> x -> Maybe x
forall a. a -> Maybe a
Just ((DirC p, DirC q) -> x
k (DirC p
DirC p
dp, DirC q
DirC q
dq)))))

-- | Left associator for the composition product:
-- @((p ◁ q) ◁ r) -> (p ◁ (q ◁ r))@.
compAssocLC ::
  EvalC ('CComp ('CComp p q) r) x ->
  EvalC ('CComp p ('CComp q r)) x
compAssocLC :: forall (p :: Span) (q :: Span) (r :: Span) x.
EvalC ('CComp ('CComp p q) r) x -> EvalC ('CComp p ('CComp q r)) x
compAssocLC (ECC ((PosC p
i, DirC p -> PosC q
f), DirC p -> PosC q
g) (DirC p, DirC q) -> x
k) =
  (PosC p, DirC p -> PosC ('CComp q r))
-> ((DirC p, DirC ('CComp q r)) -> x)
-> EvalC ('CComp p ('CComp q r)) x
forall (p :: Span) (q :: Span) x.
(PosC p, DirC p -> PosC q)
-> ((DirC p, DirC q) -> x) -> EvalC ('CComp p q) x
ECC
    ( PosC p
i,
      \DirC p
dp ->
        let j :: PosC q
j = DirC p -> PosC q
f DirC p
dp
            h :: DirC q -> PosC q
h DirC q
dq = DirC p -> PosC q
g (DirC p
dp, DirC q
dq)
         in (PosC q
j, DirC q -> PosC r
DirC q -> PosC q
h)
    )
    (\(DirC p
dp, (DirC q
dq, DirC r
dr)) -> (DirC p, DirC q) -> x
k ((DirC p
dp, DirC q
dq), DirC r
DirC q
dr))

-- | Right associator for the composition product.
compAssocRC ::
  EvalC ('CComp p ('CComp q r)) x ->
  EvalC ('CComp ('CComp p q) r) x
compAssocRC :: forall (p :: Span) (q :: Span) (r :: Span) x.
EvalC ('CComp p ('CComp q r)) x -> EvalC ('CComp ('CComp p q) r) x
compAssocRC (ECC (PosC p
i, DirC p -> PosC q
h) (DirC p, DirC q) -> x
k) =
  let f :: DirC p -> PosC q
f DirC p
dp = (PosC q, DirC q -> PosC r) -> PosC q
forall a b. (a, b) -> a
fst (DirC p -> PosC q
h DirC p
DirC p
dp)
      g :: (DirC p, DirC q) -> PosC r
g (DirC p
dp, DirC q
dq) = (PosC q, DirC q -> PosC r) -> DirC q -> PosC r
forall a b. (a, b) -> b
snd (DirC p -> PosC q
h DirC p
DirC p
dp) DirC q
dq
   in (PosC ('CComp p q), DirC ('CComp p q) -> PosC r)
-> ((DirC ('CComp p q), DirC r) -> x)
-> EvalC ('CComp ('CComp p q) r) x
forall (p :: Span) (q :: Span) x.
(PosC p, DirC p -> PosC q)
-> ((DirC p, DirC q) -> x) -> EvalC ('CComp p q) x
ECC ((PosC p
PosC p
i, DirC p -> PosC q
f), (DirC p, DirC q) -> PosC r
DirC ('CComp p q) -> PosC r
g) (\((DirC p
dp, DirC q
dq), DirC r
dr) -> (DirC p, DirC q) -> x
k (DirC p
DirC p
dp, (DirC q
dq, DirC r
dr)))

-- ** Sum / product distributivity

-- | Left distributivity of 'CProd' over 'CSum':
-- @'CProd' ('CSum' p q) r -> 'CSum' ('CProd' p r) ('CProd' q r)@.
prodSumDistrLC ::
  EvalC ('CProd ('CSum p q) r) x ->
  EvalC ('CSum ('CProd p r) ('CProd q r)) x
prodSumDistrLC :: forall (p :: Span) (q :: Span) (r :: Span) x.
EvalC ('CProd ('CSum p q) r) x
-> EvalC ('CSum ('CProd p r) ('CProd q r)) x
prodSumDistrLC (EPC (ESC (Left EvalC p x
u), EvalC q x
w)) = Either (EvalC ('CProd p r) x) (EvalC ('CProd q r) x)
-> EvalC ('CSum ('CProd p r) ('CProd q r)) x
forall (p :: Span) x (q :: Span).
Either (EvalC p x) (EvalC q x) -> EvalC ('CSum p q) x
ESC (EvalC ('CProd p r) x
-> Either (EvalC ('CProd p r) x) (EvalC ('CProd q r) x)
forall a b. a -> Either a b
Left ((EvalC p x, EvalC r x) -> EvalC ('CProd p r) x
forall (p :: Span) x (q :: Span).
(EvalC p x, EvalC q x) -> EvalC ('CProd p q) x
EPC (EvalC p x
EvalC p x
u, EvalC r x
EvalC q x
w)))
prodSumDistrLC (EPC (ESC (Right EvalC q x
v), EvalC q x
w)) = Either (EvalC ('CProd p r) x) (EvalC ('CProd q r) x)
-> EvalC ('CSum ('CProd p r) ('CProd q r)) x
forall (p :: Span) x (q :: Span).
Either (EvalC p x) (EvalC q x) -> EvalC ('CSum p q) x
ESC (EvalC ('CProd q r) x
-> Either (EvalC ('CProd p r) x) (EvalC ('CProd q r) x)
forall a b. b -> Either a b
Right ((EvalC q x, EvalC r x) -> EvalC ('CProd q r) x
forall (p :: Span) x (q :: Span).
(EvalC p x, EvalC q x) -> EvalC ('CProd p q) x
EPC (EvalC q x
EvalC q x
v, EvalC r x
EvalC q x
w)))

-- | Right distributivity of 'CProd' over 'CSum':
-- @'CSum' ('CProd' p r) ('CProd q r) -> 'CProd' ('CSum' p q) r@.
prodSumDistrRC ::
  EvalC ('CSum ('CProd p r) ('CProd q r)) x ->
  EvalC ('CProd ('CSum p q) r) x
prodSumDistrRC :: forall (p :: Span) (r :: Span) (q :: Span) x.
EvalC ('CSum ('CProd p r) ('CProd q r)) x
-> EvalC ('CProd ('CSum p q) r) x
prodSumDistrRC (ESC (Left (EPC (EvalC p x
u, EvalC q x
w)))) = (EvalC ('CSum p q) x, EvalC r x) -> EvalC ('CProd ('CSum p q) r) x
forall (p :: Span) x (q :: Span).
(EvalC p x, EvalC q x) -> EvalC ('CProd p q) x
EPC (Either (EvalC p x) (EvalC q x) -> EvalC ('CSum p q) x
forall (p :: Span) x (q :: Span).
Either (EvalC p x) (EvalC q x) -> EvalC ('CSum p q) x
ESC (EvalC p x -> Either (EvalC p x) (EvalC q x)
forall a b. a -> Either a b
Left EvalC p x
EvalC p x
u), EvalC r x
EvalC q x
w)
prodSumDistrRC (ESC (Right (EPC (EvalC p x
v, EvalC q x
w)))) = (EvalC ('CSum p q) x, EvalC r x) -> EvalC ('CProd ('CSum p q) r) x
forall (p :: Span) x (q :: Span).
(EvalC p x, EvalC q x) -> EvalC ('CProd p q) x
EPC (Either (EvalC p x) (EvalC q x) -> EvalC ('CSum p q) x
forall (p :: Span) x (q :: Span).
Either (EvalC p x) (EvalC q x) -> EvalC ('CSum p q) x
ESC (EvalC q x -> Either (EvalC p x) (EvalC q x)
forall a b. b -> Either a b
Right EvalC q x
EvalC p x
v), EvalC r x
EvalC q x
w)

-- | Position isomorphism for the left distributivity of 'CProd' over 'CSum'.
distrPosLC ::
  PosC ('CProd ('CSum p q) r) ->
  PosC ('CSum ('CProd p r) ('CProd q r))
distrPosLC :: forall (p :: Span) (q :: Span) (r :: Span).
PosC ('CProd ('CSum p q) r)
-> PosC ('CSum ('CProd p r) ('CProd q r))
distrPosLC (Left PosC p
i, PosC r
j) = (PosC p, PosC r) -> Either (PosC p, PosC r) (PosC q, PosC r)
forall a b. a -> Either a b
Left (PosC p
i, PosC r
j)
distrPosLC (Right PosC q
k, PosC r
j) = (PosC q, PosC r) -> Either (PosC p, PosC r) (PosC q, PosC r)
forall a b. b -> Either a b
Right (PosC q
k, PosC r
j)

-- | Direction isomorphism for the left distributivity of 'CProd' over 'CSum'.
distrDirLC ::
  DirC ('CProd ('CSum p q) r) ->
  DirC ('CSum ('CProd p r) ('CProd q r))
distrDirLC :: forall (p :: Span) (q :: Span) (r :: Span).
DirC ('CProd ('CSum p q) r)
-> DirC ('CSum ('CProd p r) ('CProd q r))
distrDirLC = \case
  Left (Left DirC p
dp, PosC r
j) -> Either (DirC p, PosC r) (PosC p, DirC r)
-> Either
     (Either (DirC p, PosC r) (PosC p, DirC r))
     (Either (DirC q, PosC r) (PosC q, DirC r))
forall a b. a -> Either a b
Left ((DirC p, PosC r) -> Either (DirC p, PosC r) (PosC p, DirC r)
forall a b. a -> Either a b
Left (DirC p
dp, PosC r
j))
  Left (Right DirC q
dq, PosC r
j) -> Either (DirC q, PosC r) (PosC q, DirC r)
-> Either
     (Either (DirC p, PosC r) (PosC p, DirC r))
     (Either (DirC q, PosC r) (PosC q, DirC r))
forall a b. b -> Either a b
Right ((DirC q, PosC r) -> Either (DirC q, PosC r) (PosC q, DirC r)
forall a b. a -> Either a b
Left (DirC q
dq, PosC r
j))
  Right (Left PosC p
i, DirC r
e) -> Either (DirC p, PosC r) (PosC p, DirC r)
-> Either
     (Either (DirC p, PosC r) (PosC p, DirC r))
     (Either (DirC q, PosC r) (PosC q, DirC r))
forall a b. a -> Either a b
Left ((PosC p, DirC r) -> Either (DirC p, PosC r) (PosC p, DirC r)
forall a b. b -> Either a b
Right (PosC p
i, DirC r
e))
  Right (Right PosC q
k, DirC r
e) -> Either (DirC q, PosC r) (PosC q, DirC r)
-> Either
     (Either (DirC p, PosC r) (PosC p, DirC r))
     (Either (DirC q, PosC r) (PosC q, DirC r))
forall a b. b -> Either a b
Right ((PosC q, DirC r) -> Either (DirC q, PosC r) (PosC q, DirC r)
forall a b. b -> Either a b
Right (PosC q
k, DirC r
e))