{-# LANGUAGE GADTs, TypeFamilies, ScopedTypeVariables, FlexibleContexts #-} {-# OPTIONS -Wall #-} module Language.Hakaru.Symbolic where import Prelude hiding (Real) data Real data Prob data Measure a data Dist a data Exact class IntComp repr where int :: Integer -> repr Integer class BoolComp repr where bool :: Bool -> repr Bool class RealComp repr where real :: Rational -> repr Real exp :: repr Real -> repr Real -> repr Real sqrt, cos, sin :: repr Real -> repr Real -- polymorphic operations and integer powering -- probably should restrict 'a' to be some kind of numeric type? class SymbComp repr where add, minus, mul :: repr a -> repr a -> repr a pow :: repr Real -> repr Integer -> repr Real scale :: repr Integer -> repr Real -> repr Real class MeasMonad repr where bind :: repr (Measure a) -> (repr a -> repr (Measure b)) -> repr (Measure b) ret :: repr a -> repr (Measure a) class Distrib repr where uniform, normal :: repr Real -> repr Real -> repr (Dist Real) uniformD :: repr Integer -> repr Integer -> repr (Dist Integer) class Conditioning repr where conditioned, unconditioned :: repr (Dist a) -> repr (Measure a) -- Printer (to Maple) data Pos = Front | Back type VarCounter = Int newtype Maple a = Maple { unMaple :: Pos -> VarCounter -> String } type family MPL a type instance MPL Real = Rational type instance MPL Integer = Integer type instance MPL Bool = Bool -- if it weren't for the constraints, we could/should use Applicative pure :: Show (MPL a) => MPL a -> Maple a pure x = Maple $ \_ _ -> show x liftA1 :: (String -> String) -> Maple a -> Maple a liftA1 pr x = Maple $ \f h -> pr (unMaple x f h) liftA2 :: (String -> String -> String) -> Maple a -> Maple a -> Maple a liftA2 pr e1 e2 = Maple $ \f h -> pr (unMaple e1 f h) (unMaple e2 f h) -- variant for ret liftA1M :: (String -> String) -> Maple a -> Maple (Measure a) liftA1M pr x = Maple $ \f h -> pr (unMaple x f h) -- variant for pow liftA2aba :: (String -> String -> String) -> Maple a -> Maple b -> Maple a liftA2aba pr e1 e2 = Maple $ \f h -> pr (unMaple e1 f h) (unMaple e2 f h) -- variant for scale liftA2baa :: (String -> String -> String) -> Maple b -> Maple a -> Maple a liftA2baa pr e1 e2 = Maple $ \f h -> pr (unMaple e1 f h) (unMaple e2 f h) mkPr :: String -> (String -> String) mkPr s t = s ++ "(" ++ t ++ ")" d2m :: Maple (Dist a) -> Maple (Measure a) d2m e = Maple $ unMaple e infixPr :: String -> (String -> String -> String) infixPr s a b = a ++ s ++ b -- This is quite scary. Probably a mistake. reify :: forall a. Read a => Pos -> VarCounter -> Maple a -> a reify f h e = (read (unMaple e f h) :: a) name :: String -> VarCounter -> String name s h = s ++ show h var :: String -> VarCounter -> Maple a var s h = Maple $ \_ _ -> name s h binder :: (String -> String -> Maybe String) -> (String -> String -> VarCounter -> Maybe String) -> String -> Maple a -> Maple a -> Maple (Dist a) binder pr1 pr2 oper e1 e2 = Maple $ pr_ where pr_ Front h = let x1 = unMaple e1 Front h x2 = unMaple e2 Front h in case (pr1 x1 x2, pr2 x1 x2 h) of (Just z, Just w) -> z ++ " * " ++ oper ++ " (" ++ w ++ " * " (Nothing, Just w) -> oper ++ " (" ++ w ++ " * " (Just z, Nothing) -> z ++ " * " ++ oper ++ " (" (Nothing, Nothing) -> oper ++ " (" pr_ Back h = ", " ++ (name "x" h) ++ "=" ++ unMaple e1 Back h ++ ".." ++ unMaple e2 Back h ++ ")" instance RealComp Maple where -- serious problem here: all exact numbers will be printed as -- floats, which will really hamper the use of Maple in any -- serious way. This needs a rethink. real = pure exp = liftA2 $ infixPr "^" sqrt = liftA1 $ mkPr "sqrt" cos = liftA1 $ mkPr "cos" sin = liftA1 $ mkPr "sin" instance SymbComp Maple where add = liftA2 $ infixPr "+" minus = liftA2 $ infixPr "-" mul = liftA2 $ infixPr "*" pow = liftA2aba $ infixPr "^" scale = liftA2baa $ infixPr "*" instance IntComp Maple where int = pure instance BoolComp Maple where bool = pure instance MeasMonad Maple where ret = liftA1M $ mkPr "g" bind m c = Maple $ \f h -> unMaple m Front h ++ unMaple (c $ var "x" h) f (succ h) ++ unMaple m Back h instance Distrib Maple where uniform = binder (\e1 e2 -> Just $ show (1/((read e2 :: Rational) - (read e1 :: Rational)))) (\_ _ _ -> Nothing) "Int" uniformD = binder (\e1 e2 -> let d = (read e2 :: Integer) - (read e1) in if d == 1 then Nothing else Just $ "(1 / " ++ show d ++ ")") (\_ _ _ -> Nothing) "Sum" normal = binder (\_ _ -> Nothing) (\e1 e2 h -> Just $ "PDF (Normal (" ++ e1 ++ ", " ++ e2 ++ "), " ++ (name "x" h) ++ ")") "Int" instance Conditioning Maple where unconditioned = d2m conditioned = d2m view :: Maple a -> String view e = unMaple e Front 0 lift :: Maple Integer -> Maple Real lift x = Maple $ \f h -> unMaple x f h -- TEST CASES exp1, exp2, exp3, exp4 :: Maple (Measure Real) exp1 = unconditioned (uniform (real 1) (real 3)) `bind` ret -- Borel's Paradox Simplified exp2 = unconditioned (uniformD (int 1) (int 3)) `bind` \s -> unconditioned (uniform (real (-1)) (real 1)) `bind` \x -> let y = s `scale` x in ret y -- Borel's Paradox exp3 = unconditioned (uniformD (int 1) (int 2)) `bind` \s -> unconditioned (uniform (real (-1)) (real 1)) `bind` \x -> let y = (Language.Hakaru.Symbolic.sqrt ((real 1 ) `minus` (Language.Hakaru.Symbolic.pow (lift s) (int 2)))) `mul` (Language.Hakaru.Symbolic.sin x) in ret y exp4 = unconditioned (normal (real 1) (real 4)) `bind` ret test, test2, test3, test4 :: String test = view exp1 test2 = view exp2 test3 = view exp3 test4 = view exp4