LAoP.Utils

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.

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)

• Natural data type

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

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)

Defined in LAoP.Utils.Internal

Methods

minBound :: Natural n m

maxBound :: Natural n m

(KnownNat n, KnownNat m) => Enum (Natural n m)

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)

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)

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

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)

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)

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)

Defined in LAoP.Utils.Internal

Methods

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

show :: Natural start end -> String

showList :: [Natural start end] -> ShowS

Generic (Natural start end)

Defined in LAoP.Utils.Internal

Associated Types

type Rep (Natural start end) :: Type -> Type

Methods

from :: Natural start end -> Rep (Natural start end) x

to :: Rep (Natural start end) x -> Natural start end

NFData (Natural start end)

Defined in LAoP.Utils.Internal

Methods

rnf :: Natural start end -> ()

type Rep (Natural start end)

Defined in LAoP.Utils.Internal

type Rep (Natural start end) = D1 (MetaData "Natural" "LAoP.Utils.Internal" "laop-0.1.1.0-77r4sagBL01x6jU5Cku3u" True) (C1 (MetaCons "Nat" PrefixI False) (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 Int)))

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

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'

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'

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

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

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

List data type

newtype List a

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)

Defined in LAoP.Utils.Internal

Methods

minBound :: List a

maxBound :: List a

(Bounded a, Enum a, Eq a) => Enum (List a)

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)

Defined in LAoP.Utils.Internal

Methods

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

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

Read a => Read (List a)

Defined in LAoP.Utils.Internal

Methods

readsPrec :: Int -> ReadS (List a)

readList :: ReadS [List a]

readPrec :: ReadPrec (List a)

readListPrec :: ReadPrec [List a]

Show a => Show (List a)

Defined in LAoP.Utils.Internal

Methods

showsPrec :: Int -> List a -> ShowS

show :: List a -> String

showList :: [List a] -> ShowS

Category type-class

class Category k where

Constrained category instance

Associated Types

type Object k o :: Constraint

Methods

id :: Object k a => k a a

(.) :: k b c -> k a b -> k a c

Instances

Category Relation

It is possible to implement a constrained version of the category type class.

Defined in LAoP.Relation.Internal

Associated Types

type Object Relation o :: Constraint

Methods

id :: Object Relation a => Relation a a

(.) :: Relation b c -> Relation a b -> Relation a c

Num e => Category (Matrix e)

It is possible to implement a constrained version of the category type class.

Defined in LAoP.Matrix.Internal

Associated Types

type Object (Matrix e) o :: Constraint

Methods

id :: Object (Matrix e) a => Matrix e a a

(.) :: Matrix e b c -> Matrix e a b -> Matrix e a c

Num e => Category (Matrix e)

It is possible to implement a constrained version of the category type class.

Defined in LAoP.Matrix.Type

Associated Types

type Object (Matrix e) o :: Constraint

Methods

id :: Object (Matrix e) a => Matrix e a a

(.) :: Matrix e b c -> Matrix e a b -> Matrix e a c

Category ((->) :: Type -> Type -> Type)

Defined in LAoP.Utils.Internal

Associated Types

type Object (->) o :: Constraint

Methods

id :: Object (->) a => a -> a

(.) :: (b -> c) -> (a -> b) -> a -> c