Hansei - Embedded Domain-Specific Languages for Probabilistic Programming (Oleg)

2.1 Tagless Final Probabilistic Language

We define the syntax of the language as the following:

type prob = float

module type ProbSig = sig
  type ’a pm
  type (’a,’b) arr
  val b : bool -> bool pm
  val dist : (prob * ’a) list -> ’a pm
  val neg : bool pm -> bool pm
  val con : bool pm -> bool pm -> bool pm
  val dis : bool pm -> bool pm -> bool pm
  val if_ ; bool pm -> (unit -> ’a pm) -> (unit -> ’a pm) -> ’a pm
  val lam : (’a pm -> ’b pm) -> (’a,’b) arr pm
  val app : (’a,’b) arr pm -> (’a pm -> ’b pm)
end

type Prob = Float

class ProbSig a b | a -> b, b -> a where
  data family ProbMonad a
  data family Arr a b
  b    :: Bool -> ProbMonad Bool
  dist :: [(Prob, a)] -> ProbMonad a
  neg  :: ProbMonad Bool -> ProbMonad Bool
  and  :: ProbMonad Bool -> ProbMonad Bool -> ProbMonad Bool
  or   :: ProbMonad Bool -> ProbMonad Bool -> ProbMonad Bool
  if_  :: ProbMonad Bool -> (() -> ProbMonad a) -> (() -> ProbMonad a) -> ProbMonad a
  lam  :: (ProbMonad a -> ProbMonad b) -> ProbMonad (Arr a b)
  app  :: ProbMonad (Arr a b) -> (ProbMonad a -> ProbMonad b)

For simplicity, the signature ProbSig includes only the base type of booleans, and the operations necessary for a simple probabilistic model example.

Following the tagless-final approach, a boolean expression in the DSL denotes a distribution over booleans, and is represented as an expression of the type ProbMonad Bool. Here ProbMonad is an abstract type constructor. Different implementations of ProbSig define ProbMonad in their own ways, giving rise to different interpreters of the same DSL.

For example:

The “true” literal in the DSL is represented as b true which has the abstract type ProbMonad Bool.
A function expression in the DSL, for example of type Bool -> Bool is represented as an expression of type ProbMonad (Arr Bool Bool). Here, Arr is a binary type constructor.
We use higher-order abstract syntax to represent binding. For example, we represent the curried binary function λx. λy. x ∧ ¬y on booleans as lam (\x -> lam (\y -> and x (neg y))), whose inferred type is ProbMonad (Arr (Arr Bool Bool) Bool)). To apply this function to the literal “false”, we write app (lam (\x -> ...)) (b false).

This DSL is probabilistic only due to the presence of the dist construct, which takes a list of values and their probabilities. The dist expression then denotes a stochastic computation with the given discrete distribution.

A probabilistic program is a functor that takes a ProbSig instance as its argument.

lawn :: ProbSig s => 
lawn = let flip p         = dist [(p, true), (1 - p, false)]
           let_ e f       = app (lam f) e
           grass_model () = let_ (flip 0.3) (\rain -> 
                              let_ (flip 0.5) (\sprinkler ->
                                let_ (or (and (flip 0.9) rain)
                                          (or (and (flip 0.8) sprinkler)
                                               (flip 0.1))) (\grass_is_wet ->
                                      if_ grass_is_wet (\() -> rain) (\() -> dist [])
                                                            )
                                               )
                                             )

Last updated on 13 Nov 2020
Published on 13 Nov 2020