LAoP.Matrix.Nat

The LAoP discipline generalises relations and functions treating them as Boolean matrices and in turn consider these as arrows.

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 offers a newtype wrapper around Matrix that uses type level naturals instead of standard data types for the matrices dimensions.

Documentation

LAoP (Linear Algebra of Programming) Inductive Matrix definition.

LAoP generalises relations and functions treating them as Boolean matrices and in turn consider these as arrows. This library offers many of the combinators mentioned in the work of Macedo (2012) and Oliveira (2012).

This definition is a wrapper around Type but dimensions are type level Naturals. Type inference might not be as desired.

There exists two type families that make it easier to write matrix dimensions: FromNat and Count. This approach leads to a very straightforward implementation of LAoP combinators.

Type safe matrix representation

newtype Matrix e (cols :: Nat) (rows :: Nat)

Constructors

M (Matrix e (FromNat cols) (FromNat rows))

Instances

Num e => Category (Matrix e :: Nat -> Nat -> Type)

It isn't possible to implement the id function so it's implementation is undefined. However comp can be and this partial class implementation exists just to make the code more readable.

Please use identity instead.

Defined in LAoP.Matrix.Nat

Methods

id :: Matrix e a a

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

Eq e => Eq (Matrix e cols rows)

Defined in LAoP.Matrix.Nat

Methods

(==) :: Matrix e cols rows -> Matrix e cols rows -> Bool

(/=) :: Matrix e cols rows -> Matrix e cols rows -> Bool

Num e => Num (Matrix e cols rows)

Defined in LAoP.Matrix.Nat

Methods

(+) :: Matrix e cols rows -> Matrix e cols rows -> Matrix e cols rows

(-) :: Matrix e cols rows -> Matrix e cols rows -> Matrix e cols rows

(*) :: Matrix e cols rows -> Matrix e cols rows -> Matrix e cols rows

negate :: Matrix e cols rows -> Matrix e cols rows

abs :: Matrix e cols rows -> Matrix e cols rows

signum :: Matrix e cols rows -> Matrix e cols rows

fromInteger :: Integer -> Matrix e cols rows

Ord e => Ord (Matrix e cols rows)

Defined in LAoP.Matrix.Nat

Methods

compare :: Matrix e cols rows -> Matrix e cols rows -> Ordering

(<) :: Matrix e cols rows -> Matrix e cols rows -> Bool

(<=) :: Matrix e cols rows -> Matrix e cols rows -> Bool

(>) :: Matrix e cols rows -> Matrix e cols rows -> Bool

(>=) :: Matrix e cols rows -> Matrix e cols rows -> Bool

max :: Matrix e cols rows -> Matrix e cols rows -> Matrix e cols rows

min :: Matrix e cols rows -> Matrix e cols rows -> Matrix e cols rows

Show e => Show (Matrix e cols rows)

Defined in LAoP.Matrix.Nat

Methods

showsPrec :: Int -> Matrix e cols rows -> ShowS

show :: Matrix e cols rows -> String

showList :: [Matrix e cols rows] -> ShowS

NFData e => NFData (Matrix e cols rows)

Defined in LAoP.Matrix.Nat

Methods

rnf :: Matrix e cols rows -> ()

Constraint type synonyms

type Countable a = KnownNat (Count a)

Constraint type synonyms to keep the type signatures less convoluted

type CountableDimensions a b = (Countable a, Countable b)

type CountableN a = KnownNat (Count (FromNat a))

type CountableNz a = KnownNat (Count (Normalize a))

type CountableDimensionsN a b = (CountableN a, CountableN b)

type FromListsN e a b = FromLists e (FromNat a) (FromNat b)

type FromListsNz e a b = FromLists e (Normalize a) (Normalize b)

type Liftable e a b = (Bounded a, Bounded b, Enum a, Enum b, Eq b, Num e, Ord e)

type TrivialE a b = FromNat (a + b) ~ Either (FromNat a) (FromNat b)

type TrivialP a b = FromNat (a * b) ~ FromNat (Count (FromNat a) * Count (FromNat b))

Primitives

empty :: Matrix e 0 0

one :: e -> Matrix e 1 1

junc :: TrivialE a b => Matrix e a rows -> Matrix e b rows -> Matrix e (a + b) rows

split :: TrivialE a b => Matrix e cols a -> Matrix e cols b -> Matrix e cols (a + b)

