Language.Hakaru.Evaluation.Lazy

Lazy partial evaluation.

BUG: completely gave up on structure sharing. Need to add that back in. cf., gvidal-lopstr07lncs.pdf for an approach much like my old one.

Lazy partial evaluation

type TermEvaluator abt m = forall a. abt '[] a -> m (Whnf abt a)

A function for evaluating any term to weak-head normal form.

type MeasureEvaluator abt m = forall a. abt '[] (HMeasure a) -> m (Whnf abt a)

A function for "performing" an HMeasure monadic action. This could mean actual random sampling, or simulated sampling by generating a new term and returning the newly bound variable, or anything else.

type CaseEvaluator abt m = forall a b. abt '[] a -> [Branch a abt b] -> m (Whnf abt b)

A function for evaluating any case-expression to weak-head normal form.

type VariableEvaluator abt m = forall a. Variable a -> m (Whnf abt a)

A function for evaluating any variable to weak-head normal form.

evaluate :: forall abt m p. (ABT Term abt, EvaluationMonad abt m p) => MeasureEvaluator abt m -> (TermEvaluator abt m -> CaseEvaluator abt m) -> TermEvaluator abt m

Lazy partial evaluation with some given "perform" and "evaluateCase" functions. The first argument to evaluateCase will be the TermEvaluator we're constructing (thus tying the knot). N.B., if p ~ 'Pure then the "perform" function will never be called.

We factor out the CaseEvaluator because some code (e.g., disintegration) may need to do something special rather than just relying on the defaultCaseEvaluator implementation.

Helper functions

update :: forall abt m p. (ABT Term abt, EvaluationMonad abt m p) => MeasureEvaluator abt m -> TermEvaluator abt m -> VariableEvaluator abt m

defaultCaseEvaluator :: forall abt m p. (ABT Term abt, EvaluationMonad abt m p) => TermEvaluator abt m -> CaseEvaluator abt m

A simple CaseEvaluator which uses the DatumEvaluator to force the scrutinee, and if matchBranches succeeds then we call the TermEvaluator to continue evaluating the body of the matched branch. If we GotStuck then we return a Neutral term of the case expression itself (n.b, any side effects from having called the DatumEvaluator will still persist when returning this neutral term). If we didn't get stuck and yet none of the branches matches, then we throw an exception.

toStatements :: Assocs (abt '[]) -> [Statement abt p]

Helpers that should really go away

class Interp a a' | a -> a' where

Minimal complete definition

reify, reflect

Methods

reify :: ABT Term abt => Head abt a -> a'

reflect :: ABT Term abt => a' -> Head abt a

Instances

Interp HUnit ()

Methods

reify :: ABT Hakaru Term abt => Head abt HUnit -> ()

reflect :: ABT Hakaru Term abt => () -> Head abt HUnit

Interp HBool Bool

Methods

reify :: ABT Hakaru Term abt => Head abt HBool -> Bool

reflect :: ABT Hakaru Term abt => Bool -> Head abt HBool

Interp HNat Natural

Methods

reify :: ABT Hakaru Term abt => Head abt HNat -> Natural

reflect :: ABT Hakaru Term abt => Natural -> Head abt HNat

Interp HInt Integer

Methods

reify :: ABT Hakaru Term abt => Head abt HInt -> Integer

reflect :: ABT Hakaru Term abt => Integer -> Head abt HInt

Interp HProb NonNegativeRational

Methods

reify :: ABT Hakaru Term abt => Head abt HProb -> NonNegativeRational

reflect :: ABT Hakaru Term abt => NonNegativeRational -> Head abt HProb

Interp HReal Rational

Methods

reify :: ABT Hakaru Term abt => Head abt HReal -> Rational

reflect :: ABT Hakaru Term abt => Rational -> Head abt HReal

reifyPair :: ABT Term abt => Head abt (HPair a b) -> (abt '[] a, abt '[] b)