Copyright	Copyright (c) 2016 the Hakaru team
License	BSD3
Maintainer	wren@community.haskell.org
Stability	experimental
Portability	GHC-only
Safe Haskell	None
Language	Haskell2010

Language.Hakaru.Syntax.Prelude

Contents

Basic syntax
Measures
Data types (other than booleans)
Case and Branch
Lambda calculus
Arrays
Implementation details

Description

A replacement for Haskell's Prelude, using the familiar symbols in order to construct ASTs and ABTs. This is only necessary if we want to use Hakaru as an embedded language in Haskell, but it also provides some examples of how to use the infrastructure.

TODO: is there a way to get rid of the need to specify '[] everywhere in here? Some sort of distinction between the Var vs the Open parts of View?

Synopsis

Basic syntax

Types and coercions

ann_ :: ABT Term abt => Sing a -> abt '[] a -> abt '[] a Source #

triv :: TrivialABT Term '[] a -> TrivialABT Term '[] a Source #

memo :: MemoizedABT Term '[] a -> MemoizedABT Term '[] a Source #

coerceTo_ :: ABT Term abt => Coercion a b -> abt '[] a -> abt '[] b Source #

fromProb :: ABT Term abt => abt '[] HProb -> abt '[] HReal Source #

nat2int :: ABT Term abt => abt '[] HNat -> abt '[] HInt Source #

nat2prob :: ABT Term abt => abt '[] HNat -> abt '[] HProb Source #

fromInt :: ABT Term abt => abt '[] HInt -> abt '[] HReal Source #

nat2real :: ABT Term abt => abt '[] HNat -> abt '[] HReal Source #

unsafeFrom_ :: ABT Term abt => Coercion a b -> abt '[] b -> abt '[] a Source #

unsafeProb :: ABT Term abt => abt '[] HReal -> abt '[] HProb Source #

unsafeProbFraction :: forall abt a. (ABT Term abt, HFractional_ a) => abt '[] a -> abt '[] HProb Source #

unsafeProbFraction_ :: ABT Term abt => HFractional a -> abt '[] a -> abt '[] HProb Source #

unsafeProbSemiring :: forall abt a. (ABT Term abt, HSemiring_ a) => abt '[] a -> abt '[] HProb Source #

unsafeProbSemiring_ :: ABT Term abt => HSemiring a -> abt '[] a -> abt '[] HProb Source #

Numeric literals

literal_ :: ABT Term abt => Literal a -> abt '[] a Source #

nat_ :: ABT Term abt => Natural -> abt '[] HNat Source #

int_ :: ABT Term abt => Integer -> abt '[] HInt Source #

prob_ :: ABT Term abt => NonNegativeRational -> abt '[] HProb Source #

real_ :: ABT Term abt => Rational -> abt '[] HReal Source #

fromRational :: forall abt a. (ABT Term abt, HFractional_ a) => Rational -> abt '[] a Source #

half :: forall abt a. (ABT Term abt, HFractional_ a) => abt '[] a Source #

third :: (ABT Term abt, HFractional_ a) => abt '[] a Source #

Booleans

true :: ABT Term abt => abt '[] HBool Source #

false :: ABT Term abt => abt '[] HBool Source #

bool_ :: ABT Term abt => Bool -> abt '[] HBool Source #

if_ :: ABT Term abt => abt '[] HBool -> abt '[] a -> abt '[] a -> abt '[] a Source #

not :: ABT Term abt => abt '[] HBool -> abt '[] HBool Source #

(&&) :: ABT Term abt => abt '[] HBool -> abt '[] HBool -> abt '[] HBool infixr 3 Source #

