Language.Hakaru.Evaluation.Types

The data types for Language.Hakaru.Evaluation.Lazy

BUG: completely gave up on structure sharing. Need to add that back in.

TODO: once we figure out the exact API/type of evaluate and can separate it from Disintegrate.hs vs its other clients (i.e., Sample.hs and Expect.hs), this file will prolly be broken up into Lazy.hs itself vs Disintegrate.hs

Terms in particular known forms/formats

data Head :: ([Hakaru] -> Hakaru -> *) -> Hakaru -> * where

A "weak-head" for the sake of Whnf. N.B., this doesn't exactly correlate with the usual notion of "weak-head"; in particular we keep track of type annotations and coercions, and don't reduce integration/summation. So really we should use some other name for Whnf...

Constructors

WLiteral :: !(Literal a) -> Head abt a

WDatum :: !(Datum (abt '[]) (HData' t)) -> Head abt (HData' t)

WEmpty :: !(Sing (HArray a)) -> Head abt (HArray a)

WArray :: !(abt '[] HNat) -> !(abt '[HNat] a) -> Head abt (HArray a)

WLam :: !(abt '[a] b) -> Head abt (a :-> b)

WMeasureOp :: (typs ~ UnLCs args, args ~ LCs typs) => !(MeasureOp typs a) -> !(SArgs abt args) -> Head abt (HMeasure a)

WDirac :: !(abt '[] a) -> Head abt (HMeasure a)

WMBind :: !(abt '[] (HMeasure a)) -> !(abt '[a] (HMeasure b)) -> Head abt (HMeasure b)

WPlate :: !(abt '[] HNat) -> !(abt '[HNat] (HMeasure a)) -> Head abt (HMeasure (HArray a))

WChain :: !(abt '[] HNat) -> !(abt '[] s) -> !(abt '[s] (HMeasure (HPair a s))) -> Head abt (HMeasure (HPair (HArray a) s))

WSuperpose :: !(NonEmpty (abt '[] HProb, abt '[] (HMeasure a))) -> Head abt (HMeasure a)

WReject :: !(Sing (HMeasure a)) -> Head abt (HMeasure a)

WCoerceTo :: !(Coercion a b) -> !(Head abt a) -> Head abt b

WUnsafeFrom :: !(Coercion a b) -> !(Head abt b) -> Head abt a

WIntegrate :: !(abt '[] HReal) -> !(abt '[] HReal) -> !(abt '[HReal] HProb) -> Head abt HProb

Instances

Traversable21 Hakaru Hakaru [Hakaru] Head

Methods

traverse21 :: Applicative f => (forall h i. a h i -> f (b h i)) -> t a j -> f (t b j)

Foldable21 Hakaru Hakaru [Hakaru] Head

Methods

fold21 :: Monoid m => f (Lift2 k2 k1 m) j -> m

foldMap21 :: Monoid m => (forall h i. a h i -> m) -> f a j -> m

Functor21 Hakaru Hakaru [Hakaru] Head

Methods

fmap21 :: (forall h i. a h i -> b h i) -> f a j -> f b j

fromHead :: ABT Term abt => Head abt a -> abt '[] a

Forget that something is a head.

toHead :: ABT Term abt => abt '[] a -> Maybe (Head abt a)

Identify terms which are already heads.

viewHeadDatum :: ABT Term abt => Head abt (HData' t) -> Datum (abt '[]) (HData' t)

data Whnf abt a

Weak head-normal forms are either heads or neutral terms (i.e., a term whose reduction is blocked on some free variable).

Constructors

Head_ !(Head abt a)

Neutral !(abt '[] a)

Instances

Traversable21 Hakaru Hakaru [Hakaru] Whnf

Methods

traverse21 :: Applicative f => (forall h i. a h i -> f (b h i)) -> t a j -> f (t b j)

Foldable21 Hakaru Hakaru [Hakaru] Whnf

Methods

fold21 :: Monoid m => f (Lift2 k2 k1 m) j -> m

foldMap21 :: Monoid m => (forall h i. a h i -> m) -> f a j -> m

Functor21 Hakaru Hakaru [Hakaru] Whnf

Methods

fmap21 :: (forall h i. a h i -> b h i) -> f a j -> f b j

ABT Hakaru Term abt => Coerce (Whnf abt)

Methods

coerceTo :: Coercion a b -> Whnf abt a -> Whnf abt b

coerceFrom :: Coercion a b -> Whnf abt b -> Whnf abt a

fromWhnf :: ABT Term abt => Whnf abt a -> abt '[] a

Forget that something is a WHNF.

toWhnf :: ABT Term abt => abt '[] a -> Maybe (Whnf abt a)

Identify terms which are already heads. N.B., we make no attempt to identify neutral terms, we just massage the type of toHead.

caseWhnf :: Whnf abt a -> (Head abt a -> r) -> (abt '[] a -> r) -> r

Case analysis on Whnf as a combinator.

viewWhnfDatum :: ABT Term abt => Whnf abt (HData' t) -> Maybe (Datum (abt '[]) (HData' t))

Given some WHNF, try to extract a Datum from it.

data Lazy abt a

Lazy terms are either thunks (i.e., any term, which we may decide to evaluate later) or are already evaluated to WHNF.

Constructors

Whnf_ !(Whnf abt a)

Thunk !(abt '[] a)

Instances

Traversable21 Hakaru Hakaru [Hakaru] Lazy

Methods

traverse21 :: Applicative f => (forall h i. a h i -> f (b h i)) -> t a j -> f (t b j)

Foldable21 Hakaru Hakaru [Hakaru] Lazy

Methods

fold21 :: Monoid m => f (Lift2 k2 k1 m) j -> m

foldMap21 :: Monoid m => (forall h i. a h i -> m) -> f a j -> m

Functor21 Hakaru Hakaru [Hakaru] Lazy

Methods

fmap21 :: (forall h i. a h i -> b h i) -> f a j -> f b j

fromLazy :: ABT Term abt => Lazy abt a -> abt '[] a

Forget whether a term has been evaluated to WHNF or not.

caseLazy :: Lazy abt a -> (Whnf abt a -> r) -> (abt '[] a -> r) -> r

Case analysis on Lazy as a combinator.

getLazyVariable :: ABT Term abt => Lazy abt a -> Maybe (Variable a)

Is the lazy value a variable?

isLazyVariable :: ABT Term abt => Lazy abt a -> Bool

Boolean-blind variant of getLazyVariable

getLazyLiteral :: ABT Term abt => Lazy abt a -> Maybe (Literal a)

Is the lazy value a literal?

isLazyLiteral :: ABT Term abt => Lazy abt a -> Bool

Boolean-blind variant of getLazyLiteral

The monad for partial evaluation

data Purity

A kind for indexing Statement to know whether the statement is pure (and thus can be evaluated in any ambient monad) vs impure (i.e., must be evaluated in the HMeasure monad).

TODO: better names!

Constructors

Pure

Impure

ExpectP

Instances

Eq Purity

Methods

(==) :: Purity -> Purity -> Bool

(/=) :: Purity -> Purity -> Bool

Read Purity

Methods

readsPrec :: Int -> ReadS Purity

readList :: ReadS [Purity]

readPrec :: ReadPrec Purity

readListPrec :: ReadPrec [Purity]

Show Purity

Methods

showsPrec :: Int -> Purity -> ShowS

show :: Purity -> String

showList :: [Purity] -> ShowS

data Statement :: ([Hakaru] -> Hakaru -> *) -> Purity -> * where

A single statement in some ambient monad (specified by the p type index). In particular, note that the the first argument to MBind (or Let_) together with the variable bound in the second argument forms the "statement" (leaving out the body of the second argument, which may be part of a following statement). In addition to these binding constructs, we also include a few non-binding statements like SWeight.

The semantics of this type are as follows. Let ss :: [Statement abt p] be a sequence of statements. We have Γ: the collection of all free variables that occur in the term expressions in ss, viewed as a measureable space (namely the product of the measureable spaces for each variable). And we have Δ: the collection of all variables bound by the statements in ss, also viewed as a measurable space. The semantic interpretation of ss is a measurable function of type Γ ':-> M Δ where M is either HMeasure (if p ~ 'Impure) or Identity (if p ~ 'Pure).

Constructors

SBind :: forall abt a. !(Variable a) -> !(Lazy abt (HMeasure a)) -> [Index (abt '[])] -> Statement abt Impure

SLet :: forall abt p a. !(Variable a) -> !(Lazy abt a) -> [Index (abt '[])] -> Statement abt p

SWeight :: forall abt. !(Lazy abt HProb) -> [Index (abt '[])] -> Statement abt Impure

SGuard :: forall abt xs a. !(List1 Variable xs) -> !(Pattern xs a) -> !(Lazy abt a) -> [Index (abt '[])] -> Statement abt Impure

SStuff0 :: forall abt. (abt '[] HProb -> abt '[] HProb) -> [Index (abt '[])] -> Statement abt ExpectP

SStuff1 :: forall abt a. !(Variable a) -> (abt '[] HProb -> abt '[] HProb) -> [Index (abt '[])] -> Statement abt ExpectP

statementVars :: Statement abt p -> VarSet (KProxy :: KProxy Hakaru)

isBoundBy :: Variable (a :: Hakaru) -> Statement abt p -> Maybe ()

Is the variable bound by the statement?

We return Maybe () rather than Bool because in our primary use case we're already in the Maybe monad and so it's easier to just stick with that. If we find other situations where we'd really rather have the Bool, then we can easily change things and use some boolToMaybe function to do the coercion wherever needed.

data Index ast

Instances

ABT Hakaru Term abt => Eq (Index (abt ([] Hakaru)))

Methods

(==) :: Index (abt [Hakaru]) -> Index (abt [Hakaru]) -> Bool

(/=) :: Index (abt [Hakaru]) -> Index (abt [Hakaru]) -> Bool

ABT Hakaru Term abt => Ord (Index (abt ([] Hakaru)))

Methods

compare :: Index (abt [Hakaru]) -> Index (abt [Hakaru]) -> Ordering

(<) :: Index (abt [Hakaru]) -> Index (abt [Hakaru]) -> Bool

(<=) :: Index (abt [Hakaru]) -> Index (abt [Hakaru]) -> Bool

(>) :: Index (abt [Hakaru]) -> Index (abt [Hakaru]) -> Bool

(>=) :: Index (abt [Hakaru]) -> Index (abt [Hakaru]) -> Bool

max :: Index (abt [Hakaru]) -> Index (abt [Hakaru]) -> Index (abt [Hakaru])

min :: Index (abt [Hakaru]) -> Index (abt [Hakaru]) -> Index (abt [Hakaru])

indVar :: Index ast -> Variable HNat

indSize :: Index ast -> ast HNat

class (Functor m, Applicative m, Monad m, ABT Term abt) => EvaluationMonad abt m p | m -> abt p where

This class captures the monadic operations needed by the evaluate function in Language.Hakaru.Lazy.

Minimal complete definition

freshNat, unsafePush, select

Methods

freshNat :: m Nat

Return a fresh natural number. That is, a number which is not the varID of any free variable in the expressions of interest, and isn't a number we've returned previously.

freshenStatement :: Statement abt p -> m (Statement abt p, Assocs (Variable :: Hakaru -> *))

Internal function for renaming the variables bound by a statement. We return the renamed statement along with a substitution for mapping the old variable names to their new variable names.

getIndices :: m [Index (abt '[])]

Returns the current Indices. Currently, this is only applicable to the Disintegration Monad, but could be relevant as other partial evaluators begin to handle Plate and Array

unsafePush :: Statement abt p -> m ()

Add a statement to the top of the context. This is unsafe because it may allow confusion between variables with the same name but different scopes (thus, may allow variable capture). Prefer using push_, push, or pushes.

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

Call unsafePush repeatedly. Is part of the class since we may be able to do this more efficiently than actually calling unsafePush repeatedly.

N.B., this should push things in the same order as pushes does.

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

Look for the statement s binding the variable. If found, then call the continuation with s in the context where s itself and everything s (transitively)depends on is included but everything that (transitively)depends on s is excluded; thus, the continuation may only alter the dependencies of s. After the continuation returns, restore all the bindings that were removed before calling the continuation. If no such s can be found, then return Nothing without altering the context at all.

N.B., the statement s itself is popped! Thus, it is up to the continuation to make sure to push new statements that bind all the variables bound by s!

TODO: pass the continuation more detail, so it can avoid needing to be in the Maybe monad due to the redundant call to varEq in the continuation. In particular, we want to do this so that we can avoid the return type m (Maybe (Maybe r)) while still correctly handling statements like SStuff1 which (a) do bind variables and thus should shadow bindings further up the ListContext, but which (b) offer up no expression the variable is bound to, and thus cannot be altered by forcing etc. To do all this, we need to pass the TypeEq proof from (the varEq call in) the isBoundBy call in the instance; but that means we also need some way of tying it together with the existential variable in the Statement. Perhaps we should have an alternative statement type which exposes the existential?

Instances

ABT Hakaru Term abt => EvaluationMonad abt (Dis abt) Impure

Methods

freshNat :: Dis abt Nat

freshenStatement :: Statement abt Impure -> Dis abt (Statement abt Impure, Assocs Hakaru (Variable Hakaru))

getIndices :: Dis abt [Index (abt [Hakaru])]

unsafePush :: Statement abt Impure -> Dis abt ()

unsafePushes :: [Statement abt Impure] -> Dis abt ()

select :: Variable Hakaru a -> (Statement abt Impure -> Maybe (Dis abt r)) -> Dis abt (Maybe r)

ABT Hakaru Term abt => EvaluationMonad abt (Eval abt) Pure

Methods

freshNat :: Eval abt Nat

freshenStatement :: Statement abt Pure -> Eval abt (Statement abt Pure, Assocs Hakaru (Variable Hakaru))

getIndices :: Eval abt [Index (abt [Hakaru])]

unsafePush :: Statement abt Pure -> Eval abt ()

unsafePushes :: [Statement abt Pure] -> Eval abt ()

select :: Variable Hakaru a -> (Statement abt Pure -> Maybe (Eval abt r)) -> Eval abt (Maybe r)

ABT Hakaru Term abt => EvaluationMonad abt (Expect abt) ExpectP

Methods

freshNat :: Expect abt Nat

freshenStatement :: Statement abt ExpectP -> Expect abt (Statement abt ExpectP, Assocs Hakaru (Variable Hakaru))

getIndices :: Expect abt [Index (abt [Hakaru])]

unsafePush :: Statement abt ExpectP -> Expect abt ()

unsafePushes :: [Statement abt ExpectP] -> Expect abt ()

select :: Variable Hakaru a -> (Statement abt ExpectP -> Maybe (Expect abt r)) -> Expect abt (Maybe r)

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

Methods

freshNat :: PEval abt p m Nat

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

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

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

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

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

freshVar :: EvaluationMonad abt m p => Text -> Sing (a :: Hakaru) -> m (Variable a)

Given some hint and type, generate a variable with a fresh varID.

freshenVar :: EvaluationMonad abt m p => Variable (a :: Hakaru) -> m (Variable a)

Given a variable, return a new variable with the same hint and type but with a fresh varID.

data Hint a

Constructors

Hint !Text !(Sing a)

freshVars :: EvaluationMonad abt m p => List1 Hint xs -> m (List1 Variable xs)

Call freshVar repeatedly. TODO: make this more efficient than actually calling freshVar repeatedly.

freshenVars :: EvaluationMonad abt m p => List1 Variable (xs :: [Hakaru]) -> m (List1 Variable xs)

Call freshenVar repeatedly. TODO: make this more efficient than actually calling freshenVar repeatedly.

freshInd :: EvaluationMonad abt m p => abt '[] HNat -> m (Index (abt '[]))

Given a size, generate a fresh Index

push

Arguments

:: (ABT Term abt, EvaluationMonad abt m p)

=> Statement abt p

the statement to push

-> abt xs a

the "rest" of the term

-> (abt xs a -> m r)

what to do with the renamed "rest"

-> m r

the final result

Push a statement onto the context, renaming variables along the way. The second argument represents "the rest of the term" after we've peeled the statement off; it's passed so that we can update the variable names there so that they match with the (renamed)binding statement. The third argument is the continuation for what to do with the renamed term. Rather than taking the second and third arguments we could return an Assocs giving the renaming of variables; however, doing that would make it too easy to accidentally drop the substitution on the floor rather than applying it to the term before calling the continuation.

pushes

Arguments

:: (ABT Term abt, EvaluationMonad abt m p)

=> [Statement abt p]

the statements to push

-> abt xs a

the "rest" of the term

-> (abt xs a -> m r)

what to do with the renamed "rest"

-> m r

the final result

Call push repeatedly. (N.B., is more efficient than actually calling push repeatedly.) The head is pushed first and thus is the furthest away in the final context, whereas the tail is pushed last and is the closest in the final context.