{-# LANGUAGE CPP , DataKinds , PolyKinds , GADTs , StandaloneDeriving , TypeOperators , TypeFamilies , FlexibleContexts , UndecidableInstances , Rank2Types #-} {-# OPTIONS_GHC -Wall -fwarn-tabs #-} ---------------------------------------------------------------- -- 2016.02.21 -- | -- Module : Language.Hakaru.Syntax.AST -- Copyright : Copyright (c) 2016 the Hakaru team -- License : BSD3 -- Maintainer : wren@community.haskell.org -- Stability : experimental -- Portability : GHC-only -- -- 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 -- -- 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? ---------------------------------------------------------------- module Language.Hakaru.Syntax.AST ( -- * Syntactic forms SCon(..) , SArgs(..) , Term(..) -- * Operators , LC, LCs, UnLCs , LC_(..) , NaryOp(..) , PrimOp(..) , ArrayOp(..) , MeasureOp(..) -- * Constant values , Literal(..) -- * implementation details , foldMapPairs , traversePairs ) where import Data.Sequence (Seq) import qualified Data.Foldable as F import qualified Data.List.NonEmpty as L #if __GLASGOW_HASKELL__ < 710 import Data.Monoid (Monoid(..)) import Control.Applicative import Data.Traversable #endif import Control.Arrow ((***)) import Data.Ratio (numerator, denominator) import Data.Number.Natural import Language.Hakaru.Syntax.IClasses import Language.Hakaru.Types.DataKind import Language.Hakaru.Types.Sing import Language.Hakaru.Types.HClasses import Language.Hakaru.Types.Coercion import Language.Hakaru.Syntax.Datum import Language.Hakaru.Syntax.ABT (ABT(syn)) ---------------------------------------------------------------- ---------------------------------------------------------------- -- BUG: can't UNPACK 'Integer' and 'Natural' like we can for 'Int' and 'Nat' -- -- | 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. data Literal :: Hakaru -> * where LNat :: !Natural -> Literal 'HNat LInt :: !Integer -> Literal 'HInt LProb :: {-# UNPACK #-} !NonNegativeRational -> Literal 'HProb LReal :: {-# UNPACK #-} !Rational -> Literal 'HReal instance JmEq1 Literal where jmEq1 (LNat x) (LNat y) = if x == y then Just Refl else Nothing jmEq1 (LInt x) (LInt y) = if x == y then Just Refl else Nothing jmEq1 (LProb x) (LProb y) = if x == y then Just Refl else Nothing jmEq1 (LReal x) (LReal y) = if x == y then Just Refl else Nothing jmEq1 _ _ = Nothing instance Eq1 Literal where eq1 (LNat x) (LNat y) = x == y eq1 (LInt x) (LInt y) = x == y eq1 (LProb x) (LProb y) = x == y eq1 (LReal x) (LReal y) = x == y eq1 _ _ = False instance Eq (Literal a) where (==) = eq1 -- TODO: instance Read (Literal a) instance Show1 Literal where showsPrec1 p t = case t of LNat v -> showParen_0 p "LNat" v LInt v -> showParen_0 p "LInt" v LProb v -> showParen_0 p "LProb" v -- TODO: pretty print as decimals instead of using the Show Rational instance LReal v -> showParen_0 p "LReal" v -- TODO: pretty print as decimals instead of using the Show Rational instance instance Show (Literal a) where showsPrec = showsPrec1 show = show1 -- TODO: first optimize the @Coercion a b@ to choose the most desirable of many equivalent paths? instance Coerce Literal where coerceTo CNil v = v coerceTo (CCons c cs) v = coerceTo cs (primCoerceTo c v) coerceFrom CNil v = v coerceFrom (CCons c cs) v = primCoerceFrom c (coerceFrom cs v) instance PrimCoerce Literal where primCoerceTo c = case c of Signed HRing_Int -> \(LNat n) -> LInt (nat2int n) Signed HRing_Real -> \(LProb p) -> LReal (prob2real p) Continuous HContinuous_Prob -> \(LNat n) -> LProb (nat2prob n) Continuous HContinuous_Real -> \(LInt i) -> LReal (int2real i) where -- HACK: type signatures needed to avoid defaulting nat2int :: Natural -> Integer nat2int = fromNatural nat2prob :: Natural -> NonNegativeRational nat2prob = unsafeNonNegativeRational . toRational -- N.B., is actually safe here prob2real :: NonNegativeRational -> Rational prob2real = fromNonNegativeRational int2real :: Integer -> Rational int2real = fromIntegral primCoerceFrom c = case c of Signed HRing_Int -> \(LInt i) -> LNat (int2nat i) Signed HRing_Real -> \(LReal r) -> LProb (real2prob r) Continuous HContinuous_Prob -> \(LProb p) -> LNat (prob2nat p) Continuous HContinuous_Real -> \(LReal r) -> LInt (real2int r) where -- HACK: type signatures needed to avoid defaulting -- TODO: how to handle the errors? Generate error code in hakaru? capture it in a monad? int2nat :: Integer -> Natural int2nat x = case toNatural x of Just y -> y Nothing -> error "primCoerceFrom@Literal: negative HInt" prob2nat :: NonNegativeRational -> Natural prob2nat x = if denominator x == 1 then numerator x else error "primCoerceFrom@Literal: non-integral HProb" real2prob :: Rational -> NonNegativeRational real2prob x = case toNonNegativeRational x of Just y -> y Nothing -> error "primCoerceFrom@Literal: negative HReal" real2int :: Rational -> Integer real2int x = if denominator x == 1 then numerator x else error "primCoerceFrom@Literal: non-integral HReal" ---------------------------------------------------------------- -- TODO: helper functions for splitting NaryOp_ into components to group up like things. (e.g., grouping all the Literals together so we can do constant propagation) -- | 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. data NaryOp :: Hakaru -> * where And :: NaryOp HBool Or :: NaryOp HBool Xor :: NaryOp HBool -- N.B., even though 'Iff' is associative (in Boolean algebras), -- we should not support n-ary uses in our *surface* syntax. -- Because it's too easy for folks to confuse "a <=> b <=> c" -- with "(a <=> b) /\ (b <=> c)". Iff :: NaryOp HBool -- == Not (Xor x y) -- These two don't necessarily have identity elements; thus, -- @NaryOp_ Min []@ and @NaryOp_ Max []@ may not be well-defined... -- TODO: check for those cases! Min :: !(HOrd a) -> NaryOp a Max :: !(HOrd a) -> NaryOp a Sum :: !(HSemiring a) -> NaryOp a Prod :: !(HSemiring a) -> NaryOp a {- GCD :: !(GCD_Domain a) -> NaryOp a LCM :: !(GCD_Domain a) -> NaryOp a -} -- TODO: instance Read (NaryOp a) deriving instance Show (NaryOp a) instance JmEq1 NaryOp where jmEq1 And And = Just Refl jmEq1 Or Or = Just Refl jmEq1 Xor Xor = Just Refl jmEq1 Iff Iff = Just Refl jmEq1 (Min a) (Min b) = jmEq1 (sing_HOrd a) (sing_HOrd b) jmEq1 (Max a) (Max b) = jmEq1 (sing_HOrd a) (sing_HOrd b) jmEq1 (Sum a) (Sum b) = jmEq1 a b jmEq1 (Prod a) (Prod b) = jmEq1 a b jmEq1 _ _ = Nothing -- TODO: We could optimize this like we do for 'Literal' instance Eq1 NaryOp where eq1 x y = maybe False (const True) (jmEq1 x y) instance Eq (NaryOp a) where -- This one can be derived (==) = eq1 ---------------------------------------------------------------- -- TODO: should we define our own datakind for @([Hakaru], Hakaru)@ or perhaps for the @/\a -> ([a], Hakaru)@ part of it? -- | Locally closed values (i.e., not binding forms) of a given type. -- TODO: come up with a better name type LC (a :: Hakaru) = '( '[], a ) -- BUG: how to declare that these are inverses? type family LCs (xs :: [Hakaru]) :: [([Hakaru], Hakaru)] where LCs '[] = '[] LCs (x ': xs) = LC x ': LCs xs type family UnLCs (xs :: [([Hakaru], Hakaru)]) :: [Hakaru] where UnLCs '[] = '[] UnLCs ( '( '[], x ) ': xs) = x ': UnLCs xs -- | 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). data PrimOp :: [Hakaru] -> Hakaru -> * where -- -- -- Here we have /monomorphic/ operators -- -- The Boolean operators -- TODO: most of these we'll want to optimize away according -- to some circuit-minimization procedure. But we're not -- committing to any particular minimal complete set of primops -- just yet. -- N.B., general circuit minimization problem is Sigma_2^P-complete, -- which is outside of PTIME; so we'll just have to approximate -- it for now, or link into something like Espresso or an -- implementation of Quine–McCluskey -- cf., -- cf., -- cf., Not :: PrimOp '[ HBool ] HBool -- And, Or, Xor, Iff Impl :: PrimOp '[ HBool, HBool ] HBool -- Impl x y == Or (Not x) y Diff :: PrimOp '[ HBool, HBool ] HBool -- Diff x y == Not (Impl x y) Nand :: PrimOp '[ HBool, HBool ] HBool -- Nand aka Alternative Denial, Sheffer stroke Nor :: PrimOp '[ HBool, HBool ] HBool -- Nor aka Joint Denial, aka Quine dagger, aka Pierce arrow -- -- The remaining eight binops are completely uninteresting: -- flip Impl -- flip Diff -- const -- flip const -- (Not .) . const == const . Not -- (Not .) . flip const -- const (const True) -- const (const False) -- -- Trigonometry operators Pi :: PrimOp '[] 'HProb -- TODO: maybe make this HContinuous polymorphic? -- TODO: if we're going to bother naming the hyperbolic ones, why not also name /a?(csc|sec|cot)h?/ eh? -- TODO: capture more domain information in these types? 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 -- -- Other Real\/Prob-valued operators -- N.B., we only give the safe\/exact versions here. The old -- more lenient versions now require explicit coercions. Some -- of those coercions are safe, but others are not. This way -- we're explicit about where things can fail. -- N.B., we also have @NatPow{'HReal} :: 'HReal -> 'HNat -> 'HReal@, -- but non-integer real powers of negative reals are not real numbers! -- TODO: may need @SafeFrom_@ in order to branch on the input -- in order to provide the old unsafe behavior. RealPow :: PrimOp '[ 'HProb, 'HReal ] 'HProb -- ComplexPow :: PrimOp '[ 'HProb, 'HComplex ] 'HComplex -- is uniquely well-defined. Though we may want to implement -- it via @r**z = ComplexExp (z * RealLog r)@ -- Defining @HReal -> HComplex -> HComplex@ requires either -- multivalued functions, or a choice of complex logarithm and -- making it discontinuous. Exp :: PrimOp '[ 'HReal ] 'HProb Log :: PrimOp '[ 'HProb ] 'HReal -- TODO: Log1p, Expm1 Infinity :: HIntegrable a -> PrimOp '[] a -- TODO: add Factorial as the appropriate type restriction of GammaFunc? GammaFunc :: PrimOp '[ 'HReal ] 'HProb BetaFunc :: PrimOp '[ 'HProb, 'HProb ] 'HProb -- -- -- Here we have the /polymorphic/ operators -- -- HEq and HOrd operators -- TODO: equality doesn't make constructive sense on the reals... -- would it be better to constructivize our notion of total ordering? -- TODO: should we have LessEq as a primitive, rather than treating it as a macro? Equal :: !(HEq a) -> PrimOp '[ a, a ] HBool Less :: !(HOrd a) -> PrimOp '[ a, a ] HBool -- -- HSemiring operators (the non-n-ary ones) NatPow :: !(HSemiring a) -> PrimOp '[ a, 'HNat ] a -- TODO: would it help to have a specialized version for when -- we happen to know that the 'HNat is a Literal? Same goes for -- the other powers\/roots -- -- TODO: add a specialized version which returns NonNegative -- when the power is even? N.B., be sure not to actually constrain -- it to HRing (necessary for calling it \"NonNegative\") -- -- HRing operators -- TODO: break these apart into a hierarchy of classes. N.B, -- there are two different interpretations of "abs" and "signum". -- On the one hand we can think of rings as being generated -- from semirings closed under subtraction/negation. From this -- perspective we have abs as a projection into the underlying -- semiring, and signum as a projection giving us the residual -- sign lost by the abs projection. On the other hand, we have -- the view of "abs" as a norm (i.e., distance to the "origin -- point"), which is the more common perspective for complex -- numbers and vector spaces; and relatedly, we have "signum" -- as returning the value on the unit (hyper)sphere, of the -- normalized unit vector. In another class, if we have a notion -- of an "origin axis" then we can have a function Arg which -- returns the angle to that axis, and therefore define signum -- in terms of Arg. -- Ring: Semiring + negate, abs, signum -- NormedLinearSpace: LinearSpace + originPoint, norm, Arg -- ??: NormedLinearSpace + originAxis, angle Negate :: !(HRing a) -> PrimOp '[ a ] a Abs :: !(HRing a) -> PrimOp '[ a ] (NonNegative a) -- cf., -- cf., -- Should we have Maple5's \"csgn\" as well as the usual \"sgn\"? -- Also note that the \"generalized signum\" anticommutes with Dirac delta! Signum :: !(HRing a) -> PrimOp '[ a ] a -- Law: x = coerceTo_ signed (abs_ x) * signum x -- More strictly/exactly, the result of Signum should be either -- zero or an @a@-unit value. For Int and Real, the units are -- +1 and -1. For Complex, the units are any point on the unit -- circle. For vectors, the units are any unit vector. Thus, -- more generally: -- Law : x = coerceTo_ signed (abs_ x) `scaleBy` signum x -- TODO: would it be worth defining the associated type of unit values for @a@? Probably... -- TODO: are there any salient types which support abs\/norm but -- do not have all units and thus do not support signum\/normalize? -- -- HFractional operators Recip :: !(HFractional a) -> PrimOp '[ a ] a -- generates macro: IntPow -- -- HRadical operators -- TODO: flip argument order to match our prelude's @thRootOf@? NatRoot :: !(HRadical a) -> PrimOp '[ a, 'HNat ] a -- generates macros: Sqrt, NonNegativeRationalPow, and RationalPow -- -- HContinuous operators -- TODO: what goes here, if anything? cf., Erf :: !(HContinuous a) -> PrimOp '[ a ] a -- TODO: make Pi and Infinity HContinuous-polymorphic so that we can avoid the explicit coercion? Probably more mess than benefit. -- TODO: instance Read (PrimOp args a) deriving instance Show (PrimOp args a) instance JmEq2 PrimOp where jmEq2 Not Not = Just (Refl, Refl) jmEq2 Impl Impl = Just (Refl, Refl) jmEq2 Diff Diff = Just (Refl, Refl) jmEq2 Nand Nand = Just (Refl, Refl) jmEq2 Nor Nor = Just (Refl, Refl) jmEq2 Pi Pi = Just (Refl, Refl) jmEq2 Sin Sin = Just (Refl, Refl) jmEq2 Cos Cos = Just (Refl, Refl) jmEq2 Tan Tan = Just (Refl, Refl) jmEq2 Asin Asin = Just (Refl, Refl) jmEq2 Acos Acos = Just (Refl, Refl) jmEq2 Atan Atan = Just (Refl, Refl) jmEq2 Sinh Sinh = Just (Refl, Refl) jmEq2 Cosh Cosh = Just (Refl, Refl) jmEq2 Tanh Tanh = Just (Refl, Refl) jmEq2 Asinh Asinh = Just (Refl, Refl) jmEq2 Acosh Acosh = Just (Refl, Refl) jmEq2 Atanh Atanh = Just (Refl, Refl) jmEq2 RealPow RealPow = Just (Refl, Refl) jmEq2 Exp Exp = Just (Refl, Refl) jmEq2 Log Log = Just (Refl, Refl) jmEq2 GammaFunc GammaFunc = Just (Refl, Refl) jmEq2 BetaFunc BetaFunc = Just (Refl, Refl) jmEq2 (Equal a) (Equal b) = jmEq1 (sing_HEq a) (sing_HEq b) >>= \Refl -> Just (Refl, Refl) jmEq2 (Less a) (Less b) = jmEq1 (sing_HOrd a) (sing_HOrd b) >>= \Refl -> Just (Refl, Refl) jmEq2 (Infinity a) (Infinity b) = jmEq1 (sing_HIntegrable a) (sing_HIntegrable b) >>= \Refl -> Just (Refl, Refl) jmEq2 (NatPow a) (NatPow b) = jmEq1 a b >>= \Refl -> Just (Refl, Refl) jmEq2 (Negate a) (Negate b) = jmEq1 a b >>= \Refl -> Just (Refl, Refl) jmEq2 (Abs a) (Abs b) = jmEq1 a b >>= \Refl -> Just (Refl, Refl) jmEq2 (Signum a) (Signum b) = jmEq1 a b >>= \Refl -> Just (Refl, Refl) jmEq2 (Recip a) (Recip b) = jmEq1 a b >>= \Refl -> Just (Refl, Refl) jmEq2 (NatRoot a) (NatRoot b) = jmEq1 a b >>= \Refl -> Just (Refl, Refl) jmEq2 (Erf a) (Erf b) = jmEq1 a b >>= \Refl -> Just (Refl, Refl) jmEq2 _ _ = Nothing -- TODO: We could optimize this like we do for 'Literal' instance Eq2 PrimOp where eq2 x y = maybe False (const True) (jmEq2 x y) instance Eq1 (PrimOp args) where eq1 = eq2 instance Eq (PrimOp args a) where -- This one can be derived (==) = eq1 ---------------------------------------------------------------- -- | 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 -- 'Language.Hakaru.Syntax.AST.Sing.sing_ArrayOp', that'd be -- better still. data ArrayOp :: [Hakaru] -> Hakaru -> * where -- HACK: is there any way we can avoid storing the Sing values here, while still implementing 'sing_PrimOp'? Index :: !(Sing a) -> ArrayOp '[ 'HArray a, 'HNat ] a Size :: !(Sing a) -> ArrayOp '[ 'HArray a ] 'HNat -- The first argument should be a monoid, but we don't enforce -- that; it's the user's responsibility. Reduce :: !(Sing a) -> ArrayOp '[ a ':-> a ':-> a, a, 'HArray a ] a -- TODO: would it make sense to have a specialized version for when the first argument is some \"Op\", in order to avoid the need for lambdas? -- TODO: instance Read (ArrayOp args a) deriving instance Show (ArrayOp args a) instance JmEq2 ArrayOp where jmEq2 (Index a) (Index b) = jmEq1 a b >>= \Refl -> Just (Refl, Refl) jmEq2 (Size a) (Size b) = jmEq1 a b >>= \Refl -> Just (Refl, Refl) jmEq2 (Reduce a) (Reduce b) = jmEq1 a b >>= \Refl -> Just (Refl, Refl) jmEq2 _ _ = Nothing -- TODO: We could optimize this like we do for 'Literal' instance Eq2 ArrayOp where eq2 x y = maybe False (const True) (jmEq2 x y) instance Eq1 (ArrayOp args) where eq1 = eq2 instance Eq (ArrayOp args a) where -- This one can be derived (==) = eq1 ---------------------------------------------------------------- -- | 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 'Language.Hakaru.Syntax.AST.Sing.sing_MeasureOp', -- that'd be better still. data MeasureOp :: [Hakaru] -> Hakaru -> * where -- We might consider making Lebesgue and Counting polymorphic, -- since their restrictions to HProb and HNat are perfectly -- valid primitive measures. However, there are many other -- restrictions on measures we may want to consider, so handling -- these two here would only complicate matters. Lebesgue :: MeasureOp '[] 'HReal Counting :: MeasureOp '[] 'HInt Categorical :: MeasureOp '[ 'HArray 'HProb ] 'HNat -- TODO: make Uniform polymorphic, so that if the two inputs -- are HProb then we know the measure must be over HProb too. -- More generally, if the first input is HProb (since the second -- input is assumed to be greater thant he first); though that -- would be a bit ugly IMO. Uniform :: MeasureOp '[ 'HReal, 'HReal ] 'HReal Normal :: MeasureOp '[ 'HReal, 'HProb ] 'HReal Poisson :: MeasureOp '[ 'HProb ] 'HNat Gamma :: MeasureOp '[ 'HProb, 'HProb ] 'HProb Beta :: MeasureOp '[ 'HProb, 'HProb ] 'HProb -- TODO: instance Read (MeasureOp typs a) deriving instance Show (MeasureOp typs a) instance JmEq2 MeasureOp where jmEq2 Lebesgue Lebesgue = Just (Refl, Refl) jmEq2 Counting Counting = Just (Refl, Refl) jmEq2 Categorical Categorical = Just (Refl, Refl) jmEq2 Uniform Uniform = Just (Refl, Refl) jmEq2 Normal Normal = Just (Refl, Refl) jmEq2 Poisson Poisson = Just (Refl, Refl) jmEq2 Gamma Gamma = Just (Refl, Refl) jmEq2 Beta Beta = Just (Refl, Refl) jmEq2 _ _ = Nothing -- TODO: We could optimize this like we do for 'Literal' instance Eq2 MeasureOp where eq2 x y = maybe False (const True) (jmEq2 x y) instance Eq1 (MeasureOp typs) where eq1 = eq2 instance Eq (MeasureOp typs a) where -- This one can be derived (==) = eq1 ---------------------------------------------------------------- ---------------------------------------------------------------- -- N.B., the precedence of (:$) must be lower than (:*). -- N.B., if these are changed, then be sure to update the Show instances infix 4 :$ -- Chosen to be at the same precedence as (<$>) rather than ($) infixr 5 :* -- Chosen to match (:) -- | 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'. data SCon :: [([Hakaru], Hakaru)] -> Hakaru -> * where -- BUG: haddock doesn't like annotations on GADT constructors -- -- -- Standard lambda calculus stuff Lam_ :: SCon '[ '( '[ a ], b ) ] (a ':-> b) App_ :: SCon '[ LC (a ':-> b ), LC a ] b Let_ :: SCon '[ LC a, '( '[ a ], b ) ] b -- TODO: a general \"@letrec*@\" version of let-binding so we can have mutual recursion -- -- TODO: if we decide to add arbitrary fixedpoints back in, we -- should probably prefer only recursive-functions: -- `SCon '[ '( '[ a ':-> b, a ], a ':-> b ) ] (a ':-> b)` -- over than the previous recursive-everything: -- `SCon '[ '( '[ a ], a ) ] a` -- Or, if we really want to guarantee soundness, then we should -- only have the inductive principles for each HData. -- -- Type munging CoerceTo_ :: !(Coercion a b) -> SCon '[ LC a ] b UnsafeFrom_ :: !(Coercion a b) -> SCon '[ LC b ] a -- TODO: add something like @SafeFrom_ :: Coercion a b -> abt b -> Term abt ('HMaybe a)@ so we can capture the safety of patterns like @if_ (0 <= x) (let x_ = unsafeFrom signed x in...) (...)@ Of course, since we're just going to do case analysis on the result; why not make it a binding form directly? -- TODO: we'll probably want some more general thing to capture these sorts of patterns. For example, in the default implementation of Uniform we see: @if_ (lo < x && x < hi) (... unsafeFrom_ signed (hi - lo) ...) (...)@ -- HACK: we must add the constraints that 'LCs' and 'UnLCs' are inverses, so that we have those in scope when doing case analysis (e.g., in TypeCheck.hs). -- As for this file itself, we can get it to typecheck by using 'UnLCs' in the argument rather than 'LCs' in the result; trying to do things the other way results in type inference issues in the typeclass instances for 'SCon' 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) -- TODO: unify Plate and Chain as @sequence@ a~la traversable? Plate :: SCon '[ LC 'HNat , '( '[ 'HNat ], 'HMeasure a) ] ('HMeasure ('HArray a)) -- TODO: if we swap the order of arguments to 'Chain', we could -- change the functional argument to be a binding form in order -- to avoid the need for lambdas. It'd no longer be trivial to -- see 'Chain' as an instance of @sequence@, but might be worth -- it... Of course, we also need to handle the fact that it's -- an array of transition functions; i.e., we could do: -- > chain n s0 $ \i s -> do {...} Chain :: SCon '[ LC 'HNat, LC s , '( '[ s ], 'HMeasure (HPair a s)) ] ('HMeasure (HPair ('HArray a) s)) -- -- Continuous and discrete integration. -- TODO: make Integrate and Summate polymorphic, so that if the -- two inputs are HProb then we know the function must be over -- HProb\/HNat too. More generally, if the first input is HProb -- (since the second input is assumed to be greater than the -- first); though that would be a bit ugly IMO. Integrate :: SCon '[ LC 'HReal, LC 'HReal, '( '[ 'HReal ], 'HProb) ] 'HProb -- TODO: the high and low bounds *should* be HInt. The only reason we use HReal is so that we can have infinite summations. Once we figure out a way to handle infinite bounds here, we can make the switch 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 -- -- Internalized program transformations -- TODO: do these belong in their own place? -- -- We generally want to evaluate these away at compile-time, -- but sometimes we may be stuck with a few unresolved things -- for open terms. -- TODO: did we want the singleton @a@ argument back? Expect :: SCon '[ LC ('HMeasure a), '( '[ a ], 'HProb) ] 'HProb -- TODO: implement a \"change of variables\" program transformation -- to map, say, @Lam_ x. blah (Expect x)@ into @Lam x'. blah x'@. -- Or, perhaps rather, transform it into @Lam_ x. App_ (Lam_ x'. blah x') (Expect x)@. -- TODO: add the four ops for disintegration Observe :: SCon '[ LC ('HMeasure a), LC a ] ('HMeasure a) deriving instance Eq (SCon args a) -- TODO: instance Read (SCon args a) deriving instance Show (SCon args a) ---------------------------------------------------------------- -- TODO: ideally we'd like to make SArgs totally flat, like tuples and arrays. Is there a way to do that with data families? -- TODO: is there any good way to reuse 'List1' instead of defining 'SArgs' (aka @List2@)? -- TODO: come up with a better name for 'End' -- TODO: unify this with 'List1'? However, strictness differences... -- -- | 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. data SArgs :: ([Hakaru] -> Hakaru -> *) -> [([Hakaru], Hakaru)] -> * where End :: SArgs abt '[] (:*) :: !(abt vars a) -> !(SArgs abt args) -> SArgs abt ( '(vars, a) ': args) -- TODO: instance Read (SArgs abt args) instance Show2 abt => Show1 (SArgs abt) where showsPrec1 _ End = showString "End" showsPrec1 p (e :* es) = showParen (p > 5) ( showsPrec2 (p+1) e . showString " :* " . showsPrec1 (p+1) es ) instance Show2 abt => Show (SArgs abt args) where showsPrec = showsPrec1 show = show1 instance Eq2 abt => Eq1 (SArgs abt) where eq1 End End = True eq1 (x :* xs) (y :* ys) = eq2 x y && eq1 xs ys eq1 _ _ = False instance Eq2 abt => Eq (SArgs abt args) where (==) = eq1 instance Functor21 SArgs where fmap21 f (e :* es) = f e :* fmap21 f es fmap21 _ End = End instance Foldable21 SArgs where foldMap21 f (e :* es) = f e `mappend` foldMap21 f es foldMap21 _ End = mempty instance Traversable21 SArgs where traverse21 f (e :* es) = (:*) <$> f e <*> traverse21 f es traverse21 _ End = pure End ---------------------------------------------------------------- -- | 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. data Term :: ([Hakaru] -> Hakaru -> *) -> Hakaru -> * where -- BUG: haddock doesn't like annotations on GADT constructors -- -- Simple syntactic forms (i.e., generalized quantifiers) (:$) :: !(SCon args a) -> !(SArgs abt args) -> Term abt a -- N-ary operators NaryOp_ :: !(NaryOp a) -> !(Seq (abt '[] a)) -> Term abt a -- TODO: 'Literal_', 'Empty_', 'Array_', and 'Datum_' are generalized quantifiers (to the same extent that 'Ann_', 'CoerceTo_', and 'UnsafeFrom_' are). Should we move them into 'SCon' just for the sake of minimizing how much lives in 'Term'? Or are they unique enough to be worth keeping here? -- Literal\/Constant values Literal_ :: !(Literal a) -> Term abt a -- These two constructors are here rather than in 'ArrayOp' because 'Array_' is a binding form; though it also means they're together with the other intro forms like 'Literal_' and 'Datum_'. -- -- TODO: should we add a @Sing a@ argument to avoid ambiguity of 'Empty_'? Empty_ :: !(Sing ('HArray a)) -> Term abt ('HArray a) Array_ :: !(abt '[] 'HNat) -> !(abt '[ 'HNat ] a) -> Term abt ('HArray a) -- -- User-defined data types -- BUG: even though the 'Datum' type has a single constructor, we get a warning about not being able to UNPACK it in 'Datum_'... wtf? -- -- A data constructor applied to some expressions. N.B., this -- definition only accounts for data constructors which are -- fully saturated. Unsaturated constructors will need to be -- eta-expanded. Datum_ :: !(Datum (abt '[]) (HData' t)) -> Term abt (HData' t) -- Generic case-analysis (via ABTs and Structural Focalization). Case_ :: !(abt '[] a) -> [Branch a abt b] -> Term abt b -- Linear combinations of measures. Superpose_ :: L.NonEmpty (abt '[] 'HProb, abt '[] ('HMeasure a)) -> Term abt ('HMeasure a) Reject_ :: !(Sing ('HMeasure a)) -> Term abt ('HMeasure a) ---------------------------------------------------------------- -- N.B., having a @singTerm :: Term abt a -> Sing a@ doesn't make -- sense: That's what 'inferType' is for, but not all terms can be -- inferred; some must be checked... Similarly, we can't derive -- Read, since that's what typechecking is all about. -- | 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. newtype LC_ (abt :: [Hakaru] -> Hakaru -> *) (a :: Hakaru) = LC_ { unLC_ :: abt '[] a } instance Show2 abt => Show1 (LC_ abt) where showsPrec1 p = showsPrec2 p . unLC_ show1 = show2 . unLC_ -- Alas, these two instances require importing ABT.hs -- HACK: these instances require -XUndecidableInstances instance ABT Term abt => Coerce (LC_ abt) where coerceTo CNil e = e coerceTo c (LC_ e) = LC_ (syn (CoerceTo_ c :$ e :* End)) coerceFrom CNil e = e coerceFrom c (LC_ e) = LC_ (syn (UnsafeFrom_ c :$ e :* End)) instance ABT Term abt => Coerce (Term abt) where coerceTo CNil e = e coerceTo c e = CoerceTo_ c :$ syn e :* End coerceFrom CNil e = e coerceFrom c e = UnsafeFrom_ c :$ syn e :* End instance Show2 abt => Show1 (Term abt) where showsPrec1 p t = case t of o :$ es -> showParen (p > 4) ( showsPrec (p+1) o . showString " :$ " . showsPrec1 (p+1) es ) NaryOp_ o es -> showParen (p > 9) ( showString "NaryOp_ " . showsPrec 11 o . showString " " . showParen True ( showString "Seq.fromList " . showList2 (F.toList es) ) ) Literal_ v -> showParen_0 p "Literal_" v Empty_ _ -> showString "Empty_" Array_ e1 e2 -> showParen_22 p "Array_" e1 e2 Datum_ d -> showParen_1 p "Datum_" (fmap11 LC_ d) Case_ e bs -> showParen (p > 9) ( showString "Case_ " . showsPrec2 11 e . showString " " . showList1 bs ) Superpose_ pes -> showParen (p > 9) ( showString "Superpose_ " . showListWith (\(e1,e2) -> showTuple [shows2 e1, shows2 e2]) (L.toList pes) ) Reject_ _ -> showString "Reject_" instance Show2 abt => Show (Term abt a) where showsPrec = showsPrec1 show = show1 ---------------------------------------------------------------- instance Functor21 Term where fmap21 f (o :$ es) = o :$ fmap21 f es fmap21 f (NaryOp_ o es) = NaryOp_ o (fmap f es) fmap21 _ (Literal_ v) = Literal_ v fmap21 _ (Empty_ t) = Empty_ t fmap21 f (Array_ e1 e2) = Array_ (f e1) (f e2) fmap21 f (Datum_ d) = Datum_ (fmap11 f d) fmap21 f (Case_ e bs) = Case_ (f e) (map (fmap21 f) bs) fmap21 f (Superpose_ pes) = Superpose_ (L.map (f *** f) pes) fmap21 _ (Reject_ t) = Reject_ t ---------------------------------------------------------------- instance Foldable21 Term where foldMap21 f (_ :$ es) = foldMap21 f es foldMap21 f (NaryOp_ _ es) = F.foldMap f es foldMap21 _ (Literal_ _) = mempty foldMap21 _ (Empty_ _) = mempty foldMap21 f (Array_ e1 e2) = f e1 `mappend` f e2 foldMap21 f (Datum_ d) = foldMap11 f d foldMap21 f (Case_ e bs) = f e `mappend` F.foldMap (foldMap21 f) bs foldMap21 f (Superpose_ pes) = foldMapPairs f pes foldMap21 _ (Reject_ _) = mempty foldMapPairs :: (Monoid m, F.Foldable f) => (forall h i. abt h i -> m) -> f (abt xs a, abt ys b) -> m foldMapPairs f = F.foldMap $ \(e1,e2) -> f e1 `mappend` f e2 ---------------------------------------------------------------- instance Traversable21 Term where traverse21 f (o :$ es) = (o :$) <$> traverse21 f es traverse21 f (NaryOp_ o es) = NaryOp_ o <$> traverse f es traverse21 _ (Literal_ v) = pure $ Literal_ v traverse21 _ (Empty_ typ) = pure $ Empty_ typ traverse21 f (Array_ e1 e2) = Array_ <$> f e1 <*> f e2 traverse21 f (Datum_ d) = Datum_ <$> traverse11 f d traverse21 f (Case_ e bs) = Case_ <$> f e <*> traverse (traverse21 f) bs traverse21 f (Superpose_ pes) = Superpose_ <$> traversePairs f pes traverse21 _ (Reject_ typ) = pure $ Reject_ typ 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)) traversePairs f = traverse $ \(x,y) -> (,) <$> f x <*> f y ---------------------------------------------------------------- ----------------------------------------------------------- fin.