laop-0.1.0.3

Copyright(c) Armando Santos 2019-2020
Maintainerarmandoifsantos@gmail.com
Stabilityexperimental
Safe HaskellNone
LanguageHaskell2010

LAoP.Utils

Contents

Description

LAoP is a library for algebraic (inductive) construction and manipulation of matrices in Haskell. See my Msc Thesis for the motivation behind the library, the underlying theory, and implementation details.

This module provides the Natural data type. The semantic associated with this data type is that it's meant to be a restricted Int value.

Synopsis

Documentation

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 1 6 can only be instanciated with nat n where 1 <= n <= 6. Why, You might ask, because with normal Ints 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 think Int are enough

die :: Dist Int 6
die = unifrom [1..6] 

-- Promote Int 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 1 6 -> Natural 1 6 -> Natural 1 12
ssAdd = coerceNat (+) 

ssAddM = fromF' (uncurry sumSS)

die :: Dist (Natural 1 6) 6
die = uniform [nat 1 6 1 .. nat 6]

dieSumProb = ssAddM comp (khatri die die)

data Natural (start :: Nat) (end :: Nat) Source #

Wrapper around Ints that have a restrictive semantic associated. A value of type Natural n m can only be instanciated with some Int i that's n <= i <= m.

Instances
(KnownNat n, KnownNat m) => Bounded (Natural n m) Source # 
Instance details

Defined in LAoP.Utils.Internal

Methods

minBound :: Natural n m #

maxBound :: Natural n m #

(KnownNat n, KnownNat m) => Enum (Natural n m) Source # 
Instance details

Defined in LAoP.Utils.Internal

Methods

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 # 
Instance details

Defined in LAoP.Utils.Internal

Methods

(==) :: Natural start end -> Natural start end -> Bool #

(/=) :: Natural start end -> Natural start end -> Bool #

(KnownNat n, KnownNat m) => Num (Natural n m) Source #

Throws a runtime error if any of the operations overflows or underflows.

Instance details

Defined in LAoP.Utils.Internal

Methods

(+) :: 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 # 
Instance details

Defined in LAoP.Utils.Internal

Methods

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 # 
Instance details

Defined in LAoP.Utils.Internal

Methods

readsPrec :: Int -> ReadS (Natural start end) #

readList :: ReadS [Natural start end] #

readPrec :: ReadPrec (Natural start end) #

readListPrec :: ReadPrec [Natural start end] #

Show (Natural start end) Source # 
Instance details

Defined in LAoP.Utils.Internal

Methods

showsPrec :: Int -> Natural start end -> ShowS #

show :: Natural start end -> String #

showList :: [Natural start end] -> ShowS #

NFData (Natural start end) Source # 
Instance details

Defined in LAoP.Utils.Internal

Methods

rnf :: Natural start end -> () #

nat :: forall n m. (KnownNat n, KnownNat m) => Int -> Natural n m Source #

Natural constructor function. Throws a runtime error if the Int value is greater than the corresponding m or lower than n in the Natural n m type.

Coerce auxiliar functions to help promote Int typed functions to

coerceNat :: (Int -> Int -> Int) -> Natural a a' -> Natural b b' -> Natural c c' Source #

Auxiliary function that promotes binary Int functions to Natural binary functions.

coerceNat2 :: ((Int, Int) -> Int -> Int) -> (Natural a a', Natural b b') -> Natural c c' -> Natural d d' Source #

Auxiliary function that promotes ternary (binary) Int functions to Natural functions.

coerceNat3 :: (Int -> Int -> a) -> Natural b b' -> Natural c c' -> a Source #

Auxiliary function that promotes ternary (binary) Int functions to Natural functions.

Powerset data type

newtype List a Source #

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.

Constructors

L [a] 
Instances
(Enum a, Bounded a) => Bounded (List a) Source # 
Instance details

Defined in LAoP.Utils.Internal

Methods

minBound :: List a #

maxBound :: List a #

(Bounded a, Enum a, Eq a) => Enum (List a) Source # 
Instance details

Defined in LAoP.Utils.Internal

Methods

succ :: List a -> List a #

pred :: List a -> List a #

toEnum :: Int -> List a #

fromEnum :: List a -> Int #

enumFrom :: List a -> [List a] #

enumFromThen :: List a -> List a -> [List a] #

enumFromTo :: List a -> List a -> [List a] #

enumFromThenTo :: List a -> List a -> List a -> [List a] #

Eq a => Eq (List a) Source # 
Instance details

Defined in LAoP.Utils.Internal

Methods

(==) :: List a -> List a -> Bool #

(/=) :: List a -> List a -> Bool #

Read a => Read (List a) Source # 
Instance details

Defined in LAoP.Utils.Internal

Show a => Show (List a) Source # 
Instance details

Defined in LAoP.Utils.Internal

Methods

showsPrec :: Int -> List a -> ShowS #

show :: List a -> String #

showList :: [List a] -> ShowS #