Copyright	(c) Armando Santos 2019-2020
Maintainer	armandoifsantos@gmail.com
Stability	experimental
Safe Haskell	None
Language	Haskell2010

LAoP.Matrix.Nat

Contents

Type safe matrix representation
Constraint type synonyms
Primitives
Auxiliary type families
Matrix construction and conversion
Misc
Biproduct approach
Matrix composition and lifting
- Arrow matrix combinators
Matrix printing

Description

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.

Synopsis

newtype Matrix e (cols :: Nat) (rows :: Nat) = M (Matrix e (FromNat cols) (FromNat rows))
type Countable a = KnownNat (Count a)
type CountableDims a b = (Countable a, Countable b)
type CountableN a = KnownNat (Count (FromNat a))
type CountableNz a = KnownNat (Count (Normalize a))
type CountableDimsN a b = (CountableN a, CountableN b)
type FLN e a b = FL (FromNat a) (FromNat b)
type FLNz e a b = FL (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))
one :: e -> Matrix e 1 1
join :: TrivialE a b => Matrix e a rows -> Matrix e b rows -> Matrix e (a + b) rows
fork :: TrivialE a b => Matrix e cols a -> Matrix e cols b -> Matrix e cols (a + b)
type family FromNat (n :: Nat) :: Type where ...
type family Count (d :: Type) :: Nat where ...
type family Normalize (d :: Type) :: Type where ...
type FL a b = FromLists a b
fromLists :: FLN e cols rows => [[e]] -> Matrix e cols rows
toLists :: Matrix e cols rows -> [[e]]
toList :: Matrix e cols rows -> [e]
matrixBuilder' :: (FLN e cols rows, CountableN cols, CountableN rows) => ((Int, Int) -> e) -> Matrix e cols rows
row :: FL (FromNat cols) () => [e] -> Matrix e cols 1
col :: FL () (FromNat rows) => [e] -> Matrix e 1 rows
zeros :: (Num e, FLN e cols rows, CountableN cols, CountableN rows) => Matrix e cols rows
ones :: (Num e, FLN e cols rows, CountableN cols, CountableN rows) => Matrix e cols rows
bang :: forall e cols. (Num e, Enum e, FL (FromNat cols) (), CountableN cols) => Matrix e cols 1
constant :: (Num e, FLN e cols rows, CountableN cols, CountableN rows) => e -> Matrix e cols rows
columns :: CountableN cols => Matrix e cols rows -> Int
rows :: CountableN rows => Matrix e cols rows -> Int
tr :: Matrix e cols rows -> Matrix e rows cols
(.|) :: Num e => e -> Matrix e cols rows -> Matrix e cols rows
(./) :: Fractional e => Matrix e cols rows -> e -> Matrix e cols rows
select :: (Num e, FLN 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
cond :: (FromNat (Count (FromNat cols)) ~ FromNat cols, CountableN cols, FL () (FromNat cols), FL (FromNat cols) (), FLN e cols cols, Liftable e a Bool) => (a -> Bool) -> Matrix e cols rows -> Matrix e cols rows -> Matrix e cols rows
abideJF :: Matrix e cols rows -> Matrix e cols rows
abideFJ :: Matrix e cols rows -> Matrix e cols rows
zipWithM :: (e -> f -> g) -> Matrix e cols rows -> Matrix f cols rows -> Matrix g cols rows
(===) :: TrivialE a b => Matrix e cols a -> Matrix e cols b -> Matrix e cols (a + b)
p1 :: (Num e, CountableDimsN n m, FLN e n m, FLN e m m, TrivialE m n) => Matrix e (m + n) m
p2 :: (Num e, CountableDimsN n m, FLN e m n, FLN e n n, TrivialE m n) => Matrix e (m + n) n
(|||) :: TrivialE a b => Matrix e a rows -> Matrix e b rows -> Matrix e (a + b) rows
i1 :: (Num e, CountableDimsN n rows, FLN e n rows, FLN e rows rows, TrivialE rows n) => Matrix e rows (rows + n)
i2 :: (Num e, CountableDimsN rows m, FLN e m rows, FLN e rows rows, TrivialE m rows) => Matrix e rows (m + rows)
(-|-) :: (Num e, CountableDimsN j k, FLN e k k, FLN e j k, FLN e k j, FLN e j j, TrivialE n m, TrivialE k j) => Matrix e n k -> Matrix e m j -> Matrix e (n + m) (k + j)
(><) :: forall e m p n q. (Num e, CountableDimsN m n, CountableDimsN p q, CountableDimsN (m * n) (p * q), FLN e (m * n) m, FLN e (m * n) n, FLN e (p * q) p, FLN e (p * q) q, TrivialP m n, TrivialP p q) => Matrix e m p -> Matrix e n q -> Matrix e (m * n) (p * q)
fstM :: forall e m k. (Num e, CountableDimsN m k, CountableN (m * k), FLN e (m * k) m, TrivialP m k) => Matrix e (m * k) m
sndM :: forall e m k. (Num e, CountableDimsN k m, FLN e (m * k) k, CountableN (m * k), TrivialP m k) => Matrix e (m * k) k
kr :: forall e cols a b. (Num e, CountableDimsN a b, CountableN (a * b), FLN e (a * b) a, FLN e (a * b) b, TrivialP a b) => Matrix e cols a -> Matrix e cols b -> Matrix e cols (a * b)
iden :: (Num e, FLN 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, FLN e rows cols) => (a -> b) -> Matrix e cols rows
fromF :: (Liftable e a b, CountableNz a, CountableNz b, FLNz e b a) => (a -> b) -> Matrix e (Count a) (Count b)
pretty :: (CountableDimsN cols rows, Show e) => Matrix e cols rows -> String
prettyPrint :: (CountableDimsN cols rows, Show e) => Matrix e cols rows -> IO ()

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) Source #

