f047a9c...master · laop

git.iko.soy/laop

on master help sign in

28 files changed+2449−1467

since splitsnapshots

unifiedsplit

.github/workflows/ci.ymlnew file+43

@@ -0,0 +1,43 @@

1+name: CI

3+# Trigger the workflow on push or pull request, but only for the master branch

4+on:

5+ pull_request:

6+ push:

7+ branches: [master]

9+jobs:

10+ build:

11+ name: ghc ${{ matrix.ghc }}

12+ runs-on: ubuntu-16.04

13+ strategy:

14+ matrix:

15+ cabal: ["3.0"]

16+ ghc:

17+ - "8.6.5"

18+ - "8.8.3"

19+

20+ steps:

21+ - uses: actions/checkout@v2

22+ if: github.event.action == 'opened' || github.event.action == 'synchronize' || github.event.ref == 'refs/heads/master'

23+

24+ - uses: actions/setup-haskell@v1

25+ name: Setup Haskell

26+ with:

27+ ghc-version: ${{ matrix.ghc }}

28+ cabal-version: ${{ matrix.cabal }}

29+

30+ - uses: actions/cache@v1

31+ name: Cache ~/.cabal/store

32+ with:

33+ path: ~/.cabal/store

34+ key: ${{ runner.os }}-${{ matrix.ghc }}-cabal

35+

36+ - name: Build

37+ run: |

38+ cabal v2-update

39+ cabal v2-build --enable-tests --enable-benchmarks

40+

41+ - name: Test

42+ run: |

43+ cabal v2-test --enable-tests

.gitignore+54−2

@@ -1,3 +1,55 @@

1+### Haskell

2+dist

3+dist-*

4+cabal-dev

5+*.o

6+*.hi

7+*.chi

8+*.chs.h

9+*.dyn_o

10+*.dyn_hi

11+*.prof

12+*.aux

13+*.hp

14+*.eventlog

15+.virtualenv

16+.hsenv

17+.hpc

18+.cabal-sandbox/

19+cabal.sandbox.config

20+cabal.config

21+cabal.project.local

22+.ghc.environment.*

23+.HTF/

24+# Stack

125.stack-work/

2−laop.cabal

3−*~

26+stack.yaml.lock

27+

28+### IDE/support

29+# Vim

30+[._]*.s[a-v][a-z]

31+[._]*.sw[a-p]

32+[._]s[a-v][a-z]

33+[._]sw[a-p]

34+*~

35+tags

36+

37+# IntellijIDEA

38+.idea/

39+.ideaHaskellLib/

40+*.iml

41+

42+# Atom

43+.haskell-ghc-mod.json

44+

45+# VS

46+.vscode/

47+

48+# Emacs

49+*#

50+.dir-locals.el

51+TAGS

52+

53+# other

54+.DS_Store

55+hackage.sh

.travis.ymlnew file+47

@@ -0,0 +1,47 @@

1+sudo: true

2+language: haskell

4+git:

5+ depth: 5

7+cabal: "3.0"

9+cache:

10+ directories:

11+ - "$HOME/.cabal/store"

12+ - "$HOME/.stack"

13+ - "$TRAVIS_BUILD_DIR/.stack-work"

14+

15+matrix:

16+ include:

17+ - ghc: 8.6.5

18+ - ghc: 8.8.3

19+

20+ - ghc: 8.8.3

21+ env: STACK_YAML="$TRAVIS_BUILD_DIR/stack-8.8.3.yaml"

22+

23+ - ghc: 8.6.5

24+ env: STACK_YAML="$TRAVIS_BUILD_DIR/stack.yaml"

25+

26+

27+install:

28+ - |

29+ if [ -z "$STACK_YAML" ]; then

30+ cabal v2-update

31+ cabal v2-build --enable-tests --enable-benchmarks

32+ else

33+ curl -sSL https://get.haskellstack.org/ | sh

34+ stack --version

35+ stack build --system-ghc --test --bench --no-run-tests --no-run-benchmarks

36+ fi

37+

38+script:

39+ - |

40+ if [ -z "$STACK_YAML" ]; then

41+ cabal v2-test --enable-tests

42+ else

43+ stack test --system-ghc

44+ fi

45+

46+notifications:

47+ email: false

CHANGELOG.mdnew file+17

@@ -0,0 +1,17 @@

1+# Changelog

3+`laop` uses [PVP Versioning][1].

4+The changelog is available [on GitHub][2].

6+## 0.1.1.1

8+* Bump base version to work with cabal

10+## 0.1.1.0

11+

12+* Package is more organized and now has tests and benchmarks separated

13+* Repository is more organized and clean

14+* Added CI

15+

16+[1]: https://pvp.haskell.org

17+[2]: https://github.com/bolt12/laop2/releases

ChangeLog.mddeleted−3

@@ -1,3 +0,0 @@

1−# Changelog for laop

2−

3−## Unreleased changes

LICENSE+17−26

@@ -1,30 +1,21 @@

1+MIT License

5−Redistribution and use in source and binary forms, with or without

6−modification, are permitted provided that the following conditions are met:

5+Permission is hereby granted, free of charge, to any person obtaining a copy

6+of this software and associated documentation files (the "Software"), to deal

7+in the Software without restriction, including without limitation the rights

8+to use, copy, modify, merge, publish, distribute, sublicense, and/or sell

9+copies of the Software, and to permit persons to whom the Software is

10+furnished to do so, subject to the following conditions:

711

8− * Redistributions of source code must retain the above copyright

9− notice, this list of conditions and the following disclaimer.

12+The above copyright notice and this permission notice shall be included in all

13+copies or substantial portions of the Software.

1014

11− * Redistributions in binary form must reproduce the above

12− copyright notice, this list of conditions and the following

13− disclaimer in the documentation and/or other materials provided

14− with the distribution.

15−

16− * Neither the name of Armando Santos nor the names of other

17− contributors may be used to endorse or promote products derived

18− from this software without specific prior written permission.

19−

20−THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS

21−"AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT

22−LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR

23−A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT

24−OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL,

25−SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT

26−LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE,

27−DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY

28−THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT

