| Safe Haskell | None |
|---|---|
| Language | GHC2024 |
Circuit.Prob
Description
Probability as a double-dual continuation category.
A morphism Prob arr r a b is an expectation transformer: it turns a
continuation arr (x, b) r (a "test" on the output) into a continuation
arr (x, a) r (a test on the input). The rank-2 quantification over x
is the cost of arrow-polymorphism — the same move used by Poles.
This is the categorical substrate for probability, conditioning, and
verification: choosing the dualizing object r picks the semantics.
r = Log Doubleover(->)gives expectation transformers / measures.r = Boolover(->)gives Dijkstra's weakest-precondition semantics.r = Min Double(tropical) gives Bellman Viterbi MAP semantics.
This module currently provides structural instances for the function arrow
(->). Effectful variants (e.g. Kleisli m) follow the same pattern but
need scalar-lifting plumbing; the function case is where the design is
easiest to validate.
The tensor action on Prob is premonoidal in general: two valid nestings
(parFG and parGF) agree only on the linear (commutative) fragment. We
therefore do not provide a canonical Tensor instance; use
the explicit nesting you mean.
Synopsis
- newtype Prob (arr :: Type -> k -> Type) (r :: k) a b = Prob {
- runProb :: forall x. arr (x, b) r -> arr (x, a) r
- embed :: (a -> b) -> Prob (->) r a b
- fromWeighted :: Semiring r => [(b, r)] -> Prob (->) r () b
- score :: (r -> r) -> Prob (->) r a a
- mass :: Semiring r => Prob (->) r a b -> a -> r
- copyP :: Prob (->) r a (a, a)
- discardP :: Prob (->) r a ()
- choiceBy :: (r -> r -> r) -> Prob (->) r a b -> Prob (->) r a b -> Prob (->) r a b
- orP :: Prob (->) Bool a b -> Prob (->) Bool a b -> Prob (->) Bool a b
- parFG :: Prob (->) r a b -> Prob (->) r c d -> Prob (->) r (a, c) (b, d)
- parGF :: Prob (->) r a b -> Prob (->) r c d -> Prob (->) r (a, c) (b, d)
- traceE :: Prob (->) r (Either a s) (Either b s) -> Prob (->) r a b
- traceEN :: r -> Int -> Prob (->) r (Either a s) (Either b s) -> Prob (->) r a b
- class Semiring r where
- newtype Tropical = Tropical {}
Double-dual probability arrow
newtype Prob (arr :: Type -> k -> Type) (r :: k) a b Source #
Double-dual embedding of arr with respect to dualizing object r.
A value Prob arr r a b reads an output-continuation arr (x, b) r and
produces an input-continuation arr (x, a) r. Composition is continuation
composition (contravariant in the middle type).
Instances
| Channel (,) (Prob (->) r :: Type -> Type -> Type) Source # | The cartesian structural morphisms are deterministic, so they are just
|
| Strength (,) (Prob (->) r :: Type -> Type -> Type) Source # | |
Defined in Circuit.Prob | |
| Unital (,) (Prob (->) r :: Type -> Type -> Type) Source # | The cartesian unitors are deterministic, so they embed cleanly. This is
why the |
| Category arr => Category (Prob arr r :: Type -> Type -> Type) Source # | Identity and composition are arrow-polymorphic: they only manipulate the
continuation function, never the base arrow. This is why |
Primitive constructors
embed :: (a -> b) -> Prob (->) r a b Source #
Embed a deterministic function as a probability morphism.
The continuation is applied to the transformed output, with the context wire carried along unchanged.
fromWeighted :: Semiring r => [(b, r)] -> Prob (->) r () b Source #
Build a probability morphism from a finite weighted table.
This is the bridge to Weighted and the entry point for
genuine measures in the linear fragment: every entry contributes linearly
to the expectation.
score :: (r -> r) -> Prob (->) r a a Source #
Scale the result of a continuation.
With endomorphisms r -> r this is a modality, not necessarily a scalar
multiplication. The definitional law is the anti-homomorphism
score w . score v = score (v . w); commutativity holds only when the
endos commute. For the probabilistic sub-case score (w *), the usual
multiplicative law is recovered.
mass :: Semiring r => Prob (->) r a b -> a -> r Source #
Compute the total mass of an unnormalised morphism against the unit continuation.
Cartesian copy/discard (deterministic)
copyP :: Prob (->) r a (a, a) Source #
Deterministic copy. Naturality of this morphism characterises the
deterministic fragment: copyP . embed h == parFG (embed h) (embed h) . copyP.
discardP :: Prob (->) r a () Source #
Deterministic discard. On the mass-1 fragment f . discardP == discardP;
unnormalised morphisms fail this equation.
Choice combined by a scalar operation
choiceBy :: (r -> r -> r) -> Prob (->) r a b -> Prob (->) r a b -> Prob (->) r a b Source #
Binary choice combined by a scalar operation. This one combinator covers several rows of the instance table:
choiceBy (||)— angelic / reachability (Bool).choiceBy (&&)— demonic / refutation (Bool).choiceBy (+)— sum of weighted alternatives (Num r).choiceBy min— tropical / Viterbi choice (Ord r).
orP :: Prob (->) Bool a b -> Prob (->) Bool a b -> Prob (->) Bool a b Source #
Angelic choice for r = Bool (weakest-precondition / reachability
semantics). Succeeds if either branch can; short-circuiting of (||)
gives the trace on this scalar for free.
Parallel nestings (Fubini on the linear fragment)
parFG :: Prob (->) r a b -> Prob (->) r c d -> Prob (->) r (a, c) (b, d) Source #
Parallel composition: g runs at context (x, b), f runs at context
(x, c). This is one of two lawful nestings; it agrees with parGF on
the linear/commutative fragment.
parGF :: Prob (->) r a b -> Prob (->) r c d -> Prob (->) r (a, c) (b, d) Source #
Parallel composition: f runs at context (x, d), g runs at context
(x, a). The other nesting; agrees with parFG on the linear fragment.
Traced Either (explicit, computability varies by scalar)
traceE :: Prob (->) r (Either a s) (Either b s) -> Prob (->) r a b Source #
Least-fixpoint trace over the Either tensor.
This is the denotationally correct definition: Right values feed back into
the body, Left values escape. For genuinely cyclic bodies and strict
numeric scalars (e.g. r = Double) it diverges — the geometric series
exists but strict (+) never reaches it. Use traceEN for a computable
approximation, or switch to a scalar whose lattice structure supplies the
fixpoint (e.g. r = Bool, where (||) short-circuits) or to an effectful
base arrow where sampling terminates almost surely.
We do not provide a Traced Either (Prob (->) r) instance because the
canonical trace is only available on a fragment; traceE and traceEN are
exported as explicit choices.
traceEN :: r -> Int -> Prob (->) r (Either a s) (Either b s) -> Prob (->) r a b Source #
Fuel-bounded variant of traceE. After the fuel is exhausted, re-entries
contribute the supplied zero value. This converges to the least fixpoint
with error proportional to the probability of not having terminated by the
fuel limit.
Semiring scalars
class Semiring r where Source #
A semiring: an additive monoid and a multiplicative monoid, with multiplication distributing over addition.
This class is intentionally minimal. It captures the scalar structure
needed by Prob without pulling in a full numeric prelude.
Methods
Min-plus tropical semiring over Double.
Addition is min, multiplication is ordinary addition, the additive unit
is positive infinity, and the multiplicative unit is zero.
Constructors
| Tropical | |
Fields | |