Auxiliary type families

type family FromNat (n :: Nat) :: Type where ...

Type family that computes of a given type dimension from a given natural

Thanks to Li-Yao Xia this type family is super fast.

Equations

FromNat 0 = Void

FromNat 1 = ()

FromNat n = FromNat' (Mod n 2 == 0) (FromNat (Div n 2))

type family Count (d :: Type) :: Nat where ...

Type family that computes the cardinality of a given type dimension.

It can also count the cardinality of custom types that implement the Generic instance.

Equations

Count (Natural n m) = (m - n) + 1

Count (List a) = (^) 2 (Count a)

Count (Either a b) = (+) (Count a) (Count b)

Count (a, b) = * (Count a) (Count b)

Count (a -> b) = (^) (Count b) (Count a)

Count (M1 _ _ f p) = Count (f p)

Count (K1 _ _ _) = 1

Count (V1 _) = 0

Count (U1 _) = 1

Count ((:*:) a b p) = Count (a p) * Count (b p)

Count ((:+:) a b p) = Count (a p) + Count (b p)

Count d = Count (Rep d R)

type family Normalize (d :: Type) :: Type where ...

Type family that normalizes the representation of a given data structure

Equations

Normalize (Either a b) = Either (Normalize a) (Normalize b)

Normalize d = FromNat (Count d)

Matrix construction and conversion

class FromLists e cols rows

Type class for defining the fromList conversion function.

Given that it is not possible to branch on types at the term level type classes are needed very much like an inductive definition but on types.

Minimal complete definition

fromLists

Instances

FromLists e () ()

Defined in LAoP.Matrix.Internal

Methods

fromLists :: [[e]] -> Matrix e () ()

FromLists e Void Void

Defined in LAoP.Matrix.Internal

Methods

fromLists :: [[e]] -> Matrix e Void Void

(FromLists e () a, FromLists e () b, Countable a) => FromLists e () (Either a b)

Defined in LAoP.Matrix.Internal

Methods

fromLists :: [[e]] -> Matrix e () (Either a b)

FromLists e () rows => FromLists e () (Either () rows)

Defined in LAoP.Matrix.Internal

Methods

fromLists :: [[e]] -> Matrix e () (Either () rows)

(FromLists e a (), FromLists e b (), Countable a) => FromLists e (Either a b) ()

Defined in LAoP.Matrix.Internal

Methods

fromLists :: [[e]] -> Matrix e (Either a b) ()

FromLists e cols () => FromLists e (Either () cols) ()

Defined in LAoP.Matrix.Internal

Methods

fromLists :: [[e]] -> Matrix e (Either () cols) ()

(FromLists e (Either a b) c, FromLists e (Either a b) d, Countable c) => FromLists e (Either a b) (Either c d)

Defined in LAoP.Matrix.Internal

Methods

fromLists :: [[e]] -> Matrix e (Either a b) (Either c d)

fromLists :: FromListsN e cols rows => [[e]] -> Matrix e cols rows

toLists :: Matrix e cols rows -> [[e]]

toList :: Matrix e cols rows -> [e]

matrixBuilder :: (FromListsN e cols rows, CountableN cols, CountableN rows) => ((Int, Int) -> e) -> Matrix e cols rows

row :: FromLists e (FromNat cols) () => [e] -> Matrix e cols 1

col :: FromLists e () (FromNat rows) => [e] -> Matrix e 1 rows

zeros :: (Num e, FromListsN e cols rows, CountableN cols, CountableN rows) => Matrix e cols rows

ones :: (Num e, FromListsN e cols rows, CountableN cols, CountableN rows) => Matrix e cols rows

bang :: forall e cols. (Num e, Enum e, FromLists e (FromNat cols) (), CountableN cols) => Matrix e cols 1

constant :: (Num e, FromListsN e cols rows, CountableN cols, CountableN rows) => e -> Matrix e cols rows

Misc

Get dimensions

columns :: CountableN cols => Matrix e cols rows -> Int

rows :: CountableN rows => Matrix e cols rows -> Int

Matrix Transposition

tr :: Matrix e cols rows -> Matrix e rows cols

Matrix transposition

Selective operator

select :: (Num e, FromListsN e rows1 rows1, CountableN rows1, FromNat rows2 ~ FromNat rows1, FromNat cols1 ~ FromNat cols2, FromNat rows3 ~ Either (FromNat cols3) (FromNat rows1)) => Matrix e cols1 rows3 -> Matrix e cols3 rows1 -> Matrix e cols2 rows2

