{-# LANGUAGE DataKinds
           , TypeOperators
           , NoImplicitPrelude
           , FlexibleContexts
           , GADTs
           , TypeFamilies
           , FlexibleInstances
           , ViewPatterns
           #-}

{-# OPTIONS_GHC -Wall -fwarn-tabs #-}
----------------------------------------------------------------
--                                                    2016.04.21
-- |
-- Module      :  Language.Hakaru.Inference
-- Copyright   :  Copyright (c) 2016 the Hakaru team
-- License     :  BSD3
-- Maintainer  :  wren@community.haskell.org
-- Stability   :  experimental
-- Portability :  GHC-only
--
-- TODO: we may want to give these longer\/more-explicit names so
-- as to be a bit less ambiguous in the larger Haskell ecosystem.
----------------------------------------------------------------
module Language.Hakaru.Inference
    ( priorAsProposal
    , mh, mh'
    , mcmc, mcmc'
    , gibbsProposal
    , slice
    , sliceX
    , incompleteBeta
    , regBeta
    , tCDF
    , approxMh
    , kl
    ) where

import Prelude (($), (.), error, Maybe(..), return)
import qualified Prelude as P
import Language.Hakaru.Types.DataKind
import Language.Hakaru.Types.Sing
import Language.Hakaru.Syntax.AST (Term)
import Language.Hakaru.Syntax.ABT (ABT, binder)
import Language.Hakaru.Syntax.Prelude
import Language.Hakaru.Syntax.Transform (TransformCtx(..), minimalCtx)
import Language.Hakaru.Syntax.TypeOf
import Language.Hakaru.Expect (expect, normalize)
import Language.Hakaru.Disintegrate (determine
                                    ,density, densityInCtx
                                    ,disintegrate, disintegrateInCtx)
import Language.Hakaru.Syntax.IClasses (TypeEq(..), JmEq1(..))

import qualified Data.Text as Text
import Control.Monad.Except (MonadError(..))

import qualified Control.Applicative as P

----------------------------------------------------------------
----------------------------------------------------------------
priorAsProposal
    :: (ABT Term abt, SingI a, SingI b)
    => abt '[] ('HMeasure (HPair a b))
    -> abt '[] (HPair a b)
    -> abt '[] ('HMeasure (HPair a b))
priorAsProposal :: abt '[] ('HMeasure (HPair a b))
-> abt '[] (HPair a b) -> abt '[] ('HMeasure (HPair a b))
priorAsProposal abt '[] ('HMeasure (HPair a b))
p abt '[] (HPair a b)
x =
    abt '[] 'HProb -> abt '[] ('HMeasure HBool)
forall (abt :: [Hakaru] -> Hakaru -> *).
ABT Term abt =>
abt '[] 'HProb -> abt '[] ('HMeasure HBool)
bern (NonNegativeRational -> abt '[] 'HProb
forall (abt :: [Hakaru] -> Hakaru -> *).
ABT Term abt =>
NonNegativeRational -> abt '[] 'HProb
prob_ NonNegativeRational
0.5) abt '[] ('HMeasure HBool)
-> (abt '[] HBool -> abt '[] ('HMeasure (HPair a b)))
-> abt '[] ('HMeasure (HPair a b))
forall (abt :: [Hakaru] -> Hakaru -> *) (a :: Hakaru)
       (b :: Hakaru).
ABT Term abt =>
abt '[] ('HMeasure a)
-> (abt '[] a -> abt '[] ('HMeasure b)) -> abt '[] ('HMeasure b)
>>= \abt '[] HBool
c ->
    abt '[] ('HMeasure (HPair a b))
p abt '[] ('HMeasure (HPair a b))
-> (abt '[] (HPair a b) -> abt '[] ('HMeasure (HPair a b)))
-> abt '[] ('HMeasure (HPair a b))
forall (abt :: [Hakaru] -> Hakaru -> *) (a :: Hakaru)
       (b :: Hakaru).
ABT Term abt =>
abt '[] ('HMeasure a)
-> (abt '[] a -> abt '[] ('HMeasure b)) -> abt '[] ('HMeasure b)
>>= \abt '[] (HPair a b)
x' ->
    abt '[] (HPair a b) -> abt '[] ('HMeasure (HPair a b))
forall (abt :: [Hakaru] -> Hakaru -> *) (a :: Hakaru).
ABT Term abt =>
abt '[] a -> abt '[] ('HMeasure a)
dirac (abt '[] (HPair a b) -> abt '[] ('HMeasure (HPair a b)))
-> abt '[] (HPair a b) -> abt '[] ('HMeasure (HPair a b))
forall a b. (a -> b) -> a -> b
$
        abt '[] HBool
-> abt '[] (HPair a b)
-> abt '[] (HPair a b)
-> abt '[] (HPair a b)
forall (abt :: [Hakaru] -> Hakaru -> *) (a :: Hakaru).
ABT Term abt =>
abt '[] HBool -> abt '[] a -> abt '[] a -> abt '[] a
if_ abt '[] HBool
c
            (abt '[] a -> abt '[] b -> abt '[] (HPair a b)
forall (abt :: [Hakaru] -> Hakaru -> *) (a :: Hakaru)
       (b :: Hakaru).
(ABT Term abt, SingI a, SingI b) =>
abt '[] a -> abt '[] b -> abt '[] (HPair a b)
pair (abt '[] (HPair a b) -> abt '[] a
forall (abt :: [Hakaru] -> Hakaru -> *) (a :: Hakaru)
       (b :: Hakaru).
ABT Term abt =>
abt '[] (HPair a b) -> abt '[] a
fst abt '[] (HPair a b)
x ) (abt '[] (HPair a b) -> abt '[] b
forall (abt :: [Hakaru] -> Hakaru -> *) (a :: Hakaru)
       (b :: Hakaru).
ABT Term abt =>
abt '[] (HPair a b) -> abt '[] b
snd abt '[] (HPair a b)
x'))
            (abt '[] a -> abt '[] b -> abt '[] (HPair a b)
forall (abt :: [Hakaru] -> Hakaru -> *) (a :: Hakaru)
       (b :: Hakaru).
(ABT Term abt, SingI a, SingI b) =>
abt '[] a -> abt '[] b -> abt '[] (HPair a b)
pair (abt '[] (HPair a b) -> abt '[] a
forall (abt :: [Hakaru] -> Hakaru -> *) (a :: Hakaru)
       (b :: Hakaru).
ABT Term abt =>
abt '[] (HPair a b) -> abt '[] a
fst abt '[] (HPair a b)
x') (abt '[] (HPair a b) -> abt '[] b
forall (abt :: [Hakaru] -> Hakaru -> *) (a :: Hakaru)
       (b :: Hakaru).
ABT Term abt =>
abt '[] (HPair a b) -> abt '[] b
snd abt '[] (HPair a b)
x ))


-- We don't do the accept\/reject part of MCMC here, because @min@
-- and @bern@ don't do well in @simplify@! So we'll be passing the
-- resulting AST of 'mh' to 'simplify' before plugging that into
-- @mcmc@; that's why 'easierRoadmapProg4' and 'easierRoadmapProg4''
-- have different types.
--
-- TODO: the @a@ type should be pure (aka @a ~ Expect' a@ in the old parlance).
-- BUG: get rid of the SingI requirements due to using 'lam'
mh'  :: (ABT Term abt)
     => TransformCtx
     -> abt '[] (a ':-> 'HMeasure a)
     -> abt '[] ('HMeasure a)
     -> Maybe (abt '[] (a ':-> 'HMeasure (HPair a 'HProb)))
mh' :: TransformCtx
-> abt '[] (a ':-> 'HMeasure a)
-> abt '[] ('HMeasure a)
-> Maybe (abt '[] (a ':-> 'HMeasure (HPair a 'HProb)))
mh' TransformCtx
ctx abt '[] (a ':-> 'HMeasure a)
proposal abt '[] ('HMeasure a)
target =
        abt '[] (a ':-> 'HProb)
-> (abt '[] (a ':-> 'HProb)
    -> abt '[] (a ':-> 'HMeasure (HPair a 'HProb)))
-> abt '[] (a ':-> 'HMeasure (HPair a 'HProb))
forall (abt :: [Hakaru] -> Hakaru -> *) (a :: Hakaru)
       (b :: Hakaru).
ABT Term abt =>
abt '[] a -> (abt '[] a -> abt '[] b) -> abt '[] b
let_ (abt '[] (a ':-> 'HProb)
 -> (abt '[] (a ':-> 'HProb)
     -> abt '[] (a ':-> 'HMeasure (HPair a 'HProb)))
 -> abt '[] (a ':-> 'HMeasure (HPair a 'HProb)))
-> Maybe (abt '[] (a ':-> 'HProb))
-> Maybe
     ((abt '[] (a ':-> 'HProb)
       -> abt '[] (a ':-> 'HMeasure (HPair a 'HProb)))
      -> abt '[] (a ':-> 'HMeasure (HPair a 'HProb)))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
P.<$> ([abt '[] (a ':-> 'HProb)] -> Maybe (abt '[] (a ':-> 'HProb))
forall (abt :: [Hakaru] -> Hakaru -> *) (a :: Hakaru).
ABT Term abt =>
[abt '[] a] -> Maybe (abt '[] a)
determine ([abt '[] (a ':-> 'HProb)] -> Maybe (abt '[] (a ':-> 'HProb)))
-> [abt '[] (a ':-> 'HProb)] -> Maybe (abt '[] (a ':-> 'HProb))
forall a b. (a -> b) -> a -> b
$ TransformCtx -> abt '[] ('HMeasure a) -> [abt '[] (a ':-> 'HProb)]
forall (abt :: [Hakaru] -> Hakaru -> *) (a :: Hakaru).
ABT Term abt =>
TransformCtx -> abt '[] ('HMeasure a) -> [abt '[] (a ':-> 'HProb)]
densityInCtx TransformCtx
ctx abt '[] ('HMeasure a)
target) Maybe
  ((abt '[] (a ':-> 'HProb)
    -> abt '[] (a ':-> 'HMeasure (HPair a 'HProb)))
   -> abt '[] (a ':-> 'HMeasure (HPair a 'HProb)))
