laop-0.1.0.0: An inductive matrix definition library à la LAoP

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

LAoP.Matrix.Nat

Contents

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

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 FromListsN e a b = FromLists e (FromNat a) (FromNat 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 #