McCarthy's Conditional

cond :: (FromNat (Count (FromNat cols)) ~ FromNat cols, CountableN cols, FromLists e () (FromNat cols), FromLists e (FromNat cols) (), FromListsN e cols cols, Liftable e a Bool) => (a -> Bool) -> Matrix e cols rows -> Matrix e cols rows -> Matrix e cols rows

Matrix "abiding"

abideJS :: Matrix e cols rows -> Matrix e cols rows

Matrix abide Junc Split

abideSJ :: Matrix e cols rows -> Matrix e cols rows

Matrix abide Split Junc

Zip Matrices

zipWithM :: (e -> f -> g) -> Matrix e cols rows -> Matrix f cols rows -> Matrix g cols rows

Zip two matrices with a given binary function

Biproduct approach

Split

(===) :: TrivialE a b => Matrix e cols a -> Matrix e cols b -> Matrix e cols (a + b) infixl 2

Projections

p1 :: (Num e, CountableDimensionsN n m, FromListsN e n m, FromListsN e m m, TrivialE m n) => Matrix e (m + n) m

p2 :: (Num e, CountableDimensionsN n m, FromListsN e m n, FromListsN e n n, TrivialE m n) => Matrix e (m + n) n

Junc

(|||) :: TrivialE a b => Matrix e a rows -> Matrix e b rows -> Matrix e (a + b) rows infixl 3

Injections

i1 :: (Num e, CountableDimensionsN n rows, FromListsN e n rows, FromListsN e rows rows, TrivialE rows n) => Matrix e rows (rows + n)

i2 :: (Num e, CountableDimensionsN rows m, FromListsN e m rows, FromListsN e rows rows, TrivialE m rows) => Matrix e rows (m + rows)

Bifunctors

(-|-) :: (Num e, CountableDimensionsN j k, FromListsN e k k, FromListsN e j k, FromListsN e k j, FromListsN e j j, TrivialE n m, TrivialE k j) => Matrix e n k -> Matrix e m j -> Matrix e (n + m) (k + j) infixl 5

Coproduct Bifunctor

(><) :: forall e m p n q. (Num e, CountableDimensionsN m n, CountableDimensionsN p q, CountableDimensionsN (m * n) (p * q), FromListsN e (m * n) m, FromListsN e (m * n) n, FromListsN e (p * q) p, FromListsN e (p * q) q, TrivialP m n, TrivialP p q) => Matrix e m p -> Matrix e n q -> Matrix e (m * n) (p * q) infixl 4

Product Bifunctor (Kronecker)

Applicative matrix combinators

Note that given the restrictions imposed it is not possible to implement the standard type classes present in standard Haskell. *** Matrix pairing projections

kp1 :: forall e m k. (Num e, CountableDimensionsN m k, CountableN (m * k), FromListsN e (m * k) m, TrivialP m k) => Matrix e (m * k) m

Khatri Rao Product and projections

kp2 :: forall e m k. (Num e, CountableDimensionsN k m, FromListsN e (m * k) k, CountableN (m * k), TrivialP m k) => Matrix e (m * k) k

Matrix pairing

khatri :: forall e cols a b. (Num e, CountableDimensionsN a b, CountableN (a * b), FromListsN e (a * b) a, FromListsN e (a * b) b, TrivialP a b) => Matrix e cols a -> Matrix e cols b -> Matrix e cols (a * b)

Matrix composition and lifting

Arrow matrix combinators

Note that given the restrictions imposed it is not possible to implement the standard type classes present in standard Haskell.

identity :: (Num e, FromListsN e cols cols, CountableN cols) => Matrix e cols cols

comp :: Num e => Matrix e cr rows -> Matrix e cols cr -> Matrix e cols rows

fromF :: (Liftable e a b, CountableN cols, CountableN rows, FromListsN e rows cols) => (a -> b) -> Matrix e cols rows

fromF' :: (Liftable e a b, CountableNz a, CountableNz b, FromListsNz e b a) => (a -> b) -> Matrix e (Count a) (Count b)

Matrix printing

pretty :: (CountableDimensionsN cols rows, Show e) => Matrix e cols rows -> String

prettyPrint :: (CountableDimensionsN cols rows, Show e) => Matrix e cols rows -> IO ()