Safe Haskell	None
Language	GHC2024

Circuit.Diff.Evidence

Contents

Evidence-carrying channel
Concrete channels
Wrappers for knot bodies

Description

Star-elimination evidence as a channel type.

The insight is that star-elimination structure is data carried on a wire, not wiring itself. circuits keeps yank free of evidence; 'circuits-diff' instead uses a channel whose values carry their own elimination dictionary.

A StarChannel s is both the feedback state (the s field) and the dictionary needed to solve affine feedback equations over that state. The dictionary part of the value is carried through the trace unchanged; the data part is updated by the knot body.

Synopsis

data StarChannel s = StarChannel {
- starDim :: Int
- starData :: s
- starZero :: Int -> s
- starBasis :: Int -> Int -> s
- starAdd :: s -> s -> s
- starNegate :: s -> s
- starSelfMatrix :: Int -> (s -> s) -> Matrix (Scalar s)
- starApplyMatrix :: Matrix (Scalar s) -> s -> s
- starMatrix :: Matrix (Scalar s) -> Matrix (Scalar s)
}
type family Scalar s
fieldStarChannel :: StarChannel FieldStar
listStarChannel :: (StarSemiring a, Subtractive a) => Int -> StarChannel [a]
withStarChannel :: StarChannel s -> Pullback (s, b) (s, c) -> Pullback (StarChannel s, b) (StarChannel s, c)
withStarChannelDiff :: forall {k} s (p :: k) b c. StarChannel s -> Diff p (s, b) (s, c) -> Diff p (StarChannel s, b) (StarChannel s, c)

Evidence-carrying channel

data StarChannel s Source #

A feedback channel that carries its own star-elimination dictionary.

The matrix carrier is fixed by the Scalar type family so that circuits-diff (which already depends on circuits-mat) can use dense matrices directly, while circuits remains ignorant of matrices.

A value bundles the current feedback state (starData) with the operations needed to eliminate a self-coupled affine knot over that state. The dictionary fields are expected to be preserved by a knot body; withStarChannel and withStarChannelDiff are the canonical ways to build such bodies.

Constructors

StarChannel

Fields

starDim :: Int
Dimension of the channel cotangent space.
starData :: s
Current feedback state.
starZero :: Int -> s
Zero channel cotangent of the given dimension.
starBasis :: Int -> Int -> s
Basis vector e_i: starBasis dim i.
starAdd :: s -> s -> s
Componentwise sum of two channel cotangents.
starNegate :: s -> s
Additive inverse of a channel cotangent.
starSelfMatrix :: Int -> (s -> s) -> Matrix (Scalar s)
Build the self-coupling matrix of a linear map s -> s by probing each basis vector of the given dimension.
starApplyMatrix :: Matrix (Scalar s) -> s -> s
Apply a matrix to a channel cotangent.
starMatrix :: Matrix (Scalar s) -> Matrix (Scalar s)
Kleene star of a square self-coupling matrix.

type family Scalar s Source #

Scalar carrier associated with a star-channel state type.

For scalar channels the scalar is the state itself; for list channels it is the list element type.

Instances

Instances details

type Scalar FieldStar Source #
Instance details Defined in Circuit.Diff.Evidence type Scalar FieldStar = FieldStar
type Scalar [a] Source #
Instance details Defined in Circuit.Diff.Evidence type Scalar [a] = a

Concrete channels

fieldStarChannel :: StarChannel FieldStar Source #

Evidence for a one-dimensional FieldStar channel.

The matrix carrier is Matrix FieldStar — a 1×1 matrix whose single element is the scalar channel cotangent.

listStarChannel :: (StarSemiring a, Subtractive a) => Int -> StarChannel [a] Source #

Evidence for an n-dimensional list channel.

The matrix carrier is Matrix a; the channel cotangent is [a].

Wrappers for knot bodies

withStarChannel :: StarChannel s -> Pullback (s, b) (s, c) -> Pullback (StarChannel s, b) (StarChannel s, c) Source #

Wrap a pullback computation on the underlying channel s into a computation on StarChannel s.

The supplied dict provides the elimination dictionary; the body only needs to update starData. The output value reuses dict's dictionary fields, so solveStarBody can read them directly from the exposed channel type.

withStarChannelDiff :: forall {k} s (p :: k) b c. StarChannel s -> Diff p (s, b) (s, c) -> Diff p (StarChannel s, b) (StarChannel s, c) Source #

Wrap a Diff computation on the underlying channel s into a computation on StarChannel s.

This is the forward-differentiable analogue of withStarChannel: the forward pass threads the StarChannel state, and the backward pass threads its cotangent through the same dictionary.