README.md · laop · git.iko.soy

git.iko.soy/laop

on master help sign in

laop/README.md

276 lines 9.4 kB history raw

1# laop - Linear Algebra of Programming library

3[![GitHub CI](https://github.com/bolt12/laop/workflows/CI/badge.svg)](https://github.com/bolt12/laop/actions)

4[![Build status](https://img.shields.io/travis/bolt12/laop.svg?logo=travis)](https://travis-ci.org/bolt12/laop)

5[![Hackage](https://img.shields.io/hackage/v/laop.svg?logo=haskell)](https://hackage.haskell.org/package/laop)

6[![Stackage Lts](http://stackage.org/package/laop/badge/lts)](http://stackage.org/lts/package/laop)

7[![Stackage Nightly](http://stackage.org/package/laop/badge/nightly)](http://stackage.org/nightly/package/laop)

9The LAoP discipline generalises relations and functions treating them as

10Boolean matrices and in turn consider these as arrows.

12__LAoP__ is a library for algebraic (inductive) construction and manipulation of matrices

13in Haskell. See [my Msc Thesis](https://github.com/bolt12/master-thesis) for the

14motivation behind the library, the underlying theory, and implementation details.

16This 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).

19See the package in hackage [here](https://hackage.haskell.org/package/laop-0.1.1.0)

21A Functional Pearl has been written and can be regarded as the [reference document](https://github.com/bolt12/tymfgg-pearl) for this library.

23## Features

25This library offers 3 main matrix programming modules:

27- One in which matrices are typed with type level natural numbers;

28- One in which matrices are typed with arbitrary generic data types;

29- One in which matrices are regarded as relations, i.e. boolean matrices;

31There's also an experimental module that uses matrices to represent probability

32distributions.

34The most interesting feature is that matrices are represented as an inductive data type.

35Given this formulation, matrix algorithms can be expressed in a much more elegant and

36calculational style than the traditional vector of vectors representation. This data type

37guarantees that a matrix will always have valid dimensions. It can also express block matrix

38computations naturally, which leads to total, efficient and statically typed manipulation

39and transformation functions.

41Like 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.

43Given this, this new matrix formulation compared to other libraries:

45- Is more compositional and polymorphic and does not have partial matrix manipulation functions (hence less chances for usage errors);

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.

48## Known issues

50Unfortunately, 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).

52## Notes

54This is still a work in progress, any feedback is welcome!

56## Example

58```Haskell

59{-# LANGUAGE DeriveGeneric #-}

60{-# LANGUAGE FlexibleContexts #-}

61{-# LANGUAGE TypeOperators #-}

62{-# LANGUAGE TypeApplications #-}

63{-# LANGUAGE DataKinds #-}

65module Main where

67import Matrix.Type

68import Utils