Control.Monad.Distribution

Reexports

Definitions

record Dist : Axis -> Type

  Convex combination of a finite set of types, a point in a simplex △^(i-1)
  i=2 -> △¹ -> line segment
  i=3 -> △² -> triangle
  ...
  Probabilities are represented as logits, represented as a rank 1 tensor.
  Because the tensor has a name, and `Dist` is a thin wrapper around it,
  the name is exposed at the type level, allowing named operations to be
  extended to distributions
  TODO change description, as now `Dist` involves containers
  TODO, is Dist a quotient container?

Totality: total
Visibility: public export
Constructor: 

MkDist : Tensor [a] Double -> Dist a

Projection: 

.logits : Dist a -> Tensor [a] Double

  Probabilities are represented as logits

Hints:

AllDisplay2D [a] Double => IsFoldable (a .cont) => AllAlgebra [a] Double => TensorCubEvidence [a] => Display2D (Dist a)

AllDisplay2D [a] Double => IsFoldable (a .cont) => AllAlgebra [a] Double => TensorCubEvidence [a] => Show (Dist a)

.logits : Dist a -> Tensor [a] Double

  Probabilities are represented as logits

Totality: total
Visibility: public export

logits : Dist a -> Tensor [a] Double

  Probabilities are represented as logits

Totality: total
Visibility: public export

uniform : (a .cont) .Shp -> Dist a

  Logit representation of the uniform distribution
  Is defined for a container once the choice of shape is made

Totality: total
Visibility: public export

diracDelta : IsDecidable (a .cont) => (s : (a .cont) .Shp) -> (a .cont) .Pos s -> Dist a

  Logit representation of dirac delta at the position `p` of the shape `s`
  Note that `0` is the canonical choice, as softargmax subtracts the max

Totality: total
Visibility: public export

uniform : IsNaperian a => Dist a

Totality: total
Visibility: public export

diracDelta : {auto {conArg:10177} : IsNaperian a} -> DecEq (Log a) => Log a -> Dist a

Totality: total
Visibility: public export

Dist : Axis -> Cont

  Container whose choice of a shape is a distribution over some choices, 
  and a position is a specific choice made.

Totality: total
Visibility: public export

uniformLens : a .cont =%> Dist a

Totality: total
Visibility: public export

Simplex : Axis -> AddCont

  Container whose shapes are distributions (over positions over some chosen
  container shape), and positions are their gradients.
  Both are represented as logits
  If we were treating this as non-logit distributions then we'd have a
  one less dimension: both for the simplex in the forward pass and the
  gradients in the backwards one
  That is, the effective dimension of this space is n-1 (we can add a
  constant to all logits without changing the answer), and there's a
  direction in the gradient logit space that does not affect output

Totality: total
Visibility: public export

ProbabilisticChoice : (a : Axis) -> (a .cont) .filledWith AddCont -> AddCont

  A distribution over a container of branches, together with answers ready 
  when any branch is chosen, computed only when the branch is asked for
  TODO do we think of distr. on the fw pass as being part of Simplex or Nap?

Totality: total
Visibility: public export

pendingChoice : (branches : (a .cont) .filledWith AddCont) -> ProbabilisticChoice a branches =%+> (Dist a >-+@ AddContDPair (index branches))

  Each probabilistic choice can be turned into a sequence of producing a 
  distribution, waiting for the response from the environment about which 
  choice to make, then making that choice

Totality: total
Visibility: public export