Copyright | Copyright (c) 2016 the Hakaru team |
---|---|
License | BSD3 |
Maintainer | wren@community.haskell.org |
Stability | experimental |
Portability | GHC-only |
Safe Haskell | None |
Language | Haskell2010 |
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
- data Head :: ([Hakaru] -> Hakaru -> *) -> Hakaru -> * where
- 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
- fromHead :: ABT Term abt => Head abt a -> abt '[] a
- toHead :: ABT Term abt => abt '[] a -> Maybe (Head abt a)
- viewHeadDatum :: ABT Term abt => Head abt (HData' t) -> Datum (abt '[]) (HData' t)
- data Whnf abt a
- fromWhnf :: ABT Term abt => Whnf abt a -> abt '[] a
- toWhnf :: ABT Term abt => abt '[] a -> Maybe (Whnf abt a)
- caseWhnf :: Whnf abt a -> (Head abt a -> r) -> (abt '[] a -> r) -> r
- viewWhnfDatum :: ABT Term abt => Whnf abt (HData' t) -> Maybe (Datum (abt '[]) (HData' t))
- data Lazy abt a
- fromLazy :: ABT Term abt => Lazy abt a -> abt '[] a
- caseLazy :: Lazy abt a -> (Whnf abt a -> r) -> (abt '[] a -> r) -> r
- getLazyVariable :: ABT Term abt => Lazy abt a -> Maybe (Variable a)
- isLazyVariable :: ABT Term abt => Lazy abt a -> Bool
- getLazyLiteral :: ABT Term abt => Lazy abt a -> Maybe (Literal a)
- isLazyLiteral :: ABT Term abt => Lazy abt a -> Bool
- type TermEvaluator abt m = forall a. abt '[] a -> m (Whnf abt a)
- type MeasureEvaluator abt m = forall a. abt '[] (HMeasure a) -> m (Whnf abt a)
- type CaseEvaluator abt m = forall a b. abt '[] a -> [Branch a abt b] -> m (Whnf abt b)
- type VariableEvaluator abt m = forall a. Variable a -> m (Whnf abt a)
- data Purity
- data Statement :: ([Hakaru] -> Hakaru -> *) -> (Hakaru -> *) -> Purity -> * where
- 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 ()
- data Index ast
- indVar :: Index ast -> Variable HNat
- indSize :: Index ast -> ast HNat
- fromIndex :: ABT Term abt => Index (abt '[]) -> abt '[] HNat
- newtype Location a = Location (Variable a)
- 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)
- freshenLocs :: EvaluationMonad abt m p => List1 Location (ls :: [Hakaru]) -> m (List1 Location ls)
- 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
- defaultCaseEvaluator :: forall abt m p. (ABT Term abt, EvaluationMonad abt m p) => TermEvaluator abt m -> CaseEvaluator abt m
- 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)
- freshenVar :: EvaluationMonad abt m p => Variable (a :: Hakaru) -> m (Variable a)
- data Hint a = Hint !Text !(Sing a)
- freshVars :: EvaluationMonad abt m p => List1 Hint xs -> m (List1 Variable xs)
- freshenVars :: EvaluationMonad abt m p => List1 Variable (xs :: [Hakaru]) -> m (List1 Variable xs)
- freshInd :: EvaluationMonad abt m p => abt '[] HNat -> m (Index (abt '[]))
- push :: (ABT Term abt, EvaluationMonad abt m p) => Statement abt Variable p -> abt xs a -> m (abt xs a)
- pushes :: (ABT Term abt, EvaluationMonad abt m p) => [Statement abt Variable p] -> abt xs a -> m (abt xs a)
Terms in particular known forms/formats
data Head :: ([Hakaru] -> Hakaru -> *) -> Hakaru -> * where Source #
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
...
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 |
toHead :: ABT Term abt => abt '[] a -> Maybe (Head abt a) Source #
Identify terms which are already heads.
Weak head-normal forms are either heads or neutral terms (i.e., a term whose reduction is blocked on some free variable).
toWhnf :: ABT Term abt => abt '[] a -> Maybe (Whnf abt a) Source #
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 Source #
Case analysis on Whnf
as a combinator.
viewWhnfDatum :: ABT Term abt => Whnf abt (HData' t) -> Maybe (Datum (abt '[]) (HData' t)) Source #
Given some WHNF, try to extract a Datum
from it.
Lazy terms are either thunks (i.e., any term, which we may decide to evaluate later) or are already evaluated to WHNF.
fromLazy :: ABT Term abt => Lazy abt a -> abt '[] a Source #
Forget whether a term has been evaluated to WHNF or not.
caseLazy :: Lazy abt a -> (Whnf abt a -> r) -> (abt '[] a -> r) -> r Source #
Case analysis on Lazy
as a combinator.
getLazyVariable :: ABT Term abt => Lazy abt a -> Maybe (Variable a) Source #
Is the lazy value a variable?
isLazyVariable :: ABT Term abt => Lazy abt a -> Bool Source #
Boolean-blind variant of getLazyVariable
getLazyLiteral :: ABT Term abt => Lazy abt a -> Maybe (Literal a) Source #
Is the lazy value a literal?
isLazyLiteral :: ABT Term abt => Lazy abt a -> Bool Source #
Boolean-blind variant of getLazyLiteral
Lazy partial evaluation
type TermEvaluator abt m = forall a. abt '[] a -> m (Whnf abt a) Source #
A function for evaluating any term to weak-head normal form.
type MeasureEvaluator abt m = forall a. abt '[] (HMeasure a) -> m (Whnf abt a) Source #
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) Source #
A function for evaluating any case-expression to weak-head normal form.
type VariableEvaluator abt m = forall a. Variable a -> m (Whnf abt a) Source #
A function for evaluating any variable to weak-head normal form.
The monad for partial evaluation
data Statement :: ([Hakaru] -> Hakaru -> *) -> (Hakaru -> *) -> Purity -> * where Source #
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
).
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 |
isBoundBy :: Location (a :: Hakaru) -> Statement abt Location p -> Maybe () Source #
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.
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
Distinguish between variables and heap locations
locEq :: (Show1 (Sing :: k -> *), JmEq1 (Sing :: k -> *)) => Location (a :: k) -> Location (b :: k) -> Maybe (TypeEq a b) Source #
fromLocation :: Location a -> Variable a Source #
freshenLoc :: EvaluationMonad abt m p => Location (a :: Hakaru) -> m (Location a) Source #
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) Source #
Call freshenLoc
repeatedly
emptyLAssocs :: LAssocs abt Source #
singletonLAssocs :: Location a -> f a -> LAssocs f Source #
lookupLAssoc :: (Show1 (Sing :: k -> *), JmEq1 (Sing :: k -> *)) => Location (a :: k) -> LAssocs ast -> Maybe (ast a) Source #
class (Functor m, Applicative m, Monad m, ABT Term abt) => EvaluationMonad abt m p | m -> abt p where Source #
This class captures the monadic operations needed by the
evaluate
function in Language.Hakaru.Lazy.
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 -> *)) Source #
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 '[])] Source #
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 () Source #
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 () Source #
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) Source #
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') Source #
extFreeVars :: abt xs a -> m (VarSet (KindOf a)) Source #
evaluateCase :: TermEvaluator abt m -> CaseEvaluator abt m Source #
evaluateVar :: MeasureEvaluator abt m -> TermEvaluator abt m -> VariableEvaluator abt m Source #
defaultCaseEvaluator :: forall abt m p. (ABT Term abt, EvaluationMonad abt m p) => TermEvaluator abt m -> CaseEvaluator abt m Source #
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.
extSubst :: forall abt a xs b m p. EvaluationMonad abt m p => Variable a -> abt '[] a -> abt xs b -> m (abt xs b) Source #
extSubsts :: forall abt a xs m p. EvaluationMonad abt m p => Assocs (abt '[]) -> abt xs a -> m (abt xs a) Source #
freshVar :: EvaluationMonad abt m p => Text -> Sing (a :: Hakaru) -> m (Variable a) Source #
Given some hint and type, generate a variable with a fresh
varID
.
freshenVar :: EvaluationMonad abt m p => Variable (a :: Hakaru) -> m (Variable a) Source #
Given a variable, return a new variable with the same hint and
type but with a fresh varID
.
freshenVars :: EvaluationMonad abt m p => List1 Variable (xs :: [Hakaru]) -> m (List1 Variable xs) Source #
Call freshenVar
repeatedly.
TODO: make this more efficient than actually calling freshenVar
repeatedly.
freshInd :: EvaluationMonad abt m p => abt '[] HNat -> m (Index (abt '[])) Source #
Given a size, generate a fresh Index
:: (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.
:: (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 |