-> Maybe
     (abt '[] (a ':-> 'HProb)
      -> abt '[] (a ':-> 'HMeasure (HPair a 'HProb)))
-> Maybe (abt '[] (a ':-> 'HMeasure (HPair a 'HProb)))
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
P.<*> (abt '[] (a ':-> 'HProb)
 -> abt '[] (a ':-> 'HMeasure (HPair a 'HProb)))
-> Maybe
     (abt '[] (a ':-> 'HProb)
      -> abt '[] (a ':-> 'HMeasure (HPair a 'HProb)))
forall (f :: * -> *) a. Applicative f => a -> f a
P.pure (\abt '[] (a ':-> 'HProb)
mu ->
        (abt '[] a -> abt '[] ('HMeasure (HPair a 'HProb)))
-> abt '[] (a ':-> 'HMeasure (HPair a 'HProb))
lam' ((abt '[] a -> abt '[] ('HMeasure (HPair a 'HProb)))
 -> abt '[] (a ':-> 'HMeasure (HPair a 'HProb)))
-> (abt '[] a -> abt '[] ('HMeasure (HPair a 'HProb)))
-> abt '[] (a ':-> 'HMeasure (HPair a 'HProb))
forall a b. (a -> b) -> a -> b
$ \abt '[] a
old ->
            abt '[] (a ':-> 'HMeasure a) -> abt '[] a -> abt '[] ('HMeasure a)
forall (abt :: [Hakaru] -> Hakaru -> *) (a :: Hakaru)
       (b :: Hakaru).
ABT Term abt =>
abt '[] (a ':-> b) -> abt '[] a -> abt '[] b
app abt '[] (a ':-> 'HMeasure a)
proposal abt '[] a
old abt '[] ('HMeasure a)
-> (abt '[] a -> abt '[] ('HMeasure (HPair a 'HProb)))
-> abt '[] ('HMeasure (HPair a 'HProb))
forall (abt :: [Hakaru] -> Hakaru -> *) (a :: Hakaru)
       (b :: Hakaru).
ABT Term abt =>
abt '[] ('HMeasure a)
-> (abt '[] a -> abt '[] ('HMeasure b)) -> abt '[] ('HMeasure b)
>>= \abt '[] a
new ->
            abt '[] (HPair a 'HProb) -> abt '[] ('HMeasure (HPair a 'HProb))
forall (abt :: [Hakaru] -> Hakaru -> *) (a :: Hakaru).
ABT Term abt =>
abt '[] a -> abt '[] ('HMeasure a)
dirac (abt '[] (HPair a 'HProb) -> abt '[] ('HMeasure (HPair a 'HProb)))
-> abt '[] (HPair a 'HProb) -> abt '[] ('HMeasure (HPair a 'HProb))
forall a b. (a -> b) -> a -> b
$ abt '[] a -> abt '[] 'HProb -> abt '[] (HPair a 'HProb)
pair' abt '[] a
new (abt '[] (a ':-> 'HProb)
mu abt '[] (a ':-> 'HProb) -> abt '[] a -> abt '[] 'HProb
forall (abt :: [Hakaru] -> Hakaru -> *) (a :: Hakaru)
       (b :: Hakaru).
ABT Term abt =>
abt '[] (a ':-> b) -> abt '[] a -> abt '[] b
`app` {-pair-} abt '[] a
new {-old-} abt '[] 'HProb -> abt '[] 'HProb -> abt '[] 'HProb
forall (abt :: [Hakaru] -> Hakaru -> *) (a :: Hakaru).
(ABT Term abt, HFractional_ a) =>
abt '[] a -> abt '[] a -> abt '[] a
/ abt '[] (a ':-> 'HProb)
mu abt '[] (a ':-> 'HProb) -> abt '[] a -> abt '[] 'HProb
forall (abt :: [Hakaru] -> Hakaru -> *) (a :: Hakaru)
       (b :: Hakaru).
ABT Term abt =>
abt '[] (a ':-> b) -> abt '[] a -> abt '[] b
`app` {-pair-} abt '[] a
old {-new-}))
  where lam' :: (abt '[] a -> abt '[] ('HMeasure (HPair a 'HProb)))
-> abt '[] (a ':-> 'HMeasure (HPair a 'HProb))
lam' abt '[] a -> abt '[] ('HMeasure (HPair a 'HProb))
f = Text
-> Sing a
-> (abt '[] a -> abt '[] ('HMeasure (HPair a 'HProb)))
-> abt '[] (a ':-> 'HMeasure (HPair a 'HProb))
forall (abt :: [Hakaru] -> Hakaru -> *) (a :: Hakaru)
       (b :: Hakaru).
ABT Term abt =>
Text -> Sing a -> (abt '[] a -> abt '[] b) -> abt '[] (a ':-> b)
lamWithVar Text
Text.empty (Sing ('HMeasure a) -> Sing a
forall (a :: Hakaru). Sing ('HMeasure a) -> Sing a
sUnMeasure (Sing ('HMeasure a) -> Sing a) -> Sing ('HMeasure a) -> Sing a
forall a b. (a -> b) -> a -> b
$ abt '[] ('HMeasure a) -> Sing ('HMeasure a)
forall (abt :: [Hakaru] -> Hakaru -> *) (a :: Hakaru).
ABT Term abt =>
abt '[] a -> Sing a
typeOf abt '[] ('HMeasure a)
target) abt '[] a -> abt '[] ('HMeasure (HPair a 'HProb))
f
        pair' :: abt '[] a -> abt '[] 'HProb -> abt '[] (HPair a 'HProb)
pair'  = Sing a
-> Sing 'HProb
-> abt '[] a
-> abt '[] 'HProb
-> abt '[] (HPair a 'HProb)
forall (abt :: [Hakaru] -> Hakaru -> *) (a :: Hakaru)
       (b :: Hakaru).
ABT Term abt =>
Sing a -> Sing b -> abt '[] a -> abt '[] b -> abt '[] (HPair a b)
pair_ (Sing ('HMeasure a) -> Sing a
forall (a :: Hakaru). Sing ('HMeasure a) -> Sing a
sUnMeasure (Sing ('HMeasure a) -> Sing a) -> Sing ('HMeasure a) -> Sing a
forall a b. (a -> b) -> a -> b
$ abt '[] ('HMeasure a) -> Sing ('HMeasure a)
forall (abt :: [Hakaru] -> Hakaru -> *) (a :: Hakaru).
ABT Term abt =>
abt '[] a -> Sing a
typeOf abt '[] ('HMeasure a)
target) Sing 'HProb
SProb

mh  :: (ABT Term abt)
     => abt '[] (a ':-> 'HMeasure a)
     -> abt '[] ('HMeasure a)
     -> abt '[] (a ':-> 'HMeasure (HPair a 'HProb))
mh :: abt '[] (a ':-> 'HMeasure a)
-> abt '[] ('HMeasure a)
-> abt '[] (a ':-> 'HMeasure (HPair a 'HProb))
mh abt '[] (a ':-> 'HMeasure a)
proposal abt '[] ('HMeasure a)
target =
  abt '[] (a ':-> 'HMeasure (HPair a 'HProb))
-> (abt '[] (a ':-> 'HMeasure (HPair a 'HProb))
    -> abt '[] (a ':-> 'HMeasure (HPair a 'HProb)))
-> Maybe (abt '[] (a ':-> 'HMeasure (HPair a 'HProb)))
-> abt '[] (a ':-> 'HMeasure (HPair a 'HProb))
forall b a. b -> (a -> b) -> Maybe a -> b
P.maybe ([Char] -> abt '[] (a ':-> 'HMeasure (HPair a 'HProb))
forall a. HasCallStack => [Char] -> a
error [Char]
"mh: couldn't compute density") abt '[] (a ':-> 'HMeasure (HPair a 'HProb))
-> abt '[] (a ':-> 'HMeasure (HPair a 'HProb))
forall a. a -> a
P.id (Maybe (abt '[] (a ':-> 'HMeasure (HPair a 'HProb)))
 -> abt '[] (a ':-> 'HMeasure (HPair a 'HProb)))
-> Maybe (abt '[] (a ':-> 'HMeasure (HPair a 'HProb)))
-> abt '[] (a ':-> 'HMeasure (HPair a 'HProb))
forall a b. (a -> b) -> a -> b
$
  TransformCtx
-> abt '[] (a ':-> 'HMeasure a)
-> abt '[] ('HMeasure a)
-> Maybe (abt '[] (a ':-> 'HMeasure (HPair a 'HProb)))
forall (abt :: [Hakaru] -> Hakaru -> *) (a :: Hakaru).
ABT Term abt =>
TransformCtx
-> abt '[] (a ':-> 'HMeasure a)
-> abt '[] ('HMeasure a)
-> Maybe (abt '[] (a ':-> 'HMeasure (HPair a 'HProb)))
mh' TransformCtx
minimalCtx abt '[] (a ':-> 'HMeasure a)
proposal abt '[] ('HMeasure a)
target

-- BUG: get rid of the SingI requirements due to using 'lam' in 'mh'
mcmc' :: (ABT Term abt)
      => TransformCtx
      -> abt '[] (a ':-> 'HMeasure a)
      -> abt '[] ('HMeasure a)
      -> Maybe (abt '[] (a ':-> 'HMeasure a))
mcmc' :: TransformCtx
-> abt '[] (a ':-> 'HMeasure a)
-> abt '[] ('HMeasure a)
-> Maybe (abt '[] (a ':-> 'HMeasure a))
mcmc' TransformCtx
ctx abt '[] (a ':-> 'HMeasure a)
proposal abt '[] ('HMeasure a)
target =
    abt '[] (a ':-> 'HMeasure (HPair a 'HProb))
-> (abt '[] (a ':-> 'HMeasure (HPair a 'HProb))
    -> abt '[] (a ':-> 'HMeasure a))
