Language.Hakaru.Evaluation.PEvalMonad

A unified EvaluationMonad for pure evaluation, expect, and disintegrate.

The unified PEval monad

List-based version

data ListContext abt p

An ordered collection of statements representing the context surrounding the current focus of our program transformation. That is, since some transformations work from the bottom up, we need to keep track of the statements we passed along the way when reaching for the bottom.

The tail of the list takes scope over the head of the list. Thus, the back/end of the list is towards the top of the program, whereas the front of the list is towards the bottom.

This type was formerly called Heap (presumably due to the Statement type being called Binding) but that seems like a misnomer to me since this really has nothing to do with allocation. However, it is still like a heap inasmuch as it's a dependency graph and we may wish to change the topological sorting or remove "garbage" (subject to correctness criteria).

TODO: Figure out what to do with SWeight, SGuard, SStuff, etc, so that we can use an IntMap (Statement abt) in order to speed up the lookup times in select. (Assuming callers don't use unsafePush unsafely: we can recover the order things were inserted from their varID since we've freshened them all and therefore their IDs are monotonic in the insertion order.)

Constructors

ListContext

Fields

• nextFreshNat :: !Nat
• statements :: [Statement abt Location p]

type PAns p abt m a = ListContext abt p -> m (P p abt '[] a)

newtype PEval abt p m x

TODO: give this a better, more informative name!

Constructors

PEval

Fields

• unPEval :: forall a. (x -> PAns p abt m a) -> PAns p abt m a

Instances

ABT Hakaru Term abt => EvaluationMonad abt (PEval abt p m) p

Methods

freshNat :: PEval abt p m Nat

freshLocStatement :: Statement abt (Variable Hakaru) p -> PEval abt p m (Statement abt (Location Hakaru) p, Assocs Hakaru (Variable Hakaru))

getIndices :: PEval abt p m [Index (abt [Hakaru])]

unsafePush :: Statement abt (Location Hakaru) p -> PEval abt p m ()

unsafePushes :: [Statement abt (Location Hakaru) p] -> PEval abt p m ()

select :: Location Hakaru a -> (Statement abt (Location Hakaru) p -> Maybe (PEval abt p m r)) -> PEval abt p m (Maybe r)

substVar :: Variable Hakaru a -> abt [Hakaru] a -> forall b'. Variable Hakaru b' -> PEval abt p m (abt [Hakaru] b')

extFreeVars :: abt xs a -> PEval abt p m (VarSet Hakaru (KindOf Hakaru a))

evaluateCase :: TermEvaluator abt (PEval abt p m) -> CaseEvaluator abt (PEval abt p m)

evaluateVar :: MeasureEvaluator abt (PEval abt p m) -> TermEvaluator abt (PEval abt p m) -> VariableEvaluator abt (PEval abt p m)

Monad (PEval abt p m)

Methods

(>>=) :: PEval abt p m a -> (a -> PEval abt p m b) -> PEval abt p m b

(>>) :: PEval abt p m a -> PEval abt p m b -> PEval abt p m b

return :: a -> PEval abt p m a

fail :: String -> PEval abt p m a

Functor (PEval abt p m)

Methods

fmap :: (a -> b) -> PEval abt p m a -> PEval abt p m b

(<$) :: a -> PEval abt p m b -> PEval abt p m a

Applicative (PEval abt p m)

Methods

pure :: a -> PEval abt p m a

(<*>) :: PEval abt p m (a -> b) -> PEval abt p m a -> PEval abt p m b

(*>) :: PEval abt p m a -> PEval abt p m b -> PEval abt p m b

(<*) :: PEval abt p m a -> PEval abt p m b -> PEval abt p m a

Alternative m => Alternative (PEval abt p m)

Methods

empty :: PEval abt p m a

(<|>) :: PEval abt p m a -> PEval abt p m a -> PEval abt p m a

some :: PEval abt p m a -> PEval abt p m [a]

many :: PEval abt p m a -> PEval abt p m [a]

Alternative m => MonadPlus (PEval abt p m)

Methods

mzero :: PEval abt p m a

mplus :: PEval abt p m a -> PEval abt p m a -> PEval abt p m a

runPureEval :: (ABT Term abt, Applicative m, Foldable f) => PEval abt Pure m (abt '[] a) -> f (Some2 abt) -> m (abt '[] a)

runImpureEval :: (ABT Term abt, Applicative m, Foldable f) => PEval abt Impure m (abt '[] a) -> f (Some2 abt) -> m (abt '[] (HMeasure a))

Run an Impure computation in the PEval monad, residualizing out all the statements in the final evaluation context. The second argument should include all the terms altered by the PEval expression; this is necessary to ensure proper hygiene; for example(s):

runPEval (perform e) [Some2 e]
runPEval (constrainOutcome e v) [Some2 e, Some2 v]

We use Some2 on the inputs because it doesn't matter what their type or locally-bound variables are, so we want to allow f to contain terms with different indices.

runExpectEval :: (ABT Term abt, Applicative m, Foldable f) => PEval abt ExpectP m (abt '[] a) -> abt '[a] HProb -> f (Some2 abt) -> m (abt '[] HProb)

TODO: IntMap-based version

Operators on the disintegration monad

The "zero" and "one"

bot :: (ABT Term abt, Alternative m) => PEval abt p m a

It is impossible to satisfy the constraints, or at least we give up on trying to do so. This function is identical to empty and mzero for PEval; we just give it its own name since this is the name used in our papers.

TODO: add some sort of trace information so we can get a better idea what caused a disintegration to fail.

Emitting code

emit :: (ABT Term abt, Functor m) => Text -> Sing a -> (forall r. P p abt '[a] r -> P p abt '[] r) -> PEval abt p m (Variable a)

Emit some code that binds a variable, and return the variable thus bound. The function says what to wrap the result of the continuation with; i.e., what we're actually emitting.

emitMBind :: (ABT Term abt, Functor m) => abt '[] (HMeasure a) -> PEval abt Impure m (Variable a)

Emit an MBind (i.e., "m >>= x ->") and return the variable thus bound (i.e., x).

emitLet :: (ABT Term abt, Functor m) => abt '[] a -> PEval abt p m (Variable a)

A smart constructor for emitting let-bindings. If the input is already a variable then we just return it; otherwise we emit the let-binding. N.B., this function provides the invariant that the result is in fact a variable; whereas emitLet' does not.

emitLet' :: (ABT Term abt, Functor m) => abt '[] a -> PEval abt p m (abt '[] a)

A smart constructor for emitting let-bindings. If the input is already a variable or a literal constant, then we just return it; otherwise we emit the let-binding. N.B., this function provides weaker guarantees on the type of the result; if you require the result to always be a variable, then see emitLet instead.

emitUnpair :: (ABT Term abt, Applicative m) => Whnf abt (HPair a b) -> PEval abt p m (abt '[] a, abt '[] b)

A smart constructor for emitting "unpair". If the input argument is actually a constructor then we project out the two components; otherwise we emit the case-binding and return the two variables.

emit_ :: (ABT Term abt, Functor m) => (forall r. P p abt '[] r -> P p abt '[] r) -> PEval abt p m ()

Emit some code that doesn't bind any variables. This function provides an optimisation over using emit and then discarding the generated variable.

emitMBind_ :: (ABT Term abt, Functor m) => abt '[] (HMeasure HUnit) -> PEval abt Impure m ()

Emit an MBind that discards its result (i.e., "m >>"). We restrict the type of the argument to be HUnit so as to avoid accidentally dropping things.

emitGuard :: (ABT Term abt, Functor m) => abt '[] HBool -> PEval abt Impure m ()

Emit an assertion that the condition is true.

emitWeight :: (ABT Term abt, Functor m) => abt '[] HProb -> PEval abt Impure m ()

emitFork_ :: (ABT Term abt, Applicative m, Traversable t) => (forall r. t (P p abt '[] r) -> P p abt '[] r) -> t (PEval abt p m a) -> PEval abt p m a

Run each of the elements of the traversable using the same heap and continuation for each one, then pass the results to a function for emitting code.

emitSuperpose :: (ABT Term abt, Functor m) => [abt '[] (HMeasure a)] -> PEval abt Impure m (Variable a)

Emit a Superpose_ of the alternatives, each with unit weight.

choose :: (ABT Term abt, Applicative m) => [PEval abt Impure m a] -> PEval abt Impure m a

Emit a Superpose_ of the alternatives, each with unit weight.