View ProbMonad.hs
{-# LANGUAGE GADTs #-}
{-
The following code is based on experimental code by Aslan Askerov
based on Ramsey and Pfeffers "Stochastic Lambda Calculus and Monads of
Probability Distributions". Implementation of random n is from
Audebaud and Paulin-Mohring paper, so is the random walk example.
This gist is used here http://madsbuch.com/blog/the-probability-monad/
The class hierarchy is as follows:
View Proof.hs
{-# LANGUAGE GADTs #-} -- soft dependent types
{-# LANGUAGE PolyKinds #-} -- Allow general specification of Refl
{-# LANGUAGE RankNTypes #-} -- The forall stuff
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE TypeFamilies #-}
module Proof where
-- Our type level numerals
data Nat = Z | S Nat