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)

WArrayLiteral :: [abt '[] 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

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)

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

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.

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 -> *) -> (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.

Statements are parameterized by the type of the bound element, which (if present) is either a Variable or a Location.

The semantics of this type are as follows. Let ss :: [Statement abt v 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 v a. !(v a) -> !(Lazy abt (HMeasure a)) -> [Index (abt '[])] -> Statement abt v Impure

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

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

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

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

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

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

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

Is the Location 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

A type for tracking the arrays under which the term resides This is used as a binding form when we "lift" transformations (currently only Disintegrate) to work on arrays

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

fromIndex :: ABT Term abt => Index (abt '[]) -> abt '[] HNat

newtype Location a

Distinguish between variables and heap locations

Constructors

Location (Variable a)

Instances

Show (Sing k a) => Show (Location k a)

Methods

showsPrec :: Int -> Location k a -> ShowS

show :: Location k a -> String

showList :: [Location k a] -> ShowS

locEq :: (Show1 (Sing :: k -> *), JmEq1 (Sing :: k -> *)) => Location (a :: k) -> Location (b :: k) -> Maybe (TypeEq a b)

locHint :: Location a -> Text

locType :: Location a -> Sing a

locations1 :: List1 Variable a -> List1 Location a

fromLocation :: Location a -> Variable a

fromLocations1 :: List1 Location a -> List1 Variable a

freshenLoc :: EvaluationMonad abt m p => Location (a :: Hakaru) -> m (Location a)

Given a location, return a new Location with the same hint and type but with a fresh ID

freshenLocs :: EvaluationMonad abt m p => List1 Location (ls :: [Hakaru]) -> m (List1 Location ls)

Call freshenLoc repeatedly

data LAssoc ast

data LAssocs ast

emptyLAssocs :: LAssocs abt

singletonLAssocs :: Location a -> f a -> LAssocs f

toLAssocs1 :: List1 Location xs -> List1 ast xs -> LAssocs ast

insertLAssocs :: LAssocs ast -> LAssocs ast -> LAssocs ast

lookupLAssoc :: (Show1 (Sing :: k -> *), JmEq1 (Sing :: k -> *)) => Location (a :: k) -> LAssocs ast -> Maybe (ast a)

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.

freshLocStatement :: Statement abt Variable p -> m (Statement abt Location 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 Location 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 Location 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 :: Location (a :: Hakaru) -> (Statement abt Location 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?

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

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

evaluateCase :: TermEvaluator abt m -> CaseEvaluator abt m

evaluateVar :: MeasureEvaluator abt m -> TermEvaluator abt m -> VariableEvaluator abt m

Instances

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

Methods

freshNat :: Dis abt Nat

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

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

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

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

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

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

extFreeVars :: abt xs a -> Dis abt (VarSet Hakaru (KindOf Hakaru a))

evaluateCase :: TermEvaluator abt (Dis abt) -> CaseEvaluator abt (Dis abt)

evaluateVar :: MeasureEvaluator abt (Dis abt) -> TermEvaluator abt (Dis abt) -> VariableEvaluator abt (Dis abt)

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

Methods

freshNat :: Eval abt Nat

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

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

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

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

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

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

extFreeVars :: abt xs a -> Eval abt (VarSet Hakaru (KindOf Hakaru a))

evaluateCase :: TermEvaluator abt (Eval abt) -> CaseEvaluator abt (Eval abt)

evaluateVar :: MeasureEvaluator abt (Eval abt) -> TermEvaluator abt (Eval abt) -> VariableEvaluator abt (Eval abt)

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

Methods

freshNat :: Expect abt Nat

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

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

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

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

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

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

extFreeVars :: abt xs a -> Expect abt (VarSet Hakaru (KindOf Hakaru a))

evaluateCase :: TermEvaluator abt (Expect abt) -> CaseEvaluator abt (Expect abt)

evaluateVar :: MeasureEvaluator abt (Expect abt) -> TermEvaluator abt (Expect abt) -> VariableEvaluator abt (Expect abt)

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)

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.

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

extSubst :: forall abt a xs b m p. EvaluationMonad abt m p => Variable a -> abt '[] a -> abt xs b -> m (abt xs b)

extSubsts :: forall abt a xs m p. EvaluationMonad abt m p => Assocs (abt '[]) -> abt xs a -> m (abt xs a)

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 Variable 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 (abt xs a)

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 Variable 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 (abt xs a)

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.