Safe Haskell | None |
---|---|
Language | Haskell2010 |
Synopsis
- newtype Natural (start :: Nat) (end :: Nat) = Nat Int
- nat :: forall n m. (KnownNat n, KnownNat m) => Int -> Natural n m
- coerceNat :: (Int -> Int -> Int) -> Natural a a' -> Natural b b' -> Natural c c'
- coerceNat2 :: ((Int, Int) -> Int -> Int) -> (Natural a a', Natural b b') -> Natural c c' -> Natural d d'
- coerceNat3 :: (Int -> Int -> a) -> Natural b b' -> Natural c c' -> a
- newtype List a = L [a]
Documentation
This is an internal module and it is not meant to be imported.
Utility module that provides the Natural
data type.
The semantic associated with this data type is that
it's meant to be a restricted Int
value. For example
the type Natural 6
can only be instanciated with Nat n
where 0 <= n <= 6
. Why, You might ask, because with normal
Int
s it is not possible to have a decent Enum (Int, Int)
instance. See the following probabilistic programming model as and
example:
We want to calculate the probability of the sum of two dice throws. To do this we start by defining the sample space:
type SampleSpace = Int -- We thinkInt
are enough die :: Dist Int 6 die = unifrom [1..6] -- PromoteInt
addition to a matrix addM = fromF (uncurry (+)) -- Impossible
The last line is impossible because (Int, Int)
does not have
a good Enum
instance: [(0, 1), (0, 2), .. (0, maxBound), (1, 0),
..]
. And we'd like the addition matrix to be of 36 columns by 12
rows but limited to integers up to 6
!
One way to solve this issue is by defining and auxilary data type to represent the sample space:
data SampleSpace = S1 | S2 | S3 | S4 | S5 | S6 deriving (Show, Eq, Enum, Bounded) -- Enum and Bounded are important
And write the sample space addition function:
ssAdd :: SampleSpace -> SampleSpace -> Int ssAdd a b = (fromEnum a + 1) + (fromEnum b + 1)
And then promote that function to matrix and everything is alright:
ssAddM = fromF' (uncurry ssAdd)
dieSumProb = ssAddM comp
(khatri die die)
This is a nice solution for small sample spaces. But for larger ones
it is not feasible to write a data type with hundreds of constructors
and then write manipulation functions that need to deal with them.
To mitigate this limitation the Natural
type comes a long way and
allows one to model the sample in an easier way. See for instance:
ssAdd :: Natural 6 -> Natural 6 -> Natural 12
ssAdd = coerceNat (+)
ssAddM = fromF' (uncurry sumSS)
die :: Dist (Natural 6) 6
die = uniform [nat @6 1 .. nat 6]
dieSumProb = ssAddM comp
(khatri die die)
Natural
data type
newtype Natural (start :: Nat) (end :: Nat) Source #
Wrapper around Int
s that have a restrictive semantic associated.
A value of type
can only be instanciated with some Natural
n mInt
i
that's n <= i <= m
.
Instances
(KnownNat n, KnownNat m) => Bounded (Natural n m) Source # | |
(KnownNat n, KnownNat m) => Enum (Natural n m) Source # | |
Defined in LAoP.Utils.Internal succ :: Natural n m -> Natural n m # pred :: Natural n m -> Natural n m # toEnum :: Int -> Natural n m # fromEnum :: Natural n m -> Int # enumFrom :: Natural n m -> [Natural n m] # enumFromThen :: Natural n m -> Natural n m -> [Natural n m] # enumFromTo :: Natural n m -> Natural n m -> [Natural n m] # enumFromThenTo :: Natural n m -> Natural n m -> Natural n m -> [Natural n m] # | |
Eq (Natural start end) Source # | |
(KnownNat n, KnownNat m) => Num (Natural n m) Source # | Throws a runtime error if any of the operations overflows or underflows. |
Defined in LAoP.Utils.Internal (+) :: Natural n m -> Natural n m -> Natural n m # (-) :: Natural n m -> Natural n m -> Natural n m # (*) :: Natural n m -> Natural n m -> Natural n m # negate :: Natural n m -> Natural n m # abs :: Natural n m -> Natural n m # signum :: Natural n m -> Natural n m # fromInteger :: Integer -> Natural n m # | |
Ord (Natural start end) Source # | |
Defined in LAoP.Utils.Internal compare :: Natural start end -> Natural start end -> Ordering # (<) :: Natural start end -> Natural start end -> Bool # (<=) :: Natural start end -> Natural start end -> Bool # (>) :: Natural start end -> Natural start end -> Bool # (>=) :: Natural start end -> Natural start end -> Bool # max :: Natural start end -> Natural start end -> Natural start end # min :: Natural start end -> Natural start end -> Natural start end # | |
Read (Natural start end) Source # | |
Show (Natural start end) Source # | |
NFData (Natural start end) Source # | |
Defined in LAoP.Utils.Internal |
Coerce auxiliar functions to help promote Int
typed functions to
coerceNat2 :: ((Int, Int) -> Int -> Int) -> (Natural a a', Natural b b') -> Natural c c' -> Natural d d' Source #
Powerset data type
Powerset data type.
This data type is a newtype wrapper around '[]'. This exists in order to
implement an Enum
and Bounded
instance that cannot be harmful for the outside.
L [a] |
Orphan instances
(Bounded a, Bounded b) => Bounded (Either a b) Source # | |
(Enum a, Bounded a, Enum b, Bounded b) => Enum (Either a b) Source # | |
succ :: Either a b -> Either a b # pred :: Either a b -> Either a b # fromEnum :: Either a b -> Int # enumFrom :: Either a b -> [Either a b] # enumFromThen :: Either a b -> Either a b -> [Either a b] # enumFromTo :: Either a b -> Either a b -> [Either a b] # enumFromThenTo :: Either a b -> Either a b -> Either a b -> [Either a b] # | |
(Enum a, Enum b, Bounded b) => Enum (a, b) Source # | Optimized |