@@ -1,11 +1,5 @@
1# laop - Linear Algebra of Programming library
1# laop - Linear Algebra of Programming library
3−[](https://github.com/bolt12/laop/actions)
4−[](https://travis-ci.org/bolt12/laop)
5−[](https://hackage.haskell.org/package/laop)
6−[](http://stackage.org/lts/package/laop)
7−[](http://stackage.org/nightly/package/laop)
9The LAoP discipline generalises relations and functions treating them as
3The LAoP discipline generalises relations and functions treating them as
10Boolean matrices and in turn consider these as arrows.
4Boolean matrices and in turn consider these as arrows.
@@ -16,38 +10,40 @@ motivation behind the library, the underlying theory, and implementation details
16This module offers many of the combinators mentioned in the work of
10This module offers many of the combinators mentioned in the work of
17[Macedo (2012)](https://repositorium.sdum.uminho.pt/handle/1822/22894) and [Oliveira (2012)](https://pdfs.semanticscholar.org/ccf5/27fa9179081223bffe8067edd81948644fc0.pdf).
11[Macedo (2012)](https://repositorium.sdum.uminho.pt/handle/1822/22894) and [Oliveira (2012)](https://pdfs.semanticscholar.org/ccf5/27fa9179081223bffe8067edd81948644fc0.pdf).
19−See the package in hackage [here](https://hackage.haskell.org/package/laop-0.1.1.0)
13+See the package in hackage [here](https://hackage.haskell.org/package/laop-0.1.0.5)
15+There are a couple of repos with a WIP of benchmarks comparing [matrix composition](https://github.com/bolt12/laop-benchmarks) and a real use case of [data analytics](https://github.com/bolt12/laop-analytics).
21A Functional Pearl has been written and can be regarded as the [reference document](https://github.com/bolt12/tymfgg-pearl) for this library.
17A Functional Pearl has been written and can be regarded as the [reference document](https://github.com/bolt12/tymfgg-pearl) for this library.
23## Features
19## Features
25−This library offers 3 main matrix programming modules:
21+This library offers:
27−- One in which matrices are typed with type level natural numbers;
23+- An internal module representation that uses normal datatypes (`Void`, `()`, `Either`) for matrix dimensions and two
28−- One in which matrices are typed with arbitrary generic data types;
24+ type families `FromNat` and `Count` to make it easier to work with these type of matrices.
29−- One in which matrices are regarded as relations, i.e. boolean matrices;
25+- An interfacing module that uses generalised types for the dimensions and is just a newtype wrapper
30−
26+ around the internal matrix data type.
31−There's also an experimental module that uses matrices to represent probability
27+- An interfacing module that uses type level naturals for the dimensions and is just a newtype wrapper
32−distributions.
28+ around the internal matrix data type.
33−
29+- An interfacing module that restricts the matrix contents to being only 0's or 1's (True
34−The most interesting feature is that matrices are represented as an inductive data type.
30+ and False). This module is called 'Relation' and offers many of the combinators seen in
35−Given this formulation, matrix algorithms can be expressed in a much more elegant and
31+ AoP and Relational Calculus/Algebra.
36−calculational style than the traditional vector of vectors representation. This data type
32+- A very simple Probabilistic Programming module and several functions and data types to
37−guarantees that a matrix will always have valid dimensions. It can also express block matrix
33+ make it easier to deal with sample space.
38−computations naturally, which leads to total, efficient and statically typed manipulation
34+
39−and transformation functions.
35+Given this, this new matrix formulation compared to other libraries one has much more advantages, such as:
41−Like matrix multiplication, other common operations, such as matrix transposition, benefit from a block-oriented structure that leads to a simple and natural divide-and-conquer algorithmic solution. Performance wise, this means that without much effort we can obtain optimal cache-oblivious algorithms.
37+- Has an inductive definition enabling writing matrix manipulation functions in a much more elegant and calculational way;
42−
38+- Statically typed dimensions;
43−Given this, this new matrix formulation compared to other libraries:
39+- Polymorphic data type dimensions;
44−
40+- Polymorphic matrix content;
45−- Is more compositional and polymorphic and does not have partial matrix manipulation functions (hence less chances for usage errors);
41+- Awesome dimension type inference;
46−- Our implementation of matrices enables simple manipulation of submatrices, making it particularly suitable for formal verification and equation reasoning, using the mathematical framework defined by the linear algebra of programming. Furthermore, the data type constructors ensure that the matrices of this kind are sound, i.e. malformed matrices with incorrect dimensions of the sort, can not be constructed.
42+- Fast type natural conversion via `FromNat` type family;
47−
43+- Matrix `Junc` and `Split`-ing in O(1);
48−## Known issues
44+- Matrix composition takes advantage of divide-and-conquer and fusion laws.
50−Unfortunately, due to the use of type-level programming features, this approach sometimes requires type dimensions to be constrainted, in some way, impossible to write idiomatic Arrow instances, for example. Type inference isn't perfect, when it comes to infer the types of matrices which dimensions are computed using type level naturals multiplication, the compiler needs type annotations in order to succeed. And not all kinds of programs can be modeled using matrices, namely programs that deal with arbitrary infinite data types such as lists or integers (although there are some workarounds).
46+Unfortunately, this approach does not solve the issue of type dimensions being in some way constrainted making it impossible to write Arrow instances, for example. Type inference isn't perfect, when it comes to infer the types of matrices which dimensions are computed using type level naturals multiplication, the compiler needs type annotations in order to succeed.