-> abt '[] (a ':-> 'HMeasure a)
forall (abt :: [Hakaru] -> Hakaru -> *) (a :: Hakaru)
       (b :: Hakaru).
ABT Term abt =>
abt '[] a -> (abt '[] a -> abt '[] b) -> abt '[] b
let_ (abt '[] (a ':-> 'HMeasure (HPair a 'HProb))
 -> (abt '[] (a ':-> 'HMeasure (HPair a 'HProb))
     -> abt '[] (a ':-> 'HMeasure a))
 -> abt '[] (a ':-> 'HMeasure a))
-> Maybe (abt '[] (a ':-> 'HMeasure (HPair a 'HProb)))
-> Maybe
     ((abt '[] (a ':-> 'HMeasure (HPair a 'HProb))
       -> abt '[] (a ':-> 'HMeasure a))
      -> abt '[] (a ':-> 'HMeasure a))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
P.<$> TransformCtx
-> abt '[] (a ':-> 'HMeasure a)
-> abt '[] ('HMeasure a)
-> Maybe (abt '[] (a ':-> 'HMeasure (HPair a 'HProb)))
forall (abt :: [Hakaru] -> Hakaru -> *) (a :: Hakaru).
ABT Term abt =>
TransformCtx
-> abt '[] (a ':-> 'HMeasure a)
-> abt '[] ('HMeasure a)
-> Maybe (abt '[] (a ':-> 'HMeasure (HPair a 'HProb)))
mh' TransformCtx
ctx abt '[] (a ':-> 'HMeasure a)
proposal abt '[] ('HMeasure a)
target Maybe
  ((abt '[] (a ':-> 'HMeasure (HPair a 'HProb))
    -> abt '[] (a ':-> 'HMeasure a))
   -> abt '[] (a ':-> 'HMeasure a))
-> Maybe
     (abt '[] (a ':-> 'HMeasure (HPair a 'HProb))
      -> abt '[] (a ':-> 'HMeasure a))
-> Maybe (abt '[] (a ':-> 'HMeasure a))
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
P.<*> (abt '[] (a ':-> 'HMeasure (HPair a 'HProb))
 -> abt '[] (a ':-> 'HMeasure a))
-> Maybe
     (abt '[] (a ':-> 'HMeasure (HPair a 'HProb))
      -> abt '[] (a ':-> 'HMeasure a))
forall (f :: * -> *) a. Applicative f => a -> f a
P.pure (\abt '[] (a ':-> 'HMeasure (HPair a 'HProb))
f ->
    Text
-> Sing a
-> (abt '[] a -> abt '[] ('HMeasure a))
-> abt '[] (a ':-> 'HMeasure a)
forall (abt :: [Hakaru] -> Hakaru -> *) (a :: Hakaru)
       (b :: Hakaru).
ABT Term abt =>
Text -> Sing a -> (abt '[] a -> abt '[] b) -> abt '[] (a ':-> b)
lamWithVar Text
Text.empty (Sing ('HMeasure a) -> Sing a
forall (a :: Hakaru). Sing ('HMeasure a) -> Sing a
sUnMeasure (Sing ('HMeasure a) -> Sing a) -> Sing ('HMeasure a) -> Sing a
forall a b. (a -> b) -> a -> b
$ abt '[] ('HMeasure a) -> Sing ('HMeasure a)
forall (abt :: [Hakaru] -> Hakaru -> *) (a :: Hakaru).
ABT Term abt =>
abt '[] a -> Sing a
typeOf abt '[] ('HMeasure a)
target) ((abt '[] a -> abt '[] ('HMeasure a))
 -> abt '[] (a ':-> 'HMeasure a))
-> (abt '[] a -> abt '[] ('HMeasure a))
-> abt '[] (a ':-> 'HMeasure a)
forall a b. (a -> b) -> a -> b
$ \abt '[] a
old ->
        abt '[] (a ':-> 'HMeasure (HPair a 'HProb))
-> abt '[] a -> abt '[] ('HMeasure (HPair a 'HProb))
forall (abt :: [Hakaru] -> Hakaru -> *) (a :: Hakaru)
       (b :: Hakaru).
ABT Term abt =>
abt '[] (a ':-> b) -> abt '[] a -> abt '[] b
app abt '[] (a ':-> 'HMeasure (HPair a 'HProb))
f abt '[] a
old abt '[] ('HMeasure (HPair a 'HProb))
-> (abt '[] (HPair a 'HProb) -> abt '[] ('HMeasure a))
-> abt '[] ('HMeasure a)
forall (abt :: [Hakaru] -> Hakaru -> *) (a :: Hakaru)
       (b :: Hakaru).
ABT Term abt =>
abt '[] ('HMeasure a)
-> (abt '[] a -> abt '[] ('HMeasure b)) -> abt '[] ('HMeasure b)
>>= \abt '[] (HPair a 'HProb)
new_ratio ->
        abt '[] (HPair a 'HProb)
new_ratio abt '[] (HPair a 'HProb)
-> (abt '[] a -> abt '[] 'HProb -> abt '[] ('HMeasure a))
-> abt '[] ('HMeasure a)
forall (abt :: [Hakaru] -> Hakaru -> *) (a :: Hakaru) (b :: Hakaru)
       (c :: Hakaru).
ABT Term abt =>
abt '[] (HPair a b)
-> (abt '[] a -> abt '[] b -> abt '[] c) -> abt '[] c
`unpair` \abt '[] a
new abt '[] 'HProb
ratio ->
        abt '[] 'HProb -> abt '[] ('HMeasure HBool)
forall (abt :: [Hakaru] -> Hakaru -> *).
ABT Term abt =>
abt '[] 'HProb -> abt '[] ('HMeasure HBool)
bern (abt '[] 'HProb -> abt '[] 'HProb -> abt '[] 'HProb
forall (abt :: [Hakaru] -> Hakaru -> *) (a :: Hakaru).
(ABT Term abt, HOrd_ a) =>
abt '[] a -> abt '[] a -> abt '[] a
min (NonNegativeRational -> abt '[] 'HProb
forall (abt :: [Hakaru] -> Hakaru -> *).
ABT Term abt =>
NonNegativeRational -> abt '[] 'HProb
prob_ NonNegativeRational
1) abt '[] 'HProb
ratio) abt '[] ('HMeasure HBool)
-> (abt '[] HBool -> abt '[] ('HMeasure a))
-> abt '[] ('HMeasure a)
forall (abt :: [Hakaru] -> Hakaru -> *) (a :: Hakaru)
       (b :: Hakaru).
ABT Term abt =>
abt '[] ('HMeasure a)
-> (abt '[] a -> abt '[] ('HMeasure b)) -> abt '[] ('HMeasure b)
>>= \abt '[] HBool
accept ->
        abt '[] a -> abt '[] ('HMeasure a)
forall (abt :: [Hakaru] -> Hakaru -> *) (a :: Hakaru).
ABT Term abt =>
abt '[] a -> abt '[] ('HMeasure a)
dirac (abt '[] HBool -> abt '[] a -> abt '[] a -> abt '[] a
forall (abt :: [Hakaru] -> Hakaru -> *) (a :: Hakaru).
ABT Term abt =>
abt '[] HBool -> abt '[] a -> abt '[] a -> abt '[] a
if_ abt '[] HBool
accept abt '[] a
new abt '[] a
old))

mcmc :: (ABT Term abt)
     => abt '[] (a ':-> 'HMeasure a)
     -> abt '[] ('HMeasure a)
     -> abt '[] (a ':-> 'HMeasure a)
mcmc :: abt '[] (a ':-> 'HMeasure a)
-> abt '[] ('HMeasure a) -> abt '[] (a ':-> 'HMeasure a)
mcmc abt '[] (a ':-> 'HMeasure a)
proposal abt '[] ('HMeasure a)
target =
  abt '[] (a ':-> 'HMeasure a)
-> (abt '[] (a ':-> 'HMeasure a) -> abt '[] (a ':-> 'HMeasure a))
-> Maybe (abt '[] (a ':-> 'HMeasure a))
-> abt '[] (a ':-> 'HMeasure a)
forall b a. b -> (a -> b) -> Maybe a -> b
P.maybe ([Char] -> abt '[] (a ':-> 'HMeasure a)
forall a. HasCallStack => [Char] -> a
error [Char]
"mcmc: couldn't compute density") abt '[] (a ':-> 'HMeasure a) -> abt '[] (a ':-> 'HMeasure a)
forall a. a -> a
P.id (Maybe (abt '[] (a ':-> 'HMeasure a))
 -> abt '[] (a ':-> 'HMeasure a))
-> Maybe (abt '[] (a ':-> 'HMeasure a))
-> abt '[] (a ':-> 'HMeasure a)
forall a b. (a -> b) -> a -> b
$
  TransformCtx
-> abt '[] (a ':-> 'HMeasure a)
-> abt '[] ('HMeasure a)
-> Maybe (abt '[] (a ':-> 'HMeasure a))
forall (abt :: [Hakaru] -> Hakaru -> *) (a :: Hakaru).
ABT Term abt =>
TransformCtx
-> abt '[] (a ':-> 'HMeasure a)
-> abt '[] ('HMeasure a)
-> Maybe (abt '[] (a ':-> 'HMeasure a))
mcmc' TransformCtx
minimalCtx abt '[] (a ':-> 'HMeasure a)
proposal abt '[] ('HMeasure a)
target

gibbsProposal
    :: (ABT Term abt, SingI a, SingI b)
    => abt '[] ('HMeasure (HPair a b))
    -> abt '[] (HPair a b)
    -> abt '[] ('HMeasure (HPair a b))
gibbsProposal :: abt '[] ('HMeasure (HPair a b))
-> abt '[] (HPair a b) -> abt '[] ('HMeasure (HPair a b))
gibbsProposal abt '[] ('HMeasure (HPair a b))
p abt '[] (HPair a b)
xy =
    case [abt '[] (a ':-> 'HMeasure b)]
-> Maybe (abt '[] (a ':-> 'HMeasure b))
forall (abt :: [Hakaru] -> Hakaru -> *) (a :: Hakaru).
ABT Term abt =>
[abt '[] a] -> Maybe (abt '[] a)
determine ([abt '[] (a ':-> 'HMeasure b)]
 -> Maybe (abt '[] (a ':-> 'HMeasure b)))
-> [abt '[] (a ':-> 'HMeasure b)]
-> Maybe (abt '[] (a ':-> 'HMeasure b))
forall a b. (a -> b) -> a -> b
$ abt '[] ('HMeasure (HPair a b)) -> [abt '[] (a ':-> 'HMeasure b)]
forall (abt :: [Hakaru] -> Hakaru -> *) (a :: Hakaru)
       (b :: Hakaru).
ABT Term abt =>
abt '[] ('HMeasure (HPair a b)) -> [abt '[] (a ':-> 'HMeasure b)]
disintegrate abt '[] ('HMeasure (HPair a b))
p of
    Maybe (abt '[] (a ':-> 'HMeasure b))
Nothing -> [Char] -> abt '[] ('HMeasure (HPair a b))
forall a. HasCallStack => [Char] -> a
error [Char]
"gibbsProposal: couldn't disintegrate"
    Just abt '[] (a ':-> 'HMeasure b)
q ->
        abt '[] (HPair a b)
xy abt '[] (HPair a b)
-> (abt '[] a -> abt '[] b -> abt '[] ('HMeasure (HPair a b)))
-> abt '[] ('HMeasure (HPair a b))
forall (abt :: [Hakaru] -> Hakaru -> *) (a :: Hakaru) (b :: Hakaru)
       (c :: Hakaru).
ABT Term abt =>
abt '[] (HPair a b)
-> (abt '[] a -> abt '[] b -> abt '[] c) -> abt '[] c
`unpair` \abt '[] a
x abt '[] b
_y ->
        abt '[] a -> abt '[] b -> abt '[] (HPair a b)
forall (abt :: [Hakaru] -> Hakaru -> *) (a :: Hakaru)
       (b :: Hakaru).
(ABT Term abt, SingI a, SingI b) =>
abt '[] a -> abt '[] b -> abt '[] (HPair a b)
pair abt '[] a
x (abt '[] b -> abt '[] (HPair a b))
-> abt '[] ('HMeasure b) -> abt '[] ('HMeasure (HPair a b))
forall (abt :: [Hakaru] -> Hakaru -> *) (a :: Hakaru)
       (b :: Hakaru).
(ABT Term abt, SingI a) =>
(abt '[] a -> abt '[] b)
-> abt '[] ('HMeasure a) -> abt '[] ('HMeasure b)
<$> abt '[] ('HMeasure b) -> abt '[] ('HMeasure b)
forall (abt :: [Hakaru] -> Hakaru -> *) (a :: Hakaru).
ABT Term abt =>
abt '[] ('HMeasure a) -> abt '[] ('HMeasure a)
normalize (abt '[] (a ':-> 'HMeasure b)
q abt '[] (a ':-> 'HMeasure b) -> abt '[] a -> abt '[] ('HMeasure b)
forall (abt :: [Hakaru] -> Hakaru -> *) (a :: Hakaru)
       (b :: Hakaru).
