Language.Hakaru.Syntax.AST

The generating functor for the raw syntax, along with various helper types. For a more tutorial sort of introduction to how things are structured here and in Language.Hakaru.Syntax.ABT, see http://winterkoninkje.dreamwidth.org/103978.html

TODO: are we finally at the place where we can get rid of all those annoying underscores?

TODO: what is the runtime cost of storing all these dictionary singletons? For existential type variables, it should be the same as using a type class constraint; but for non-existential type variables it'll, what, double the size of the AST?

Syntactic forms

data SCon :: [([Hakaru], Hakaru)] -> Hakaru -> * where

The constructor of a (:$) node in the Term. Each of these constructors denotes a "normal/standard/basic" syntactic form (i.e., a generalized quantifier). In the literature, these syntactic forms are sometimes called "operators", but we avoid calling them that so as not to introduce confusion vs PrimOp etc. Instead we use the term "operator" to refer to any primitive function or constant; that is, non-binding syntactic forms. Also in the literature, the SCon type itself is usually called the "signature" of the term language. However, we avoid calling it that since our Term has constructors other than just (:$), so SCon does not give a complete signature for our terms.

The main reason for breaking this type out and using it in conjunction with (:$) and SArgs is so that we can easily pattern match on fully saturated nodes. For example, we want to be able to match MeasureOp_ Uniform :$ lo :* hi :* End without needing to deal with App_ nodes nor viewABT.

Constructors

