Browse Source

Work on formalising probabilities.

idris
Thomas Kerber 1 year ago
parent
commit
7d08352f39
Signed by: Thomas Kerber <t.kerber@ed.ac.uk> GPG Key ID: 8489B911F9ED617B
4 changed files with 78 additions and 59 deletions
  1. +66
    -43
      Yggdrasil/Distribution.idr
  2. +1
    -0
      Yggdrasil/Extensible.idr
  3. +0
    -16
      Yggdrasil/Zn.idr
  4. +11
    -0
      yggdrasil.ipkg

+ 66
- 43
Yggdrasil/Distribution.idr View File

@@ -1,51 +1,71 @@
module Yggdrasil.Distribution

import Control.Monad.Identity
import Yggdrasil.Zn
import Data.Fin
import Data.QQ.SternBrocot
import Data.ZZ
import Yggdrasil.Extensible

public export
interface Sampler s where
sampleZn : {n : Nat} -> s -> (Zn (S n), s)

export
data DistributionT : (Type -> Type) -> Type -> Type where
MkDistributionT : {a : Type} ->
({s : Type} -> Sampler s => s -> m (Pair a s)) ->
DistributionT m a

export
Distribution : Type -> Type
Distribution = DistributionT Identity

Functor f => Functor (DistributionT f) where
map g (MkDistributionT d) = MkDistributionT
(\s => map (\(a, s) => (g a, s)) (d s))

Monad m => Applicative (DistributionT m) where
pure x = MkDistributionT (\s => pure (x, s))
(MkDistributionT fa) <*> (MkDistributionT xa) = MkDistributionT (\s => do
(f, s') <- fa s
(x, s'') <- xa s'
pure (f x, s''))

Monad m => Monad (DistributionT m) where
(MkDistributionT a) >>= b = MkDistributionT (\s =>
a s >>= (\(a', s') => let (MkDistributionT b') = (b a') in b' s'))

export
coin : Distribution Bool
coin = map toBool $ MkDistributionT (Id . sampleZn)

distZn : {n : Nat} -> Distribution (Zn (S n))
distZn = MkDistributionT (Id . sampleZn)

export
liftDistribution : Monad m => Distribution b -> DistributionT m b
liftDistribution (MkDistributionT d) = MkDistributionT $ pure . runIdentity . d

export
uniform : (l : List a) -> {auto ok : NonEmpty l} -> Distribution a
uniform (x::xs) = map (indexZn (x::xs)) (distZn {n=length xs})
sample : {n : Nat} -> s -> (Fin (S n), s)

data D : Type -> Type where
||| A value is a distribution.
PureD : a -> D a
||| Sample from Fin, where n >= 2
SampleD : {n : Nat} -> D (Fin (S (S n)))
||| Allow sampling depending on the value of a previous sample.
BindD : D a -> (a -> D b) -> D b

Functor D where
map f x = BindD x (PureD . f)

Applicative D where
pure = PureD
f <*> x = BindD f (\f' => BindD x (\x' => PureD (f' x')))

Monad D where
(>>=) = BindD

allFin : (n : Nat) -> List (Fin n)
allFin Z = []
allFin (S n) = FZ :: map FS (allFin n)

Num QQ where
a + b = ?add_qq
a * b = ?mult_qq
fromInteger i = ?fromInt_qq

Neg QQ where
negate q = ?negate_qq
a - b = ?subtract_qq

data Event : (a -> Bool) -> D a -> QQ -> Type where
||| If `f x` is true, it's pure distribution has probability 1.
PureT : f a = True -> Event f (PureD a) (1 # 1)
||| If `f x` is false, it's pure distribution has probability 0.
PureF : f a = False -> Event f (PureD a) (0 # 1)
||| If we know the number of samples where `f x` is true,
NFin : length (filter f (allFin (S (S n)))) = m ->
Event f (SampleD {n=n}) (Pos m # S (S n))
CondBind : (f x = True -> Event g (bnd x) p1) ->
(f x = False -> Event g (bnd x) p2) ->
Event f d p3 ->
Event g (BindD d bnd) (p3 * p1 + (1 - p3) * p2)

data DualEvent : {d1 : D a} -> {d2 : D a} ->
(f : (a -> Bool)) ->
(p : QQ) ->
Event f d1 p ->
Event f d2 p ->
Type where
MkDual : (f : a -> Bool) ->
(p : QQ) ->
(e1 : Event f d1 p) ->
(e2 : Event f d2 p) ->
DualEvent f p e1 e2

infixr 5 $=

data ($=) : D a -> D a -> Type where
EEq : Eq a => ((x : a) -> DualEvent {d1=d1} {d2=d2} f p e1 e2) -> d1 $= d2

+ 1
- 0
Yggdrasil/Extensible.idr View File

@@ -2,6 +2,7 @@ import Prelude.Cast

infixr 5 ^=

export
data (^=) : a -> b -> Type where
Refl : x ^= x
Extend : {a : Type} -> {b : Type} -> (f : a -> b) -> (g : a -> b) -> ((x : a) -> f x ^= g x) -> f ^= g

+ 0
- 16
Yggdrasil/Zn.idr View File

@@ -1,16 +0,0 @@
module Yggdrasil.Zn

public export
data Zn : Nat -> Type where
ZnZ : Zn (S n)
ZnS : Zn n -> Zn (S n)

export
toBool : Zn 2 -> Bool
toBool ZnZ = False
toBool (ZnS ZnZ) = True

export
indexZn : (l : List a) -> Zn (length l) -> a
indexZn (x :: _) ZnZ = x
indexZn (_ :: xs) (ZnS n') = indexZn xs n'

+ 11
- 0
yggdrasil.ipkg View File

@@ -0,0 +1,11 @@
package yggdrasil

version = "0.0"
readme = README.md
license = "AGPLv3"
author = "Thomas Kerber <tk@drwx.org>"
sourceloc = https://git.drwx.org/phd/yggdrasil.git
modules = Yggdrasil.ExecutionModel
, Yggdrasil.Distribution
, Yggdrasil.Extensible
pkgs = base, effects, contrib, rationals

Loading…
Cancel
Save