Constructors

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

Instances

Eq e => Eq (Matrix e cols rows) Source #
Instance details 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) Source #
Instance details 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) Source #
Instance details 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) Source #
Instance details 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) Source #
Instance details Defined in LAoP.Matrix.Nat Methods rnf :: Matrix e cols rows -> () #

Constraint type synonyms

type Countable a = KnownNat (Count a) Source #

Constraint type synonyms to keep the type signatures less convoluted

type CountableDims a b = (Countable a, Countable b) Source #

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

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

type CountableDimsN a b = (CountableN a, CountableN b) Source #

type FLN e a b = FL (FromNat a) (FromNat b) Source #

type FLNz e a b = FL (Normalize a) (Normalize b) Source #

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

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

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

Primitives

one :: e -> Matrix e 1 1 Source #

join :: TrivialE a b => Matrix e a rows -> Matrix e b rows -> Matrix e (a + b) rows Source #

fork :: TrivialE a b => Matrix e cols a -> Matrix e cols b -> Matrix e cols (a + b) Source #

Auxiliary type families

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

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 1 = ()
FromNat n = FromNat' (Mod n 2 == 0) (FromNat (Div n 2))

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

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 ... Source #

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

type FL a b = FromLists a b Source #

fromLists :: FLN e cols rows => [[e]] -> Matrix e cols rows Source #

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

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

matrixBuilder' :: (FLN e cols rows, CountableN cols, CountableN rows) => ((Int, Int) -> e) -> Matrix e cols rows Source #

Matrix builder function. Constructs a matrix provided with a construction function that operates with indices.

row :: FL (FromNat cols) () => [e] -> Matrix e cols 1 Source #

col :: FL () (FromNat rows) => [e] -> Matrix e 1 rows Source #

zeros :: (Num e, FLN e cols rows, CountableN cols, CountableN rows) => Matrix e cols rows Source #

