| Safe Haskell | None |
|---|---|
| Language | GHC2024 |
Circuit.Inference.Prob
Description
Effectful probability row: Prob (K m) r.
The function-arrow instances in Circuit.Prob are the reference semantics.
This module ports the cartesian and cocartesian structural instances to the
K base arrow, which is the substrate for sampling-based inference.
The tensor remains premonoidal: the two nestings parFGK and parGFK agree
on distribution but differ operationally when effects do not commute.
Synopsis
- newtype Prob (arr :: Type -> k -> Type) (r :: k) a b = Prob {
- runProb :: forall x. arr (x, b) r -> arr (x, a) r
- embedK :: forall {k} a b (m :: k -> Type) (r :: k). (a -> b) -> Prob (K m) r a b
- fromWeightedK :: forall r (m :: Type -> Type) b. (Num r, Monad m) => [(b, r)] -> Prob (K m) r () b
- scoreK :: forall (m :: Type -> Type) r a. Monad m => (r -> r) -> Prob (K m) r a a
- massK :: Monad m => r -> Prob (K m) r a b -> a -> m r
- copyPK :: forall {k} (m :: k -> Type) (r :: k) a. Prob (K m) r a (a, a)
- discardPK :: forall {k} (m :: k -> Type) (r :: k) a. Prob (K m) r a ()
- choiceByK :: forall (m :: Type -> Type) r a b. Monad m => (r -> r -> r) -> Prob (K m) r a b -> Prob (K m) r a b -> Prob (K m) r a b
- orPK :: forall (m :: Type -> Type) a b. Monad m => Prob (K m) Bool a b -> Prob (K m) Bool a b -> Prob (K m) Bool a b
- parFGK :: forall {k} (m :: k -> Type) (r :: k) a b c d. Prob (K m) r a b -> Prob (K m) r c d -> Prob (K m) r (a, c) (b, d)
- parGFK :: forall {k} (m :: k -> Type) (r :: k) a b c d. Prob (K m) r a b -> Prob (K m) r c d -> Prob (K m) r (a, c) (b, d)
- traceEK :: forall {k} (m :: k -> Type) (r :: k) a s b. Prob (K m) r (Either a s) (Either b s) -> Prob (K m) r a b
- traceENK :: forall (m :: Type -> Type) r a s b. Monad m => r -> Int -> Prob (K m) r (Either a s) (Either b s) -> Prob (K m) r a b
Re-export base type
newtype Prob (arr :: Type -> k -> Type) (r :: k) a b #
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
| Monad m => Channel Either (Prob (K m) r :: Type -> Type -> Type) Source # | |
| Monad m => Channel (,) (Prob (K m) r :: Type -> Type -> Type) Source # | |
| Channel (,) (Prob (->) r :: Type -> Type -> Type) # | The cartesian structural morphisms are deterministic, so they are just
|
| Monad m => Strength Either (Prob (K m) r :: Type -> Type -> Type) Source # | |
| Monad m => Strength (,) (Prob (K m) r :: Type -> Type -> Type) Source # | |
| Strength (,) (Prob (->) r :: Type -> Type -> Type) # | |
Defined in Circuit.Prob | |
| Unital (,) (Prob (->) r :: Type -> Type -> Type) # | The cartesian unitors are deterministic, so they embed cleanly. This is
why the |
| Category arr => Category (Prob arr r :: Type -> Type -> Type) # | Identity and composition are arrow-polymorphic: they only manipulate the
continuation function, never the base arrow. This is why |
K primitives
embedK :: forall {k} a b (m :: k -> Type) (r :: k). (a -> b) -> Prob (K m) r a b Source #
Lift a pure function into an effectful probability morphism.
fromWeightedK :: forall r (m :: Type -> Type) b. (Num r, Monad m) => [(b, r)] -> Prob (K m) r () b Source #
Build a probability morphism from a finite weighted table.
scoreK :: forall (m :: Type -> Type) r a. Monad m => (r -> r) -> Prob (K m) r a a Source #
Scale the result of a continuation.
massK :: Monad m => r -> Prob (K m) r a b -> a -> m r Source #
Compute the total mass of an unnormalised morphism against the unit continuation.
discardPK :: forall {k} (m :: k -> Type) (r :: k) a. Prob (K m) r a () Source #
Deterministic discard.
choiceByK :: forall (m :: Type -> Type) r a b. Monad m => (r -> r -> r) -> Prob (K m) r a b -> Prob (K m) r a b -> Prob (K m) r a b Source #
Binary choice combined by a scalar operation.
orPK :: forall (m :: Type -> Type) a b. Monad m => Prob (K m) Bool a b -> Prob (K m) Bool a b -> Prob (K m) Bool a b Source #
Angelic choice for r = Bool.
Parallel nestings (premonoidal)
parFGK :: forall {k} (m :: k -> Type) (r :: k) a b c d. Prob (K m) r a b -> Prob (K m) r c d -> Prob (K m) r (a, c) (b, d) Source #
Parallel composition: g runs at context (x, b), f runs at context
(x, c). One of two lawful nestings; operationally distinct from parGFK
when the underlying monad has ordered effects.
parGFK :: forall {k} (m :: k -> Type) (r :: k) a b c d. Prob (K m) r a b -> Prob (K m) r c d -> Prob (K m) 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 parFGK on distribution for the
linear fragment, but differs operationally on ordered effects.
Traced Either over effectful base arrows
traceEK :: forall {k} (m :: k -> Type) (r :: k) a s b. Prob (K m) r (Either a s) (Either b s) -> Prob (K m) r a b Source #
Least-fixpoint trace over the Either tensor for K m.
Recursive re-entries are productive because each recursive call is an
effectful action in m. For almost-surely terminating bodies (e.g. a
geometric sampler) the trace returns a sample rather than diverging.
traceENK :: forall (m :: Type -> Type) r a s b. Monad m => r -> Int -> Prob (K m) r (Either a s) (Either b s) -> Prob (K m) r a b Source #
Fuel-bounded variant of traceEK.