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)
- 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
- data Purity
- data Statement :: ([Hakaru] -> Hakaru -> *) -> Purity -> * where
- 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 ()
- data Index ast
- 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
- 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 p -> abt xs a -> (abt xs a -> m r) -> m r
- pushes :: (ABT Term abt, EvaluationMonad abt m p) => [Statement abt p] -> abt xs a -> (abt xs a -> m r) -> m r

# 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) | |

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`

# The monad for partial evaluation

data Statement :: ([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`

.

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`

).

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 |

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

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.

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.

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

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 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.

:: (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 |