ABT Term abt =>
abt '[] (a ':-> b) -> abt '[] a -> abt '[] b
`app` abt '[] a
x)


-- Slice sampling can be thought of:
--
-- slice target x = do
--      u  <- uniform(0, density(target, x))
--      x' <- lebesgue
--      condition (density(target, x') >= u) true
--      return x'

slice
    :: (ABT Term abt)
    => abt '[] ('HMeasure 'HReal)
    -> abt '[] ('HReal ':-> 'HMeasure 'HReal)
slice :: abt '[] ('HMeasure 'HReal)
-> abt '[] ('HReal ':-> 'HMeasure 'HReal)
slice abt '[] ('HMeasure 'HReal)
target =
    case [abt '[] ('HReal ':-> 'HProb)]
-> Maybe (abt '[] ('HReal ':-> 'HProb))
forall (abt :: [Hakaru] -> Hakaru -> *) (a :: Hakaru).
ABT Term abt =>
[abt '[] a] -> Maybe (abt '[] a)
determine ([abt '[] ('HReal ':-> 'HProb)]
 -> Maybe (abt '[] ('HReal ':-> 'HProb)))
-> [abt '[] ('HReal ':-> 'HProb)]
-> Maybe (abt '[] ('HReal ':-> 'HProb))
forall a b. (a -> b) -> a -> b
$ abt '[] ('HMeasure 'HReal) -> [abt '[] ('HReal ':-> 'HProb)]
forall (abt :: [Hakaru] -> Hakaru -> *) (a :: Hakaru).
ABT Term abt =>
abt '[] ('HMeasure a) -> [abt '[] (a ':-> 'HProb)]
density abt '[] ('HMeasure 'HReal)
target of
    Maybe (abt '[] ('HReal ':-> 'HProb))
Nothing -> [Char] -> abt '[] ('HReal ':-> 'HMeasure 'HReal)
forall a. HasCallStack => [Char] -> a
error [Char]
"slice: couldn't get density"
    Just abt '[] ('HReal ':-> 'HProb)
