From ad8338e8c2d21b3465559dac1725b886a17e401e Mon Sep 17 00:00:00 2001 From: Alex Gryzlov Date: Fri, 26 May 2017 15:18:38 +0300 Subject: [PATCH] update for idris 1.0 --- README.md | 2 +- src/Probability/Core.idr | 19 +++++++------ src/Probability/Display.idr | 38 ++++++++++++++------------ src/Probability/Examples/MontyHall.idr | 12 ++++---- src/Probability/Monad.idr | 1 + src/Probability/Utils.idr | 3 +- 6 files changed, 40 insertions(+), 35 deletions(-) diff --git a/README.md b/README.md index d5c1f6d..97284db 100644 --- a/README.md +++ b/README.md @@ -8,7 +8,7 @@ It is heavily inspired by the [Probabilistic Functional Programming](https://web Much of the expressivity and power of this approach comes from the natural functorial, applicative and monadic structures on probability distributions. The implementation of these structures via the corresponding type classes is the core of the library, and is borrowed almost exactly from PFP. -Needs Idris 0.9.19 or the current Github version. +Needs Idris 1.0 or the current Github version. ### Examples #### Six-Sided Die diff --git a/src/Probability/Core.idr b/src/Probability/Core.idr index 76d5ef5..3661ae2 100644 --- a/src/Probability/Core.idr +++ b/src/Probability/Core.idr @@ -5,23 +5,24 @@ import Probability.Utils %default total +%access export + ||| Representation of a probability distribution -abstract data Probability p a = Pr (List (a,p)) -%access public - - ---- Types ---- +public export Prob : Type -> Type -Prob = Probability Float +Prob = Probability Double +public export Transition : Type -> Type -> Type Transition a b = a -> Prob b +public export Trans : Type -> Type Trans t = Transition t t @@ -46,20 +47,20 @@ flat : List a -> Prob a flat l = let s = (1 / (cast $ length l)) in Pr $ (\x => (x,s)) <$> l -shape : List a -> List Float -> Prob a +shape : List a -> List Double -> Prob a shape xs ps = Pr $ zipWith MkPair xs (normalize ps) ---- Instances ---- -instance Functor (Probability p) where +Functor (Probability p) where map f (Pr l) = Pr $ left f <$> l -instance Num p => Applicative (Probability p) where +Num p => Applicative (Probability p) where pure = certainly fm <*> m = Pr [ (f x, q*w) | (f,w) <- runProb fm, (x,q) <- runProb m ] -instance Num p => Monad (Probability p) where +Num p => Monad (Probability p) where d >>= f = Pr [ (y, q*w) | (x,w) <- runProb d, (y,q) <- runProb (f x) ] diff --git a/src/Probability/Display.idr b/src/Probability/Display.idr index f8e2ffe..2d279f5 100644 --- a/src/Probability/Display.idr +++ b/src/Probability/Display.idr @@ -6,23 +6,25 @@ import Probability.Utils %default total +%access export + ||| Sets the width of terminal graph displays -width : Float +width : Double width = 30 ---- Floating Point Utils ---- -castFN : Float -> Nat +castFN : Double -> Nat castFN = cast . cast {to=Integer} -intPart : Float -> Float +intPart : Double -> Double intPart = cast . cast {to=Integer} -fracPart : Float -> Float +fracPart : Double -> Double fracPart x = x - intPart x -||| Raise a float to an arbitrary integral power -fpow : Float -> Integer -> Float +||| Raise a double to an arbitrary integral power +fpow : Double -> Integer -> Double fpow f p = if p >= 0 then pow f (cast p) else 1 / (pow f $ cast $ abs p) @@ -38,25 +40,25 @@ tipChars = ["▉", "▎", "▏"] -tipVals : List Float +tipVals : List Double tipVals = (+ 0.0625) . (/8) . cast <$> reverse [1..7] -- = [15/16, 13/16, 11/16, 9/16, 7/16, 5/16, 3/16] -tips : List (Float,String) +tips : List (Double,String) tips = zipWith MkPair tipVals tipChars -selectTip : Float -> String +selectTip : Double -> String selectTip x = let l = filter (\p => fst p < x) tips in case l of [] => "" ((f,s)::ss) => s -bar : Float -> String +bar : Double -> String bar f = pack (replicate (castFN f) '█') ++ selectTip (fracPart f) -bars : List Float -> List String +bars : List Double -> List String bars l = let mx = foldr max 0 l in map bar $ map (* width/mx) l @@ -82,26 +84,26 @@ digit 7 = '7' digit 8 = '8' digit 9 = '9' -digAt : Float -> Integer -> Integer +digAt : Double -> Integer -> Integer digAt x i = flip mod 10 $ cast $ abs $ x / (fpow 10 i) -charAt : Float -> Integer -> Char +charAt : Double -> Integer -> Char charAt x i = digit $ digAt x i -scanUp : Float -> Integer -> Integer +scanUp : Double -> Integer -> Integer scanUp x n = if x < (fpow 10 $ n + 1) then n else scanUp x (n + 1) -scanDown : Float -> Integer -> Integer +scanDown : Double -> Integer -> Integer scanDown x n = if x > (fpow 10 $ -n) then -n else scanDown x (n + 1) -||| Find the leading digit of a Float -maxdig : Float -> Integer +||| Find the leading digit of a Double +maxdig : Double -> Integer maxdig x = if x > 1 then scanUp x 0 else scanDown x 1 ||| Show 4 digits (not necessarily significant) of a percentage -showPercent : Float -> String +showPercent : Double -> String showPercent x = let y = 100 * x s1 = pack $ (charAt y) <$> [1,0] s2 = pack $ (charAt y) <$> [-1,-2] diff --git a/src/Probability/Examples/MontyHall.idr b/src/Probability/Examples/MontyHall.idr index ad18120..a9042ed 100644 --- a/src/Probability/Examples/MontyHall.idr +++ b/src/Probability/Examples/MontyHall.idr @@ -11,13 +11,13 @@ import Data.Vect data Door = One | Two | Three -instance Eq Door where +Eq Door where One == One = True Two == Two = True Three == Three = True _ == _ = False -instance Show Door where +Show Door where show One = "Door #1" show Two = "Door #2" show Three = "Door #3" @@ -47,10 +47,10 @@ score {k} v = case k of data GameScore = Score (Vect (S (S n)) Door) -instance Eq GameScore where +Eq GameScore where (Score v) == (Score w) = vecEq v w -instance Show GameScore where +Show GameScore where show (Score v) = let status = if score v then " WIN " else " LOSE " in status ++ show v @@ -58,10 +58,10 @@ instance Show GameScore where data GameOutcome = Outcome (Monty (S (S n))) -instance Eq GameOutcome where +Eq GameOutcome where (Outcome v) == (Outcome w) = score v == score w -instance Show GameOutcome where +Show GameOutcome where show (Outcome v) = if score v then " WIN " else " LOSE " diff --git a/src/Probability/Monad.idr b/src/Probability/Monad.idr index 3504244..6c6a484 100644 --- a/src/Probability/Monad.idr +++ b/src/Probability/Monad.idr @@ -3,6 +3,7 @@ module Probability.Monad %default total +%access export infixr 6 >=> (>=>) : Monad m => (a -> m b) -> (b -> m c) -> a -> m c diff --git a/src/Probability/Utils.idr b/src/Probability/Utils.idr index ff40ce8..07adedc 100644 --- a/src/Probability/Utils.idr +++ b/src/Probability/Utils.idr @@ -5,6 +5,7 @@ import Data.Vect %default total +%access export infixl 5 ::~ @@ -19,7 +20,7 @@ vecEq [] [] = True vecEq _ _ = False -normalize : List Float -> List Float +normalize : List Double -> List Double normalize l = (/ (sum l)) <$> l left : (a -> c) -> (a,b) -> (c,b)