and :: ABT Term abt => [abt '[] HBool] -> abt '[] HBool Source #

(||) :: ABT Term abt => abt '[] HBool -> abt '[] HBool -> abt '[] HBool infixr 2 Source #

or :: ABT Term abt => [abt '[] HBool] -> abt '[] HBool Source #

nand :: ABT Term abt => abt '[] HBool -> abt '[] HBool -> abt '[] HBool Source #

nor :: ABT Term abt => abt '[] HBool -> abt '[] HBool -> abt '[] HBool Source #

Equality and ordering

(==) :: (ABT Term abt, HEq_ a) => abt '[] a -> abt '[] a -> abt '[] HBool infix 4 Source #

(/=) :: (ABT Term abt, HEq_ a) => abt '[] a -> abt '[] a -> abt '[] HBool infix 4 Source #

(<) :: (ABT Term abt, HOrd_ a) => abt '[] a -> abt '[] a -> abt '[] HBool infix 4 Source #

(<=) :: (ABT Term abt, HOrd_ a) => abt '[] a -> abt '[] a -> abt '[] HBool infix 4 Source #

(>) :: (ABT Term abt, HOrd_ a) => abt '[] a -> abt '[] a -> abt '[] HBool infix 4 Source #

(>=) :: (ABT Term abt, HOrd_ a) => abt '[] a -> abt '[] a -> abt '[] HBool infix 4 Source #

min :: (ABT Term abt, HOrd_ a) => abt '[] a -> abt '[] a -> abt '[] a Source #

minimum :: (ABT Term abt, HOrd_ a) => [abt '[] a] -> abt '[] a Source #

max :: (ABT Term abt, HOrd_ a) => abt '[] a -> abt '[] a -> abt '[] a Source #

maximum :: (ABT Term abt, HOrd_ a) => [abt '[] a] -> abt '[] a Source #

Semirings

zero :: forall abt a. (ABT Term abt, HSemiring_ a) => abt '[] a Source #

zero_ :: ABT Term abt => HSemiring a -> abt '[] a Source #

one :: forall abt a. (ABT Term abt, HSemiring_ a) => abt '[] a Source #

one_ :: ABT Term abt => HSemiring a -> abt '[] a Source #

(+) :: (ABT Term abt, HSemiring_ a) => abt '[] a -> abt '[] a -> abt '[] a infixl 6 Source #

sum :: (ABT Term abt, HSemiring_ a) => [abt '[] a] -> abt '[] a Source #

(*) :: (ABT Term abt, HSemiring_ a) => abt '[] a -> abt '[] a -> abt '[] a infixl 7 Source #

prod :: (ABT Term abt, HSemiring_ a) => [abt '[] a] -> abt '[] a Source #

(^) :: (ABT Term abt, HSemiring_ a) => abt '[] a -> abt '[] HNat -> abt '[] a infixr 8 Source #

square :: (ABT Term abt, HRing_ a) => abt '[] a -> abt '[] (NonNegative a) Source #

unsafeMinusNat :: ABT Term abt => abt '[] HNat -> abt '[] HNat -> abt '[] HNat Source #

unsafeMinusProb :: ABT Term abt => abt '[] HProb -> abt '[] HProb -> abt '[] HProb Source #

unsafeMinus :: (ABT Term abt, HSemiring_ a) => abt '[] a -> abt '[] a -> abt '[] a Source #

For any semiring we can attempt subtraction by lifting to a ring, subtracting there, and then lowering back to the semiring. Of course, the lowering step may well fail.

unsafeMinus_ :: ABT Term abt => HSemiring a -> abt '[] a -> abt '[] a -> abt '[] a Source #

A variant of unsafeMinus for explicitly passing the semiring instance.

unsafeDiv :: (ABT Term abt, HSemiring_ a) => abt '[] a -> abt '[] a -> abt '[] a Source #

For any semiring we can attempt division by lifting to a semifield, dividing there, and then lowering back to the semiring. Of course, the lowering step may well fail.

unsafeDiv_ :: ABT Term abt => HSemiring a -> abt '[] a -> abt '[] a -> abt '[] a Source #

A variant of unsafeDiv for explicitly passing the semiring instance.

Rings

(-) :: (ABT Term abt, HRing_ a) => abt '[] a -> abt '[] a -> abt '[] a infixl 6 Source #

negate :: (ABT Term abt, HRing_ a) => abt '[] a -> abt '[] a Source #

negative :: (ABT Term abt, HRing_ a) => abt '[] (NonNegative a) -> abt '[] a Source #

An occasionally helpful variant of negate.

abs :: (ABT Term abt, HRing_ a) => abt '[] a -> abt '[] a Source #

abs_ :: (ABT Term abt, HRing_ a) => abt '[] a -> abt '[] (NonNegative a) Source #

signum :: (ABT Term abt, HRing_ a) => abt '[] a -> abt '[] a Source #

Fractional

(/) :: (ABT Term abt, HFractional_ a) => abt '[] a -> abt '[] a -> abt '[] a infixl 7 Source #

recip :: (ABT Term abt, HFractional_ a) => abt '[] a -> abt '[] a Source #

(^^) :: (ABT Term abt, HFractional_ a) => abt '[] a -> abt '[] HInt -> abt '[] a infixr 8 Source #

Radical

sqrt :: (ABT Term abt, HRadical_ a) => abt '[] a -> abt '[] a Source #

thRootOf :: (ABT Term abt, HRadical_ a) => abt '[] HNat -> abt '[] a -> abt '[] a infixl 9 Source #

Integration

integrate :: ABT Term abt => abt '[] HReal -> abt '[] HReal -> (abt '[] HReal -> abt '[] HProb) -> abt '[] HProb Source #

summate :: (ABT Term abt, HDiscrete_ a, HSemiring_ b, SingI a) => abt '[] a -> abt '[] a -> (abt '[] a -> abt '[] b) -> abt '[] b Source #

product :: (ABT Term abt, HDiscrete_ a, HSemiring_ b, SingI a) => abt '[] a -> abt '[] a -> (abt '[] a -> abt '[] b) -> abt '[] b Source #

Continuous

class RealProb a where Source #

Minimal complete definition

(**), exp, erf, pi, gammaFunc

Methods

(**) :: ABT Term abt => abt '[] HProb -> abt '[] a -> abt '[] HProb infixr 8 Source #

exp :: ABT Term abt => abt '[] a -> abt '[] HProb Source #

erf :: ABT Term abt => abt '[] a -> abt '[] a Source #

pi :: ABT Term abt => abt '[] a Source #

gammaFunc :: ABT Term abt => abt '[] a -> abt '[] HProb Source #

Instances

RealProb HProb Source #
Methods (**) :: ABT Hakaru Term abt => abt [Hakaru] HProb -> abt [Hakaru] HProb -> abt [Hakaru] HProb Source # exp :: ABT Hakaru Term abt => abt [Hakaru] HProb -> abt [Hakaru] HProb Source # erf :: ABT Hakaru Term abt => abt [Hakaru] HProb -> abt [Hakaru] HProb Source # pi :: ABT Hakaru Term abt => abt [Hakaru] HProb Source # gammaFunc :: ABT Hakaru Term abt => abt [Hakaru] HProb -> abt [Hakaru] HProb Source #
RealProb HReal Source #
Methods (**) :: ABT Hakaru Term abt => abt [Hakaru] HProb -> abt [Hakaru] HReal -> abt [Hakaru] HProb Source # exp :: ABT Hakaru Term abt => abt [Hakaru] HReal -> abt [Hakaru] HProb Source # erf :: ABT Hakaru Term abt => abt [Hakaru] HReal -> abt [Hakaru] HReal Source # pi :: ABT Hakaru Term abt => abt [Hakaru] HReal Source # gammaFunc :: ABT Hakaru Term abt => abt [Hakaru] HReal -> abt [Hakaru] HProb Source #

class Integrable a where Source #

Minimal complete definition

infinity

Methods

infinity :: ABT Term abt => abt '[] a Source #

Instances

Integrable HNat Source #
Methods infinity :: ABT Hakaru Term abt => abt [Hakaru] HNat Source #
Integrable HInt Source #
Methods infinity :: ABT Hakaru Term abt => abt [Hakaru] HInt Source #
Integrable HProb Source #
Methods infinity :: ABT Hakaru Term abt => abt [Hakaru] HProb Source #
Integrable HReal Source #
Methods infinity :: ABT Hakaru Term abt => abt [Hakaru] HReal Source #

betaFunc :: ABT Term abt => abt '[] HProb -> abt '[] HProb -> abt '[] HProb Source #

log :: ABT Term abt => abt '[] HProb -> abt '[] HReal Source #

logBase :: ABT Term abt => abt '[] HProb -> abt '[] HProb -> abt '[] HReal Source #

negativeInfinity :: (ABT Term abt, HRing_ a, Integrable a) => abt '[] a Source #

Trig

sin :: ABT Term abt => abt '[] HReal -> abt '[] HReal Source #

cos :: ABT Term abt => abt '[] HReal -> abt '[] HReal Source #

tan :: ABT Term abt => abt '[] HReal -> abt '[] HReal Source #

asin :: ABT Term abt => abt '[] HReal -> abt '[] HReal Source #

acos :: ABT Term abt => abt '[] HReal -> abt '[] HReal Source #

atan :: ABT Term abt => abt '[] HReal -> abt '[] HReal Source #

sinh :: ABT Term abt => abt '[] HReal -> abt '[] HReal Source #

cosh :: ABT Term abt => abt '[] HReal -> abt '[] HReal Source #

tanh :: ABT Term abt => abt '[] HReal -> abt '[] HReal Source #

asinh :: ABT Term abt => abt '[] HReal -> abt '[] HReal Source #

acosh :: ABT Term abt => abt '[] HReal -> abt '[] HReal Source #

atanh :: ABT Term abt => abt '[] HReal -> abt '[] HReal Source #

Measures

Abstract nonsense

dirac :: ABT Term abt => abt '[] a -> abt '[] (HMeasure a) Source #

(<$>) :: (ABT Term abt, SingI a) => (abt '[] a -> abt '[] b) -> abt '[] (HMeasure a) -> abt '[] (HMeasure b) infixl 4 Source #

(<*>) :: (ABT Term abt, SingI a, SingI b) => abt '[] (HMeasure (a :-> b)) -> abt '[] (HMeasure a) -> abt '[] (HMeasure b) infixl 4 Source #

N.B, this function may introduce administrative redexes. Moreover, it's not clear that we should even allow the type 'HMeasure (a ':-> b)!

(<*) :: (ABT Term abt, SingI a, SingI b) => abt '[] (HMeasure a) -> abt '[] (HMeasure b) -> abt '[] (HMeasure a) infixl 4 Source #

(*>) :: (ABT Term abt, SingI a) => abt '[] (HMeasure a) -> abt '[] (HMeasure b) -> abt '[] (HMeasure b) infixl 4 Source #

(>>=) :: ABT Term abt => abt '[] (HMeasure a) -> (abt '[] a -> abt '[] (HMeasure b)) -> abt '[] (HMeasure b) infixl 1 Source #

(>>) :: (ABT Term abt, SingI a) => abt '[] (HMeasure a) -> abt '[] (HMeasure b) -> abt '[] (HMeasure b) infixl 1 Source #

bindx :: (ABT Term abt, SingI a, SingI b) => abt '[] (HMeasure a) -> (abt '[] a -> abt '[] (HMeasure b)) -> abt '[] (HMeasure (HPair a b)) Source #

liftM2 :: (ABT Term abt, SingI a, SingI b) => (abt '[] a -> abt '[] b -> abt '[] c) -> abt '[] (HMeasure a) -> abt '[] (HMeasure b) -> abt '[] (HMeasure c) Source #

Linear operators

superpose :: ABT Term abt => NonEmpty (abt '[] HProb, abt '[] (HMeasure a)) -> abt '[] (HMeasure a) Source #

(<|>) :: ABT Term abt => abt '[] (HMeasure a) -> abt '[] (HMeasure a) -> abt '[] (HMeasure a) Source #

The sum of two measures. Is called mplus in the Core Hakaru paper.

weight :: ABT Term abt => abt '[] HProb -> abt '[] (HMeasure HUnit) Source #

Adjust the weight of the current measure.

N.B., the name for this function is terribly inconsistent across the literature, even just the Hakaru literature, let alone the Hakaru code base. It is variously called "factor" or "weight"; though "factor" is also used to mean the function factor or the function observe, and "weight" is also used to mean the weight function.

withWeight :: ABT Term abt => abt '[] HProb -> abt '[] (HMeasure w) -> abt '[] (HMeasure w) Source #

A variant of weight which removes an administrative (dirac unit >>) redex.

TODO: ideally we'll be able to get rid of this function entirely, and be able to trust optimization to clean up any redexes introduced by weight.

weightedDirac :: (ABT Term abt, SingI a) => abt '[] a -> abt '[] HProb -> abt '[] (HMeasure a) Source #

A particularly common use case of weight:

weightedDirac e p
    == weight p (dirac e)
    == weight p *> dirac e
    == dirac e <* weight p

reject :: ABT Term abt => Sing (HMeasure a) -> abt '[] (HMeasure a) Source #

The empty measure. Is called fail in the Core Hakaru paper.

guard :: ABT Term abt => abt '[] HBool -> abt '[] (HMeasure HUnit) Source #

Assert that a condition is true.

N.B., the name for this function is terribly inconsistent across the literature, even just the Hakaru literature, let alone the Hakaru code base. It is variously called "factor" or "observe"; though "factor" is also used to mean the function pose, and "observe" is also used to mean the backwards part of Lazy.hs.

withGuard :: ABT Term abt => abt '[] HBool -> abt '[] (HMeasure a) -> abt '[] (HMeasure a) Source #

A variant of guard which removes an administrative (dirac unit >>) redex.

TODO: ideally we'll be able to get rid of this function entirely, and be able to trust optimization to clean up any redexes introduced by guard.

Measure operators

When two versions of the same operator are given, the one without the prime builds an AST using the built-in operator, whereas the one with the prime is a default definition in terms of more primitive measure operators.

lebesgue :: ABT Term abt => abt '[] (HMeasure HReal) Source #

counting :: ABT Term abt => abt '[] (HMeasure HInt) Source #

densityCategorical :: ABT Term abt => abt '[] (HArray HProb) -> abt '[] HNat -> abt '[] HProb Source #

categorical :: ABT Term abt => abt '[] (HArray HProb) -> abt '[] (HMeasure HNat) Source #

categorical' :: ABT Term abt => abt '[] (HArray HProb) -> abt '[] (HMeasure HNat) Source #

densityUniform :: ABT Term abt => abt '[] HReal -> abt '[] HReal -> abt '[] HReal -> abt '[] HProb Source #

uniform :: ABT Term abt => abt '[] HReal -> abt '[] HReal -> abt '[] (HMeasure HReal) Source #

uniform' :: ABT Term abt => abt '[] HReal -> abt '[] HReal -> abt '[] (HMeasure HReal) Source #

densityNormal :: ABT Term abt => abt '[] HReal -> abt '[] HProb -> abt '[] HReal -> abt '[] HProb Source #

normal :: ABT Term abt => abt '[] HReal -> abt '[] HProb -> abt '[] (HMeasure HReal) Source #

normal' :: ABT Term abt => abt '[] HReal -> abt '[] HProb -> abt '[] (HMeasure HReal) Source #

densityPoisson :: ABT Term abt => abt '[] HProb -> abt '[] HNat -> abt '[] HProb Source #

poisson :: ABT Term abt => abt '[] HProb -> abt '[] (HMeasure HNat) Source #

poisson' :: ABT Term abt => abt '[] HProb -> abt '[] (HMeasure HNat) Source #

densityGamma :: ABT Term abt => abt '[] HProb -> abt '[] HProb -> abt '[] HProb -> abt '[] HProb Source #

gamma :: ABT Term abt => abt '[] HProb -> abt '[] HProb -> abt '[] (HMeasure HProb) Source #

gamma' :: ABT Term abt => abt '[] HProb -> abt '[] HProb -> abt '[] (HMeasure HProb) Source #

densityBeta :: ABT Term abt => abt '[] HProb -> abt '[] HProb -> abt '[] HProb -> abt '[] HProb Source #

beta :: ABT Term abt => abt '[] HProb -> abt '[] HProb -> abt '[] (HMeasure HProb) Source #

beta' :: ABT Term abt => abt '[] HProb -> abt '[] HProb -> abt '[] (HMeasure HProb) Source #

beta'' :: ABT Term abt => abt '[] HProb -> abt '[] HProb -> abt '[] (HMeasure HProb) Source #

plateWithVar :: ABT Term abt => abt '[] HNat -> Variable HNat -> abt '[] (HMeasure a) -> abt '[] (HMeasure (HArray a)) Source #

plate :: ABT Term abt => abt '[] HNat -> (abt '[] HNat -> abt '[] (HMeasure a)) -> abt '[] (HMeasure (HArray a)) Source #

plate' :: (ABT Term abt, SingI a) => abt '[] (HArray (HMeasure a)) -> abt '[] (HMeasure (HArray a)) Source #

chain :: (ABT Term abt, SingI s) => abt '[] HNat -> abt '[] s -> (abt '[] s -> abt '[] (HMeasure (HPair a s))) -> abt '[] (HMeasure (HPair (HArray a) s)) Source #

chain' :: (ABT Term abt, SingI s, SingI a) => abt '[] (HArray (s :-> HMeasure (HPair a s))) -> abt '[] s -> abt '[] (HMeasure (HPair (HArray a) s)) Source #

invgamma :: ABT Term abt => abt '[] HProb -> abt '[] HProb -> abt '[] (HMeasure HProb) Source #

exponential :: ABT Term abt => abt '[] HProb -> abt '[] (HMeasure HProb) Source #

chi2 :: ABT Term abt => abt '[] HProb -> abt '[] (HMeasure HProb) Source #

cauchy :: ABT Term abt => abt '[] HReal -> abt '[] HProb -> abt '[] (HMeasure HReal) Source #

laplace :: ABT Term abt => abt '[] HReal -> abt '[] HProb -> abt '[] (HMeasure HReal) Source #

studentT :: ABT Term abt => abt '[] HReal -> abt '[] HProb -> abt '[] HProb -> abt '[] (HMeasure HReal) Source #

weibull :: ABT Term abt => abt '[] HProb -> abt '[] HProb -> abt '[] (HMeasure HProb) Source #

bern :: ABT Term abt => abt '[] HProb -> abt '[] (HMeasure HBool) Source #

mix :: ABT Term abt => abt '[] (HArray HProb) -> abt '[] (HMeasure HNat) Source #

binomial :: ABT Term abt => abt '[] HNat -> abt '[] HProb -> abt '[] (HMeasure HInt) Source #

negativeBinomial :: ABT Term abt => abt '[] HNat -> abt '[] HProb -> abt '[] (HMeasure HNat) Source #

geometric :: ABT Term abt => abt '[] HProb -> abt '[] (HMeasure HNat) Source #

multinomial :: ABT Term abt => abt '[] HNat -> abt '[] (HArray HProb) -> abt '[] (HMeasure (HArray HProb)) Source #

dirichlet :: ABT Term abt => abt '[] (HArray HProb) -> abt '[] (HMeasure (HArray HProb)) Source #

Data types (other than booleans)

datum_ :: ABT Term abt => Datum (abt '[]) (HData' t) -> abt '[] (HData' t) Source #

Case and Branch

case_ :: ABT Term abt => abt '[] a -> [Branch a abt b] -> abt '[] b Source #

branch :: ABT Term abt => Pattern xs a -> abt xs b -> Branch a abt b Source #

HUnit

unit :: ABT Term abt => abt '[] HUnit Source #

HPair

pair :: (ABT Term abt, SingI a, SingI b) => abt '[] a -> abt '[] b -> abt '[] (HPair a b) Source #

pair_ :: ABT Term abt => Sing a -> Sing b -> abt '[] a -> abt '[] b -> abt '[] (HPair a b) Source #

unpair :: forall abt a b c. ABT Term abt => abt '[] (HPair a b) -> (abt '[] a -> abt '[] b -> abt '[] c) -> abt '[] c Source #

fst :: ABT Term abt => abt '[] (HPair a b) -> abt '[] a Source #

snd :: ABT Term abt => abt '[] (HPair a b) -> abt '[] b Source #

swap :: (ABT Term abt, SingI a, SingI b) => abt '[] (HPair a b) -> abt '[] (HPair b a) Source #

HEither

left :: (ABT Term abt, SingI a, SingI b) => abt '[] a -> abt '[] (HEither a b) Source #

right :: (ABT Term abt, SingI a, SingI b) => abt '[] b -> abt '[] (HEither a b) Source #

uneither :: ABT Term abt => abt '[] (HEither a b) -> (abt '[] a -> abt '[] c) -> (abt '[] b -> abt '[] c) -> abt '[] c Source #

HMaybe

nothing :: (ABT Term abt, SingI a) => abt '[] (HMaybe a) Source #

just :: (ABT Term abt, SingI a) => abt '[] a -> abt '[] (HMaybe a) Source #

maybe :: (ABT Term abt, SingI a) => Maybe (abt '[] a) -> abt '[] (HMaybe a) Source #

unmaybe :: ABT Term abt => abt '[] (HMaybe a) -> abt '[] b -> (abt '[] a -> abt '[] b) -> abt '[] b Source #

HList

nil :: (ABT Term abt, SingI a) => abt '[] (HList a) Source #

cons :: (ABT Term abt, SingI a) => abt '[] a -> abt '[] (HList a) -> abt '[] (HList a) Source #

list :: (ABT Term abt, SingI a) => [abt '[] a] -> abt '[] (HList a) Source #

Lambda calculus

lam :: (ABT Term abt, SingI a) => (abt '[] a -> abt '[] b) -> abt '[] (a :-> b) Source #

A variant of lamWithVar for automatically computing the type via sing.

lamWithVar :: ABT Term abt => Text -> Sing a -> (abt '[] a -> abt '[] b) -> abt '[] (a :-> b) Source #

Create a lambda abstraction. The first two arguments give the hint and type of the lambda-bound variable in the result. If you want to automatically fill those in, then see lam.

let_ :: ABT Term abt => abt '[] a -> (abt '[] a -> abt '[] b) -> abt '[] b Source #

app :: ABT Term abt => abt '[] (a :-> b) -> abt '[] a -> abt '[] b infixl 9 Source #

app2 :: ABT Term abt => abt '[] (a :-> (b :-> c)) -> abt '[] a -> abt '[] b -> abt '[] c Source #

app3 :: ABT Term abt => abt '[] (a :-> (b :-> (c :-> d))) -> abt '[] a -> abt '[] b -> abt '[] c -> abt '[] d Source #

Arrays

empty :: (ABT Term abt, SingI a) => abt '[] (HArray a) Source #

arrayWithVar :: ABT Term abt => abt '[] HNat -> Variable HNat -> abt '[] a -> abt '[] (HArray a) Source #

array :: ABT Term abt => abt '[] HNat -> (abt '[] HNat -> abt '[] a) -> abt '[] (HArray a) Source #

(!) :: ABT Term abt => abt '[] (HArray a) -> abt '[] HNat -> abt '[] a infixl 9 Source #

size :: ABT Term abt => abt '[] (HArray a) -> abt '[] HNat Source #

reduce :: ABT Term abt => (abt '[] a -> abt '[] a -> abt '[] a) -> abt '[] a -> abt '[] (HArray a) -> abt '[] a Source #

sumV :: (ABT Term abt, HSemiring_ a) => abt '[] (HArray a) -> abt '[] a Source #

summateV :: ABT Term abt => abt '[] (HArray HProb) -> abt '[] HProb Source #

appendV :: ABT Term abt => abt '[] (HArray a) -> abt '[] (HArray a) -> abt '[] (HArray a) Source #

mapV :: ABT Term abt => (abt '[] a -> abt '[] b) -> abt '[] (HArray a) -> abt '[] (HArray b) Source #

mapWithIndex :: ABT Term abt => (abt '[] HNat -> abt '[] a -> abt '[] b) -> abt '[] (HArray a) -> abt '[] (HArray b) Source #

normalizeV :: ABT Term abt => abt '[] (HArray HProb) -> abt '[] (HArray HProb) Source #

constV :: ABT Term abt => abt '[] HNat -> abt '[] b -> abt '[] (HArray b) Source #

unitV :: ABT Term abt => abt '[] HNat -> abt '[] HNat -> abt '[] (HArray HProb) Source #

zipWithV :: ABT Term abt => (abt '[] a -> abt '[] b -> abt '[] c) -> abt '[] (HArray a) -> abt '[] (HArray b) -> abt '[] (HArray c) Source #

Implementation details

primOp0_ :: ABT Term abt => PrimOp '[] a -> abt '[] a Source #

primOp1_ :: ABT Term abt => PrimOp '[a] b -> abt '[] a -> abt '[] b Source #

primOp2_ :: ABT Term abt => PrimOp '[a, b] c -> abt '[] a -> abt '[] b -> abt '[] c Source #

primOp3_ :: ABT Term abt => PrimOp '[a, b, c] d -> abt '[] a -> abt '[] b -> abt '[] c -> abt '[] d Source #

arrayOp0_ :: ABT Term abt => ArrayOp '[] a -> abt '[] a Source #

arrayOp1_ :: ABT Term abt => ArrayOp '[a] b -> abt '[] a -> abt '[] b Source #

arrayOp2_ :: ABT Term abt => ArrayOp '[a, b] c -> abt '[] a -> abt '[] b -> abt '[] c Source #

arrayOp3_ :: ABT Term abt => ArrayOp '[a, b, c] d -> abt '[] a -> abt '[] b -> abt '[] c -> abt '[] d Source #

measure0_ :: ABT Term abt => MeasureOp '[] a -> abt '[] (HMeasure a) Source #

measure1_ :: ABT Term abt => MeasureOp '[a] b -> abt '[] a -> abt '[] (HMeasure b) Source #

measure2_ :: ABT Term abt => MeasureOp '[a, b] c -> abt '[] a -> abt '[] b -> abt '[] (HMeasure c) Source #

unsafeNaryOp_ :: ABT Term abt => NaryOp a -> [abt '[] a] -> abt '[] a Source #

Apply an n-ary operator to a list. This smart constructor will flatten nested calls to the same operator. And if there is exactly one element in the flattened sequence, then it will remove the NaryOp_ node from the AST.

N.B., if the flattened sequence is empty, this smart constructor will return an AST which applies the operator to the empty sequence; which may or may not be unsafe. If the operator has an identity element, then it's fine (operating on the empty sequence evaluates to the identity element). However, if the operator doesn't have an identity, then the generated code will error whenever we attempt to run it.

naryOp_withIdentity :: ABT Term abt => NaryOp a -> abt '[] a -> [abt '[] a] -> abt '[] a Source #

A variant of unsafeNaryOp_ which will replace operating over the empty sequence with a specified identity element. The produced AST has the same semantics, we're just preemptively evaluating/simplifying the NaryOp_ node of the AST.

N.B., this function does not simplify away the identity element if it exists in the flattened sequence! We should add that in the future.

naryOp2_ :: ABT Term abt => NaryOp a -> abt '[] a -> abt '[] a -> abt '[] a Source #