densAt ->
        (abt '[] 'HReal -> abt '[] ('HMeasure 'HReal))
-> abt '[] ('HReal ':-> 'HMeasure 'HReal)
forall (abt :: [Hakaru] -> Hakaru -> *) (a :: Hakaru)
       (b :: Hakaru).
(ABT Term abt, SingI a) =>
(abt '[] a -> abt '[] b) -> abt '[] (a ':-> b)
lam ((abt '[] 'HReal -> abt '[] ('HMeasure 'HReal))
 -> abt '[] ('HReal ':-> 'HMeasure 'HReal))
-> (abt '[] 'HReal -> abt '[] ('HMeasure 'HReal))
-> abt '[] ('HReal ':-> 'HMeasure 'HReal)
forall a b. (a -> b) -> a -> b
$ \abt '[] 'HReal
x ->
        abt '[] 'HReal -> abt '[] 'HReal -> abt '[] ('HMeasure 'HReal)
forall (abt :: [Hakaru] -> Hakaru -> *).
ABT Term abt =>
abt '[] 'HReal -> abt '[] 'HReal -> abt '[] ('HMeasure 'HReal)
uniform (Rational -> abt '[] 'HReal
forall (abt :: [Hakaru] -> Hakaru -> *).
ABT Term abt =>
Rational -> abt '[] 'HReal
real_ Rational
0) (abt '[] 'HProb -> abt '[] 'HReal
forall (abt :: [Hakaru] -> Hakaru -> *).
ABT Term abt =>
abt '[] 'HProb -> abt '[] 'HReal
fromProb (abt '[] 'HProb -> abt '[] 'HReal)
-> abt '[] 'HProb -> abt '[] 'HReal
forall a b. (a -> b) -> a -> b
$ abt '[] ('HReal ':-> 'HProb) -> abt '[] 'HReal -> abt '[] 'HProb
forall (abt :: [Hakaru] -> Hakaru -> *) (a :: Hakaru)
       (b :: Hakaru).
ABT Term abt =>
abt '[] (a ':-> b) -> abt '[] a -> abt '[] b
app abt '[] ('HReal ':-> 'HProb)
densAt abt '[] 'HReal
x) abt '[] ('HMeasure 'HReal)
-> (abt '[] 'HReal -> abt '[] ('HMeasure 'HReal))
-> abt '[] ('HMeasure 'HReal)
forall (abt :: [Hakaru] -> Hakaru -> *) (a :: Hakaru)
       (b :: Hakaru).
ABT Term abt =>
abt '[] ('HMeasure a)
-> (abt '[] a -> abt '[] ('HMeasure b)) -> abt '[] ('HMeasure b)
>>= \abt '[] 'HReal
u ->
        abt '[] ('HMeasure 'HReal) -> abt '[] ('HMeasure 'HReal)
forall (abt :: [Hakaru] -> Hakaru -> *) (a :: Hakaru).
ABT Term abt =>
abt '[] ('HMeasure a) -> abt '[] ('HMeasure a)
normalize (abt '[] ('HMeasure 'HReal) -> abt '[] ('HMeasure 'HReal))
-> abt '[] ('HMeasure 'HReal) -> abt '[] ('HMeasure 'HReal)
forall a b. (a -> b) -> a -> b
$
        abt '[] ('HMeasure 'HReal)
forall (abt :: [Hakaru] -> Hakaru -> *).
ABT Term abt =>
abt '[] ('HMeasure 'HReal)
lebesgue abt '[] ('HMeasure 'HReal)
-> (abt '[] 'HReal -> abt '[] ('HMeasure 'HReal))
-> abt '[] ('HMeasure 'HReal)
forall (abt :: [Hakaru] -> Hakaru -> *) (a :: Hakaru)
       (b :: Hakaru).
ABT Term abt =>
abt '[] ('HMeasure a)
-> (abt '[] a -> abt '[] ('HMeasure b)) -> abt '[] ('HMeasure b)
>>= \abt '[] 'HReal
x' ->
        abt '[] HBool
-> abt '[] ('HMeasure 'HReal) -> abt '[] ('HMeasure 'HReal)
forall (abt :: [Hakaru] -> Hakaru -> *) (a :: Hakaru).
ABT Term abt =>
abt '[] HBool -> abt '[] ('HMeasure a) -> abt '[] ('HMeasure a)
withGuard (abt '[] 'HReal
u abt '[] 'HReal -> abt '[] 'HReal -> abt '[] HBool
forall (abt :: [Hakaru] -> Hakaru -> *) (a :: Hakaru).
(ABT Term abt, HOrd_ a) =>
abt '[] a -> abt '[] a -> abt '[] HBool
< (abt '[] 'HProb -> abt '[] 'HReal
forall (abt :: [Hakaru] -> Hakaru -> *).
ABT Term abt =>
abt '[] 'HProb -> abt '[] 'HReal
fromProb (abt '[] 'HProb -> abt '[] 'HReal)
-> abt '[] 'HProb -> abt '[] 'HReal
forall a b. (a -> b) -> a -> b
$ abt '[] ('HReal ':-> 'HProb) -> abt '[] 'HReal -> abt '[] 'HProb
forall (abt :: [Hakaru] -> Hakaru -> *) (a :: Hakaru)
       (b :: Hakaru).
ABT Term abt =>
abt '[] (a ':-> b) -> abt '[] a -> abt '[] b
app abt '[] ('HReal ':-> 'HProb)
densAt abt '[] 'HReal
x')) (abt '[] ('HMeasure 'HReal) -> abt '[] ('HMeasure 'HReal))
-> abt '[] ('HMeasure 'HReal) -> abt '[] ('HMeasure 'HReal)
forall a b. (a -> b) -> a -> b
$
        abt '[] 'HReal -> abt '[] ('HMeasure 'HReal)
forall (abt :: [Hakaru] -> Hakaru -> *) (a :: Hakaru).
ABT Term abt =>
abt '[] a -> abt '[] ('HMeasure a)
dirac abt '[] 'HReal
x'


sliceX
    :: (ABT Term abt, SingI a)
    => abt '[] ('HMeasure a)
    -> abt '[] ('HMeasure (HPair a 'HReal))
sliceX :: abt '[] ('HMeasure a) -> abt '[] ('HMeasure (HPair a 'HReal))
sliceX abt '[] ('HMeasure a)
target =
    case [abt '[] (a ':-> 'HProb)] -> Maybe (abt '[] (a ':-> 'HProb))
forall (abt :: [Hakaru] -> Hakaru -> *) (a :: Hakaru).
ABT Term abt =>
[abt '[] a] -> Maybe (abt '[] a)
determine ([abt '[] (a ':-> 'HProb)] -> Maybe (abt '[] (a ':-> 'HProb)))
-> [abt '[] (a ':-> 'HProb)] -> Maybe (abt '[] (a ':-> 'HProb))
forall a b. (a -> b) -> a -> b
$ abt '[] ('HMeasure a) -> [abt '[] (a ':-> 'HProb)]
forall (abt :: [Hakaru] -> Hakaru -> *) (a :: Hakaru).
ABT Term abt =>
abt '[] ('HMeasure a) -> [abt '[] (a ':-> 'HProb)]
density abt '[] ('HMeasure a)
target of
    Maybe (abt '[] (a ':-> 'HProb))
Nothing -> [Char] -> abt '[] ('HMeasure (HPair a 'HReal))
forall a. HasCallStack => [Char] -> a
error [Char]
"sliceX: couldn't get density"
    Just abt '[] (a ':-> 'HProb)
densAt ->
        abt '[] ('HMeasure a)
target abt '[] ('HMeasure a)
-> (abt '[] a -> abt '[] ('HMeasure 'HReal))
-> abt '[] ('HMeasure (HPair a 'HReal))
forall (abt :: [Hakaru] -> Hakaru -> *) (a :: Hakaru)
       (b :: Hakaru).
(ABT Term abt, SingI a, SingI b) =>
abt '[] ('HMeasure a)
-> (abt '[] a -> abt '[] ('HMeasure b))
-> abt '[] ('HMeasure (HPair a b))
`bindx` \abt '[] a
x ->
        abt '[] 'HReal -> abt '[] 'HReal -> abt '[] ('HMeasure 'HReal)
forall (abt :: [Hakaru] -> Hakaru -> *).
ABT Term abt =>
abt '[] 'HReal -> abt '[] 'HReal -> abt '[] ('HMeasure 'HReal)
uniform (Rational -> abt '[] 'HReal
forall (abt :: [Hakaru] -> Hakaru -> *).
ABT Term abt =>
Rational -> abt '[] 'HReal
real_ Rational
0) (abt '[] 'HProb -> abt '[] 'HReal
forall (abt :: [Hakaru] -> Hakaru -> *).
ABT Term abt =>
abt '[] 'HProb -> abt '[] 'HReal
fromProb (abt '[] 'HProb -> abt '[] 'HReal)
-> abt '[] 'HProb -> abt '[] 'HReal
forall a b. (a -> b) -> a -> b
$ abt '[] (a ':-> 'HProb) -> abt '[] a -> abt '[] 'HProb
forall (abt :: [Hakaru] -> Hakaru -> *) (a :: Hakaru)
       (b :: Hakaru).
ABT Term abt =>
abt '[] (a ':-> b) -> abt '[] a -> abt '[] b
app abt '[] (a ':-> 'HProb)
densAt abt '[] a
x)


incompleteBeta
    :: (ABT Term abt)
    => abt '[] 'HProb
    -> abt '[] 'HProb
    -> abt '[] 'HProb
    -> abt '[] 'HProb
incompleteBeta :: abt '[] 'HProb
-> abt '[] 'HProb -> abt '[] 'HProb -> abt '[] 'HProb
incompleteBeta abt '[] 'HProb
x abt '[] 'HProb
a abt '[] 'HProb
b =
    let one' :: abt '[] 'HReal
one' = Rational -> abt '[] 'HReal
forall (abt :: [Hakaru] -> Hakaru -> *).
ABT Term abt =>
Rational -> abt '[] 'HReal
real_ Rational
1 in
    abt '[] 'HReal
-> abt '[] 'HReal
-> (abt '[] 'HReal -> abt '[] 'HProb)
-> abt '[] 'HProb
forall (abt :: [Hakaru] -> Hakaru -> *).
ABT Term abt =>
abt '[] 'HReal
-> abt '[] 'HReal
-> (abt '[] 'HReal -> abt '[] 'HProb)
-> abt '[] 'HProb
integrate (Rational -> abt '[] 'HReal
forall (abt :: [Hakaru] -> Hakaru -> *).
ABT Term abt =>
Rational -> abt '[] 'HReal
real_ Rational
0) (abt '[] 'HProb -> abt '[] 'HReal
forall (abt :: [Hakaru] -> Hakaru -> *).
ABT Term abt =>
abt '[] 'HProb -> abt '[] 'HReal
fromProb abt '[] 'HProb
x) ((abt '[] 'HReal -> abt '[] 'HProb) -> abt '[] 'HProb)
-> (abt '[] 'HReal -> abt '[] 'HProb) -> abt '[] 'HProb
forall a b. (a -> b) -> a -> b
$ \abt '[] 'HReal
t ->
        abt '[] 'HReal -> abt '[] 'HProb
forall (abt :: [Hakaru] -> Hakaru -> *).
ABT Term abt =>
abt '[] 'HReal -> abt '[] 'HProb
unsafeProb abt '[] 'HReal
t abt '[] 'HProb -> abt '[] 'HReal -> abt '[] 'HProb
forall (a :: Hakaru) (abt :: [Hakaru] -> Hakaru -> *).
(RealProb a, ABT Term abt) =>
abt '[] 'HProb -> abt '[] a -> abt '[] 'HProb
** (abt '[] 'HProb -> abt '[] 'HReal
forall (abt :: [Hakaru] -> Hakaru -> *).
ABT Term abt =>
abt '[] 'HProb -> abt '[] 'HReal
fromProb abt '[] 'HProb
a abt '[] 'HReal -> abt '[] 'HReal -> abt '[] 'HReal
forall (abt :: [Hakaru] -> Hakaru -> *) (a :: Hakaru).
(ABT Term abt, HRing_ a) =>
abt '[] a -> abt '[] a -> abt '[] a
- abt '[] 'HReal
one')
        abt '[] 'HProb -> abt '[] 'HProb -> abt '[] 'HProb
forall (abt :: [Hakaru] -> Hakaru -> *) (a :: Hakaru).
(ABT Term abt, HSemiring_ a) =>
abt '[] a -> abt '[] a -> abt '[] a
* abt '[] 'HReal -> abt '[] 'HProb
forall (abt :: [Hakaru] -> Hakaru -> *).
ABT Term abt =>
abt '[] 'HReal -> abt '[] 'HProb
unsafeProb (abt '[] 'HReal
one' abt '[] 'HReal -> abt '[] 'HReal -> abt '[] 'HReal
forall (abt :: [Hakaru] -> Hakaru -> *) (a :: Hakaru).
(ABT Term abt, HRing_ a) =>
abt '[] a -> abt '[] a -> abt '[] a
- abt '[] 'HReal
t) abt '[] 'HProb -> abt '[] 'HReal -> abt '[] 'HProb
forall (a :: Hakaru) (abt :: [Hakaru] -> Hakaru -> *).
(RealProb a, ABT Term abt) =>
abt '[] 'HProb -> abt '[] a -> abt '[] 'HProb
** (abt '[] 'HProb -> abt '[] 'HReal
forall (abt :: [Hakaru] -> Hakaru -> *).
ABT Term abt =>
abt '[] 'HProb -> abt '[] 'HReal
fromProb abt '[] 'HProb
b abt '[] 'HReal -> abt '[] 'HReal -> abt '[] 'HReal
forall (abt :: [Hakaru] -> Hakaru -> *) (a :: Hakaru).
(ABT Term abt, HRing_ a) =>
abt '[] a -> abt '[] a -> abt '[] a
- abt '[] 'HReal
one')


regBeta -- TODO: rename 'regularBeta'
    :: (ABT Term abt)
    => abt '[] 'HProb
    -> abt '[] 'HProb
    -> abt '[] 'HProb
    -> abt '[] 'HProb
regBeta :: abt '[] 'HProb
-> abt '[] 'HProb -> abt '[] 'HProb -> abt '[] 'HProb
regBeta abt '[] 'HProb
x abt '[] 'HProb
a abt '[] 'HProb
b = abt '[] 'HProb
-> abt '[] 'HProb -> abt '[] 'HProb -> abt '[] 'HProb
forall (abt :: [Hakaru] -> Hakaru -> *).
ABT Term abt =>
abt '[] 'HProb
-> abt '[] 'HProb -> abt '[] 'HProb -> abt '[] 'HProb
incompleteBeta abt '[] 'HProb
x abt '[] 'HProb
a abt '[] 'HProb
b abt '[] 'HProb -> abt '[] 'HProb -> abt '[] 'HProb
forall (abt :: [Hakaru] -> Hakaru -> *) (a :: Hakaru).
(ABT Term abt, HFractional_ a) =>
abt '[] a -> abt '[] a -> abt '[] a
/ abt '[] 'HProb -> abt '[] 'HProb -> abt '[] 'HProb
forall (abt :: [Hakaru] -> Hakaru -> *).
ABT Term abt =>
abt '[] 'HProb -> abt '[] 'HProb -> abt '[] 'HProb
betaFunc abt '[] 'HProb
a abt '[] 'HProb
b


tCDF :: (ABT Term abt) => abt '[] 'HReal -> abt '[] 'HProb -> abt '[] 'HProb
tCDF :: abt '[] 'HReal -> abt '[] 'HProb -> abt '[] 'HProb
tCDF abt '[] 'HReal
x abt '[] 'HProb
v =
    let b :: abt '[] 'HProb
b = abt '[] 'HProb
-> abt '[] 'HProb -> abt '[] 'HProb -> abt '[] 'HProb
forall (abt :: [Hakaru] -> Hakaru -> *).
ABT Term abt =>
abt '[] 'HProb
-> abt '[] 'HProb -> abt '[] 'HProb -> abt '[] 'HProb
regBeta (abt '[] 'HProb
v abt '[] 'HProb -> abt '[] 'HProb -> abt '[] 'HProb
forall (abt :: [Hakaru] -> Hakaru -> *) (a :: Hakaru).
(ABT Term abt, HFractional_ a) =>
abt '[] a -> abt '[] a -> abt '[] a
/ (abt '[] 'HReal -> abt '[] 'HProb
forall (abt :: [Hakaru] -> Hakaru -> *).
ABT Term abt =>
abt '[] 'HReal -> abt '[] 'HProb
unsafeProb (abt '[] 'HReal
xabt '[] 'HReal -> abt '[] 'HReal -> abt '[] 'HReal
forall (abt :: [Hakaru] -> Hakaru -> *) (a :: Hakaru).
(ABT Term abt, HSemiring_ a) =>
abt '[] a -> abt '[] a -> abt '[] a
*abt '[] 'HReal
x) abt '[] 'HProb -> abt '[] 'HProb -> abt '[] 'HProb
forall (abt :: [Hakaru] -> Hakaru -> *) (a :: Hakaru).
(ABT Term abt, HSemiring_ a) =>
abt '[] a -> abt '[] a -> abt '[] a
+ abt '[] 'HProb
v)) (abt '[] 'HProb
v abt '[] 'HProb -> abt '[] 'HProb -> abt '[] 'HProb
forall (abt :: [Hakaru] -> Hakaru -> *) (a :: Hakaru).
(ABT Term abt, HFractional_ a) =>
abt '[] a -> abt '[] a -> abt '[] a
/ NonNegativeRational -> abt '[] 'HProb
forall (abt :: [Hakaru] -> Hakaru -> *).
ABT Term abt =>
NonNegativeRational -> abt '[] 'HProb
prob_ NonNegativeRational
2) (NonNegativeRational -> abt '[] 'HProb
forall (abt :: [Hakaru] -> Hakaru -> *).
ABT Term abt =>
NonNegativeRational -> abt '[] 'HProb
prob_ NonNegativeRational
0.5)
    in  abt '[] 'HReal -> abt '[] 'HProb
forall (abt :: [Hakaru] -> Hakaru -> *).
ABT Term abt =>
abt '[] 'HReal -> abt '[] 'HProb
unsafeProb (abt '[] 'HReal -> abt '[] 'HProb)
-> abt '[] 'HReal -> abt '[] 'HProb
forall a b. (a -> b) -> a -> b
$ Rational -> abt '[] 'HReal
forall (abt :: [Hakaru] -> Hakaru -> *).
ABT Term abt =>
Rational -> abt '[] 'HReal
real_ Rational
1 abt '[] 'HReal -> abt '[] 'HReal -> abt '[] 'HReal
forall (abt :: [Hakaru] -> Hakaru -> *) (a :: Hakaru).
(ABT Term abt, HRing_ a) =>
abt '[] a -> abt '[] a -> abt '[] a
- Rational -> abt '[] 'HReal
forall (abt :: [Hakaru] -> Hakaru -> *).
ABT Term abt =>
Rational -> abt '[] 'HReal
real_ Rational
0.5 abt '[] 'HReal -> abt '[] 'HReal -> abt '[] 'HReal
forall (abt :: [Hakaru] -> Hakaru -> *) (a :: Hakaru).
(ABT Term abt, HSemiring_ a) =>
abt '[] a -> abt '[] a -> abt '[] a
* abt '[] 'HProb -> abt '[] 'HReal
forall (abt :: [Hakaru] -> Hakaru -> *).
ABT Term abt =>
abt '[] 'HProb -> abt '[] 'HReal
fromProb abt '[] 'HProb
b


-- BUG: get rid of the SingI requirements due to using 'lam'
approxMh
    :: (ABT Term abt, SingI a)
    => (abt '[] a -> abt '[] ('HMeasure a))
    -> abt '[] ('HMeasure a)
    -> [abt '[] a -> abt '[] ('HMeasure a)]
    -> abt '[] (a ':-> 'HMeasure a)
approxMh :: (abt '[] a -> abt '[] ('HMeasure a))
-> abt '[] ('HMeasure a)
-> [abt '[] a -> abt '[] ('HMeasure a)]
-> abt '[] (a ':-> 'HMeasure a)
approxMh abt '[] a -> abt '[] ('HMeasure a)
_ abt '[] ('HMeasure a)
_ [] = [Char] -> abt '[] (a ':-> 'HMeasure a)
forall a. HasCallStack => [Char] -> a
error [Char]
"TODO: approxMh for empty list"
approxMh abt '[] a -> abt '[] ('HMeasure a)
proposal abt '[] ('HMeasure a)
prior (abt '[] a -> abt '[] ('HMeasure a)
_:[abt '[] a -> abt '[] ('HMeasure a)]
xs) =
    case [abt '[] (HPair a a ':-> 'HProb)]
-> Maybe (abt '[] (HPair a a ':-> 'HProb))
forall (abt :: [Hakaru] -> Hakaru -> *) (a :: Hakaru).
ABT Term abt =>
[abt '[] a] -> Maybe (abt '[] a)
determine ([abt '[] (HPair a a ':-> 'HProb)]
 -> Maybe (abt '[] (HPair a a ':-> 'HProb)))
-> (abt '[] ('HMeasure (HPair a a))
    -> [abt '[] (HPair a a ':-> 'HProb)])
-> abt '[] ('HMeasure (HPair a a))
-> Maybe (abt '[] (HPair a a ':-> 'HProb))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. abt '[] ('HMeasure (HPair a a))
-> [abt '[] (HPair a a ':-> 'HProb)]
forall (abt :: [Hakaru] -> Hakaru -> *) (a :: Hakaru).
ABT Term abt =>
abt '[] ('HMeasure a) -> [abt '[] (a ':-> 'HProb)]
density (abt '[] ('HMeasure (HPair a a))
 -> Maybe (abt '[] (HPair a a ':-> 'HProb)))
-> abt '[] ('HMeasure (HPair a a))
-> Maybe (abt '[] (HPair a a ':-> 'HProb))
forall a b. (a -> b) -> a -> b
$ abt '[] ('HMeasure a)
-> (abt '[] a -> abt '[] ('HMeasure a))
-> abt '[] ('HMeasure (HPair a a))
forall (abt :: [Hakaru] -> Hakaru -> *) (a :: Hakaru)
       (b :: Hakaru).
(ABT Term abt, SingI a, SingI b) =>
abt '[] ('HMeasure a)
-> (abt '[] a -> abt '[] ('HMeasure b))
-> abt '[] ('HMeasure (HPair a b))
bindx abt '[] ('HMeasure a)
prior abt '[] a -> abt '[] ('HMeasure a)
proposal of
    Maybe (abt '[] (HPair a a ':-> 'HProb))
Nothing -> [Char] -> abt '[] (a ':-> 'HMeasure a)
forall a. HasCallStack => [Char] -> a
error [Char]
"approxMh: couldn't get density"
    Just abt '[] (HPair a a ':-> 'HProb)
theDensity ->
        (abt '[] a -> abt '[] ('HMeasure a))
-> abt '[] (a ':-> 'HMeasure a)
forall (abt :: [Hakaru] -> Hakaru -> *) (a :: Hakaru)
       (b :: Hakaru).
(ABT Term abt, SingI a) =>
(abt '[] a -> abt '[] b) -> abt '[] (a ':-> b)
lam ((abt '[] a -> abt '[] ('HMeasure a))
 -> abt '[] (a ':-> 'HMeasure a))
-> (abt '[] a -> abt '[] ('HMeasure a))
-> abt '[] (a ':-> 'HMeasure a)
forall a b. (a -> b) -> a -> b
$ \abt '[] a
old ->
        abt '[] (HPair a a ':-> 'HProb)
-> (abt '[] (HPair a a ':-> 'HProb) -> abt '[] ('HMeasure a))
-> abt '[] ('HMeasure a)
forall (abt :: [Hakaru] -> Hakaru -> *) (a :: Hakaru)
       (b :: Hakaru).
ABT Term abt =>
abt '[] a -> (abt '[] a -> abt '[] b) -> abt '[] b
let_ abt '[] (HPair a a ':-> 'HProb)
theDensity ((abt '[] (HPair a a ':-> 'HProb) -> abt '[] ('HMeasure a))
 -> abt '[] ('HMeasure a))
-> (abt '[] (HPair a a ':-> 'HProb) -> abt '[] ('HMeasure a))
-> abt '[] ('HMeasure a)
forall a b. (a -> b) -> a -> b
$ \abt '[] (HPair a a ':-> 'HProb)
mu ->
        abt '[] 'HReal -> abt '[] 'HProb
forall (abt :: [Hakaru] -> Hakaru -> *).
ABT Term abt =>
abt '[] 'HReal -> abt '[] 'HProb
unsafeProb (abt '[] 'HReal -> abt '[] 'HProb)
-> abt '[] ('HMeasure 'HReal) -> abt '[] ('HMeasure 'HProb)
forall (abt :: [Hakaru] -> Hakaru -> *) (a :: Hakaru)
       (b :: Hakaru).
(ABT Term abt, SingI a) =>
(abt '[] a -> abt '[] b)
-> abt '[] ('HMeasure a) -> abt '[] ('HMeasure b)
<$> abt '[] 'HReal -> abt '[] 'HReal -> abt '[] ('HMeasure 'HReal)
forall (abt :: [Hakaru] -> Hakaru -> *).
ABT Term abt =>
abt '[] 'HReal -> abt '[] 'HReal -> abt '[] ('HMeasure 'HReal)
uniform (Rational -> abt '[] 'HReal
forall (abt :: [Hakaru] -> Hakaru -> *).
ABT Term abt =>
Rational -> abt '[] 'HReal
real_ Rational
0) (Rational -> abt '[] 'HReal
forall (abt :: [Hakaru] -> Hakaru -> *).
ABT Term abt =>
Rational -> abt '[] 'HReal
real_ Rational
1) abt '[] ('HMeasure 'HProb)
-> (abt '[] 'HProb -> abt '[] ('HMeasure a))
-> abt '[] ('HMeasure a)
forall (abt :: [Hakaru] -> Hakaru -> *) (a :: Hakaru)
       (b :: Hakaru).
ABT Term abt =>
abt '[] ('HMeasure a)
-> (abt '[] a -> abt '[] ('HMeasure b)) -> abt '[] ('HMeasure b)
>>= \abt '[] 'HProb
u ->
        abt '[] a -> abt '[] ('HMeasure a)
proposal abt '[] a
old abt '[] ('HMeasure a)
-> (abt '[] a -> abt '[] ('HMeasure a)) -> abt '[] ('HMeasure a)
forall (abt :: [Hakaru] -> Hakaru -> *) (a :: Hakaru)
       (b :: Hakaru).
ABT Term abt =>
abt '[] ('HMeasure a)
-> (abt '[] a -> abt '[] ('HMeasure b)) -> abt '[] ('HMeasure b)
>>= \abt '[] a
new ->
        abt '[] 'HProb
-> (abt '[] 'HProb -> abt '[] ('HMeasure a))
-> abt '[] ('HMeasure a)
forall (abt :: [Hakaru] -> Hakaru -> *) (a :: Hakaru)
       (b :: Hakaru).
ABT Term abt =>
abt '[] a -> (abt '[] a -> abt '[] b) -> abt '[] b
let_ (abt '[] 'HProb
u abt '[] 'HProb -> abt '[] 'HProb -> abt '[] 'HProb
forall (abt :: [Hakaru] -> Hakaru -> *) (a :: Hakaru).
(ABT Term abt, HSemiring_ a) =>
abt '[] a -> abt '[] a -> abt '[] a
* abt '[] (HPair a a ':-> 'HProb)
mu abt '[] (HPair a a ':-> 'HProb)
-> abt '[] (HPair a a) -> abt '[] 'HProb
forall (abt :: [Hakaru] -> Hakaru -> *) (a :: Hakaru)
       (b :: Hakaru).
ABT Term abt =>
abt '[] (a ':-> b) -> abt '[] a -> abt '[] b
`app` abt '[] a -> abt '[] a -> abt '[] (HPair a a)
forall (abt :: [Hakaru] -> Hakaru -> *) (a :: Hakaru)
       (b :: Hakaru).
(ABT Term abt, SingI a, SingI b) =>
abt '[] a -> abt '[] b -> abt '[] (HPair a b)
pair abt '[] a
new abt '[] a
old abt '[] 'HProb -> abt '[] 'HProb -> abt '[] 'HProb
forall (abt :: [Hakaru] -> Hakaru -> *) (a :: Hakaru).
(ABT Term abt, HFractional_ a) =>
abt '[] a -> abt '[] a -> abt '[] a
/ abt '[] (HPair a a ':-> 'HProb)
mu abt '[] (HPair a a ':-> 'HProb)
-> abt '[] (HPair a a) -> abt '[] 'HProb
forall (abt :: [Hakaru] -> Hakaru -> *) (a :: Hakaru)
       (b :: Hakaru).
ABT Term abt =>
abt '[] (a ':-> b) -> abt '[] a -> abt '[] b
`app` abt '[] a -> abt '[] a -> abt '[] (HPair a a)
forall (abt :: [Hakaru] -> Hakaru -> *) (a :: Hakaru)
       (b :: Hakaru).
(ABT Term abt, SingI a, SingI b) =>
abt '[] a -> abt '[] b -> abt '[] (HPair a b)
pair abt '[] a
old abt '[] a
new) ((abt '[] 'HProb -> abt '[] ('HMeasure a))
 -> abt '[] ('HMeasure a))
-> (abt '[] 'HProb -> abt '[] ('HMeasure a))
-> abt '[] ('HMeasure a)
forall a b. (a -> b) -> a -> b
$ \abt '[] 'HProb
u0 ->
        abt '[] 'HProb
-> (abt '[] 'HProb -> abt '[] ('HMeasure a))
-> abt '[] ('HMeasure a)
forall (abt :: [Hakaru] -> Hakaru -> *) (a :: Hakaru)
       (b :: Hakaru).
ABT Term abt =>
abt '[] a -> (abt '[] a -> abt '[] b) -> abt '[] b
let_ (abt '[] a -> abt '[] a -> abt '[] 'HProb
forall p p. p -> p -> abt '[] 'HProb
l abt '[] a
new abt '[] a
new abt '[] 'HProb -> abt '[] 'HProb -> abt '[] 'HProb
forall (abt :: [Hakaru] -> Hakaru -> *) (a :: Hakaru).
(ABT Term abt, HFractional_ a) =>
abt '[] a -> abt '[] a -> abt '[] a
/ abt '[] a -> abt '[] a -> abt '[] 'HProb
forall p p. p -> p -> abt '[] 'HProb
l abt '[] a
old abt '[] a
old) ((abt '[] 'HProb -> abt '[] ('HMeasure a))
 -> abt '[] ('HMeasure a))
-> (abt '[] 'HProb -> abt '[] ('HMeasure a))
-> abt '[] ('HMeasure a)
forall a b. (a -> b) -> a -> b
$ \abt '[] 'HProb
l0 ->
        abt '[] 'HProb
-> (abt '[] 'HProb -> abt '[] ('HMeasure a))
-> abt '[] ('HMeasure a)
forall (abt :: [Hakaru] -> Hakaru -> *) (a :: Hakaru)
       (b :: Hakaru).
ABT Term abt =>
abt '[] a -> (abt '[] a -> abt '[] b) -> abt '[] b
let_ (abt '[] 'HReal -> abt '[] 'HProb -> abt '[] 'HProb
forall (abt :: [Hakaru] -> Hakaru -> *).
ABT Term abt =>
abt '[] 'HReal -> abt '[] 'HProb -> abt '[] 'HProb
tCDF (abt '[] 'HReal
n abt '[] 'HReal -> abt '[] 'HReal -> abt '[] 'HReal
forall (abt :: [Hakaru] -> Hakaru -> *) (a :: Hakaru).
(ABT Term abt, HRing_ a) =>
abt '[] a -> abt '[] a -> abt '[] a
- Rational -> abt '[] 'HReal
forall (abt :: [Hakaru] -> Hakaru -> *).
ABT Term abt =>
Rational -> abt '[] 'HReal
real_ Rational
1) (abt '[] 'HProb -> abt '[] 'HProb -> abt '[] 'HProb
forall (abt :: [Hakaru] -> Hakaru -> *).
ABT Term abt =>
abt '[] 'HProb -> abt '[] 'HProb -> abt '[] 'HProb
udif abt '[] 'HProb
l0 abt '[] 'HProb
u0)) ((abt '[] 'HProb -> abt '[] ('HMeasure a))
 -> abt '[] ('HMeasure a))
-> (abt '[] 'HProb -> abt '[] ('HMeasure a))
-> abt '[] ('HMeasure a)
forall a b. (a -> b) -> a -> b
$ \abt '[] 'HProb
delta ->
        abt '[] HBool
-> abt '[] ('HMeasure a)
-> abt '[] ('HMeasure a)
-> abt '[] ('HMeasure a)
forall (abt :: [Hakaru] -> Hakaru -> *) (a :: Hakaru).
ABT Term abt =>
abt '[] HBool -> abt '[] a -> abt '[] a -> abt '[] a
if_ (abt '[] 'HProb
delta abt '[] 'HProb -> abt '[] 'HProb -> abt '[] HBool
forall (abt :: [Hakaru] -> Hakaru -> *) (a :: Hakaru).
(ABT Term abt, HOrd_ a) =>
abt '[] a -> abt '[] a -> abt '[] HBool
< abt '[] 'HProb
eps)
            (abt '[] HBool
-> abt '[] ('HMeasure a)
-> abt '[] ('HMeasure a)
-> abt '[] ('HMeasure a)
forall (abt :: [Hakaru] -> Hakaru -> *) (a :: Hakaru).
ABT Term abt =>
abt '[] HBool -> abt '[] a -> abt '[] a -> abt '[] a
if_ (abt '[] 'HProb
u0 abt '[] 'HProb -> abt '[] 'HProb -> abt '[] HBool
forall (abt :: [Hakaru] -> Hakaru -> *) (a :: Hakaru).
(ABT Term abt, HOrd_ a) =>
abt '[] a -> abt '[] a -> abt '[] HBool
< abt '[] 'HProb
l0)
                (abt '[] a -> abt '[] ('HMeasure a)
forall (abt :: [Hakaru] -> Hakaru -> *) (a :: Hakaru).
ABT Term abt =>
abt '[] a -> abt '[] ('HMeasure a)
dirac abt '[] a
new)
                (abt '[] a -> abt '[] ('HMeasure a)
forall (abt :: [Hakaru] -> Hakaru -> *) (a :: Hakaru).
ABT Term abt =>
abt '[] a -> abt '[] ('HMeasure a)
dirac abt '[] a
old))
            ((abt '[] a -> abt '[] ('HMeasure a))
-> abt '[] ('HMeasure a)
-> [abt '[] a -> abt '[] ('HMeasure a)]
-> abt '[] (a ':-> 'HMeasure a)
forall (abt :: [Hakaru] -> Hakaru -> *) (a :: Hakaru).
(ABT Term abt, SingI a) =>
(abt '[] a -> abt '[] ('HMeasure a))
-> abt '[] ('HMeasure a)
-> [abt '[] a -> abt '[] ('HMeasure a)]
-> abt '[] (a ':-> 'HMeasure a)
approxMh abt '[] a -> abt '[] ('HMeasure a)
proposal abt '[] ('HMeasure a)
prior [abt '[] a -> abt '[] ('HMeasure a)]
xs abt '[] (a ':-> 'HMeasure a) -> abt '[] a -> abt '[] ('HMeasure a)
forall (abt :: [Hakaru] -> Hakaru -> *) (a :: Hakaru)
       (b :: Hakaru).
ABT Term abt =>
abt '[] (a ':-> b) -> abt '[] a -> abt '[] b
`app` abt '[] a
old)
    where
    n :: abt '[] 'HReal
n   = Rational -> abt '[] 'HReal
forall (abt :: [Hakaru] -> Hakaru -> *).
ABT Term abt =>
Rational -> abt '[] 'HReal
real_ Rational
2000
    eps :: abt '[] 'HProb
eps = NonNegativeRational -> abt '[] 'HProb
forall (abt :: [Hakaru] -> Hakaru -> *).
ABT Term abt =>
NonNegativeRational -> abt '[] 'HProb
prob_ NonNegativeRational
0.05
    udif :: abt '[] 'HProb -> abt '[] 'HProb -> abt '[] 'HProb
udif abt '[] 'HProb
lo abt '[] 'HProb
hi = abt '[] 'HReal -> abt '[] 'HProb
forall (abt :: [Hakaru] -> Hakaru -> *).
ABT Term abt =>
abt '[] 'HReal -> abt '[] 'HProb
unsafeProb (abt '[] 'HReal -> abt '[] 'HProb)
-> abt '[] 'HReal -> abt '[] 'HProb
forall a b. (a -> b) -> a -> b
$ abt '[] 'HProb -> abt '[] 'HReal
forall (abt :: [Hakaru] -> Hakaru -> *).
ABT Term abt =>
abt '[] 'HProb -> abt '[] 'HReal
fromProb abt '[] 'HProb
lo abt '[] 'HReal -> abt '[] 'HReal -> abt '[] 'HReal
forall (abt :: [Hakaru] -> Hakaru -> *) (a :: Hakaru).
(ABT Term abt, HRing_ a) =>
abt '[] a -> abt '[] a -> abt '[] a
- abt '[] 'HProb -> abt '[] 'HReal
forall (abt :: [Hakaru] -> Hakaru -> *).
ABT Term abt =>
abt '[] 'HProb -> abt '[] 'HReal
fromProb abt '[] 'HProb
hi
    l :: p -> p -> abt '[] 'HProb
l = \p
_d1 p
_d2 -> NonNegativeRational -> abt '[] 'HProb
forall (abt :: [Hakaru] -> Hakaru -> *).
ABT Term abt =>
NonNegativeRational -> abt '[] 'HProb
prob_ NonNegativeRational
2 -- determine (density (\theta -> x theta))

kl :: (ABT Term abt)
   => abt '[] ('HMeasure a)
   -> abt '[] ('HMeasure a)
   -> Maybe (abt '[] 'HProb)
kl :: abt '[] ('HMeasure a)
-> abt '[] ('HMeasure a) -> Maybe (abt '[] 'HProb)
kl abt '[] ('HMeasure a)
p abt '[] ('HMeasure a)
q = do
  abt '[] (a ':-> 'HProb)
dp <- [abt '[] (a ':-> 'HProb)] -> Maybe (abt '[] (a ':-> 'HProb))
forall (abt :: [Hakaru] -> Hakaru -> *) (a :: Hakaru).
ABT Term abt =>
[abt '[] a] -> Maybe (abt '[] a)
determine ([abt '[] (a ':-> 'HProb)] -> Maybe (abt '[] (a ':-> 'HProb)))
-> [abt '[] (a ':-> 'HProb)] -> Maybe (abt '[] (a ':-> 'HProb))
forall a b. (a -> b) -> a -> b
$ abt '[] ('HMeasure a) -> [abt '[] (a ':-> 'HProb)]
forall (abt :: [Hakaru] -> Hakaru -> *) (a :: Hakaru).
ABT Term abt =>
abt '[] ('HMeasure a) -> [abt '[] (a ':-> 'HProb)]
density abt '[] ('HMeasure a)
p
  abt '[] (a ':-> 'HProb)
dq <- [abt '[] (a ':-> 'HProb)] -> Maybe (abt '[] (a ':-> 'HProb))
forall (abt :: [Hakaru] -> Hakaru -> *) (a :: Hakaru).
ABT Term abt =>
[abt '[] a] -> Maybe (abt '[] a)
determine ([abt '[] (a ':-> 'HProb)] -> Maybe (abt '[] (a ':-> 'HProb)))
-> [abt '[] (a ':-> 'HProb)] -> Maybe (abt '[] (a ':-> 'HProb))
forall a b. (a -> b) -> a -> b
$ abt '[] ('HMeasure a) -> [abt '[] (a ':-> 'HProb)]
forall (abt :: [Hakaru] -> Hakaru -> *) (a :: Hakaru).
ABT Term abt =>
abt '[] ('HMeasure a) -> [abt '[] (a ':-> 'HProb)]
density abt '[] ('HMeasure a)
q
  abt '[] 'HProb -> Maybe (abt '[] 'HProb)
forall (m :: * -> *) a. Monad m => a -> m a
return
    (abt '[] 'HProb -> Maybe (abt '[] 'HProb))
-> ((abt '[] a -> abt '[] 'HProb) -> abt '[] 'HProb)
-> (abt '[] a -> abt '[] 'HProb)
-> Maybe (abt '[] 'HProb)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. abt '[] ('HMeasure a) -> abt '[a] 'HProb -> abt '[] 'HProb
forall (abt :: [Hakaru] -> Hakaru -> *) (a :: Hakaru).
ABT Term abt =>
abt '[] ('HMeasure a) -> abt '[a] 'HProb -> abt '[] 'HProb
expect abt '[] ('HMeasure a)
p
    (abt '[a] 'HProb -> abt '[] 'HProb)
-> ((abt '[] a -> abt '[] 'HProb) -> abt '[a] 'HProb)
-> (abt '[] a -> abt '[] 'HProb)
-> abt '[] 'HProb
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Text -> Sing a -> (abt '[] a -> abt '[] 'HProb) -> abt '[a] 'HProb
forall a1 (syn :: ([a1] -> a1 -> *) -> a1 -> *)
       (abt :: [a1] -> a1 -> *) (a2 :: a1) (xs :: [a1]) (b :: a1).
ABT syn abt =>
Text -> Sing a2 -> (abt '[] a2 -> abt xs b) -> abt (a2 : xs) b
binder Text
Text.empty (Sing ('HMeasure a) -> Sing a
forall (a :: Hakaru). Sing ('HMeasure a) -> Sing a
sUnMeasure (Sing ('HMeasure a) -> Sing a) -> Sing ('HMeasure a) -> Sing a
forall a b. (a -> b) -> a -> b
$ abt '[] ('HMeasure a) -> Sing ('HMeasure a)
forall (abt :: [Hakaru] -> Hakaru -> *) (a :: Hakaru).
ABT Term abt =>
abt '[] a -> Sing a
typeOf abt '[] ('HMeasure a)
p)
    ((abt '[] a -> abt '[] 'HProb) -> Maybe (abt '[] 'HProb))
-> (abt '[] a -> abt '[] 'HProb) -> Maybe (abt '[] 'HProb)
forall a b. (a -> b) -> a -> b
$ \abt '[] a
i -> abt '[] 'HReal -> abt '[] 'HProb
forall (abt :: [Hakaru] -> Hakaru -> *).
ABT Term abt =>
abt '[] 'HReal -> abt '[] 'HProb
unsafeProb (abt '[] 'HReal -> abt '[] 'HProb)
-> abt '[] 'HReal -> abt '[] 'HProb
forall a b. (a -> b) -> a -> b
$ abt '[] 'HProb -> abt '[] 'HReal
forall (abt :: [Hakaru] -> Hakaru -> *).
ABT Term abt =>
abt '[] 'HProb -> abt '[] 'HReal
log (abt '[] (a ':-> 'HProb) -> abt '[] a -> abt '[] 'HProb
forall (abt :: [Hakaru] -> Hakaru -> *) (a :: Hakaru)
       (b :: Hakaru).
ABT Term abt =>
abt '[] (a ':-> b) -> abt '[] a -> abt '[] b
app abt '[] (a ':-> 'HProb)
dp abt '[] a
i abt '[] 'HProb -> abt '[] 'HProb -> abt '[] 'HProb
forall (abt :: [Hakaru] -> Hakaru -> *) (a :: Hakaru).
(ABT Term abt, HFractional_ a) =>
abt '[] a -> abt '[] a -> abt '[] a
/ abt '[] (a ':-> 'HProb) -> abt '[] a -> abt '[] 'HProb
forall (abt :: [Hakaru] -> Hakaru -> *) (a :: Hakaru)
       (b :: Hakaru).
ABT Term abt =>
abt '[] (a ':-> b) -> abt '[] a -> abt '[] b
app abt '[] (a ':-> 'HProb)
dq abt '[] a
i)