Lam_ :: SCon '['('[a], b)] (a :-> b)

App_ :: SCon '[LC (a :-> b), LC a] b

Let_ :: SCon '[LC a, '('[a], b)] b

CoerceTo_ :: !(Coercion a b) -> SCon '[LC a] b

UnsafeFrom_ :: !(Coercion a b) -> SCon '[LC b] a

PrimOp_ :: (typs ~ UnLCs args, args ~ LCs typs) => !(PrimOp typs a) -> SCon args a

ArrayOp_ :: (typs ~ UnLCs args, args ~ LCs typs) => !(ArrayOp typs a) -> SCon args a

MeasureOp_ :: (typs ~ UnLCs args, args ~ LCs typs) => !(MeasureOp typs a) -> SCon args (HMeasure a)

Dirac :: SCon '[LC a] (HMeasure a)

MBind :: SCon '[LC (HMeasure a), '('[a], HMeasure b)] (HMeasure b)

Plate :: SCon '[LC HNat, '('[HNat], HMeasure a)] (HMeasure (HArray a))

Chain :: SCon '[LC HNat, LC s, '('[s], HMeasure (HPair a s))] (HMeasure (HPair (HArray a) s))

Integrate :: SCon '[LC HReal, LC HReal, '('[HReal], HProb)] HProb

Summate :: HDiscrete a -> HSemiring b -> SCon '[LC a, LC a, '('[a], b)] b

Product :: HDiscrete a -> HSemiring b -> SCon '[LC a, LC a, '('[a], b)] b

Expect :: SCon '[LC (HMeasure a), '('[a], HProb)] HProb

Observe :: SCon '[LC (HMeasure a), LC a] (HMeasure a)

Instances

Eq (SCon args a)

Methods

(==) :: SCon args a -> SCon args a -> Bool

(/=) :: SCon args a -> SCon args a -> Bool

Show (SCon args a)

Methods

showsPrec :: Int -> SCon args a -> ShowS

show :: SCon args a -> String

showList :: [SCon args a] -> ShowS

data SArgs :: ([Hakaru] -> Hakaru -> *) -> [([Hakaru], Hakaru)] -> * where

The arguments to a (:$) node in the Term; that is, a list of ASTs, where the whole list is indexed by a (type-level) list of the indices of each element.

Constructors

End :: SArgs abt '[]

(:*) :: !(abt vars a) -> !(SArgs abt args) -> SArgs abt ('(vars, a) ': args) infixr 5

Instances

Traversable21 [([Hakaru], Hakaru)] Hakaru [Hakaru] SArgs

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 [Hakaru] SArgs

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 [Hakaru] SArgs

Methods

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

Eq2 Hakaru [Hakaru] abt => Eq1 [([Hakaru], Hakaru)] (SArgs abt)

Methods

eq1 :: a i -> a i -> Bool

Show2 Hakaru [Hakaru] abt => Show1 [([Hakaru], Hakaru)] (SArgs abt)

Methods

showsPrec1 :: Int -> a i -> ShowS

show1 :: a i -> String

Eq2 Hakaru [Hakaru] abt => Eq (SArgs abt args)

Methods

(==) :: SArgs abt args -> SArgs abt args -> Bool

(/=) :: SArgs abt args -> SArgs abt args -> Bool

Show2 Hakaru [Hakaru] abt => Show (SArgs abt args)

Methods

showsPrec :: Int -> SArgs abt args -> ShowS

show :: SArgs abt args -> String

showList :: [SArgs abt args] -> ShowS

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

The generating functor for Hakaru ASTs. This type is given in open-recursive form, where the first type argument gives the recursive form. The recursive form abt does not have exactly the same kind as Term abt because every Term represents a locally-closed term whereas the underlying abt may bind some variables.

Constructors

(:$) :: !(SCon args a) -> !(SArgs abt args) -> Term abt a infix 4

NaryOp_ :: !(NaryOp a) -> !(Seq (abt '[] a)) -> Term abt a

Literal_ :: !(Literal a) -> Term abt a

Empty_ :: !(Sing (HArray a)) -> Term abt (HArray a)

Array_ :: !(abt '[] HNat) -> !(abt '[HNat] a) -> Term abt (HArray a)

Datum_ :: !(Datum (abt '[]) (HData' t)) -> Term abt (HData' t)

Case_ :: !(abt '[] a) -> [Branch a abt b] -> Term abt b

Superpose_ :: NonEmpty (abt '[] HProb, abt '[] (HMeasure a)) -> Term abt (HMeasure a)

Reject_ :: !(Sing (HMeasure a)) -> Term abt (HMeasure a)

Instances

Traversable21 Hakaru Hakaru [Hakaru] Term

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] Term

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] Term

Methods

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

Show2 Hakaru [Hakaru] abt => Show1 Hakaru (Term abt)

Methods

showsPrec1 :: Int -> a i -> ShowS

show1 :: a i -> String

ABT Hakaru Term abt => Coerce (Term abt)

Methods

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

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

Show2 Hakaru [Hakaru] abt => Show (Term abt a)

Methods

showsPrec :: Int -> Term abt a -> ShowS

show :: Term abt a -> String

showList :: [Term abt a] -> ShowS

Operators

type LC a = '('[], a)

Locally closed values (i.e., not binding forms) of a given type. TODO: come up with a better name

type family LCs (xs :: [Hakaru]) :: [([Hakaru], Hakaru)] where ...

Equations

LCs '[] = '[]

LCs (x ': xs) = LC x ': LCs xs

type family UnLCs (xs :: [([Hakaru], Hakaru)]) :: [Hakaru] where ...

Equations

UnLCs '[] = '[]

UnLCs ('('[], x) ': xs) = x ': UnLCs xs

newtype LC_ abt a

A newtype of abt '[], because sometimes we need this in order to give instances for things. In particular, this is often used to derive the obvious Foo1 (abt '[]) instance from an underlying Foo2 abt instance. The primary motivating example is to give the Datum_ branch of the Show1 (Term abt) instance.

Constructors

LC_

Fields

• unLC_ :: abt '[] a

Instances

Show2 Hakaru [Hakaru] abt => Show1 Hakaru (LC_ abt)

Methods

showsPrec1 :: Int -> a i -> ShowS

show1 :: a i -> String

ABT Hakaru Term abt => Coerce (LC_ abt)

Methods

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

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

ABT Hakaru Term abt => Pretty (LC_ abt)

Methods

prettyPrec_ :: Int -> LC_ abt a -> Docs

data NaryOp :: Hakaru -> * where

Primitive associative n-ary functions. By flattening the trees for associative operators, we can more easily perform equivalence checking and pattern matching (e.g., to convert exp (a * log b) into b ** a, regardless of whether a is a product of things or not). Notably, because of this encoding, we encode things like subtraction and division by their unary operators (negation and reciprocal).

We do not make any assumptions about whether these semigroups are monoids, commutative, idempotent, or anything else. That has to be handled by transformations, rather than by the AST itself.

Constructors

And :: NaryOp HBool

Or :: NaryOp HBool

Xor :: NaryOp HBool

Iff :: NaryOp HBool

Min :: !(HOrd a) -> NaryOp a

Max :: !(HOrd a) -> NaryOp a

Sum :: !(HSemiring a) -> NaryOp a

Prod :: !(HSemiring a) -> NaryOp a

Instances

JmEq1 Hakaru NaryOp

Methods

jmEq1 :: a i -> a j -> Maybe (TypeEq NaryOp i j)

Eq1 Hakaru NaryOp

Methods

eq1 :: a i -> a i -> Bool

Eq (NaryOp a)

Methods

(==) :: NaryOp a -> NaryOp a -> Bool

(/=) :: NaryOp a -> NaryOp a -> Bool

Show (NaryOp a)

Methods

showsPrec :: Int -> NaryOp a -> ShowS

show :: NaryOp a -> String

showList :: [NaryOp a] -> ShowS

data PrimOp :: [Hakaru] -> Hakaru -> * where

Simple primitive functions, and constants. N.B., nothing in here should produce or consume things of HMeasure or HArray type (except perhaps in a totally polymorphic way).

Constructors

Not :: PrimOp '[HBool] HBool

Impl :: PrimOp '[HBool, HBool] HBool

Diff :: PrimOp '[HBool, HBool] HBool

Nand :: PrimOp '[HBool, HBool] HBool

Nor :: PrimOp '[HBool, HBool] HBool

Pi :: PrimOp '[] HProb

Sin :: PrimOp '[HReal] HReal

Cos :: PrimOp '[HReal] HReal

Tan :: PrimOp '[HReal] HReal

Asin :: PrimOp '[HReal] HReal

Acos :: PrimOp '[HReal] HReal

Atan :: PrimOp '[HReal] HReal

Sinh :: PrimOp '[HReal] HReal

Cosh :: PrimOp '[HReal] HReal

Tanh :: PrimOp '[HReal] HReal

Asinh :: PrimOp '[HReal] HReal

Acosh :: PrimOp '[HReal] HReal

Atanh :: PrimOp '[HReal] HReal

RealPow :: PrimOp '[HProb, HReal] HProb

Exp :: PrimOp '[HReal] HProb

Log :: PrimOp '[HProb] HReal

Infinity :: HIntegrable a -> PrimOp '[] a

GammaFunc :: PrimOp '[HReal] HProb

BetaFunc :: PrimOp '[HProb, HProb] HProb

Equal :: !(HEq a) -> PrimOp '[a, a] HBool

Less :: !(HOrd a) -> PrimOp '[a, a] HBool

NatPow :: !(HSemiring a) -> PrimOp '[a, HNat] a

Negate :: !(HRing a) -> PrimOp '[a] a

Abs :: !(HRing a) -> PrimOp '[a] (NonNegative a)

Signum :: !(HRing a) -> PrimOp '[a] a

Recip :: !(HFractional a) -> PrimOp '[a] a

NatRoot :: !(HRadical a) -> PrimOp '[a, HNat] a

Erf :: !(HContinuous a) -> PrimOp '[a] a

Instances

Eq1 Hakaru (PrimOp args)

Methods

eq1 :: a i -> a i -> Bool

JmEq2 Hakaru [Hakaru] PrimOp

Methods

jmEq2 :: a i1 j1 -> a i2 j2 -> Maybe (TypeEq k1 i1 i2, TypeEq PrimOp j1 j2)

Eq2 Hakaru [Hakaru] PrimOp

Methods

eq2 :: a i j -> a i j -> Bool

Eq (PrimOp args a)

Methods

(==) :: PrimOp args a -> PrimOp args a -> Bool

(/=) :: PrimOp args a -> PrimOp args a -> Bool

Show (PrimOp args a)

Methods

showsPrec :: Int -> PrimOp args a -> ShowS

show :: PrimOp args a -> String

showList :: [PrimOp args a] -> ShowS

data ArrayOp :: [Hakaru] -> Hakaru -> * where

Primitive operators for consuming or transforming arrays.

TODO: we may want to replace the Sing arguments with something more specific in order to capture any restrictions on what can be stored in an array. Or, if we can get rid of them entirely while still implementing all the use sites of sing_ArrayOp, that'd be better still.

Constructors

Index :: !(Sing a) -> ArrayOp '[HArray a, HNat] a

Size :: !(Sing a) -> ArrayOp '[HArray a] HNat

Reduce :: !(Sing a) -> ArrayOp '[a :-> (a :-> a), a, HArray a] a

Instances

Eq1 Hakaru (ArrayOp args)

Methods

eq1 :: a i -> a i -> Bool

JmEq2 Hakaru [Hakaru] ArrayOp

Methods

jmEq2 :: a i1 j1 -> a i2 j2 -> Maybe (TypeEq k1 i1 i2, TypeEq ArrayOp j1 j2)

Eq2 Hakaru [Hakaru] ArrayOp

Methods

eq2 :: a i j -> a i j -> Bool

Eq (ArrayOp args a)

Methods

(==) :: ArrayOp args a -> ArrayOp args a -> Bool

(/=) :: ArrayOp args a -> ArrayOp args a -> Bool

Show (ArrayOp args a)

Methods

showsPrec :: Int -> ArrayOp args a -> ShowS

show :: ArrayOp args a -> String

showList :: [ArrayOp args a] -> ShowS

data MeasureOp :: [Hakaru] -> Hakaru -> * where

Primitive operators to produce, consume, or transform distributions/measures. This corresponds to the old Mochastic class, except that MBind and Superpose_ are handled elsewhere since they are not simple operators. (Also Dirac is handled elsewhere since it naturally fits with MBind, even though it is a siple operator.)

TODO: we may want to replace the Sing arguments with something more specific in order to capture any restrictions on what can be a measure space (e.g., to exclude functions). Or, if we can get rid of them entirely while still implementing all the use sites of sing_MeasureOp, that'd be better still.

Constructors

Lebesgue :: MeasureOp '[] HReal

Counting :: MeasureOp '[] HInt

Categorical :: MeasureOp '[HArray HProb] HNat

Uniform :: MeasureOp '[HReal, HReal] HReal

Normal :: MeasureOp '[HReal, HProb] HReal

Poisson :: MeasureOp '[HProb] HNat

Gamma :: MeasureOp '[HProb, HProb] HProb

Beta :: MeasureOp '[HProb, HProb] HProb

Instances

Eq1 Hakaru (MeasureOp typs)

Methods

eq1 :: a i -> a i -> Bool

JmEq2 Hakaru [Hakaru] MeasureOp

Methods

jmEq2 :: a i1 j1 -> a i2 j2 -> Maybe (TypeEq k1 i1 i2, TypeEq MeasureOp j1 j2)

Eq2 Hakaru [Hakaru] MeasureOp

Methods

eq2 :: a i j -> a i j -> Bool

Eq (MeasureOp typs a)

Methods

(==) :: MeasureOp typs a -> MeasureOp typs a -> Bool

(/=) :: MeasureOp typs a -> MeasureOp typs a -> Bool

Show (MeasureOp typs a)

Methods

showsPrec :: Int -> MeasureOp typs a -> ShowS

show :: MeasureOp typs a -> String

showList :: [MeasureOp typs a] -> ShowS

Constant values

data Literal :: Hakaru -> * where

Numeric literals for the primitive numeric types. In addition to being normal forms, these are also ground terms: that is, not only are they closed (i.e., no free variables), they also have no bound variables and thus no binding forms. Notably, we store literals using exact types so that none of our program transformations have to worry about issues like overflow or floating-point fuzz.

Constructors

LNat :: !Natural -> Literal HNat

LInt :: !Integer -> Literal HInt

LProb :: !NonNegativeRational -> Literal HProb

LReal :: !Rational -> Literal HReal

Instances

Coerce Literal

Methods

coerceTo :: Coercion a b -> Literal a -> Literal b

coerceFrom :: Coercion a b -> Literal b -> Literal a

PrimCoerce Literal

Methods

primCoerceTo :: PrimCoercion a b -> Literal a -> Literal b

primCoerceFrom :: PrimCoercion a b -> Literal b -> Literal a

Pretty Literal

Methods

prettyPrec_ :: Int -> Literal a -> Docs

JmEq1 Hakaru Literal

Methods

jmEq1 :: a i -> a j -> Maybe (TypeEq Literal i j)

Eq1 Hakaru Literal

Methods

eq1 :: a i -> a i -> Bool

Show1 Hakaru Literal

Methods

showsPrec1 :: Int -> a i -> ShowS

show1 :: a i -> String

Eq (Literal a)

Methods

(==) :: Literal a -> Literal a -> Bool

(/=) :: Literal a -> Literal a -> Bool

Show (Literal a)

Methods

showsPrec :: Int -> Literal a -> ShowS

show :: Literal a -> String

showList :: [Literal a] -> ShowS

implementation details

foldMapPairs :: (Monoid m, Foldable f) => (forall h i. abt h i -> m) -> f (abt xs a, abt ys b) -> m

traversePairs :: (Applicative f, Traversable t) => (forall h i. abt1 h i -> f (abt2 h i)) -> t (abt1 xs a, abt1 ys b) -> f (t (abt2 xs a, abt2 ys b))