ones :: (Num e, FLN e cols rows, CountableN cols, CountableN rows) => Matrix e cols rows Source #

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

constant :: (Num e, FLN e cols rows, CountableN cols, CountableN rows) => e -> Matrix e cols rows Source #

Misc

Get dimensions

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

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

Matrix Transposition

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

Matrix transposition

Scalar multiplication/division of matrices

(.|) :: Num e => e -> Matrix e cols rows -> Matrix e cols rows infixl 7 Source #

Scalar multiplication of matrices.

(./) :: Fractional e => Matrix e cols rows -> e -> Matrix e cols rows infixl 7 Source #

Scalar multiplication of matrices.

Selective operator

select :: (Num e, FLN 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 Source #

McCarthy's Conditional

cond :: (FromNat (Count (FromNat cols)) ~ FromNat cols, CountableN cols, FL () (FromNat cols), FL (FromNat cols) (), FLN e cols cols, Liftable e a Bool) => (a -> Bool) -> Matrix e cols rows -> Matrix e cols rows -> Matrix e cols rows Source #

Matrix "abiding"

abideJF :: Matrix e cols rows -> Matrix e cols rows Source #

Matrix abide Join Fork

abideFJ :: Matrix e cols rows -> Matrix e cols rows Source #

Matrix abide Fork Join

Zip Matrices

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

Zip two matrices with a given binary function

Biproduct approach

Fork

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

Projections

p1 :: (Num e, CountableDimsN n m, FLN e n m, FLN e m m, TrivialE m n) => Matrix e (m + n) m Source #

p2 :: (Num e, CountableDimsN n m, FLN e m n, FLN e n n, TrivialE m n) => Matrix e (m + n) n Source #

Join

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

Injections

i1 :: (Num e, CountableDimsN n rows, FLN e n rows, FLN e rows rows, TrivialE rows n) => Matrix e rows (rows + n) Source #

i2 :: (Num e, CountableDimsN rows m, FLN e m rows, FLN e rows rows, TrivialE m rows) => Matrix e rows (m + rows) Source #

Bifunctors

(-|-) :: (Num e, CountableDimsN j k, FLN e k k, FLN e j k, FLN e k j, FLN 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 Source #

Coproduct Bifunctor (Direct sum)

(><) :: forall e m p n q. (Num e, CountableDimsN m n, CountableDimsN p q, CountableDimsN (m * n) (p * q), FLN e (m * n) m, FLN e (m * n) n, FLN e (p * q) p, FLN 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 Source #

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

fstM :: forall e m k. (Num e, CountableDimsN m k, CountableN (m * k), FLN e (m * k) m, TrivialP m k) => Matrix e (m * k) m Source #

Khatri Rao Product first projection

sndM :: forall e m k. (Num e, CountableDimsN k m, FLN e (m * k) k, CountableN (m * k), TrivialP m k) => Matrix e (m * k) k Source #

Khatri Rao Product second projection

Matrix pairing

kr :: forall e cols a b. (Num e, CountableDimsN a b, CountableN (a * b), FLN e (a * b) a, FLN e (a * b) b, TrivialP a b) => Matrix e cols a -> Matrix e cols b -> Matrix e cols (a * b) Source #

Khatri Rao Product

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.

iden :: (Num e, FLN e cols cols, CountableN cols) => Matrix e cols cols Source #

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

fromF' :: (Liftable e a b, CountableN cols, CountableN rows, FLN e rows cols) => (a -> b) -> Matrix e cols rows Source #

fromF :: (Liftable e a b, CountableNz a, CountableNz b, FLNz e b a) => (a -> b) -> Matrix e (Count a) (Count b) Source #

Matrix printing

pretty :: (CountableDimsN cols rows, Show e) => Matrix e cols rows -> String Source #

prettyPrint :: (CountableDimsN cols rows, Show e) => Matrix e cols rows -> IO () Source #