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 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))
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)
type family FromNat (n :: Nat) :: Type where ...
type family Count (d :: Type) :: Nat where ...
type family Normalize (d :: Type) :: Type where ...
class FromLists e cols rows
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
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
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
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
abideJS :: Matrix e cols rows -> Matrix e cols rows
abideSJ :: Matrix e cols rows -> Matrix e cols rows
(===) :: TrivialE a b => Matrix e cols a -> Matrix e cols b -> Matrix e cols (a + b)
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
(|||) :: TrivialE a b => Matrix e a rows -> Matrix e b rows -> Matrix e (a + b) rows
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)
(-|-) :: (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)
(><) :: 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)
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
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
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)
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)
pretty :: (CountableN cols, Show e) => Matrix e cols rows -> String
prettyPrint :: (CountableN cols, 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

Num e => Category (Matrix e :: Nat -> Nat -> Type) Source #	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.
Instance details 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) 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 CountableDimensions a b = (Countable a, Countable b) Source #

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

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

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

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

type FromListsNz e a b = FromLists e (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

empty :: Matrix e 0 0 Source #

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

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

split :: 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 0 = Void
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 (Powerset a) = (^) (Count a) (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 d = FromNat (Count d)

Matrix construction and conversion

class FromLists e cols rows Source #

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 bery much like an inductive definition but on types.

Minimal complete definition

fromLists

Instances

FromLists e () () Source #
Instance details Defined in LAoP.Matrix.Internal Methods fromLists :: [[e]] -> Matrix e () ()
FromLists e Void Void Source #
Instance details 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) Source #
Instance details Defined in LAoP.Matrix.Internal Methods fromLists :: [[e]] -> Matrix e () (Either a b)
FromLists e () rows => FromLists e () (Either () rows) Source #
Instance details 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) () Source #
Instance details Defined in LAoP.Matrix.Internal Methods fromLists :: [[e]] -> Matrix e (Either a b) ()
FromLists e cols () => FromLists e (Either () cols) () Source #
Instance details 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) Source #
Instance details 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 Source #

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

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

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

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

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

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

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

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

constant :: (Num e, FromListsN 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

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

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

Matrix "abiding"

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

Matrix abide Junc Split

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

Matrix abide Split Junc

Biproduct approach

Split

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

Projections

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

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

Junc

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

Injections

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

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

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

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 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

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

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

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

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 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, FromListsN e rows cols) => (a -> b) -> Matrix e cols rows Source #

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

Matrix printing

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

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