29−(INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE

30−OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.

15+THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR

16+IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY,

17+FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE

18+AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER

19+LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM,

20+OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE

21+SOFTWARE.

README.md+107−24

@@ -1,5 +1,11 @@

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

39The LAoP discipline generalises relations and functions treating them as

410Boolean matrices and in turn consider these as arrows.

511

@@ -10,33 +16,38 @@ motivation behind the library, the underlying theory, and implementation details

1016This module offers many of the combinators mentioned in the work of

1117[Macedo (2012)](https://repositorium.sdum.uminho.pt/handle/1822/22894) and [Oliveira (2012)](https://pdfs.semanticscholar.org/ccf5/27fa9179081223bffe8067edd81948644fc0.pdf).

1218

13−See the candidate package in hackage [here](https://hackage.haskell.org/package/laop-0.1.0.0/candidate)

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

20+

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

1422

1523## Features

1624

17−This library offers:

18−

19−- An internal representation that uses normal datatypes (`Void`, `()`, `Either`) for matrix dimensions and two

20− type families `FromNat` and `Count` to make it easier to work with these type of matrices.

21−- A module that uses generalised types for the dimensions and is just a newtype wrapper

22− around the internal matrix data type.

23−- Other that uses type level naturals for the dimensions and is just a newtype wrapper

24− around the internal matrix data type.

25−- A very simple Probabilistic Programming module and several functions and data types to

26− make it easier to deal with sample space.

27−

28−Given this, this new matrix formulation compared to other libraries one has much more advantages, such as:

29−

30−- Has an inductive definition enabling writing matrix manipulation functions in a much more elegant and calculational way;

31−- Statically typed dimensions;

32−- Polymorphic data type dimensions;

33−- Polymorphic matrix content;

34−- Awesome dimension type inference;

35−- Fast type natural conversion via `FromNat` type family;

36−- Matrix `Junc` and `Split`-ing in O(1);

37−- Matrix composition takes advantage of divide-and-conquer and fusion laws.

38−

39−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.

25+This library offers 3 main matrix programming modules:

26+

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;

30+

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

32+distributions.

33+

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

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

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

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

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

39+and transformation functions.

40+

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.

42+

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

44+

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.

47+

48+## Known issues

49+

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

4051

4152## Notes

4253

@@ -118,6 +129,73 @@ grass_wet = row [0,1] . kp1

118129rainning :: Matrix Double (Bool, (Bool, Bool)) One

119130rainning = row [0,1] . kp2 . kp2

120131

132+-- Alcuin Puzzle

133+

134+data Being = Farmer | Fox | Goose | Beans

135+ deriving (Bounded, Enum, Eq, Show, Generic)

136+

137+data Bank = LeftB | RightB

138+ deriving (Bounded, Enum, Eq, Show, Generic)

139+

140+eats :: Being -> Being -> Bool

141+eats Fox Goose = True

142+eats Goose Beans = True

143+eats _ _ = False

144+

145+eatsR :: R.Relation Being Being

146+eatsR = R.toRel eats

147+

148+cross :: Bank -> Bank

149+cross LeftB = RightB

150+cross RightB = LeftB

151+

152+crossR :: R.Relation Bank Bank

153+crossR = R.fromF' cross

154+

155+-- | Initial state, everyone in the left bank

156+locationLeft :: Being -> Bank

157+locationLeft _ = LeftB

158+

159+locationLeftR :: R.Relation Being Bank

160+locationLeftR = R.fromF' locationLeft

161+

162+-- | Initial state, everyone in the right bank

163+locationRight :: Being -> Bank

164+locationRight _ = RightB

165+

166+locationRightR :: R.Relation Being Bank

167+locationRightR = R.fromF' locationRight

168+

169+-- Properties

170+

171+-- Being at the same bank

172+sameBank :: R.Relation Being Bank -> R.Relation Being Being

173+sameBank = R.ker

174+

175+-- Risk of somebody eating somebody else

176+canEat :: R.Relation Being Bank -> R.Relation Being Being

177+canEat w = sameBank w `R.intersection` eatsR

178+

179+-- "Starvation" property.

180+inv :: R.Relation Being Bank -> Bool

181+inv w = (w `R.comp` canEat w) `R.sse` (w `R.comp` farmer)

182+ where

183+ farmer :: R.Relation Being Being

184+ farmer = R.fromF' (const Farmer)

185+

186+-- Arbitrary state

187+bankState :: Being -> Bank -> Bool

188+bankState Farmer LeftB = True

189+bankState Fox LeftB = True

190+bankState Goose RightB = True

191+bankState Beans RightB = True

192+bankState _ _ = False

193+

194+bankStateR :: R.Relation Being Bank

195+bankStateR = R.toRel bankState

196+

197+-- Main

198+

121199main :: IO ()

122200main = do

123201 putStrLn "Monty Hall Problem solution:"

@@ -132,6 +210,8 @@ main = do

132210 prettyPrint (grass_wet . state)

133211 putStrLn "\n Probability of rain:"

134212 prettyPrint (rainning . state)

213+ putStrLn "\n Is the arbitrary state a valid state? (Alcuin Puzzle)"

214+ print (inv bankStateR)

135215```

136216

137217```Shell

@@ -190,4 +270,7 @@ Monty Hall Problem solution:

190270┌ ┐

191271│ 0.2 │

192272└ ┘

273+

274+Is the arbitrary state a valid state? (Alcuin Puzzle)

275+False

193276```

Setup.hsdeleted−2

@@ -1,2 +0,0 @@

1−import Distribution.Simple

2−main = defaultMain

appveyor.ymlnew file+34

@@ -0,0 +1,34 @@

1+clone_folder: "c:\\WORK"

2+clone_depth: 5

4+# Do not build feature branch with open Pull Requests

5+skip_branch_with_pr: true

7+platform:

8+ - x86_64

10+cache:

11+ - "C:\\SR"

12+ - dist-newstyle

13+

14+environment:

15+ global:

16+ CABOPTS: --store-dir=C:\\SR

17+

18+ matrix:

19+ - GHCVER: 8.6.5

20+

21+install:

22+ - choco source add -n mistuke -s https://www.myget.org/F/mistuke/api/v2

23+ - choco install -y cabal --version 2.4.1.0

24+ - choco install -y ghc --version 8.6.3

25+ - refreshenv

26+

27+before_build:

28+ - cabal --version

29+ - ghc --version

30+ - cabal %CABOPTS% v2-update

31+

32+build_script:

33+ - cabal %CABOPTS% v2-build --enable-tests

34+ - cabal %CABOPTS% v2-test --enable-tests

benchmark/Main.hsnew file+175

@@ -0,0 +1,175 @@

1+{-# LANGUAGE KindSignatures #-}

2+{-# LANGUAGE GeneralizedNewtypeDeriving #-}

3+{-# LANGUAGE DerivingVia #-}

4+{-# LANGUAGE DataKinds #-}

5+{-# LANGUAGE BangPatterns #-}

6+{-# LANGUAGE TypeApplications #-}

7+{-# LANGUAGE FlexibleContexts #-}

8+{-# LANGUAGE AllowAmbiguousTypes #-}

9+{-# LANGUAGE ScopedTypeVariables #-}

10+

11+module Main (main) where

12+

13+import LAoP.Dist.Internal

14+import LAoP.Utils

15+import LAoP.Matrix.Type hiding (CountableN, Countable, FLN)

16+import qualified LAoP.Matrix.Type as T (FLN)

17+import Criterion.Main

18+import Control.DeepSeq

19+import Test.QuickCheck

20+import GHC.TypeLits

21+import Data.Proxy

22+import Prelude hiding (id, (.))

23+

24+selectM2 ::

25+ ( Num e,

26+ T.FLN b b,

27+ CountableN b

28+ ) => Matrix e cols (Either a b) -> Matrix e a b -> Matrix e cols b

29+selectM2 m y = join y iden `comp` m

30+

31+selectD2 ::

32+ ( FLN b b,

33+ CountableN b

34+ ) => Dist (Either a b) -> Matrix Prob a b -> Dist b

35+selectD2 (D d) m = D (join m iden `comp` d)

36+

37+-- Composition with iden

38+compId m = comp iden m

39+

40+randomDist :: forall a . (Countable a, FLN () a) => Gen (Dist a)

41+randomDist = do

42+ let size = fromInteger (natVal (Proxy :: Proxy (Count a)))

43+ l <- vectorOf size (arbitrary :: Gen Prob)

44+ let ln = normalize l

45+ lr = map (:[]) ln

46+ m = fromLists lr

47+ return (D m)

48+

49+randomMatrix :: forall a b . (CountableDims a b, FLN a b) => Gen (Matrix Prob a b)

50+randomMatrix = do

51+ let cols = fromInteger (natVal (Proxy :: Proxy (Count a)))

52+ rows = fromInteger (natVal (Proxy :: Proxy (Count b)))

53+ l <- vectorOf (cols * rows) arbitrary

54+ let lr = buildList l cols

55+ m = fromLists lr

56+ return m

57+

58+buildList [] _ = []

59+buildList l r = take r l : buildList (drop r l) r

60+

61+normalize :: [Prob] -> [Prob]

62+normalize l = let l' = map abs l

63+ s = sum l'

64+ in map (/ s) l'

65+

66+-- Probability

67+newtype Probability = P Double

68+ deriving (Num, Show, Fractional, NFData) via Double

69+newtype Dist' a = D' { unD :: [(a,Probability)] }

70+ deriving (Show, NFData)

71+

72+instance Functor Dist' where

73+ fmap f (D' d) = D' [(f x,p) | (x,p) <- d]

74+

75+instance Applicative Dist' where

76+ pure x = D' [(x, 1)]

77+ fm <*> m = D' [(f x,q*p) | (f,p) <- unD fm, (x,q) <- unD m]

78+

79+class Applicative f => Selective f where

80+ select :: f (Either a b) -> f (a -> b) -> f b

81+

82+instance Selective Dist' where

83+ select x y = (\e f -> either f id e) <$> x <*> y -- selectA

84+

85+instance Monad Dist' where

86+ return = pure

87+ (D' d) >>= f = D' [(y,q*p) | (x,p) <- d, (y,q) <- unD (f x)]

88+

89+normalize2 :: forall a . (Enum a, Bounded a) => [Probability] -> [(a, Probability)]

90+normalize2 l = let l' = map abs l

91+ as = [minBound .. maxBound]

92+ s = sum l'

93+ probs = map (/ s) l'

94+ in zip as probs

95+

96+randomDist2 :: forall a . (Countable a, Enum a, Bounded a) => Gen (Dist' a)

97+randomDist2 = do

98+ let size = fromInteger (natVal (Proxy :: Proxy (Count a)))

99+ l <- vectorOf size (arbitrary :: Gen Prob)

100+ let ln = normalize2 @a (map P l)

101+ return (D' ln)

102+

103+normalize3 :: forall a . [a] -> [Probability] -> [(a, Probability)]

104+normalize3 as l = let s = sum l

105+ probs = map (/ s) l

106+ in zip as probs

107+

108+randomDistF :: forall a b . (CountableDims a b, CoArbitrary a, Arbitrary b) => Gen (Dist' (a -> b))

109+randomDistF = do

110+ let a = fromInteger (natVal (Proxy :: Proxy (Count a)))

111+ b = fromInteger (natVal (Proxy :: Proxy (Count b)))

112+ size = a * b

113+ l <- vectorOf size (arbitrary :: Gen Prob)

114+ l2 <- vectorOf size (arbitrary :: Gen (a -> b))

115+ let !ln = normalize3 l2 (map P l)

116+ return (D' ln)

117+

118+instance CoArbitrary (Natural a b)

119+

120+instance forall (a :: Nat) (b :: Nat). (KnownNat a, KnownNat b) => Arbitrary (Natural a b)

121+ where

122+ arbitrary =

123+ let bottom = fromInteger (natVal (Proxy :: Proxy a))

124+ top = fromInteger (natVal (Proxy :: Proxy b))

125+ in do

126+ x <- arbitrary `suchThat` (\n -> n >= bottom && n <= top)

127+ return (nat x)

128+

129+setupEnv = do

130+ m11 <- generate (resize 1 (randomMatrix @(Natural 0 10) @(Natural 0 10) ))

131+ m12 <- generate (resize 1 (randomMatrix @(Natural 0 10) @(Natural 0 10) ))

132+ m21 <- generate (resize 1 (randomMatrix @(Natural 0 100) @(Natural 0 100) ))

133+ m22 <- generate (resize 1 (randomMatrix @(Natural 0 100) @(Natural 0 100) ))

134+ m31 <- generate (resize 1 (randomMatrix @(Natural 0 200) @(Natural 0 200) ))

135+ m32 <- generate (resize 1 (randomMatrix @(Natural 0 200) @(Natural 0 200) ))

136+ return (m11, m12, m21, m22, m31, m32)

137+

138+setupEnv2 = do

139+ m21 <- generate (resize 1 (randomMatrix @(Natural 0 100) @(Natural 0 100) ))

140+ m40 <- generate (resize 1 (randomMatrix @(Natural 0 100) @(Either (Natural 0 100) (Natural 0 100) )))

141+ dist <- generate (resize 1 (randomDist @(Either (Natural 0 100) (Natural 0 100)) ))

142+ dist2 <- generate (resize 1 (randomMatrix @(Natural 0 100) @(Natural 0 100) ))

143+ distList1 <- generate (resize 1 (randomDist2 @(Either (Natural 0 100) (Natural 0 100))))

144+ distList2 <- generate (resize 1 (randomDistF @(Natural 0 100) @(Natural 0 100)))

145+ return (m21, m40, dist, dist2, distList1, distList2)

146+

147+main :: IO ()

148+main = defaultMain [

149+ env setupEnv $ \ ~(m11, m12, m21, m22, m31, m32) -> bgroup "Matrix Composition" [

150+ bgroup "10x10" [

151+ bench "WHNF - 10x10" $ whnf (comp m11) m12

152+ , bench "NF - 10x10" $ nf (comp m11) m12

153+ ],

154+ bgroup "100x100" [

155+ bench "WHNF - 100x100" $ whnf (comp m21) m22

156+ , bench "NF - 100x100" $ nf (comp m21) m22

157+ ],

158+ bgroup "200x200" [

159+ bench "WHNF - 200x200" $ whnf (comp m31) m32

160+ , bench "NF - 200x200" $ nf (comp m31) m32

161+ ],

162+ bgroup "200x200 - RULES" [

163+ bench "No rules - 200x200" $ nf (comp m21) iden

164+ , bench "Rules - 200x200" $ nf compId m21

165+ ] ],

166+ env setupEnv2 $ \ ~(m21, m40, dist, dist2, dl1, dl2) -> bgroup "Matrix vs List - `select`" [

167+ bgroup "Distribution `select` - 100+100 / 100x100" [

168+ bench "List Distribution - Applicative version" $ nf (select dl1) dl2

169+ , bench "Matrix Distribution - Applicative version" $ nf (selectD2 dist) dist2

170+ , bench "Matrix Distribution - Selective version" $ nf (selectD dist) dist2

171+ ],

172+ bgroup "Matrix `select` - 100x(100+100) / 100x100" [

173+ bench "Applicative version" $ nf (selectM2 m40) m21

174+ , bench "Selective version" $ nf (selectM m40) m21

175+ ] ] ]

laop.cabalnew file+89

@@ -0,0 +1,89 @@

1+cabal-version: 2.4

2+name: laop

3+version: 0.1.1.1

4+synopsis: Matrix programming library

5+description: Matrix programming library that uses a type-safe inductive definition

6+ inspired by the Linear Algebra of Programming

7+homepage: https://github.com/bolt12/laop

8+bug-reports: https://github.com/bolt12/laop/issues

9+license: MIT

10+license-file: LICENSE

11+author: Armando Santos

12+maintainer: Armando Santos <armandoifsantos@gmail.com>

13+copyright: 2020 Armando Santos

14+category: Data

15+build-type: Simple

16+extra-doc-files: README.md

17+ CHANGELOG.md

18+tested-with: GHC == 8.6.5

19+ GHC == 8.8.3

20+

21+source-repository head

22+ type: git

23+ location: https://github.com/bolt12/laop.git

24+

25+common common-options

26+ build-depends: base >= 4.12.0.0 && < 5,

27+ deepseq

28+

29+ ghc-options: -Wall

30+ -Wcompat

31+ -Widentities

32+ -Wincomplete-uni-patterns

33+ -Wincomplete-record-updates

34+ if impl(ghc >= 8.0)

35+ ghc-options: -Wredundant-constraints

36+ if impl(ghc >= 8.2)

37+ ghc-options: -fhide-source-paths

38+ if impl(ghc >= 8.4)

39+ ghc-options: -Wmissing-export-lists

40+ -Wpartial-fields

41+ if impl(ghc >= 8.8)

42+ ghc-options: -Wmissing-deriving-strategies

43+

44+ default-language: Haskell2010

45+

46+library

47+ import: common-options

48+ hs-source-dirs: src

49+ exposed-modules: LAoP.Dist

50+ LAoP.Dist.Internal

51+ LAoP.Matrix.Internal

52+ LAoP.Matrix.Nat

53+ LAoP.Matrix.Type

54+ LAoP.Relation

55+ LAoP.Relation.Internal

56+ LAoP.Utils

57+ LAoP.Utils.Internal

58+

59+test-suite laop-test

60+ import: common-options

61+ type: exitcode-stdio-1.0

62+ hs-source-dirs: test

63+ other-modules: Examples.Readme

64+ main-is: Spec.hs

65+ build-depends: laop

66+ ghc-options: -threaded

67+ -rtsopts

68+ -with-rtsopts=-N

69+ -funfolding-use-threshold=16

70+ -fexcess-precision

71+ -optc-O3

72+ -optc-ffast-math

73+

74+benchmark laop-benchmark

75+ import: common-options

76+ type: exitcode-stdio-1.0

77+ hs-source-dirs: benchmark

78+ main-is: Main.hs

79+ build-depends: criterion

80+ , QuickCheck

81+ , deepseq

82+ , laop

83+ ghc-options: -threaded

84+ -rtsopts

85+ -with-rtsopts=-N

86+ -funfolding-use-threshold=16

87+ -fexcess-precision

88+ -optc-O3

89+ -optc-ffast-math

package.yamldeleted−48

@@ -1,48 +0,0 @@

1−name: laop

2−version: 0.1.0.0

3−github: "bolt12/laop"

4−license: BSD3

5−author: "Armando Santos"

6−maintainer: "armandoifsantos@gmail.com"

7−copyright: "MIT"

8−

9−extra-source-files:

10−- README.md

11−- ChangeLog.md

12−

13−# Metadata used when publishing your package

14−# synopsis: Short description of your package

15−# category: Web

16−

17−# To avoid duplicated efforts in documentation and dealing with the

18−# complications of embedding Haddock markup inside cabal files, it is

19−# common to point users to the README.md file.

20−description: Please see the README on GitHub at <https://github.com/bolt12/laop#readme>

21−

22−dependencies:

23−- base >= 4.7 && < 5

24−

25−library:

26− source-dirs: src

27−

28−executables:

29− laop-exe:

30− main: Main.hs

31− source-dirs: app

32− ghc-options:

33− - -threaded

34− - -rtsopts

35− - -with-rtsopts=-N

36− dependencies:

37− - laop

38−

39−tests:

40− laop-test:

41− main: Spec.hs

42− source-dirs: test

43− ghc-options:

44− - -threaded

45− - -rtsopts

46− - -with-rtsopts=-N

47− dependencies:

48− - laop

src/LAoP/Dist.hs+10

@@ -36,6 +36,14 @@ module LAoP.Dist

3636 Dist (..),

3737 Prob,

3838

39+ -- * Constraint type synonyms

40+ Countable,

41+ CountableN,

42+ CountableDimsN,

43+ FLN,

44+ Liftable,

45+ TrivialP,

46+

3947 -- * Functor instance equivalent functions

4048 fmapD,

4149

@@ -45,6 +53,8 @@ module LAoP.Dist

4553

4654 -- * Selective equivalent functions

4755 selectD,

56+ branchD,

57+ ifD,

4858

4959 -- * Monad equivalent functions

5060 returnD,

src/LAoP/Dist/Internal.hs+87−36

@@ -1,3 +1,5 @@

1+{-# LANGUAGE DerivingVia #-}

2+{-# LANGUAGE ConstraintKinds #-}

13{-# LANGUAGE GADTs #-}

24{-# LANGUAGE AllowAmbiguousTypes #-}

35{-# LANGUAGE TypeApplications #-}

@@ -8,18 +10,27 @@

810{-# LANGUAGE RankNTypes #-}

911

1012module LAoP.Dist.Internal

11− (

13+ (

1214 Dist(..),

1315 Prob,

1416

17+ Countable,

18+ CountableN,

19+ CountableDimsN,

20+ FLN,

21+ Liftable,

22+ TrivialP,

23+

1524 fmapD,

1625 unitD,

1726 multD,

1827 selectD,

28+ branchD,

29+ ifD,

1930 returnD,

2031 bindD,

2132 (??),

22−

33+

2334 choose,

2435 shape,

2536 linear,

@@ -32,11 +43,15 @@ module LAoP.Dist.Internal

3243 )

3344 where

3445

35−import LAoP.Matrix.Type

46+import LAoP.Matrix.Type hiding (TrivialP, Countable, CountableDims, CountableN, CountableDimsN, Liftable, FLN)

47+import Prelude hiding (id, (.))

48+import qualified LAoP.Matrix.Internal as I

3649import LAoP.Utils

3750import GHC.TypeLits

3851import Data.Proxy

3952import Data.List (sortBy)

53+import Control.DeepSeq

54+import Data.Bool

4055

4156-- | Type synonym for probability value

4257type Prob = Double

@@ -44,17 +59,21 @@ type Prob = Double

4459-- | Type synonym for column vector matrices. This represents a probability

4560-- distribution.

4661newtype Dist a = D (Matrix Prob () a)

62+ deriving (Show, Num, Eq, Ord, NFData) via (Matrix Prob () a)

63+

64+-- | Constraint type synonyms to keep the type signatures less convoluted

65+type Countable a = KnownNat (I.Count a)

66+type CountableN a = KnownNat (I.Count (I.Normalize a))

67+type CountableDimsN a b = (CountableN a, CountableN b)

68+type FLN a b = I.FL (I.Normalize a) (I.Normalize b)

69+type Liftable a b = (Bounded a, Bounded b, Enum a, Enum b, Eq b, Num Prob, Ord Prob)

70+type TrivialP a b = Normalize (a, b) ~ Normalize (Normalize a, Normalize b)

4771

4872-- | Functor instance

4973fmapD ::

50− ( Bounded a,

51− Bounded b,

52− Enum a,

53− Enum b,

54− Eq b,

55− KnownNat (Count (Normalize a)),

56− KnownNat (Count (Normalize b)),

57− FromLists Prob (Normalize b) (Normalize a)

74+ ( Liftable a b,

75+ CountableDimsN a b,

76+ FLN b a

5877 )

5978 =>

6079 (a -> b) -> Dist a -> Dist b

@@ -66,26 +85,58 @@ unitD = D (one 1)

6685

6786-- | Applicative/Monoidal instance 'mult' function

6887multD ::

69− ( KnownNat (Count (Normalize a)),

70− KnownNat (Count (Normalize b)),

71− KnownNat (Count (Normalize (a, b))),

72− FromLists Prob (Normalize (a, b)) (Normalize a),

73− FromLists Prob (Normalize (a, b)) (Normalize b),

74− Normalize (a, b) ~ Normalize (Normalize a, Normalize b)

88+ ( CountableDimsN a b,

89+ CountableN (a, b),

90+ FLN (a, b) a,

91+ FLN (a, b) b,

92+ TrivialP a b

7593 ) => Dist a -> Dist b -> Dist (a, b)

76−multD (D a) (D b) = D (khatri a b)

94+multD (D a) (D b) = D (kr a b)

7795

7896-- | Selective instance function

7997selectD ::

80− ( Normalize (Either a b) ~ Either (Normalize a) (Normalize b),

81− FromLists Prob (Normalize b) (Normalize b),

82− KnownNat (Count (Normalize b))

98+ ( FLN b b,

99+ CountableN b

83100 ) => Dist (Either a b) -> Matrix Prob a b -> Dist b

84−selectD (D d) m = D (junc m identity `comp` d)

85−

101+selectD (D d) m = D (selectM d m)

102+

103+-- | Chooses which of the two given effectful

104+-- functions to apply to a given argument;

105+branchD ::

106+ ( Num e,

107+ CountableDimsN a b,

108+ CountableDimsN c (Either b c),

109+ FLN c b,

110+ FLN a b,

111+ FLN a a,

112+ FLN b b,

113+ FLN c c,

114+ FLN b a,

115+ FLN b c,

116+ FLN (Either b c) b,

117+ FLN (Either b c) c

118+ )

119+ => Dist (Either a b) -> Matrix Prob a c -> Matrix Prob b c -> Dist c

120+branchD x l r = f x `selectD` g l `selectD` r

121+ where

122+ f (D m) = D (fork (tr i1) (i1 `comp` tr i2) `comp` m)

123+ g m = i2 `comp` m

124+

125+-- | Branch on a Boolean value, skipping unnecessary computations.

126+ifD ::

127+ ( CountableDimsN a (Either () a),

128+ FLN a a,

129+ FLN a (),

130+ FLN () a,

131+ FLN (Either () a) a

132+ )

133+ => Dist Bool -> Dist a -> Dist a -> Dist a

134+ifD x (D t) (D e) = branchD x' t e

135+ where

136+ x' = bool (Right ()) (Left ()) `fmapD` x

86137

87138-- | Monad instance 'return' function

88−returnD :: forall a . (Enum a, FromLists Prob () (Normalize a), KnownNat (Count a)) => a -> Dist a

139+returnD :: forall a . (Enum a, FLN () a, Countable a) => a -> Dist a

89140returnD a = D (col l)

90141 where

91142 i = fromInteger $ natVal (Proxy :: Proxy (Count a))

@@ -99,8 +150,8 @@ bindD (D d) m = D (m `comp` d)

99150-- | Extract probabilities given an Event.

100151(??) ::

101152 ( Enum a,

102− KnownNat (Count a),

103− FromLists Prob () (Normalize a)

153+ Countable a,

154+ FLN () a

104155 ) => (a -> Bool) -> Dist a -> Prob

105156(??) p d =

106157 let l = toValues d

@@ -110,11 +161,11 @@ bindD (D d) m = D (m `comp` d)

110161-- Distribution Construction

111162

112163-- | Constructs a Bernoulli distribution

113−choose :: (FromLists Prob () (Normalize a)) => Prob -> Dist a

164+choose :: (FLN () a) => Prob -> Dist a

114165choose prob = D (col [prob, 1 - prob])

115166

116167-- | Creates a distribution given a shape function

117−shape :: (FromLists Prob () (Normalize a)) => (Prob -> Prob) -> [a] -> Dist a

168+shape :: (FLN () a) => (Prob -> Prob) -> [a] -> Dist a

118169shape _ [] = error "Probability.shape: empty list"

119170shape f xs =

120171 let incr = 1 / fromIntegral (length xs - 1)

@@ -122,23 +173,23 @@ shape f xs =

122173 in fromFreqs (zip xs ps)

123174

124175-- | Constructs a Linear distribution

125−linear :: (FromLists Prob () (Normalize a)) => [a] -> Dist a

176+linear :: (FLN () a) => [a] -> Dist a

126177linear = shape id

127178

128179-- | Constructs an Uniform distribution

129−uniform :: (FromLists Prob () (Normalize a)) => [a] -> Dist a

180+uniform :: (FLN () a) => [a] -> Dist a

130181uniform = shape (const 1)

131182

132183-- | Constructs an Negative Exponential distribution

133−negExp :: (FromLists Prob () (Normalize a)) => [a] -> Dist a

184+negExp :: (FLN () a) => [a] -> Dist a

134185negExp = shape (\x -> exp (-x))

135186

136187-- | Constructs an Normal distribution

137−normal :: (FromLists Prob () (Normalize a)) => [a] -> Dist a

188+normal :: (FLN () a) => [a] -> Dist a

138189normal = shape (normalCurve 0.5 0.5)

139190

140191-- | Transforms a 'Dist' into a list of pairs.

141−toValues :: forall a . (Enum a, KnownNat (Count a), FromLists Prob () (Normalize a)) => Dist a -> [(a, Prob)]

192+toValues :: forall a . (Enum a, Countable a, FLN () a) => Dist a -> [(a, Prob)]

142193toValues (D d) =

143194 let rows = fromInteger (natVal (Proxy :: Proxy (Count a)))

144195 probs = toList d

@@ -146,7 +197,7 @@ toValues (D d) =

146197 in res

147198

148199-- | Pretty a distribution

149−prettyDist :: forall a. (Show a, Enum a, KnownNat (Count a), FromLists Prob () (Normalize a)) => Dist a -> String

200+prettyDist :: forall a. (Show a, Enum a, Countable a, FLN () a) => Dist a -> String

150201prettyDist d =

151202 let values = sortBy (\(a, p1) (b, p2) -> compare p2 p1) (toValues @a d)

152203 w = maximum (map (length . show . fst) values)

@@ -158,12 +209,12 @@ prettyDist d =

158209 showR n x = show x ++ " "

159210

160211-- | Pretty Print a distribution

161−prettyPrintDist :: forall a . (Show a, Enum a, KnownNat (Count a), FromLists Prob () (Normalize a)) => Dist a -> IO ()

212+prettyPrintDist :: forall a . (Show a, Enum a, Countable a, FLN () a) => Dist a -> IO ()

162213prettyPrintDist = putStrLn . prettyDist @a

163214

164215-- Auxiliary functions

165216

166−fromFreqs :: (FromLists Prob () (Normalize a)) => [(a,Prob)] -> Dist a

217+fromFreqs :: (FLN () a) => [(a,Prob)] -> Dist a

167218fromFreqs xs = D (col (map (\(x,p) -> p/q) xs))

168219 where q = sum $ map snd xs

169220

src/LAoP/Matrix/Internal.hs+472−439

@@ -1,4 +1,6 @@

1+{-# LANGUAGE StrictData #-}

12{-# LANGUAGE TypeFamilyDependencies #-}

3+{-# LANGUAGE ConstraintKinds #-}

24{-# LANGUAGE AllowAmbiguousTypes #-}

35{-# LANGUAGE DataKinds #-}

46{-# LANGUAGE FlexibleContexts #-}

@@ -28,7 +30,7 @@

2830-- motivation behind the library, the underlying theory, and implementation details.

2931--

3032-- This module offers many of the combinators mentioned in the work of

31−-- Macedo (2012) and Oliveira (2012).

33+-- Macedo (2012) and Oliveira (2012).

3234--

3335-- This is an Internal module and it is no supposed to be imported.

3436--

@@ -41,17 +43,26 @@ module LAoP.Matrix.Internal

4143 --

4244 -- There exists two type families that make it easier to write

4345 -- matrix dimensions: 'FromNat' and 'Count'. This approach

44− -- leads to a very straightforward implementation

45− -- of LAoP combinators.

46+ -- leads to a very straightforward implementation

47+ -- of LAoP combinators.

4648

4749 -- * Type safe matrix representation

4850 Matrix (..),

4951

52+ -- * Constraint type aliases

53+ Countable,

54+ CountableDims,

55+ CountableN,

56+ CountableDimsN,

57+ FL,

58+ FLN,

59+ Liftable,

60+ Trivial,

61+

5062 -- * Primitives

51− empty,

5263 one,

53− junc,

54− split,

64+ join,

65+ fork,

5566

5667 -- * Auxiliary type families

5768 FromNat,

@@ -64,6 +75,7 @@ module LAoP.Matrix.Internal

6475 toLists,

6576 toList,

6677 matrixBuilder,

78+ matrixBuilder',

6779 row,

6880 col,

6981 zeros,

@@ -74,28 +86,38 @@ module LAoP.Matrix.Internal

7486 -- * Misc

7587 -- ** Get dimensions

7688 columns,

89+ columns',

7790 rows,

91+ rows',

7892

7993 -- ** Matrix Transposition

8094 tr,

8195

96+ -- ** Scalar multiplication/division of matrices

97+ (.|),

98+ (./),

99+

82100 -- ** Selective operator

83− select,

101+ select,

102+ branch,

84103

85104 -- ** McCarthy's Conditional

86105 cond,

87106

88107 -- ** Matrix "abiding"

89− abideJS,

90− abideSJ,

108+ abideJF,

109+ abideFJ,

110+

111+ -- ** Zip matrices

112+ zipWithM,

91113

92114 -- * Biproduct approach

93− -- ** Split

115+ -- ** Fork

94116 (===),

95117 -- *** Projections

96118 p1,

97119 p2,

98− -- ** Junc

120+ -- ** Join

99121 (|||),

100122 -- *** Injections

101123 i1,

@@ -108,12 +130,13 @@ module LAoP.Matrix.Internal

108130

109131 -- | Note that given the restrictions imposed it is not possible to

110132 -- implement the standard type classes present in standard Haskell.

133+

111134 -- *** Matrix pairing projections

112− kp1,

113− kp2,

135+ fstM,

136+ sndM,

114137

115138 -- *** Matrix pairing

116− khatri,

139+ kr,

117140

118141 -- * Matrix composition and lifting

119142

@@ -121,10 +144,10 @@ module LAoP.Matrix.Internal

121144

122145 -- | Note that given the restrictions imposed it is not possible to

123146 -- implement the standard type classes present in standard Haskell.

124− identity,

147+ iden,

125148 comp,

126− fromF,

127149 fromF',

150+ fromF,

128151

129152 -- * Matrix printing

130153 pretty,

@@ -134,6 +157,9 @@ module LAoP.Matrix.Internal

134157 toBool,

135158 fromBool,

136159 compRel,

160+ divR,

161+ divL,

162+ divS,

137163 fromFRel,

138164 fromFRel',

139165 toRel,

@@ -148,21 +174,22 @@ import LAoP.Utils.Internal

148174import Data.Bool

149175import Data.Kind

150176import Data.List

177+import Data.Maybe

151178import Data.Proxy

179+import Data.Typeable

152180import Data.Void

153181import GHC.TypeLits

154182import Data.Type.Equality

155183import GHC.Generics

156184import Control.DeepSeq

157−import Control.Category

158−import Prelude hiding ((.))

185+import Prelude hiding (id, (.))

186+import qualified Prelude (id, (.))

159187

160188-- | LAoP (Linear Algebra of Programming) Inductive Matrix definition.

161189data Matrix e cols rows where

162− Empty :: Matrix e Void Void

163190 One :: e -> Matrix e () ()

164− Junc :: Matrix e a rows -> Matrix e b rows -> Matrix e (Either a b) rows

165− Split :: Matrix e cols a -> Matrix e cols b -> Matrix e cols (Either a b)

191+ Join :: Matrix e a rows -> Matrix e b rows -> Matrix e (Either a b) rows

192+ Fork :: Matrix e cols a -> Matrix e cols b -> Matrix e cols (Either a b)

166193

167194deriving instance (Show e) => Show (Matrix e cols rows)

168195

@@ -172,221 +199,214 @@ deriving instance (Show e) => Show (Matrix e cols rows)

172199-- 'Generic' instance.

173200type family Count (d :: Type) :: Nat where

174201 Count (Natural n m) = (m - n) + 1

175− Count (Either a b) = (+) (Count a) (Count b)

176− Count (a, b) = (*) (Count a) (Count b)

177− Count (a -> b) = (^) (Count b) (Count a)

202+ Count (List a) = (^) 2 (Count a)

203+ Count (Either a b) = (+) (Count a) (Count b)

204+ Count (a, b) = (*) (Count a) (Count b)

205+ Count (a -> b) = (^) (Count b) (Count a)

178206 -- Generics

179− Count (M1 _ _ f p) = Count (f p)

180− Count (K1 _ _ _) = 1

181− Count (V1 _) = 0

182− Count (U1 _) = 1

207+ Count (M1 _ _ f p) = Count (f p)

208+ Count (K1 _ _ _) = 1

209+ Count (V1 _) = 0

210+ Count (U1 _) = 1

183211 Count ((:*:) a b p) = Count (a p) * Count (b p)

184212 Count ((:+:) a b p) = Count (a p) + Count (b p)

185− Count d = Count (Rep d R)

213+ Count d = Count (Rep d R)

186214

187215-- | Type family that computes of a given type dimension from a given natural

188216--

189217-- Thanks to Li-Yao Xia this type family is super fast.

190218type family FromNat (n :: Nat) :: Type where

191− FromNat 0 = Void

192219 FromNat 1 = ()

193220 FromNat n = FromNat' (Mod n 2 == 0) (FromNat (Div n 2))

194221

195222type family FromNat' (b :: Bool) (m :: Type) :: Type where

196− FromNat' 'True m = Either m m

223+ FromNat' 'True m = Either m m

197224 FromNat' 'False m = Either () (Either m m)

198225

199226-- | Type family that normalizes the representation of a given data

200227-- structure

201228type family Normalize (d :: Type) :: Type where

202− Normalize d = FromNat (Count d)

203−

204−-- | It isn't possible to implement the 'id' function so it's

205−-- implementation is 'undefined'. However 'comp' can be and this partial

206−-- class implementation exists just to make the code more readable.

207−--

208−-- Please use 'identity' instead.

229+ Normalize (Either a b) = Either (Normalize a) (Normalize b)

230+ Normalize d = FromNat (Count d)

231+

232+-- | Constraint type synonyms to keep the type signatures less convoluted

233+type Countable a = KnownNat (Count a)

234+type CountableN a = KnownNat (Count (Normalize a))

235+type CountableDims a b = (Countable a, Countable b)

236+type CountableDimsN a b = (CountableN a, CountableN b)

237+type FL a b = FromLists a b

238+type FLN a b = FromLists (Normalize a) (Normalize b)

239+type Liftable e a b = (Bounded a, Bounded b, Enum a, Enum b, Eq b, Num e, Ord e)

240+type Trivial a = FromNat (Count a) ~ a

241+

242+-- | It is possible to implement a constrained version of the category type

243+-- class.

209244instance (Num e) => Category (Matrix e) where

210− id = undefined

211− (.) = comp

245+ type Object (Matrix e) a = (FL a a, Countable a)

246+ id = iden

247+ (.) = comp

212248

213249instance NFData e => NFData (Matrix e cols rows) where

214− rnf Empty = ()

215− rnf (One e) = rnf e

216− rnf (Junc a b) = rnf a `seq` rnf b

217− rnf (Split a b) = rnf a `seq` rnf b

250+ rnf (One e) = rnf e

251+ rnf (Join a b) = rnf a `seq` rnf b

252+ rnf (Fork a b) = rnf a `seq` rnf b

218253

219254instance Eq e => Eq (Matrix e cols rows) where

220− Empty == Empty = True

221− (One a) == (One b) = a == b

222− (Junc a b) == (Junc c d) = a == c && b == d

223− (Split a b) == (Split c d) = a == c && b == d

224− x@(Split _ _) == y@(Junc _ _) = x == abideJS y

225− x@(Junc _ _) == y@(Split _ _) = abideJS x == y

255+ (One a) == (One b) = a == b

256+ (Join a b) == (Join c d) = a == c && b == d

257+ (Fork a b) == (Fork c d) = a == c && b == d

258+ x@(Fork _ _) == y@(Join _ _) = x == abideJF y

259+ x@(Join _ _) == y@(Fork _ _) = abideJF x == y

226260

227261instance Num e => Num (Matrix e cols rows) where

262+ a + b = zipWithM (+) a b

228263

229− Empty + Empty = Empty

230− (One a) + (One b) = One (a + b)

231− (Junc a b) + (Junc c d) = Junc (a + c) (b + d)

232− (Split a b) + (Split c d) = Split (a + c) (b + d)

233− x@(Split _ _) + y@(Junc _ _) = x + abideJS y

234− x@(Junc _ _) + y@(Split _ _) = abideJS x + y

235−

236− Empty - Empty = Empty

237− (One a) - (One b) = One (a - b)

238− (Junc a b) - (Junc c d) = Junc (a - c) (b - d)

239− (Split a b) - (Split c d) = Split (a - c) (b - d)

240− x@(Split _ _) - y@(Junc _ _) = x - abideJS y

241− x@(Junc _ _) - y@(Split _ _) = abideJS x - y

242−

243− Empty * Empty = Empty

244− (One a) * (One b) = One (a * b)

245− (Junc a b) * (Junc c d) = Junc (a * c) (b * d)

246− (Split a b) * (Split c d) = Split (a * c) (b * d)

247− x@(Split _ _) * y@(Junc _ _) = x * abideJS y

248− x@(Junc _ _) * y@(Split _ _) = abideJS x * y

249−

250− abs Empty = Empty

251− abs (One a) = One (abs a)

252− abs (Junc a b) = Junc (abs a) (abs b)

253− abs (Split a b) = Split (abs a) (abs b)

254−

255− signum Empty = Empty

256− signum (One a) = One (signum a)

257− signum (Junc a b) = Junc (signum a) (signum b)

258− signum (Split a b) = Split (signum a) (signum b)

264+ a - b = zipWithM (-) a b

265+

266+ a * b = zipWithM (*) a b

267+

268+ abs (One a) = One (abs a)

269+ abs (Join a b) = Join (abs a) (abs b)

270+ abs (Fork a b) = Fork (abs a) (abs b)

271+

272+ signum (One a) = One (signum a)

273+ signum (Join a b) = Join (signum a) (signum b)

274+ signum (Fork a b) = Fork (signum a) (signum b)

259275

260276instance Ord e => Ord (Matrix e cols rows) where

261− Empty <= Empty = True

262− (One a) <= (One b) = a <= b

263− (Junc a b) <= (Junc c d) = (a <= c) && (b <= d)

264− (Split a b) <= (Split c d) = (a <= c) && (b <= d)

265− x@(Split _ _) <= y@(Junc _ _) = x <= abideJS y

266− x@(Junc _ _) <= y@(Split _ _) = abideJS x <= y

277+ (One a) <= (One b) = a <= b

278+ (Join a b) <= (Join c d) = (a <= c) && (b <= d)

279+ (Fork a b) <= (Fork c d) = (a <= c) && (b <= d)

280+ x@(Fork _ _) <= y@(Join _ _) = x <= abideJF y

281+ x@(Join _ _) <= y@(Fork _ _) = abideJF x <= y

267282

268283-- Primitives

269284

270−-- | Empty matrix constructor

271−empty :: Matrix e Void Void

272−empty = Empty

273−

274285-- | Unit matrix constructor

275286one :: e -> Matrix e () ()

276287one = One

277288

278−-- | Matrix 'Junc' constructor

279−junc :: Matrix e a rows -> Matrix e b rows -> Matrix e (Either a b) rows

280−junc = Junc

289+-- | Matrix 'Join' constructor

290+join :: Matrix e a rows -> Matrix e b rows -> Matrix e (Either a b) rows

291+join = Join

281292

282293infixl 3 |||

283294

284−-- | Matrix 'Junc' constructor

295+-- | Matrix 'Join' constructor

285296(|||) :: Matrix e a rows -> Matrix e b rows -> Matrix e (Either a b) rows

286−(|||) = Junc

297+(|||) = Join

287298

288−-- | Matrix 'Split' constructor

289−split :: Matrix e cols a -> Matrix e cols b -> Matrix e cols (Either a b)

290−split = Split

299+-- | Matrix 'Fork' constructor

300+fork :: Matrix e cols a -> Matrix e cols b -> Matrix e cols (Either a b)

301+fork = Fork

291302

292303infixl 2 ===

293304

294−-- | Matrix 'Split' constructor

305+-- | Matrix 'Fork' constructor

295306(===) :: Matrix e cols a -> Matrix e cols b -> Matrix e cols (Either a b)

296−(===) = Split

307+(===) = Fork

297308

298309-- Construction

299310

300311-- | Type class for defining the 'fromList' conversion function.

301312--

302313-- Given that it is not possible to branch on types at the term level type

303−-- classes are needed bery much like an inductive definition but on types.

304−class FromLists e cols rows where

314+-- classes are needed very much like an inductive definition but on types.

315+class FromLists cols rows where

305316 -- | Build a matrix out of a list of list of elements. Throws a runtime

306317 -- error if the dimensions do not match.

307318 fromLists :: [[e]] -> Matrix e cols rows

308319

309−instance FromLists e Void Void where

310− fromLists [] = Empty

311− fromLists _ = error "Wrong dimensions"

312−

313−instance {-# OVERLAPPING #-} FromLists e () () where

320+instance FromLists () () where

314321 fromLists [[e]] = One e

315322 fromLists _ = error "Wrong dimensions"

316323

317−instance {-# OVERLAPPING #-} (FromLists e cols ()) => FromLists e (Either () cols) () where

318− fromLists [h : t] = Junc (One h) (fromLists [t])

324+instance (FromLists cols ()) => FromLists (Either () cols) () where

325+ fromLists [h : t] = Join (One h) (fromLists [t])

319326 fromLists _ = error "Wrong dimensions"

320327

321−instance {-# OVERLAPPABLE #-} (FromLists e a (), FromLists e b (), KnownNat (Count a)) => FromLists e (Either a b) () where

322− fromLists [l] =

328+instance {-# OVERLAPPABLE #-}

329+ (FromLists a (), FromLists b (), Countable a) => FromLists (Either a b) () where

330+ fromLists [l] =

323331 let rowsA = fromInteger (natVal (Proxy :: Proxy (Count a)))

324− in Junc (fromLists [take rowsA l]) (fromLists [drop rowsA l])

332+ in Join (fromLists [take rowsA l]) (fromLists [drop rowsA l])

325333 fromLists _ = error "Wrong dimensions"

326334

327−instance {-# OVERLAPPING #-} (FromLists e () rows) => FromLists e () (Either () rows) where

328− fromLists ([h] : t) = Split (One h) (fromLists t)

335+instance (FromLists () rows) => FromLists () (Either () rows) where

336+ fromLists ([h] : t) = Fork (One h) (fromLists t)

329337 fromLists _ = error "Wrong dimensions"

330338

331−instance {-# OVERLAPPABLE #-} (FromLists e () a, FromLists e () b, KnownNat (Count a)) => FromLists e () (Either a b) where

332− fromLists l@([_] : _) =

339+instance {-# OVERLAPPABLE #-}

340+ (FromLists () a, FromLists () b, Countable a) => FromLists () (Either a b) where

341+ fromLists l@([_] : _) =

333342 let rowsA = fromInteger (natVal (Proxy :: Proxy (Count a)))

334− in Split (fromLists (take rowsA l)) (fromLists (drop rowsA l))

343+ in Fork (fromLists (take rowsA l)) (fromLists (drop rowsA l))

335344 fromLists _ = error "Wrong dimensions"

336345

337−instance {-# OVERLAPPABLE #-} (FromLists e (Either a b) c, FromLists e (Either a b) d, KnownNat (Count c)) => FromLists e (Either a b) (Either c d) where

346+instance (FromLists (Either a b) c, FromLists (Either a b) d, Countable c)

347+ => FromLists (Either a b) (Either c d) where

338348 fromLists l@(h : t) =

339349 let lh = length h

340350 rowsC = fromInteger (natVal (Proxy :: Proxy (Count c)))

341− condition = all (== lh) (map length t)

351+ condition = all ((== lh) . length) t

342352 in if lh > 0 && condition

343− then Split (fromLists (take rowsC l)) (fromLists (drop rowsC l))

353+ then Fork (fromLists (take rowsC l)) (fromLists (drop rowsC l))

344354 else error "Not all rows have the same length"

345355

346356-- | Matrix builder function. Constructs a matrix provided with

347−-- a construction function.

348−matrixBuilder ::

357+-- a construction function that operates with indices.

358+matrixBuilder' ::

349359 forall e cols rows.

350− ( FromLists e cols rows,

351− KnownNat (Count cols),

352− KnownNat (Count rows)

353− ) =>

354− ((Int, Int) -> e) ->

355− Matrix e cols rows

356−matrixBuilder f =

360+ ( FL cols rows,

361+ CountableDims cols rows

362+ ) => ((Int, Int) -> e) -> Matrix e cols rows

363+matrixBuilder' f =

357364 let c = fromInteger $ natVal (Proxy :: Proxy (Count cols))

358365 r = fromInteger $ natVal (Proxy :: Proxy (Count rows))

359366 positions = [(a, b) | a <- [0 .. (r - 1)], b <- [0 .. (c - 1)]]

360367 in fromLists . map (map f) . groupBy (\(x, _) (w, _) -> x == w) $ positions

361368

369+-- | Matrix builder function. Constructs a matrix provided with

370+-- a construction function that operates with arbitrary types.

371+matrixBuilder ::

372+ forall e a b.

373+ ( FLN a b,

374+ Enum a,

375+ Enum b,

376+ Bounded a,

377+ Bounded b,

378+ Eq a,

379+ Countable b

380+ ) => ((a, b) -> e) -> Matrix e (Normalize a) (Normalize b)

381+matrixBuilder f =

382+ let r = fromInteger $ natVal (Proxy :: Proxy (Count b))

383+ positions = [(a, b) | a <- [minBound .. maxBound], b <- [minBound .. maxBound]]

384+ in fromLists . map (map f) . transpose . buildList r $ positions

385+ where

386+ buildList _ [] = []

387+ buildList r l = take r l : buildList r (drop r l)

388+

362389-- | Constructs a column vector matrix

363−col :: (FromLists e () rows) => [e] -> Matrix e () rows

390+col :: (FL () rows) => [e] -> Matrix e () rows

364391col = fromLists . map (: [])

365392

366393-- | Constructs a row vector matrix

367−row :: (FromLists e cols ()) => [e] -> Matrix e cols ()

394+row :: (FL cols ()) => [e] -> Matrix e cols ()

368395row = fromLists . (: [])

369396

370397-- | Lifts functions to matrices with arbitrary dimensions.

371398--

372399-- NOTE: Be careful to not ask for a matrix bigger than the cardinality of

373400-- types @a@ or @b@ allows.

374−fromF ::

401+fromF' ::

375402 forall a b cols rows e.

376− ( Bounded a,

377− Bounded b,

378− Enum a,

379− Enum b,

380− Eq b,

381− Num e,

382− Ord e,

383− KnownNat (Count cols),

384− KnownNat (Count rows),

385− FromLists e rows cols

403+ ( Liftable e a b,

404+ CountableDims cols rows,

405+ FL rows cols

386406 ) =>

387407 (a -> b) ->

388408 Matrix e cols rows

389−fromF f =

409+fromF' f =

390410 let minA = minBound @a

391411 maxA = maxBound @a

392412 minB = minBound @b

@@ -396,8 +416,8 @@ fromF f =

396416 elementsA = take ccols [minA .. maxA]

397417 elementsB = take rrows [minB .. maxB]

398418 combinations = (,) <$> elementsA <*> elementsB

399− combAp = map snd . sort . map (\(a, b) -> if f a == b

400− then ((fromEnum a, fromEnum b), 1)

419+ combAp = map snd . sort . map (\(a, b) -> if f a == b

420+ then ((fromEnum a, fromEnum b), 1)

401421 else ((fromEnum a, fromEnum b), 0)) $ combinations

402422 mList = buildList combAp rrows

403423 in tr $ fromLists mList

@@ -407,48 +427,23 @@ fromF f =

407427

408428-- | Lifts functions to matrices with dimensions matching @a@ and @b@

409429-- cardinality's.

410−fromF' ::

430+fromF ::

411431 forall a b e.

412− ( Bounded a,

413− Bounded b,

414− Enum a,

415− Enum b,

416− Eq b,

417− Num e,

418− Ord e,

419− KnownNat (Count (Normalize a)),

420− KnownNat (Count (Normalize b)),

421− FromLists e (Normalize b) (Normalize a)

432+ ( Liftable e a b,

433+ CountableDimsN a b,

434+ FLN b a

422435 ) =>

423436 (a -> b) ->

424437 Matrix e (Normalize a) (Normalize b)

425−fromF' f =

426− let minA = minBound @a

427− maxA = maxBound @a

428− minB = minBound @b

429− maxB = maxBound @b

430− ccols = fromInteger $ natVal (Proxy :: Proxy (Count (Normalize a)))

431− rrows = fromInteger $ natVal (Proxy :: Proxy (Count (Normalize b)))

432− elementsA = take ccols [minA .. maxA]

433− elementsB = take rrows [minB .. maxB]

434− combinations = (,) <$> elementsA <*> elementsB

435− combAp = map snd . sort . map (\(a, b) -> if f a == b

436− then ((fromEnum a, fromEnum b), 1)

437− else ((fromEnum a, fromEnum b), 0)) $ combinations

438− mList = buildList combAp rrows

439− in tr $ fromLists mList

440− where

441− buildList [] _ = []

442− buildList l r = take r l : buildList (drop r l) r

438+fromF = fromF'

443439

444440-- Conversion

445441

446442-- | Converts a matrix to a list of lists of elements.

447443toLists :: Matrix e cols rows -> [[e]]

448−toLists Empty = []

449444toLists (One e) = [[e]]

450−toLists (Split l r) = toLists l ++ toLists r

451−toLists (Junc l r) = zipWith (++) (toLists l) (toLists r)

445+toLists (Fork l r) = toLists l ++ toLists r

446+toLists (Join l r) = zipWith (++) (toLists l) (toLists r)

452447

453448-- | Converts a matrix to a list of elements.

454449toList :: Matrix e cols rows -> [e]

@@ -457,37 +452,38 @@ toList = concat . toLists

457452-- Zeros Matrix

458453

459454-- | The zero matrix. A matrix wholly filled with zeros.

460−zeros :: (Num e, FromLists e cols rows, KnownNat (Count cols), KnownNat (Count rows)) => Matrix e cols rows

461−zeros = matrixBuilder (const 0)

455+zeros :: (Num e, FL cols rows, CountableDims cols rows) => Matrix e cols rows

456+zeros = matrixBuilder' (const 0)

462457

463458-- Ones Matrix

464459

465460-- | The ones matrix. A matrix wholly filled with ones.

466461--

467462-- Also known as T (Top) matrix.

468−ones :: (Num e, FromLists e cols rows, KnownNat (Count cols), KnownNat (Count rows)) => Matrix e cols rows

469−ones = matrixBuilder (const 1)

463+ones :: (Num e, FL cols rows, CountableDims cols rows) => Matrix e cols rows

464+ones = matrixBuilder' (const 1)

470465

471466-- Const Matrix

472467

473468-- | The constant matrix constructor. A matrix wholly filled with a given

474469-- value.

475−constant :: (Num e, FromLists e cols rows, KnownNat (Count cols), KnownNat (Count rows)) => e -> Matrix e cols rows

476−constant e = matrixBuilder (const e)

470+constant :: (Num e, FL cols rows, CountableDims cols rows) => e -> Matrix e cols rows

471+constant e = matrixBuilder' (const e)

477472

478473-- Bang Matrix

479474

480475-- | The T (Top) row vector matrix.

481−bang :: forall e cols. (Num e, Enum e, FromLists e cols (), KnownNat (Count cols)) => Matrix e cols ()

476+bang :: forall e cols. (Num e, Enum e, FL cols (), Countable cols) => Matrix e cols ()

482477bang =

483478 let c = fromInteger $ natVal (Proxy :: Proxy (Count cols))

484479 in fromLists [take c [1, 1 ..]]

485480

486−-- Identity Matrix

481+-- iden Matrix

487482

488−-- | Identity matrix.

489−identity :: (Num e, FromLists e cols cols, KnownNat (Count cols)) => Matrix e cols cols

490−identity = matrixBuilder (bool 0 1 . uncurry (==))

483+-- | iden matrix.

484+iden :: forall e cols . (Num e, FL cols cols, Countable cols) => Matrix e cols cols

485+iden = matrixBuilder' (bool 0 1 . uncurry (==))

486+{-# NOINLINE iden #-}

491487

492488-- Matrix composition (MMM)

493489

@@ -496,60 +492,90 @@ identity = matrixBuilder (bool 0 1 . uncurry (==))

496492-- This definition takes advantage of divide-and-conquer and fusion laws

497493-- from LAoP.

498494comp :: (Num e) => Matrix e cr rows -> Matrix e cols cr -> Matrix e cols rows

499−comp Empty Empty = Empty

500−comp (One a) (One b) = One (a * b)

501−comp (Junc a b) (Split c d) = comp a c + comp b d -- Divide-and-conquer law

502−comp (Split a b) c = Split (comp a c) (comp b c) -- Split fusion law

503−comp c (Junc a b) = Junc (comp c a) (comp c b) -- Junc fusion law

495+comp (One a) (One b) = One (a * b)

496+comp (Join a b) (Fork c d) = comp a c + comp b d -- Divide-and-conquer law

497+comp (Fork a b) c = Fork (comp a c) (comp b c) -- Fork fusion law

498+comp c (Join a b) = Join (comp c a) (comp c b) -- Join fusion law

499+{-# NOINLINE comp #-}

500+{-# RULES

501+ "comp/iden1" forall m. comp m iden = m ;

502+ "comp/iden2" forall m. comp iden m = m

503+#-}

504+

505+-- Scalar multiplication of matrices

506+

507+infixl 7 .|

508+-- | Scalar multiplication of matrices.

509+(.|) :: Num e => e -> Matrix e cols rows -> Matrix e cols rows

510+(.|) e (One a) = One (e * a)

511+(.|) e (Join a b) = Join (e .| a) (e .| b)

512+(.|) e (Fork a b) = Fork (e .| a) (e .| b)

513+

514+-- Scalar division of matrices

515+

516+infixl 7 ./

517+-- | Scalar multiplication of matrices.

518+(./) :: Fractional e => Matrix e cols rows -> e -> Matrix e cols rows

519+(./) (One a) e = One (a / e)

520+(./) (Join a b) e = Join (a ./ e) (b ./ e)

521+(./) (Fork a b) e = Fork (a ./ e) (b ./ e)

504522

505523-- Projections

506524

507525-- | Biproduct first component projection

508−p1 :: forall e m n. (Num e, KnownNat (Count n), KnownNat (Count m), FromLists e n m, FromLists e m m) => Matrix e (Either m n) m

509−p1 =

510− let iden = identity :: Matrix e m m

511− zero = zeros :: Matrix e n m

512− in junc iden zero

526+p1 :: (Num e, CountableDims n m, FL n m, FL m m) => Matrix e (Either m n) m

527+p1 = join id zeros

513528

514529-- | Biproduct second component projection

515−p2 :: forall e m n. (Num e, KnownNat (Count n), KnownNat (Count m), FromLists e m n, FromLists e n n) => Matrix e (Either m n) n

516−p2 =

517− let iden = identity :: Matrix e n n

518− zero = zeros :: Matrix e m n

519− in junc zero iden

530+p2 :: (Num e, CountableDims n m, FL m n, FL n n) => Matrix e (Either m n) n

531+p2 = join zeros id

520532

521533-- Injections

522534

523535-- | Biproduct first component injection

524−i1 :: (Num e, KnownNat (Count n), KnownNat (Count m), FromLists e n m, FromLists e m m) => Matrix e m (Either m n)

536+i1 :: (Num e, CountableDims n m, FL n m, FL m m) => Matrix e m (Either m n)

525537i1 = tr p1

526538

527539-- | Biproduct second component injection

528−i2 :: (Num e, KnownNat (Count n), KnownNat (Count m), FromLists e m n, FromLists e n n) => Matrix e n (Either m n)

540+i2 :: (Num e, CountableDims n m, FL m n, FL n n) => Matrix e n (Either m n)

529541i2 = tr p2

530542

531543-- Dimensions

532544

533545-- | Obtain the number of rows.

534546--

535−-- NOTE: The 'KnownNat' constaint is needed in order to obtain the

536−-- dimensions in constant time.

537−--

538−-- TODO: A 'rows' function that does not need the 'KnownNat' constraint in

539−-- exchange for performance.

540−rows :: forall e cols rows. (KnownNat (Count rows)) => Matrix e cols rows -> Int

547+-- NOTE: The 'KnownNat' constraint is needed in order to obtain the

548+-- dimensions in constant time. For a version that doesn't require the

549+-- constraint see 'rows''.

550+rows :: forall e cols rows. (Countable rows) => Matrix e cols rows -> Int

541551rows _ = fromInteger $ natVal (Proxy :: Proxy (Count rows))

542552

553+-- | Obtain the number of rows in an inefficient manner, but without any

554+-- constraints.

555+--

556+-- For a more efficient version see 'rows'.

557+rows' :: Matrix e cols rows -> Int

558+rows' (One _) = 1

559+rows' (Join lhs _) = rows' lhs

560+rows' (Fork top bottom) = rows' top + rows' bottom

561+

543562-- | Obtain the number of columns.

544−--

545−-- NOTE: The 'KnownNat' constaint is needed in order to obtain the

546−-- dimensions in constant time.

547563--

548−-- TODO: A 'columns' function that does not need the 'KnownNat' constraint in

549−-- exchange for performance.

550−columns :: forall e cols rows. (KnownNat (Count cols)) => Matrix e cols rows -> Int

564+-- NOTE: The 'KnownNat' constraint is needed in order to obtain the

565+-- dimensions in constant time. For a version that doesn't require the

566+-- constraint see 'columns''.

567+columns :: forall e cols rows. (Countable cols) => Matrix e cols rows -> Int

551568columns _ = fromInteger $ natVal (Proxy :: Proxy (Count cols))

552569

570+-- | Obtain the number of columns in an inefficient manner, but without any

571+-- constraints.

572+--

573+-- For a more efficient version see 'columns'.

574+columns' :: Matrix e cols rows -> Int

575+columns' (One _) = 1

576+columns' (Join lhs rhs) = columns' lhs + columns' rhs

577+columns' (Fork top _) = columns' top

578+

553579-- Coproduct Bifunctor

554580

555581infixl 5 -|-

@@ -558,157 +584,172 @@ infixl 5 -|-

558584(-|-) ::

559585 forall e n k m j.

560586 ( Num e,

561− KnownNat (Count j),

562− KnownNat (Count k),

563− FromLists e k k,

564− FromLists e j k,

565− FromLists e k j,

566− FromLists e j j

587+ CountableDims j k,

588+ FL k k,

589+ FL j k,

590+ FL k j,

591+ FL j j

567592 ) =>

568593 Matrix e n k ->

569594 Matrix e m j ->

570595 Matrix e (Either n m) (Either k j)

571−(-|-) a b = Junc (i1 . a) (i2 . b)

596+(-|-) a b = Join (i1 . a) (i2 . b)

572597

573598-- Khatri Rao Product and projections

574599

575600-- | Khatri Rao product first component projection matrix.

576−kp1 ::

601+fstM ::

577602 forall e m k .

578603 ( Num e,

579− KnownNat (Count k),

580− FromLists e (FromNat (Count m * Count k)) m,

581− KnownNat (Count m),

582− KnownNat (Count (Normalize (m, k)))

604+ CountableDims k m,

605+ FL (Normalize (m, k)) m,

606+ CountableN (m, k)

583607 ) => Matrix e (Normalize (m, k)) m

584−kp1 = matrixBuilder f

608+fstM = matrixBuilder' f

585609 where

586610 offset = fromInteger (natVal (Proxy :: Proxy (Count k)))

587611 f (x, y)

588612 | y >= (x * offset) && y <= (x * offset + offset - 1) = 1

589− | otherwise = 0

613+ | otherwise = 0

590614

591615-- | Khatri Rao product second component projection matrix.

592−kp2 ::

616+sndM ::

593617 forall e m k .

594618 ( Num e,

595− KnownNat (Count k),

596− FromLists e (FromNat (Count m * Count k)) k,

597− KnownNat (Count m),

598− KnownNat (Count (Normalize (m, k)))

619+ CountableDims k m,

620+ FL (Normalize (m, k)) k,

621+ CountableN (m, k)

599622 ) => Matrix e (Normalize (m, k)) k

600−kp2 = matrixBuilder f

623+sndM = matrixBuilder' f

601624 where

602625 offset = fromInteger (natVal (Proxy :: Proxy (Count k)))

603626 f (x, y)

604627 | x == y || mod (y - x) offset == 0 = 1

605− | otherwise = 0

628+ | otherwise = 0

606629

607630-- | Khatri Rao Matrix product also known as matrix pairing.

608631--

609632-- NOTE: That this is not a true categorical product, see for instance:

610−--

633+--

611634-- @

612−-- | kp1 . khatri a b == a

613−-- khatri a b ==> |

614−-- | kp2 . khatri a b == b

635+-- | fstM . kr a b == a

636+-- kr a b ==> |

637+-- | sndM . kr a b == b

615638-- @

616639--

617640-- __Emphasis__ on the implication symbol.

618−khatri ::

619− forall e cols a b.

641+kr ::

642+ forall e cols a b.

620643 ( Num e,

621− KnownNat (Count a),

622− KnownNat (Count b),

623− KnownNat (Count (Normalize (a, b))),

624− FromLists e (Normalize (a, b)) a,

625− FromLists e (Normalize (a, b)) b

644+ CountableDims a b,

645+ CountableN (a, b),

646+ FL (Normalize (a, b)) a,

647+ FL (Normalize (a, b)) b

626648 ) => Matrix e cols a -> Matrix e cols b -> Matrix e cols (Normalize (a, b))

627−khatri a b =

628− let kp1' = kp1 @e @a @b

629− kp2' = kp2 @e @a @b

630− in (tr kp1') . a * (tr kp2') . b

649+kr a b =

650+ let fstM' = fstM @e @a @b

651+ sndM' = sndM @e @a @b

652+ in (tr fstM' . a) * (tr sndM' . b)

631653

632654-- Product Bifunctor (Kronecker)

633655

634656infixl 4 ><

635657

636658-- | Matrix product functor also known as kronecker product

637−(><) ::

638− forall e m p n q.

659+(><) ::

660+ forall e m p n q.

639661 ( Num e,

640− KnownNat (Count m),

641− KnownNat (Count n),

642− KnownNat (Count p),

643− KnownNat (Count q),

644− KnownNat (Count (Normalize (m, n))),

645− FromLists e (Normalize (m, n)) m,

646− FromLists e (Normalize (m, n)) n,

647− KnownNat (Count (Normalize (p, q))),

648− FromLists e (Normalize (p, q)) p,

649− FromLists e (Normalize (p, q)) q

650− )

662+ CountableDims m n,

663+ CountableDims p q,

664+ CountableDimsN (m, n) (p, q),

665+ FL (Normalize (m, n)) m,

666+ FL (Normalize (m, n)) n,

667+ FL (Normalize (p, q)) p,

668+ FL (Normalize (p, q)) q

669+ )

651670 => Matrix e m p -> Matrix e n q -> Matrix e (Normalize (m, n)) (Normalize (p, q))

652671(><) a b =

653− let kp1' = kp1 @e @m @n

654− kp2' = kp2 @e @m @n

655− in khatri (a . kp1') (b . kp2')

672+ let fstM' = fstM @e @m @n

673+ sndM' = sndM @e @m @n

674+ in kr (a . fstM') (b . sndM')

656675

657−-- Matrix abide Junc Split

676+-- Matrix abide Join Fork

658677

659−-- | Matrix "abiding" followin the 'Junc'-'Split' abide law.

660−--

678+-- | Matrix "abiding" following the 'Join'-'Fork' exchange law.

679+--

661680-- Law:

662681--

663682-- @

664−-- 'Junc' ('Split' a c) ('Split' b d) == 'Split' ('Junc' a b) ('Junc' c d)

683+-- 'Join' ('Fork' a c) ('Fork' b d) == 'Fork' ('Join' a b) ('Join' c d)

665684-- @

666−abideJS :: Matrix e cols rows -> Matrix e cols rows

667−abideJS (Junc (Split a c) (Split b d)) = Split (Junc (abideJS a) (abideJS b)) (Junc (abideJS c) (abideJS d)) -- Junc-Split abide law

668−abideJS Empty = Empty

669−abideJS (One e) = One e

670−abideJS (Junc a b) = Junc (abideJS a) (abideJS b)

671−abideJS (Split a b) = Split (abideJS a) (abideJS b)

685+abideJF :: Matrix e cols rows -> Matrix e cols rows

686+abideJF (Join (Fork a c) (Fork b d)) = Fork (Join (abideJF a) (abideJF b)) (Join (abideJF c) (abideJF d)) -- Join-Fork abide law

687+abideJF (One e) = One e

688+abideJF (Join a b) = Join (abideJF a) (abideJF b)

689+abideJF (Fork a b) = Fork (abideJF a) (abideJF b)

672690

673−-- Matrix abide Split Junc

691+-- Matrix abide Fork Join

674692

675−-- | Matrix "abiding" followin the 'Split'-'Junc' abide law.

676−--

693+-- | Matrix "abiding" followin the 'Fork'-'Join' abide law.

694+--

677695-- @

678−-- 'Split' ('Junc' a b) ('Junc' c d) == 'Junc' ('Split' a c) ('Split' b d)

696+-- 'Fork' ('Join' a b) ('Join' c d) == 'Join' ('Fork' a c) ('Fork' b d)

679697-- @

680−abideSJ :: Matrix e cols rows -> Matrix e cols rows

681−abideSJ (Split (Junc a b) (Junc c d)) = Junc (Split (abideSJ a) (abideSJ c)) (Split (abideSJ b) (abideSJ d)) -- Split-Junc abide law

682−abideSJ Empty = Empty

683−abideSJ (One e) = One e

684−abideSJ (Junc a b) = Junc (abideSJ a) (abideSJ b)

685−abideSJ (Split a b) = Split (abideSJ a) (abideSJ b)

698+abideFJ :: Matrix e cols rows -> Matrix e cols rows

699+abideFJ (Fork (Join a b) (Join c d)) = Join (Fork (abideFJ a) (abideFJ c)) (Fork (abideFJ b) (abideFJ d)) -- Fork-Join abide law

700+abideFJ (One e) = One e

701+abideFJ (Join a b) = Join (abideFJ a) (abideFJ b)

702+abideFJ (Fork a b) = Fork (abideFJ a) (abideFJ b)

686703

687704-- Matrix transposition

688705

689706-- | Matrix transposition.

690707tr :: Matrix e cols rows -> Matrix e rows cols

691−tr Empty = Empty

692−tr (One e) = One e

693−tr (Junc a b) = Split (tr a) (tr b)

694−tr (Split a b) = Junc (tr a) (tr b)

708+tr (One e) = One e

709+tr (Join a b) = Fork (tr a) (tr b)

710+tr (Fork a b) = Join (tr a) (tr b)

695711

696712-- Selective 'select' operator

697713

698714-- | Selective functors 'select' operator equivalent inspired by the

699715-- ArrowMonad solution presented in the paper.

700−select :: (Num e, FromLists e b b, KnownNat (Count b)) => Matrix e cols (Either a b) -> Matrix e a b -> Matrix e cols b

701−select m y = junc y identity . m

716+select :: (Num e, FL b b, Countable b) => Matrix e cols (Either a b) -> Matrix e a b -> Matrix e cols b

717+select (Fork a b) y = y . a + b -- Divide-and-conquer law

718+select (Join (Fork a c) (Fork b d)) y = join (y . a + c) (y . b + d) -- Pattern matching + DnC law

719+select m y = join y id . m

720+

721+branch ::

722+ ( Num e,

723+ CountableDims a b,

724+ CountableDims c (Either b c),

725+ FL c b,

726+ FL a b,

727+ FL a a,

728+ FL b b,

729+ FL c c,

730+ FL b a,

731+ FL b c,

732+ FL (Either b c) b,

733+ FL (Either b c) c

734+ )

735+ => Matrix e cols (Either a b) -> Matrix e a c -> Matrix e b c -> Matrix e cols c

736+branch x l r = f x `select` g l `select` r

737+ where

738+ f :: (Num e, Countable a, CountableDims b c, FL a b, FL c b, FL b b, FL b a, FL a a)

739+ => Matrix e cols (Either a b) -> Matrix e cols (Either a (Either b c))

740+ f m = fork (tr i1) (i1 . tr i2) . m

741+ g :: (Num e, CountableDims b c, FL b c, FL c c) => Matrix e a c -> Matrix e a (Either b c)

742+ g m = i2 . m

702743

703744-- McCarthy's Conditional

704745

705746-- | McCarthy's Conditional expresses probabilistic choice.

706747cond ::

707− ( cols ~ FromNat (Count cols),

708− KnownNat (Count cols),

709− FromLists e () cols,

710− FromLists e cols (),

711− FromLists e cols cols,

748+ ( Trivial cols,

749+ Countable cols,

750+ FL () cols,

751+ FL cols (),

752+ FL cols cols,

712753 Bounded a,

713754 Enum a,

714755 Num e,

@@ -716,14 +757,14 @@ cond ::

716757 )

717758 =>

718759 (a -> Bool) -> Matrix e cols rows -> Matrix e cols rows -> Matrix e cols rows

719−cond p f g = junc f g . grd p

720−

721−grd ::

722− ( q ~ FromNat (Count q),

723− KnownNat (Count q),

724− FromLists e () q,

725− FromLists e q (),

726− FromLists e q q,

760+cond p f g = join f g . grd p

761+

762+grd ::

763+ ( Trivial q,

764+ Countable q,

765+ FL () q,

766+ FL q (),

767+ FL q q,

727768 Bounded a,

728769 Enum a,

729770 Num e,

@@ -731,62 +772,88 @@ grd ::

731772 )

732773 =>

733774 (a -> Bool) -> Matrix e q (Either q q)

734−grd f = split (corr f) (corr (not . f))

735−

736−corr ::

737− forall e a q .

738− ( q ~ FromNat (Count q),

739− KnownNat (Count q),

740− FromLists e () q,

741− FromLists e q (),

742− FromLists e q q,

743− Bounded a,

744− Enum a,

745− Num e,

746− Ord e

747− )

775+grd f = fork (corr f) (corr (not . f))

776+

777+corr ::

778+ forall e a q .

779+ ( Trivial q,

780+ Countable q,

781+ FL () q,

782+ FL q (),

783+ FL q q,

784+ Liftable e a Bool

785+ )

748786 => (a -> Bool) -> Matrix e q q

749−corr p = let f = fromF p :: Matrix e q ()

750− in khatri f (identity :: Matrix e q q)

787+corr p = let f = fromF' p :: Matrix e q ()

788+ in kr f (id :: Matrix e q q)

751789

752790-- Pretty print

753791

754792prettyAux :: Show e => [[e]] -> [[e]] -> String

755793prettyAux [] _ = ""

756−prettyAux [[e]] m = "│ " ++ fill (show e) ++ " │\n"

794+prettyAux [[e]] m = "│ " ++ fill (show e) ++ " │\n"

757795 where

758796 v = fmap show m

759797 widest = maximum $ fmap length v

760798 fill str = replicate (widest - length str - 2) ' ' ++ str

761−prettyAux [h] m = "│ " ++ fill (unwords $ map show h) ++ " │\n"

799+prettyAux [h] m = "│ " ++ fill (unwords $ map show h) ++ " │\n"

762800 where

763− v = fmap show m

764− widest = maximum $ fmap length v

801+ v = fmap show m

802+ widest = maximum $ fmap length v

765803 fill str = replicate (widest - length str - 2) ' ' ++ str

766−prettyAux (h : t) l = "│ " ++ fill (unwords $ map show h) ++ " │\n" ++

804+prettyAux (h : t) l = "│ " ++ fill (unwords $ map show h) ++ " │\n" ++

767805 prettyAux t l

768806 where

769− v = fmap show l

770− widest = maximum $ fmap length v

807+ v = fmap show l

808+ widest = maximum $ fmap length v

771809 fill str = replicate (widest - length str - 2) ' ' ++ str

772810

773811-- | Matrix pretty printer

774−pretty :: (KnownNat (Count cols), Show e) => Matrix e cols rows -> String

775−pretty m = "┌ " ++ unwords (replicate (columns m) blank) ++ " ┐\n" ++

776− prettyAux (toLists m) (toLists m) ++

777− "└ " ++ unwords (replicate (columns m) blank) ++ " ┘"

778− where

779− v = fmap show (toList m)

780− widest = maximum $ fmap length v

812+pretty :: (CountableDims cols rows, Show e) => Matrix e cols rows -> String

813+pretty m = concat

814+ [ "┌ ", unwords (replicate (columns m) blank), " ┐\n"

815+ , unlines

816+ [ "│ " ++ unwords (fmap (\j -> fill $ show $ getElem i j m) [1..columns m]) ++ " │" | i <- [1..rows m] ]

817+ , "└ ", unwords (replicate (columns m) blank), " ┘"

818+ ]

819+ where

820+ strings = map show (toList m)

821+ widest = maximum $ map length strings

781822 fill str = replicate (widest - length str) ' ' ++ str

782− blank = fill ""

823+ blank = fill ""

824+ safeGet i j m

825+ | i > rows m || j > columns m || i < 1 || j < 1 = Nothing

826+ | otherwise = Just $ unsafeGet i j m (toList m)

827+ unsafeGet i j m l = l !! encode (columns m) (i,j)

828+ encode m (i,j) = (i-1)*m + j - 1

829+ getElem i j m =

830+ fromMaybe

831+ (error $

832+ "getElem: Trying to get the "

833+ ++ show (i, j)

834+ ++ " element from a "

835+ ++ show (rows m) ++ "x" ++ show (columns m)

836+ ++ " matrix."

837+ )

838+ (safeGet i j m)

783839

784840-- | Matrix pretty printer

785−prettyPrint :: (KnownNat (Count cols), Show e) => Matrix e cols rows -> IO ()

841+prettyPrint :: (CountableDims cols rows, Show e) => Matrix e cols rows -> IO ()

786842prettyPrint = putStrLn . pretty

787843

844+-- | Zip two matrices with a given binary function

845+zipWithM :: (e -> f -> g) -> Matrix e cols rows -> Matrix f cols rows -> Matrix g cols rows

846+zipWithM f (One a) (One b) = One (f a b)

847+zipWithM f (Join a b) (Join c d) = Join (zipWithM f a c) (zipWithM f b d)

848+zipWithM f (Fork a b) (Fork c d) = Fork (zipWithM f a c) (zipWithM f b d)

849+zipWithM f x@(Fork _ _) y@(Join _ _) = zipWithM f x (abideJF y)

850+zipWithM f x@(Join _ _) y@(Fork _ _) = zipWithM f (abideJF x) y

851+

788852-- Relational operators functions

789853

854+type Boolean = Natural 0 1

855+type Relation a b = Matrix Boolean a b

856+

790857-- | Helper conversion function

791858toBool :: (Num e, Eq e) => e -> Bool

792859toBool n

@@ -799,143 +866,109 @@ fromBool True = nat 1

799866fromBool False = nat 0

800867

801868-- | Relational negation

802−negateM :: Matrix (Natural 0 1) cols rows -> Matrix (Natural 0 1) cols rows

803−negateM Empty = Empty

804−negateM (One (Nat 0)) = One (Nat 1)

805−negateM (One (Nat 1)) = One (Nat 0)

806−negateM (Junc a b) = Junc (negateM a) (negateM b)

807−negateM (Split a b) = Split (negateM a) (negateM b)

869+negateM :: Relation cols rows -> Relation cols rows

870+negateM (One (Nat p)) = One (Nat (negate p))

871+negateM (Join a b) = Join (negateM a) (negateM b)

872+negateM (Fork a b) = Fork (negateM a) (negateM b)

808873

809874-- | Relational addition

810−orM :: Matrix (Natural 0 1) cols rows -> Matrix (Natural 0 1) cols rows -> Matrix (Natural 0 1) cols rows

811−orM Empty Empty = Empty

812−orM (One a) (One b) = One (fromBool (toBool a || toBool b))

813−orM (Junc a b) (Junc c d) = Junc (orM a c) (orM b d)

814−orM (Split a b) (Split c d) = Split (orM a c) (orM b d)

815−orM x@(Split _ _) y@(Junc _ _) = orM x (abideJS y)

816−orM x@(Junc _ _) y@(Split _ _) = orM (abideJS x) y

875+orM :: Relation cols rows -> Relation cols rows -> Relation cols rows

876+orM (One a) (One b) = One (fromBool (toBool a || toBool b))

877+orM (Join a b) (Join c d) = Join (orM a c) (orM b d)

878+orM (Fork a b) (Fork c d) = Fork (orM a c) (orM b d)

879+orM x@(Fork _ _) y@(Join _ _) = orM x (abideJF y)

880+orM x@(Join _ _) y@(Fork _ _) = orM (abideJF x) y

817881

818882-- | Relational multiplication

819−andM :: Matrix (Natural 0 1) cols rows -> Matrix (Natural 0 1) cols rows -> Matrix (Natural 0 1) cols rows

820−andM Empty Empty = Empty

821−andM (One a) (One b) = One (fromBool (toBool a && toBool b))

822−andM (Junc a b) (Junc c d) = Junc (andM a c) (andM b d)

823−andM (Split a b) (Split c d) = Split (andM a c) (andM b d)

824−andM x@(Split _ _) y@(Junc _ _) = andM x (abideJS y)

825−andM x@(Junc _ _) y@(Split _ _) = andM (abideJS x) y

883+andM :: Relation cols rows -> Relation cols rows -> Relation cols rows

884+andM (One a) (One b) = One (fromBool (toBool a && toBool b))

885+andM (Join a b) (Join c d) = Join (andM a c) (andM b d)

886+andM (Fork a b) (Fork c d) = Fork (andM a c) (andM b d)

887+andM x@(Fork _ _) y@(Join _ _) = andM x (abideJF y)

888+andM x@(Join _ _) y@(Fork _ _) = andM (abideJF x) y

826889

827890-- | Relational subtraction

828−subM :: Matrix (Natural 0 1) cols rows -> Matrix (Natural 0 1) cols rows -> Matrix (Natural 0 1) cols rows

829−subM Empty Empty = Empty

830−subM (One a) (One b) = if a - b < nat 0 then One (nat 0) else One (a - b)

831−subM (Junc a b) (Junc c d) = Junc (subM a c) (subM b d)

832−subM (Split a b) (Split c d) = Split (subM a c) (subM b d)

833−subM x@(Split _ _) y@(Junc _ _) = subM x (abideJS y)

834−subM x@(Junc _ _) y@(Split _ _) = subM (abideJS x) y

891+subM :: Relation cols rows -> Relation cols rows -> Relation cols rows

892+subM (One a) (One b) = if a - b < nat 0 then One (nat 0) else One (a - b)

893+subM (Join a b) (Join c d) = Join (subM a c) (subM b d)

894+subM (Fork a b) (Fork c d) = Fork (subM a c) (subM b d)

895+subM x@(Fork _ _) y@(Join _ _) = subM x (abideJF y)

896+subM x@(Join _ _) y@(Fork _ _) = subM (abideJF x) y

835897

836898-- | Matrix relational composition.

837−compRel :: Matrix (Natural 0 1) cr rows -> Matrix (Natural 0 1) cols cr -> Matrix (Natural 0 1) cols rows

838−compRel Empty Empty = Empty

839−compRel (One a) (One b) = One (fromBool (toBool a && toBool b))

840−compRel (Junc a b) (Split c d) = orM (compRel a c) (compRel b d) -- Divide-and-conquer law

841−compRel (Split a b) c = Split (compRel a c) (compRel b c) -- Split fusion law

842−compRel c (Junc a b) = Junc (compRel c a) (compRel c b) -- Junc fusion law

899+compRel :: Relation cr rows -> Relation cols cr -> Relation cols rows

900+compRel (One a) (One b) = One (fromBool (toBool a && toBool b))

901+compRel (Join a b) (Fork c d) = orM (compRel a c) (compRel b d) -- Divide-and-conquer law

902+compRel (Fork a b) c = Fork (compRel a c) (compRel b c) -- Fork fusion law

903+compRel c (Join a b) = Join (compRel c a) (compRel c b) -- Join fusion law

904+

905+-- | Matrix relational right division

906+divR :: Relation b c -> Relation b a -> Relation a c

907+divR (One a) (One b) = One (fromBool (not (toBool b) || toBool a)) -- b implies a

908+divR (Join a b) (Join c d) = andM (divR a c) (divR b d)

909+divR (Fork a b) c = Fork (divR a c) (divR b c)

910+divR c (Fork a b) = Join (divR c a) (divR c b)

911+

912+-- | Matrix relational left division

913+divL :: Relation c b -> Relation a b -> Relation a c

914+divL x y = tr (divR (tr y) (tr x))

915+

916+-- | Matrix relational symmetric division

917+divS :: Relation c a -> Relation b a -> Relation c b

918+divS s r = divL r s `intersection` divR (tr r) (tr s)

919+ where

920+ intersection = andM

843921

844922-- | Lifts functions to relations with arbitrary dimensions.

845923--

846924-- NOTE: Be careful to not ask for a relation bigger than the cardinality of

847925-- types @a@ or @b@ allows.

848−fromFRel ::

926+fromFRel' ::

849927 forall a b cols rows.

850− ( Bounded a,

851− Bounded b,

852− Enum a,

853− Enum b,

854− Eq b,

855− KnownNat (Count cols),

856− KnownNat (Count rows),

857− FromLists (Natural 0 1) rows cols

928+ ( Liftable Boolean a b,

929+ CountableDims cols rows,

930+ FL rows cols

858931 ) =>

859932 (a -> b) ->

860− Matrix (Natural 0 1) cols rows

861−fromFRel f =

862− let minA = minBound @a

863− maxA = maxBound @a

864− minB = minBound @b

865− maxB = maxBound @b

866− ccols = fromInteger $ natVal (Proxy :: Proxy (Count cols))

867− rrows = fromInteger $ natVal (Proxy :: Proxy (Count rows))

868− elementsA = take ccols [minA .. maxA]

869− elementsB = take rrows [minB .. maxB]

870− combinations = (,) <$> elementsA <*> elementsB

871− combAp = map snd . sort . map (\(a, b) -> if f a == b

872− then ((fromEnum a, fromEnum b), nat 1)

873− else ((fromEnum a, fromEnum b), nat 0)) $ combinations

874− mList = buildList combAp rrows

875− in tr $ fromLists mList

876− where

877− buildList [] _ = []

878− buildList l r = take r l : buildList (drop r l) r

933+ Relation cols rows

934+fromFRel' = fromF'

879935

880936-- | Lifts functions to relations with dimensions matching @a@ and @b@

881937-- cardinality's.

882−fromFRel' ::

938+fromFRel ::

883939 forall a b.

884− ( Bounded a,

885− Bounded b,

886− Enum a,

887− Enum b,

888− Eq b,

889− KnownNat (Count (Normalize a)),

890− KnownNat (Count (Normalize b)),

891− FromLists (Natural 0 1) (Normalize b) (Normalize a)

940+ ( Liftable Boolean a b,

941+ CountableDimsN a b,

942+ FLN b a

892943 ) =>

893944 (a -> b) ->

894− Matrix (Natural 0 1) (Normalize a) (Normalize b)

895−fromFRel' f =

896− let minA = minBound @a

897− maxA = maxBound @a

898− minB = minBound @b

899− maxB = maxBound @b

900− ccols = fromInteger $ natVal (Proxy :: Proxy (Count (Normalize a)))

901− rrows = fromInteger $ natVal (Proxy :: Proxy (Count (Normalize b)))

902− elementsA = take ccols [minA .. maxA]

903− elementsB = take rrows [minB .. maxB]

904− combinations = (,) <$> elementsA <*> elementsB

905− combAp = map snd . sort . map (\(a, b) -> if f a == b

906− then ((fromEnum a, fromEnum b), nat 1)

907− else ((fromEnum a, fromEnum b), nat 0)) $ combinations

908− mList = buildList combAp rrows

909− in tr $ fromLists mList

910− where

911− buildList [] _ = []

912− buildList l r = take r l : buildList (drop r l) r

945+ Relation (Normalize a) (Normalize b)

946+fromFRel = fromFRel'

913947

914948-- | Lifts a relation function to a Boolean Matrix

915−toRel ::

949+toRel ::

916950 forall a b.

917951 ( Bounded a,

918952 Bounded b,

919953 Enum a,

920954 Enum b,

921955 Eq b,

922− KnownNat (Count (Normalize a)),

923− KnownNat (Count (Normalize b)),

924− FromLists (Natural 0 1) (Normalize b) (Normalize a)

925− )

926− => (a -> b -> Bool) -> Matrix (Natural 0 1) (Normalize a) (Normalize b)

956+ CountableDims a b,

957+ FLN b a

958+ )

959+ => (a -> b -> Bool) -> Relation (Normalize a) (Normalize b)

927960toRel f =

928961 let minA = minBound @a

929962 maxA = maxBound @a

930963 minB = minBound @b

931964 maxB = maxBound @b

932− ccols = fromInteger $ natVal (Proxy :: Proxy (Count (Normalize a)))

933− rrows = fromInteger $ natVal (Proxy :: Proxy (Count (Normalize b)))

965+ ccols = fromInteger $ natVal (Proxy :: Proxy (Count a))

966+ rrows = fromInteger $ natVal (Proxy :: Proxy (Count b))

934967 elementsA = take ccols [minA .. maxA]

935968 elementsB = take rrows [minB .. maxB]

936969 combinations = (,) <$> elementsA <*> elementsB

937− combAp = map snd . sort . map (\(a, b) -> if uncurry f (a, b)

938− then ((fromEnum a, fromEnum b), nat 1)

970+ combAp = map snd . sort . map (\(a, b) -> if uncurry f (a, b)

971+ then ((fromEnum a, fromEnum b), nat 1)

939972 else ((fromEnum a, fromEnum b), nat 0)) $ combinations

940973 mList = buildList combAp rrows

941974 in tr $ fromLists mList

src/LAoP/Matrix/Nat.hs+194−187

@@ -1,3 +1,4 @@

1+{-# LANGUAGE ConstraintKinds #-}

12{-# LANGUAGE AllowAmbiguousTypes #-}

23{-# LANGUAGE DataKinds #-}

34{-# LANGUAGE DerivingVia #-}

@@ -53,11 +54,22 @@ module LAoP.Matrix.Nat

5354 -- * Type safe matrix representation

5455 Matrix (..),

5556

57+ -- * Constraint type synonyms

58+ Countable,

59+ CountableDims,

60+ CountableN,

61+ CountableNz,

62+ CountableDimsN,

63+ FLN,

64+ FLNz,

65+ Liftable,

66+ TrivialE,

67+ TrivialP,

68+

5669 -- * Primitives

57− empty,

5870 one,

59− junc,

60− split,

71+ join,

72+ fork,

6173

6274 -- * Auxiliary type families

6375 I.FromNat,

@@ -65,11 +77,11 @@ module LAoP.Matrix.Nat

6577 I.Normalize,

6678

6779 -- * Matrix construction and conversion

68− I.FromLists,

80+ I.FL,

6981 fromLists,

7082 toLists,

7183 toList,

72− matrixBuilder,

84+ matrixBuilder',

7385 row,

7486 col,

7587 zeros,

@@ -85,6 +97,10 @@ module LAoP.Matrix.Nat

8597 -- ** Matrix Transposition

8698 tr,

8799

100+ -- ** Scalar multiplication/division of matrices

101+ (.|),

102+ (./),

103+

88104 -- ** Selective operator

89105 select,

90106

@@ -92,16 +108,19 @@ module LAoP.Matrix.Nat

92108 cond,

93109

94110 -- ** Matrix "abiding"

95− abideJS,

96− abideSJ,

111+ abideJF,

112+ abideFJ,

113+

114+ -- ** Zip Matrices

115+ zipWithM,

97116

98117 -- * Biproduct approach

99− -- ** Split

118+ -- ** Fork

100119 (===),

101120 -- *** Projections

102121 p1,

103122 p2,

104− -- ** Junc

123+ -- ** Join

105124 (|||),

106125 -- *** Injections

107126 i1,

@@ -115,11 +134,11 @@ module LAoP.Matrix.Nat

115134 -- | Note that given the restrictions imposed it is not possible to

116135 -- implement the standard type classes present in standard Haskell.

117136 -- *** Matrix pairing projections

118− kp1,

119− kp2,

137+ fstM,

138+ sndM,

120139

121140 -- *** Matrix pairing

122− khatri,

141+ kr,

123142

124143 -- * Matrix composition and lifting

125144

@@ -127,10 +146,10 @@ module LAoP.Matrix.Nat

127146

128147 -- | Note that given the restrictions imposed it is not possible to

129148 -- implement the standard type classes present in standard Haskell.

130− identity,

149+ iden,

131150 comp,

132− fromF,

133151 fromF',

152+ fromF,

134153

135154 -- * Matrix printing

136155 pretty,

@@ -141,107 +160,95 @@ where

141160import Data.Proxy

142161import GHC.TypeLits

143162import Control.DeepSeq

144−import qualified Control.Category as C

145163import qualified LAoP.Matrix.Internal as I

146164

147165newtype Matrix e (cols :: Nat) (rows :: Nat) = M (I.Matrix e (I.FromNat cols) (I.FromNat rows))

148166 deriving (Show, Num, Eq, Ord, NFData) via (I.Matrix e (I.FromNat cols) (I.FromNat rows))

149167

150−-- | It isn't possible to implement the 'id' function so it's

151−-- implementation is 'undefined'. However 'comp' can be and this partial

152−-- class implementation exists just to make the code more readable.

153−--

154−-- Please use 'identity' instead.

155−instance (Num e) => C.Category (Matrix e) where

156− id = undefined

157− (.) = comp

168+-- | Constraint type synonyms to keep the type signatures less convoluted

169+type Countable a = KnownNat (I.Count a)

170+type CountableDims a b = (Countable a, Countable b)

171+type CountableN a = KnownNat (I.Count (I.FromNat a))

172+type CountableNz a = KnownNat (I.Count (I.Normalize a))

173+type CountableDimsN a b = (CountableN a, CountableN b)

174+type FLN e a b = I.FL (I.FromNat a) (I.FromNat b)

175+type FLNz e a b = I.FL (I.Normalize a) (I.Normalize b)

176+type Liftable e a b = (Bounded a, Bounded b, Enum a, Enum b, Eq b, Num e, Ord e)

177+type TrivialE a b = I.FromNat (a + b) ~ Either (I.FromNat a) (I.FromNat b)

178+type TrivialP a b = I.FromNat (a * b) ~ I.FromNat (I.Count (I.FromNat a) * I.Count (I.FromNat b))

158179

159180-- Primitives

160181

161−empty :: Matrix e 0 0

162−empty = M I.Empty

163−

164182one :: e -> Matrix e 1 1

165183one = M . I.One

166184

167−junc ::

168− (I.FromNat cols3 ~ Either (I.FromNat cols1) (I.FromNat cols2)) =>

169− Matrix e cols1 rows ->

170− Matrix e cols2 rows ->

171− Matrix e cols3 rows

172−junc (M a) (M b) = M (I.Junc a b)

185+join ::

186+ (TrivialE a b) =>

187+ Matrix e a rows ->

188+ Matrix e b rows ->

189+ Matrix e (a + b) rows

190+join (M a) (M b) = M (I.Join a b)

173191

174192infixl 3 |||

175193(|||) ::

176− (I.FromNat cols3 ~ Either (I.FromNat cols1) (I.FromNat cols2)) =>

177− Matrix e cols1 rows ->

178− Matrix e cols2 rows ->

179− Matrix e cols3 rows

180−(|||) = junc

181−

182−split ::

183− (I.FromNat rows3 ~ Either (I.FromNat rows1) (I.FromNat rows2)) =>

184− Matrix e cols rows1 ->

185− Matrix e cols rows2 ->

186− Matrix e cols rows3

187−split (M a) (M b) = M (I.Split a b)

194+ (TrivialE a b) =>

195+ Matrix e a rows ->

196+ Matrix e b rows ->

197+ Matrix e (a + b) rows

198+(|||) = join

199+

200+fork ::

201+ (TrivialE a b) =>

202+ Matrix e cols a ->

203+ Matrix e cols b ->

204+ Matrix e cols (a + b)

205+fork (M a) (M b) = M (I.Fork a b)

188206

189207infixl 2 ===

190208(===) ::

191− (I.FromNat rows3 ~ Either (I.FromNat rows1) (I.FromNat rows2)) =>

192− Matrix e cols rows1 ->

193− Matrix e cols rows2 ->

194− Matrix e cols rows3

195−(===) = split

209+ (TrivialE a b) =>

210+ Matrix e cols a ->

211+ Matrix e cols b ->

212+ Matrix e cols (a + b)

213+(===) = fork

196214

197215-- Construction

198216

199−fromLists :: (I.FromLists e (I.FromNat cols) (I.FromNat rows)) => [[e]] -> Matrix e cols rows

217+fromLists :: (FLN e cols rows) => [[e]] -> Matrix e cols rows

200218fromLists = M . I.fromLists

201219

202−matrixBuilder ::

203− (I.FromLists e (I.FromNat cols) (I.FromNat rows), KnownNat (I.Count (I.FromNat cols)), KnownNat (I.Count (I.FromNat rows))) =>

204− ((Int, Int) -> e) ->

205− Matrix e cols rows

206−matrixBuilder = M . I.matrixBuilder

220+-- | Matrix builder function. Constructs a matrix provided with

221+-- a construction function that operates with indices.

222+matrixBuilder' ::

223+ (FLN e cols rows, CountableN cols, CountableN rows)

224+ => ((Int, Int) -> e) -> Matrix e cols rows

225+matrixBuilder' = M . I.matrixBuilder'

207226

208−col :: (I.FromLists e () (I.FromNat rows)) => [e] -> Matrix e 1 rows

227+col :: (I.FL () (I.FromNat rows)) => [e] -> Matrix e 1 rows

209228col = M . I.col

210229

211−row :: (I.FromLists e (I.FromNat cols) ()) => [e] -> Matrix e cols 1

230+row :: (I.FL (I.FromNat cols) ()) => [e] -> Matrix e cols 1

212231row = M . I.row

213232

214−fromF ::

215− ( Bounded a,

216− Bounded b,

217− Enum a,

218− Enum b,

219− Eq b,

220− Num e,

221− Ord e,

222− KnownNat (I.Count (I.FromNat cols)),

223− KnownNat (I.Count (I.FromNat rows)),

224− I.FromLists e (I.FromNat rows) (I.FromNat cols)

233+fromF' ::

234+ ( Liftable e a b,

235+ CountableN cols,

236+ CountableN rows,

237+ FLN e rows cols

225238 ) =>

226239 (a -> b) ->

227240 Matrix e cols rows

228−fromF = M . I.fromF

241+fromF' = M . I.fromF'

229242

230−fromF' ::

231− ( Bounded a,

232− Bounded b,

233− Enum a,

234− Enum b,

235− Eq b,

236− Num e,

237− Ord e,

238− KnownNat (I.Count (I.Normalize a)),

239− KnownNat (I.Count (I.Normalize b)),

240− I.FromLists e (I.Normalize b) (I.Normalize a)

243+fromF ::

244+ ( Liftable e a b,

245+ CountableNz a,

246+ CountableNz b,

247+ FLNz e b a

241248 ) =>

242249 (a -> b) ->

243250 Matrix e (I.Count a) (I.Count b)

244−fromF' = M . I.fromF'

251+fromF = undefined -- M . I.fromF

245252

246253-- Conversion

247254

@@ -254,21 +261,21 @@ toList (M m) = I.toList m

254261-- Zeros Matrix

255262

256263zeros ::

257− (Num e, I.FromLists e (I.FromNat cols) (I.FromNat rows), KnownNat (I.Count (I.FromNat cols)), KnownNat (I.Count (I.FromNat rows))) =>

264+ (Num e, FLN e cols rows, CountableN cols, CountableN rows) =>

258265 Matrix e cols rows

259266zeros = M I.zeros

260267

261268-- Ones Matrix

262269

263270ones ::

264− (Num e, I.FromLists e (I.FromNat cols) (I.FromNat rows), KnownNat (I.Count (I.FromNat cols)), KnownNat (I.Count (I.FromNat rows))) =>

271+ (Num e, FLN e cols rows, CountableN cols, CountableN rows) =>

265272 Matrix e cols rows

266273ones = M I.ones

267274

268275-- Const Matrix

269276

270277constant ::

271− (Num e, I.FromLists e (I.FromNat cols) (I.FromNat rows), KnownNat (I.Count (I.FromNat cols)), KnownNat (I.Count (I.FromNat rows))) =>

278+ (Num e, FLN e cols rows, CountableN cols, CountableN rows) =>

272279 e ->

273280 Matrix e cols rows

274281constant = M . I.constant

@@ -277,40 +284,52 @@ constant = M . I.constant

277284

278285bang ::

279286 forall e cols.

280− (Num e, Enum e, I.FromLists e (I.FromNat cols) (), KnownNat (I.Count (I.FromNat cols))) =>

287+ (Num e, Enum e, I.FL (I.FromNat cols) (), CountableN cols) =>

281288 Matrix e cols 1

282289bang = M I.bang

283290

284−-- Identity Matrix

291+-- iden Matrix

285292

286−identity ::

287− (Num e, I.FromLists e (I.FromNat cols) (I.FromNat cols), KnownNat (I.Count (I.FromNat cols))) =>

293+iden ::

294+ (Num e, FLN e cols cols, CountableN cols) =>

288295 Matrix e cols cols

289−identity = M I.identity

296+iden = M I.iden

290297

291298-- Matrix composition (MMM)

292299

293300comp :: (Num e) => Matrix e cr rows -> Matrix e cols cr -> Matrix e cols rows

294301comp (M a) (M b) = M (I.comp a b)

295302

303+-- Scalar multiplication of matrices

304+

305+infixl 7 .|

306+-- | Scalar multiplication of matrices.

307+(.|) :: Num e => e -> Matrix e cols rows -> Matrix e cols rows

308+(.|) e (M m) = M (e I..| m)

309+

310+-- Scalar division of matrices

311+

312+infixl 7 ./

313+-- | Scalar multiplication of matrices.

314+(./) :: Fractional e => Matrix e cols rows -> e -> Matrix e cols rows

315+(./) (M m) e = M (m I../ e)

316+

296317p1 ::

297318 ( Num e,

298− KnownNat (I.Count (I.FromNat n)),

299− KnownNat (I.Count (I.FromNat m)),

300− I.FromLists e (I.FromNat n) (I.FromNat m),

301− I.FromLists e (I.FromNat m) (I.FromNat m),

302− I.FromNat (m + n) ~ Either (I.FromNat m) (I.FromNat n)

319+ CountableDimsN n m,

320+ FLN e n m,

321+ FLN e m m,

322+ TrivialE m n

303323 ) =>

304324 Matrix e (m + n) m

305325p1 = M I.p1

306326

307327p2 ::

308328 ( Num e,

309− KnownNat (I.Count (I.FromNat n)),

310− KnownNat (I.Count (I.FromNat m)),

311− I.FromLists e (I.FromNat m) (I.FromNat n),

312− I.FromLists e (I.FromNat n) (I.FromNat n),

313− I.FromNat (m + n) ~ Either (I.FromNat m) (I.FromNat n)

329+ CountableDimsN n m,

330+ FLN e m n,

331+ FLN e n n,

332+ TrivialE m n

314333 ) =>

315334 Matrix e (m + n) n

316335p2 = M I.p2

@@ -319,138 +338,125 @@ p2 = M I.p2

319338

320339i1 ::

321340 ( Num e,

322− KnownNat (I.Count (I.FromNat n)),

323− KnownNat (I.Count (I.FromNat rows)),

324− I.FromLists e (I.FromNat n) (I.FromNat rows),

325− I.FromLists e (I.FromNat rows) (I.FromNat rows),

326− I.FromNat (rows + n) ~ Either (I.FromNat rows) (I.FromNat n)

341+ CountableDimsN n rows,

342+ FLN e n rows,

343+ FLN e rows rows,

344+ TrivialE rows n

327345 ) =>

328346 Matrix e rows (rows + n)

329347i1 = tr p1

330348

331349i2 ::

332350 ( Num e,

333− KnownNat (I.Count (I.FromNat rows)),

334− KnownNat (I.Count (I.FromNat m)),

335− I.FromLists e (I.FromNat m) (I.FromNat rows),

336− I.FromLists e (I.FromNat rows) (I.FromNat rows),

337− I.FromNat (m + rows) ~ Either (I.FromNat m) (I.FromNat rows)

351+ CountableDimsN rows m,

352+ FLN e m rows,

353+ FLN e rows rows,

354+ TrivialE m rows

338355 ) =>

339356 Matrix e rows (m + rows)

340357i2 = tr p2

341358

342359-- Dimensions

343360

344−rows :: (KnownNat (I.Count (I.FromNat rows))) => Matrix e cols rows -> Int

361+rows :: (CountableN rows) => Matrix e cols rows -> Int

345362rows (M m) = I.rows m

346363

347−columns :: (KnownNat (I.Count (I.FromNat cols))) => Matrix e cols rows -> Int

364+columns :: (CountableN cols) => Matrix e cols rows -> Int

348365columns (M m) = I.columns m

349366

350−-- Coproduct Bifunctor

351−

352367infixl 5 -|-

353368

369+-- | Coproduct Bifunctor (Direct sum)

354370(-|-) ::

355371 ( Num e,

356− KnownNat (I.Count (I.FromNat j)),

357− KnownNat (I.Count (I.FromNat k)),

358− I.FromLists e (I.FromNat k) (I.FromNat k),

359− I.FromLists e (I.FromNat j) (I.FromNat k),

360− I.FromLists e (I.FromNat k) (I.FromNat j),

361− I.FromLists e (I.FromNat j) (I.FromNat j),

362− I.FromNat (n + m) ~ Either (I.FromNat n) (I.FromNat m),

363− I.FromNat (k + j) ~ Either (I.FromNat k) (I.FromNat j)

372+ CountableDimsN j k,

373+ FLN e k k,

374+ FLN e j k,

375+ FLN e k j,

376+ FLN e j j,

377+ TrivialE n m,

378+ TrivialE k j

364379 ) =>

365380 Matrix e n k ->

366381 Matrix e m j ->

367382 Matrix e (n + m) (k + j)

368383(-|-) (M a) (M b) = M ((I.-|-) a b)

369384

370−-- Khatri Rao Product and projections

371−

372−kp1 ::

385+-- | Khatri Rao Product first projection

386+fstM ::

373387 forall e m k .

374388 ( Num e,

375− KnownNat (I.Count (I.FromNat m)),

376− KnownNat (I.Count (I.FromNat k)),

377− KnownNat (I.Count (I.FromNat (m * k))),

378− I.FromLists e (I.FromNat (m * k)) (I.FromNat m),

379− I.FromNat (m * k) ~ I.FromNat (I.Count (I.FromNat m) * I.Count (I.FromNat k))

389+ CountableDimsN m k,

390+ CountableN (m * k),

391+ FLN e (m * k) m,

392+ TrivialP m k

380393 ) => Matrix e (m * k) m

381−kp1 = M (I.kp1 @e @(I.FromNat m) @(I.FromNat k))

394+fstM = M (I.fstM @e @(I.FromNat m) @(I.FromNat k))

382395

383−kp2 ::

396+-- | Khatri Rao Product second projection

397+sndM ::

384398 forall e m k.

385399 ( Num e,

386− KnownNat (I.Count (I.FromNat k)),

387− I.FromLists e (I.FromNat (m * k)) (I.FromNat k),

388− KnownNat (I.Count (I.FromNat m)),

389− KnownNat (I.Count (I.FromNat (m * k))),

390− I.FromNat (m * k) ~ I.FromNat (I.Count (I.FromNat m) * I.Count (I.FromNat k))

400+ CountableDimsN k m,

401+ FLN e (m * k) k,

402+ CountableN (m * k),

403+ TrivialP m k

391404 ) => Matrix e (m * k) k

392−kp2 = M (I.kp2 @e @(I.FromNat m) @(I.FromNat k))

405+sndM = M (I.sndM @e @(I.FromNat m) @(I.FromNat k))

393406

394−khatri ::

407+-- | Khatri Rao Product

408+kr ::

395409 forall e cols a b.

396410 ( Num e,

397− KnownNat (I.Count (I.FromNat a)),

398− KnownNat (I.Count (I.FromNat b)),

399− KnownNat (I.Count (I.FromNat (a * b))),

400− I.FromLists e (I.FromNat (a * b)) (I.FromNat a),

401− I.FromLists e (I.FromNat (a * b)) (I.FromNat b),

402− I.FromNat (a * b) ~ I.FromNat (I.Count (I.FromNat a) * I.Count (I.FromNat b))

411+ CountableDimsN a b,

412+ CountableN (a * b),

413+ FLN e (a * b) a,

414+ FLN e (a * b) b,

415+ TrivialP a b

403416 ) => Matrix e cols a -> Matrix e cols b -> Matrix e cols (a * b)

404−khatri a b =

405− let kp1' = kp1 @e @a @b

406− kp2' = kp2 @e @a @b

407− in comp (tr kp1') a * comp (tr kp2') b

408−

409−-- Product Bifunctor (Kronecker)

417+kr a b =

418+ let fstM' = fstM @e @a @b

419+ sndM' = sndM @e @a @b

420+ in comp (tr fstM') a * comp (tr sndM') b

410421

422+-- | Product Bifunctor (Kronecker)

411423infixl 4 ><

412424

413425(><) ::

414426 forall e m p n q.

415427 ( Num e,

416− KnownNat (I.Count (I.FromNat m)),

417− KnownNat (I.Count (I.FromNat n)),

418− KnownNat (I.Count (I.FromNat p)),

419− KnownNat (I.Count (I.FromNat q)),

420− KnownNat (I.Count (I.FromNat (m * n))),

421− KnownNat (I.Count (I.FromNat (p * q))),

422− I.FromLists e (I.FromNat (m * n)) (I.FromNat m),

423− I.FromLists e (I.FromNat (m * n)) (I.FromNat n),

424− I.FromLists e (I.FromNat (p * q)) (I.FromNat p),

425− I.FromLists e (I.FromNat (p * q)) (I.FromNat q),

426− I.FromNat (m * n) ~ I.FromNat (I.Count (I.FromNat m) * I.Count (I.FromNat n)),

427− I.FromNat (p * q) ~ I.FromNat (I.Count (I.FromNat p) * I.Count (I.FromNat q))

428+ CountableDimsN m n,

429+ CountableDimsN p q,

430+ CountableDimsN (m * n) (p * q),

431+ FLN e (m * n) m,

432+ FLN e (m * n) n,

433+ FLN e (p * q) p,

434+ FLN e (p * q) q,

435+ TrivialP m n,

436+ TrivialP p q

428437 ) => Matrix e m p -> Matrix e n q -> Matrix e (m * n) (p * q)

429438(><) a b =

430− let kp1' = kp1 @e @m @n

431− kp2' = kp2 @e @m @n

432− in khatri (comp a kp1') (comp b kp2')

433−

434−-- Matrix abide Junc Split

439+ let fstM' = fstM @e @m @n

440+ sndM' = sndM @e @m @n

441+ in kr (comp a fstM') (comp b sndM')

435442

436−abideJS :: Matrix e cols rows -> Matrix e cols rows

437−abideJS (M m) = M (I.abideJS m)

443+-- | Matrix abide Join Fork

444+abideJF :: Matrix e cols rows -> Matrix e cols rows

445+abideJF (M m) = M (I.abideJF m)

438446

439−-- Matrix abide Split Junc

440−

441−abideSJ :: Matrix e cols rows -> Matrix e cols rows

442−abideSJ (M m) = M (I.abideSJ m)

443−

444−-- Matrix transposition

447+-- | Matrix abide Fork Join

448+abideFJ :: Matrix e cols rows -> Matrix e cols rows

449+abideFJ (M m) = M (I.abideFJ m)

445450

451+-- | Matrix transposition

446452tr :: Matrix e cols rows -> Matrix e rows cols

447453tr (M m) = M (I.tr m)

448454

449455-- Selective 'select' operator

450456select ::

451457 ( Num e,

452− I.FromLists e (I.FromNat rows1) (I.FromNat rows1),

453− KnownNat (I.Count (I.FromNat rows1)),

458+ FLN e rows1 rows1,

459+ CountableN rows1,

454460 I.FromNat rows2 ~ I.FromNat rows1,

455461 I.FromNat cols1 ~ I.FromNat cols2,

456462 I.FromNat rows3 ~ Either (I.FromNat cols3) (I.FromNat rows1)

@@ -461,14 +467,11 @@ select (M m) (M y) = M (I.select m y)

461467

462468cond ::

463469 ( I.FromNat (I.Count (I.FromNat cols)) ~ I.FromNat cols,

464− KnownNat (I.Count (I.FromNat cols)),

465− I.FromLists e () (I.FromNat cols),

466− I.FromLists e (I.FromNat cols) (),

467− I.FromLists e (I.FromNat cols) (I.FromNat cols),

468− Bounded a,

469− Enum a,

470− Num e,

471− Ord e

470+ CountableN cols,

471+ I.FL () (I.FromNat cols),

472+ I.FL (I.FromNat cols) (),

473+ FLN e cols cols,

474+ Liftable e a Bool

472475 )

473476 =>

474477 (a -> Bool) -> Matrix e cols rows -> Matrix e cols rows -> Matrix e cols rows

@@ -476,8 +479,12 @@ cond p (M a) (M b) = M (I.cond p a b)

476479

477480-- Pretty print

478481

479−pretty :: (KnownNat (I.Count (I.FromNat cols)), Show e) => Matrix e cols rows -> String

482+pretty :: (CountableDimsN cols rows, Show e) => Matrix e cols rows -> String

480483pretty (M m) = I.pretty m

481484

482−prettyPrint :: (KnownNat (I.Count (I.FromNat cols)), Show e) => Matrix e cols rows -> IO ()

485+prettyPrint :: (CountableDimsN cols rows, Show e) => Matrix e cols rows -> IO ()

483486prettyPrint (M m) = I.prettyPrint m

487+

488+-- | Zip two matrices with a given binary function

489+zipWithM :: (e -> f -> g) -> Matrix e cols rows -> Matrix f cols rows -> Matrix g cols rows

490+zipWithM f (M a) (M b) = M (I.zipWithM f a b)

src/LAoP/Matrix/Type.hs+283−240

@@ -1,10 +1,11 @@

1+{-# LANGUAGE ConstraintKinds #-}

2+{-# LANGUAGE TypeFamilies #-}

13{-# LANGUAGE AllowAmbiguousTypes #-}

24{-# LANGUAGE DataKinds #-}

35{-# LANGUAGE DerivingVia #-}

46{-# LANGUAGE FlexibleContexts #-}

57{-# LANGUAGE FlexibleInstances #-}

68{-# LANGUAGE GADTs #-}

7−{-# LANGUAGE KindSignatures #-}

89{-# LANGUAGE MultiParamTypeClasses #-}

910{-# LANGUAGE NoStarIsType #-}

1011{-# LANGUAGE RankNTypes #-}

@@ -55,15 +56,24 @@ module LAoP.Matrix.Type

5556 -- * Type safe matrix representation

5657 Matrix (..),

5758

59+ -- * Constraint type aliases

60+ Countable,

61+ CountableDims,

62+ CountableN,

63+ CountableDimsN,

64+ FLN,

65+ Liftable,

66+ Trivial,

67+ TrivialP,

68+

5869 -- * Type aliases

5970 Zero,

6071 One,

6172

6273 -- * Primitives

63− empty,

6474 one,

65− junc,

66− split,

75+ join,

76+ fork,

6777

6878 -- * Auxiliary type families

6979 I.FromNat,

@@ -75,24 +85,27 @@ module LAoP.Matrix.Type

7585 fromLists,

7686 toLists,

7787 toList,

88+ matrixBuilder',

7889 matrixBuilder,

7990 row,

8091 col,

8192 zeros,

8293 ones,

8394 bang,

95+ point,

8496 constant,

8597

8698 -- * Functor instance equivalent function

8799 fmapM,

100+ bimapM,

88101

89102 -- * Applicative/Monoidal instance equivalent functions

90103 unitM,

91104 multM,

92105

93106 -- * Selective equivalent instance function

94− selectM,

95−

107+ selectM,

108+

96109 -- * Monad equivalent instance function

97110 returnM,

98111 bindM,

@@ -100,25 +113,34 @@ module LAoP.Matrix.Type

100113 -- * Misc

101114 -- ** Get dimensions

102115 columns,

116+ columns',

103117 rows,

118+ rows',

104119

105120 -- ** Matrix Transposition

106121 tr,

107122

123+ -- ** Scalar multiplication/division of matrices

124+ (.|),

125+ (./),

126+

108127 -- ** McCarthy's Conditional

109128 cond,

110129

111130 -- ** Matrix "abiding"

112− abideJS,

113− abideSJ,

131+ abideJF,

132+ abideFJ,

133+

134+ -- ** Zip Matrices

135+ zipWithM,

114136

115137 -- * Biproduct approach

116− -- ** Split

138+ -- ** Fork

117139 (===),

118140 -- *** Projections

119141 p1,

120142 p2,

121− -- ** Junc

143+ -- ** Join

122144 (|||),

123145 -- *** Injections

124146 i1,

@@ -132,11 +154,11 @@ module LAoP.Matrix.Type

132154 -- | Note that given the restrictions imposed it is not possible to

133155 -- implement the standard type classes present in standard Haskell.

134156 -- *** Matrix pairing projections

135− kp1,

136− kp2,

157+ fstM,

158+ sndM,

137159

138160 -- *** Matrix pairing

139− khatri,

161+ kr,

140162

141163 -- * Matrix composition and lifting

142164

@@ -144,10 +166,10 @@ module LAoP.Matrix.Type

144166

145167 -- | Note that given the restrictions imposed it is not possible to

146168 -- implement the standard type classes present in standard Haskell.

147− identity,

169+ iden,

148170 comp,

149− fromF,

150171 fromF',

172+ fromF,

151173

152174 -- * Relation

153175 toRel,

@@ -161,23 +183,44 @@ where

161183import Data.Void

162184import Data.Proxy

163185import Data.Kind

164−import GHC.TypeLits

186+import GHC.TypeLits

165187import Control.DeepSeq

166188import LAoP.Utils

167−import qualified Control.Category as C

168189import qualified LAoP.Matrix.Internal as I

190+import Prelude hiding (id, (.))

169191

170192newtype Matrix e (cols :: Type) (rows :: Type) = M (I.Matrix e (I.Normalize cols) (I.Normalize rows))

171193 deriving (Show, Num, Eq, Ord, NFData) via (I.Matrix e (I.Normalize cols) (I.Normalize rows))

172194

173−-- | It isn't possible to implement the 'id' function so it's

174−-- implementation is 'undefined'. However 'comp' can be and this partial

175−-- class implementation exists just to make the code more readable.

176−--

177−-- Please use 'identity' instead.

178−instance (Num e) => C.Category (Matrix e) where

179− id = undefined

180− (.) = comp

195+-- | Constraint type synonyms to keep the type signatures less convoluted

196+type Countable a = KnownNat (I.Count a)

197+type CountableDims a b = (Countable a, Countable b)

198+type CountableN a = KnownNat (I.Count (I.Normalize a))

199+type CountableDimsN a b = (CountableN a, CountableN b)

200+type FLN a b = I.FromLists (I.Normalize a) (I.Normalize b)

201+type Liftable e a b = (Bounded a, Bounded b, Enum a, Enum b, Eq b, Num e, Ord e)

202+type Trivial a = I.Normalize (I.Normalize a) ~ I.Normalize (I.Normalize (I.Normalize a))

203+type Trivial2 a = I.Normalize a ~ I.Normalize (I.Normalize a)

204+type Trivial3 a = I.FromNat (I.Count (I.Normalize (I.Normalize a))) ~ I.Normalize (I.Normalize a)

205+type TrivialP a b = I.Normalize (a, b) ~ I.Normalize (I.Normalize a, I.Normalize b)

206+

207+-- | It is possible to implement a constrained version of the category type

208+-- class.

209+instance (Num e) => Category (Matrix e) where

210+ type Object (Matrix e) a = (FLN a a, CountableN a)

211+ id = iden

212+ (.) = comp

213+

214+-- | Bifunctor equivalent function

215+bimapM ::

216+ ( Liftable e a b,

217+ Liftable e c d,

218+ CountableDimsN a c,

219+ CountableDimsN b d,

220+ FLN d c,

221+ FLN b a

222+ ) => (a -> b) -> (c -> d) -> Matrix e a c -> Matrix e b d

223+bimapM f g m = fromF g . m . tr (fromF f)

181224

182225-- | Zero type alias

183226type Zero = Void

@@ -187,92 +230,75 @@ type One = ()

187230

188231-- Primitives

189232

190−-- | Empty matrix constructor

191−empty :: Matrix e Zero Zero

192−empty = M I.Empty

193−

194233-- | Unit matrix constructor

195234one :: e -> Matrix e One One

196235one = M . I.One

197236

198−-- | Matrix 'Junc' constructor

199−junc ::

200− (I.Normalize (Either a b) ~ Either (I.Normalize a) (I.Normalize b)) =>

237+-- | Matrix 'Join' constructor

238+join ::

201239 Matrix e a rows ->

202240 Matrix e b rows ->

203241 Matrix e (Either a b) rows

204−junc (M a) (M b) = M (I.Junc a b)

242+join (M a) (M b) = M (I.Join a b)

205243

206244infixl 3 |||

207−-- | Matrix 'Junc' constructor

245+-- | Matrix 'Join' constructor

208246(|||) ::

209− (I.Normalize (Either a b) ~ Either (I.Normalize a) (I.Normalize b)) =>

210247 Matrix e a rows ->

211248 Matrix e b rows ->

212249 Matrix e (Either a b) rows

213−(|||) = junc

250+(|||) = join

214251

215−-- | Matrix 'Split' constructor

216−split ::

217− (I.Normalize (Either a b) ~ Either (I.Normalize a) (I.Normalize b)) =>

252+-- | Matrix 'Fork' constructor

253+fork ::

218254 Matrix e cols a ->

219255 Matrix e cols b ->

220256 Matrix e cols (Either a b)

221−split (M a) (M b) = M (I.Split a b)

257+fork (M a) (M b) = M (I.Fork a b)

222258

223259infixl 2 ===

224−-- | Matrix 'Split' constructor

260+-- | Matrix 'Fork' constructor

225261(===) ::

226− (I.Normalize (Either a b) ~ Either (I.Normalize a) (I.Normalize b)) =>

227262 Matrix e cols a ->

228263 Matrix e cols b ->

229264 Matrix e cols (Either a b)

230−(===) = split

265+(===) = fork

231266

232267-- Functor hierarchy

233268

234269-- | Functor instance equivalent function

235−fmapM ::

236− ( Bounded a,

237− Bounded b,

238− Enum a,

239− Enum b,

240− Eq b,

241− Num e,

242− Ord e,

243− KnownNat (I.Count (I.Normalize a)),

244− KnownNat (I.Count (I.Normalize b)),

245− I.FromLists e (I.Normalize b) (I.Normalize a)

270+fmapM ::

271+ ( Liftable e a b,

272+ CountableDimsN a b,

273+ FLN b a

246274 )

247275 =>

248276 (a -> b) -> Matrix e c a -> Matrix e c b

249−fmapM f m = fromF' f `comp` m

277+fmapM f m = fromF f . m

250278

251279-- | Applicative instance equivalent 'unit' function,

252280unitM :: (Num e) => Matrix e () ()

253281unitM = one 1

254282

255283-- | Applicative instance equivalent 'unit' function,

256−multM ::

257− ( KnownNat (I.Count (I.Normalize a)),

258− KnownNat (I.Count (I.Normalize b)),

259− KnownNat (I.Count (I.Normalize (a, b))),

284+multM ::

285+ ( CountableDimsN a b,

286+ CountableN (a, b),

260287 Num e,

261− I.FromLists e (I.Normalize (a, b)) (I.Normalize a),

262− I.FromLists e (I.Normalize (a, b)) (I.Normalize b),

263− I.Normalize (a, b) ~ I.Normalize (I.Normalize a, I.Normalize b)

288+ FLN (a, b) a,

289+ FLN (a, b) b,

290+ TrivialP a b

264291 ) => Matrix e c a -> Matrix e c b -> Matrix e c (a, b)

265−multM a b = khatri a b

266−

292+multM = kr

267293

268294-- | Monad instance equivalent 'return' function,

269−returnM ::

270− forall e a .

271− ( Num e,

272− Enum e,

273− Enum a,

274− I.FromLists e () (I.Normalize a),

275− KnownNat (I.Count a)

295+returnM ::

296+ forall e a .

297+ ( Num e,

298+ Enum e,

299+ Enum a,

300+ FLN () a,

301+ Countable a

276302 ) => a -> Matrix e One a

277303returnM a = col l

278304 where

@@ -288,73 +314,64 @@ bindM = flip comp

288314

289315-- | Build a matrix out of a list of list of elements. Throws a runtime

290316-- error if the dimensions do not match.

291−fromLists :: (I.FromLists e (I.Normalize cols) (I.Normalize rows)) => [[e]] -> Matrix e cols rows

317+fromLists :: (FLN cols rows) => [[e]] -> Matrix e cols rows

292318fromLists = M . I.fromLists

293319

294320-- | Matrix builder function. Constructs a matrix provided with

295−-- a construction function.

321+-- a construction function that operates with indices.

322+matrixBuilder' ::

323+ (FLN cols rows, CountableDimsN cols rows )

324+ => ((Int, Int) -> e) -> Matrix e cols rows

325+matrixBuilder' = M . I.matrixBuilder'

326+

327+-- | Matrix builder function. Constructs a matrix provided with

328+-- a construction function that operates with arbitrary types.

296329matrixBuilder ::

297− (I.FromLists e (I.Normalize cols) (I.Normalize rows), KnownNat (I.Count (I.Normalize cols)), KnownNat (I.Count (I.Normalize rows))) =>

298− ((Int, Int) -> e) ->

299− Matrix e cols rows

300−matrixBuilder = M . I.matrixBuilder

330+ ( FLN a b,

331+ Enum a,

332+ Enum b,

333+ Bounded a,

334+ Bounded b,

335+ Eq a,

336+ Countable b

337+ ) => ((a, b) -> e) -> Matrix e a b

338+matrixBuilder f = M (I.matrixBuilder f)

301339

302340-- | Constructs a column vector matrix

303−col :: (I.FromLists e () (I.Normalize rows)) => [e] -> Matrix e One rows

341+col :: (FLN () rows) => [e] -> Matrix e One rows

304342col = M . I.col

305343

306344-- | Constructs a row vector matrix

307−row :: (I.FromLists e (I.Normalize cols) ()) => [e] -> Matrix e cols One

345+row :: (FLN cols ()) => [e] -> Matrix e cols One

308346row = M . I.row

309347

310348-- | Lifts functions to matrices with arbitrary dimensions.

311349--

312350-- NOTE: Be careful to not ask for a matrix bigger than the cardinality of

313351-- types @a@ or @b@ allows.

314−fromF ::

315− ( Bounded a,

316− Bounded b,

317− Enum a,

318− Enum b,

319− Eq b,

320− Num e,

321− Ord e,

322− KnownNat (I.Count (I.Normalize cols)),

323− KnownNat (I.Count (I.Normalize rows)),

324− I.FromLists e (I.Normalize rows) (I.Normalize cols)

352+fromF' ::

353+ ( Liftable e a b,

354+ CountableDimsN cols rows,

355+ FLN rows cols

325356 ) =>

326− (a -> b) ->

327− Matrix e cols rows

328−fromF = M . I.fromF

357+ (a -> b) -> Matrix e cols rows

358+fromF' = M . I.fromF'

329359

330360-- | Lifts functions to matrices with dimensions matching @a@ and @b@

331361-- cardinality's.

332−fromF' ::

333− ( Bounded a,

334− Bounded b,

335− Enum a,

336− Enum b,

337− Eq b,

338− Num e,

339− Ord e,

340− KnownNat (I.Count (I.Normalize a)),

341− KnownNat (I.Count (I.Normalize b)),

342− I.FromLists e (I.Normalize b) (I.Normalize a)

362+fromF ::

363+ ( Liftable e a b,

364+ CountableDimsN a b,

365+ FLN b a

343366 ) =>

344− (a -> b) ->

345− Matrix e a b

346−fromF' = M . I.fromF'

367+ (a -> b) -> Matrix e a b

368+fromF = M . I.fromF

347369

348370-- | Lifts relation functions to Boolean Matrix

349371toRel ::

350− ( Bounded a,

351− Bounded b,

352− Enum a,

353− Enum b,

354− Eq b,

355− KnownNat (I.Count (I.Normalize a)),

356− KnownNat (I.Count (I.Normalize b)),

357− I.FromLists (Natural 0 1) (I.Normalize b) (I.Normalize a)

372+ ( Liftable (Natural 0 1) a b,

373+ CountableDims a b,

374+ FLN b a

358375 ) => (a -> b -> Bool) -> Matrix (Natural 0 1) a b

359376toRel = M . I.toRel

360377

@@ -372,8 +389,8 @@ toList (M m) = I.toList m

372389

373390-- | The zero matrix. A matrix wholly filled with zeros.

374391zeros ::

375− (Num e, I.FromLists e (I.Normalize cols) (I.Normalize rows), KnownNat (I.Count (I.Normalize cols)), KnownNat (I.Count (I.Normalize rows))) =>

376− Matrix e cols rows

392+ (Num e, FLN cols rows, CountableDimsN cols rows)

393+ => Matrix e cols rows

377394zeros = M I.zeros

378395

379396-- Ones Matrix

@@ -382,8 +399,8 @@ zeros = M I.zeros

382399--

383400-- Also known as T (Top) matrix.

384401ones ::

385− (Num e, I.FromLists e (I.Normalize cols) (I.Normalize rows), KnownNat (I.Count (I.Normalize cols)), KnownNat (I.Count (I.Normalize rows))) =>

386− Matrix e cols rows

402+ (Num e, FLN cols rows, CountableDimsN cols rows)

403+ => Matrix e cols rows

387404ones = M I.ones

388405

389406-- Const Matrix

@@ -391,9 +408,8 @@ ones = M I.ones

391408-- | The constant matrix constructor. A matrix wholly filled with a given

392409-- value.

393410constant ::

394− (Num e, I.FromLists e (I.Normalize cols) (I.Normalize rows), KnownNat (I.Count (I.Normalize cols)), KnownNat (I.Count (I.Normalize rows))) =>

395− e ->

396− Matrix e cols rows

411+ (Num e, FLN cols rows, CountableDimsN cols rows)

412+ => e -> Matrix e cols rows

397413constant = M . I.constant

398414

399415-- Bang Matrix

@@ -401,17 +417,30 @@ constant = M . I.constant

401417-- | The T (Top) row vector matrix.

402418bang ::

403419 forall e cols.

404− (Num e, Enum e, I.FromLists e (I.Normalize cols) (), KnownNat (I.Count (I.Normalize cols))) =>

420+ (Num e, Enum e, FLN cols (), CountableN cols) =>

405421 Matrix e cols One

406422bang = M I.bang

407423

408−-- Identity Matrix

424+-- | Point constant relation

425+point ::

426+ ( Bounded a,

427+ Enum a,

428+ Eq a,

429+ Num e,

430+ Ord e,

431+ CountableN a,

432+ FLN a One

433+ ) => a -> Matrix e One a

434+point = fromF . const

435+

436+-- iden Matrix

409437

410−-- | Identity matrix

411−identity ::

412− (Num e, I.FromLists e (I.Normalize a) (I.Normalize a), KnownNat (I.Count (I.Normalize a))) =>

438+-- | iden matrix

439+iden ::

440+ (Num e, FLN a a, CountableN a) =>

413441 Matrix e a a

414−identity = M I.identity

442+iden = M I.iden

443+{-# NOINLINE iden #-}

415444

416445-- Matrix composition (MMM)

417446

@@ -421,15 +450,32 @@ identity = M I.identity

421450-- from LAoP.

422451comp :: (Num e) => Matrix e cr rows -> Matrix e cols cr -> Matrix e cols rows

423452comp (M a) (M b) = M (I.comp a b)

453+{-# NOINLINE comp #-}

454+{-# RULES

455+ "comp/iden1" forall m. comp m iden = m ;

456+ "comp/iden2" forall m. comp iden m = m

457+#-}

458+

459+-- Scalar multiplication of matrices

460+

461+infixl 7 .|

462+-- | Scalar multiplication of matrices.

463+(.|) :: Num e => e -> Matrix e cols rows -> Matrix e cols rows

464+(.|) e (M m) = M (e I..| m)

465+

466+-- Scalar division of matrices

467+

468+infixl 7 ./

469+-- | Scalar multiplication of matrices.

470+(./) :: Fractional e => Matrix e cols rows -> e -> Matrix e cols rows

471+(./) (M m) e = M (m I../ e)

424472

425473-- | Biproduct first component projection

426474p1 ::

427475 ( Num e,

428− KnownNat (I.Count (I.Normalize n)),

429− KnownNat (I.Count (I.Normalize m)),

430− I.FromLists e (I.Normalize n) (I.Normalize m),

431− I.FromLists e (I.Normalize m) (I.Normalize m),

432− I.Normalize (Either m n) ~ Either (I.Normalize m) (I.Normalize n)

476+ CountableDimsN n m,

477+ FLN n m,

478+ FLN m m

433479 ) =>

434480 Matrix e (Either m n) m

435481p1 = M I.p1

@@ -437,11 +483,9 @@ p1 = M I.p1

437483-- | Biproduct second component projection

438484p2 ::

439485 ( Num e,

440− KnownNat (I.Count (I.Normalize n)),

441− KnownNat (I.Count (I.Normalize m)),

442− I.FromLists e (I.Normalize m) (I.Normalize n),

443− I.FromLists e (I.Normalize n) (I.Normalize n),

444− I.Normalize (Either m n) ~ Either (I.Normalize m) (I.Normalize n)

486+ CountableDimsN n m,

487+ FLN m n,

488+ FLN n n

445489 ) =>

446490 Matrix e (Either m n) n

447491p2 = M I.p2

@@ -451,11 +495,9 @@ p2 = M I.p2

451495-- | Biproduct first component injection

452496i1 ::

453497 ( Num e,

454− KnownNat (I.Count (I.Normalize n)),

455− KnownNat (I.Count (I.Normalize m)),

456− I.FromLists e (I.Normalize n) (I.Normalize m),

457− I.FromLists e (I.Normalize m) (I.Normalize m),

458− I.Normalize (Either m n) ~ Either (I.Normalize m) (I.Normalize n)

498+ CountableDimsN n m,

499+ FLN n m,

500+ FLN m m

459501 ) =>

460502 Matrix e m (Either m n)

461503i1 = tr p1

@@ -463,11 +505,9 @@ i1 = tr p1

463505-- | Biproduct second component injection

464506i2 ::

465507 ( Num e,

466− KnownNat (I.Count (I.Normalize n)),

467− KnownNat (I.Count (I.Normalize m)),

468− I.FromLists e (I.Normalize m) (I.Normalize n),

469− I.FromLists e (I.Normalize n) (I.Normalize n),

470− I.Normalize (Either m n) ~ Either (I.Normalize m) (I.Normalize n)

508+ CountableDimsN n m,

509+ FLN m n,

510+ FLN n n

471511 ) =>

472512 Matrix e n (Either m n)

473513i2 = tr p2

@@ -476,24 +516,34 @@ i2 = tr p2

476516

477517-- | Obtain the number of rows.

478518--

479−-- NOTE: The 'KnownNat' constaint is needed in order to obtain the

480−-- dimensions in constant time.

481−--

482−-- TODO: A 'rows' function that does not need the 'KnownNat' constraint in

483−-- exchange for performance.

484−rows :: (KnownNat (I.Count (I.Normalize rows))) => Matrix e cols rows -> Int

519+-- NOTE: The 'KnownNat' constraint is needed in order to obtain the

520+-- dimensions in constant time. For a version that doesn't require the

521+-- constraint see 'rows''.

522+rows :: (CountableN rows) => Matrix e cols rows -> Int

485523rows (M m) = I.rows m

486524

525+-- | Obtain the number of rows in an inefficient manner, but without any

526+-- constraints.

527+--

528+-- For a more efficient version see 'rows'.

529+rows' :: Matrix e cols rows -> Int

530+rows' (M m) = I.rows' m

531+

487532-- | Obtain the number of columns.

488−--

489−-- NOTE: The 'KnownNat' constaint is needed in order to obtain the

490−-- dimensions in constant time.

491533--

492−-- TODO: A 'columns' function that does not need the 'KnownNat' constraint in

493−-- exchange for performance.

494−columns :: (KnownNat (I.Count (I.Normalize cols))) => Matrix e cols rows -> Int

534+-- NOTE: The 'KnownNat' constraint is needed in order to obtain the

535+-- dimensions in constant time. For a version that doesn't require the

536+-- constraint see 'columns''.

537+columns :: (CountableN cols) => Matrix e cols rows -> Int

495538columns (M m) = I.columns m

496539

540+-- | Obtain the number of columns in an inefficient manner, but without any

541+-- constraints.

542+--

543+-- For a more efficient version see 'columns'.

544+columns' :: Matrix e cols rows -> Int

545+columns' (M m) = I.columns' m

546+

497547-- Coproduct Bifunctor

498548

499549infixl 5 -|-

@@ -501,14 +551,11 @@ infixl 5 -|-

501551-- | Matrix coproduct functor also known as matrix direct sum.

502552(-|-) ::

503553 ( Num e,

504− KnownNat (I.Count (I.Normalize j)),

505− KnownNat (I.Count (I.Normalize k)),

506− I.FromLists e (I.Normalize k) (I.Normalize k),

507− I.FromLists e (I.Normalize j) (I.Normalize k),

508− I.FromLists e (I.Normalize k) (I.Normalize j),

509− I.FromLists e (I.Normalize j) (I.Normalize j),

510− I.Normalize (Either n m) ~ Either (I.Normalize n) (I.Normalize m),

511− I.Normalize (Either k j) ~ Either (I.Normalize k) (I.Normalize j)

554+ CountableDimsN j k,

555+ FLN k k,

556+ FLN j k,

557+ FLN k j,

558+ FLN j j

512559 ) =>

513560 Matrix e n k ->

514561 Matrix e m j ->

@@ -518,104 +565,98 @@ infixl 5 -|-

518565-- Khatri Rao Product and projections

519566

520567-- | Khatri Rao product first component projection matrix.

521−kp1 ::

568+fstM ::

522569 forall e m k .

523570 ( Num e,

524− KnownNat (I.Count (I.Normalize m)),

525− KnownNat (I.Count (I.Normalize k)),

526− KnownNat (I.Count (I.Normalize (m, k))),

527− I.FromLists e (I.Normalize (m, k)) (I.Normalize m),

528− I.Normalize (m, k) ~ I.Normalize (I.Normalize m, I.Normalize k)

571+ CountableDimsN m k,

572+ CountableN (m, k),

573+ FLN (m, k) m,

574+ TrivialP m k

529575 ) => Matrix e (m, k) m

530−kp1 = M (I.kp1 @e @(I.Normalize m) @(I.Normalize k))

576+fstM = M (I.fstM @e @(I.Normalize m) @(I.Normalize k))

531577

532578-- | Khatri Rao product second component projection matrix.

533−kp2 ::

579+sndM ::

534580 forall e m k.

535581 ( Num e,

536− KnownNat (I.Count (I.Normalize k)),

537− KnownNat (I.Count (I.Normalize m)),

538− KnownNat (I.Count (I.Normalize (m, k))),

539− I.FromLists e (I.Normalize (m, k)) (I.Normalize k),

540− I.Normalize (m, k) ~ I.Normalize (I.Normalize m, I.Normalize k)

582+ CountableDimsN k m,

583+ CountableN (m, k),

584+ FLN (m, k) k,

585+ TrivialP m k

541586 ) => Matrix e (m, k) k

542−kp2 = M (I.kp2 @e @(I.Normalize m) @(I.Normalize k))

587+sndM = M (I.sndM @e @(I.Normalize m) @(I.Normalize k))

543588

544589-- | Khatri Rao Matrix product also known as matrix pairing.

545590--

546591-- NOTE: That this is not a true categorical product, see for instance:

547−--

592+--

548593-- @

549−-- | kp1 `comp` khatri a b == a

550−-- khatri a b ==> |

551−-- | kp2 `comp` khatri a b == b

594+-- | fstM . kr a b == a

595+-- kr a b ==> |

596+-- | sndM . kr a b == b

552597-- @

553598--

554599-- __Emphasis__ on the implication symbol.

555−khatri ::

600+kr ::

556601 forall e cols a b.

557602 ( Num e,

558− KnownNat (I.Count (I.Normalize a)),

559− KnownNat (I.Count (I.Normalize b)),

560− KnownNat (I.Count (I.Normalize (a, b))),

561− I.FromLists e (I.Normalize (a, b)) (I.Normalize a),

562− I.FromLists e (I.Normalize (a, b)) (I.Normalize b),

563− I.Normalize (a, b) ~ I.Normalize (I.Normalize a, I.Normalize b)

603+ CountableDimsN a b,

604+ CountableN (a, b),

605+ FLN (a, b) a,

606+ FLN (a, b) b,

607+ TrivialP a b

564608 ) => Matrix e cols a -> Matrix e cols b -> Matrix e cols (a, b)

565−khatri a b =

566− let kp1' = kp1 @e @a @b

567− kp2' = kp2 @e @a @b

568− in comp (tr kp1') a * comp (tr kp2') b

609+kr a b =

610+ let fstM' = fstM @e @a @b

611+ sndM' = sndM @e @a @b

612+ in comp (tr fstM') a * comp (tr sndM') b

569613

570614-- Product Bifunctor (Kronecker)

571615

572616infixl 4 ><

573617

574−-- | Matrix product functor also known as kronecker product

618+-- | Matrix product functor also known as Kronecker product

575619(><) ::

576620 forall e m p n q.

577621 ( Num e,

578− KnownNat (I.Count (I.Normalize m)),

579− KnownNat (I.Count (I.Normalize n)),

580− KnownNat (I.Count (I.Normalize p)),

581− KnownNat (I.Count (I.Normalize q)),

582− KnownNat (I.Count (I.Normalize (m, n))),

583− KnownNat (I.Count (I.Normalize (p, q))),

584− I.FromLists e (I.Normalize (m, n)) (I.Normalize m),

585− I.FromLists e (I.Normalize (m, n)) (I.Normalize n),

586− I.FromLists e (I.Normalize (p, q)) (I.Normalize p),

587− I.FromLists e (I.Normalize (p, q)) (I.Normalize q),

588− I.Normalize (m, n) ~ I.Normalize (I.Normalize m, I.Normalize n),

589− I.Normalize (p, q) ~ I.Normalize (I.Normalize p, I.Normalize q)

622+ CountableDimsN m n,

623+ CountableDimsN p q,

624+ CountableDimsN (m, n) (p, q),

625+ FLN (m, n) m,

626+ FLN (m, n) n,

627+ FLN (p, q) p,

628+ FLN (p, q) q,

629+ TrivialP m n,

630+ TrivialP p q

590631 ) => Matrix e m p -> Matrix e n q -> Matrix e (m, n) (p, q)

591632(><) a b =

592− let kp1' = kp1 @e @m @n

593− kp2' = kp2 @e @m @n

594− in khatri (comp a kp1') (comp b kp2')

633+ let fstM' = fstM @e @m @n

634+ sndM' = sndM @e @m @n

635+ in kr (comp a fstM') (comp b sndM')

595636

596−-- Matrix abide Junc Split

637+-- Matrix abide Join Fork

597638

598−-- | Matrix "abiding" followin the 'Junc'-'Split' abide law.

599−--

639+-- | Matrix "abiding" followin the 'Join'-'Fork' abide law.

640+--

600641-- Law:

601642--

602643-- @

603−-- 'Junc' ('Split' a c) ('Split' b d) == 'Split' ('Junc' a b) ('Junc' c d)

644+-- 'Join' ('Fork' a c) ('Fork' b d) == 'Fork' ('Join' a b) ('Join' c d)

604645-- @

605−abideJS :: Matrix e cols rows -> Matrix e cols rows

606−abideJS (M m) = M (I.abideJS m)

646+abideJF :: Matrix e cols rows -> Matrix e cols rows

647+abideJF (M m) = M (I.abideJF m)

607648

608−-- Matrix abide Split Junc

649+-- Matrix abide Fork Join

609650

610−-- | Matrix "abiding" followin the 'Split'-'Junc' abide law.

611−--

651+-- | Matrix "abiding" followin the 'Fork'-'Join' abide law.

652+--

612653-- Law:

613654--

614655-- @

615−-- 'Split' ('Junc' a b) ('Junc' c d) == 'Junc' ('Split' a c) ('Split' b d)

656+-- 'Fork' ('Join' a b) ('Join' c d) == 'Join' ('Fork' a c) ('Fork' b d)

616657-- @

617−abideSJ :: Matrix e cols rows -> Matrix e cols rows

618−abideSJ (M m) = M (I.abideSJ m)

658+abideFJ :: Matrix e cols rows -> Matrix e cols rows

659+abideFJ (M m) = M (I.abideFJ m)

619660

620661-- Matrix transposition

621662

@@ -627,11 +668,10 @@ tr (M m) = M (I.tr m)

627668

628669-- | Selective functors 'select' operator equivalent inspired by the

629670-- ArrowMonad solution presented in the paper.

630−selectM ::

671+selectM ::

631672 ( Num e,

632− I.FromLists e (I.Normalize b) (I.Normalize b),

633− KnownNat (I.Count (I.Normalize b)),

634− I.Normalize (Either a b) ~ Either (I.Normalize a) (I.Normalize b)

673+ FLN b b,

674+ CountableN b

635675 ) => Matrix e cols (Either a b) -> Matrix e a b -> Matrix e cols b

636676selectM (M m) (M y) = M (I.select m y)

637677

@@ -639,15 +679,14 @@ selectM (M m) (M y) = M (I.select m y)

639679

640680-- | McCarthy's Conditional expresses probabilistic choice.

641681cond ::

642− ( I.Normalize (I.Normalize a) ~ I.Normalize a,

643− KnownNat (I.Count (I.Normalize a)),

644− I.FromLists e () (I.Normalize a),

645− I.FromLists e (I.Normalize a) (),

646− I.FromLists e (I.Normalize a) (I.Normalize a),

647− Bounded a,

648− Enum a,

649− Num e,

650− Ord e

682+ ( Trivial a,

683+ Trivial2 a,

684+ Trivial3 a,

685+ CountableN a,

686+ FLN () a,

687+ FLN a (),

688+ FLN a a,

689+ Liftable e a Bool

651690 )

652691 =>

653692 (a -> Bool) -> Matrix e a b -> Matrix e a b -> Matrix e a b

@@ -656,9 +695,13 @@ cond p (M a) (M b) = M (I.cond p a b)

656695-- Pretty print

657696

658697-- | Matrix pretty printer

659−pretty :: (KnownNat (I.Count (I.Normalize cols)), Show e) => Matrix e cols rows -> String

698+pretty :: (CountableDimsN cols rows, Show e) => Matrix e cols rows -> String

660699pretty (M m) = I.pretty m

661700

662701-- | Matrix pretty printer

663−prettyPrint :: (KnownNat (I.Count (I.Normalize cols)), Show e) => Matrix e cols rows -> IO ()

702+prettyPrint :: (CountableDimsN cols rows, Show e) => Matrix e cols rows -> IO ()

664703prettyPrint (M m) = I.prettyPrint m

704+

705+-- | Zip two matrices with a given binary function

706+zipWithM :: (e -> f -> g) -> Matrix e a b -> Matrix f a b -> Matrix g a b

707+zipWithM f (M a) (M b) = M (I.zipWithM f a b)

src/LAoP/Relation.hs+34−7

@@ -30,12 +30,21 @@ module LAoP.Relation

3030 Relation (..),

3131 Boolean,

3232

33+ -- * Constraint type synonyms

34+ Countable,

35+ CountableDims,

36+ CountableN,

37+ CountableDimsN,

38+ FLN,

39+ Liftable,

40+ Trivial,

41+ TrivialP,

42+

3343 -- * Primitives

34− empty,

3544 one,

36− junc,

45+ join,

3746 (|||),

38− split,

47+ fork,

3948 (===),

4049

4150 -- * Auxiliary type families

@@ -53,6 +62,7 @@ module LAoP.Relation

5362 toList,

5463 toBool,

5564 pt,

65+ belongs,

5666 relationBuilder,

5767 zeros,

5868 ones,

@@ -80,15 +90,25 @@ module LAoP.Relation

8090 injection,

8191 surjection,

8292 bijection,

93+ domain,

94+ range,

8395

8496 -- * Function division

8597 divisionF,

8698

99+ -- * Relation division

100+ divR,

101+ divL,

102+ divS,

103+ shrunkBy,

104+ overriddenBy,

105+

87106 -- * Relational pairing

88107 splitR,

108+

89109 -- ** Projections

90− p1,

91− p2,

110+ fstR,

111+ sndR,

92112 -- ** Bifunctor

93113 (><),

94114 -- * Relational coproduct

@@ -116,18 +136,25 @@ module LAoP.Relation

116136 linearOrder,

117137 equivalence,

118138 partialEquivalence,

139+ difunctional,

140+

141+ -- * Conditionals

142+ equalizer,

119143

120144 -- ** McCarthy's Conditional

121− -- cond,

145+ predR,

146+ guard,

147+ cond,

122148

123149 -- * Relational composition and lifting

124− identity,

150+ iden,

125151 comp,

126152 fromF,

127153 fromF',

128154

129155 -- ** Relational application

130156 pointAp,

157+ pointApBool,

131158

132159 -- * Matrix printing

133160 pretty,

src/LAoP/Relation/Internal.hs+558−276

@@ -1,3 +1,5 @@

1+{-# LANGUAGE TypeFamilies #-}

2+{-# LANGUAGE ConstraintKinds #-}

13{-# LANGUAGE GADTs #-}

24{-# LANGUAGE UndecidableInstances #-}

35{-# LANGUAGE FlexibleContexts #-}

@@ -39,12 +41,21 @@ module LAoP.Relation.Internal

3941 Relation (..),

4042 Boolean,

4143

44+ -- * Constraint type synonyms

45+ Countable,

46+ CountableDims,

47+ CountableN,

48+ CountableDimsN,

49+ FLN,

50+ Liftable,

51+ Trivial,

52+ TrivialP,

53+

4254 -- * Primitives

43− empty,

4455 one,

45− junc,

56+ join,

4657 (|||),

47− split,

58+ fork,

4859 (===),

4960

5061 -- * Auxiliary type families

@@ -55,13 +66,15 @@ module LAoP.Relation.Internal

5566 -- * Matrix construction and conversion

5667 I.FromLists,

5768 fromLists,

58− fromF,

5969 fromF',

70+ fromF,

6071 toRel,

6172 toLists,

6273 toList,

6374 toBool,

6475 pt,

76+ belongs,

77+ relationBuilder',

6578 relationBuilder,

6679 zeros,

6780 ones,

@@ -89,15 +102,25 @@ module LAoP.Relation.Internal

89102 injection,

90103 surjection,

91104 bijection,

105+ domain,

106+ range,

92107

93108 -- * Function division

94109 divisionF,

95110

111+ -- * Relation division

112+ divR,

113+ divL,

114+ divS,

115+ shrunkBy,

116+ overriddenBy,

117+

96118 -- * Relational pairing

97119 splitR,

120+

98121 -- ** Projections

99− p1,

100− p2,

122+ fstR,

123+ sndR,

101124 -- ** Bifunctor

102125 (><),

103126 -- * Relational coproduct

@@ -125,18 +148,25 @@ module LAoP.Relation.Internal

125148 linearOrder,

126149 equivalence,

127150 partialEquivalence,

151+ difunctional,

152+

153+ -- * Conditionals

154+ equalizer,

128155

129156 -- ** McCarthy's Conditional

130− -- cond,

157+ predR,

158+ guard,

159+ cond,

131160

132161 -- * Relational composition and lifting

133− identity,

162+ iden,

134163 comp,

135− fromF,

136164 fromF',

165+ fromF,

137166

138167 -- ** Relational application

139168 pointAp,

169+ pointApBool,

140170

141171 -- * Matrix printing

142172 pretty,

@@ -148,12 +178,13 @@ import Data.Void

148178import qualified LAoP.Matrix.Internal as I

149179import LAoP.Utils.Internal

150180import Control.DeepSeq

151−import qualified Control.Category as C

152181import Data.Bool

153182import GHC.TypeLits

183+import Prelude hiding (id, (.))

154184

155185-- | Boolean type synonym for working with boolean matrices

156186type Boolean = Natural 0 1

187+type Powerset a = List (List a)

157188

158189-- | Relation data type.

159190newtype Relation a b = R (I.Matrix Boolean (I.Normalize a) (I.Normalize b))

@@ -161,25 +192,34 @@ newtype Relation a b = R (I.Matrix Boolean (I.Normalize a) (I.Normalize b))

161192

162193deriving instance (Read (I.Matrix Boolean (I.Normalize a) (I.Normalize b))) => Read (Relation a b)

163194

164−-- | It isn't possible to implement the 'id' function so it's

165−-- implementation is 'undefined'. However 'comp' can be and this partial

166−-- class implementation exists just to make the code more readable.

167−--

168−-- Please use 'identity' instead.

169−instance C.Category Relation where

170− id = undefined

171− (.) = comp

195+-- | Constraint type synonyms to keep the type signatures less convoluted

196+type Countable a = KnownNat (I.Count a)

197+type CountableDims a b = (Countable a, Countable b)

198+type CountableN a = KnownNat (I.Count (I.Normalize a))

199+type CountableDimsN a b = (CountableN a, CountableN b)

200+type FLN a b = I.FromLists (I.Normalize a) (I.Normalize b)

201+type Liftable a b = (Bounded a, Bounded b, Enum a, Enum b, Eq b, Num Boolean, Ord Boolean)

202+type Trivial a = I.Normalize a ~ I.Normalize (I.Normalize a)

203+type TrivialP a b = I.Normalize (a, b) ~ I.Normalize (I.Normalize a, I.Normalize b)

204+

205+-- | It is possible to implement a constrained version of the category type

206+-- class.

207+instance Category Relation where

208+ type Object Relation a = (FLN a a, CountableN a)

209+ id = iden

210+ (.) = comp

172211

173212instance Num (Relation a b) where

174− -- | Matrix addition becomes Boolean matrix disjunction

213+ -- | Matrix addition becomes Boolean matrix disjointion

175214 (R a) + (R b) = R (I.orM a b)

176215

177216 -- | Matrix subtraction becomes Relational subtraction

178217 (R a) - (R b) = R (I.subM a b)

179218

180− -- | Matrix multiplication becomes Boolean matrix conjunction

219+ -- | Matrix multiplication becomes Boolean matrix conjointion

181220 (R a) * (R b) = R (I.andM a b)

182221

222+ -- | Matrix negation becomes Boolean matrix negation

183223 negate (R a) = R (I.negateM a)

184224

185225-- Type alias

@@ -188,105 +228,107 @@ type One = ()

188228

189229-- Primitives

190230

191−-- | Empty matrix constructor

192−empty :: Relation Zero Zero

193−empty = R I.Empty

194−

195231-- | Unit matrix constructor

196232one :: Boolean -> Relation One One

197233one = R . I.One

198234

199−-- | Boolean Matrix 'Junc' constructor, also known as relational coproduct.

235+-- | Boolean Matrix 'Join' constructor, also known as relational coproduct.

200236--

201237-- See 'eitherR'.

202−junc :: (I.Normalize (Either a b) ~ Either (I.Normalize a) (I.Normalize b))

203− => Relation a c -> Relation b c -> Relation (Either a b) c

204−junc (R a) (R b) = R (I.Junc a b)

238+join :: Relation a c -> Relation b c -> Relation (Either a b) c

239+join (R a) (R b) = R (I.Join a b)

205240

206241infixl 3 |||

207−-- | Boolean Matrix 'Junc' constructor

242+-- | Boolean Matrix 'Join' constructor

243+--

244+-- See 'eitherR'.

208245(|||) ::

209− (I.Normalize (Either a b) ~ Either (I.Normalize a) (I.Normalize b)) =>

210246 Relation a c ->

211247 Relation b c ->

212248 Relation (Either a b) c

213−(|||) = junc

249+(|||) = join

214250

215−-- | Boolean Matrix 'Split' constructor, also known as relational product.

216−split :: (I.Normalize (Either a b) ~ Either (I.Normalize a) (I.Normalize b))

217− => Relation c a -> Relation c b -> Relation c (Either a b)

218−split (R a) (R b) = R (I.Split a b)

251+-- | Boolean Matrix 'Fork' constructor, also known as relational product.

252+fork :: Relation c a -> Relation c b -> Relation c (Either a b)

253+fork (R a) (R b) = R (I.Fork a b)

219254

220255infixl 2 ===

221−-- | Boolean Matrix 'Split' constructor

256+-- | Boolean Matrix 'Fork' constructor

222257(===) ::

223− (I.Normalize (Either a b) ~ Either (I.Normalize a) (I.Normalize b)) =>

224258 Relation c a ->

225259 Relation c b ->

226260 Relation c (Either a b)

227−(===) = split

261+(===) = fork

228262

229263-- Construction

230264

231265-- | Build a matrix out of a list of list of elements. Throws a runtime

232266-- error if the dimensions do not match.

233−fromLists :: (I.FromLists Boolean (I.Normalize a) (I.Normalize b)) => [[Boolean]] -> Relation a b

267+fromLists :: (FLN a b) => [[Boolean]] -> Relation a b

234268fromLists = R . I.fromLists

235269

236−-- | Matrix builder function. Constructs a matrix provided with

237−-- a construction function.

270+-- | Relation builder function. Constructs a relation provided with

271+-- a construction function that operates with indices.

272+relationBuilder' ::

273+ (FLN a b, CountableDimsN a b) =>

274+ ((Int, Int) -> Boolean) -> Relation a b

275+relationBuilder' = R . I.matrixBuilder'

276+

277+-- | Relation builder function. Constructs a relation provided with

278+-- a construction function that operates with arbitrary types.

238279relationBuilder ::

239− (I.FromLists Boolean (I.Normalize a) (I.Normalize b), KnownNat (I.Count (I.Normalize a)), KnownNat (I.Count (I.Normalize b))) =>

240− ((Int, Int) -> Boolean) ->

241− Relation a b

280+ ( FLN a b,

281+ Enum a,

282+ Enum b,

283+ Bounded a,

284+ Bounded b,

285+ Eq a,

286+ CountableDims a b

287+ ) => ((a, b) -> Boolean) -> Relation a b

242288relationBuilder = R . I.matrixBuilder

243289

244290-- | Lifts functions to matrices with arbitrary dimensions.

245291--

246292-- NOTE: Be careful to not ask for a matrix bigger than the cardinality of

247293-- types @a@ or @b@ allows.

248−fromF ::

249− ( Bounded a,

250− Bounded b,

251− Enum a,

252− Enum b,

253− Eq b,

254− KnownNat (I.Count (I.Normalize c)),

255− KnownNat (I.Count (I.Normalize d)),

256− I.FromLists Boolean (I.Normalize d) (I.Normalize c)

294+fromF' ::

295+ ( Liftable a b,

296+ CountableDimsN c d,

297+ FLN d c

257298 )

258299 => (a -> b) -> Relation c d

259−fromF f = R (I.fromFRel f)

300+fromF' f = R (I.fromFRel' f)

260301

261302-- | Lifts functions to matrices with dimensions matching @a@ and @b@

262303-- cardinality's.

263−fromF' ::

264− ( Bounded b,

265− Bounded a,

266− Enum a,

267− Enum b,

268− Eq b,

269− KnownNat (I.Count (I.Normalize a)),

270− KnownNat (I.Count (I.Normalize b)),

271− I.FromLists Boolean (I.Normalize b) (I.Normalize a)

304+fromF ::

305+ ( Liftable a b,

306+ CountableDimsN a b,

307+ FLN b a

272308 )

273309 => (a -> b) -> Relation a b

274−fromF' f = R (I.fromFRel' f)

310+fromF f = R (I.fromFRel f)

275311

276312-- | Lifts relation functions to 'Relation'

277313toRel ::

278− ( Bounded b,

279− Bounded a,

280− Enum a,

281− Enum b,

282− Eq b,

283− KnownNat (I.Count (I.Normalize a)),

284− KnownNat (I.Count (I.Normalize b)),

285− I.FromLists Boolean (I.Normalize b) (I.Normalize a)

314+ ( Liftable a b,

315+ CountableDims a b,

316+ FLN b a

286317 )

287− => (a -> b -> Bool) -> Relation a b

318+ => (a -> b -> Bool) -> Relation a b

288319toRel = R . I.toRel

289320

321+-- | Lowers a 'Relation' to a function

322+fromRel ::

323+ ( Liftable a b,

324+ Eq a,

325+ CountableDimsN a b,

326+ FLN a One,

327+ FLN b One

328+ )

329+ => Relation a b -> (a -> b -> Bool)

330+fromRel r a b = pointApBool a b r

331+

290332-- Conversion

291333

292334-- | Converts a matrix to a list of lists of elements.

@@ -297,94 +339,188 @@ toLists (R m) = I.toLists m

297339toList :: Relation a b -> [Boolean]

298340toList (R m) = I.toList m

299341

300−-- | Converts a well typed @'Relation'@ to @'Bool'@.

342+-- | Converts a well typed 'Relation' to 'Bool'.

301343toBool :: Relation One One -> Bool

302344toBool r = case toList r of

303345 [Nat 0] -> False

304346 _ -> True

305347

306−-- | Power transpose

307−pt ::

308− ( Bounded a,

309− Bounded b,

310− Enum a,

311− Enum b,

348+-- | Power transpose.

349+--

350+-- Maps a relation to a set valued function.

351+pt ::

352+ ( Liftable a b,

312353 Eq a,

313− Eq b,

314− KnownNat (I.Count (I.Normalize a)),

315− KnownNat (I.Count (I.Normalize b)),

316− I.FromLists Boolean (I.Normalize a) One,

317− I.FromLists Boolean (I.Normalize b) One

354+ CountableDimsN a b,

355+ FLN a One,

356+ FLN b One

318357 )

319− => Relation a b -> (a -> [b])

358+ => Relation a b -> (a -> List b)

320359pt r a =

321− let lb = [minBound .. maxBound]

322− in [ b | b <- lb, toBool (pointAp a b r) ]

360+ let (L lb) = maxBound

361+ in L [ b | b <- lb, toBool (pointAp a b r) ]

362+

363+-- | Belongs relation

364+belongs ::

365+ ( Bounded a,

366+ Enum a,

367+ Eq a,

368+ CountableDims (List a) a,

369+ FLN a (List a)

370+ )

371+ => Relation (List a) a

372+belongs = toRel elemR

373+ where

374+ elemR (L l) x = x `elem` l

323375

324376-- Zeros Matrix

325377

326−-- | The zero matrix. A matrix wholly filled with zeros.

378+-- | The zero relation. A relation where no element of type @a@ relates

379+-- with elements of type @b@.

380+--

381+-- Also known as ⊥ (Bottom) Relation.

382+--

383+-- @

384+-- r `.` ⊥ == ⊥ `.` r == ⊥

385+-- ⊥ ``sse`` R && R ``sse`` T == True

386+-- @

327387zeros ::

328− (I.FromLists Boolean (I.Normalize a) (I.Normalize b), KnownNat (I.Count (I.Normalize a)), KnownNat (I.Count (I.Normalize b))) =>

388+ (FLN a b, CountableDimsN a b) =>

329389 Relation a b

330−zeros = relationBuilder (const (nat 0))

390+zeros = relationBuilder' (const (nat 0))

331391

332392-- Ones Matrix

333393

334−-- | The ones matrix. A matrix wholly filled with ones.

394+-- | The ones relation. A relation where every element of type @a@ relates

395+-- with every element of type @b@.

335396--

336−-- Also known as T (Top) matrix.

397+-- Also known as T (Top) Relation or universal Relation.

398+--

399+-- @

400+-- ⊥ ``sse`` R && R ``sse`` T == True

401+-- @

337402ones ::

338− (I.FromLists Boolean (I.Normalize a) (I.Normalize b), KnownNat (I.Count (I.Normalize a)), KnownNat (I.Count (I.Normalize b))) =>

403+ (FLN a b, CountableDimsN a b) =>

339404 Relation a b

340−ones = relationBuilder (const (nat 1))

405+ones = relationBuilder' (const (nat 1))

341406

342407-- Bang Matrix

343408

344−-- | The T (Top) row vector matrix.

409+-- | The T (Top) row vector relation.

345410bang ::

346− (I.FromLists Boolean (I.Normalize a) One, KnownNat (I.Count (I.Normalize a))) =>

411+ (FLN a One, CountableN a) =>

347412 Relation a One

348413bang = ones

349414

350415-- | Point constant relation

351−point ::

416+point ::

352417 ( Bounded a,

353418 Enum a,

354419 Eq a,

355− KnownNat (I.Count (I.Normalize a)),

356− I.FromLists Boolean (I.Normalize a) One

420+ CountableN a,

421+ FLN a One

357422 ) => a -> Relation One a

358−point a = fromF' (const a)

423+point = fromF . const

359424

360−-- Identity Matrix

425+-- iden Matrix

361426

362−-- | Identity matrix

363−identity ::

364− (I.FromLists Boolean (I.Normalize a) (I.Normalize a), KnownNat (I.Count (I.Normalize a))) =>

365− Relation a a

366−identity = relationBuilder (bool (nat 0) (nat 1) . uncurry (==))

427+-- | iden matrix

428+--

429+-- @

430+-- 'iden' `.` r == r == r `.` 'iden'

431+-- @

432+iden ::

433+ (FLN a a, CountableN a) => Relation a a

434+iden = relationBuilder' (bool (nat 0) (nat 1) . uncurry (==))

367435

368436-- | Relational composition

437+--

438+-- @

439+-- r `.` (s `.` p) = (r `.` s) `.` p

440+-- @

369441comp :: Relation b c -> Relation a b -> Relation a c

370442comp (R a) (R b) = R (I.compRel a b)

371443

372−-- | Relational application

444+-- | Relational right division

445+--

446+-- @'divR' x y@ is the largest relation @z@ which,

447+-- pre-composed with @y@, approximates @x@.

448+divR :: Relation b c -> Relation b a -> Relation a c

449+divR (R x) (R y) = R (I.divR x y)

450+

451+-- | Relational left division

452+--

453+-- The dual division operator:

454+--

455+-- @

456+-- 'divL' y x == 'conv' ('divR' ('conv' x) ('conv' y)

457+-- @

458+divL :: Relation c b -> Relation a b -> Relation a c

459+divL (R x) (R y) = R (I.divL x y)

460+

461+-- | Relational symmetric division

462+--

463+-- @'pointAp' c b ('divS' s r)@ means that @b@ and @c@

464+-- are related to exactly the same outputs by @r@ and by @s@.

465+divS :: Relation c a -> Relation b a -> Relation c b

466+divS (R x) (R y) = R (I.divS x y)

467+

468+-- | Relational shrinking.

469+--

470+-- @r ``shrunkBy`` s@ is the largest part of @r@ such that,

471+-- if it yields an output for an input @x@, it must be a maximum,

472+-- with respect to @s@, among all possible outputs of @x@ by @r@.

473+shrunkBy :: Relation b a -> Relation a a -> Relation b a

474+shrunkBy r s = r `intersection` divR s (conv r)

475+

476+-- | Relational overriding.

477+--

478+-- @r ``overriddenBy`` s@ yields the relation which contains the

479+-- whole of @s@ and that part of @r@ where @s@ is undefined.

480+--

481+-- @

482+-- 'zeros' ``overriddenBy`` s == s

483+-- r ``overriddenBy`` 'zeros' == r

484+-- r ``overriddenBy`` r == r

485+-- @

486+overriddenBy ::

487+ ( FLN b b,

488+ CountableN b

489+ ) => Relation a b -> Relation a b -> Relation a b

490+overriddenBy r s = s `union` r `intersection` divR zeros (conv s)

491+

492+-- | Relational application.

493+--

494+-- If @a@ and @b@ are related by 'Relation' @r@

495+-- then @'pointAp' a b r == 'one' ('nat' 1)@

373496pointAp ::

374− ( Bounded a,

375− Bounded b,

376− Enum a,

377− Enum b,

497+ ( Liftable a b,

378498 Eq a,

379− Eq b,

380− KnownNat (I.Count (I.Normalize a)),

381− KnownNat (I.Count (I.Normalize b)),

382− I.FromLists Boolean (I.Normalize a) One,

383− I.FromLists Boolean (I.Normalize b) One

499+ CountableDimsN a b,

500+ FLN a One,

501+ FLN b One

384502 ) => a -> b -> Relation a b -> Relation One One

385−pointAp a b r = conv (point b) `comp` r `comp` point a

503+pointAp a b r = conv (point b) . r . point a

504+

505+-- | Relational application

506+--

507+-- The same as 'pointAp' but converts 'Boolean' to 'Bool'

508+pointApBool ::

509+ ( Liftable a b,

510+ Eq a,

511+ CountableDimsN a b,

512+ FLN a One,

513+ FLN b One

514+ ) => a -> b -> Relation a b -> Bool

515+pointApBool a b r = toBool $ conv (point b) . r . point a

386516

387517-- | Relational converse

518+--

519+-- Given binary 'Relation' r, writing @'pointAp' a b r@

520+-- (read: “@b@ is related to @a@ by @r@”) means the same as

521+-- @'pointAp' b a ('conv' r)@, where @'conv' r@ is said to be

522+-- the converse of @r@.

523+-- In terms of grammar, @'conv' r@ corresponds to the passive voice

388524conv :: Relation a b -> Relation b a

389525conv (R a) = R (I.tr a)

390526

@@ -402,165 +538,187 @@ iff r s = r == s

402538

403539-- | Relational intersection

404540--

405−-- Lifts pointwise conjunction.

541+-- Lifts pointwise conjointion.

542+--

543+-- @

544+-- (r ``intersection`` s) ``intersection`` t == r ``intersection`` (s ``intersection`` t)

545+-- x ``sse`` r ``intersection`` s == x ``intersection`` r && x ``intersection`` s

546+-- @

406547intersection :: Relation a b -> Relation a b -> Relation a b

407548intersection a b = a * b

408549

409550-- | Relational union

410551--

411−-- Lifts pointwise disjunction.

552+-- Lifts pointwise disjointion.

553+--

554+-- @

555+-- (r ``union`` s) ``union`` t == r `'union' (s ``union`` t)

556+-- r ``union`` s ``sse`` x == r ``sse`` x && s ``sse`` x

557+-- r `.` (s ``union`` t) == (r `.` s) ``union`` (r `.` t)

558+-- (s ``union`` t) `.` r == (s `.` r) ``union`` (t `.` r)

559+-- @

412560union :: Relation a b -> Relation a b -> Relation a b

413561union a b = a + b

414562

415563-- | Relation Kernel

564+--

565+-- @

566+-- 'ker' r == 'conv' r `.` r

567+-- 'ker' r == 'img' ('conv' r)

568+-- @

416569ker :: Relation a b -> Relation a a

417−ker r = conv r `comp` r

570+ker r = conv r . r

418571

419572-- | Relation Image

573+--

574+-- @

575+-- 'img' r == r `.` conv r

576+-- 'img' r == 'ker' ('conv' r)

577+-- @

420578img :: Relation a b -> Relation b b

421−img r = r `comp` conv r

579+img r = r . conv r

422580

423−-- | Function division.

581+-- | Function division. Special case of 'divS'.

424582--

425583-- NOTE: _This is only valid_ if @f@ and @g@ are 'function's, i.e. 'simple' and

426584-- 'entire'.

427585--

428−-- @division f g == conv g `'comp'` f@

586+-- @'divisionF' f g == 'conv' g `.` f@

429587divisionF :: Relation a c -> Relation b c -> Relation a b

430−divisionF f g = conv g `comp` f

588+divisionF f g = conv g . f

431589

432590-- Taxonomy of binary relations

433591

434−-- | A 'Relation' @r@ is simple iff @'coreflexive' ('img' r)@

435−simple :: (KnownNat (I.Count (I.Normalize b)), I.FromLists Boolean (I.Normalize b) (I.Normalize b)) => Relation a b -> Bool

592+-- | A 'Relation' @r@ is 'simple' 'iff' @'coreflexive' ('img' r)@

593+simple :: (CountableN b, FLN b b) => Relation a b -> Bool

436594simple = coreflexive . img

437595

438−-- | A 'Relation' @r@ is injective iff @'coreflexive' ('ker' r)@

439−injective :: (KnownNat (I.Count (I.Normalize a)), I.FromLists Boolean (I.Normalize a) (I.Normalize a)) => Relation a b -> Bool

596+-- | A 'Relation' @r@ is 'injective' 'iff' @'coreflexive' ('ker' r)@

597+injective :: (CountableN a, FLN a a) => Relation a b -> Bool

440598injective = coreflexive . ker

441599

442−-- | A 'Relation' @r@ is entire iff @'reflexive' ('ker' r)@

443−entire :: (KnownNat (I.Count (I.Normalize a)), I.FromLists Boolean (I.Normalize a) (I.Normalize a)) => Relation a b -> Bool

600+-- | A 'Relation' @r@ is 'entire' 'iff' @'reflexive' ('ker' r)@

601+entire :: (CountableN a, FLN a a) => Relation a b -> Bool

444602entire = reflexive . ker

445603

446−-- | A 'Relation' @r@ is surjective iff @'reflexive' ('img' r)@

447−surjective :: (KnownNat (I.Count (I.Normalize b)), I.FromLists Boolean (I.Normalize b) (I.Normalize b)) => Relation a b -> Bool

604+-- | A 'Relation' @r@ is 'surjective' 'iff' @'reflexive' ('img' r)@

605+surjective :: (CountableN b, FLN b b) => Relation a b -> Bool

448606surjective = reflexive . img

449607

450−-- | A 'Relation' @r@ is a function iff @'simple' r && 'entire' r@

608+-- | A 'Relation' @r@ is a 'function' 'iff' @'simple' r && 'entire' r@

451609--

452610-- A 'function' @f@ enjoys the following properties, where @r@ and @s@ are binary

453611-- relations:

454612--

455613-- @

456−-- f `'comp'` r `'sse'` s == r `'sse'` f `'comp'` s

457−-- r `'comp'` f `'sse'` s == r `'sse'` s `'comp'` f

614+-- f `.` r ``sse`` s == r ``sse`` f `.` s

615+-- r `.` f ``sse`` s == r ``sse`` s `.` f

458616-- @

459617function ::

460− ( KnownNat (I.Count (I.Normalize b)),

461− KnownNat (I.Count (I.Normalize a)),

462− I.FromLists Boolean (I.Normalize a) (I.Normalize a),

463− I.FromLists Boolean (I.Normalize b) (I.Normalize b)

618+ ( CountableDimsN a b,

619+ FLN a a,

620+ FLN b b

464621 )

465622 => Relation a b -> Bool

466623function r = simple r && entire r

467624

468−-- | A 'Relation' @r@ is a representation iff @'injective' r && 'entire' r@

625+-- | A 'Relation' @r@ is a 'representation' 'iff' @'injective' r && 'entire' r@

469626representation ::

470− ( KnownNat (I.Count (I.Normalize a)),

471− I.FromLists Boolean (I.Normalize a) (I.Normalize a)

627+ ( CountableN a,

628+ FLN a a

472629 )

473630 => Relation a b -> Bool

474631representation r = injective r && entire r

475632

476−-- | A 'Relation' @r@ is an abstraction iff @'surjective' r && 'simple' r@

633+-- | A 'Relation' @r@ is an 'abstraction' 'iff' @'surjective' r && 'simple' r@

477634abstraction ::

478− ( KnownNat (I.Count (I.Normalize b)),

479− I.FromLists Boolean (I.Normalize b) (I.Normalize b)

635+ ( CountableN b,

636+ FLN b b

480637 )

481638 => Relation a b -> Bool

482639abstraction r = surjective r && simple r

483640

484−-- | A 'Relation' @r@ is a surjection iff @'function' r && 'abstraction' r@

641+-- | A 'Relation' @r@ is a 'surjection' 'iff' @'function' r && 'abstraction' r@

485642surjection ::

486− ( KnownNat (I.Count (I.Normalize b)),

487− KnownNat (I.Count (I.Normalize a)),

488− I.FromLists Boolean (I.Normalize a) (I.Normalize a),

489− I.FromLists Boolean (I.Normalize b) (I.Normalize b)

643+ ( CountableDimsN a b,

644+ FLN a a,

645+ FLN b b

490646 )

491647 => Relation a b -> Bool

492648surjection r = function r && abstraction r

493649

494−-- | A 'Relation' @r@ is a injection iff @'function' r && 'representation' r@

650+-- | A 'Relation' @r@ is a 'injection' 'iff' @'function' r && 'representation' r@

495651injection ::

496− ( KnownNat (I.Count (I.Normalize b)),

497− KnownNat (I.Count (I.Normalize a)),

498− I.FromLists Boolean (I.Normalize a) (I.Normalize a),

499− I.FromLists Boolean (I.Normalize b) (I.Normalize b)

652+ ( CountableDimsN a b,

653+ FLN a a,

654+ FLN b b

500655 )

501656 => Relation a b -> Bool

502657injection r = function r && representation r

503658

504−-- | A 'Relation' @r@ is an bijection iff @'injection' r && 'surjection' r@

659+-- | A 'Relation' @r@ is an 'bijection' 'iff' @'injection' r && 'surjection' r@

505660bijection ::

506− ( KnownNat (I.Count (I.Normalize b)),

507− KnownNat (I.Count (I.Normalize a)),

508− I.FromLists Boolean (I.Normalize b) (I.Normalize b),

509− I.FromLists Boolean (I.Normalize a) (I.Normalize a)

661+ ( CountableDimsN a b,

662+ FLN b b,

663+ FLN a a

510664 ) => Relation a b -> Bool

511665bijection r = injection r && surjection r

512666

513−

514667-- Properties of relations

515668

516−-- | A 'Relation' @r@ is reflexive iff @'identity' `'sse'` r@

517−reflexive :: (KnownNat (I.Count (I.Normalize a)), I.FromLists Boolean (I.Normalize a) (I.Normalize a)) => Relation a a -> Bool

518−reflexive r = identity <= r

669+-- | A 'Relation' @r@ is 'reflexive' 'iff' @'id' ``sse`` r@

670+reflexive :: (CountableN a, FLN a a) => Relation a a -> Bool

671+reflexive r = id <= r

519672

520−-- | A 'Relation' @r@ is coreflexive iff @r `'sse'` 'identity'@

521−coreflexive :: (KnownNat (I.Count (I.Normalize a)), I.FromLists Boolean (I.Normalize a) (I.Normalize a)) => Relation a a -> Bool

522−coreflexive r = r <= identity

673+-- | A 'Relation' @r@ is 'coreflexive' 'iff' @r ``sse`` 'id'@

674+coreflexive :: (CountableN a, FLN a a) => Relation a a -> Bool

675+coreflexive r = r <= id

523676

524−-- | A 'Relation' @r@ is transitive iff @(r `'comp'` r) `'sse'` r@

677+-- | A 'Relation' @r@ is 'transitive' 'iff' @(r `.` r) ``sse`` r@

525678transitive :: Relation a a -> Bool

526−transitive r = (r `comp` r) `sse` r

679+transitive r = (r . r) `sse` r

527680

528−-- | A 'Relation' @r@ is symmetric iff @r == conv r@

681+-- | A 'Relation' @r@ is 'symmetric' 'iff' @r == 'conv' r@

529682symmetric :: Relation a a -> Bool

530683symmetric r = r == conv r

531684

532−-- | A 'Relation' @r@ is anti-symmetric iff @(r `'intersection'` 'conv' r) `'sse'` 'identity'@

533−antiSymmetric :: (KnownNat (I.Count (I.Normalize a)), I.FromLists Boolean (I.Normalize a) (I.Normalize a)) => Relation a a -> Bool

534−antiSymmetric r = (r `intersection` conv r) `sse` identity

685+-- | A 'Relation' @r@ is anti-symmetric 'iff' @(r ``intersection`` 'conv' r) ``sse`` 'id'@

686+antiSymmetric :: (CountableN a, FLN a a) => Relation a a -> Bool

687+antiSymmetric r = (r `intersection` conv r) `sse` id

535688

536−-- | A 'Relation' @r@ is irreflexive iff @(r `'intersection'` identity) == 'zeros'@

537−irreflexive :: (KnownNat (I.Count (I.Normalize a)), I.FromLists Boolean (I.Normalize a) (I.Normalize a)) => Relation a a -> Bool

538−irreflexive r = (r `intersection` identity) == zeros

689+-- | A 'Relation' @r@ is 'irreflexive' 'iff' @(r ``intersection`` 'id') == 'zeros'@

690+irreflexive :: (CountableN a, FLN a a) => Relation a a -> Bool

691+irreflexive r = (r `intersection` id) == zeros

539692

540−-- | A 'Relation' @r@ is connected iff @(r `'union'` 'conv' r) == 'ones'@

541−connected :: (KnownNat (I.Count (I.Normalize a)), I.FromLists Boolean (I.Normalize a) (I.Normalize a)) => Relation a a -> Bool

693+-- | A 'Relation' @r@ is 'connected' 'iff' @(r ``union`` 'conv' r) == 'ones'@

694+connected :: (CountableN a, FLN a a) => Relation a a -> Bool

542695connected r = (r `union` conv r) == ones

543696

544−-- | A 'Relation @r@ is a preorder iff @'reflexive' r && 'transitive' r@

545−preorder :: (KnownNat (I.Count (I.Normalize a)), I.FromLists Boolean (I.Normalize a) (I.Normalize a)) => Relation a a -> Bool

697+-- | A 'Relation' @r@ is a 'preorder' 'iff' @'reflexive' r && 'transitive' r@

698+preorder :: (CountableN a, FLN a a) => Relation a a -> Bool

546699preorder r = reflexive r && transitive r

547700

548−-- | A 'Relation @r@ is a partial order iff @'antiSymmetric' r && 'preorder' r@

549−partialOrder :: (KnownNat (I.Count (I.Normalize a)), I.FromLists Boolean (I.Normalize a) (I.Normalize a)) => Relation a a -> Bool

701+-- | A 'Relation' @r@ is a partial-order 'iff' @'antiSymmetric' r && 'preorder' r@

702+partialOrder :: (CountableN a, FLN a a) => Relation a a -> Bool

550703partialOrder r = antiSymmetric r && preorder r

551704

552−-- | A 'Relation @r@ is a linear order iff @'connected' r && 'partialOrder' r@

553−linearOrder :: (KnownNat (I.Count (I.Normalize a)), I.FromLists Boolean (I.Normalize a) (I.Normalize a)) => Relation a a -> Bool

705+-- | A 'Relation' @r@ is a linear-order 'iff' @'connected' r && 'partialOrder' r@

706+linearOrder :: (CountableN a, FLN a a) => Relation a a -> Bool

554707linearOrder r = connected r && partialOrder r

555708

556−-- | A 'Relation @r@ is an equivalence iff @'symmetric' r && 'preorder' r@

557−equivalence :: (KnownNat (I.Count (I.Normalize a)), I.FromLists Boolean (I.Normalize a) (I.Normalize a)) => Relation a a -> Bool

709+-- | A 'Relation' @r@ is an 'equivalence' 'iff' @'symmetric' r && 'preorder' r@

710+equivalence :: (CountableN a, FLN a a) => Relation a a -> Bool

558711equivalence r = symmetric r && preorder r

559712

560−-- | A 'Relation @r@ is a partial equivalence iff @'partialOrder' r && 'equivalence' r@

561−partialEquivalence :: (KnownNat (I.Count (I.Normalize a)), I.FromLists Boolean (I.Normalize a) (I.Normalize a)) => Relation a a -> Bool

713+-- | A 'Relation' @r@ is a partial-equivalence 'iff' @'partialOrder' r && 'equivalence' r@

714+partialEquivalence :: (CountableN a, FLN a a) => Relation a a -> Bool

562715partialEquivalence r = partialOrder r && equivalence r

563716

717+-- | A 'Relation' @r@ is 'difunctional' or regular wherever

718+-- @r `.` 'conv' r `.` r == r@

719+difunctional :: Relation a b -> Bool

720+difunctional r = r . conv r . r == r

721+

564722-- Relational pairing

565723

566724-- | Relational pairing.

@@ -568,64 +726,81 @@ partialEquivalence r = partialOrder r && equivalence r

568726-- NOTE: That this is not a true categorical product, see for instance:

569727--

570728-- @

571−-- | 'p1' `'comp'` 'splitR' a b `'sse'` a

572−-- 'splitR' a b <=> |

573−-- | 'p2' `'comp'` 'splitR' a b `'sse'` b

729+-- | 'fstR' `.` 'splitR' a b ``sse`` a

730+-- 'splitR' a b <=> |

731+-- | 'sndR' `.` 'splitR' a b ``sse`` b

574732-- @

575733--

576734-- __Emphasis__ on the 'sse'.

735+--

736+-- @

737+-- 'splitR' r s `.` f == 'splitR' (r `.` f) (s `.` f)

738+-- (R '><' S) `.` 'splitR' p q == 'splitR' (r `.` p) (s `.` q)

739+-- 'conv' ('splitR' r s) `.` 'splitR' x y == ('conv' r `.` x) ``intersection`` ('conv' s `.` y)

740+-- @

741+--

742+-- @

743+-- 'eitherR' ('splitR' r s) ('splitR' t v) == 'splitR' ('eitherR' r t) ('eitherR' s v)

744+-- @

577745splitR ::

578− ( KnownNat (I.Count (I.Normalize a)),

579− KnownNat (I.Count (I.Normalize b)),

580− KnownNat (I.Count (I.Normalize (a, b))),

581− I.FromLists Boolean (I.Normalize (a, b)) (I.Normalize a),

582− I.FromLists Boolean (I.Normalize (a, b)) (I.Normalize b),

583− I.Normalize (a, b) ~ I.Normalize (I.Normalize a, I.Normalize b)

746+ ( CountableDimsN a b,

747+ CountableN (a, b),

748+ FLN (a, b) a,

749+ FLN (a, b) b,

750+ TrivialP a b

584751 )

585752 => Relation c a -> Relation c b -> Relation c (a, b)

586−splitR (R f) (R g) = R (I.khatri f g)

753+splitR (R f) (R g) = R (I.kr f g)

587754

588755-- | Relational pairing first component projection

589−p1 ::

756+--

757+-- @

758+-- 'fstR' `.` 'splitR' r s ``sse`` r

759+-- @

760+fstR ::

590761 forall a b .

591− ( KnownNat (I.Count (I.Normalize a)),

592− KnownNat (I.Count (I.Normalize b)),

593− KnownNat (I.Count (I.Normalize (a, b))),

594− I.FromLists Boolean (I.Normalize (a, b)) (I.Normalize a),

595− I.Normalize (a, b) ~ I.Normalize (I.Normalize a, I.Normalize b)

762+ ( CountableDimsN a b,

763+ CountableN (a, b),

764+ FLN (a, b) a,

765+ TrivialP a b

596766 )

597767 => Relation (a, b) a

598−p1 = R (I.kp1 @Boolean @(I.Normalize a) @(I.Normalize b))

768+fstR = R (I.fstM @Boolean @(I.Normalize a) @(I.Normalize b))

599769

600770-- | Relational pairing second component projection

601−p2 ::

771+--

772+-- @

773+-- 'sndR' `.` 'splitR' r s ``sse`` s

774+-- @

775+sndR ::

602776 forall a b .

603− ( KnownNat (I.Count (I.Normalize b)),

604− KnownNat (I.Count (I.Normalize a)),

605− KnownNat (I.Count (I.Normalize (a, b))),

606− I.FromLists Boolean (I.Normalize (a, b)) (I.Normalize b),

607− I.Normalize (a, b) ~ I.Normalize (I.Normalize a, I.Normalize b)

777+ ( CountableDimsN a b,

778+ CountableN (a, b),

779+ FLN (a, b) b,

780+ TrivialP a b

608781 )

609782 => Relation (a, b) b

610−p2 = R (I.kp2 @Boolean @(I.Normalize a) @(I.Normalize b))

783+sndR = R (I.sndM @Boolean @(I.Normalize a) @(I.Normalize b))

611784

612785-- Relational pairing functor

613786

614787infixl 4 ><

615788-- | Relational pairing functor

789+--

790+-- @

791+-- r '><' s == 'splitR' (r `.` fstR) (s `.` sndR)

792+-- (r '><' s) `.` (p '><' q) == (r `.` p) '><' (s `.` q)

793+-- @

616794(><) ::

617− ( KnownNat (I.Count (I.Normalize a)),

618− KnownNat (I.Count (I.Normalize b)),

619− KnownNat (I.Count (I.Normalize c)),

620− KnownNat (I.Count (I.Normalize d)),

621− KnownNat (I.Count (I.Normalize (a, c))),

622− KnownNat (I.Count (I.Normalize (b, d))),

623− I.FromLists Boolean (I.Normalize (a, c)) (I.Normalize a),

624− I.FromLists Boolean (I.Normalize (a, c)) (I.Normalize c),

625− I.FromLists Boolean (I.Normalize (b, d)) (I.Normalize b),

626− I.FromLists Boolean (I.Normalize (b, d)) (I.Normalize d),

627− I.Normalize (a, c) ~ I.Normalize (I.Normalize a, I.Normalize c),

628− I.Normalize (b, d) ~ I.Normalize (I.Normalize b, I.Normalize d)

795+ ( CountableDimsN a b,

796+ CountableDimsN c d,

797+ CountableDimsN (a, c) (b, d),

798+ FLN (a, c) a,

799+ FLN (a, c) c,

800+ FLN (b, d) b,

801+ FLN (b, d) d,

802+ TrivialP a c,

803+ TrivialP b d

629804 )

630805 => Relation a b -> Relation c d -> Relation (a, c) (b, d)

631806(><) (R a) (R b) = R ((I.><) a b)

@@ -633,28 +808,47 @@ infixl 4 ><

633808-- Relational co-products

634809

635810-- | Relational coproduct.

636−eitherR :: (I.Normalize (Either a b) ~ Either (I.Normalize a) (I.Normalize b))

637− => Relation a c -> Relation b c -> Relation (Either a b) c

638−eitherR = junc

811+--

812+-- @

813+-- | 'eitherR' a b `.` 'i1' == a

814+-- 'eitherR' a b <=> |

815+-- | 'eitherR' a b `.` 'i2' == b

816+-- @

817+--

818+-- @

819+-- 'eitherR' r s `.` 'conv' ('eitherR' t u) == (r `.` 'conv' t) ``union`` (s `.` 'conv' u)

820+-- @

821+--

822+-- @

823+-- 'eitherR' ('splitR' r s) ('splitR' t v) == 'splitR' ('eitherR' r t) ('eitherR' s v)

824+-- @

825+eitherR :: Relation a c -> Relation b c -> Relation (Either a b) c

826+eitherR = join

639827

640828-- | Relational coproduct first component injection

829+--

830+-- @

831+-- 'img' 'i1' ``union`` 'img' 'i2' == 'id'

832+-- 'i1' `.` 'i2' = 'zeros'

833+-- @

641834i1 ::

642− ( KnownNat (I.Count (I.Normalize b)),

643− KnownNat (I.Count (I.Normalize a)),

644− I.FromLists Boolean (I.Normalize b) (I.Normalize a),

645− I.FromLists Boolean (I.Normalize a) (I.Normalize a),

646− I.Normalize (Either a b) ~ Either (I.Normalize a) (I.Normalize b)

835+ ( CountableDimsN a b,

836+ FLN b a,

837+ FLN a a

647838 )

648839 => Relation a (Either a b)

649840i1 = R I.i1

650841

651842-- | Relational coproduct second component injection

843+--

844+-- @

845+-- 'img' 'i1' ``union`` 'img' 'i2' == 'id'

846+-- 'i1' `.` 'i2' = 'zeros'

847+-- @

652848i2 ::

653− ( KnownNat (I.Count (I.Normalize b)),

654− KnownNat (I.Count (I.Normalize a)),

655− I.FromLists Boolean (I.Normalize a) (I.Normalize b),

656− I.FromLists Boolean (I.Normalize b) (I.Normalize b),

657− I.Normalize (Either a b) ~ Either (I.Normalize a) (I.Normalize b)

849+ ( CountableDimsN a b,

850+ FLN a b,

851+ FLN b b

658852 )

659853 => Relation b (Either a b)

660854i2 = R I.i2

@@ -662,15 +856,16 @@ i2 = R I.i2

662856infixl 5 -|-

663857

664858-- | Relational coproduct functor.

859+--

860+-- @

861+-- r '-|-' s == 'eitherR' ('i1' `.` r) ('i2' `.` s)

862+-- @

665863(-|-) ::

666− ( KnownNat (I.Count (I.Normalize d)),

667− KnownNat (I.Count (I.Normalize b)),

668− I.FromLists Boolean (I.Normalize b) (I.Normalize b),

669− I.FromLists Boolean (I.Normalize d) (I.Normalize b),

670− I.FromLists Boolean (I.Normalize b) (I.Normalize d),

671− I.FromLists Boolean (I.Normalize d) (I.Normalize d),

672− I.Normalize (Either a c) ~ Either (I.Normalize a) (I.Normalize c),

673− I.Normalize (Either b d) ~ Either (I.Normalize b) (I.Normalize d)

864+ ( CountableDimsN b d,

865+ FLN b b,

866+ FLN d b,

867+ FLN b d,

868+ FLN d d

674869 )

675870 => Relation a b -> Relation c d -> Relation (Either a c) (Either b d)

676871(-|-) (R a) (R b) = R ((I.-|-) a b)

@@ -678,49 +873,136 @@ infixl 5 -|-

678873-- Relational "Currying"

679874

680875-- | Relational 'trans'

876+--

877+-- Every n-ary relation can be expressed as a binary relation through

878+-- 'trans'/'untrans';

879+-- more-over, where each particular attribute is placed (input/output) is irrelevant.

681880trans ::

682− ( KnownNat (I.Count (I.Normalize (a, b))),

683− KnownNat (I.Count (I.Normalize a)),

684− KnownNat (I.Count (I.Normalize (c, b))),

685− KnownNat (I.Count (I.Normalize b)),

686− KnownNat (I.Count (I.Normalize c)),

687− I.FromLists Boolean (I.Normalize (c, b)) (I.FromNat (I.Count c)),

688− I.FromLists Boolean (I.Normalize (c, b)) (I.FromNat (I.Count b)),

689− I.FromLists Boolean (I.Normalize (a, b)) (I.FromNat (I.Count b)),

690− I.FromLists Boolean (I.Normalize (a, b)) (I.FromNat (I.Count a)),

691− I.Normalize (a, b) ~ I.Normalize (I.Normalize (a, b)),

692− I.Normalize (c, b) ~ I.Normalize (I.Normalize (c, b)),

693− I.Normalize (I.Normalize a, I.Normalize b) ~ I.FromNat (I.Count (I.Normalize (a, b))),

694− I.Normalize (I.Normalize c, I.Normalize b) ~ I.FromNat (I.Count (I.Normalize (c, b)))

881+ ( CountableDimsN a b,

882+ CountableN c,

883+ CountableDimsN (a, b) (c, b),

884+ FLN (c, b) c,

885+ FLN (c, b) b,

886+ FLN (a, b) a,

887+ FLN (a, b) b,

888+ Trivial (a, b),

889+ Trivial (c, b),

890+ TrivialP a b,

891+ TrivialP c b

695892 )

696893 => Relation (a, b) c -> Relation a (c, b)

697−trans r = splitR r p2 `comp` conv p1

894+trans r = splitR r sndR . conv fstR

698895

699896-- | Relational 'untrans'

897+--

898+-- Every n-ary relation can be expressed as a binary relation through

899+-- 'trans'/'untrans';

900+-- more-over, where each particular attribute is placed (input/output) is irrelevant.

700901untrans ::

701− ( KnownNat (I.Count (I.Normalize (a, b))),

702− KnownNat (I.Count (I.Normalize a)),

703− KnownNat (I.Count (I.Normalize (c, b))),

704− KnownNat (I.Count (I.Normalize b)),

705− KnownNat (I.Count (I.Normalize c)),

706− I.FromLists Boolean (I.Normalize (c, b)) (I.FromNat (I.Count c)),

707− I.FromLists Boolean (I.Normalize (c, b)) (I.FromNat (I.Count b)),

708− I.FromLists Boolean (I.Normalize (a, b)) (I.FromNat (I.Count b)),

709− I.FromLists Boolean (I.Normalize (a, b)) (I.FromNat (I.Count a)),

710− I.Normalize (a, b) ~ I.Normalize (I.Normalize (a, b)),

711− I.Normalize (c, b) ~ I.Normalize (I.Normalize (c, b)),

712− I.Normalize (I.Normalize a, I.Normalize b) ~ I.FromNat (I.Count (I.Normalize (a, b))),

713− I.Normalize (I.Normalize c, I.Normalize b) ~ I.FromNat (I.Count (I.Normalize (c, b)))

902+ ( CountableDimsN a b,

903+ CountableN c,

904+ CountableDimsN (a, b) (c, b),

905+ FLN (c, b) c,

906+ FLN (c, b) b,

907+ FLN (a, b) b,

908+ FLN (a, b) a,

909+ Trivial (a, b),

910+ Trivial (c, b),

911+ TrivialP a b,

912+ TrivialP c b

714913 )

715914 => Relation a (c, b) -> Relation (a, b) c

716−untrans s = p1 `comp` conv (splitR (conv s) p2)

915+untrans s = fstR . conv (splitR (conv s) sndR)

916+

917+-- | Transforms predicate @p@ into a correflexive relation.

918+--

919+-- @

920+-- 'predR' ('const' True) == 'id'

921+-- 'predR' ('const' False) == 'zeros'

922+-- @

923+--

924+-- @

925+-- 'predR' q `.` 'predR' p == 'predR' q ``union`` 'predR' p

926+-- @

927+predR ::

928+ ( Bounded a,

929+ Enum a,

930+ Countable a,

931+ CountableN a,

932+ FLN a a,

933+ FLN Bool a

934+ )

935+ => Relation a Bool -> Relation a a

936+predR p = id `intersection` divisionF (fromF (const True)) p

937+

938+-- | Equalizes functions @f@ and @g@.

939+-- That is, @'equalizer' f g@ is the largest coreflexive

940+-- that restricts @g@ so that @f@ and @g@ yield the same outputs.

941+--

942+-- @

943+-- 'equalizer' r r == 'id'

944+-- 'equalizer' ('point' True) ('point' False) == 'zeros'

945+-- @

946+equalizer ::

947+ ( CountableN a,

948+ FLN a a

949+ )

950+ => Relation a b -> Relation a b -> Relation a a

951+equalizer f g = id `intersection` divisionF f g

952+

953+-- | Relational conditional guard.

954+--

955+-- @

956+-- 'guard' p = 'i2' ``overriddenBy`` 'i1' `.` 'predR' p

957+-- @

958+guard ::

959+ ( Bounded b,

960+ Enum b,

961+ CountableN b,

962+ Countable b,

963+ FLN b b,

964+ FLN Bool b

965+ ) => Relation b Bool -> Relation b (Either b b)

966+guard p = conv (eitherR (predR p) (predR (negate p)))

967+

968+-- | Relational McCarthy's conditional.

969+cond ::

970+ ( Bounded b,

971+ Enum b,

972+ Countable b,

973+ CountableN b,

974+ FLN b b,

975+ FLN Bool b

976+ )

977+ => Relation b Bool -> Relation b c -> Relation b c -> Relation b c

978+cond p r s = eitherR r s . guard p

979+

980+-- | Relational domain.

981+--

982+-- For injective relations, 'domain' and 'ker'nel coincide,

983+-- since @'ker' r ``sse`` 'id'@ in such situations.

984+domain ::

985+ ( CountableN a,

986+ FLN a a

987+ ) => Relation a b -> Relation a a

988+domain r = ker r `intersection` id

989+

990+-- | Relational range.

991+--

992+-- For functions, 'range' and 'img' (image) coincide,

993+-- since @'img' f ``sse`` id@ for any @f@.

994+range ::

995+ ( CountableN b,

996+ FLN b b

997+ ) => Relation a b -> Relation b b

998+range r = img r `intersection` id

717999

7181000-- Relation pretty print

7191001

7201002-- | Relation pretty printing

721−pretty :: (KnownNat (I.Count (I.Normalize a))) => Relation a b -> String

1003+pretty :: (CountableDimsN a b) => Relation a b -> String

7221004pretty (R a) = I.pretty a

7231005

7241006-- | Relation pretty printing

725−prettyPrint :: (KnownNat (I.Count (I.Normalize a))) => Relation a b -> IO ()

1007+prettyPrint :: (CountableDimsN a b) => Relation a b -> IO ()

7261008prettyPrint (R a) = I.prettyPrint a

src/LAoP/Utils.hs+6

@@ -94,6 +94,12 @@ module LAoP.Utils

9494 coerceNat,

9595 coerceNat2,

9696 coerceNat3,

97+

98+ -- * List data type

99+ List (..),

100+

101+ -- * Category type-class

102+ Category(..)

97103 )

98104where

99105

src/LAoP/Utils/Internal.hs+70−73

@@ -1,82 +1,13 @@

1+{-# LANGUAGE TypeFamilies #-}

2+{-# LANGUAGE DeriveGeneric #-}

13{-# LANGUAGE TypeApplications #-}

24{-# LANGUAGE DataKinds #-}

35{-# LANGUAGE FlexibleInstances #-}

46{-# LANGUAGE GeneralizedNewtypeDeriving #-}

5−{-# LANGUAGE KindSignatures #-}

67{-# LANGUAGE ScopedTypeVariables #-}

89module LAoP.Utils.Internal

9− ( -- | This is an internal module and it is not meant to be imported.

10− --

11− -- Utility module that provides the 'Natural' data type.

12− -- The semantic associated with this data type is that

13− -- it's meant to be a restricted 'Int' value. For example

14− -- the type @Natural 6@ can only be instanciated with @Nat n@

15− -- where @0 <= n <= 6@. Why, You might ask, because with normal

16− -- 'Int's it is not possible to have a decent @Enum (Int, Int)@

17− -- instance. See the following probabilistic programming model as and

18− -- example:

19− --

20− -- We want to calculate the probability of the sum of two dice throws.

21− -- To do this we start by defining the sample space:

22− --

23− -- @

24− -- type SampleSpace = Int -- We think 'Int' are enough

25− --

26− -- die :: Dist Int 6

27− -- die = unifrom [1..6]

28− --

29− -- -- Promote 'Int' addition to a matrix

30− -- addM = fromF (uncurry (+)) -- Impossible

31− -- @

32− --

33− -- The last line is impossible because @(Int, Int)@ does not have

34− -- a good 'Enum' instance: @[(0, 1), (0, 2), .. (0, maxBound), (1, 0),

35− -- ..]@. And we'd like the addition matrix to be of 36 columns by 12

36− -- rows but limited to integers up to @6@!

37− --

38− -- One way to solve this issue is by defining and auxilary data type to

39− -- represent the sample space:

40− --

41− -- @

42− -- data SampleSpace = S1 | S2 | S3 | S4 | S5 | S6

43− -- deriving (Show, Eq, Enum, Bounded) -- Enum and Bounded are

44− -- important

45− -- @

46− --

47− -- And write the sample space addition function:

48− --

49− -- @

50− -- ssAdd :: SampleSpace -> SampleSpace -> Int

51− -- ssAdd a b = (fromEnum a + 1) + (fromEnum b + 1)

52− -- @

53− --

54− -- And then promote that function to matrix and everything is alright:

55− --

56− -- @

57− -- ssAddM = fromF' (uncurry ssAdd)

58− --

59− -- dieSumProb = ssAddM `comp` (khatri die die)

60− -- @

61− --

62− -- This is a nice solution for small sample spaces. But for larger ones

63− -- it is not feasible to write a data type with hundreds of constructors

64− -- and then write manipulation functions that need to deal with them.

65− -- To mitigate this limitation the 'Natural' type comes a long way and

66− -- allows one to model the sample in an easier way. See for instance:

67− --

68− -- @

69− -- ssAdd :: Natural 6 -> Natural 6 -> Natural 12

70− -- ssAdd = coerceNat (+)

71− --

72− -- ssAddM = fromF' (uncurry sumSS)

73− --

74− -- die :: Dist (Natural 6) 6

75− -- die = uniform [nat @6 1 .. nat 6]

76− --

77− -- dieSumProb = ssAddM `comp` (khatri die die)

78− -- @

79− --

10+ (

8011 -- * 'Natural' data type

8112 Natural(..),

8213 nat,

@@ -86,19 +17,31 @@ module LAoP.Utils.Internal

8617 coerceNat,

8718 coerceNat2,

8819 coerceNat3,

20+

21+ -- * 'List' data type

22+ List (..),

23+

24+ -- * Category type class

25+ Category(..)

8926 )

9027where

9128

9229import Data.Coerce

9330import Data.Proxy

31+import Data.List

32+import Data.Maybe

9433import GHC.TypeLits

9534import Control.DeepSeq

35+import GHC.Generics

36+import Data.Kind

37+import Prelude hiding (id, (.))

38+import qualified Prelude

9639

9740-- | Wrapper around 'Int's that have a restrictive semantic associated.

9841-- A value of type @'Natural' n m@ can only be instanciated with some 'Int'

9942-- @i@ that's @n <= i <= m@.

10043newtype Natural (start :: Nat) (end :: Nat) = Nat Int

101− deriving (Show, Read, Eq, Ord, NFData)

44+ deriving (Show, Read, Eq, Ord, NFData, Generic)

10245

10346-- | Throws a runtime error if any of the operations overflows or

10447-- underflows.

@@ -197,3 +140,57 @@ instance

197140

198141 fromEnum (Left a) = fromEnum a

199142 fromEnum (Right b) = fromEnum (maxBound :: a) + fromEnum b + 1

143+

144+-- | Powerset data type.

145+--

146+-- This data type is a newtype wrapper around '[]'. This exists in order to

147+-- implement an 'Enum' and 'Bounded' instance that cannot be harmful for the outside.

148+newtype List a = L [a]

149+ deriving (Eq, Show, Read)

150+

151+powerset :: [a] -> [[a]]

152+powerset [] = [[]]

153+powerset (x:xs) = powerset xs ++ [x:ps | ps <- powerset xs]

154+

155+instance

156+ ( Enum a,

157+ Bounded a

158+ ) => Bounded (List a)

159+ where

160+ minBound = L []

161+ maxBound = L [minBound .. maxBound]

162+

163+instance

164+ ( Bounded a,

165+ Enum a,

166+ Eq a

167+ ) => Enum (List a)

168+ where

169+ toEnum i =

170+ let as = [minBound .. maxBound]

171+ in L (powerset as !! i)

172+

173+ fromEnum (L []) = 0

174+ fromEnum (L x) =

175+ let as = [minBound .. maxBound]

176+ in fromMaybe (error "Does not exist") $ elemIndex x (powerset as)

177+

178+-- | Constrained category instance

179+class Category k where

180+ type Object k o :: Constraint

181+ type Object k o = ()

182+ id :: Object k a => k a a

183+ (.) :: k b c -> k a b -> k a c

184+

185+{-# RULES

186+"identity/left" forall p .

187+ id . p = p

188+"identity/right" forall p .

189+ p . id = p

190+"association" forall p q r .

191+ (p . q) . r = p . (q . r)

192+ #-}

193+

194+instance Category (->) where

195+ id = Prelude.id

196+ (.) = (Prelude..)

stack-8.8.3.yamlnew file+1

@@ -0,0 +1 @@

1+resolver: lts-15.5

stack.yaml+1−66

@@ -1,66 +1 @@

1−# This file was automatically generated by 'stack init'

2−#

3−# Some commonly used options have been documented as comments in this file.

4−# For advanced use and comprehensive documentation of the format, please see:

5−# https://docs.haskellstack.org/en/stable/yaml_configuration/

6−

7−# Resolver to choose a 'specific' stackage snapshot or a compiler version.

8−# A snapshot resolver dictates the compiler version and the set of packages

9−# to be used for project dependencies. For example:

10−#

11−# resolver: lts-3.5

12−# resolver: nightly-2015-09-21

13−# resolver: ghc-7.10.2

14−#

15−# The location of a snapshot can be provided as a file or url. Stack assumes

16−# a snapshot provided as a file might change, whereas a url resource does not.

17−#

18−# resolver: ./custom-snapshot.yaml

19−# resolver: https://example.com/snapshots/2018-01-01.yaml

20−resolver: lts-14.18

21−

22−# User packages to be built.

23−# Various formats can be used as shown in the example below.

24−#

25−# packages:

26−# - some-directory

27−# - https://example.com/foo/bar/baz-0.0.2.tar.gz

28−# subdirs:

29−# - auto-update

30−# - wai

31−packages:

32−- .

33−# Dependency packages to be pulled from upstream that are not in the resolver.

34−# These entries can reference officially published versions as well as

35−# forks / in-progress versions pinned to a git hash. For example:

36−#

37−# extra-deps:

38−# - acme-missiles-0.3

39−# - git: https://github.com/commercialhaskell/stack.git

40−# commit: e7b331f14bcffb8367cd58fbfc8b40ec7642100a

41−#

42−# extra-deps: []

43−

44−# Override default flag values for local packages and extra-deps

45−# flags: {}

46−

47−# Extra package databases containing global packages

48−# extra-package-dbs: []

49−

50−# Control whether we use the GHC we find on the path

51−# system-ghc: true

52−#

53−# Require a specific version of stack, using version ranges

54−# require-stack-version: -any # Default

55−# require-stack-version: ">=2.1"

56−#

57−# Override the architecture used by stack, especially useful on Windows

58−# arch: i386

59−# arch: x86_64

60−#

61−# Extra directories used by stack for building

62−# extra-include-dirs: [/path/to/dir]

63−# extra-lib-dirs: [/path/to/dir]

64−#

65−# Allow a newer minor version of GHC than the snapshot specifies

66−# compiler-check: newer-minor

1+resolver: lts-14.3

stack.yaml.lock+4−4

@@ -6,7 +6,7 @@

66packages: []

77snapshots:

88- completed:

9− size: 524789

10− url: https://raw.githubusercontent.com/commercialhaskell/stackage-snapshots/master/lts/14/18.yaml

11− sha256: 646be71223e08234131c6989912e6011e01b9767bc447b6d466a35e14360bdf2

12− original: lts-14.18

9+ size: 523878

10+ url: https://raw.githubusercontent.com/commercialhaskell/stackage-snapshots/master/lts/14/3.yaml

11+ sha256: 470c46c27746a48c7c50f829efc0cf00112787a7804ee4ac7a27754658f6d92c

12+ original: lts-14.3

test/Examples/Quantum.hsnew file+31

@@ -0,0 +1,31 @@

1+{-# LANGUAGE StandaloneDeriving #-}

2+module Examples.Quantum where

4+import LAoP.Utils

5+import LAoP.Matrix.Type

6+import Data.Complex

7+import Prelude hiding (id, (.))

9+deriving instance Ord a => Ord (Complex a)

10+

11+xor :: (Bool, Bool) -> Bool

12+xor (False, b) = b

13+xor (True, b) = not b

14+

15+ker :: Num e => Matrix e a b -> Matrix e a a

16+ker m = tr m . m

17+

18+cnot :: Matrix (Complex Double) (Bool, Bool) (Bool, Bool)

19+cnot = kr fstM (fromF xor)

20+

21+ccnot :: (Num e, Ord e) => Matrix e ((Bool, Bool), Bool) ((Bool, Bool), Bool)

22+ccnot = kr fstM (fromF f)

23+ where

24+ f = xor . tp (uncurry (&&)) id

25+ tp f g (a,b) = (f a, g b)

26+

27+had :: Matrix (Complex Double) Bool Bool

28+had = (1/sqrt 2) .| fromLists [[1, 1], [1, -1]]

29+

30+bell :: Matrix (Complex Double) (Bool, Bool) (Bool, Bool)

31+bell = cnot . (had >< iden)

app/Main.hs → test/Examples/Readme.hsrenamed+61−33

@@ -1,10 +1,13 @@

1+{-# LANGUAGE GADTs #-}

12{-# LANGUAGE DeriveGeneric #-}

23{-# LANGUAGE FlexibleContexts #-}

3−{-# LANGUAGE TypeOperators #-}

44{-# LANGUAGE TypeApplications #-}

55{-# LANGUAGE DataKinds #-}

7−module Main where

7+module Examples.Readme

8+ ( exec

9+ )

10+ where

811

912import LAoP.Matrix.Type

1013import qualified LAoP.Relation as R

@@ -12,13 +15,12 @@ import LAoP.Utils

1215import LAoP.Dist

1316import GHC.TypeLits

1417import Data.Coerce

15−import GHC.Generics

16−import Control.Category hiding (id)

17−import Prelude hiding ((.))

18+import qualified GHC.Generics as G

19+import Prelude hiding (id, (.))

1820

1921-- Monty Hall Problem

2022data Outcome = Win | Lose

21− deriving (Bounded, Enum, Eq, Show, Generic)

23+ deriving (Bounded, Enum, Eq, Show, G.Generic)

2224

2325switch :: Outcome -> Outcome

2426switch Win = Lose

@@ -28,7 +30,7 @@ firstChoice :: Matrix Double () Outcome

2830firstChoice = col [1/3, 2/3]

2931

3032secondChoice :: Matrix Double Outcome Outcome

31−secondChoice = fromF' switch

33+secondChoice = fromF switch

3234

3335-- Dice sum

3436

@@ -37,7 +39,7 @@ type SS = Natural 1 6 -- Sample Space

3739sumSS :: SS -> SS -> Natural 2 12

3840sumSS = coerceNat (+)

3941

40−sumSSM = fromF' (uncurry sumSS)

42+sumSSM = fromF (uncurry sumSS)

4143

4244condition :: (Int, Int) -> Int -> Int

4345condition (fst, snd) thrd = if fst == snd

@@ -47,38 +49,64 @@ condition (fst, snd) thrd = if fst == snd

4749conditionSS :: (SS, SS) -> SS -> Natural 3 18

4850conditionSS = coerceNat2 condition

4951

50−conditionalThrows = fromF' (uncurry conditionSS) . khatri (khatri die die) die

52+conditionalThrows = fromF (uncurry conditionSS) . kr (kr die die) die

5153

5254die :: Matrix Double () SS

5355die = col $ map (const (1/6)) [nat @1 @6 1 .. nat 6]

5456

5557-- Sprinkler

58+data G = Dry | Wet

59+ deriving (Bounded, Enum, Eq, Show, G.Generic)

60+

61+data S = Off | On

62+ deriving (Bounded, Enum, Eq, Show, G.Generic)

5663

57−rain :: Matrix Double () Bool

58−rain = col [0.8, 0.2]

64+data R = No | Yes

65+ deriving (Bounded, Enum, Eq, Show, G.Generic)

66+

67+rain :: Matrix Double () R

68+rain = matrixBuilder gen

69+ where

70+ gen (_, No) = 0.8

71+ gen (_, Yes) = 0.2

5972

60−sprinkler :: Matrix Double Bool Bool

61−sprinkler = fromLists [[0.6, 0.99], [0.4, 0.01]]

73+sprinkler :: Matrix Double R S

74+sprinkler = matrixBuilder gen

75+ where

76+ gen (No, Off) = 0.6

77+ gen (No, On) = 0.4

78+ gen (Yes, Off) = 0.99

79+ gen (Yes, On) = 0.01

80+

81+grass :: Matrix Double (S, R) G

82+grass = matrixBuilder gen

83+ where

84+ gen ((Off, No), Dry) = 1

85+ gen ((Off, Yes), Dry) = 0.2

86+ gen ((On, No), Dry) = 0.1

87+ gen ((On, Yes), Dry) = 0.01

88+ gen ((Off, No), Wet) = 0

89+ gen ((Off, Yes), Wet) = 0.8

90+ gen ((On, No), Wet) = 0.9

91+ gen ((On, Yes), Wet) = 0.99

6292

63−grass :: Matrix Double (Bool, Bool) Bool

64−grass = fromLists [[1, 0.2, 0.1, 0.01], [0, 0.8, 0.9, 0.99]]

93+tag f = kr f id

6594

66−state :: Matrix Double () (Bool, (Bool, Bool))

67−state = khatri grass identity . khatri sprinkler identity . rain

95+state g s r = tag g . tag s . r

6896

69−grass_wet :: Matrix Double (Bool, (Bool, Bool)) One

70−grass_wet = row [0,1] . kp1

97+grass_wet :: Matrix Double () (G, (S, R)) -> Matrix Double One One

98+grass_wet state = row [0,1] . fstM . state

7199

72−rainning :: Matrix Double (Bool, (Bool, Bool)) One

73−rainning = row [0,1] . kp2 . kp2

100+rainning :: Matrix Double (G, (S, R)) One

101+rainning = row [0,1] . sndM . sndM

74102

75103-- Alcuin Puzzle

76104

77105data Being = Farmer | Fox | Goose | Beans

78− deriving (Bounded, Enum, Eq, Show, Generic)

106+ deriving (Bounded, Enum, Eq, Show, G.Generic)

79107

80108data Bank = LeftB | RightB

81− deriving (Bounded, Enum, Eq, Show, Generic)

109+ deriving (Bounded, Enum, Eq, Show, G.Generic)

82110

83111eats :: Being -> Being -> Bool

84112eats Fox Goose = True

@@ -93,21 +121,21 @@ cross LeftB = RightB

93121cross RightB = LeftB

94122

95123crossR :: R.Relation Bank Bank

96−crossR = R.fromF' cross

124+crossR = R.fromF cross

97125

98126-- | Initial state, everyone in the left bank

99127locationLeft :: Being -> Bank

100128locationLeft _ = LeftB

101129

102130locationLeftR :: R.Relation Being Bank

103−locationLeftR = R.fromF' locationLeft

131+locationLeftR = R.fromF locationLeft

104132

105133-- | Initial state, everyone in the right bank

106134locationRight :: Being -> Bank

107135locationRight _ = RightB

108136

109137locationRightR :: R.Relation Being Bank

110−locationRightR = R.fromF' locationRight

138+locationRightR = R.fromF locationRight

111139

112140-- Properties

113141

@@ -124,7 +152,7 @@ inv :: R.Relation Being Bank -> Bool

124152inv w = (w `R.comp` canEat w) `R.sse` (w `R.comp` farmer)

125153 where

126154 farmer :: R.Relation Being Being

127− farmer = R.fromF' (const Farmer)

155+ farmer = R.fromF (const Farmer)

128156

129157-- Arbitrary state

130158bankState :: Being -> Bank -> Bool

@@ -138,19 +166,19 @@ bankStateR :: R.Relation Being Bank

138166bankStateR = R.toRel bankState

139167

140168-- Main

141−main :: IO ()

142−main = do

169+exec :: IO ()

170+exec = do

143171 putStrLn "Monty Hall Problem solution:"

144172 prettyPrint (secondChoice . firstChoice)

145173 putStrLn "\n Sum of dices probability:"

146− prettyPrint (sumSSM `comp` khatri die die)

174+ prettyPrint (sumSSM . kr die die)

147175 putStrLn "\n Conditional dice throw:"

148176 prettyPrint conditionalThrows

149177 putStrLn "\n Checking that the last result is indeed a distribution: "

150− prettyPrint (bang . sumSSM . khatri die die)

178+ prettyPrint (bang . sumSSM . kr die die)

151179 putStrLn "\n Probability of grass being wet:"

152− prettyPrint (grass_wet . state)

180+ prettyPrint (grass_wet (state grass sprinkler rain))

153181 putStrLn "\n Probability of rain:"

154− prettyPrint (rainning . state)

182+ prettyPrint (rainning . state grass sprinkler rain)

155183 putStrLn "\n Is the arbitrary state a valid state? (Alcuin Puzzle)"

156184 print (inv bankStateR)

test/Examples/Spreadsheets.hsnew file+47

@@ -0,0 +1,47 @@

1+{-# LANGUAGE DeriveGeneric #-}

3+module Examples.Spreadsheets

5+import LAoP.Utils

6+import LAoP.Matrix.Type

7+import GHC.Generics

8+import Prelude hiding (id, (.))

10+data Student = Student1 | Student2 | Student3 | Student4

11+ deriving (Eq, Show, Enum, Bounded, Generic)

12+

13+data Question = Question1 | Question2 | Question3 | Question4

14+ deriving (Eq, Show, Enum, Bounded, Generic)

15+

16+data Results = Exam | Test | Final

17+ deriving (Eq, Show, Enum, Bounded, Generic)

18+

19+test :: Matrix Float One Results

20+test = point Test

21+

22+exam :: Matrix Float One Results

23+exam = point Exam

24+

25+final :: Matrix Float One Results

26+final = point Final

27+

28+m :: Matrix Float Question Student

29+m = fromLists [[95, 90, 100, 40], [20, 90, 90, 0], [30, 20, 95, 0], [50, 80, 100, 30]]

30+

31+w :: Matrix Float Question One

32+w = fromLists [[0.2, 0.3, 0.2, 0.3]]

33+

34+xls :: Matrix Float Question One

35+ -> Matrix Float Question Student

36+ -> Matrix Float Student One

37+ -> Matrix Float (Either Question Results) (Either One Student)

38+xls w m t = join (fork w m) (fork zeros r)

39+ where

40+ rExam = m . tr w

41+ rTest = tr t

42+ rFinal = rTest `maxPW` rExam

43+ r = (rExam . tr exam) + (rTest . tr test) + (rFinal . tr final)

44+

45+-- | Overloaded, point-wise 'max' function

46+maxPW :: Ord e => Matrix e a b -> Matrix e a b -> Matrix e a b

47+maxPW = zipWithM max

test/Spec.hs+7−1

@@ -1,2 +1,8 @@

1+module Main (main) where

3+import qualified Examples.Readme as RD

15main :: IO ()

2−main = putStrLn "Test suite not yet implemented"

6+main = do

7+ putStrLn ("Testing if README works" :: String)

8+ RD.exec