git.iko.soy/laop
on dfbd1d5 help sign in
eea6231
swap
0 ahead, 79 behind
29 files changed+1339−2869
since splitsnapshots
unifiedsplit
.github/workflows/ci.yml−43 .gitignore+2−54 .travis.yml−47 CHANGELOG.md−17 ChangeLog.md+3 LICENSE+26−17 README.md+24−107 Setup.hs+2 app/Main.hs+87 appveyor.yml−34 benchmark/Main.hs−175 laop.cabal−89 package.yaml+48 src/LAoP/Dist.hs−10 src/LAoP/Dist/Internal.hs+36−87 src/LAoP/Matrix/Internal.hs+412−487 src/LAoP/Matrix/Nat.hs+187−194 src/LAoP/Matrix/Type.hs+232−292 src/LAoP/Relation.hs+6−80 src/LAoP/Relation/Internal.hs+129−761 src/LAoP/Utils.hs−6 src/LAoP/Utils/Internal.hs+74−94 stack-8.8.3.yaml−1 stack.yaml+66−1 stack.yaml.lock+4−4 test/Examples/Quantum.hs−31 test/Examples/Readme.hs−184 test/Examples/Spreadsheets.hs−47 test/Spec.hs+1−7
.github/workflows/ci.ymldeleted−43
@@ -1,43 +0,0 @@
1−name: CI
2−
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]
8−
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+2−54
@@ -1,55 +1,3 @@
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
251.stack-work/
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
2+laop.cabal
3+*~
.travis.ymldeleted−47
@@ -1,47 +0,0 @@
1−sudo: true
2−language: haskell
3−
4−git:
5− depth: 5
6−
7−cabal: "3.0"
8−
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.mddeleted−17
@@ -1,17 +0,0 @@
1−# Changelog
2−
3−`laop` uses [PVP Versioning][1].
4−The changelog is available [on GitHub][2].
5−
6−## 0.1.1.1
7−
8−* Bump base version to work with cabal
9−
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.mdnew file+3
@@ -0,0 +1,3 @@
1+# Changelog for laop
2+
3+## Unreleased changes
LICENSE+26−17
@@ -1,21 +1,30 @@
1−MIT License
1+Copyright Armando Santos (c) 2019
22
3−Copyright (c) 2020 Armando Santos
3+All rights reserved.
44
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:
5+Redistribution and use in source and binary forms, with or without
6+modification, are permitted provided that the following conditions are met:
117
12−The above copyright notice and this permission notice shall be included in all
13−copies or substantial portions of the Software.
8+ * Redistributions of source code must retain the above copyright
9+ notice, this list of conditions and the following disclaimer.
1410
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.
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.
README.md+24−107
@@ -1,11 +1,5 @@
11# laop - Linear Algebra of Programming library
22
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)
8−
93The LAoP discipline generalises relations and functions treating them as
104Boolean matrices and in turn consider these as arrows.
115
@@ -16,38 +10,33 @@ motivation behind the library, the underlying theory, and implementation details
1610This module offers many of the combinators mentioned in the work of
1711[Macedo (2012)](https://repositorium.sdum.uminho.pt/handle/1822/22894) and [Oliveira (2012)](https://pdfs.semanticscholar.org/ccf5/27fa9179081223bffe8067edd81948644fc0.pdf).
1812
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.
13+See the candidate package in hackage [here](https://hackage.haskell.org/package/laop-0.1.0.0/candidate)
2214
2315## Features
2416
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).
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.
5140
5241## Notes
5342
@@ -129,73 +118,6 @@ grass_wet = row [0,1] . kp1
129118rainning :: Matrix Double (Bool, (Bool, Bool)) One
130119rainning = row [0,1] . kp2 . kp2
131120
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−
199121main :: IO ()
200122main = do
201123 putStrLn "Monty Hall Problem solution:"
@@ -210,8 +132,6 @@ main = do
210132 prettyPrint (grass_wet . state)
211133 putStrLn "\n Probability of rain:"
212134 prettyPrint (rainning . state)
213− putStrLn "\n Is the arbitrary state a valid state? (Alcuin Puzzle)"
214− print (inv bankStateR)
215135```
216136
217137```Shell
@@ -270,7 +190,4 @@ Monty Hall Problem solution:
270190┌ ┐
271191│ 0.2 │
272192└ ┘
273−
274−Is the arbitrary state a valid state? (Alcuin Puzzle)
275−False
276193```
Setup.hsnew file+2
@@ -0,0 +1,2 @@
1+import Distribution.Simple
2+main = defaultMain
app/Main.hsnew file+87
@@ -0,0 +1,87 @@
1+{-# LANGUAGE DeriveGeneric #-}
2+{-# LANGUAGE FlexibleContexts #-}
3+{-# LANGUAGE TypeOperators #-}
4+{-# LANGUAGE TypeApplications #-}
5+{-# LANGUAGE DataKinds #-}
6+
7+module Main where
8+
9+import LAoP.Matrix.Type
10+import LAoP.Utils
11+import LAoP.Dist
12+import GHC.TypeLits
13+import Data.Coerce
14+import GHC.Generics
15+import Control.Category hiding (id)
16+import Prelude hiding ((.))
17+
18+-- Monty Hall Problem
19+data Outcome = Win | Lose
20+ deriving (Bounded, Enum, Eq, Show, Generic)
21+
22+switch :: Outcome -> Outcome
23+switch Win = Lose
24+switch Lose = Win
25+
26+firstChoice :: Matrix Double () Outcome
27+firstChoice = col [1/3, 2/3]
28+
29+secondChoice :: Matrix Double Outcome Outcome
30+secondChoice = fromF' switch
31+
32+-- Dice sum
33+
34+type SS = Natural 1 6 -- Sample Space
35+
36+sumSS :: SS -> SS -> Natural 2 12
37+sumSS = coerceNat (+)
38+
39+sumSSM = fromF' (uncurry sumSS)
40+
41+condition :: (Int, Int) -> Int -> Int
42+condition (fst, snd) thrd = if fst == snd
43+ then fst * 3
44+ else fst + snd + thrd
45+
46+conditionSS :: (SS, SS) -> SS -> Natural 3 18
47+conditionSS = coerceNat2 condition
48+
49+conditionalThrows = fromF' (uncurry conditionSS) . khatri (khatri die die) die
50+
51+die :: Matrix Double () SS
52+die = col $ map (const (1/6)) [nat @1 @6 1 .. nat 6]
53+
54+-- Sprinkler
55+
56+rain :: Matrix Double () Bool
57+rain = col [0.8, 0.2]
58+
59+sprinkler :: Matrix Double Bool Bool
60+sprinkler = fromLists [[0.6, 0.99], [0.4, 0.01]]
61+
62+grass :: Matrix Double (Bool, Bool) Bool
63+grass = fromLists [[1, 0.2, 0.1, 0.01], [0, 0.8, 0.9, 0.99]]
64+
65+state :: Matrix Double () (Bool, (Bool, Bool))
66+state = khatri grass identity . khatri sprinkler identity . rain
67+
68+grass_wet :: Matrix Double (Bool, (Bool, Bool)) One
69+grass_wet = row [0,1] . kp1
70+
71+rainning :: Matrix Double (Bool, (Bool, Bool)) One
72+rainning = row [0,1] . kp2 . kp2
73+
74+main :: IO ()
75+main = do
76+ putStrLn "Monty Hall Problem solution:"
77+ prettyPrint (secondChoice . firstChoice)
78+ putStrLn "\n Sum of dices probability:"
79+ prettyPrint (sumSSM `comp` khatri die die)
80+ putStrLn "\n Conditional dice throw:"
81+ prettyPrint conditionalThrows
82+ putStrLn "\n Checking that the last result is indeed a distribution: "
83+ prettyPrint (bang . sumSSM . khatri die die)
84+ putStrLn "\n Probability of grass being wet:"
85+ prettyPrint (grass_wet . state)
86+ putStrLn "\n Probability of rain:"
87+ prettyPrint (rainning . state)
appveyor.ymldeleted−34
@@ -1,34 +0,0 @@
1−clone_folder: "c:\\WORK"
2−clone_depth: 5
3−
4−# Do not build feature branch with open Pull Requests
5−skip_branch_with_pr: true
6−
7−platform:
8− - x86_64
9−
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.hsdeleted−175
@@ -1,175 +0,0 @@
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.cabaldeleted−89
@@ -1,89 +0,0 @@
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.yamlnew file+48
@@ -0,0 +1,48 @@
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,14 +36,6 @@ 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−
4739 -- * Functor instance equivalent functions
4840 fmapD,
4941
@@ -53,8 +45,6 @@ module LAoP.Dist
5345
5446 -- * Selective equivalent functions
5547 selectD,
56− branchD,
57− ifD,
5848
5949 -- * Monad equivalent functions
6050 returnD,
src/LAoP/Dist/Internal.hs+36−87
@@ -1,5 +1,3 @@
1−{-# LANGUAGE DerivingVia #-}
2−{-# LANGUAGE ConstraintKinds #-}
31{-# LANGUAGE GADTs #-}
42{-# LANGUAGE AllowAmbiguousTypes #-}
53{-# LANGUAGE TypeApplications #-}
@@ -10,27 +8,18 @@
108{-# LANGUAGE RankNTypes #-}
119
1210module LAoP.Dist.Internal
13− (
11+ (
1412 Dist(..),
1513 Prob,
1614
17− Countable,
18− CountableN,
19− CountableDimsN,
20− FLN,
21− Liftable,
22− TrivialP,
23−
2415 fmapD,
2516 unitD,
2617 multD,
2718 selectD,
28− branchD,
29− ifD,
3019 returnD,
3120 bindD,
3221 (??),
33−
22+
3423 choose,
3524 shape,
3625 linear,
@@ -43,15 +32,11 @@ module LAoP.Dist.Internal
4332 )
4433 where
4534
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
35+import LAoP.Matrix.Type
4936import LAoP.Utils
5037import GHC.TypeLits
5138import Data.Proxy
5239import Data.List (sortBy)
53−import Control.DeepSeq
54−import Data.Bool
5540
5641-- | Type synonym for probability value
5742type Prob = Double
@@ -59,21 +44,17 @@ type Prob = Double
5944-- | Type synonym for column vector matrices. This represents a probability
6045-- distribution.
6146newtype 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)
7147
7248-- | Functor instance
7349fmapD ::
74− ( Liftable a b,
75− CountableDimsN a b,
76− FLN b a
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)
7758 )
7859 =>
7960 (a -> b) -> Dist a -> Dist b
@@ -85,58 +66,26 @@ unitD = D (one 1)
8566
8667-- | Applicative/Monoidal instance 'mult' function
8768multD ::
88− ( CountableDimsN a b,
89− CountableN (a, b),
90− FLN (a, b) a,
91− FLN (a, b) b,
92− TrivialP a b
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)
9375 ) => Dist a -> Dist b -> Dist (a, b)
94−multD (D a) (D b) = D (kr a b)
76+multD (D a) (D b) = D (khatri a b)
9577
9678-- | Selective instance function
9779selectD ::
98− ( FLN b b,
99− CountableN b
80+ ( Normalize (Either a b) ~ Either (Normalize a) (Normalize b),
81+ FromLists Prob (Normalize b) (Normalize b),
82+ KnownNat (Count (Normalize b))
10083 ) => Dist (Either a b) -> Matrix Prob a b -> Dist b
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
84+selectD (D d) m = D (junc m identity `comp` d)
85+
13786
13887-- | Monad instance 'return' function
139−returnD :: forall a . (Enum a, FLN () a, Countable a) => a -> Dist a
88+returnD :: forall a . (Enum a, FromLists Prob () (Normalize a), KnownNat (Count a)) => a -> Dist a
14089returnD a = D (col l)
14190 where
14291 i = fromInteger $ natVal (Proxy :: Proxy (Count a))
@@ -150,8 +99,8 @@ bindD (D d) m = D (m `comp` d)
15099-- | Extract probabilities given an Event.
151100(??) ::
152101 ( Enum a,
153− Countable a,
154− FLN () a
102+ KnownNat (Count a),
103+ FromLists Prob () (Normalize a)
155104 ) => (a -> Bool) -> Dist a -> Prob
156105(??) p d =
157106 let l = toValues d
@@ -161,11 +110,11 @@ bindD (D d) m = D (m `comp` d)
161110-- Distribution Construction
162111
163112-- | Constructs a Bernoulli distribution
164−choose :: (FLN () a) => Prob -> Dist a
113+choose :: (FromLists Prob () (Normalize a)) => Prob -> Dist a
165114choose prob = D (col [prob, 1 - prob])
166115
167116-- | Creates a distribution given a shape function
168−shape :: (FLN () a) => (Prob -> Prob) -> [a] -> Dist a
117+shape :: (FromLists Prob () (Normalize a)) => (Prob -> Prob) -> [a] -> Dist a
169118shape _ [] = error "Probability.shape: empty list"
170119shape f xs =
171120 let incr = 1 / fromIntegral (length xs - 1)
@@ -173,23 +122,23 @@ shape f xs =
173122 in fromFreqs (zip xs ps)
174123
175124-- | Constructs a Linear distribution
176−linear :: (FLN () a) => [a] -> Dist a
125+linear :: (FromLists Prob () (Normalize a)) => [a] -> Dist a
177126linear = shape id
178127
179128-- | Constructs an Uniform distribution
180−uniform :: (FLN () a) => [a] -> Dist a
129+uniform :: (FromLists Prob () (Normalize a)) => [a] -> Dist a
181130uniform = shape (const 1)
182131
183132-- | Constructs an Negative Exponential distribution
184−negExp :: (FLN () a) => [a] -> Dist a
133+negExp :: (FromLists Prob () (Normalize a)) => [a] -> Dist a
185134negExp = shape (\x -> exp (-x))
186135
187136-- | Constructs an Normal distribution
188−normal :: (FLN () a) => [a] -> Dist a
137+normal :: (FromLists Prob () (Normalize a)) => [a] -> Dist a
189138normal = shape (normalCurve 0.5 0.5)
190139
191140-- | Transforms a 'Dist' into a list of pairs.
192−toValues :: forall a . (Enum a, Countable a, FLN () a) => Dist a -> [(a, Prob)]
141+toValues :: forall a . (Enum a, KnownNat (Count a), FromLists Prob () (Normalize a)) => Dist a -> [(a, Prob)]
193142toValues (D d) =
194143 let rows = fromInteger (natVal (Proxy :: Proxy (Count a)))
195144 probs = toList d
@@ -197,7 +146,7 @@ toValues (D d) =
197146 in res
198147
199148-- | Pretty a distribution
200−prettyDist :: forall a. (Show a, Enum a, Countable a, FLN () a) => Dist a -> String
149+prettyDist :: forall a. (Show a, Enum a, KnownNat (Count a), FromLists Prob () (Normalize a)) => Dist a -> String
201150prettyDist d =
202151 let values = sortBy (\(a, p1) (b, p2) -> compare p2 p1) (toValues @a d)
203152 w = maximum (map (length . show . fst) values)
@@ -209,12 +158,12 @@ prettyDist d =
209158 showR n x = show x ++ " "
210159
211160-- | Pretty Print a distribution
212−prettyPrintDist :: forall a . (Show a, Enum a, Countable a, FLN () a) => Dist a -> IO ()
161+prettyPrintDist :: forall a . (Show a, Enum a, KnownNat (Count a), FromLists Prob () (Normalize a)) => Dist a -> IO ()
213162prettyPrintDist = putStrLn . prettyDist @a
214163
215164-- Auxiliary functions
216165
217−fromFreqs :: (FLN () a) => [(a,Prob)] -> Dist a
166+fromFreqs :: (FromLists Prob () (Normalize a)) => [(a,Prob)] -> Dist a
218167fromFreqs xs = D (col (map (\(x,p) -> p/q) xs))
219168 where q = sum $ map snd xs
220169
src/LAoP/Matrix/Internal.hs+412−487
@@ -1,6 +1,3 @@
1−{-# LANGUAGE StrictData #-}
2−{-# LANGUAGE TypeFamilyDependencies #-}
3−{-# LANGUAGE ConstraintKinds #-}
41{-# LANGUAGE AllowAmbiguousTypes #-}
52{-# LANGUAGE DataKinds #-}
63{-# LANGUAGE FlexibleContexts #-}
@@ -12,6 +9,7 @@
129{-# LANGUAGE ScopedTypeVariables #-}
1310{-# LANGUAGE StandaloneDeriving #-}
1411{-# LANGUAGE TypeApplications #-}
12+{-# LANGUAGE TypeFamilies #-}
1513{-# LANGUAGE TypeOperators #-}
1614{-# LANGUAGE UndecidableInstances #-}
1715
@@ -30,7 +28,7 @@
3028-- motivation behind the library, the underlying theory, and implementation details.
3129--
3230-- This module offers many of the combinators mentioned in the work of
33−-- Macedo (2012) and Oliveira (2012).
31+-- Macedo (2012) and Oliveira (2012).
3432--
3533-- This is an Internal module and it is no supposed to be imported.
3634--
@@ -43,26 +41,17 @@ module LAoP.Matrix.Internal
4341 --
4442 -- There exists two type families that make it easier to write
4543 -- matrix dimensions: 'FromNat' and 'Count'. This approach
46− -- leads to a very straightforward implementation
47− -- of LAoP combinators.
44+ -- leads to a very straightforward implementation
45+ -- of LAoP combinators.
4846
4947 -- * Type safe matrix representation
5048 Matrix (..),
5149
52− -- * Constraint type aliases
53− Countable,
54− CountableDims,
55− CountableN,
56− CountableDimsN,
57− FL,
58− FLN,
59− Liftable,
60− Trivial,
61−
6250 -- * Primitives
51+ empty,
6352 one,
64− join,
65− fork,
53+ junc,
54+ split,
6655
6756 -- * Auxiliary type families
6857 FromNat,
@@ -75,7 +64,6 @@ module LAoP.Matrix.Internal
7564 toLists,
7665 toList,
7766 matrixBuilder,
78− matrixBuilder',
7967 row,
8068 col,
8169 zeros,
@@ -86,38 +74,28 @@ module LAoP.Matrix.Internal
8674 -- * Misc
8775 -- ** Get dimensions
8876 columns,
89− columns',
9077 rows,
91− rows',
9278
9379 -- ** Matrix Transposition
9480 tr,
9581
96− -- ** Scalar multiplication/division of matrices
97− (.|),
98− (./),
99−
10082 -- ** Selective operator
101− select,
102− branch,
83+ select,
10384
10485 -- ** McCarthy's Conditional
10586 cond,
10687
10788 -- ** Matrix "abiding"
108− abideJF,
109− abideFJ,
110−
111− -- ** Zip matrices
112− zipWithM,
89+ abideJS,
90+ abideSJ,
11391
11492 -- * Biproduct approach
115− -- ** Fork
93+ -- ** Split
11694 (===),
11795 -- *** Projections
11896 p1,
11997 p2,
120− -- ** Join
98+ -- ** Junc
12199 (|||),
122100 -- *** Injections
123101 i1,
@@ -130,13 +108,12 @@ module LAoP.Matrix.Internal
130108
131109 -- | Note that given the restrictions imposed it is not possible to
132110 -- implement the standard type classes present in standard Haskell.
133−
134111 -- *** Matrix pairing projections
135− fstM,
136− sndM,
112+ kp1,
113+ kp2,
137114
138115 -- *** Matrix pairing
139− kr,
116+ khatri,
140117
141118 -- * Matrix composition and lifting
142119
@@ -144,10 +121,10 @@ module LAoP.Matrix.Internal
144121
145122 -- | Note that given the restrictions imposed it is not possible to
146123 -- implement the standard type classes present in standard Haskell.
147− iden,
124+ identity,
148125 comp,
149− fromF',
150126 fromF,
127+ fromF',
151128
152129 -- * Matrix printing
153130 pretty,
@@ -157,39 +134,33 @@ module LAoP.Matrix.Internal
157134 toBool,
158135 fromBool,
159136 compRel,
160− divR,
161− divL,
162− divS,
163137 fromFRel,
164138 fromFRel',
165− toRel,
166− negateM,
167139 orM,
168140 andM,
169141 subM
170142 )
171143 where
172144
173−import LAoP.Utils.Internal
145+import LAoP.Utils
174146import Data.Bool
175147import Data.Kind
176148import Data.List
177−import Data.Maybe
178149import Data.Proxy
179−import Data.Typeable
180150import Data.Void
181151import GHC.TypeLits
182152import Data.Type.Equality
183153import GHC.Generics
184154import Control.DeepSeq
185−import Prelude hiding (id, (.))
186−import qualified Prelude (id, (.))
155+import Control.Category
156+import Prelude hiding ((.))
187157
188158-- | LAoP (Linear Algebra of Programming) Inductive Matrix definition.
189159data Matrix e cols rows where
160+ Empty :: Matrix e Void Void
190161 One :: e -> Matrix e () ()
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)
162+ Junc :: Matrix e a rows -> Matrix e b rows -> Matrix e (Either a b) rows
163+ Split :: Matrix e cols a -> Matrix e cols b -> Matrix e cols (Either a b)
193164
194165deriving instance (Show e) => Show (Matrix e cols rows)
195166
@@ -199,214 +170,221 @@ deriving instance (Show e) => Show (Matrix e cols rows)
199170-- 'Generic' instance.
200171type family Count (d :: Type) :: Nat where
201172 Count (Natural n m) = (m - n) + 1
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)
173+ Count (Either a b) = (+) (Count a) (Count b)
174+ Count (a, b) = (*) (Count a) (Count b)
175+ Count (a -> b) = (^) (Count b) (Count a)
206176 -- Generics
207− Count (M1 _ _ f p) = Count (f p)
208− Count (K1 _ _ _) = 1
209− Count (V1 _) = 0
210− Count (U1 _) = 1
177+ Count (M1 _ _ f p) = Count (f p)
178+ Count (K1 _ _ _) = 1
179+ Count (V1 _) = 0
180+ Count (U1 _) = 1
211181 Count ((:*:) a b p) = Count (a p) * Count (b p)
212182 Count ((:+:) a b p) = Count (a p) + Count (b p)
213− Count d = Count (Rep d R)
183+ Count d = Count (Rep d R)
214184
215185-- | Type family that computes of a given type dimension from a given natural
216186--
217187-- Thanks to Li-Yao Xia this type family is super fast.
218188type family FromNat (n :: Nat) :: Type where
189+ FromNat 0 = Void
219190 FromNat 1 = ()
220191 FromNat n = FromNat' (Mod n 2 == 0) (FromNat (Div n 2))
221192
222193type family FromNat' (b :: Bool) (m :: Type) :: Type where
223− FromNat' 'True m = Either m m
194+ FromNat' 'True m = Either m m
224195 FromNat' 'False m = Either () (Either m m)
225196
226197-- | Type family that normalizes the representation of a given data
227198-- structure
228199type family Normalize (d :: Type) :: Type where
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.
200+ Normalize d = FromNat (Count d)
201+
202+-- | It isn't possible to implement the 'id' function so it's
203+-- implementation is 'undefined'. However 'comp' can be and this partial
204+-- class implementation exists just to make the code more readable.
205+--
206+-- Please use 'identity' instead.
244207instance (Num e) => Category (Matrix e) where
245− type Object (Matrix e) a = (FL a a, Countable a)
246− id = iden
247− (.) = comp
208+ id = undefined
209+ (.) = comp
248210
249211instance NFData e => NFData (Matrix e cols rows) where
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
212+ rnf Empty = ()
213+ rnf (One e) = rnf e
214+ rnf (Junc a b) = rnf a `seq` rnf b
215+ rnf (Split a b) = rnf a `seq` rnf b
253216
254217instance Eq e => Eq (Matrix e cols rows) where
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
218+ Empty == Empty = True
219+ (One a) == (One b) = a == b
220+ (Junc a b) == (Junc c d) = a == c && b == d
221+ (Split a b) == (Split c d) = a == c && b == d
222+ x@(Split _ _) == y@(Junc _ _) = x == abideJS y
223+ x@(Junc _ _) == y@(Split _ _) = abideJS x == y
260224
261225instance Num e => Num (Matrix e cols rows) where
262− a + b = zipWithM (+) a b
263−
264− a - b = zipWithM (-) a b
265−
266− a * b = zipWithM (*) a b
267226
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)
227+ Empty + Empty = Empty
228+ (One a) + (One b) = One (a + b)
229+ (Junc a b) + (Junc c d) = Junc (a + c) (b + d)
230+ (Split a b) + (Split c d) = Split (a + c) (b + d)
231+ x@(Split _ _) + y@(Junc _ _) = x + abideJS y
232+ x@(Junc _ _) + y@(Split _ _) = abideJS x + y
233+
234+ Empty - Empty = Empty
235+ (One a) - (One b) = One (a - b)
236+ (Junc a b) - (Junc c d) = Junc (a - c) (b - d)
237+ (Split a b) - (Split c d) = Split (a - c) (b - d)
238+ x@(Split _ _) - y@(Junc _ _) = x - abideJS y
239+ x@(Junc _ _) - y@(Split _ _) = abideJS x - y
240+
241+ Empty * Empty = Empty
242+ (One a) * (One b) = One (a * b)
243+ (Junc a b) * (Junc c d) = Junc (a * c) (b * d)
244+ (Split a b) * (Split c d) = Split (a * c) (b * d)
245+ x@(Split _ _) * y@(Junc _ _) = x * abideJS y
246+ x@(Junc _ _) * y@(Split _ _) = abideJS x * y
247+
248+ abs Empty = Empty
249+ abs (One a) = One (abs a)
250+ abs (Junc a b) = Junc (abs a) (abs b)
251+ abs (Split a b) = Split (abs a) (abs b)
252+
253+ signum Empty = Empty
254+ signum (One a) = One (signum a)
255+ signum (Junc a b) = Junc (signum a) (signum b)
256+ signum (Split a b) = Split (signum a) (signum b)
275257
276258instance Ord e => Ord (Matrix e cols rows) where
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
259+ Empty <= Empty = True
260+ (One a) <= (One b) = a <= b
261+ (Junc a b) <= (Junc c d) = (a <= c) && (b <= d)
262+ (Split a b) <= (Split c d) = (a <= c) && (b <= d)
263+ x@(Split _ _) <= y@(Junc _ _) = x <= abideJS y
264+ x@(Junc _ _) <= y@(Split _ _) = abideJS x <= y
282265
283266-- Primitives
284267
268+-- | Empty matrix constructor
269+empty :: Matrix e Void Void
270+empty = Empty
271+
285272-- | Unit matrix constructor
286273one :: e -> Matrix e () ()
287274one = One
288275
289−-- | Matrix 'Join' constructor
290−join :: Matrix e a rows -> Matrix e b rows -> Matrix e (Either a b) rows
291−join = Join
276+-- | Matrix 'Junc' constructor
277+junc :: Matrix e a rows -> Matrix e b rows -> Matrix e (Either a b) rows
278+junc = Junc
292279
293280infixl 3 |||
294281
295−-- | Matrix 'Join' constructor
282+-- | Matrix 'Junc' constructor
296283(|||) :: Matrix e a rows -> Matrix e b rows -> Matrix e (Either a b) rows
297−(|||) = Join
284+(|||) = Junc
298285
299−-- | Matrix 'Fork' constructor
300−fork :: Matrix e cols a -> Matrix e cols b -> Matrix e cols (Either a b)
301−fork = Fork
286+-- | Matrix 'Split' constructor
287+split :: Matrix e cols a -> Matrix e cols b -> Matrix e cols (Either a b)
288+split = Split
302289
303290infixl 2 ===
304291
305−-- | Matrix 'Fork' constructor
292+-- | Matrix 'Split' constructor
306293(===) :: Matrix e cols a -> Matrix e cols b -> Matrix e cols (Either a b)
307−(===) = Fork
294+(===) = Split
308295
309296-- Construction
310297
311298-- | Type class for defining the 'fromList' conversion function.
312299--
313300-- Given that it is not possible to branch on types at the term level type
314−-- classes are needed very much like an inductive definition but on types.
315−class FromLists cols rows where
301+-- classes are needed bery much like an inductive definition but on types.
302+class FromLists e cols rows where
316303 -- | Build a matrix out of a list of list of elements. Throws a runtime
317304 -- error if the dimensions do not match.
318305 fromLists :: [[e]] -> Matrix e cols rows
319306
320−instance FromLists () () where
307+instance FromLists e Void Void where
308+ fromLists [] = Empty
309+ fromLists _ = error "Wrong dimensions"
310+
311+instance {-# OVERLAPPING #-} FromLists e () () where
321312 fromLists [[e]] = One e
322313 fromLists _ = error "Wrong dimensions"
323314
324−instance (FromLists cols ()) => FromLists (Either () cols) () where
325− fromLists [h : t] = Join (One h) (fromLists [t])
315+instance {-# OVERLAPPING #-} (FromLists e cols ()) => FromLists e (Either () cols) () where
316+ fromLists [h : t] = Junc (One h) (fromLists [t])
326317 fromLists _ = error "Wrong dimensions"
327318
328−instance {-# OVERLAPPABLE #-}
329− (FromLists a (), FromLists b (), Countable a) => FromLists (Either a b) () where
330− fromLists [l] =
319+instance {-# OVERLAPPABLE #-} (FromLists e a (), FromLists e b (), KnownNat (Count a)) => FromLists e (Either a b) () where
320+ fromLists [l] =
331321 let rowsA = fromInteger (natVal (Proxy :: Proxy (Count a)))
332− in Join (fromLists [take rowsA l]) (fromLists [drop rowsA l])
322+ in Junc (fromLists [take rowsA l]) (fromLists [drop rowsA l])
333323 fromLists _ = error "Wrong dimensions"
334324
335−instance (FromLists () rows) => FromLists () (Either () rows) where
336− fromLists ([h] : t) = Fork (One h) (fromLists t)
325+instance {-# OVERLAPPING #-} (FromLists e () rows) => FromLists e () (Either () rows) where
326+ fromLists ([h] : t) = Split (One h) (fromLists t)
337327 fromLists _ = error "Wrong dimensions"
338328
339−instance {-# OVERLAPPABLE #-}
340− (FromLists () a, FromLists () b, Countable a) => FromLists () (Either a b) where
341− fromLists l@([_] : _) =
329+instance {-# OVERLAPPABLE #-} (FromLists e () a, FromLists e () b, KnownNat (Count a)) => FromLists e () (Either a b) where
330+ fromLists l@([_] : _) =
342331 let rowsA = fromInteger (natVal (Proxy :: Proxy (Count a)))
343− in Fork (fromLists (take rowsA l)) (fromLists (drop rowsA l))
332+ in Split (fromLists (take rowsA l)) (fromLists (drop rowsA l))
344333 fromLists _ = error "Wrong dimensions"
345334
346−instance (FromLists (Either a b) c, FromLists (Either a b) d, Countable c)
347− => FromLists (Either a b) (Either c d) where
335+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
348336 fromLists l@(h : t) =
349337 let lh = length h
350338 rowsC = fromInteger (natVal (Proxy :: Proxy (Count c)))
351− condition = all ((== lh) . length) t
339+ condition = all (== lh) (map length t)
352340 in if lh > 0 && condition
353− then Fork (fromLists (take rowsC l)) (fromLists (drop rowsC l))
341+ then Split (fromLists (take rowsC l)) (fromLists (drop rowsC l))
354342 else error "Not all rows have the same length"
355343
356344-- | Matrix builder function. Constructs a matrix provided with
357−-- a construction function that operates with indices.
358−matrixBuilder' ::
345+-- a construction function.
346+matrixBuilder ::
359347 forall e cols rows.
360− ( FL cols rows,
361− CountableDims cols rows
362− ) => ((Int, Int) -> e) -> Matrix e cols rows
363−matrixBuilder' f =
348+ ( FromLists e cols rows,
349+ KnownNat (Count cols),
350+ KnownNat (Count rows)
351+ ) =>
352+ ((Int, Int) -> e) ->
353+ Matrix e cols rows
354+matrixBuilder f =
364355 let c = fromInteger $ natVal (Proxy :: Proxy (Count cols))
365356 r = fromInteger $ natVal (Proxy :: Proxy (Count rows))
366357 positions = [(a, b) | a <- [0 .. (r - 1)], b <- [0 .. (c - 1)]]
367358 in fromLists . map (map f) . groupBy (\(x, _) (w, _) -> x == w) $ positions
368359
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−
389360-- | Constructs a column vector matrix
390−col :: (FL () rows) => [e] -> Matrix e () rows
361+col :: (FromLists e () rows) => [e] -> Matrix e () rows
391362col = fromLists . map (: [])
392363
393364-- | Constructs a row vector matrix
394−row :: (FL cols ()) => [e] -> Matrix e cols ()
365+row :: (FromLists e cols ()) => [e] -> Matrix e cols ()
395366row = fromLists . (: [])
396367
397368-- | Lifts functions to matrices with arbitrary dimensions.
398369--
399370-- NOTE: Be careful to not ask for a matrix bigger than the cardinality of
400371-- types @a@ or @b@ allows.
401−fromF' ::
372+fromF ::
402373 forall a b cols rows e.
403− ( Liftable e a b,
404− CountableDims cols rows,
405− FL rows cols
374+ ( Bounded a,
375+ Bounded b,
376+ Enum a,
377+ Enum b,
378+ Eq b,
379+ Num e,
380+ Ord e,
381+ KnownNat (Count cols),
382+ KnownNat (Count rows),
383+ FromLists e rows cols
406384 ) =>
407385 (a -> b) ->
408386 Matrix e cols rows
409−fromF' f =
387+fromF f =
410388 let minA = minBound @a
411389 maxA = maxBound @a
412390 minB = minBound @b
@@ -416,8 +394,8 @@ fromF' f =
416394 elementsA = take ccols [minA .. maxA]
417395 elementsB = take rrows [minB .. maxB]
418396 combinations = (,) <$> elementsA <*> elementsB
419− combAp = map snd . sort . map (\(a, b) -> if f a == b
420− then ((fromEnum a, fromEnum b), 1)
397+ combAp = map snd . sort . map (\(a, b) -> if f a == b
398+ then ((fromEnum a, fromEnum b), 1)
421399 else ((fromEnum a, fromEnum b), 0)) $ combinations
422400 mList = buildList combAp rrows
423401 in tr $ fromLists mList
@@ -427,23 +405,48 @@ fromF' f =
427405
428406-- | Lifts functions to matrices with dimensions matching @a@ and @b@
429407-- cardinality's.
430−fromF ::
408+fromF' ::
431409 forall a b e.
432− ( Liftable e a b,
433− CountableDimsN a b,
434− FLN b a
410+ ( Bounded a,
411+ Bounded b,
412+ Enum a,
413+ Enum b,
414+ Eq b,
415+ Num e,
416+ Ord e,
417+ KnownNat (Count (Normalize a)),
418+ KnownNat (Count (Normalize b)),
419+ FromLists e (Normalize b) (Normalize a)
435420 ) =>
436421 (a -> b) ->
437422 Matrix e (Normalize a) (Normalize b)
438−fromF = fromF'
423+fromF' f =
424+ let minA = minBound @a
425+ maxA = maxBound @a
426+ minB = minBound @b
427+ maxB = maxBound @b
428+ ccols = fromInteger $ natVal (Proxy :: Proxy (Count (Normalize a)))
429+ rrows = fromInteger $ natVal (Proxy :: Proxy (Count (Normalize b)))
430+ elementsA = take ccols [minA .. maxA]
431+ elementsB = take rrows [minB .. maxB]
432+ combinations = (,) <$> elementsA <*> elementsB
433+ combAp = map snd . sort . map (\(a, b) -> if f a == b
434+ then ((fromEnum a, fromEnum b), 1)
435+ else ((fromEnum a, fromEnum b), 0)) $ combinations
436+ mList = buildList combAp rrows
437+ in tr $ fromLists mList
438+ where
439+ buildList [] _ = []
440+ buildList l r = take r l : buildList (drop r l) r
439441
440442-- Conversion
441443
442444-- | Converts a matrix to a list of lists of elements.
443445toLists :: Matrix e cols rows -> [[e]]
446+toLists Empty = []
444447toLists (One e) = [[e]]
445−toLists (Fork l r) = toLists l ++ toLists r
446−toLists (Join l r) = zipWith (++) (toLists l) (toLists r)
448+toLists (Split l r) = toLists l ++ toLists r
449+toLists (Junc l r) = zipWith (++) (toLists l) (toLists r)
447450
448451-- | Converts a matrix to a list of elements.
449452toList :: Matrix e cols rows -> [e]
@@ -452,38 +455,37 @@ toList = concat . toLists
452455-- Zeros Matrix
453456
454457-- | The zero matrix. A matrix wholly filled with zeros.
455−zeros :: (Num e, FL cols rows, CountableDims cols rows) => Matrix e cols rows
456−zeros = matrixBuilder' (const 0)
458+zeros :: (Num e, FromLists e cols rows, KnownNat (Count cols), KnownNat (Count rows)) => Matrix e cols rows
459+zeros = matrixBuilder (const 0)
457460
458461-- Ones Matrix
459462
460463-- | The ones matrix. A matrix wholly filled with ones.
461464--
462465-- Also known as T (Top) matrix.
463−ones :: (Num e, FL cols rows, CountableDims cols rows) => Matrix e cols rows
464−ones = matrixBuilder' (const 1)
466+ones :: (Num e, FromLists e cols rows, KnownNat (Count cols), KnownNat (Count rows)) => Matrix e cols rows
467+ones = matrixBuilder (const 1)
465468
466469-- Const Matrix
467470
468471-- | The constant matrix constructor. A matrix wholly filled with a given
469472-- value.
470−constant :: (Num e, FL cols rows, CountableDims cols rows) => e -> Matrix e cols rows
471−constant e = matrixBuilder' (const e)
473+constant :: (Num e, FromLists e cols rows, KnownNat (Count cols), KnownNat (Count rows)) => e -> Matrix e cols rows
474+constant e = matrixBuilder (const e)
472475
473476-- Bang Matrix
474477
475478-- | The T (Top) row vector matrix.
476−bang :: forall e cols. (Num e, Enum e, FL cols (), Countable cols) => Matrix e cols ()
479+bang :: forall e cols. (Num e, Enum e, FromLists e cols (), KnownNat (Count cols)) => Matrix e cols ()
477480bang =
478481 let c = fromInteger $ natVal (Proxy :: Proxy (Count cols))
479482 in fromLists [take c [1, 1 ..]]
480483
481−-- iden Matrix
484+-- Identity Matrix
482485
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 #-}
486+-- | Identity matrix.
487+identity :: (Num e, FromLists e cols cols, KnownNat (Count cols)) => Matrix e cols cols
488+identity = matrixBuilder (bool 0 1 . uncurry (==))
487489
488490-- Matrix composition (MMM)
489491
@@ -492,90 +494,60 @@ iden = matrixBuilder' (bool 0 1 . uncurry (==))
492494-- This definition takes advantage of divide-and-conquer and fusion laws
493495-- from LAoP.
494496comp :: (Num e) => Matrix e cr rows -> Matrix e cols cr -> Matrix e cols rows
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)
497+comp Empty Empty = Empty
498+comp (One a) (One b) = One (a * b)
499+comp (Junc a b) (Split c d) = comp a c + comp b d -- Divide-and-conquer law
500+comp (Split a b) c = Split (comp a c) (comp b c) -- Split fusion law
501+comp c (Junc a b) = Junc (comp c a) (comp c b) -- Junc fusion law
522502
523503-- Projections
524504
525505-- | Biproduct first component projection
526−p1 :: (Num e, CountableDims n m, FL n m, FL m m) => Matrix e (Either m n) m
527−p1 = join id zeros
506+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
507+p1 =
508+ let iden = identity :: Matrix e m m
509+ zero = zeros :: Matrix e n m
510+ in junc iden zero
528511
529512-- | Biproduct second component projection
530−p2 :: (Num e, CountableDims n m, FL m n, FL n n) => Matrix e (Either m n) n
531−p2 = join zeros id
513+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
514+p2 =
515+ let iden = identity :: Matrix e n n
516+ zero = zeros :: Matrix e m n
517+ in junc zero iden
532518
533519-- Injections
534520
535521-- | Biproduct first component injection
536−i1 :: (Num e, CountableDims n m, FL n m, FL m m) => Matrix e m (Either m n)
522+i1 :: (Num e, KnownNat (Count n), KnownNat (Count m), FromLists e n m, FromLists e m m) => Matrix e m (Either m n)
537523i1 = tr p1
538524
539525-- | Biproduct second component injection
540−i2 :: (Num e, CountableDims n m, FL m n, FL n n) => Matrix e n (Either m n)
526+i2 :: (Num e, KnownNat (Count n), KnownNat (Count m), FromLists e m n, FromLists e n n) => Matrix e n (Either m n)
541527i2 = tr p2
542528
543529-- Dimensions
544530
545531-- | Obtain the number of rows.
546532--
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
551−rows _ = fromInteger $ natVal (Proxy :: Proxy (Count rows))
552−
553−-- | Obtain the number of rows in an inefficient manner, but without any
554−-- constraints.
533+-- NOTE: The 'KnownNat' constaint is needed in order to obtain the
534+-- dimensions in constant time.
555535--
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
536+-- TODO: A 'rows' function that does not need the 'KnownNat' constraint in
537+-- exchange for performance.
538+rows :: forall e cols rows. (KnownNat (Count rows)) => Matrix e cols rows -> Int
539+rows _ = fromInteger $ natVal (Proxy :: Proxy (Count rows))
561540
562541-- | Obtain the number of columns.
542+--
543+-- NOTE: The 'KnownNat' constaint is needed in order to obtain the
544+-- dimensions in constant time.
563545--
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
546+-- TODO: A 'columns' function that does not need the 'KnownNat' constraint in
547+-- exchange for performance.
548+columns :: forall e cols rows. (KnownNat (Count cols)) => Matrix e cols rows -> Int
568549columns _ = fromInteger $ natVal (Proxy :: Proxy (Count cols))
569550
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−
579551-- Coproduct Bifunctor
580552
581553infixl 5 -|-
@@ -584,172 +556,157 @@ infixl 5 -|-
584556(-|-) ::
585557 forall e n k m j.
586558 ( Num e,
587− CountableDims j k,
588− FL k k,
589− FL j k,
590− FL k j,
591− FL j j
559+ KnownNat (Count j),
560+ KnownNat (Count k),
561+ FromLists e k k,
562+ FromLists e j k,
563+ FromLists e k j,
564+ FromLists e j j
592565 ) =>
593566 Matrix e n k ->
594567 Matrix e m j ->
595568 Matrix e (Either n m) (Either k j)
596−(-|-) a b = Join (i1 . a) (i2 . b)
569+(-|-) a b = Junc (i1 . a) (i2 . b)
597570
598571-- Khatri Rao Product and projections
599572
600573-- | Khatri Rao product first component projection matrix.
601−fstM ::
574+kp1 ::
602575 forall e m k .
603576 ( Num e,
604− CountableDims k m,
605− FL (Normalize (m, k)) m,
606− CountableN (m, k)
577+ KnownNat (Count k),
578+ FromLists e (FromNat (Count m * Count k)) m,
579+ KnownNat (Count m),
580+ KnownNat (Count (Normalize (m, k)))
607581 ) => Matrix e (Normalize (m, k)) m
608−fstM = matrixBuilder' f
582+kp1 = matrixBuilder f
609583 where
610584 offset = fromInteger (natVal (Proxy :: Proxy (Count k)))
611585 f (x, y)
612586 | y >= (x * offset) && y <= (x * offset + offset - 1) = 1
613− | otherwise = 0
587+ | otherwise = 0
614588
615589-- | Khatri Rao product second component projection matrix.
616−sndM ::
590+kp2 ::
617591 forall e m k .
618592 ( Num e,
619− CountableDims k m,
620− FL (Normalize (m, k)) k,
621− CountableN (m, k)
593+ KnownNat (Count k),
594+ FromLists e (FromNat (Count m * Count k)) k,
595+ KnownNat (Count m),
596+ KnownNat (Count (Normalize (m, k)))
622597 ) => Matrix e (Normalize (m, k)) k
623−sndM = matrixBuilder' f
598+kp2 = matrixBuilder f
624599 where
625600 offset = fromInteger (natVal (Proxy :: Proxy (Count k)))
626601 f (x, y)
627602 | x == y || mod (y - x) offset == 0 = 1
628− | otherwise = 0
603+ | otherwise = 0
629604
630605-- | Khatri Rao Matrix product also known as matrix pairing.
631606--
632607-- NOTE: That this is not a true categorical product, see for instance:
633−--
608+--
634609-- @
635−-- | fstM . kr a b == a
636−-- kr a b ==> |
637−-- | sndM . kr a b == b
610+-- | kp1 . khatri a b == a
611+-- khatri a b ==> |
612+-- | kp2 . khatri a b == b
638613-- @
639614--
640615-- __Emphasis__ on the implication symbol.
641−kr ::
642− forall e cols a b.
616+khatri ::
617+ forall e cols a b.
643618 ( Num e,
644− CountableDims a b,
645− CountableN (a, b),
646− FL (Normalize (a, b)) a,
647− FL (Normalize (a, b)) b
619+ KnownNat (Count a),
620+ KnownNat (Count b),
621+ KnownNat (Count (Normalize (a, b))),
622+ FromLists e (Normalize (a, b)) a,
623+ FromLists e (Normalize (a, b)) b
648624 ) => Matrix e cols a -> Matrix e cols b -> Matrix e cols (Normalize (a, 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)
625+khatri a b =
626+ let kp1' = kp1 @e @a @b
627+ kp2' = kp2 @e @a @b
628+ in (tr kp1') . a * (tr kp2') . b
653629
654630-- Product Bifunctor (Kronecker)
655631
656632infixl 4 ><
657633
658634-- | Matrix product functor also known as kronecker product
659−(><) ::
660− forall e m p n q.
635+(><) ::
636+ forall e m p n q.
661637 ( Num e,
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− )
638+ KnownNat (Count m),
639+ KnownNat (Count n),
640+ KnownNat (Count p),
641+ KnownNat (Count q),
642+ KnownNat (Count (Normalize (m, n))),
643+ FromLists e (Normalize (m, n)) m,
644+ FromLists e (Normalize (m, n)) n,
645+ KnownNat (Count (Normalize (p, q))),
646+ FromLists e (Normalize (p, q)) p,
647+ FromLists e (Normalize (p, q)) q
648+ )
670649 => Matrix e m p -> Matrix e n q -> Matrix e (Normalize (m, n)) (Normalize (p, q))
671650(><) a b =
672− let fstM' = fstM @e @m @n
673− sndM' = sndM @e @m @n
674− in kr (a . fstM') (b . sndM')
651+ let kp1' = kp1 @e @m @n
652+ kp2' = kp2 @e @m @n
653+ in khatri (a . kp1') (b . kp2')
675654
676−-- Matrix abide Join Fork
655+-- Matrix abide Junc Split
677656
678−-- | Matrix "abiding" following the 'Join'-'Fork' exchange law.
679−--
657+-- | Matrix "abiding" followin the 'Junc'-'Split' abide law.
658+--
680659-- Law:
681660--
682661-- @
683−-- 'Join' ('Fork' a c) ('Fork' b d) == 'Fork' ('Join' a b) ('Join' c d)
662+-- 'Junc' ('Split' a c) ('Split' b d) == 'Split' ('Junc' a b) ('Junc' c d)
684663-- @
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)
664+abideJS :: Matrix e cols rows -> Matrix e cols rows
665+abideJS (Junc (Split a c) (Split b d)) = Split (Junc (abideJS a) (abideJS b)) (Junc (abideJS c) (abideJS d)) -- Junc-Split abide law
666+abideJS Empty = Empty
667+abideJS (One e) = One e
668+abideJS (Junc a b) = Junc (abideJS a) (abideJS b)
669+abideJS (Split a b) = Split (abideJS a) (abideJS b)
690670
691−-- Matrix abide Fork Join
671+-- Matrix abide Split Junc
692672
693−-- | Matrix "abiding" followin the 'Fork'-'Join' abide law.
694−--
673+-- | Matrix "abiding" followin the 'Split'-'Junc' abide law.
674+--
695675-- @
696−-- 'Fork' ('Join' a b) ('Join' c d) == 'Join' ('Fork' a c) ('Fork' b d)
676+-- 'Split' ('Junc' a b) ('Junc' c d) == 'Junc' ('Split' a c) ('Split' b d)
697677-- @
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)
678+abideSJ :: Matrix e cols rows -> Matrix e cols rows
679+abideSJ (Split (Junc a b) (Junc c d)) = Junc (Split (abideSJ a) (abideSJ c)) (Split (abideSJ b) (abideSJ d)) -- Split-Junc abide law
680+abideSJ Empty = Empty
681+abideSJ (One e) = One e
682+abideSJ (Junc a b) = Junc (abideSJ a) (abideSJ b)
683+abideSJ (Split a b) = Split (abideSJ a) (abideSJ b)
703684
704685-- Matrix transposition
705686
706687-- | Matrix transposition.
707688tr :: Matrix e cols rows -> Matrix e rows cols
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)
689+tr Empty = Empty
690+tr (One e) = One e
691+tr (Junc a b) = Split (tr a) (tr b)
692+tr (Split a b) = Junc (tr a) (tr b)
711693
712694-- Selective 'select' operator
713695
714696-- | Selective functors 'select' operator equivalent inspired by the
715697-- ArrowMonad solution presented in the paper.
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
698+select :: (Num e, FromLists e b b, KnownNat (Count b)) => Matrix e cols (Either a b) -> Matrix e a b -> Matrix e cols b
699+select m y = junc y identity . m
743700
744701-- McCarthy's Conditional
745702
746703-- | McCarthy's Conditional expresses probabilistic choice.
747704cond ::
748− ( Trivial cols,
749− Countable cols,
750− FL () cols,
751− FL cols (),
752− FL cols cols,
705+ ( cols ~ FromNat (Count cols),
706+ KnownNat (Count cols),
707+ FromLists e () cols,
708+ FromLists e cols (),
709+ FromLists e cols cols,
753710 Bounded a,
754711 Enum a,
755712 Num e,
@@ -757,14 +714,14 @@ cond ::
757714 )
758715 =>
759716 (a -> Bool) -> Matrix e cols rows -> Matrix e cols rows -> Matrix e cols rows
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,
717+cond p f g = junc f g . grd p
718+
719+grd ::
720+ ( q ~ FromNat (Count q),
721+ KnownNat (Count q),
722+ FromLists e () q,
723+ FromLists e q (),
724+ FromLists e q q,
768725 Bounded a,
769726 Enum a,
770727 Num e,
@@ -772,88 +729,62 @@ grd ::
772729 )
773730 =>
774731 (a -> Bool) -> Matrix e q (Either q q)
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− )
732+grd f = split (corr f) (corr (not . f))
733+
734+corr ::
735+ forall e a q .
736+ ( q ~ FromNat (Count q),
737+ KnownNat (Count q),
738+ FromLists e () q,
739+ FromLists e q (),
740+ FromLists e q q,
741+ Bounded a,
742+ Enum a,
743+ Num e,
744+ Ord e
745+ )
786746 => (a -> Bool) -> Matrix e q q
787−corr p = let f = fromF' p :: Matrix e q ()
788− in kr f (id :: Matrix e q q)
747+corr p = let f = fromF p :: Matrix e q ()
748+ in khatri f (identity :: Matrix e q q)
789749
790750-- Pretty print
791751
792752prettyAux :: Show e => [[e]] -> [[e]] -> String
793753prettyAux [] _ = ""
794−prettyAux [[e]] m = "│ " ++ fill (show e) ++ " │\n"
754+prettyAux [[e]] m = "│ " ++ fill (show e) ++ " │\n"
795755 where
796756 v = fmap show m
797757 widest = maximum $ fmap length v
798758 fill str = replicate (widest - length str - 2) ' ' ++ str
799−prettyAux [h] m = "│ " ++ fill (unwords $ map show h) ++ " │\n"
759+prettyAux [h] m = "│ " ++ fill (unwords $ map show h) ++ " │\n"
800760 where
801− v = fmap show m
802− widest = maximum $ fmap length v
761+ v = fmap show m
762+ widest = maximum $ fmap length v
803763 fill str = replicate (widest - length str - 2) ' ' ++ str
804−prettyAux (h : t) l = "│ " ++ fill (unwords $ map show h) ++ " │\n" ++
764+prettyAux (h : t) l = "│ " ++ fill (unwords $ map show h) ++ " │\n" ++
805765 prettyAux t l
806766 where
807− v = fmap show l
808− widest = maximum $ fmap length v
767+ v = fmap show l
768+ widest = maximum $ fmap length v
809769 fill str = replicate (widest - length str - 2) ' ' ++ str
810770
811771-- | Matrix pretty printer
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
772+pretty :: (KnownNat (Count cols), Show e) => Matrix e cols rows -> String
773+pretty m = "┌ " ++ unwords (replicate (columns m) blank) ++ " ┐\n" ++
774+ prettyAux (toLists m) (toLists m) ++
775+ "└ " ++ unwords (replicate (columns m) blank) ++ " ┘"
776+ where
777+ v = fmap show (toList m)
778+ widest = maximum $ fmap length v
822779 fill str = replicate (widest - length str) ' ' ++ str
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)
780+ blank = fill ""
839781
840782-- | Matrix pretty printer
841−prettyPrint :: (CountableDims cols rows, Show e) => Matrix e cols rows -> IO ()
783+prettyPrint :: (KnownNat (Count cols), Show e) => Matrix e cols rows -> IO ()
842784prettyPrint = putStrLn . pretty
843785
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−
852786-- Relational operators functions
853787
854−type Boolean = Natural 0 1
855−type Relation a b = Matrix Boolean a b
856−
857788-- | Helper conversion function
858789toBool :: (Num e, Eq e) => e -> Bool
859790toBool n
@@ -865,110 +796,104 @@ fromBool :: Bool -> Natural 0 1
865796fromBool True = nat 1
866797fromBool False = nat 0
867798
868−-- | Relational negation
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)
873−
874799-- | Relational addition
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
800+orM :: Matrix (Natural 0 1) cols rows -> Matrix (Natural 0 1) cols rows -> Matrix (Natural 0 1) cols rows
801+orM Empty Empty = Empty
802+orM (One a) (One b) = One (fromBool (toBool a || toBool b))
803+orM (Junc a b) (Junc c d) = Junc (orM a c) (orM b d)
804+orM (Split a b) (Split c d) = Split (orM a c) (orM b d)
805+orM x@(Split _ _) y@(Junc _ _) = orM x (abideJS y)
806+orM x@(Junc _ _) y@(Split _ _) = orM (abideJS x) y
881807
882808-- | Relational multiplication
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
809+andM :: Matrix (Natural 0 1) cols rows -> Matrix (Natural 0 1) cols rows -> Matrix (Natural 0 1) cols rows
810+andM Empty Empty = Empty
811+andM (One a) (One b) = One (fromBool (toBool a && toBool b))
812+andM (Junc a b) (Junc c d) = Junc (andM a c) (andM b d)
813+andM (Split a b) (Split c d) = Split (andM a c) (andM b d)
814+andM x@(Split _ _) y@(Junc _ _) = andM x (abideJS y)
815+andM x@(Junc _ _) y@(Split _ _) = andM (abideJS x) y
889816
890817-- | Relational subtraction
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
818+subM :: Matrix (Natural 0 1) cols rows -> Matrix (Natural 0 1) cols rows -> Matrix (Natural 0 1) cols rows
819+subM Empty Empty = Empty
820+subM (One a) (One b) = if a - b < nat 0 then One (nat 0) else One (a - b)
821+subM (Junc a b) (Junc c d) = Junc (subM a c) (subM b d)
822+subM (Split a b) (Split c d) = Split (subM a c) (subM b d)
823+subM x@(Split _ _) y@(Junc _ _) = subM x (abideJS y)
824+subM x@(Junc _ _) y@(Split _ _) = subM (abideJS x) y
897825
898826-- | Matrix relational composition.
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
827+compRel :: Matrix (Natural 0 1) cr rows -> Matrix (Natural 0 1) cols cr -> Matrix (Natural 0 1) cols rows
828+compRel Empty Empty = Empty
829+compRel (One a) (One b) = One (fromBool (toBool a && toBool b))
830+compRel (Junc a b) (Split c d) = orM (compRel a c) (compRel b d) -- Divide-and-conquer law
831+compRel (Split a b) c = Split (compRel a c) (compRel b c) -- Split fusion law
832+compRel c (Junc a b) = Junc (compRel c a) (compRel c b) -- Junc fusion law
921833
922834-- | Lifts functions to relations with arbitrary dimensions.
923835--
924836-- NOTE: Be careful to not ask for a relation bigger than the cardinality of
925837-- types @a@ or @b@ allows.
926−fromFRel' ::
838+fromFRel ::
927839 forall a b cols rows.
928− ( Liftable Boolean a b,
929− CountableDims cols rows,
930− FL rows cols
840+ ( Bounded a,
841+ Bounded b,
842+ Enum a,
843+ Enum b,
844+ Eq b,
845+ KnownNat (Count cols),
846+ KnownNat (Count rows),
847+ FromLists (Natural 0 1) rows cols
931848 ) =>
932849 (a -> b) ->
933− Relation cols rows
934−fromFRel' = fromF'
850+ Matrix (Natural 0 1) cols rows
851+fromFRel f =
852+ let minA = minBound @a
853+ maxA = maxBound @a
854+ minB = minBound @b
855+ maxB = maxBound @b
856+ ccols = fromInteger $ natVal (Proxy :: Proxy (Count cols))
857+ rrows = fromInteger $ natVal (Proxy :: Proxy (Count rows))
858+ elementsA = take ccols [minA .. maxA]
859+ elementsB = take rrows [minB .. maxB]
860+ combinations = (,) <$> elementsA <*> elementsB
861+ combAp = map snd . sort . map (\(a, b) -> if f a == b
862+ then ((fromEnum a, fromEnum b), nat 1)
863+ else ((fromEnum a, fromEnum b), nat 0)) $ combinations
864+ mList = buildList combAp rrows
865+ in tr $ fromLists mList
866+ where
867+ buildList [] _ = []
868+ buildList l r = take r l : buildList (drop r l) r
935869
936870-- | Lifts functions to relations with dimensions matching @a@ and @b@
937871-- cardinality's.
938−fromFRel ::
872+fromFRel' ::
939873 forall a b.
940− ( Liftable Boolean a b,
941− CountableDimsN a b,
942− FLN b a
874+ ( Bounded a,
875+ Bounded b,
876+ Enum a,
877+ Enum b,
878+ Eq b,
879+ KnownNat (Count (Normalize a)),
880+ KnownNat (Count (Normalize b)),
881+ FromLists (Natural 0 1) (Normalize b) (Normalize a)
943882 ) =>
944883 (a -> b) ->
945− Relation (Normalize a) (Normalize b)
946−fromFRel = fromFRel'
947−
948−-- | Lifts a relation function to a Boolean Matrix
949−toRel ::
950− forall a b.
951− ( Bounded a,
952− Bounded b,
953− Enum a,
954− Enum b,
955− Eq b,
956− CountableDims a b,
957− FLN b a
958− )
959− => (a -> b -> Bool) -> Relation (Normalize a) (Normalize b)
960−toRel f =
884+ Matrix (Natural 0 1) (Normalize a) (Normalize b)
885+fromFRel' f =
961886 let minA = minBound @a
962887 maxA = maxBound @a
963888 minB = minBound @b
964889 maxB = maxBound @b
965− ccols = fromInteger $ natVal (Proxy :: Proxy (Count a))
966− rrows = fromInteger $ natVal (Proxy :: Proxy (Count b))
890+ ccols = fromInteger $ natVal (Proxy :: Proxy (Count (Normalize a)))
891+ rrows = fromInteger $ natVal (Proxy :: Proxy (Count (Normalize b)))
967892 elementsA = take ccols [minA .. maxA]
968893 elementsB = take rrows [minB .. maxB]
969894 combinations = (,) <$> elementsA <*> elementsB
970− combAp = map snd . sort . map (\(a, b) -> if uncurry f (a, b)
971− then ((fromEnum a, fromEnum b), nat 1)
895+ combAp = map snd . sort . map (\(a, b) -> if f a == b
896+ then ((fromEnum a, fromEnum b), nat 1)
972897 else ((fromEnum a, fromEnum b), nat 0)) $ combinations
973898 mList = buildList combAp rrows
974899 in tr $ fromLists mList
src/LAoP/Matrix/Nat.hs+187−194
@@ -1,4 +1,3 @@
1−{-# LANGUAGE ConstraintKinds #-}
21{-# LANGUAGE AllowAmbiguousTypes #-}
32{-# LANGUAGE DataKinds #-}
43{-# LANGUAGE DerivingVia #-}
@@ -54,22 +53,11 @@ module LAoP.Matrix.Nat
5453 -- * Type safe matrix representation
5554 Matrix (..),
5655
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−
6956 -- * Primitives
57+ empty,
7058 one,
71− join,
72− fork,
59+ junc,
60+ split,
7361
7462 -- * Auxiliary type families
7563 I.FromNat,
@@ -77,11 +65,11 @@ module LAoP.Matrix.Nat
7765 I.Normalize,
7866
7967 -- * Matrix construction and conversion
80− I.FL,
68+ I.FromLists,
8169 fromLists,
8270 toLists,
8371 toList,
84− matrixBuilder',
72+ matrixBuilder,
8573 row,
8674 col,
8775 zeros,
@@ -97,10 +85,6 @@ module LAoP.Matrix.Nat
9785 -- ** Matrix Transposition
9886 tr,
9987
100− -- ** Scalar multiplication/division of matrices
101− (.|),
102− (./),
103−
10488 -- ** Selective operator
10589 select,
10690
@@ -108,19 +92,16 @@ module LAoP.Matrix.Nat
10892 cond,
10993
11094 -- ** Matrix "abiding"
111− abideJF,
112− abideFJ,
113−
114− -- ** Zip Matrices
115− zipWithM,
95+ abideJS,
96+ abideSJ,
11697
11798 -- * Biproduct approach
118− -- ** Fork
99+ -- ** Split
119100 (===),
120101 -- *** Projections
121102 p1,
122103 p2,
123− -- ** Join
104+ -- ** Junc
124105 (|||),
125106 -- *** Injections
126107 i1,
@@ -134,11 +115,11 @@ module LAoP.Matrix.Nat
134115 -- | Note that given the restrictions imposed it is not possible to
135116 -- implement the standard type classes present in standard Haskell.
136117 -- *** Matrix pairing projections
137− fstM,
138− sndM,
118+ kp1,
119+ kp2,
139120
140121 -- *** Matrix pairing
141− kr,
122+ khatri,
142123
143124 -- * Matrix composition and lifting
144125
@@ -146,10 +127,10 @@ module LAoP.Matrix.Nat
146127
147128 -- | Note that given the restrictions imposed it is not possible to
148129 -- implement the standard type classes present in standard Haskell.
149− iden,
130+ identity,
150131 comp,
151− fromF',
152132 fromF,
133+ fromF',
153134
154135 -- * Matrix printing
155136 pretty,
@@ -160,95 +141,107 @@ where
160141import Data.Proxy
161142import GHC.TypeLits
162143import Control.DeepSeq
144+import qualified Control.Category as C
163145import qualified LAoP.Matrix.Internal as I
164146
165147newtype Matrix e (cols :: Nat) (rows :: Nat) = M (I.Matrix e (I.FromNat cols) (I.FromNat rows))
166148 deriving (Show, Num, Eq, Ord, NFData) via (I.Matrix e (I.FromNat cols) (I.FromNat rows))
167149
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))
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
179158
180159-- Primitives
181160
161+empty :: Matrix e 0 0
162+empty = M I.Empty
163+
182164one :: e -> Matrix e 1 1
183165one = M . I.One
184166
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)
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)
191173
192174infixl 3 |||
193175(|||) ::
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)
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)
206188
207189infixl 2 ===
208190(===) ::
209− (TrivialE a b) =>
210− Matrix e cols a ->
211− Matrix e cols b ->
212− Matrix e cols (a + b)
213−(===) = fork
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
214196
215197-- Construction
216198
217−fromLists :: (FLN e cols rows) => [[e]] -> Matrix e cols rows
199+fromLists :: (I.FromLists e (I.FromNat cols) (I.FromNat rows)) => [[e]] -> Matrix e cols rows
218200fromLists = M . I.fromLists
219201
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'
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
226207
227−col :: (I.FL () (I.FromNat rows)) => [e] -> Matrix e 1 rows
208+col :: (I.FromLists e () (I.FromNat rows)) => [e] -> Matrix e 1 rows
228209col = M . I.col
229210
230−row :: (I.FL (I.FromNat cols) ()) => [e] -> Matrix e cols 1
211+row :: (I.FromLists e (I.FromNat cols) ()) => [e] -> Matrix e cols 1
231212row = M . I.row
232213
233−fromF' ::
234− ( Liftable e a b,
235− CountableN cols,
236− CountableN rows,
237− FLN e rows cols
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)
238225 ) =>
239226 (a -> b) ->
240227 Matrix e cols rows
241−fromF' = M . I.fromF'
228+fromF = M . I.fromF
242229
243−fromF ::
244− ( Liftable e a b,
245− CountableNz a,
246− CountableNz b,
247− FLNz e b a
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)
248241 ) =>
249242 (a -> b) ->
250243 Matrix e (I.Count a) (I.Count b)
251−fromF = undefined -- M . I.fromF
244+fromF' = M . I.fromF'
252245
253246-- Conversion
254247
@@ -261,21 +254,21 @@ toList (M m) = I.toList m
261254-- Zeros Matrix
262255
263256zeros ::
264− (Num e, FLN e cols rows, CountableN cols, CountableN rows) =>
257+ (Num e, I.FromLists e (I.FromNat cols) (I.FromNat rows), KnownNat (I.Count (I.FromNat cols)), KnownNat (I.Count (I.FromNat rows))) =>
265258 Matrix e cols rows
266259zeros = M I.zeros
267260
268261-- Ones Matrix
269262
270263ones ::
271− (Num e, FLN e cols rows, CountableN cols, CountableN rows) =>
264+ (Num e, I.FromLists e (I.FromNat cols) (I.FromNat rows), KnownNat (I.Count (I.FromNat cols)), KnownNat (I.Count (I.FromNat rows))) =>
272265 Matrix e cols rows
273266ones = M I.ones
274267
275268-- Const Matrix
276269
277270constant ::
278− (Num e, FLN e cols rows, CountableN cols, CountableN rows) =>
271+ (Num e, I.FromLists e (I.FromNat cols) (I.FromNat rows), KnownNat (I.Count (I.FromNat cols)), KnownNat (I.Count (I.FromNat rows))) =>
279272 e ->
280273 Matrix e cols rows
281274constant = M . I.constant
@@ -284,52 +277,40 @@ constant = M . I.constant
284277
285278bang ::
286279 forall e cols.
287− (Num e, Enum e, I.FL (I.FromNat cols) (), CountableN cols) =>
280+ (Num e, Enum e, I.FromLists e (I.FromNat cols) (), KnownNat (I.Count (I.FromNat cols))) =>
288281 Matrix e cols 1
289282bang = M I.bang
290283
291−-- iden Matrix
284+-- Identity Matrix
292285
293−iden ::
294− (Num e, FLN e cols cols, CountableN cols) =>
286+identity ::
287+ (Num e, I.FromLists e (I.FromNat cols) (I.FromNat cols), KnownNat (I.Count (I.FromNat cols))) =>
295288 Matrix e cols cols
296−iden = M I.iden
289+identity = M I.identity
297290
298291-- Matrix composition (MMM)
299292
300293comp :: (Num e) => Matrix e cr rows -> Matrix e cols cr -> Matrix e cols rows
301294comp (M a) (M b) = M (I.comp a b)
302295
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−
317296p1 ::
318297 ( Num e,
319− CountableDimsN n m,
320− FLN e n m,
321− FLN e m m,
322− TrivialE m n
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)
323303 ) =>
324304 Matrix e (m + n) m
325305p1 = M I.p1
326306
327307p2 ::
328308 ( Num e,
329− CountableDimsN n m,
330− FLN e m n,
331− FLN e n n,
332− TrivialE m n
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)
333314 ) =>
334315 Matrix e (m + n) n
335316p2 = M I.p2
@@ -338,125 +319,138 @@ p2 = M I.p2
338319
339320i1 ::
340321 ( Num e,
341− CountableDimsN n rows,
342− FLN e n rows,
343− FLN e rows rows,
344− TrivialE rows n
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)
345327 ) =>
346328 Matrix e rows (rows + n)
347329i1 = tr p1
348330
349331i2 ::
350332 ( Num e,
351− CountableDimsN rows m,
352− FLN e m rows,
353− FLN e rows rows,
354− TrivialE m rows
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)
355338 ) =>
356339 Matrix e rows (m + rows)
357340i2 = tr p2
358341
359342-- Dimensions
360343
361−rows :: (CountableN rows) => Matrix e cols rows -> Int
344+rows :: (KnownNat (I.Count (I.FromNat rows))) => Matrix e cols rows -> Int
362345rows (M m) = I.rows m
363346
364−columns :: (CountableN cols) => Matrix e cols rows -> Int
347+columns :: (KnownNat (I.Count (I.FromNat cols))) => Matrix e cols rows -> Int
365348columns (M m) = I.columns m
366349
350+-- Coproduct Bifunctor
351+
367352infixl 5 -|-
368353
369−-- | Coproduct Bifunctor (Direct sum)
370354(-|-) ::
371355 ( Num e,
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
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)
379364 ) =>
380365 Matrix e n k ->
381366 Matrix e m j ->
382367 Matrix e (n + m) (k + j)
383368(-|-) (M a) (M b) = M ((I.-|-) a b)
384369
385−-- | Khatri Rao Product first projection
386−fstM ::
370+-- Khatri Rao Product and projections
371+
372+kp1 ::
387373 forall e m k .
388374 ( Num e,
389− CountableDimsN m k,
390− CountableN (m * k),
391− FLN e (m * k) m,
392− TrivialP m k
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))
393380 ) => Matrix e (m * k) m
394−fstM = M (I.fstM @e @(I.FromNat m) @(I.FromNat k))
381+kp1 = M (I.kp1 @e @(I.FromNat m) @(I.FromNat k))
395382
396−-- | Khatri Rao Product second projection
397−sndM ::
383+kp2 ::
398384 forall e m k.
399385 ( Num e,
400− CountableDimsN k m,
401− FLN e (m * k) k,
402− CountableN (m * k),
403− TrivialP m k
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))
404391 ) => Matrix e (m * k) k
405−sndM = M (I.sndM @e @(I.FromNat m) @(I.FromNat k))
392+kp2 = M (I.kp2 @e @(I.FromNat m) @(I.FromNat k))
406393
407−-- | Khatri Rao Product
408−kr ::
394+khatri ::
409395 forall e cols a b.
410396 ( Num e,
411− CountableDimsN a b,
412− CountableN (a * b),
413− FLN e (a * b) a,
414− FLN e (a * b) b,
415− TrivialP a b
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))
416403 ) => Matrix e cols a -> Matrix e cols b -> Matrix e cols (a * b)
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
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)
421410
422−-- | Product Bifunctor (Kronecker)
423411infixl 4 ><
424412
425413(><) ::
426414 forall e m p n q.
427415 ( Num e,
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
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))
437428 ) => Matrix e m p -> Matrix e n q -> Matrix e (m * n) (p * q)
438429(><) a b =
439− let fstM' = fstM @e @m @n
440− sndM' = sndM @e @m @n
441− in kr (comp a fstM') (comp b sndM')
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
442435
443−-- | Matrix abide Join Fork
444−abideJF :: Matrix e cols rows -> Matrix e cols rows
445−abideJF (M m) = M (I.abideJF m)
436+abideJS :: Matrix e cols rows -> Matrix e cols rows
437+abideJS (M m) = M (I.abideJS m)
446438
447−-- | Matrix abide Fork Join
448−abideFJ :: Matrix e cols rows -> Matrix e cols rows
449−abideFJ (M m) = M (I.abideFJ m)
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
450445
451−-- | Matrix transposition
452446tr :: Matrix e cols rows -> Matrix e rows cols
453447tr (M m) = M (I.tr m)
454448
455449-- Selective 'select' operator
456450select ::
457451 ( Num e,
458− FLN e rows1 rows1,
459− CountableN rows1,
452+ I.FromLists e (I.FromNat rows1) (I.FromNat rows1),
453+ KnownNat (I.Count (I.FromNat rows1)),
460454 I.FromNat rows2 ~ I.FromNat rows1,
461455 I.FromNat cols1 ~ I.FromNat cols2,
462456 I.FromNat rows3 ~ Either (I.FromNat cols3) (I.FromNat rows1)
@@ -467,11 +461,14 @@ select (M m) (M y) = M (I.select m y)
467461
468462cond ::
469463 ( I.FromNat (I.Count (I.FromNat cols)) ~ I.FromNat cols,
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
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
475472 )
476473 =>
477474 (a -> Bool) -> Matrix e cols rows -> Matrix e cols rows -> Matrix e cols rows
@@ -479,12 +476,8 @@ cond p (M a) (M b) = M (I.cond p a b)
479476
480477-- Pretty print
481478
482−pretty :: (CountableDimsN cols rows, Show e) => Matrix e cols rows -> String
479+pretty :: (KnownNat (I.Count (I.FromNat cols)), Show e) => Matrix e cols rows -> String
483480pretty (M m) = I.pretty m
484481
485−prettyPrint :: (CountableDimsN cols rows, Show e) => Matrix e cols rows -> IO ()
482+prettyPrint :: (KnownNat (I.Count (I.FromNat cols)), Show e) => Matrix e cols rows -> IO ()
486483prettyPrint (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+232−292
@@ -1,11 +1,10 @@
1−{-# LANGUAGE ConstraintKinds #-}
2−{-# LANGUAGE TypeFamilies #-}
31{-# LANGUAGE AllowAmbiguousTypes #-}
42{-# LANGUAGE DataKinds #-}
53{-# LANGUAGE DerivingVia #-}
64{-# LANGUAGE FlexibleContexts #-}
75{-# LANGUAGE FlexibleInstances #-}
86{-# LANGUAGE GADTs #-}
7+{-# LANGUAGE KindSignatures #-}
98{-# LANGUAGE MultiParamTypeClasses #-}
109{-# LANGUAGE NoStarIsType #-}
1110{-# LANGUAGE RankNTypes #-}
@@ -56,24 +55,15 @@ module LAoP.Matrix.Type
5655 -- * Type safe matrix representation
5756 Matrix (..),
5857
59− -- * Constraint type aliases
60− Countable,
61− CountableDims,
62− CountableN,
63− CountableDimsN,
64− FLN,
65− Liftable,
66− Trivial,
67− TrivialP,
68−
6958 -- * Type aliases
7059 Zero,
7160 One,
7261
7362 -- * Primitives
63+ empty,
7464 one,
75− join,
76− fork,
65+ junc,
66+ split,
7767
7868 -- * Auxiliary type families
7969 I.FromNat,
@@ -85,27 +75,24 @@ module LAoP.Matrix.Type
8575 fromLists,
8676 toLists,
8777 toList,
88− matrixBuilder',
8978 matrixBuilder,
9079 row,
9180 col,
9281 zeros,
9382 ones,
9483 bang,
95− point,
9684 constant,
9785
9886 -- * Functor instance equivalent function
9987 fmapM,
100− bimapM,
10188
10289 -- * Applicative/Monoidal instance equivalent functions
10390 unitM,
10491 multM,
10592
10693 -- * Selective equivalent instance function
107− selectM,
108−
94+ selectM,
95+
10996 -- * Monad equivalent instance function
11097 returnM,
11198 bindM,
@@ -113,34 +100,25 @@ module LAoP.Matrix.Type
113100 -- * Misc
114101 -- ** Get dimensions
115102 columns,
116− columns',
117103 rows,
118− rows',
119104
120105 -- ** Matrix Transposition
121106 tr,
122107
123− -- ** Scalar multiplication/division of matrices
124− (.|),
125− (./),
126−
127108 -- ** McCarthy's Conditional
128109 cond,
129110
130111 -- ** Matrix "abiding"
131− abideJF,
132− abideFJ,
133−
134− -- ** Zip Matrices
135− zipWithM,
112+ abideJS,
113+ abideSJ,
136114
137115 -- * Biproduct approach
138− -- ** Fork
116+ -- ** Split
139117 (===),
140118 -- *** Projections
141119 p1,
142120 p2,
143− -- ** Join
121+ -- ** Junc
144122 (|||),
145123 -- *** Injections
146124 i1,
@@ -154,11 +132,11 @@ module LAoP.Matrix.Type
154132 -- | Note that given the restrictions imposed it is not possible to
155133 -- implement the standard type classes present in standard Haskell.
156134 -- *** Matrix pairing projections
157− fstM,
158− sndM,
135+ kp1,
136+ kp2,
159137
160138 -- *** Matrix pairing
161− kr,
139+ khatri,
162140
163141 -- * Matrix composition and lifting
164142
@@ -166,13 +144,10 @@ module LAoP.Matrix.Type
166144
167145 -- | Note that given the restrictions imposed it is not possible to
168146 -- implement the standard type classes present in standard Haskell.
169− iden,
147+ identity,
170148 comp,
171− fromF',
172149 fromF,
173−
174− -- * Relation
175− toRel,
150+ fromF',
176151
177152 -- * Matrix printing
178153 pretty,
@@ -183,44 +158,22 @@ where
183158import Data.Void
184159import Data.Proxy
185160import Data.Kind
186−import GHC.TypeLits
161+import GHC.TypeLits
187162import Control.DeepSeq
188−import LAoP.Utils
163+import qualified Control.Category as C
189164import qualified LAoP.Matrix.Internal as I
190−import Prelude hiding (id, (.))
191165
192166newtype Matrix e (cols :: Type) (rows :: Type) = M (I.Matrix e (I.Normalize cols) (I.Normalize rows))
193167 deriving (Show, Num, Eq, Ord, NFData) via (I.Matrix e (I.Normalize cols) (I.Normalize rows))
194168
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)
169+-- | It isn't possible to implement the 'id' function so it's
170+-- implementation is 'undefined'. However 'comp' can be and this partial
171+-- class implementation exists just to make the code more readable.
172+--
173+-- Please use 'identity' instead.
174+instance (Num e) => C.Category (Matrix e) where
175+ id = undefined
176+ (.) = comp
224177
225178-- | Zero type alias
226179type Zero = Void
@@ -230,75 +183,92 @@ type One = ()
230183
231184-- Primitives
232185
186+-- | Empty matrix constructor
187+empty :: Matrix e Zero Zero
188+empty = M I.Empty
189+
233190-- | Unit matrix constructor
234191one :: e -> Matrix e One One
235192one = M . I.One
236193
237−-- | Matrix 'Join' constructor
238−join ::
194+-- | Matrix 'Junc' constructor
195+junc ::
196+ (I.Normalize (Either a b) ~ Either (I.Normalize a) (I.Normalize b)) =>
239197 Matrix e a rows ->
240198 Matrix e b rows ->
241199 Matrix e (Either a b) rows
242−join (M a) (M b) = M (I.Join a b)
200+junc (M a) (M b) = M (I.Junc a b)
243201
244202infixl 3 |||
245−-- | Matrix 'Join' constructor
203+-- | Matrix 'Junc' constructor
246204(|||) ::
205+ (I.Normalize (Either a b) ~ Either (I.Normalize a) (I.Normalize b)) =>
247206 Matrix e a rows ->
248207 Matrix e b rows ->
249208 Matrix e (Either a b) rows
250−(|||) = join
209+(|||) = junc
251210
252−-- | Matrix 'Fork' constructor
253−fork ::
211+-- | Matrix 'Split' constructor
212+split ::
213+ (I.Normalize (Either a b) ~ Either (I.Normalize a) (I.Normalize b)) =>
254214 Matrix e cols a ->
255215 Matrix e cols b ->
256216 Matrix e cols (Either a b)
257−fork (M a) (M b) = M (I.Fork a b)
217+split (M a) (M b) = M (I.Split a b)
258218
259219infixl 2 ===
260−-- | Matrix 'Fork' constructor
220+-- | Matrix 'Split' constructor
261221(===) ::
222+ (I.Normalize (Either a b) ~ Either (I.Normalize a) (I.Normalize b)) =>
262223 Matrix e cols a ->
263224 Matrix e cols b ->
264225 Matrix e cols (Either a b)
265−(===) = fork
226+(===) = split
266227
267228-- Functor hierarchy
268229
269230-- | Functor instance equivalent function
270−fmapM ::
271− ( Liftable e a b,
272− CountableDimsN a b,
273− FLN b a
231+fmapM ::
232+ ( Bounded a,
233+ Bounded b,
234+ Enum a,
235+ Enum b,
236+ Eq b,
237+ Num e,
238+ Ord e,
239+ KnownNat (I.Count (I.Normalize a)),
240+ KnownNat (I.Count (I.Normalize b)),
241+ I.FromLists e (I.Normalize b) (I.Normalize a)
274242 )
275243 =>
276244 (a -> b) -> Matrix e c a -> Matrix e c b
277−fmapM f m = fromF f . m
245+fmapM f m = fromF' f `comp` m
278246
279247-- | Applicative instance equivalent 'unit' function,
280248unitM :: (Num e) => Matrix e () ()
281249unitM = one 1
282250
283251-- | Applicative instance equivalent 'unit' function,
284−multM ::
285− ( CountableDimsN a b,
286− CountableN (a, b),
252+multM ::
253+ ( KnownNat (I.Count (I.Normalize a)),
254+ KnownNat (I.Count (I.Normalize b)),
255+ KnownNat (I.Count (I.Normalize (a, b))),
287256 Num e,
288− FLN (a, b) a,
289− FLN (a, b) b,
290− TrivialP a b
257+ I.FromLists e (I.Normalize (a, b)) (I.Normalize a),
258+ I.FromLists e (I.Normalize (a, b)) (I.Normalize b),
259+ I.Normalize (a, b) ~ I.Normalize (I.Normalize a, I.Normalize b)
291260 ) => Matrix e c a -> Matrix e c b -> Matrix e c (a, b)
292−multM = kr
261+multM a b = khatri a b
262+
293263
294264-- | Monad instance equivalent 'return' function,
295−returnM ::
296− forall e a .
297− ( Num e,
298− Enum e,
299− Enum a,
300− FLN () a,
301− Countable a
265+returnM ::
266+ forall e a .
267+ ( Num e,
268+ Enum e,
269+ Enum a,
270+ I.FromLists e () (I.Normalize a),
271+ KnownNat (I.Count a)
302272 ) => a -> Matrix e One a
303273returnM a = col l
304274 where
@@ -314,66 +284,62 @@ bindM = flip comp
314284
315285-- | Build a matrix out of a list of list of elements. Throws a runtime
316286-- error if the dimensions do not match.
317−fromLists :: (FLN cols rows) => [[e]] -> Matrix e cols rows
287+fromLists :: (I.FromLists e (I.Normalize cols) (I.Normalize rows)) => [[e]] -> Matrix e cols rows
318288fromLists = M . I.fromLists
319289
320290-- | Matrix builder function. Constructs a matrix provided with
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.
291+-- a construction function.
329292matrixBuilder ::
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)
293+ (I.FromLists e (I.Normalize cols) (I.Normalize rows), KnownNat (I.Count (I.Normalize cols)), KnownNat (I.Count (I.Normalize rows))) =>
294+ ((Int, Int) -> e) ->
295+ Matrix e cols rows
296+matrixBuilder = M . I.matrixBuilder
339297
340298-- | Constructs a column vector matrix
341−col :: (FLN () rows) => [e] -> Matrix e One rows
299+col :: (I.FromLists e () (I.Normalize rows)) => [e] -> Matrix e One rows
342300col = M . I.col
343301
344302-- | Constructs a row vector matrix
345−row :: (FLN cols ()) => [e] -> Matrix e cols One
303+row :: (I.FromLists e (I.Normalize cols) ()) => [e] -> Matrix e cols One
346304row = M . I.row
347305
348306-- | Lifts functions to matrices with arbitrary dimensions.
349307--
350308-- NOTE: Be careful to not ask for a matrix bigger than the cardinality of
351309-- types @a@ or @b@ allows.
352−fromF' ::
353− ( Liftable e a b,
354− CountableDimsN cols rows,
355− FLN rows cols
310+fromF ::
311+ ( Bounded a,
312+ Bounded b,
313+ Enum a,
314+ Enum b,
315+ Eq b,
316+ Num e,
317+ Ord e,
318+ KnownNat (I.Count (I.Normalize cols)),
319+ KnownNat (I.Count (I.Normalize rows)),
320+ I.FromLists e (I.Normalize rows) (I.Normalize cols)
356321 ) =>
357− (a -> b) -> Matrix e cols rows
358−fromF' = M . I.fromF'
322+ (a -> b) ->
323+ Matrix e cols rows
324+fromF = M . I.fromF
359325
360326-- | Lifts functions to matrices with dimensions matching @a@ and @b@
361327-- cardinality's.
362−fromF ::
363− ( Liftable e a b,
364− CountableDimsN a b,
365− FLN b a
328+fromF' ::
329+ ( Bounded a,
330+ Bounded b,
331+ Enum a,
332+ Enum b,
333+ Eq b,
334+ Num e,
335+ Ord e,
336+ KnownNat (I.Count (I.Normalize a)),
337+ KnownNat (I.Count (I.Normalize b)),
338+ I.FromLists e (I.Normalize b) (I.Normalize a)
366339 ) =>
367− (a -> b) -> Matrix e a b
368−fromF = M . I.fromF
369−
370−-- | Lifts relation functions to Boolean Matrix
371−toRel ::
372− ( Liftable (Natural 0 1) a b,
373− CountableDims a b,
374− FLN b a
375− ) => (a -> b -> Bool) -> Matrix (Natural 0 1) a b
376−toRel = M . I.toRel
340+ (a -> b) ->
341+ Matrix e a b
342+fromF' = M . I.fromF'
377343
378344-- Conversion
379345
@@ -389,8 +355,8 @@ toList (M m) = I.toList m
389355
390356-- | The zero matrix. A matrix wholly filled with zeros.
391357zeros ::
392− (Num e, FLN cols rows, CountableDimsN cols rows)
393− => Matrix e cols rows
358+ (Num e, I.FromLists e (I.Normalize cols) (I.Normalize rows), KnownNat (I.Count (I.Normalize cols)), KnownNat (I.Count (I.Normalize rows))) =>
359+ Matrix e cols rows
394360zeros = M I.zeros
395361
396362-- Ones Matrix
@@ -399,8 +365,8 @@ zeros = M I.zeros
399365--
400366-- Also known as T (Top) matrix.
401367ones ::
402− (Num e, FLN cols rows, CountableDimsN cols rows)
403− => Matrix e cols rows
368+ (Num e, I.FromLists e (I.Normalize cols) (I.Normalize rows), KnownNat (I.Count (I.Normalize cols)), KnownNat (I.Count (I.Normalize rows))) =>
369+ Matrix e cols rows
404370ones = M I.ones
405371
406372-- Const Matrix
@@ -408,8 +374,9 @@ ones = M I.ones
408374-- | The constant matrix constructor. A matrix wholly filled with a given
409375-- value.
410376constant ::
411− (Num e, FLN cols rows, CountableDimsN cols rows)
412− => e -> Matrix e cols rows
377+ (Num e, I.FromLists e (I.Normalize cols) (I.Normalize rows), KnownNat (I.Count (I.Normalize cols)), KnownNat (I.Count (I.Normalize rows))) =>
378+ e ->
379+ Matrix e cols rows
413380constant = M . I.constant
414381
415382-- Bang Matrix
@@ -417,30 +384,17 @@ constant = M . I.constant
417384-- | The T (Top) row vector matrix.
418385bang ::
419386 forall e cols.
420− (Num e, Enum e, FLN cols (), CountableN cols) =>
387+ (Num e, Enum e, I.FromLists e (I.Normalize cols) (), KnownNat (I.Count (I.Normalize cols))) =>
421388 Matrix e cols One
422389bang = M I.bang
423390
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
391+-- Identity Matrix
437392
438−-- | iden matrix
439−iden ::
440− (Num e, FLN a a, CountableN a) =>
393+-- | Identity matrix
394+identity ::
395+ (Num e, I.FromLists e (I.Normalize a) (I.Normalize a), KnownNat (I.Count (I.Normalize a))) =>
441396 Matrix e a a
442−iden = M I.iden
443−{-# NOINLINE iden #-}
397+identity = M I.identity
444398
445399-- Matrix composition (MMM)
446400
@@ -450,32 +404,15 @@ iden = M I.iden
450404-- from LAoP.
451405comp :: (Num e) => Matrix e cr rows -> Matrix e cols cr -> Matrix e cols rows
452406comp (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)
472407
473408-- | Biproduct first component projection
474409p1 ::
475410 ( Num e,
476− CountableDimsN n m,
477− FLN n m,
478− FLN m m
411+ KnownNat (I.Count (I.Normalize n)),
412+ KnownNat (I.Count (I.Normalize m)),
413+ I.FromLists e (I.Normalize n) (I.Normalize m),
414+ I.FromLists e (I.Normalize m) (I.Normalize m),
415+ I.Normalize (Either m n) ~ Either (I.Normalize m) (I.Normalize n)
479416 ) =>
480417 Matrix e (Either m n) m
481418p1 = M I.p1
@@ -483,9 +420,11 @@ p1 = M I.p1
483420-- | Biproduct second component projection
484421p2 ::
485422 ( Num e,
486− CountableDimsN n m,
487− FLN m n,
488− FLN n n
423+ KnownNat (I.Count (I.Normalize n)),
424+ KnownNat (I.Count (I.Normalize m)),
425+ I.FromLists e (I.Normalize m) (I.Normalize n),
426+ I.FromLists e (I.Normalize n) (I.Normalize n),
427+ I.Normalize (Either m n) ~ Either (I.Normalize m) (I.Normalize n)
489428 ) =>
490429 Matrix e (Either m n) n
491430p2 = M I.p2
@@ -495,9 +434,11 @@ p2 = M I.p2
495434-- | Biproduct first component injection
496435i1 ::
497436 ( Num e,
498− CountableDimsN n m,
499− FLN n m,
500− FLN m m
437+ KnownNat (I.Count (I.Normalize n)),
438+ KnownNat (I.Count (I.Normalize m)),
439+ I.FromLists e (I.Normalize n) (I.Normalize m),
440+ I.FromLists e (I.Normalize m) (I.Normalize m),
441+ I.Normalize (Either m n) ~ Either (I.Normalize m) (I.Normalize n)
501442 ) =>
502443 Matrix e m (Either m n)
503444i1 = tr p1
@@ -505,9 +446,11 @@ i1 = tr p1
505446-- | Biproduct second component injection
506447i2 ::
507448 ( Num e,
508− CountableDimsN n m,
509− FLN m n,
510− FLN n n
449+ KnownNat (I.Count (I.Normalize n)),
450+ KnownNat (I.Count (I.Normalize m)),
451+ I.FromLists e (I.Normalize m) (I.Normalize n),
452+ I.FromLists e (I.Normalize n) (I.Normalize n),
453+ I.Normalize (Either m n) ~ Either (I.Normalize m) (I.Normalize n)
511454 ) =>
512455 Matrix e n (Either m n)
513456i2 = tr p2
@@ -516,34 +459,24 @@ i2 = tr p2
516459
517460-- | Obtain the number of rows.
518461--
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
523−rows (M m) = I.rows m
524−
525−-- | Obtain the number of rows in an inefficient manner, but without any
526−-- constraints.
462+-- NOTE: The 'KnownNat' constaint is needed in order to obtain the
463+-- dimensions in constant time.
527464--
528−-- For a more efficient version see 'rows'.
529−rows' :: Matrix e cols rows -> Int
530−rows' (M m) = I.rows' m
465+-- TODO: A 'rows' function that does not need the 'KnownNat' constraint in
466+-- exchange for performance.
467+rows :: (KnownNat (I.Count (I.Normalize rows))) => Matrix e cols rows -> Int
468+rows (M m) = I.rows m
531469
532470-- | Obtain the number of columns.
471+--
472+-- NOTE: The 'KnownNat' constaint is needed in order to obtain the
473+-- dimensions in constant time.
533474--
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
475+-- TODO: A 'columns' function that does not need the 'KnownNat' constraint in
476+-- exchange for performance.
477+columns :: (KnownNat (I.Count (I.Normalize cols))) => Matrix e cols rows -> Int
538478columns (M m) = I.columns m
539479
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−
547480-- Coproduct Bifunctor
548481
549482infixl 5 -|-
@@ -551,11 +484,14 @@ infixl 5 -|-
551484-- | Matrix coproduct functor also known as matrix direct sum.
552485(-|-) ::
553486 ( Num e,
554− CountableDimsN j k,
555− FLN k k,
556− FLN j k,
557− FLN k j,
558− FLN j j
487+ KnownNat (I.Count (I.Normalize j)),
488+ KnownNat (I.Count (I.Normalize k)),
489+ I.FromLists e (I.Normalize k) (I.Normalize k),
490+ I.FromLists e (I.Normalize j) (I.Normalize k),
491+ I.FromLists e (I.Normalize k) (I.Normalize j),
492+ I.FromLists e (I.Normalize j) (I.Normalize j),
493+ I.Normalize (Either n m) ~ Either (I.Normalize n) (I.Normalize m),
494+ I.Normalize (Either k j) ~ Either (I.Normalize k) (I.Normalize j)
559495 ) =>
560496 Matrix e n k ->
561497 Matrix e m j ->
@@ -565,98 +501,104 @@ infixl 5 -|-
565501-- Khatri Rao Product and projections
566502
567503-- | Khatri Rao product first component projection matrix.
568−fstM ::
504+kp1 ::
569505 forall e m k .
570506 ( Num e,
571− CountableDimsN m k,
572− CountableN (m, k),
573− FLN (m, k) m,
574− TrivialP m k
507+ KnownNat (I.Count (I.Normalize m)),
508+ KnownNat (I.Count (I.Normalize k)),
509+ KnownNat (I.Count (I.Normalize (m, k))),
510+ I.FromLists e (I.Normalize (m, k)) (I.Normalize m),
511+ I.Normalize (m, k) ~ I.Normalize (I.Normalize m, I.Normalize k)
575512 ) => Matrix e (m, k) m
576−fstM = M (I.fstM @e @(I.Normalize m) @(I.Normalize k))
513+kp1 = M (I.kp1 @e @(I.Normalize m) @(I.Normalize k))
577514
578515-- | Khatri Rao product second component projection matrix.
579−sndM ::
516+kp2 ::
580517 forall e m k.
581518 ( Num e,
582− CountableDimsN k m,
583− CountableN (m, k),
584− FLN (m, k) k,
585− TrivialP m k
519+ KnownNat (I.Count (I.Normalize k)),
520+ KnownNat (I.Count (I.Normalize m)),
521+ KnownNat (I.Count (I.Normalize (m, k))),
522+ I.FromLists e (I.Normalize (m, k)) (I.Normalize k),
523+ I.Normalize (m, k) ~ I.Normalize (I.Normalize m, I.Normalize k)
586524 ) => Matrix e (m, k) k
587−sndM = M (I.sndM @e @(I.Normalize m) @(I.Normalize k))
525+kp2 = M (I.kp2 @e @(I.Normalize m) @(I.Normalize k))
588526
589527-- | Khatri Rao Matrix product also known as matrix pairing.
590528--
591529-- NOTE: That this is not a true categorical product, see for instance:
592−--
530+--
593531-- @
594−-- | fstM . kr a b == a
595−-- kr a b ==> |
596−-- | sndM . kr a b == b
532+-- | kp1 `comp` khatri a b == a
533+-- khatri a b ==> |
534+-- | kp2 `comp` khatri a b == b
597535-- @
598536--
599537-- __Emphasis__ on the implication symbol.
600−kr ::
538+khatri ::
601539 forall e cols a b.
602540 ( Num e,
603− CountableDimsN a b,
604− CountableN (a, b),
605− FLN (a, b) a,
606− FLN (a, b) b,
607− TrivialP a b
541+ KnownNat (I.Count (I.Normalize a)),
542+ KnownNat (I.Count (I.Normalize b)),
543+ KnownNat (I.Count (I.Normalize (a, b))),
544+ I.FromLists e (I.Normalize (a, b)) (I.Normalize a),
545+ I.FromLists e (I.Normalize (a, b)) (I.Normalize b),
546+ I.Normalize (a, b) ~ I.Normalize (I.Normalize a, I.Normalize b)
608547 ) => Matrix e cols a -> Matrix e cols b -> Matrix e cols (a, 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
548+khatri a b =
549+ let kp1' = kp1 @e @a @b
550+ kp2' = kp2 @e @a @b
551+ in comp (tr kp1') a * comp (tr kp2') b
613552
614553-- Product Bifunctor (Kronecker)
615554
616555infixl 4 ><
617556
618−-- | Matrix product functor also known as Kronecker product
557+-- | Matrix product functor also known as kronecker product
619558(><) ::
620559 forall e m p n q.
621560 ( Num e,
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
561+ KnownNat (I.Count (I.Normalize m)),
562+ KnownNat (I.Count (I.Normalize n)),
563+ KnownNat (I.Count (I.Normalize p)),
564+ KnownNat (I.Count (I.Normalize q)),
565+ KnownNat (I.Count (I.Normalize (m, n))),
566+ KnownNat (I.Count (I.Normalize (p, q))),
567+ I.FromLists e (I.Normalize (m, n)) (I.Normalize m),
568+ I.FromLists e (I.Normalize (m, n)) (I.Normalize n),
569+ I.FromLists e (I.Normalize (p, q)) (I.Normalize p),
570+ I.FromLists e (I.Normalize (p, q)) (I.Normalize q),
571+ I.Normalize (m, n) ~ I.Normalize (I.Normalize m, I.Normalize n),
572+ I.Normalize (p, q) ~ I.Normalize (I.Normalize p, I.Normalize q)
631573 ) => Matrix e m p -> Matrix e n q -> Matrix e (m, n) (p, q)
632574(><) a b =
633− let fstM' = fstM @e @m @n
634− sndM' = sndM @e @m @n
635− in kr (comp a fstM') (comp b sndM')
575+ let kp1' = kp1 @e @m @n
576+ kp2' = kp2 @e @m @n
577+ in khatri (comp a kp1') (comp b kp2')
636578
637−-- Matrix abide Join Fork
579+-- Matrix abide Junc Split
638580
639−-- | Matrix "abiding" followin the 'Join'-'Fork' abide law.
640−--
581+-- | Matrix "abiding" followin the 'Junc'-'Split' abide law.
582+--
641583-- Law:
642584--
643585-- @
644−-- 'Join' ('Fork' a c) ('Fork' b d) == 'Fork' ('Join' a b) ('Join' c d)
586+-- 'Junc' ('Split' a c) ('Split' b d) == 'Split' ('Junc' a b) ('Junc' c d)
645587-- @
646−abideJF :: Matrix e cols rows -> Matrix e cols rows
647−abideJF (M m) = M (I.abideJF m)
588+abideJS :: Matrix e cols rows -> Matrix e cols rows
589+abideJS (M m) = M (I.abideJS m)
648590
649−-- Matrix abide Fork Join
591+-- Matrix abide Split Junc
650592
651−-- | Matrix "abiding" followin the 'Fork'-'Join' abide law.
652−--
593+-- | Matrix "abiding" followin the 'Split'-'Junc' abide law.
594+--
653595-- Law:
654596--
655597-- @
656−-- 'Fork' ('Join' a b) ('Join' c d) == 'Join' ('Fork' a c) ('Fork' b d)
598+-- 'Split' ('Junc' a b) ('Junc' c d) == 'Junc' ('Split' a c) ('Split' b d)
657599-- @
658−abideFJ :: Matrix e cols rows -> Matrix e cols rows
659−abideFJ (M m) = M (I.abideFJ m)
600+abideSJ :: Matrix e cols rows -> Matrix e cols rows
601+abideSJ (M m) = M (I.abideSJ m)
660602
661603-- Matrix transposition
662604
@@ -668,10 +610,11 @@ tr (M m) = M (I.tr m)
668610
669611-- | Selective functors 'select' operator equivalent inspired by the
670612-- ArrowMonad solution presented in the paper.
671−selectM ::
613+selectM ::
672614 ( Num e,
673− FLN b b,
674− CountableN b
615+ I.FromLists e (I.Normalize b) (I.Normalize b),
616+ KnownNat (I.Count (I.Normalize b)),
617+ I.Normalize (Either a b) ~ Either (I.Normalize a) (I.Normalize b)
675618 ) => Matrix e cols (Either a b) -> Matrix e a b -> Matrix e cols b
676619selectM (M m) (M y) = M (I.select m y)
677620
@@ -679,14 +622,15 @@ selectM (M m) (M y) = M (I.select m y)
679622
680623-- | McCarthy's Conditional expresses probabilistic choice.
681624cond ::
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
625+ ( I.Normalize (I.Normalize a) ~ I.Normalize a,
626+ KnownNat (I.Count (I.Normalize a)),
627+ I.FromLists e () (I.Normalize a),
628+ I.FromLists e (I.Normalize a) (),
629+ I.FromLists e (I.Normalize a) (I.Normalize a),
630+ Bounded a,
631+ Enum a,
632+ Num e,
633+ Ord e
690634 )
691635 =>
692636 (a -> Bool) -> Matrix e a b -> Matrix e a b -> Matrix e a b
@@ -695,13 +639,9 @@ cond p (M a) (M b) = M (I.cond p a b)
695639-- Pretty print
696640
697641-- | Matrix pretty printer
698−pretty :: (CountableDimsN cols rows, Show e) => Matrix e cols rows -> String
642+pretty :: (KnownNat (I.Count (I.Normalize cols)), Show e) => Matrix e cols rows -> String
699643pretty (M m) = I.pretty m
700644
701645-- | Matrix pretty printer
702−prettyPrint :: (CountableDimsN cols rows, Show e) => Matrix e cols rows -> IO ()
646+prettyPrint :: (KnownNat (I.Count (I.Normalize cols)), Show e) => Matrix e cols rows -> IO ()
703647prettyPrint (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+6−80
@@ -30,22 +30,11 @@ 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−
4333 -- * Primitives
34+ empty,
4435 one,
45− join,
46− (|||),
47− fork,
48− (===),
36+ junc,
37+ split,
4938
5039 -- * Auxiliary type families
5140 FromNat,
@@ -55,74 +44,21 @@ module LAoP.Relation
5544 -- * Matrix construction and conversion
5645 FromLists,
5746 fromLists,
58− fromF,
59− fromF',
60− toRel,
6147 toLists,
6248 toList,
63− toBool,
64− pt,
65− belongs,
66− relationBuilder,
49+ matrixBuilder,
6750 zeros,
6851 ones,
6952 bang,
70− point,
7153
7254 -- * Relational operations
7355 conv,
7456 intersection,
7557 union,
7658 sse,
77− implies,
78− iff,
7959 ker,
8060 img,
8161
82− -- * Taxonomy of binary relations
83− injective,
84− entire,
85− simple,
86− surjective,
87− representation,
88− function,
89− abstraction,
90− injection,
91− surjection,
92− bijection,
93− domain,
94− range,
95−
96− -- * Function division
97− divisionF,
98−
99− -- * Relation division
100− divR,
101− divL,
102− divS,
103− shrunkBy,
104− overriddenBy,
105−
106− -- * Relational pairing
107− splitR,
108−
109− -- ** Projections
110− fstR,
111− sndR,
112− -- ** Bifunctor
113− (><),
114− -- * Relational coproduct
115− eitherR,
116− -- ** Injections
117− i1,
118− i2,
119− -- ** Bifunctor
120− (-|-),
121−
122− -- * Relational "currying"
123− trans,
124− untrans,
125−
12662 -- * (Endo-)Relational properties
12763 reflexive,
12864 coreflexive,
@@ -136,26 +72,16 @@ module LAoP.Relation
13672 linearOrder,
13773 equivalence,
13874 partialEquivalence,
139− difunctional,
140−
141− -- * Conditionals
142− equalizer,
14375
14476 -- ** McCarthy's Conditional
145− predR,
146− guard,
147− cond,
77+ -- cond,
14878
14979 -- * Relational composition and lifting
150− iden,
80+ identity,
15181 comp,
15282 fromF,
15383 fromF',
15484
155− -- ** Relational application
156− pointAp,
157− pointApBool,
158−
15985 -- * Matrix printing
16086 pretty,
16187 prettyPrint
src/LAoP/Relation/Internal.hs+129−761
@@ -1,9 +1,6 @@
1−{-# LANGUAGE TypeFamilies #-}
2−{-# LANGUAGE ConstraintKinds #-}
31{-# LANGUAGE GADTs #-}
42{-# LANGUAGE UndecidableInstances #-}
53{-# LANGUAGE FlexibleContexts #-}
6−{-# LANGUAGE TypeApplications #-}
74{-# LANGUAGE ScopedTypeVariables #-}
85{-# LANGUAGE StandaloneDeriving #-}
96{-# LANGUAGE DerivingVia #-}
@@ -29,7 +26,7 @@
2926
3027module LAoP.Relation.Internal
3128 ( -- | This definition makes use of the fact that 'Void' is
32− -- isomorphic to 0 and 'One' to 1 and captures matrix
29+ -- isomorphic to 0 and '()' to 1 and captures matrix
3330 -- dimensions as stacks of 'Either's.
3431 --
3532 -- There exists two type families that make it easier to write
@@ -41,22 +38,11 @@ module LAoP.Relation.Internal
4138 Relation (..),
4239 Boolean,
4340
44− -- * Constraint type synonyms
45− Countable,
46− CountableDims,
47− CountableN,
48− CountableDimsN,
49− FLN,
50− Liftable,
51− Trivial,
52− TrivialP,
53−
5441 -- * Primitives
42+ empty,
5543 one,
56− join,
57− (|||),
58− fork,
59− (===),
44+ junc,
45+ split,
6046
6147 -- * Auxiliary type families
6248 I.FromNat,
@@ -66,75 +52,21 @@ module LAoP.Relation.Internal
6652 -- * Matrix construction and conversion
6753 I.FromLists,
6854 fromLists,
69− fromF',
70− fromF,
71− toRel,
7255 toLists,
7356 toList,
74− toBool,
75− pt,
76− belongs,
77− relationBuilder',
78− relationBuilder,
57+ matrixBuilder,
7958 zeros,
8059 ones,
8160 bang,
82− point,
8361
8462 -- * Relational operations
8563 conv,
8664 intersection,
8765 union,
8866 sse,
89− implies,
90− iff,
9167 ker,
9268 img,
9369
94− -- * Taxonomy of binary relations
95− injective,
96− entire,
97− simple,
98− surjective,
99− representation,
100− function,
101− abstraction,
102− injection,
103− surjection,
104− bijection,
105− domain,
106− range,
107−
108− -- * Function division
109− divisionF,
110−
111− -- * Relation division
112− divR,
113− divL,
114− divS,
115− shrunkBy,
116− overriddenBy,
117−
118− -- * Relational pairing
119− splitR,
120−
121− -- ** Projections
122− fstR,
123− sndR,
124− -- ** Bifunctor
125− (><),
126− -- * Relational coproduct
127− eitherR,
128− -- ** Injections
129− i1,
130− i2,
131− -- ** Bifunctor
132− (-|-),
133−
134− -- * Relational "currying"
135− trans,
136− untrans,
137−
13870 -- * (Endo-)Relational properties
13971 reflexive,
14072 coreflexive,
@@ -148,25 +80,15 @@ module LAoP.Relation.Internal
14880 linearOrder,
14981 equivalence,
15082 partialEquivalence,
151− difunctional,
152−
153− -- * Conditionals
154− equalizer,
15583
15684 -- ** McCarthy's Conditional
157− predR,
158− guard,
159− cond,
85+ -- cond,
16086
16187 -- * Relational composition and lifting
162− iden,
88+ identity,
16389 comp,
164− fromF',
16590 fromF,
166−
167− -- ** Relational application
168− pointAp,
169− pointApBool,
91+ fromF',
17092
17193 -- * Matrix printing
17294 pretty,
@@ -176,15 +98,15 @@ module LAoP.Relation.Internal
17698
17799import Data.Void
178100import qualified LAoP.Matrix.Internal as I
179−import LAoP.Utils.Internal
101+import LAoP.Utils
180102import Control.DeepSeq
103+import qualified Control.Category as C
104+import Data.Coerce
181105import Data.Bool
182106import GHC.TypeLits
183−import Prelude hiding (id, (.))
184107
185108-- | Boolean type synonym for working with boolean matrices
186109type Boolean = Natural 0 1
187−type Powerset a = List (List a)
188110
189111-- | Relation data type.
190112newtype Relation a b = R (I.Matrix Boolean (I.Normalize a) (I.Normalize b))
@@ -192,142 +114,113 @@ newtype Relation a b = R (I.Matrix Boolean (I.Normalize a) (I.Normalize b))
192114
193115deriving instance (Read (I.Matrix Boolean (I.Normalize a) (I.Normalize b))) => Read (Relation a b)
194116
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
117+-- | It isn't possible to implement the 'id' function so it's
118+-- implementation is 'undefined'. However 'comp' can be and this partial
119+-- class implementation exists just to make the code more readable.
120+--
121+-- Please use 'identity' instead.
122+instance C.Category Relation where
123+ id = undefined
124+ (.) = comp
211125
212126instance Num (Relation a b) where
213− -- | Matrix addition becomes Boolean matrix disjointion
127+ -- | Matrix addition becomes Boolean matrix disjunction
214128 (R a) + (R b) = R (I.orM a b)
215129
216130 -- | Matrix subtraction becomes Relational subtraction
217131 (R a) - (R b) = R (I.subM a b)
218132
219− -- | Matrix multiplication becomes Boolean matrix conjointion
133+ -- | Matrix multiplication becomes Boolean matrix conjunction
220134 (R a) * (R b) = R (I.andM a b)
221135
222− -- | Matrix negation becomes Boolean matrix negation
223− negate (R a) = R (I.negateM a)
224−
225136-- Type alias
226137type Zero = Void
227138type One = ()
228139
229140-- Primitives
230141
142+-- | Empty matrix constructor
143+empty :: Relation Zero Zero
144+empty = R I.Empty
145+
231146-- | Unit matrix constructor
232147one :: Boolean -> Relation One One
233148one = R . I.One
234149
235−-- | Boolean Matrix 'Join' constructor, also known as relational coproduct.
236−--
237−-- See 'eitherR'.
238−join :: Relation a c -> Relation b c -> Relation (Either a b) c
239−join (R a) (R b) = R (I.Join a b)
150+-- | Boolean Matrix 'Junc' constructor
151+junc :: (I.Normalize (Either a b) ~ Either (I.Normalize a) (I.Normalize b))
152+ => Relation a c -> Relation b c -> Relation (Either a b) c
153+junc (R a) (R b) = R (I.Junc a b)
240154
241155infixl 3 |||
242−-- | Boolean Matrix 'Join' constructor
243−--
244−-- See 'eitherR'.
156+-- | Boolean Matrix 'Junc' constructor
245157(|||) ::
158+ (I.Normalize (Either a b) ~ Either (I.Normalize a) (I.Normalize b)) =>
246159 Relation a c ->
247160 Relation b c ->
248161 Relation (Either a b) c
249−(|||) = join
162+(|||) = junc
250163
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)
164+-- | Boolean Matrix 'Split' constructor
165+split :: (I.Normalize (Either a b) ~ Either (I.Normalize a) (I.Normalize b))
166+ => Relation c a -> Relation c b -> Relation c (Either a b)
167+split (R a) (R b) = R (I.Split a b)
254168
255169infixl 2 ===
256−-- | Boolean Matrix 'Fork' constructor
170+-- | Boolean Matrix 'Split' constructor
257171(===) ::
172+ (I.Normalize (Either a b) ~ Either (I.Normalize a) (I.Normalize b)) =>
258173 Relation c a ->
259174 Relation c b ->
260175 Relation c (Either a b)
261−(===) = fork
176+(===) = split
262177
263178-- Construction
264179
265180-- | Build a matrix out of a list of list of elements. Throws a runtime
266181-- error if the dimensions do not match.
267−fromLists :: (FLN a b) => [[Boolean]] -> Relation a b
182+fromLists :: (I.FromLists Boolean (I.Normalize a) (I.Normalize b)) => [[Boolean]] -> Relation a b
268183fromLists = R . I.fromLists
269184
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.
279−relationBuilder ::
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
288−relationBuilder = R . I.matrixBuilder
185+-- | Matrix builder function. Constructs a matrix provided with
186+-- a construction function.
187+matrixBuilder ::
188+ (I.FromLists Boolean (I.Normalize a) (I.Normalize b), KnownNat (I.Count (I.Normalize a)), KnownNat (I.Count (I.Normalize b))) =>
189+ ((Int, Int) -> Boolean) ->
190+ Relation a b
191+matrixBuilder = R . I.matrixBuilder
289192
290193-- | Lifts functions to matrices with arbitrary dimensions.
291194--
292195-- NOTE: Be careful to not ask for a matrix bigger than the cardinality of
293196-- types @a@ or @b@ allows.
294−fromF' ::
295− ( Liftable a b,
296− CountableDimsN c d,
297− FLN d c
197+fromF ::
198+ ( Bounded a,
199+ Bounded b,
200+ Enum a,
201+ Enum b,
202+ Eq b,
203+ KnownNat (I.Count (I.Normalize c)),
204+ KnownNat (I.Count (I.Normalize d)),
205+ I.FromLists Boolean (I.Normalize d) (I.Normalize c)
298206 )
299207 => (a -> b) -> Relation c d
300−fromF' f = R (I.fromFRel' f)
208+fromF f = R (I.fromFRel f)
301209
302210-- | Lifts functions to matrices with dimensions matching @a@ and @b@
303211-- cardinality's.
304−fromF ::
305− ( Liftable a b,
306− CountableDimsN a b,
307− FLN b a
212+fromF' ::
213+ ( Bounded b,
214+ Bounded a,
215+ Enum a,
216+ Enum b,
217+ Eq b,
218+ KnownNat (I.Count (I.Normalize a)),
219+ KnownNat (I.Count (I.Normalize b)),
220+ I.FromLists Boolean (I.Normalize b) (I.Normalize a)
308221 )
309222 => (a -> b) -> Relation a b
310−fromF f = R (I.fromFRel f)
311−
312−-- | Lifts relation functions to 'Relation'
313−toRel ::
314− ( Liftable a b,
315− CountableDims a b,
316− FLN b a
317− )
318− => (a -> b -> Bool) -> Relation a b
319−toRel = R . I.toRel
320−
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
223+fromF' f = R (I.fromFRel' f)
331224
332225-- Conversion
333226
@@ -339,188 +232,46 @@ toLists (R m) = I.toLists m
339232toList :: Relation a b -> [Boolean]
340233toList (R m) = I.toList m
341234
342−-- | Converts a well typed 'Relation' to 'Bool'.
343−toBool :: Relation One One -> Bool
344−toBool r = case toList r of
345− [Nat 0] -> False
346− _ -> True
347−
348−-- | Power transpose.
349−--
350−-- Maps a relation to a set valued function.
351−pt ::
352− ( Liftable a b,
353− Eq a,
354− CountableDimsN a b,
355− FLN a One,
356− FLN b One
357− )
358− => Relation a b -> (a -> List b)
359−pt r a =
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
375−
376235-- Zeros Matrix
377236
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−-- @
237+-- | The zero matrix. A matrix wholly filled with zeros.
387238zeros ::
388− (FLN a b, CountableDimsN a b) =>
239+ (I.FromLists Boolean (I.Normalize a) (I.Normalize b), KnownNat (I.Count (I.Normalize a)), KnownNat (I.Count (I.Normalize b))) =>
389240 Relation a b
390−zeros = relationBuilder' (const (nat 0))
241+zeros = matrixBuilder (const (nat 0))
391242
392243-- Ones Matrix
393244
394−-- | The ones relation. A relation where every element of type @a@ relates
395−-- with every element of type @b@.
245+-- | The ones matrix. A matrix wholly filled with ones.
396246--
397−-- Also known as T (Top) Relation or universal Relation.
398−--
399−-- @
400−-- ⊥ ``sse`` R && R ``sse`` T == True
401−-- @
247+-- Also known as T (Top) matrix.
402248ones ::
403− (FLN a b, CountableDimsN a b) =>
249+ (I.FromLists Boolean (I.Normalize a) (I.Normalize b), KnownNat (I.Count (I.Normalize a)), KnownNat (I.Count (I.Normalize b))) =>
404250 Relation a b
405−ones = relationBuilder' (const (nat 1))
251+ones = matrixBuilder (const (nat 1))
406252
407253-- Bang Matrix
408254
409−-- | The T (Top) row vector relation.
255+-- | The T (Top) row vector matrix.
410256bang ::
411− (FLN a One, CountableN a) =>
257+ forall e a.
258+ (I.FromLists Boolean (I.Normalize a) (), KnownNat (I.Count (I.Normalize a))) =>
412259 Relation a One
413260bang = ones
414261
415−-- | Point constant relation
416−point ::
417− ( Bounded a,
418− Enum a,
419− Eq a,
420− CountableN a,
421− FLN a One
422− ) => a -> Relation One a
423−point = fromF . const
424−
425−-- iden Matrix
262+-- Identity Matrix
426263
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 (==))
264+-- | Identity matrix
265+identity ::
266+ (I.FromLists Boolean (I.Normalize a) (I.Normalize a), KnownNat (I.Count (I.Normalize a))) =>
267+ Relation a a
268+identity = matrixBuilder (bool (nat 0) (nat 1) . uncurry (==))
435269
436270-- | Relational composition
437−--
438−-- @
439−-- r `.` (s `.` p) = (r `.` s) `.` p
440−-- @
441−comp :: Relation b c -> Relation a b -> Relation a c
271+comp :: forall a b c . Relation b c -> Relation a b -> Relation a c
442272comp (R a) (R b) = R (I.compRel a b)
443273
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)@
496−pointAp ::
497− ( Liftable a b,
498− Eq a,
499− CountableDimsN a b,
500− FLN a One,
501− FLN b One
502− ) => a -> b -> Relation a b -> Relation One One
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
516−
517274-- | 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
524275conv :: Relation a b -> Relation b a
525276conv (R a) = R (I.tr a)
526277
@@ -528,481 +279,98 @@ conv (R a) = R (I.tr a)
528279sse :: Relation a b -> Relation a b -> Bool
529280sse a b = a <= b
530281
531−-- | Relational implication (the same as @'sse'@)
532−implies :: Relation a b -> Relation a b -> Relation a b
533−implies r s = negate r `union` s
534−
535−-- | Relational bi-implication
536−iff :: Relation a b -> Relation a b -> Bool
537−iff r s = r == s
538−
539282-- | Relational intersection
540283--
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−-- @
284+-- @M `inter` N = M * N@
547285intersection :: Relation a b -> Relation a b -> Relation a b
548286intersection a b = a * b
549287
550288-- | Relational union
551289--
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−-- @
290+-- @M `union` N = M + N - M * N
560291union :: Relation a b -> Relation a b -> Relation a b
561−union a b = a + b
292+union a b = a + b - a * b
562293
563294-- | Relation Kernel
564−--
565−-- @
566−-- 'ker' r == 'conv' r `.` r
567−-- 'ker' r == 'img' ('conv' r)
568−-- @
569295ker :: Relation a b -> Relation a a
570−ker r = conv r . r
296+ker r = conv r `comp` r
571297
572298-- | Relation Image
573−--
574−-- @
575−-- 'img' r == r `.` conv r
576−-- 'img' r == 'ker' ('conv' r)
577−-- @
578299img :: Relation a b -> Relation b b
579−img r = r . conv r
300+img r = r `comp` conv r
580301
581−-- | Function division. Special case of 'divS'.
582−--
583−-- NOTE: _This is only valid_ if @f@ and @g@ are 'function's, i.e. 'simple' and
584−-- 'entire'.
585−--
586−-- @'divisionF' f g == 'conv' g `.` f@
587−divisionF :: Relation a c -> Relation b c -> Relation a b
588−divisionF f g = conv g . f
302+-- | Properties of relations
589303
590−-- Taxonomy of binary relations
304+-- | A 'Relation' @r@ is reflexive iff @'identity' `'sse'` r@
305+reflexive :: (KnownNat (I.Count (I.Normalize a)), I.FromLists Boolean (I.Normalize a) (I.Normalize a)) => Relation a a -> Bool
306+reflexive r = identity <= r
591307
592−-- | A 'Relation' @r@ is 'simple' 'iff' @'coreflexive' ('img' r)@
593−simple :: (CountableN b, FLN b b) => Relation a b -> Bool
308+-- | A 'Relation' @r@ is coreflexive iff @r `'sse'` 'identity'@
309+coreflexive :: (KnownNat (I.Count (I.Normalize a)), I.FromLists Boolean (I.Normalize a) (I.Normalize a)) => Relation a a -> Bool
310+coreflexive r = r <= identity
311+
312+-- | A 'Relation' @r@ is simple iff @'coreflexive' ('img' r)@
313+simple :: (KnownNat (I.Count (I.Normalize b)), I.FromLists Boolean (I.Normalize b) (I.Normalize b)) => Relation a b -> Bool
594314simple = coreflexive . img
595315
596−-- | A 'Relation' @r@ is 'injective' 'iff' @'coreflexive' ('ker' r)@
597−injective :: (CountableN a, FLN a a) => Relation a b -> Bool
316+-- | A 'Relation' @r@ is injective iff @'coreflexive' ('ker' r)@
317+injective :: (KnownNat (I.Count (I.Normalize a)), I.FromLists Boolean (I.Normalize a) (I.Normalize a)) => Relation a b -> Bool
598318injective = coreflexive . ker
599319
600−-- | A 'Relation' @r@ is 'entire' 'iff' @'reflexive' ('ker' r)@
601−entire :: (CountableN a, FLN a a) => Relation a b -> Bool
320+-- | A 'Relation' @r@ is entire iff @'reflexive' ('ker' r)@
321+entire :: (KnownNat (I.Count (I.Normalize a)), I.FromLists Boolean (I.Normalize a) (I.Normalize a)) => Relation a b -> Bool
602322entire = reflexive . ker
603323
604−-- | A 'Relation' @r@ is 'surjective' 'iff' @'reflexive' ('img' r)@
605−surjective :: (CountableN b, FLN b b) => Relation a b -> Bool
324+-- | A 'Relation' @r@ is surjective iff @'reflexive' ('img' r)@
325+surjective :: (KnownNat (I.Count (I.Normalize b)), I.FromLists Boolean (I.Normalize b) (I.Normalize b)) => Relation a b -> Bool
606326surjective = reflexive . img
607327
608−-- | A 'Relation' @r@ is a 'function' 'iff' @'simple' r && 'entire' r@
609−--
610−-- A 'function' @f@ enjoys the following properties, where @r@ and @s@ are binary
611−-- relations:
612−--
613−-- @
614−-- f `.` r ``sse`` s == r ``sse`` f `.` s
615−-- r `.` f ``sse`` s == r ``sse`` s `.` f
616−-- @
617−function ::
618− ( CountableDimsN a b,
619− FLN a a,
620− FLN b b
621− )
622− => Relation a b -> Bool
623−function r = simple r && entire r
624−
625−-- | A 'Relation' @r@ is a 'representation' 'iff' @'injective' r && 'entire' r@
626−representation ::
627− ( CountableN a,
628− FLN a a
629− )
630− => Relation a b -> Bool
631−representation r = injective r && entire r
632−
633−-- | A 'Relation' @r@ is an 'abstraction' 'iff' @'surjective' r && 'simple' r@
634−abstraction ::
635− ( CountableN b,
636− FLN b b
637− )
638− => Relation a b -> Bool
639−abstraction r = surjective r && simple r
640−
641−-- | A 'Relation' @r@ is a 'surjection' 'iff' @'function' r && 'abstraction' r@
642−surjection ::
643− ( CountableDimsN a b,
644− FLN a a,
645− FLN b b
646− )
647− => Relation a b -> Bool
648−surjection r = function r && abstraction r
649−
650−-- | A 'Relation' @r@ is a 'injection' 'iff' @'function' r && 'representation' r@
651−injection ::
652− ( CountableDimsN a b,
653− FLN a a,
654− FLN b b
655− )
656− => Relation a b -> Bool
657−injection r = function r && representation r
658−
659−-- | A 'Relation' @r@ is an 'bijection' 'iff' @'injection' r && 'surjection' r@
660−bijection ::
661− ( CountableDimsN a b,
662− FLN b b,
663− FLN a a
664− ) => Relation a b -> Bool
665−bijection r = injection r && surjection r
666−
667−-- Properties of relations
668−
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
672−
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
676−
677−-- | A 'Relation' @r@ is 'transitive' 'iff' @(r `.` r) ``sse`` r@
328+-- | A 'Relation' @r@ is transitive iff @(r `'comp'` r) `'sse'` r@
678329transitive :: Relation a a -> Bool
679−transitive r = (r . r) `sse` r
330+transitive r = (r `comp` r) `sse` r
680331
681−-- | A 'Relation' @r@ is 'symmetric' 'iff' @r == 'conv' r@
332+-- | A 'Relation' @r@ is symmetric iff @r == r@
682333symmetric :: Relation a a -> Bool
683−symmetric r = r == conv r
334+symmetric r = r == r
684335
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
336+-- | A 'Relation' @r@ is anti-symmetric iff @(r `'intersection'` 'conv' r) `'sse'` 'identity'@
337+antiSymmetric :: (KnownNat (I.Count (I.Normalize a)), I.FromLists Boolean (I.Normalize a) (I.Normalize a)) => Relation a a -> Bool
338+antiSymmetric r = (r `intersection` conv r) `sse` identity
688339
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
340+-- | A 'Relation' @r@ is irreflexive iff @(r `'intersection'` identity) == 'zeros'@
341+irreflexive :: (KnownNat (I.Count (I.Normalize a)), I.FromLists Boolean (I.Normalize a) (I.Normalize a)) => Relation a a -> Bool
342+irreflexive r = (r `intersection` identity) == zeros
692343
693−-- | A 'Relation' @r@ is 'connected' 'iff' @(r ``union`` 'conv' r) == 'ones'@
694−connected :: (CountableN a, FLN a a) => Relation a a -> Bool
344+-- | A 'Relation' @r@ is connected iff @(r `'union'` 'conv' r) == 'ones'@
345+connected :: (KnownNat (I.Count (I.Normalize a)), I.FromLists Boolean (I.Normalize a) (I.Normalize a)) => Relation a a -> Bool
695346connected r = (r `union` conv r) == ones
696347
697−-- | A 'Relation' @r@ is a 'preorder' 'iff' @'reflexive' r && 'transitive' r@
698−preorder :: (CountableN a, FLN a a) => Relation a a -> Bool
348+-- | A 'Relation @r@ is a preorder iff @'reflexive' r && 'transitive' r@
349+preorder :: (KnownNat (I.Count (I.Normalize a)), I.FromLists Boolean (I.Normalize a) (I.Normalize a)) => Relation a a -> Bool
699350preorder r = reflexive r && transitive r
700351
701−-- | A 'Relation' @r@ is a partial-order 'iff' @'antiSymmetric' r && 'preorder' r@
702−partialOrder :: (CountableN a, FLN a a) => Relation a a -> Bool
352+-- | A 'Relation @r@ is a partial order iff @'antiSymmetric' r && 'preorder' r@
353+partialOrder :: (KnownNat (I.Count (I.Normalize a)), I.FromLists Boolean (I.Normalize a) (I.Normalize a)) => Relation a a -> Bool
703354partialOrder r = antiSymmetric r && preorder r
704355
705−-- | A 'Relation' @r@ is a linear-order 'iff' @'connected' r && 'partialOrder' r@
706−linearOrder :: (CountableN a, FLN a a) => Relation a a -> Bool
356+-- | A 'Relation @r@ is a linear order iff @'connected' r && 'partialOrder' r@
357+linearOrder :: (KnownNat (I.Count (I.Normalize a)), I.FromLists Boolean (I.Normalize a) (I.Normalize a)) => Relation a a -> Bool
707358linearOrder r = connected r && partialOrder r
708359
709−-- | A 'Relation' @r@ is an 'equivalence' 'iff' @'symmetric' r && 'preorder' r@
710−equivalence :: (CountableN a, FLN a a) => Relation a a -> Bool
360+-- | A 'Relation @r@ is an equivalence iff @'symmetric' r && 'preorder' r@
361+equivalence :: (KnownNat (I.Count (I.Normalize a)), I.FromLists Boolean (I.Normalize a) (I.Normalize a)) => Relation a a -> Bool
711362equivalence r = symmetric r && preorder r
712363
713−-- | A 'Relation' @r@ is a partial-equivalence 'iff' @'partialOrder' r && 'equivalence' r@
714−partialEquivalence :: (CountableN a, FLN a a) => Relation a a -> Bool
364+-- | A 'Relation @r@ is a partial equivalence iff @'partialOrder' r && 'equivalence' r@
365+partialEquivalence :: (KnownNat (I.Count (I.Normalize a)), I.FromLists Boolean (I.Normalize a) (I.Normalize a)) => Relation a a -> Bool
715366partialEquivalence r = partialOrder r && equivalence r
716367
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−
722−-- Relational pairing
723−
724−-- | Relational pairing.
725−--
726−-- NOTE: That this is not a true categorical product, see for instance:
727−--
728−-- @
729−-- | 'fstR' `.` 'splitR' a b ``sse`` a
730−-- 'splitR' a b <=> |
731−-- | 'sndR' `.` 'splitR' a b ``sse`` b
732−-- @
733−--
734−-- __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−-- @
745−splitR ::
746− ( CountableDimsN a b,
747− CountableN (a, b),
748− FLN (a, b) a,
749− FLN (a, b) b,
750− TrivialP a b
751− )
752− => Relation c a -> Relation c b -> Relation c (a, b)
753−splitR (R f) (R g) = R (I.kr f g)
754−
755−-- | Relational pairing first component projection
756−--
757−-- @
758−-- 'fstR' `.` 'splitR' r s ``sse`` r
759−-- @
760−fstR ::
761− forall a b .
762− ( CountableDimsN a b,
763− CountableN (a, b),
764− FLN (a, b) a,
765− TrivialP a b
766− )
767− => Relation (a, b) a
768−fstR = R (I.fstM @Boolean @(I.Normalize a) @(I.Normalize b))
769−
770−-- | Relational pairing second component projection
771−--
772−-- @
773−-- 'sndR' `.` 'splitR' r s ``sse`` s
774−-- @
775−sndR ::
776− forall a b .
777− ( CountableDimsN a b,
778− CountableN (a, b),
779− FLN (a, b) b,
780− TrivialP a b
781− )
782− => Relation (a, b) b
783−sndR = R (I.sndM @Boolean @(I.Normalize a) @(I.Normalize b))
784−
785−-- Relational pairing functor
786−
787−infixl 4 ><
788−-- | Relational pairing functor
789−--
790−-- @
791−-- r '><' s == 'splitR' (r `.` fstR) (s `.` sndR)
792−-- (r '><' s) `.` (p '><' q) == (r `.` p) '><' (s `.` q)
793−-- @
794−(><) ::
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
804− )
805− => Relation a b -> Relation c d -> Relation (a, c) (b, d)
806−(><) (R a) (R b) = R ((I.><) a b)
807−
808−-- Relational co-products
809−
810−-- | Relational coproduct.
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
827−
828−-- | Relational coproduct first component injection
829−--
830−-- @
831−-- 'img' 'i1' ``union`` 'img' 'i2' == 'id'
832−-- 'i1' `.` 'i2' = 'zeros'
833−-- @
834−i1 ::
835− ( CountableDimsN a b,
836− FLN b a,
837− FLN a a
838− )
839− => Relation a (Either a b)
840−i1 = R I.i1
841−
842−-- | Relational coproduct second component injection
843−--
844−-- @
845−-- 'img' 'i1' ``union`` 'img' 'i2' == 'id'
846−-- 'i1' `.` 'i2' = 'zeros'
847−-- @
848−i2 ::
849− ( CountableDimsN a b,
850− FLN a b,
851− FLN b b
852− )
853− => Relation b (Either a b)
854−i2 = R I.i2
855−
856−infixl 5 -|-
857−
858−-- | Relational coproduct functor.
859−--
860−-- @
861−-- r '-|-' s == 'eitherR' ('i1' `.` r) ('i2' `.` s)
862−-- @
863−(-|-) ::
864− ( CountableDimsN b d,
865− FLN b b,
866− FLN d b,
867− FLN b d,
868− FLN d d
869− )
870− => Relation a b -> Relation c d -> Relation (Either a c) (Either b d)
871−(-|-) (R a) (R b) = R ((I.-|-) a b)
872−
873−-- Relational "Currying"
874−
875−-- | 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.
880−trans ::
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
892− )
893− => Relation (a, b) c -> Relation a (c, b)
894−trans r = splitR r sndR . conv fstR
895−
896−-- | 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.
901−untrans ::
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
913− )
914− => Relation a (c, b) -> Relation (a, b) c
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
999−
1000368-- Relation pretty print
1001369
1002370-- | Relation pretty printing
1003−pretty :: (CountableDimsN a b) => Relation a b -> String
371+pretty :: (KnownNat (I.Count (I.Normalize a))) => Relation a b -> String
1004372pretty (R a) = I.pretty a
1005373
1006374-- | Relation pretty printing
1007−prettyPrint :: (CountableDimsN a b) => Relation a b -> IO ()
375+prettyPrint :: (KnownNat (I.Count (I.Normalize a))) => Relation a b -> IO ()
1008376prettyPrint (R a) = I.prettyPrint a
src/LAoP/Utils.hs−6
@@ -94,12 +94,6 @@ module LAoP.Utils
9494 coerceNat,
9595 coerceNat2,
9696 coerceNat3,
97−
98− -- * List data type
99− List (..),
100−
101− -- * Category type-class
102− Category(..)
10397 )
10498where
10599
src/LAoP/Utils/Internal.hs+74−94
@@ -1,15 +1,84 @@
1−{-# LANGUAGE TypeFamilies #-}
2−{-# LANGUAGE DeriveGeneric #-}
31{-# LANGUAGE TypeApplications #-}
42{-# LANGUAGE DataKinds #-}
53{-# LANGUAGE FlexibleInstances #-}
64{-# LANGUAGE GeneralizedNewtypeDeriving #-}
5+{-# LANGUAGE KindSignatures #-}
76{-# LANGUAGE ScopedTypeVariables #-}
87
98module LAoP.Utils.Internal
10− (
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+ --
1180 -- * 'Natural' data type
12− Natural(..),
81+ Natural,
1382 nat,
1483
1584 -- * Coerce auxiliar functions to help promote 'Int' typed functions to
@@ -17,31 +86,19 @@ module LAoP.Utils.Internal
1786 coerceNat,
1887 coerceNat2,
1988 coerceNat3,
20−
21− -- * 'List' data type
22− List (..),
23−
24− -- * Category type class
25− Category(..)
2689 )
2790where
2891
2992import Data.Coerce
3093import Data.Proxy
31−import Data.List
32−import Data.Maybe
3394import GHC.TypeLits
3495import Control.DeepSeq
35−import GHC.Generics
36−import Data.Kind
37−import Prelude hiding (id, (.))
38−import qualified Prelude
3996
4097-- | Wrapper around 'Int's that have a restrictive semantic associated.
4198-- A value of type @'Natural' n m@ can only be instanciated with some 'Int'
4299-- @i@ that's @n <= i <= m@.
43100newtype Natural (start :: Nat) (end :: Nat) = Nat Int
44− deriving (Show, Read, Eq, Ord, NFData, Generic)
101+ deriving (Show, Read, Eq, Ord, NFData)
45102
46103-- | Throws a runtime error if any of the operations overflows or
47104-- underflows.
@@ -117,80 +174,3 @@ instance
117174 fstI = fromEnum a
118175 sndI = fromEnum b
119176 in fstI * lengthB + sndI
120−
121−instance
122− ( Bounded a,
123− Bounded b
124− ) => Bounded (Either a b)
125− where
126− minBound = Left (minBound :: a)
127− maxBound = Right (maxBound :: b)
128−
129−instance
130− ( Enum a,
131− Bounded a,
132− Enum b,
133− Bounded b
134− ) => Enum (Either a b)
135− where
136− toEnum i =
137− let la = fmap Left ([minBound..maxBound] :: [a])
138− lb = fmap Right ([minBound..maxBound] :: [b])
139− in (la ++ lb) !! i
140−
141− fromEnum (Left a) = fromEnum a
142− 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.yamldeleted−1
@@ -1 +0,0 @@
1−resolver: lts-15.5
stack.yaml+66−1
@@ -1 +1,66 @@
1−resolver: lts-14.3
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
stack.yaml.lock+4−4
@@ -6,7 +6,7 @@
66packages: []
77snapshots:
88- completed:
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
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
test/Examples/Quantum.hsdeleted−31
@@ -1,31 +0,0 @@
1−{-# LANGUAGE StandaloneDeriving #-}
2−module Examples.Quantum where
3−
4−import LAoP.Utils
5−import LAoP.Matrix.Type
6−import Data.Complex
7−import Prelude hiding (id, (.))
8−
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)
test/Examples/Readme.hsdeleted−184
@@ -1,184 +0,0 @@
1−{-# LANGUAGE GADTs #-}
2−{-# LANGUAGE DeriveGeneric #-}
3−{-# LANGUAGE FlexibleContexts #-}
4−{-# LANGUAGE TypeApplications #-}
5−{-# LANGUAGE DataKinds #-}
6−
7−module Examples.Readme
8− ( exec
9− )
10− where
11−
12−import LAoP.Matrix.Type
13−import qualified LAoP.Relation as R
14−import LAoP.Utils
15−import LAoP.Dist
16−import GHC.TypeLits
17−import Data.Coerce
18−import qualified GHC.Generics as G
19−import Prelude hiding (id, (.))
20−
21−-- Monty Hall Problem
22−data Outcome = Win | Lose
23− deriving (Bounded, Enum, Eq, Show, G.Generic)
24−
25−switch :: Outcome -> Outcome
26−switch Win = Lose
27−switch Lose = Win
28−
29−firstChoice :: Matrix Double () Outcome
30−firstChoice = col [1/3, 2/3]
31−
32−secondChoice :: Matrix Double Outcome Outcome
33−secondChoice = fromF switch
34−
35−-- Dice sum
36−
37−type SS = Natural 1 6 -- Sample Space
38−
39−sumSS :: SS -> SS -> Natural 2 12
40−sumSS = coerceNat (+)
41−
42−sumSSM = fromF (uncurry sumSS)
43−
44−condition :: (Int, Int) -> Int -> Int
45−condition (fst, snd) thrd = if fst == snd
46− then fst * 3
47− else fst + snd + thrd
48−
49−conditionSS :: (SS, SS) -> SS -> Natural 3 18
50−conditionSS = coerceNat2 condition
51−
52−conditionalThrows = fromF (uncurry conditionSS) . kr (kr die die) die
53−
54−die :: Matrix Double () SS
55−die = col $ map (const (1/6)) [nat @1 @6 1 .. nat 6]
56−
57−-- 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)
63−
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
72−
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
92−
93−tag f = kr f id
94−
95−state g s r = tag g . tag s . r
96−
97−grass_wet :: Matrix Double () (G, (S, R)) -> Matrix Double One One
98−grass_wet state = row [0,1] . fstM . state
99−
100−rainning :: Matrix Double (G, (S, R)) One
101−rainning = row [0,1] . sndM . sndM
102−
103−-- Alcuin Puzzle
104−
105−data Being = Farmer | Fox | Goose | Beans
106− deriving (Bounded, Enum, Eq, Show, G.Generic)
107−
108−data Bank = LeftB | RightB
109− deriving (Bounded, Enum, Eq, Show, G.Generic)
110−
111−eats :: Being -> Being -> Bool
112−eats Fox Goose = True
113−eats Goose Beans = True
114−eats _ _ = False
115−
116−eatsR :: R.Relation Being Being
117−eatsR = R.toRel eats
118−
119−cross :: Bank -> Bank
120−cross LeftB = RightB
121−cross RightB = LeftB
122−
123−crossR :: R.Relation Bank Bank
124−crossR = R.fromF cross
125−
126−-- | Initial state, everyone in the left bank
127−locationLeft :: Being -> Bank
128−locationLeft _ = LeftB
129−
130−locationLeftR :: R.Relation Being Bank
131−locationLeftR = R.fromF locationLeft
132−
133−-- | Initial state, everyone in the right bank
134−locationRight :: Being -> Bank
135−locationRight _ = RightB
136−
137−locationRightR :: R.Relation Being Bank
138−locationRightR = R.fromF locationRight
139−
140−-- Properties
141−
142−-- Being at the same bank
143−sameBank :: R.Relation Being Bank -> R.Relation Being Being
144−sameBank = R.ker
145−
146−-- Risk of somebody eating somebody else
147−canEat :: R.Relation Being Bank -> R.Relation Being Being
148−canEat w = sameBank w `R.intersection` eatsR
149−
150−-- "Starvation" property.
151−inv :: R.Relation Being Bank -> Bool
152−inv w = (w `R.comp` canEat w) `R.sse` (w `R.comp` farmer)
153− where
154− farmer :: R.Relation Being Being
155− farmer = R.fromF (const Farmer)
156−
157−-- Arbitrary state
158−bankState :: Being -> Bank -> Bool
159−bankState Farmer LeftB = True
160−bankState Fox LeftB = True
161−bankState Goose RightB = True
162−bankState Beans RightB = True
163−bankState _ _ = False
164−
165−bankStateR :: R.Relation Being Bank
166−bankStateR = R.toRel bankState
167−
168−-- Main
169−exec :: IO ()
170−exec = do
171− putStrLn "Monty Hall Problem solution:"
172− prettyPrint (secondChoice . firstChoice)
173− putStrLn "\n Sum of dices probability:"
174− prettyPrint (sumSSM . kr die die)
175− putStrLn "\n Conditional dice throw:"
176− prettyPrint conditionalThrows
177− putStrLn "\n Checking that the last result is indeed a distribution: "
178− prettyPrint (bang . sumSSM . kr die die)
179− putStrLn "\n Probability of grass being wet:"
180− prettyPrint (grass_wet (state grass sprinkler rain))
181− putStrLn "\n Probability of rain:"
182− prettyPrint (rainning . state grass sprinkler rain)
183− putStrLn "\n Is the arbitrary state a valid state? (Alcuin Puzzle)"
184− print (inv bankStateR)
test/Examples/Spreadsheets.hsdeleted−47
@@ -1,47 +0,0 @@
1−{-# LANGUAGE DeriveGeneric #-}
2−
3−module Examples.Spreadsheets
4−
5−import LAoP.Utils
6−import LAoP.Matrix.Type
7−import GHC.Generics
8−import Prelude hiding (id, (.))
9−
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+1−7
@@ -1,8 +1,2 @@
1−module Main (main) where
2−
3−import qualified Examples.Readme as RD
4−
51main :: IO ()
6−main = do
7− putStrLn ("Testing if README works" :: String)
8− RD.exec
2+main = putStrLn "Test suite not yet implemented"