git.iko.soy/laop
on master help sign in
swap
eea623165 ahead, 0 behind
.ghc.environment.x86_64-linux-8.6.5deleted−17
since splitsnapshots
unifiedsplit
@@ -1,17 +0,0 @@
1−-- This is a GHC environment file written by cabal. This means you can
2−-- run ghc or ghci and get the environment of the project as a whole.
3−-- But you still need to use cabal repl $target to get the environment
4−-- of specific components (libs, exes, tests etc) because each one can
5−-- have its own source dirs, cpp flags etc.
6−--
7−clear-package-db
8−global-package-db
9−package-db /home/bolt/.cabal/store/ghc-8.6.5/package.db
10−package-db packagedb/ghc-8.6.5
11−package-id laop-0.1.0.0-inplace
12−package-id base-4.12.0.0
13−package-id ghc-prim-0.5.3
14−package-id rts
15−package-id integer-gmp-1.0.2.0
16−package-id deepseq-1.4.4.0
17−package-id array-0.5.3.0
.github/workflows/ci.ymlnew file+43
@@ -0,0 +1,43 @@
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+54−2
@@ -1,3 +1,55 @@
1+### Haskell
2+dist
3+dist-*
4+cabal-dev
5+*.o
6+*.hi
7+*.chi
8+*.chs.h
9+*.dyn_o
10+*.dyn_hi
11+*.prof
12+*.aux
13+*.hp
14+*.eventlog
15+.virtualenv
16+.hsenv
17+.hpc
18+.cabal-sandbox/
19+cabal.sandbox.config
20+cabal.config
21+cabal.project.local
22+.ghc.environment.*
23+.HTF/
24+# Stack
1.stack-work/
25.stack-work/
2−laop.cabal
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]
3−*~
34+*~
35+tags
36+
37+# IntellijIDEA
38+.idea/
39+.ideaHaskellLib/
40+*.iml
41+
42+# Atom
43+.haskell-ghc-mod.json
44+
45+# VS
46+.vscode/
47+
48+# Emacs
49+*#
50+.dir-locals.el
51+TAGS
52+
53+# other
54+.DS_Store
55+hackage.sh
.travis.ymlnew file+47
@@ -0,0 +1,47 @@
1+sudo: true
2+language: haskell
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.mdnew file+17
@@ -0,0 +1,17 @@
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.mddeleted−3
@@ -1,3 +0,0 @@
1−# Changelog for laop
2−
3−## Unreleased changes
LICENSE+17−26
@@ -1,30 +1,21 @@
1−Copyright Armando Santos (c) 2019
1+MIT License
2
2
3−All rights reserved.
3+Copyright (c) 2020 Armando Santos
4
4
5−Redistribution and use in source and binary forms, with or without
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
6−modification, are permitted provided that the following conditions are met:
10+furnished to do so, subject to the following conditions:
7
11
8− * Redistributions of source code must retain the above copyright
12+The above copyright notice and this permission notice shall be included in all
9− notice, this list of conditions and the following disclaimer.
13+copies or substantial portions of the Software.
10
14
11− * Redistributions in binary form must reproduce the above
15+THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR
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
16+IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY,
23−A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT
17+FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE
24−OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL,
18+AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER
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
19+LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM,
29−(INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE
20+OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE
30−OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
21+SOFTWARE.
README.md+107−24
@@ -1,5 +1,11 @@
1# laop - Linear Algebra of Programming library
1# laop - Linear Algebra of Programming library
2
2
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+
3The LAoP discipline generalises relations and functions treating them as
9The LAoP discipline generalises relations and functions treating them as
4Boolean matrices and in turn consider these as arrows.
10Boolean matrices and in turn consider these as arrows.
5
11
@@ -10,33 +16,38 @@ motivation behind the library, the underlying theory, and implementation details
10This module offers many of the combinators mentioned in the work of
16This module offers many of the combinators mentioned in the work of
11[Macedo (2012)](https://repositorium.sdum.uminho.pt/handle/1822/22894) and [Oliveira (2012)](https://pdfs.semanticscholar.org/ccf5/27fa9179081223bffe8067edd81948644fc0.pdf).
17[Macedo (2012)](https://repositorium.sdum.uminho.pt/handle/1822/22894) and [Oliveira (2012)](https://pdfs.semanticscholar.org/ccf5/27fa9179081223bffe8067edd81948644fc0.pdf).
12
18
13−See the candidate package in hackage [here](https://hackage.haskell.org/package/laop-0.1.0.0/candidate)
19+See the package in hackage [here](https://hackage.haskell.org/package/laop-0.1.1.0)
20+
21+A Functional Pearl has been written and can be regarded as the [reference document](https://github.com/bolt12/tymfgg-pearl) for this library.
14
22
15## Features
23## Features
16
24
17−This library offers:
25+This library offers 3 main matrix programming modules:
18−
26+
19−- An internal representation that uses normal datatypes (`Void`, `()`, `Either`) for matrix dimensions and two
27+- One in which matrices are typed with type level natural numbers;
20− type families `FromNat` and `Count` to make it easier to work with these type of matrices.
28+- One in which matrices are typed with arbitrary generic data types;
21−- A module that uses generalised types for the dimensions and is just a newtype wrapper
29+- One in which matrices are regarded as relations, i.e. boolean matrices;
22− around the internal matrix data type.
30+
23−- Other that uses type level naturals for the dimensions and is just a newtype wrapper
31+There's also an experimental module that uses matrices to represent probability
24− around the internal matrix data type.
32+distributions.
25−- A very simple Probabilistic Programming module and several functions and data types to
33+
26− make it easier to deal with sample space.
34+The most interesting feature is that matrices are represented as an inductive data type.
27−
35+Given this formulation, matrix algorithms can be expressed in a much more elegant and
28−Given this, this new matrix formulation compared to other libraries one has much more advantages, such as:
36+calculational style than the traditional vector of vectors representation. This data type
29−
37+guarantees that a matrix will always have valid dimensions. It can also express block matrix
30−- Has an inductive definition enabling writing matrix manipulation functions in a much more elegant and calculational way;
38+computations naturally, which leads to total, efficient and statically typed manipulation
31−- Statically typed dimensions;
39+and transformation functions.
32−- Polymorphic data type dimensions;
40+
33−- Polymorphic matrix content;
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.
34−- Awesome dimension type inference;
42+
35−- Fast type natural conversion via `FromNat` type family;
43+Given this, this new matrix formulation compared to other libraries:
36−- Matrix `Junc` and `Split`-ing in O(1);
44+
37−- Matrix composition takes advantage of divide-and-conquer and fusion laws.
45+- Is more compositional and polymorphic and does not have partial matrix manipulation functions (hence less chances for usage errors);
38−
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+
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.
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).
40
51
41## Notes
52## Notes
42
53
@@ -118,6 +129,73 @@ grass_wet = row [0,1] . kp1
118rainning :: Matrix Double (Bool, (Bool, Bool)) One
129rainning :: Matrix Double (Bool, (Bool, Bool)) One
119rainning = row [0,1] . kp2 . kp2
130rainning = row [0,1] . kp2 . kp2
120
131
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+
121main :: IO ()
199main :: IO ()
122main = do
200main = do
123 putStrLn "Monty Hall Problem solution:"
201 putStrLn "Monty Hall Problem solution:"
@@ -132,6 +210,8 @@ main = do
132 prettyPrint (grass_wet . state)
210 prettyPrint (grass_wet . state)
133 putStrLn "\n Probability of rain:"
211 putStrLn "\n Probability of rain:"
134 prettyPrint (rainning . state)
212 prettyPrint (rainning . state)
213+ putStrLn "\n Is the arbitrary state a valid state? (Alcuin Puzzle)"
214+ print (inv bankStateR)
135```
215```
136
216
137```Shell
217```Shell
@@ -190,4 +270,7 @@ Monty Hall Problem solution:
190┌ ┐
270┌ ┐
191│ 0.2 │
271│ 0.2 │
192└ ┘
272└ ┘
273+
274+Is the arbitrary state a valid state? (Alcuin Puzzle)
275+False
193```
276```
Setup.hsdeleted−2
@@ -1,2 +0,0 @@
1−import Distribution.Simple
2−main = defaultMain
appveyor.ymlnew file+34
@@ -0,0 +1,34 @@
1+clone_folder: "c:\\WORK"
2+clone_depth: 5
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.hsnew file+175
@@ -0,0 +1,175 @@
1+{-# LANGUAGE KindSignatures #-}
2+{-# LANGUAGE GeneralizedNewtypeDeriving #-}
3+{-# LANGUAGE DerivingVia #-}
4+{-# LANGUAGE DataKinds #-}
5+{-# LANGUAGE BangPatterns #-}
6+{-# LANGUAGE TypeApplications #-}
7+{-# LANGUAGE FlexibleContexts #-}
8+{-# LANGUAGE AllowAmbiguousTypes #-}
9+{-# LANGUAGE ScopedTypeVariables #-}
10+
11+module Main (main) where
12+
13+import LAoP.Dist.Internal
14+import LAoP.Utils
15+import LAoP.Matrix.Type hiding (CountableN, Countable, FLN)
16+import qualified LAoP.Matrix.Type as T (FLN)
17+import Criterion.Main
18+import Control.DeepSeq
19+import Test.QuickCheck
20+import GHC.TypeLits
21+import Data.Proxy
22+import Prelude hiding (id, (.))
23+
24+selectM2 ::
25+ ( Num e,
26+ T.FLN b b,
27+ CountableN b
28+ ) => Matrix e cols (Either a b) -> Matrix e a b -> Matrix e cols b
29+selectM2 m y = join y iden `comp` m
30+
31+selectD2 ::
32+ ( FLN b b,
33+ CountableN b
34+ ) => Dist (Either a b) -> Matrix Prob a b -> Dist b
35+selectD2 (D d) m = D (join m iden `comp` d)
36+
37+-- Composition with iden
38+compId m = comp iden m
39+
40+randomDist :: forall a . (Countable a, FLN () a) => Gen (Dist a)
41+randomDist = do
42+ let size = fromInteger (natVal (Proxy :: Proxy (Count a)))
43+ l <- vectorOf size (arbitrary :: Gen Prob)
44+ let ln = normalize l
45+ lr = map (:[]) ln
46+ m = fromLists lr
47+ return (D m)
48+
49+randomMatrix :: forall a b . (CountableDims a b, FLN a b) => Gen (Matrix Prob a b)
50+randomMatrix = do
51+ let cols = fromInteger (natVal (Proxy :: Proxy (Count a)))
52+ rows = fromInteger (natVal (Proxy :: Proxy (Count b)))
53+ l <- vectorOf (cols * rows) arbitrary
54+ let lr = buildList l cols
55+ m = fromLists lr
56+ return m
57+
58+buildList [] _ = []
59+buildList l r = take r l : buildList (drop r l) r
60+
61+normalize :: [Prob] -> [Prob]
62+normalize l = let l' = map abs l
63+ s = sum l'
64+ in map (/ s) l'
65+
66+-- Probability
67+newtype Probability = P Double
68+ deriving (Num, Show, Fractional, NFData) via Double
69+newtype Dist' a = D' { unD :: [(a,Probability)] }
70+ deriving (Show, NFData)
71+
72+instance Functor Dist' where
73+ fmap f (D' d) = D' [(f x,p) | (x,p) <- d]
74+
75+instance Applicative Dist' where
76+ pure x = D' [(x, 1)]
77+ fm <*> m = D' [(f x,q*p) | (f,p) <- unD fm, (x,q) <- unD m]
78+
79+class Applicative f => Selective f where
80+ select :: f (Either a b) -> f (a -> b) -> f b
81+
82+instance Selective Dist' where
83+ select x y = (\e f -> either f id e) <$> x <*> y -- selectA
84+
85+instance Monad Dist' where
86+ return = pure
87+ (D' d) >>= f = D' [(y,q*p) | (x,p) <- d, (y,q) <- unD (f x)]
88+
89+normalize2 :: forall a . (Enum a, Bounded a) => [Probability] -> [(a, Probability)]
90+normalize2 l = let l' = map abs l
91+ as = [minBound .. maxBound]
92+ s = sum l'
93+ probs = map (/ s) l'
94+ in zip as probs
95+
96+randomDist2 :: forall a . (Countable a, Enum a, Bounded a) => Gen (Dist' a)
97+randomDist2 = do
98+ let size = fromInteger (natVal (Proxy :: Proxy (Count a)))
99+ l <- vectorOf size (arbitrary :: Gen Prob)
100+ let ln = normalize2 @a (map P l)
101+ return (D' ln)
102+
103+normalize3 :: forall a . [a] -> [Probability] -> [(a, Probability)]
104+normalize3 as l = let s = sum l
105+ probs = map (/ s) l
106+ in zip as probs
107+
108+randomDistF :: forall a b . (CountableDims a b, CoArbitrary a, Arbitrary b) => Gen (Dist' (a -> b))
109+randomDistF = do
110+ let a = fromInteger (natVal (Proxy :: Proxy (Count a)))
111+ b = fromInteger (natVal (Proxy :: Proxy (Count b)))
112+ size = a * b
113+ l <- vectorOf size (arbitrary :: Gen Prob)
114+ l2 <- vectorOf size (arbitrary :: Gen (a -> b))
115+ let !ln = normalize3 l2 (map P l)
116+ return (D' ln)
117+
118+instance CoArbitrary (Natural a b)
119+
120+instance forall (a :: Nat) (b :: Nat). (KnownNat a, KnownNat b) => Arbitrary (Natural a b)
121+ where
122+ arbitrary =
123+ let bottom = fromInteger (natVal (Proxy :: Proxy a))
124+ top = fromInteger (natVal (Proxy :: Proxy b))
125+ in do
126+ x <- arbitrary `suchThat` (\n -> n >= bottom && n <= top)
127+ return (nat x)
128+
129+setupEnv = do
130+ m11 <- generate (resize 1 (randomMatrix @(Natural 0 10) @(Natural 0 10) ))
131+ m12 <- generate (resize 1 (randomMatrix @(Natural 0 10) @(Natural 0 10) ))
132+ m21 <- generate (resize 1 (randomMatrix @(Natural 0 100) @(Natural 0 100) ))
133+ m22 <- generate (resize 1 (randomMatrix @(Natural 0 100) @(Natural 0 100) ))
134+ m31 <- generate (resize 1 (randomMatrix @(Natural 0 200) @(Natural 0 200) ))
135+ m32 <- generate (resize 1 (randomMatrix @(Natural 0 200) @(Natural 0 200) ))
136+ return (m11, m12, m21, m22, m31, m32)
137+
138+setupEnv2 = do
139+ m21 <- generate (resize 1 (randomMatrix @(Natural 0 100) @(Natural 0 100) ))
140+ m40 <- generate (resize 1 (randomMatrix @(Natural 0 100) @(Either (Natural 0 100) (Natural 0 100) )))
141+ dist <- generate (resize 1 (randomDist @(Either (Natural 0 100) (Natural 0 100)) ))
142+ dist2 <- generate (resize 1 (randomMatrix @(Natural 0 100) @(Natural 0 100) ))
143+ distList1 <- generate (resize 1 (randomDist2 @(Either (Natural 0 100) (Natural 0 100))))
144+ distList2 <- generate (resize 1 (randomDistF @(Natural 0 100) @(Natural 0 100)))
145+ return (m21, m40, dist, dist2, distList1, distList2)
146+
147+main :: IO ()
148+main = defaultMain [
149+ env setupEnv $ \ ~(m11, m12, m21, m22, m31, m32) -> bgroup "Matrix Composition" [
150+ bgroup "10x10" [
151+ bench "WHNF - 10x10" $ whnf (comp m11) m12
152+ , bench "NF - 10x10" $ nf (comp m11) m12
153+ ],
154+ bgroup "100x100" [
155+ bench "WHNF - 100x100" $ whnf (comp m21) m22
156+ , bench "NF - 100x100" $ nf (comp m21) m22
157+ ],
158+ bgroup "200x200" [
159+ bench "WHNF - 200x200" $ whnf (comp m31) m32
160+ , bench "NF - 200x200" $ nf (comp m31) m32
161+ ],
162+ bgroup "200x200 - RULES" [
163+ bench "No rules - 200x200" $ nf (comp m21) iden
164+ , bench "Rules - 200x200" $ nf compId m21
165+ ] ],
166+ env setupEnv2 $ \ ~(m21, m40, dist, dist2, dl1, dl2) -> bgroup "Matrix vs List - `select`" [
167+ bgroup "Distribution `select` - 100+100 / 100x100" [
168+ bench "List Distribution - Applicative version" $ nf (select dl1) dl2
169+ , bench "Matrix Distribution - Applicative version" $ nf (selectD2 dist) dist2
170+ , bench "Matrix Distribution - Selective version" $ nf (selectD dist) dist2
171+ ],
172+ bgroup "Matrix `select` - 100x(100+100) / 100x100" [
173+ bench "Applicative version" $ nf (selectM2 m40) m21
174+ , bench "Selective version" $ nf (selectM m40) m21
175+ ] ] ]
hackage.shdeleted−10
@@ -1,10 +0,0 @@
1−#!/bin/sh
2−set -e
3−
4−dir=$(mktemp -d dist-docs.XXXXXX)
5−trap 'rm -r "$dir"' EXIT
6−
7−# assumes cabal 2.4 or later
8−cabal v2-haddock --builddir="$dir" --haddock-for-hackage --enable-doc
9−
10−cabal upload -d $dir/*-docs.tar.gz
laop-0.1.0.0-docs.tar.gzdeleted

Binary file not shown.

laop.cabalnew file+89
@@ -0,0 +1,89 @@
1+cabal-version: 2.4
2+name: laop
3+version: 0.1.1.1
4+synopsis: Matrix programming library
5+description: Matrix programming library that uses a type-safe inductive definition
6+ inspired by the Linear Algebra of Programming
7+homepage: https://github.com/bolt12/laop
8+bug-reports: https://github.com/bolt12/laop/issues
9+license: MIT
10+license-file: LICENSE
11+author: Armando Santos
12+maintainer: Armando Santos <armandoifsantos@gmail.com>
13+copyright: 2020 Armando Santos
14+category: Data
15+build-type: Simple
16+extra-doc-files: README.md
17+ CHANGELOG.md
18+tested-with: GHC == 8.6.5
19+ GHC == 8.8.3
20+
21+source-repository head
22+ type: git
23+ location: https://github.com/bolt12/laop.git
24+
25+common common-options
26+ build-depends: base >= 4.12.0.0 && < 5,
27+ deepseq
28+
29+ ghc-options: -Wall
30+ -Wcompat
31+ -Widentities
32+ -Wincomplete-uni-patterns
33+ -Wincomplete-record-updates
34+ if impl(ghc >= 8.0)
35+ ghc-options: -Wredundant-constraints
36+ if impl(ghc >= 8.2)
37+ ghc-options: -fhide-source-paths
38+ if impl(ghc >= 8.4)
39+ ghc-options: -Wmissing-export-lists
40+ -Wpartial-fields
41+ if impl(ghc >= 8.8)
42+ ghc-options: -Wmissing-deriving-strategies
43+
44+ default-language: Haskell2010
45+
46+library
47+ import: common-options
48+ hs-source-dirs: src
49+ exposed-modules: LAoP.Dist
50+ LAoP.Dist.Internal
51+ LAoP.Matrix.Internal
52+ LAoP.Matrix.Nat
53+ LAoP.Matrix.Type
54+ LAoP.Relation
55+ LAoP.Relation.Internal
56+ LAoP.Utils
57+ LAoP.Utils.Internal
58+
59+test-suite laop-test
60+ import: common-options
61+ type: exitcode-stdio-1.0
62+ hs-source-dirs: test
63+ other-modules: Examples.Readme
64+ main-is: Spec.hs
65+ build-depends: laop
66+ ghc-options: -threaded
67+ -rtsopts
68+ -with-rtsopts=-N
69+ -funfolding-use-threshold=16
70+ -fexcess-precision
71+ -optc-O3
72+ -optc-ffast-math
73+
74+benchmark laop-benchmark
75+ import: common-options
76+ type: exitcode-stdio-1.0
77+ hs-source-dirs: benchmark
78+ main-is: Main.hs
79+ build-depends: criterion
80+ , QuickCheck
81+ , deepseq
82+ , laop
83+ ghc-options: -threaded
84+ -rtsopts
85+ -with-rtsopts=-N
86+ -funfolding-use-threshold=16
87+ -fexcess-precision
88+ -optc-O3
89+ -optc-ffast-math
package.yamldeleted−48
@@ -1,48 +0,0 @@
1−name: laop
2−version: 0.1.0.0
3−github: "bolt12/laop"
4−license: BSD3
5−author: "Armando Santos"
6−maintainer: "armandoifsantos@gmail.com"
7−copyright: "MIT"
8−
9−extra-source-files:
10−- README.md
11−- ChangeLog.md
12−
13−# Metadata used when publishing your package
14−# synopsis: Short description of your package
15−# category: Web
16−
17−# To avoid duplicated efforts in documentation and dealing with the
18−# complications of embedding Haddock markup inside cabal files, it is
19−# common to point users to the README.md file.
20−description: Please see the README on GitHub at <https://github.com/bolt12/laop#readme>
21−
22−dependencies:
23−- base >= 4.7 && < 5
24−
25−library:
26− source-dirs: src
27−
28−executables:
29− laop-exe:
30− main: Main.hs
31− source-dirs: app
32− ghc-options:
33− - -threaded
34− - -rtsopts
35− - -with-rtsopts=-N
36− dependencies:
37− - laop
38−
39−tests:
40− laop-test:
41− main: Spec.hs
42− source-dirs: test
43− ghc-options:
44− - -threaded
45− - -rtsopts
46− - -with-rtsopts=-N
47− dependencies:
48− - laop
src/LAoP/Dist.hs+10
@@ -36,6 +36,14 @@ module LAoP.Dist
36 Dist (..),
36 Dist (..),
37 Prob,
37 Prob,
38
38
39+ -- * Constraint type synonyms
40+ Countable,
41+ CountableN,
42+ CountableDimsN,
43+ FLN,
44+ Liftable,
45+ TrivialP,
46+
39 -- * Functor instance equivalent functions
47 -- * Functor instance equivalent functions
40 fmapD,
48 fmapD,
41
49
@@ -45,6 +53,8 @@ module LAoP.Dist
45
53
46 -- * Selective equivalent functions
54 -- * Selective equivalent functions
47 selectD,
55 selectD,
56+ branchD,
57+ ifD,
48
58
49 -- * Monad equivalent functions
59 -- * Monad equivalent functions
50 returnD,
60 returnD,
src/LAoP/Dist/Internal.hs+87−36
@@ -1,3 +1,5 @@
1+{-# LANGUAGE DerivingVia #-}
2+{-# LANGUAGE ConstraintKinds #-}
1{-# LANGUAGE GADTs #-}
3{-# LANGUAGE GADTs #-}
2{-# LANGUAGE AllowAmbiguousTypes #-}
4{-# LANGUAGE AllowAmbiguousTypes #-}
3{-# LANGUAGE TypeApplications #-}
5{-# LANGUAGE TypeApplications #-}
@@ -8,18 +10,27 @@
8{-# LANGUAGE RankNTypes #-}
10{-# LANGUAGE RankNTypes #-}
9
11
10module LAoP.Dist.Internal
12module LAoP.Dist.Internal
11− (
13+ (
12 Dist(..),
14 Dist(..),
13 Prob,
15 Prob,
14
16
17+ Countable,
18+ CountableN,
19+ CountableDimsN,
20+ FLN,
21+ Liftable,
22+ TrivialP,
23+
15 fmapD,
24 fmapD,
16 unitD,
25 unitD,
17 multD,
26 multD,
18 selectD,
27 selectD,
28+ branchD,
29+ ifD,
19 returnD,
30 returnD,
20 bindD,
31 bindD,
21 (??),
32 (??),
22−
33+
23 choose,
34 choose,
24 shape,
35 shape,
25 linear,
36 linear,
@@ -32,11 +43,15 @@ module LAoP.Dist.Internal
32 )
43 )
33 where
44 where
34
45
35−import LAoP.Matrix.Type
46+import LAoP.Matrix.Type hiding (TrivialP, Countable, CountableDims, CountableN, CountableDimsN, Liftable, FLN)
47+import Prelude hiding (id, (.))
48+import qualified LAoP.Matrix.Internal as I
36import LAoP.Utils
49import LAoP.Utils
37import GHC.TypeLits
50import GHC.TypeLits
38import Data.Proxy
51import Data.Proxy
39import Data.List (sortBy)
52import Data.List (sortBy)
53+import Control.DeepSeq
54+import Data.Bool
40
55
41-- | Type synonym for probability value
56-- | Type synonym for probability value
42type Prob = Double
57type Prob = Double
@@ -44,17 +59,21 @@ type Prob = Double
44-- | Type synonym for column vector matrices. This represents a probability
59-- | Type synonym for column vector matrices. This represents a probability
45-- distribution.
60-- distribution.
46newtype Dist a = D (Matrix Prob () a)
61newtype 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)
47
71
48-- | Functor instance
72-- | Functor instance
49fmapD ::
73fmapD ::
50− ( Bounded a,
74+ ( Liftable a b,
51− Bounded b,
75+ CountableDimsN a b,
52− Enum a,
76+ FLN b a
53− Enum b,
54− Eq b,
55− KnownNat (Count (Normalize a)),
56− KnownNat (Count (Normalize b)),
57− FromLists Prob (Normalize b) (Normalize a)
58 )
77 )
59 =>
78 =>
60 (a -> b) -> Dist a -> Dist b
79 (a -> b) -> Dist a -> Dist b
@@ -66,26 +85,58 @@ unitD = D (one 1)
66
85
67-- | Applicative/Monoidal instance 'mult' function
86-- | Applicative/Monoidal instance 'mult' function
68multD ::
87multD ::
69− ( KnownNat (Count (Normalize a)),
88+ ( CountableDimsN a b,
70− KnownNat (Count (Normalize b)),
89+ CountableN (a, b),
71− KnownNat (Count (Normalize (a, b))),
90+ FLN (a, b) a,
72− FromLists Prob (Normalize (a, b)) (Normalize a),
91+ FLN (a, b) b,
73− FromLists Prob (Normalize (a, b)) (Normalize b),
92+ TrivialP a b
74− Normalize (a, b) ~ Normalize (Normalize a, Normalize b)
75 ) => Dist a -> Dist b -> Dist (a, b)
93 ) => Dist a -> Dist b -> Dist (a, b)
76−multD (D a) (D b) = D (khatri a b)
94+multD (D a) (D b) = D (kr a b)
77
95
78-- | Selective instance function
96-- | Selective instance function
79selectD ::
97selectD ::
80− ( Normalize (Either a b) ~ Either (Normalize a) (Normalize b),
98+ ( FLN b b,
81− FromLists Prob (Normalize b) (Normalize b),
99+ CountableN b
82− KnownNat (Count (Normalize b))
83 ) => Dist (Either a b) -> Matrix Prob a b -> Dist b
100 ) => Dist (Either a b) -> Matrix Prob a b -> Dist b
84−selectD (D d) m = D (junc m identity `comp` d)
101+selectD (D d) m = D (selectM d m)
85−
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
86
137
87-- | Monad instance 'return' function
138-- | Monad instance 'return' function
88−returnD :: forall a . (Enum a, FromLists Prob () (Normalize a), KnownNat (Count a)) => a -> Dist a
139+returnD :: forall a . (Enum a, FLN () a, Countable a) => a -> Dist a
89returnD a = D (col l)
140returnD a = D (col l)
90 where
141 where
91 i = fromInteger $ natVal (Proxy :: Proxy (Count a))
142 i = fromInteger $ natVal (Proxy :: Proxy (Count a))
@@ -99,8 +150,8 @@ bindD (D d) m = D (m `comp` d)
99-- | Extract probabilities given an Event.
150-- | Extract probabilities given an Event.
100(??) ::
151(??) ::
101 ( Enum a,
152 ( Enum a,
102− KnownNat (Count a),
153+ Countable a,
103− FromLists Prob () (Normalize a)
154+ FLN () a
104 ) => (a -> Bool) -> Dist a -> Prob
155 ) => (a -> Bool) -> Dist a -> Prob
105(??) p d =
156(??) p d =
106 let l = toValues d
157 let l = toValues d
@@ -110,11 +161,11 @@ bindD (D d) m = D (m `comp` d)
110-- Distribution Construction
161-- Distribution Construction
111
162
112-- | Constructs a Bernoulli distribution
163-- | Constructs a Bernoulli distribution
113−choose :: (FromLists Prob () (Normalize a)) => Prob -> Dist a
164+choose :: (FLN () a) => Prob -> Dist a
114choose prob = D (col [prob, 1 - prob])
165choose prob = D (col [prob, 1 - prob])
115
166
116-- | Creates a distribution given a shape function
167-- | Creates a distribution given a shape function
117−shape :: (FromLists Prob () (Normalize a)) => (Prob -> Prob) -> [a] -> Dist a
168+shape :: (FLN () a) => (Prob -> Prob) -> [a] -> Dist a
118shape _ [] = error "Probability.shape: empty list"
169shape _ [] = error "Probability.shape: empty list"
119shape f xs =
170shape f xs =
120 let incr = 1 / fromIntegral (length xs - 1)
171 let incr = 1 / fromIntegral (length xs - 1)
@@ -122,23 +173,23 @@ shape f xs =
122 in fromFreqs (zip xs ps)
173 in fromFreqs (zip xs ps)
123
174
124-- | Constructs a Linear distribution
175-- | Constructs a Linear distribution
125−linear :: (FromLists Prob () (Normalize a)) => [a] -> Dist a
176+linear :: (FLN () a) => [a] -> Dist a
126linear = shape id
177linear = shape id
127
178
128-- | Constructs an Uniform distribution
179-- | Constructs an Uniform distribution
129−uniform :: (FromLists Prob () (Normalize a)) => [a] -> Dist a
180+uniform :: (FLN () a) => [a] -> Dist a
130uniform = shape (const 1)
181uniform = shape (const 1)
131
182
132-- | Constructs an Negative Exponential distribution
183-- | Constructs an Negative Exponential distribution
133−negExp :: (FromLists Prob () (Normalize a)) => [a] -> Dist a
184+negExp :: (FLN () a) => [a] -> Dist a
134negExp = shape (\x -> exp (-x))
185negExp = shape (\x -> exp (-x))
135
186
136-- | Constructs an Normal distribution
187-- | Constructs an Normal distribution
137−normal :: (FromLists Prob () (Normalize a)) => [a] -> Dist a
188+normal :: (FLN () a) => [a] -> Dist a
138normal = shape (normalCurve 0.5 0.5)
189normal = shape (normalCurve 0.5 0.5)
139
190
140-- | Transforms a 'Dist' into a list of pairs.
191-- | Transforms a 'Dist' into a list of pairs.
141−toValues :: forall a . (Enum a, KnownNat (Count a), FromLists Prob () (Normalize a)) => Dist a -> [(a, Prob)]
192+toValues :: forall a . (Enum a, Countable a, FLN () a) => Dist a -> [(a, Prob)]
142toValues (D d) =
193toValues (D d) =
143 let rows = fromInteger (natVal (Proxy :: Proxy (Count a)))
194 let rows = fromInteger (natVal (Proxy :: Proxy (Count a)))
144 probs = toList d
195 probs = toList d
@@ -146,7 +197,7 @@ toValues (D d) =
146 in res
197 in res
147
198
148-- | Pretty a distribution
199-- | Pretty a distribution
149−prettyDist :: forall a. (Show a, Enum a, KnownNat (Count a), FromLists Prob () (Normalize a)) => Dist a -> String
200+prettyDist :: forall a. (Show a, Enum a, Countable a, FLN () a) => Dist a -> String
150prettyDist d =
201prettyDist d =
151 let values = sortBy (\(a, p1) (b, p2) -> compare p2 p1) (toValues @a d)
202 let values = sortBy (\(a, p1) (b, p2) -> compare p2 p1) (toValues @a d)
152 w = maximum (map (length . show . fst) values)
203 w = maximum (map (length . show . fst) values)
@@ -158,12 +209,12 @@ prettyDist d =
158 showR n x = show x ++ " "
209 showR n x = show x ++ " "
159
210
160-- | Pretty Print a distribution
211-- | Pretty Print a distribution
161−prettyPrintDist :: forall a . (Show a, Enum a, KnownNat (Count a), FromLists Prob () (Normalize a)) => Dist a -> IO ()
212+prettyPrintDist :: forall a . (Show a, Enum a, Countable a, FLN () a) => Dist a -> IO ()
162prettyPrintDist = putStrLn . prettyDist @a
213prettyPrintDist = putStrLn . prettyDist @a
163
214
164-- Auxiliary functions
215-- Auxiliary functions
165
216
166−fromFreqs :: (FromLists Prob () (Normalize a)) => [(a,Prob)] -> Dist a
217+fromFreqs :: (FLN () a) => [(a,Prob)] -> Dist a
167fromFreqs xs = D (col (map (\(x,p) -> p/q) xs))
218fromFreqs xs = D (col (map (\(x,p) -> p/q) xs))
168 where q = sum $ map snd xs
219 where q = sum $ map snd xs
169
220
src/LAoP/Matrix/Internal.hs+437−429
@@ -1,4 +1,6 @@
1+{-# LANGUAGE StrictData #-}
1{-# LANGUAGE TypeFamilyDependencies #-}
2{-# LANGUAGE TypeFamilyDependencies #-}
3+{-# LANGUAGE ConstraintKinds #-}
2{-# LANGUAGE AllowAmbiguousTypes #-}
4{-# LANGUAGE AllowAmbiguousTypes #-}
3{-# LANGUAGE DataKinds #-}
5{-# LANGUAGE DataKinds #-}
4{-# LANGUAGE FlexibleContexts #-}
6{-# LANGUAGE FlexibleContexts #-}
@@ -28,7 +30,7 @@
28-- motivation behind the library, the underlying theory, and implementation details.
30-- motivation behind the library, the underlying theory, and implementation details.
29--
31--
30-- This module offers many of the combinators mentioned in the work of
32-- This module offers many of the combinators mentioned in the work of
31−-- Macedo (2012) and Oliveira (2012).
33+-- Macedo (2012) and Oliveira (2012).
32--
34--
33-- This is an Internal module and it is no supposed to be imported.
35-- This is an Internal module and it is no supposed to be imported.
34--
36--
@@ -41,17 +43,26 @@ module LAoP.Matrix.Internal
41 --
43 --
42 -- There exists two type families that make it easier to write
44 -- There exists two type families that make it easier to write
43 -- matrix dimensions: 'FromNat' and 'Count'. This approach
45 -- matrix dimensions: 'FromNat' and 'Count'. This approach
44− -- leads to a very straightforward implementation
46+ -- leads to a very straightforward implementation
45− -- of LAoP combinators.
47+ -- of LAoP combinators.
46
48
47 -- * Type safe matrix representation
49 -- * Type safe matrix representation
48 Matrix (..),
50 Matrix (..),
49
51
52+ -- * Constraint type aliases
53+ Countable,
54+ CountableDims,
55+ CountableN,
56+ CountableDimsN,
57+ FL,
58+ FLN,
59+ Liftable,
60+ Trivial,
61+
50 -- * Primitives
62 -- * Primitives
51− empty,
52 one,
63 one,
53− junc,
64+ join,
54− split,
65+ fork,
55
66
56 -- * Auxiliary type families
67 -- * Auxiliary type families
57 FromNat,
68 FromNat,
@@ -64,6 +75,7 @@ module LAoP.Matrix.Internal
64 toLists,
75 toLists,
65 toList,
76 toList,
66 matrixBuilder,
77 matrixBuilder,
78+ matrixBuilder',
67 row,
79 row,
68 col,
80 col,
69 zeros,
81 zeros,
@@ -74,28 +86,38 @@ module LAoP.Matrix.Internal
74 -- * Misc
86 -- * Misc
75 -- ** Get dimensions
87 -- ** Get dimensions
76 columns,
88 columns,
89+ columns',
77 rows,
90 rows,
91+ rows',
78
92
79 -- ** Matrix Transposition
93 -- ** Matrix Transposition
80 tr,
94 tr,
81
95
96+ -- ** Scalar multiplication/division of matrices
97+ (.|),
98+ (./),
99+
82 -- ** Selective operator
100 -- ** Selective operator
83− select,
101+ select,
102+ branch,
84
103
85 -- ** McCarthy's Conditional
104 -- ** McCarthy's Conditional
86 cond,
105 cond,
87
106
88 -- ** Matrix "abiding"
107 -- ** Matrix "abiding"
89− abideJS,
108+ abideJF,
90− abideSJ,
109+ abideFJ,
110+
111+ -- ** Zip matrices
112+ zipWithM,
91
113
92 -- * Biproduct approach
114 -- * Biproduct approach
93− -- ** Split
115+ -- ** Fork
94 (===),
116 (===),
95 -- *** Projections
117 -- *** Projections
96 p1,
118 p1,
97 p2,
119 p2,
98− -- ** Junc
120+ -- ** Join
99 (|||),
121 (|||),
100 -- *** Injections
122 -- *** Injections
101 i1,
123 i1,
@@ -108,12 +130,13 @@ module LAoP.Matrix.Internal
108
130
109 -- | Note that given the restrictions imposed it is not possible to
131 -- | Note that given the restrictions imposed it is not possible to
110 -- implement the standard type classes present in standard Haskell.
132 -- implement the standard type classes present in standard Haskell.
133+
111 -- *** Matrix pairing projections
134 -- *** Matrix pairing projections
112− kp1,
135+ fstM,
113− kp2,
136+ sndM,
114
137
115 -- *** Matrix pairing
138 -- *** Matrix pairing
116− khatri,
139+ kr,
117
140
118 -- * Matrix composition and lifting
141 -- * Matrix composition and lifting
119
142
@@ -121,10 +144,10 @@ module LAoP.Matrix.Internal
121
144
122 -- | Note that given the restrictions imposed it is not possible to
145 -- | Note that given the restrictions imposed it is not possible to
123 -- implement the standard type classes present in standard Haskell.
146 -- implement the standard type classes present in standard Haskell.
124− identity,
147+ iden,
125 comp,
148 comp,
126− fromF,
127 fromF',
149 fromF',
150+ fromF,
128
151
129 -- * Matrix printing
152 -- * Matrix printing
130 pretty,
153 pretty,
@@ -151,21 +174,22 @@ import LAoP.Utils.Internal
151import Data.Bool
174import Data.Bool
152import Data.Kind
175import Data.Kind
153import Data.List
176import Data.List
177+import Data.Maybe
154import Data.Proxy
178import Data.Proxy
179+import Data.Typeable
155import Data.Void
180import Data.Void
156import GHC.TypeLits
181import GHC.TypeLits
157import Data.Type.Equality
182import Data.Type.Equality
158import GHC.Generics
183import GHC.Generics
159import Control.DeepSeq
184import Control.DeepSeq
160−import Control.Category
185+import Prelude hiding (id, (.))
161−import Prelude hiding ((.))
186+import qualified Prelude (id, (.))
162
187
163-- | LAoP (Linear Algebra of Programming) Inductive Matrix definition.
188-- | LAoP (Linear Algebra of Programming) Inductive Matrix definition.
164data Matrix e cols rows where
189data Matrix e cols rows where
165− Empty :: Matrix e Void Void
166 One :: e -> Matrix e () ()
190 One :: e -> Matrix e () ()
167− Junc :: Matrix e a rows -> Matrix e b rows -> Matrix e (Either a b) rows
191+ Join :: Matrix e a rows -> Matrix e b rows -> Matrix e (Either a b) rows
168− Split :: Matrix e cols a -> Matrix e cols b -> Matrix e cols (Either a b)
192+ Fork :: Matrix e cols a -> Matrix e cols b -> Matrix e cols (Either a b)
169
193
170deriving instance (Show e) => Show (Matrix e cols rows)
194deriving instance (Show e) => Show (Matrix e cols rows)
171
195
@@ -175,7 +199,7 @@ deriving instance (Show e) => Show (Matrix e cols rows)
175-- 'Generic' instance.
199-- 'Generic' instance.
176type family Count (d :: Type) :: Nat where
200type family Count (d :: Type) :: Nat where
177 Count (Natural n m) = (m - n) + 1
201 Count (Natural n m) = (m - n) + 1
178− Count (Powerset a) = (^) (Count a) (Count a)
202+ Count (List a) = (^) 2 (Count a)
179 Count (Either a b) = (+) (Count a) (Count b)
203 Count (Either a b) = (+) (Count a) (Count b)
180 Count (a, b) = (*) (Count a) (Count b)
204 Count (a, b) = (*) (Count a) (Count b)
181 Count (a -> b) = (^) (Count b) (Count a)
205 Count (a -> b) = (^) (Count b) (Count a)
@@ -192,205 +216,197 @@ type family Count (d :: Type) :: Nat where
192--
216--
193-- Thanks to Li-Yao Xia this type family is super fast.
217-- Thanks to Li-Yao Xia this type family is super fast.
194type family FromNat (n :: Nat) :: Type where
218type family FromNat (n :: Nat) :: Type where
195− FromNat 0 = Void
196 FromNat 1 = ()
219 FromNat 1 = ()
197 FromNat n = FromNat' (Mod n 2 == 0) (FromNat (Div n 2))
220 FromNat n = FromNat' (Mod n 2 == 0) (FromNat (Div n 2))
198
221
199type family FromNat' (b :: Bool) (m :: Type) :: Type where
222type family FromNat' (b :: Bool) (m :: Type) :: Type where
200− FromNat' 'True m = Either m m
223+ FromNat' 'True m = Either m m
201 FromNat' 'False m = Either () (Either m m)
224 FromNat' 'False m = Either () (Either m m)
202
225
203-- | Type family that normalizes the representation of a given data
226-- | Type family that normalizes the representation of a given data
204-- structure
227-- structure
205type family Normalize (d :: Type) :: Type where
228type 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)
206− Normalize d = FromNat (Count d)
240+type Trivial a = FromNat (Count a) ~ a
207−
241+
208−-- | It isn't possible to implement the 'id' function so it's
242+-- | It is possible to implement a constrained version of the category type
209−-- implementation is 'undefined'. However 'comp' can be and this partial
243+-- class.
210−-- class implementation exists just to make the code more readable.
211−--
212−-- Please use 'identity' instead.
213instance (Num e) => Category (Matrix e) where
244instance (Num e) => Category (Matrix e) where
214− id = undefined
245+ type Object (Matrix e) a = (FL a a, Countable a)
246+ id = iden
215− (.) = comp
247+ (.) = comp
216
248
217instance NFData e => NFData (Matrix e cols rows) where
249instance NFData e => NFData (Matrix e cols rows) where
218− rnf Empty = ()
219− rnf (One e) = rnf e
250+ rnf (One e) = rnf e
220− rnf (Junc a b) = rnf a `seq` rnf b
251+ rnf (Join a b) = rnf a `seq` rnf b
221− rnf (Split a b) = rnf a `seq` rnf b
252+ rnf (Fork a b) = rnf a `seq` rnf b
222
253
223instance Eq e => Eq (Matrix e cols rows) where
254instance Eq e => Eq (Matrix e cols rows) where
224− Empty == Empty = True
225− (One a) == (One b) = a == b
255+ (One a) == (One b) = a == b
226− (Junc a b) == (Junc c d) = a == c && b == d
256+ (Join a b) == (Join c d) = a == c && b == d
227− (Split a b) == (Split c d) = a == c && b == d
257+ (Fork a b) == (Fork c d) = a == c && b == d
228− x@(Split _ _) == y@(Junc _ _) = x == abideJS y
258+ x@(Fork _ _) == y@(Join _ _) = x == abideJF y
229− x@(Junc _ _) == y@(Split _ _) = abideJS x == y
259+ x@(Join _ _) == y@(Fork _ _) = abideJF x == y
230
260
231instance Num e => Num (Matrix e cols rows) where
261instance 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
267+
268+ abs (One a) = One (abs a)
269+ abs (Join a b) = Join (abs a) (abs b)
270+ abs (Fork a b) = Fork (abs a) (abs b)
232
271
233− Empty + Empty = Empty
234− (One a) + (One b) = One (a + b)
235− (Junc a b) + (Junc c d) = Junc (a + c) (b + d)
236− (Split a b) + (Split c d) = Split (a + c) (b + d)
237− x@(Split _ _) + y@(Junc _ _) = x + abideJS y
238− x@(Junc _ _) + y@(Split _ _) = abideJS x + y
239−
240− Empty - Empty = Empty
241− (One a) - (One b) = One (a - b)
242− (Junc a b) - (Junc c d) = Junc (a - c) (b - d)
243− (Split a b) - (Split c d) = Split (a - c) (b - d)
244− x@(Split _ _) - y@(Junc _ _) = x - abideJS y
245− x@(Junc _ _) - y@(Split _ _) = abideJS x - y
246−
247− Empty * Empty = Empty
248− (One a) * (One b) = One (a * b)
249− (Junc a b) * (Junc c d) = Junc (a * c) (b * d)
250− (Split a b) * (Split c d) = Split (a * c) (b * d)
251− x@(Split _ _) * y@(Junc _ _) = x * abideJS y
252− x@(Junc _ _) * y@(Split _ _) = abideJS x * y
253−
254− abs Empty = Empty
255− abs (One a) = One (abs a)
256− abs (Junc a b) = Junc (abs a) (abs b)
257− abs (Split a b) = Split (abs a) (abs b)
258−
259− signum Empty = Empty
260− signum (One a) = One (signum a)
272+ signum (One a) = One (signum a)
261− signum (Junc a b) = Junc (signum a) (signum b)
273+ signum (Join a b) = Join (signum a) (signum b)
262− signum (Split a b) = Split (signum a) (signum b)
274+ signum (Fork a b) = Fork (signum a) (signum b)
263
275
264instance Ord e => Ord (Matrix e cols rows) where
276instance Ord e => Ord (Matrix e cols rows) where
265− Empty <= Empty = True
266− (One a) <= (One b) = a <= b
277+ (One a) <= (One b) = a <= b
267− (Junc a b) <= (Junc c d) = (a <= c) && (b <= d)
278+ (Join a b) <= (Join c d) = (a <= c) && (b <= d)
268− (Split a b) <= (Split c d) = (a <= c) && (b <= d)
279+ (Fork a b) <= (Fork c d) = (a <= c) && (b <= d)
269− x@(Split _ _) <= y@(Junc _ _) = x <= abideJS y
280+ x@(Fork _ _) <= y@(Join _ _) = x <= abideJF y
270− x@(Junc _ _) <= y@(Split _ _) = abideJS x <= y
281+ x@(Join _ _) <= y@(Fork _ _) = abideJF x <= y
271
282
272-- Primitives
283-- Primitives
273
284
274−-- | Empty matrix constructor
275−empty :: Matrix e Void Void
276−empty = Empty
277−
278-- | Unit matrix constructor
285-- | Unit matrix constructor
279one :: e -> Matrix e () ()
286one :: e -> Matrix e () ()
280one = One
287one = One
281
288
282−-- | Matrix 'Junc' constructor
289+-- | Matrix 'Join' constructor
283−junc :: Matrix e a rows -> Matrix e b rows -> Matrix e (Either a b) rows
290+join :: Matrix e a rows -> Matrix e b rows -> Matrix e (Either a b) rows
284−junc = Junc
291+join = Join
285
292
286infixl 3 |||
293infixl 3 |||
287
294
288−-- | Matrix 'Junc' constructor
295+-- | Matrix 'Join' constructor
289(|||) :: Matrix e a rows -> Matrix e b rows -> Matrix e (Either a b) rows
296(|||) :: Matrix e a rows -> Matrix e b rows -> Matrix e (Either a b) rows
290−(|||) = Junc
297+(|||) = Join
291
298
292−-- | Matrix 'Split' constructor
299+-- | Matrix 'Fork' constructor
293−split :: Matrix e cols a -> Matrix e cols b -> Matrix e cols (Either a b)
300+fork :: Matrix e cols a -> Matrix e cols b -> Matrix e cols (Either a b)
294−split = Split
301+fork = Fork
295
302
296infixl 2 ===
303infixl 2 ===
297
304
298−-- | Matrix 'Split' constructor
305+-- | Matrix 'Fork' constructor
299(===) :: Matrix e cols a -> Matrix e cols b -> Matrix e cols (Either a b)
306(===) :: Matrix e cols a -> Matrix e cols b -> Matrix e cols (Either a b)
300−(===) = Split
307+(===) = Fork
301
308
302-- Construction
309-- Construction
303
310
304-- | Type class for defining the 'fromList' conversion function.
311-- | Type class for defining the 'fromList' conversion function.
305--
312--
306-- Given that it is not possible to branch on types at the term level type
313-- Given that it is not possible to branch on types at the term level type
307−-- classes are needed bery much like an inductive definition but on types.
314+-- classes are needed very much like an inductive definition but on types.
308−class FromLists e cols rows where
315+class FromLists cols rows where
309 -- | Build a matrix out of a list of list of elements. Throws a runtime
316 -- | Build a matrix out of a list of list of elements. Throws a runtime
310 -- error if the dimensions do not match.
317 -- error if the dimensions do not match.
311 fromLists :: [[e]] -> Matrix e cols rows
318 fromLists :: [[e]] -> Matrix e cols rows
312
319
313−instance FromLists e Void Void where
320+instance FromLists () () where
314− fromLists [] = Empty
315− fromLists _ = error "Wrong dimensions"
316−
317−instance {-# OVERLAPPING #-} FromLists e () () where
318 fromLists [[e]] = One e
321 fromLists [[e]] = One e
319 fromLists _ = error "Wrong dimensions"
322 fromLists _ = error "Wrong dimensions"
320
323
321−instance {-# OVERLAPPING #-} (FromLists e cols ()) => FromLists e (Either () cols) () where
324+instance (FromLists cols ()) => FromLists (Either () cols) () where
322− fromLists [h : t] = Junc (One h) (fromLists [t])
325+ fromLists [h : t] = Join (One h) (fromLists [t])
323 fromLists _ = error "Wrong dimensions"
326 fromLists _ = error "Wrong dimensions"
324
327
328+instance {-# OVERLAPPABLE #-}
325−instance {-# OVERLAPPABLE #-} (FromLists e a (), FromLists e b (), KnownNat (Count a)) => FromLists e (Either a b) () where
329+ (FromLists a (), FromLists b (), Countable a) => FromLists (Either a b) () where
326− fromLists [l] =
330+ fromLists [l] =
327 let rowsA = fromInteger (natVal (Proxy :: Proxy (Count a)))
331 let rowsA = fromInteger (natVal (Proxy :: Proxy (Count a)))
328− in Junc (fromLists [take rowsA l]) (fromLists [drop rowsA l])
332+ in Join (fromLists [take rowsA l]) (fromLists [drop rowsA l])
329 fromLists _ = error "Wrong dimensions"
333 fromLists _ = error "Wrong dimensions"
330
334
331−instance {-# OVERLAPPING #-} (FromLists e () rows) => FromLists e () (Either () rows) where
335+instance (FromLists () rows) => FromLists () (Either () rows) where
332− fromLists ([h] : t) = Split (One h) (fromLists t)
336+ fromLists ([h] : t) = Fork (One h) (fromLists t)
333 fromLists _ = error "Wrong dimensions"
337 fromLists _ = error "Wrong dimensions"
334
338
339+instance {-# OVERLAPPABLE #-}
335−instance {-# OVERLAPPABLE #-} (FromLists e () a, FromLists e () b, KnownNat (Count a)) => FromLists e () (Either a b) where
340+ (FromLists () a, FromLists () b, Countable a) => FromLists () (Either a b) where
336− fromLists l@([_] : _) =
341+ fromLists l@([_] : _) =
337 let rowsA = fromInteger (natVal (Proxy :: Proxy (Count a)))
342 let rowsA = fromInteger (natVal (Proxy :: Proxy (Count a)))
338− in Split (fromLists (take rowsA l)) (fromLists (drop rowsA l))
343+ in Fork (fromLists (take rowsA l)) (fromLists (drop rowsA l))
339 fromLists _ = error "Wrong dimensions"
344 fromLists _ = error "Wrong dimensions"
340
345
341−instance {-# OVERLAPPABLE #-} (FromLists e (Either a b) c, FromLists e (Either a b) d, KnownNat (Count c)) => FromLists e (Either a b) (Either c d) where
346+instance (FromLists (Either a b) c, FromLists (Either a b) d, Countable c)
347+ => FromLists (Either a b) (Either c d) where
342 fromLists l@(h : t) =
348 fromLists l@(h : t) =
343 let lh = length h
349 let lh = length h
344 rowsC = fromInteger (natVal (Proxy :: Proxy (Count c)))
350 rowsC = fromInteger (natVal (Proxy :: Proxy (Count c)))
345− condition = all (== lh) (map length t)
351+ condition = all ((== lh) . length) t
346 in if lh > 0 && condition
352 in if lh > 0 && condition
347− then Split (fromLists (take rowsC l)) (fromLists (drop rowsC l))
353+ then Fork (fromLists (take rowsC l)) (fromLists (drop rowsC l))
348 else error "Not all rows have the same length"
354 else error "Not all rows have the same length"
349
355
350-- | Matrix builder function. Constructs a matrix provided with
356-- | Matrix builder function. Constructs a matrix provided with
351−-- a construction function.
357+-- a construction function that operates with indices.
352−matrixBuilder ::
358+matrixBuilder' ::
353 forall e cols rows.
359 forall e cols rows.
354− ( FromLists e cols rows,
360+ ( FL cols rows,
355− KnownNat (Count cols),
361+ CountableDims cols rows
356− KnownNat (Count rows)
357− ) =>
358− ((Int, Int) -> e) ->
359− Matrix e cols rows
362+ ) => ((Int, Int) -> e) -> Matrix e cols rows
360−matrixBuilder f =
363+matrixBuilder' f =
361 let c = fromInteger $ natVal (Proxy :: Proxy (Count cols))
364 let c = fromInteger $ natVal (Proxy :: Proxy (Count cols))
362 r = fromInteger $ natVal (Proxy :: Proxy (Count rows))
365 r = fromInteger $ natVal (Proxy :: Proxy (Count rows))
363 positions = [(a, b) | a <- [0 .. (r - 1)], b <- [0 .. (c - 1)]]
366 positions = [(a, b) | a <- [0 .. (r - 1)], b <- [0 .. (c - 1)]]
364 in fromLists . map (map f) . groupBy (\(x, _) (w, _) -> x == w) $ positions
367 in fromLists . map (map f) . groupBy (\(x, _) (w, _) -> x == w) $ positions
365
368
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+
366-- | Constructs a column vector matrix
389-- | Constructs a column vector matrix
367−col :: (FromLists e () rows) => [e] -> Matrix e () rows
390+col :: (FL () rows) => [e] -> Matrix e () rows
368col = fromLists . map (: [])
391col = fromLists . map (: [])
369
392
370-- | Constructs a row vector matrix
393-- | Constructs a row vector matrix
371−row :: (FromLists e cols ()) => [e] -> Matrix e cols ()
394+row :: (FL cols ()) => [e] -> Matrix e cols ()
372row = fromLists . (: [])
395row = fromLists . (: [])
373
396
374-- | Lifts functions to matrices with arbitrary dimensions.
397-- | Lifts functions to matrices with arbitrary dimensions.
375--
398--
376-- NOTE: Be careful to not ask for a matrix bigger than the cardinality of
399-- NOTE: Be careful to not ask for a matrix bigger than the cardinality of
377-- types @a@ or @b@ allows.
400-- types @a@ or @b@ allows.
378−fromF ::
401+fromF' ::
379 forall a b cols rows e.
402 forall a b cols rows e.
380− ( Bounded a,
403+ ( Liftable e a b,
381− Bounded b,
404+ CountableDims cols rows,
382− Enum a,
383− Enum b,
384− Eq b,
385− Num e,
386− Ord e,
387− KnownNat (Count cols),
388− KnownNat (Count rows),
389− FromLists e rows cols
405+ FL rows cols
390 ) =>
406 ) =>
391 (a -> b) ->
407 (a -> b) ->
392 Matrix e cols rows
408 Matrix e cols rows
393−fromF f =
409+fromF' f =
394 let minA = minBound @a
410 let minA = minBound @a
395 maxA = maxBound @a
411 maxA = maxBound @a
396 minB = minBound @b
412 minB = minBound @b
@@ -400,8 +416,8 @@ fromF f =
400 elementsA = take ccols [minA .. maxA]
416 elementsA = take ccols [minA .. maxA]
401 elementsB = take rrows [minB .. maxB]
417 elementsB = take rrows [minB .. maxB]
402 combinations = (,) <$> elementsA <*> elementsB
418 combinations = (,) <$> elementsA <*> elementsB
403− combAp = map snd . sort . map (\(a, b) -> if f a == b
419+ combAp = map snd . sort . map (\(a, b) -> if f a == b
404− then ((fromEnum a, fromEnum b), 1)
420+ then ((fromEnum a, fromEnum b), 1)
405 else ((fromEnum a, fromEnum b), 0)) $ combinations
421 else ((fromEnum a, fromEnum b), 0)) $ combinations
406 mList = buildList combAp rrows
422 mList = buildList combAp rrows
407 in tr $ fromLists mList
423 in tr $ fromLists mList
@@ -411,48 +427,23 @@ fromF f =
411
427
412-- | Lifts functions to matrices with dimensions matching @a@ and @b@
428-- | Lifts functions to matrices with dimensions matching @a@ and @b@
413-- cardinality's.
429-- cardinality's.
414−fromF' ::
430+fromF ::
415 forall a b e.
431 forall a b e.
416− ( Bounded a,
432+ ( Liftable e a b,
417− Bounded b,
433+ CountableDimsN a b,
418− Enum a,
434+ FLN b a
419− Enum b,
420− Eq b,
421− Num e,
422− Ord e,
423− KnownNat (Count (Normalize a)),
424− KnownNat (Count (Normalize b)),
425− FromLists e (Normalize b) (Normalize a)
426 ) =>
435 ) =>
427 (a -> b) ->
436 (a -> b) ->
428 Matrix e (Normalize a) (Normalize b)
437 Matrix e (Normalize a) (Normalize b)
429−fromF' f =
438+fromF = fromF'
430− let minA = minBound @a
431− maxA = maxBound @a
432− minB = minBound @b
433− maxB = maxBound @b
434− ccols = fromInteger $ natVal (Proxy :: Proxy (Count (Normalize a)))
435− rrows = fromInteger $ natVal (Proxy :: Proxy (Count (Normalize b)))
436− elementsA = take ccols [minA .. maxA]
437− elementsB = take rrows [minB .. maxB]
438− combinations = (,) <$> elementsA <*> elementsB
439− combAp = map snd . sort . map (\(a, b) -> if f a == b
440− then ((fromEnum a, fromEnum b), 1)
441− else ((fromEnum a, fromEnum b), 0)) $ combinations
442− mList = buildList combAp rrows
443− in tr $ fromLists mList
444− where
445− buildList [] _ = []
446− buildList l r = take r l : buildList (drop r l) r
447
439
448-- Conversion
440-- Conversion
449
441
450-- | Converts a matrix to a list of lists of elements.
442-- | Converts a matrix to a list of lists of elements.
451toLists :: Matrix e cols rows -> [[e]]
443toLists :: Matrix e cols rows -> [[e]]
452−toLists Empty = []
453toLists (One e) = [[e]]
444toLists (One e) = [[e]]
454−toLists (Split l r) = toLists l ++ toLists r
445+toLists (Fork l r) = toLists l ++ toLists r
455−toLists (Junc l r) = zipWith (++) (toLists l) (toLists r)
446+toLists (Join l r) = zipWith (++) (toLists l) (toLists r)
456
447
457-- | Converts a matrix to a list of elements.
448-- | Converts a matrix to a list of elements.
458toList :: Matrix e cols rows -> [e]
449toList :: Matrix e cols rows -> [e]
@@ -461,37 +452,38 @@ toList = concat . toLists
461-- Zeros Matrix
452-- Zeros Matrix
462
453
463-- | The zero matrix. A matrix wholly filled with zeros.
454-- | The zero matrix. A matrix wholly filled with zeros.
464−zeros :: (Num e, FromLists e cols rows, KnownNat (Count cols), KnownNat (Count rows)) => Matrix e cols rows
455+zeros :: (Num e, FL cols rows, CountableDims cols rows) => Matrix e cols rows
465−zeros = matrixBuilder (const 0)
456+zeros = matrixBuilder' (const 0)
466
457
467-- Ones Matrix
458-- Ones Matrix
468
459
469-- | The ones matrix. A matrix wholly filled with ones.
460-- | The ones matrix. A matrix wholly filled with ones.
470--
461--
471-- Also known as T (Top) matrix.
462-- Also known as T (Top) matrix.
472−ones :: (Num e, FromLists e cols rows, KnownNat (Count cols), KnownNat (Count rows)) => Matrix e cols rows
463+ones :: (Num e, FL cols rows, CountableDims cols rows) => Matrix e cols rows
473−ones = matrixBuilder (const 1)
464+ones = matrixBuilder' (const 1)
474
465
475-- Const Matrix
466-- Const Matrix
476
467
477-- | The constant matrix constructor. A matrix wholly filled with a given
468-- | The constant matrix constructor. A matrix wholly filled with a given
478-- value.
469-- value.
479−constant :: (Num e, FromLists e cols rows, KnownNat (Count cols), KnownNat (Count rows)) => e -> Matrix e cols rows
470+constant :: (Num e, FL cols rows, CountableDims cols rows) => e -> Matrix e cols rows
480−constant e = matrixBuilder (const e)
471+constant e = matrixBuilder' (const e)
481
472
482-- Bang Matrix
473-- Bang Matrix
483
474
484-- | The T (Top) row vector matrix.
475-- | The T (Top) row vector matrix.
485−bang :: forall e cols. (Num e, Enum e, FromLists e cols (), KnownNat (Count cols)) => Matrix e cols ()
476+bang :: forall e cols. (Num e, Enum e, FL cols (), Countable cols) => Matrix e cols ()
486bang =
477bang =
487 let c = fromInteger $ natVal (Proxy :: Proxy (Count cols))
478 let c = fromInteger $ natVal (Proxy :: Proxy (Count cols))
488 in fromLists [take c [1, 1 ..]]
479 in fromLists [take c [1, 1 ..]]
489
480
490−-- Identity Matrix
481+-- iden Matrix
491
482
492−-- | Identity matrix.
483+-- | iden matrix.
493−identity :: (Num e, FromLists e cols cols, KnownNat (Count cols)) => Matrix e cols cols
484+iden :: forall e cols . (Num e, FL cols cols, Countable cols) => Matrix e cols cols
494−identity = matrixBuilder (bool 0 1 . uncurry (==))
485+iden = matrixBuilder' (bool 0 1 . uncurry (==))
486+{-# NOINLINE iden #-}
495
487
496-- Matrix composition (MMM)
488-- Matrix composition (MMM)
497
489
@@ -500,60 +492,90 @@ identity = matrixBuilder (bool 0 1 . uncurry (==))
500-- This definition takes advantage of divide-and-conquer and fusion laws
492-- This definition takes advantage of divide-and-conquer and fusion laws
501-- from LAoP.
493-- from LAoP.
502comp :: (Num e) => Matrix e cr rows -> Matrix e cols cr -> Matrix e cols rows
494comp :: (Num e) => Matrix e cr rows -> Matrix e cols cr -> Matrix e cols rows
503−comp Empty Empty = Empty
504−comp (One a) (One b) = One (a * b)
495+comp (One a) (One b) = One (a * b)
505−comp (Junc a b) (Split c d) = comp a c + comp b d -- Divide-and-conquer law
496+comp (Join a b) (Fork c d) = comp a c + comp b d -- Divide-and-conquer law
506−comp (Split a b) c = Split (comp a c) (comp b c) -- Split fusion law
497+comp (Fork a b) c = Fork (comp a c) (comp b c) -- Fork fusion law
507−comp c (Junc a b) = Junc (comp c a) (comp c b) -- Junc 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)
508
522
509-- Projections
523-- Projections
510
524
511-- | Biproduct first component projection
525-- | Biproduct first component projection
512−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
526+p1 :: (Num e, CountableDims n m, FL n m, FL m m) => Matrix e (Either m n) m
513−p1 =
527+p1 = join id zeros
514− let iden = identity :: Matrix e m m
515− zero = zeros :: Matrix e n m
516− in junc iden zero
517
528
518-- | Biproduct second component projection
529-- | Biproduct second component projection
519−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
530+p2 :: (Num e, CountableDims n m, FL m n, FL n n) => Matrix e (Either m n) n
520−p2 =
531+p2 = join zeros id
521− let iden = identity :: Matrix e n n
522− zero = zeros :: Matrix e m n
523− in junc zero iden
524
532
525-- Injections
533-- Injections
526
534
527-- | Biproduct first component injection
535-- | Biproduct first component injection
528−i1 :: (Num e, KnownNat (Count n), KnownNat (Count m), FromLists e n m, FromLists e m m) => Matrix e m (Either m n)
536+i1 :: (Num e, CountableDims n m, FL n m, FL m m) => Matrix e m (Either m n)
529i1 = tr p1
537i1 = tr p1
530
538
531-- | Biproduct second component injection
539-- | Biproduct second component injection
532−i2 :: (Num e, KnownNat (Count n), KnownNat (Count m), FromLists e m n, FromLists e n n) => Matrix e n (Either m n)
540+i2 :: (Num e, CountableDims n m, FL m n, FL n n) => Matrix e n (Either m n)
533i2 = tr p2
541i2 = tr p2
534
542
535-- Dimensions
543-- Dimensions
536
544
537-- | Obtain the number of rows.
545-- | Obtain the number of rows.
538--
546--
539−-- NOTE: The 'KnownNat' constaint is needed in order to obtain the
547+-- NOTE: The 'KnownNat' constraint is needed in order to obtain the
540−-- dimensions in constant time.
548+-- dimensions in constant time. For a version that doesn't require the
541−--
549+-- constraint see 'rows''.
542−-- TODO: A 'rows' function that does not need the 'KnownNat' constraint in
543−-- exchange for performance.
544−rows :: forall e cols rows. (KnownNat (Count rows)) => Matrix e cols rows -> Int
550+rows :: forall e cols rows. (Countable rows) => Matrix e cols rows -> Int
545rows _ = fromInteger $ natVal (Proxy :: Proxy (Count rows))
551rows _ = fromInteger $ natVal (Proxy :: Proxy (Count rows))
546
552
553+-- | Obtain the number of rows in an inefficient manner, but without any
554+-- constraints.
555+--
556+-- For a more efficient version see 'rows'.
557+rows' :: Matrix e cols rows -> Int
558+rows' (One _) = 1
559+rows' (Join lhs _) = rows' lhs
560+rows' (Fork top bottom) = rows' top + rows' bottom
561+
547-- | Obtain the number of columns.
562-- | Obtain the number of columns.
548−--
549−-- NOTE: The 'KnownNat' constaint is needed in order to obtain the
550−-- dimensions in constant time.
551--
563--
552−-- TODO: A 'columns' function that does not need the 'KnownNat' constraint in
564+-- NOTE: The 'KnownNat' constraint is needed in order to obtain the
553−-- exchange for performance.
565+-- dimensions in constant time. For a version that doesn't require the
566+-- constraint see 'columns''.
554−columns :: forall e cols rows. (KnownNat (Count cols)) => Matrix e cols rows -> Int
567+columns :: forall e cols rows. (Countable cols) => Matrix e cols rows -> Int
555columns _ = fromInteger $ natVal (Proxy :: Proxy (Count cols))
568columns _ = fromInteger $ natVal (Proxy :: Proxy (Count cols))
556
569
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+
557-- Coproduct Bifunctor
579-- Coproduct Bifunctor
558
580
559infixl 5 -|-
581infixl 5 -|-
@@ -562,157 +584,172 @@ infixl 5 -|-
562(-|-) ::
584(-|-) ::
563 forall e n k m j.
585 forall e n k m j.
564 ( Num e,
586 ( Num e,
565− KnownNat (Count j),
587+ CountableDims j k,
566− KnownNat (Count k),
588+ FL k k,
567− FromLists e k k,
589+ FL j k,
568− FromLists e j k,
590+ FL k j,
569− FromLists e k j,
591+ FL j j
570− FromLists e j j
571 ) =>
592 ) =>
572 Matrix e n k ->
593 Matrix e n k ->
573 Matrix e m j ->
594 Matrix e m j ->
574 Matrix e (Either n m) (Either k j)
595 Matrix e (Either n m) (Either k j)
575−(-|-) a b = Junc (i1 . a) (i2 . b)
596+(-|-) a b = Join (i1 . a) (i2 . b)
576
597
577-- Khatri Rao Product and projections
598-- Khatri Rao Product and projections
578
599
579-- | Khatri Rao product first component projection matrix.
600-- | Khatri Rao product first component projection matrix.
580−kp1 ::
601+fstM ::
581 forall e m k .
602 forall e m k .
582 ( Num e,
603 ( Num e,
583− KnownNat (Count k),
604+ CountableDims k m,
584− FromLists e (FromNat (Count m * Count k)) m,
585− KnownNat (Count m),
586− KnownNat (Count (Normalize (m, k)))
605+ FL (Normalize (m, k)) m,
606+ CountableN (m, k)
587 ) => Matrix e (Normalize (m, k)) m
607 ) => Matrix e (Normalize (m, k)) m
588−kp1 = matrixBuilder f
608+fstM = matrixBuilder' f
589 where
609 where
590 offset = fromInteger (natVal (Proxy :: Proxy (Count k)))
610 offset = fromInteger (natVal (Proxy :: Proxy (Count k)))
591 f (x, y)
611 f (x, y)
592 | y >= (x * offset) && y <= (x * offset + offset - 1) = 1
612 | y >= (x * offset) && y <= (x * offset + offset - 1) = 1
593− | otherwise = 0
613+ | otherwise = 0
594
614
595-- | Khatri Rao product second component projection matrix.
615-- | Khatri Rao product second component projection matrix.
596−kp2 ::
616+sndM ::
597 forall e m k .
617 forall e m k .
598 ( Num e,
618 ( Num e,
599− KnownNat (Count k),
619+ CountableDims k m,
600− FromLists e (FromNat (Count m * Count k)) k,
601− KnownNat (Count m),
602− KnownNat (Count (Normalize (m, k)))
620+ FL (Normalize (m, k)) k,
621+ CountableN (m, k)
603 ) => Matrix e (Normalize (m, k)) k
622 ) => Matrix e (Normalize (m, k)) k
604−kp2 = matrixBuilder f
623+sndM = matrixBuilder' f
605 where
624 where
606 offset = fromInteger (natVal (Proxy :: Proxy (Count k)))
625 offset = fromInteger (natVal (Proxy :: Proxy (Count k)))
607 f (x, y)
626 f (x, y)
608 | x == y || mod (y - x) offset == 0 = 1
627 | x == y || mod (y - x) offset == 0 = 1
609− | otherwise = 0
628+ | otherwise = 0
610
629
611-- | Khatri Rao Matrix product also known as matrix pairing.
630-- | Khatri Rao Matrix product also known as matrix pairing.
612--
631--
613-- NOTE: That this is not a true categorical product, see for instance:
632-- NOTE: That this is not a true categorical product, see for instance:
614−--
633+--
615-- @
634-- @
616−-- | kp1 . khatri a b == a
635+-- | fstM . kr a b == a
617−-- khatri a b ==> |
636+-- kr a b ==> |
618−-- | kp2 . khatri a b == b
637+-- | sndM . kr a b == b
619-- @
638-- @
620--
639--
621-- __Emphasis__ on the implication symbol.
640-- __Emphasis__ on the implication symbol.
622−khatri ::
641+kr ::
623− forall e cols a b.
642+ forall e cols a b.
624 ( Num e,
643 ( Num e,
625− KnownNat (Count a),
644+ CountableDims a b,
626− KnownNat (Count b),
645+ CountableN (a, b),
627− KnownNat (Count (Normalize (a, b))),
628− FromLists e (Normalize (a, b)) a,
646+ FL (Normalize (a, b)) a,
629− FromLists e (Normalize (a, b)) b
647+ FL (Normalize (a, b)) b
630 ) => Matrix e cols a -> Matrix e cols b -> Matrix e cols (Normalize (a, b))
648 ) => Matrix e cols a -> Matrix e cols b -> Matrix e cols (Normalize (a, b))
631−khatri a b =
649+kr a b =
632− let kp1' = kp1 @e @a @b
650+ let fstM' = fstM @e @a @b
633− kp2' = kp2 @e @a @b
651+ sndM' = sndM @e @a @b
634− in (tr kp1') . a * (tr kp2') . b
652+ in (tr fstM' . a) * (tr sndM' . b)
635
653
636-- Product Bifunctor (Kronecker)
654-- Product Bifunctor (Kronecker)
637
655
638infixl 4 ><
656infixl 4 ><
639
657
640-- | Matrix product functor also known as kronecker product
658-- | Matrix product functor also known as kronecker product
641−(><) ::
659+(><) ::
642− forall e m p n q.
660+ forall e m p n q.
643 ( Num e,
661 ( Num e,
644− KnownNat (Count m),
662+ CountableDims m n,
645− KnownNat (Count n),
663+ CountableDims p q,
646− KnownNat (Count p),
664+ CountableDimsN (m, n) (p, q),
647− KnownNat (Count q),
648− KnownNat (Count (Normalize (m, n))),
649− FromLists e (Normalize (m, n)) m,
665+ FL (Normalize (m, n)) m,
650− FromLists e (Normalize (m, n)) n,
666+ FL (Normalize (m, n)) n,
651− KnownNat (Count (Normalize (p, q))),
652− FromLists e (Normalize (p, q)) p,
667+ FL (Normalize (p, q)) p,
653− FromLists e (Normalize (p, q)) q
668+ FL (Normalize (p, q)) q
654− )
669+ )
655 => Matrix e m p -> Matrix e n q -> Matrix e (Normalize (m, n)) (Normalize (p, q))
670 => Matrix e m p -> Matrix e n q -> Matrix e (Normalize (m, n)) (Normalize (p, q))
656(><) a b =
671(><) a b =
657− let kp1' = kp1 @e @m @n
672+ let fstM' = fstM @e @m @n
658− kp2' = kp2 @e @m @n
673+ sndM' = sndM @e @m @n
659− in khatri (a . kp1') (b . kp2')
674+ in kr (a . fstM') (b . sndM')
660
675
661−-- Matrix abide Junc Split
676+-- Matrix abide Join Fork
662
677
663−-- | Matrix "abiding" followin the 'Junc'-'Split' abide law.
678+-- | Matrix "abiding" following the 'Join'-'Fork' exchange law.
664−--
679+--
665-- Law:
680-- Law:
666--
681--
667-- @
682-- @
668−-- 'Junc' ('Split' a c) ('Split' b d) == 'Split' ('Junc' a b) ('Junc' c d)
683+-- 'Join' ('Fork' a c) ('Fork' b d) == 'Fork' ('Join' a b) ('Join' c d)
669-- @
684-- @
670−abideJS :: Matrix e cols rows -> Matrix e cols rows
685+abideJF :: Matrix e cols rows -> Matrix e cols rows
671−abideJS (Junc (Split a c) (Split b d)) = Split (Junc (abideJS a) (abideJS b)) (Junc (abideJS c) (abideJS d)) -- Junc-Split abide law
686+abideJF (Join (Fork a c) (Fork b d)) = Fork (Join (abideJF a) (abideJF b)) (Join (abideJF c) (abideJF d)) -- Join-Fork abide law
672−abideJS Empty = Empty
673−abideJS (One e) = One e
687+abideJF (One e) = One e
674−abideJS (Junc a b) = Junc (abideJS a) (abideJS b)
688+abideJF (Join a b) = Join (abideJF a) (abideJF b)
675−abideJS (Split a b) = Split (abideJS a) (abideJS b)
689+abideJF (Fork a b) = Fork (abideJF a) (abideJF b)
676
690
677−-- Matrix abide Split Junc
691+-- Matrix abide Fork Join
678
692
679−-- | Matrix "abiding" followin the 'Split'-'Junc' abide law.
693+-- | Matrix "abiding" followin the 'Fork'-'Join' abide law.
680−--
694+--
681-- @
695-- @
682−-- 'Split' ('Junc' a b) ('Junc' c d) == 'Junc' ('Split' a c) ('Split' b d)
696+-- 'Fork' ('Join' a b) ('Join' c d) == 'Join' ('Fork' a c) ('Fork' b d)
683-- @
697-- @
684−abideSJ :: Matrix e cols rows -> Matrix e cols rows
698+abideFJ :: Matrix e cols rows -> Matrix e cols rows
685−abideSJ (Split (Junc a b) (Junc c d)) = Junc (Split (abideSJ a) (abideSJ c)) (Split (abideSJ b) (abideSJ d)) -- Split-Junc abide law
699+abideFJ (Fork (Join a b) (Join c d)) = Join (Fork (abideFJ a) (abideFJ c)) (Fork (abideFJ b) (abideFJ d)) -- Fork-Join abide law
686−abideSJ Empty = Empty
687−abideSJ (One e) = One e
700+abideFJ (One e) = One e
688−abideSJ (Junc a b) = Junc (abideSJ a) (abideSJ b)
701+abideFJ (Join a b) = Join (abideFJ a) (abideFJ b)
689−abideSJ (Split a b) = Split (abideSJ a) (abideSJ b)
702+abideFJ (Fork a b) = Fork (abideFJ a) (abideFJ b)
690
703
691-- Matrix transposition
704-- Matrix transposition
692
705
693-- | Matrix transposition.
706-- | Matrix transposition.
694tr :: Matrix e cols rows -> Matrix e rows cols
707tr :: Matrix e cols rows -> Matrix e rows cols
695−tr Empty = Empty
696−tr (One e) = One e
708+tr (One e) = One e
697−tr (Junc a b) = Split (tr a) (tr b)
709+tr (Join a b) = Fork (tr a) (tr b)
698−tr (Split a b) = Junc (tr a) (tr b)
710+tr (Fork a b) = Join (tr a) (tr b)
699
711
700-- Selective 'select' operator
712-- Selective 'select' operator
701
713
702-- | Selective functors 'select' operator equivalent inspired by the
714-- | Selective functors 'select' operator equivalent inspired by the
703-- ArrowMonad solution presented in the paper.
715-- 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+ )
704−select :: (Num e, FromLists e b b, KnownNat (Count b)) => Matrix e cols (Either a b) -> Matrix e a b -> Matrix e cols b
735+ => Matrix e cols (Either a b) -> Matrix e a c -> Matrix e b c -> Matrix e cols c
705−select m y = junc y identity . m
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
706
743
707-- McCarthy's Conditional
744-- McCarthy's Conditional
708
745
709-- | McCarthy's Conditional expresses probabilistic choice.
746-- | McCarthy's Conditional expresses probabilistic choice.
710cond ::
747cond ::
711− ( cols ~ FromNat (Count cols),
748+ ( Trivial cols,
712− KnownNat (Count cols),
749+ Countable cols,
713− FromLists e () cols,
750+ FL () cols,
714− FromLists e cols (),
751+ FL cols (),
715− FromLists e cols cols,
752+ FL cols cols,
716 Bounded a,
753 Bounded a,
717 Enum a,
754 Enum a,
718 Num e,
755 Num e,
@@ -720,14 +757,14 @@ cond ::
720 )
757 )
721 =>
758 =>
722 (a -> Bool) -> Matrix e cols rows -> Matrix e cols rows -> Matrix e cols rows
759 (a -> Bool) -> Matrix e cols rows -> Matrix e cols rows -> Matrix e cols rows
723−cond p f g = junc f g . grd p
760+cond p f g = join f g . grd p
724−
761+
725−grd ::
762+grd ::
726− ( q ~ FromNat (Count q),
763+ ( Trivial q,
727− KnownNat (Count q),
764+ Countable q,
728− FromLists e () q,
765+ FL () q,
729− FromLists e q (),
766+ FL q (),
730− FromLists e q q,
767+ FL q q,
731 Bounded a,
768 Bounded a,
732 Enum a,
769 Enum a,
733 Num e,
770 Num e,
@@ -735,63 +772,86 @@ grd ::
735 )
772 )
736 =>
773 =>
737 (a -> Bool) -> Matrix e q (Either q q)
774 (a -> Bool) -> Matrix e q (Either q q)
738−grd f = split (corr f) (corr (not . f))
775+grd f = fork (corr f) (corr (not . f))
739−
776+
740−corr ::
777+corr ::
741− forall e a q .
778+ forall e a q .
742− ( q ~ FromNat (Count q),
779+ ( Trivial q,
743− KnownNat (Count q),
780+ Countable q,
744− FromLists e () q,
781+ FL () q,
745− FromLists e q (),
782+ FL q (),
746− FromLists e q q,
783+ FL q q,
747− Bounded a,
784+ Liftable e a Bool
748− Enum a,
749− Num e,
750− Ord e
751− )
785+ )
752 => (a -> Bool) -> Matrix e q q
786 => (a -> Bool) -> Matrix e q q
753−corr p = let f = fromF p :: Matrix e q ()
787+corr p = let f = fromF' p :: Matrix e q ()
754− in khatri f (identity :: Matrix e q q)
788+ in kr f (id :: Matrix e q q)
755
789
756-- Pretty print
790-- Pretty print
757
791
758prettyAux :: Show e => [[e]] -> [[e]] -> String
792prettyAux :: Show e => [[e]] -> [[e]] -> String
759prettyAux [] _ = ""
793prettyAux [] _ = ""
760−prettyAux [[e]] m = "│ " ++ fill (show e) ++ " │\n"
794+prettyAux [[e]] m = "│ " ++ fill (show e) ++ " │\n"
761 where
795 where
762 v = fmap show m
796 v = fmap show m
763 widest = maximum $ fmap length v
797 widest = maximum $ fmap length v
764 fill str = replicate (widest - length str - 2) ' ' ++ str
798 fill str = replicate (widest - length str - 2) ' ' ++ str
765−prettyAux [h] m = "│ " ++ fill (unwords $ map show h) ++ " │\n"
799+prettyAux [h] m = "│ " ++ fill (unwords $ map show h) ++ " │\n"
766 where
800 where
767− v = fmap show m
801+ v = fmap show m
768− widest = maximum $ fmap length v
802+ widest = maximum $ fmap length v
769 fill str = replicate (widest - length str - 2) ' ' ++ str
803 fill str = replicate (widest - length str - 2) ' ' ++ str
770−prettyAux (h : t) l = "│ " ++ fill (unwords $ map show h) ++ " │\n" ++
804+prettyAux (h : t) l = "│ " ++ fill (unwords $ map show h) ++ " │\n" ++
771 prettyAux t l
805 prettyAux t l
772 where
806 where
773− v = fmap show l
807+ v = fmap show l
774− widest = maximum $ fmap length v
808+ widest = maximum $ fmap length v
775 fill str = replicate (widest - length str - 2) ' ' ++ str
809 fill str = replicate (widest - length str - 2) ' ' ++ str
776
810
777-- | Matrix pretty printer
811-- | Matrix pretty printer
778−pretty :: (KnownNat (Count cols), Show e) => Matrix e cols rows -> String
812+pretty :: (CountableDims cols rows, Show e) => Matrix e cols rows -> String
813+pretty m = concat
779−pretty m = "┌ " ++ unwords (replicate (columns m) blank) ++ " ┐\n" ++
814+ [ "┌ ", unwords (replicate (columns m) blank), " ┐\n"
780− prettyAux (toLists m) (toLists m) ++
815+ , unlines
816+ [ "│ " ++ unwords (fmap (\j -> fill $ show $ getElem i j m) [1..columns m]) ++ " │" | i <- [1..rows m] ]
781− "└ " ++ unwords (replicate (columns m) blank) ++ " ┘"
817+ , "└ ", unwords (replicate (columns m) blank), " ┘"
818+ ]
782− where
819+ where
783− v = fmap show (toList m)
820+ strings = map show (toList m)
784− widest = maximum $ fmap length v
821+ widest = maximum $ map length strings
785 fill str = replicate (widest - length str) ' ' ++ str
822 fill str = replicate (widest - length str) ' ' ++ str
786− blank = fill ""
823+ blank = fill ""
824+ safeGet i j m
825+ | i > rows m || j > columns m || i < 1 || j < 1 = Nothing
826+ | otherwise = Just $ unsafeGet i j m (toList m)
827+ unsafeGet i j m l = l !! encode (columns m) (i,j)
828+ encode m (i,j) = (i-1)*m + j - 1
829+ getElem i j m =
830+ fromMaybe
831+ (error $
832+ "getElem: Trying to get the "
833+ ++ show (i, j)
834+ ++ " element from a "
835+ ++ show (rows m) ++ "x" ++ show (columns m)
836+ ++ " matrix."
837+ )
838+ (safeGet i j m)
787
839
788-- | Matrix pretty printer
840-- | Matrix pretty printer
789−prettyPrint :: (KnownNat (Count cols), Show e) => Matrix e cols rows -> IO ()
841+prettyPrint :: (CountableDims cols rows, Show e) => Matrix e cols rows -> IO ()
790prettyPrint = putStrLn . pretty
842prettyPrint = putStrLn . pretty
791
843
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+
792-- Relational operators functions
852-- Relational operators functions
793
853
794−type Boolean = Natural 0 1
854+type Boolean = Natural 0 1
795type Relation a b = Matrix Boolean a b
855type Relation a b = Matrix Boolean a b
796
856
797-- | Helper conversion function
857-- | Helper conversion function
@@ -807,54 +867,47 @@ fromBool False = nat 0
807
867
808-- | Relational negation
868-- | Relational negation
809negateM :: Relation cols rows -> Relation cols rows
869negateM :: Relation cols rows -> Relation cols rows
810−negateM Empty = Empty
811−negateM (One (Nat 0)) = One (Nat 1)
870+negateM (One (Nat p)) = One (Nat (negate p))
812−negateM (One (Nat 1)) = One (Nat 0)
813−negateM (Junc a b) = Junc (negateM a) (negateM b)
871+negateM (Join a b) = Join (negateM a) (negateM b)
814−negateM (Split a b) = Split (negateM a) (negateM b)
872+negateM (Fork a b) = Fork (negateM a) (negateM b)
815
873
816-- | Relational addition
874-- | Relational addition
817orM :: Relation cols rows -> Relation cols rows -> Relation cols rows
875orM :: Relation cols rows -> Relation cols rows -> Relation cols rows
818−orM Empty Empty = Empty
819−orM (One a) (One b) = One (fromBool (toBool a || toBool b))
876+orM (One a) (One b) = One (fromBool (toBool a || toBool b))
820−orM (Junc a b) (Junc c d) = Junc (orM a c) (orM b d)
877+orM (Join a b) (Join c d) = Join (orM a c) (orM b d)
821−orM (Split a b) (Split c d) = Split (orM a c) (orM b d)
878+orM (Fork a b) (Fork c d) = Fork (orM a c) (orM b d)
822−orM x@(Split _ _) y@(Junc _ _) = orM x (abideJS y)
879+orM x@(Fork _ _) y@(Join _ _) = orM x (abideJF y)
823−orM x@(Junc _ _) y@(Split _ _) = orM (abideJS x) y
880+orM x@(Join _ _) y@(Fork _ _) = orM (abideJF x) y
824
881
825-- | Relational multiplication
882-- | Relational multiplication
826andM :: Relation cols rows -> Relation cols rows -> Relation cols rows
883andM :: Relation cols rows -> Relation cols rows -> Relation cols rows
827−andM Empty Empty = Empty
828−andM (One a) (One b) = One (fromBool (toBool a && toBool b))
884+andM (One a) (One b) = One (fromBool (toBool a && toBool b))
829−andM (Junc a b) (Junc c d) = Junc (andM a c) (andM b d)
885+andM (Join a b) (Join c d) = Join (andM a c) (andM b d)
830−andM (Split a b) (Split c d) = Split (andM a c) (andM b d)
886+andM (Fork a b) (Fork c d) = Fork (andM a c) (andM b d)
831−andM x@(Split _ _) y@(Junc _ _) = andM x (abideJS y)
887+andM x@(Fork _ _) y@(Join _ _) = andM x (abideJF y)
832−andM x@(Junc _ _) y@(Split _ _) = andM (abideJS x) y
888+andM x@(Join _ _) y@(Fork _ _) = andM (abideJF x) y
833
889
834-- | Relational subtraction
890-- | Relational subtraction
835subM :: Relation cols rows -> Relation cols rows -> Relation cols rows
891subM :: Relation cols rows -> Relation cols rows -> Relation cols rows
836−subM Empty Empty = Empty
837−subM (One a) (One b) = if a - b < nat 0 then One (nat 0) else One (a - b)
892+subM (One a) (One b) = if a - b < nat 0 then One (nat 0) else One (a - b)
838−subM (Junc a b) (Junc c d) = Junc (subM a c) (subM b d)
893+subM (Join a b) (Join c d) = Join (subM a c) (subM b d)
839−subM (Split a b) (Split c d) = Split (subM a c) (subM b d)
894+subM (Fork a b) (Fork c d) = Fork (subM a c) (subM b d)
840−subM x@(Split _ _) y@(Junc _ _) = subM x (abideJS y)
895+subM x@(Fork _ _) y@(Join _ _) = subM x (abideJF y)
841−subM x@(Junc _ _) y@(Split _ _) = subM (abideJS x) y
896+subM x@(Join _ _) y@(Fork _ _) = subM (abideJF x) y
842
897
843-- | Matrix relational composition.
898-- | Matrix relational composition.
844compRel :: Relation cr rows -> Relation cols cr -> Relation cols rows
899compRel :: Relation cr rows -> Relation cols cr -> Relation cols rows
845−compRel Empty Empty = Empty
846−compRel (One a) (One b) = One (fromBool (toBool a && toBool b))
900+compRel (One a) (One b) = One (fromBool (toBool a && toBool b))
847−compRel (Junc a b) (Split c d) = orM (compRel a c) (compRel b d) -- Divide-and-conquer law
901+compRel (Join a b) (Fork c d) = orM (compRel a c) (compRel b d) -- Divide-and-conquer law
848−compRel (Split a b) c = Split (compRel a c) (compRel b c) -- Split fusion law
902+compRel (Fork a b) c = Fork (compRel a c) (compRel b c) -- Fork fusion law
849−compRel c (Junc a b) = Junc (compRel c a) (compRel c b) -- Junc fusion law
903+compRel c (Join a b) = Join (compRel c a) (compRel c b) -- Join fusion law
850
904
851-- | Matrix relational right division
905-- | Matrix relational right division
852divR :: Relation b c -> Relation b a -> Relation a c
906divR :: Relation b c -> Relation b a -> Relation a c
853−divR Empty Empty = Empty
854divR (One a) (One b) = One (fromBool (not (toBool b) || toBool a)) -- b implies a
907divR (One a) (One b) = One (fromBool (not (toBool b) || toBool a)) -- b implies a
855−divR (Junc a b) (Junc c d) = andM (divR a c) (divR b d)
908+divR (Join a b) (Join c d) = andM (divR a c) (divR b d)
856−divR (Split a b) c = Split (divR a c) (divR b c)
909+divR (Fork a b) c = Fork (divR a c) (divR b c)
857−divR c (Split a b) = Junc (divR c a) (divR c b)
910+divR c (Fork a b) = Join (divR c a) (divR c b)
858
911
859-- | Matrix relational left division
912-- | Matrix relational left division
860divL :: Relation c b -> Relation a b -> Relation a c
913divL :: Relation c b -> Relation a b -> Relation a c
@@ -870,97 +923,52 @@ divS s r = divL r s `intersection` divR (tr r) (tr s)
870--
923--
871-- NOTE: Be careful to not ask for a relation bigger than the cardinality of
924-- NOTE: Be careful to not ask for a relation bigger than the cardinality of
872-- types @a@ or @b@ allows.
925-- types @a@ or @b@ allows.
873−fromFRel ::
926+fromFRel' ::
874 forall a b cols rows.
927 forall a b cols rows.
875− ( Bounded a,
928+ ( Liftable Boolean a b,
876− Bounded b,
929+ CountableDims cols rows,
877− Enum a,
878− Enum b,
879− Eq b,
880− KnownNat (Count cols),
881− KnownNat (Count rows),
882− FromLists (Natural 0 1) rows cols
930+ FL rows cols
883 ) =>
931 ) =>
884 (a -> b) ->
932 (a -> b) ->
885 Relation cols rows
933 Relation cols rows
886−fromFRel f =
934+fromFRel' = fromF'
887− let minA = minBound @a
888− maxA = maxBound @a
889− minB = minBound @b
890− maxB = maxBound @b
891− ccols = fromInteger $ natVal (Proxy :: Proxy (Count cols))
892− rrows = fromInteger $ natVal (Proxy :: Proxy (Count rows))
893− elementsA = take ccols [minA .. maxA]
894− elementsB = take rrows [minB .. maxB]
895− combinations = (,) <$> elementsA <*> elementsB
896− combAp = map snd . sort . map (\(a, b) -> if f a == b
897− then ((fromEnum a, fromEnum b), nat 1)
898− else ((fromEnum a, fromEnum b), nat 0)) $ combinations
899− mList = buildList combAp rrows
900− in tr $ fromLists mList
901− where
902− buildList [] _ = []
903− buildList l r = take r l : buildList (drop r l) r
904
935
905-- | Lifts functions to relations with dimensions matching @a@ and @b@
936-- | Lifts functions to relations with dimensions matching @a@ and @b@
906-- cardinality's.
937-- cardinality's.
907−fromFRel' ::
938+fromFRel ::
908 forall a b.
939 forall a b.
909− ( Bounded a,
940+ ( Liftable Boolean a b,
910− Bounded b,
941+ CountableDimsN a b,
911− Enum a,
942+ FLN b a
912− Enum b,
913− Eq b,
914− KnownNat (Count (Normalize a)),
915− KnownNat (Count (Normalize b)),
916− FromLists (Natural 0 1) (Normalize b) (Normalize a)
917 ) =>
943 ) =>
918 (a -> b) ->
944 (a -> b) ->
919 Relation (Normalize a) (Normalize b)
945 Relation (Normalize a) (Normalize b)
920−fromFRel' f =
946+fromFRel = fromFRel'
921− let minA = minBound @a
922− maxA = maxBound @a
923− minB = minBound @b
924− maxB = maxBound @b
925− ccols = fromInteger $ natVal (Proxy :: Proxy (Count (Normalize a)))
926− rrows = fromInteger $ natVal (Proxy :: Proxy (Count (Normalize b)))
927− elementsA = take ccols [minA .. maxA]
928− elementsB = take rrows [minB .. maxB]
929− combinations = (,) <$> elementsA <*> elementsB
930− combAp = map snd . sort . map (\(a, b) -> if f a == b
931− then ((fromEnum a, fromEnum b), nat 1)
932− else ((fromEnum a, fromEnum b), nat 0)) $ combinations
933− mList = buildList combAp rrows
934− in tr $ fromLists mList
935− where
936− buildList [] _ = []
937− buildList l r = take r l : buildList (drop r l) r
938
947
939-- | Lifts a relation function to a Boolean Matrix
948-- | Lifts a relation function to a Boolean Matrix
940−toRel ::
949+toRel ::
941 forall a b.
950 forall a b.
942 ( Bounded a,
951 ( Bounded a,
943 Bounded b,
952 Bounded b,
944 Enum a,
953 Enum a,
945 Enum b,
954 Enum b,
946 Eq b,
955 Eq b,
947− KnownNat (Count (Normalize a)),
956+ CountableDims a b,
948− KnownNat (Count (Normalize b)),
957+ FLN b a
949− FromLists (Natural 0 1) (Normalize b) (Normalize a)
950− )
958+ )
951 => (a -> b -> Bool) -> Relation (Normalize a) (Normalize b)
959 => (a -> b -> Bool) -> Relation (Normalize a) (Normalize b)
952toRel f =
960toRel f =
953 let minA = minBound @a
961 let minA = minBound @a
954 maxA = maxBound @a
962 maxA = maxBound @a
955 minB = minBound @b
963 minB = minBound @b
956 maxB = maxBound @b
964 maxB = maxBound @b
957− ccols = fromInteger $ natVal (Proxy :: Proxy (Count (Normalize a)))
965+ ccols = fromInteger $ natVal (Proxy :: Proxy (Count a))
958− rrows = fromInteger $ natVal (Proxy :: Proxy (Count (Normalize b)))
966+ rrows = fromInteger $ natVal (Proxy :: Proxy (Count b))
959 elementsA = take ccols [minA .. maxA]
967 elementsA = take ccols [minA .. maxA]
960 elementsB = take rrows [minB .. maxB]
968 elementsB = take rrows [minB .. maxB]
961 combinations = (,) <$> elementsA <*> elementsB
969 combinations = (,) <$> elementsA <*> elementsB
962− combAp = map snd . sort . map (\(a, b) -> if uncurry f (a, b)
970+ combAp = map snd . sort . map (\(a, b) -> if uncurry f (a, b)
963− then ((fromEnum a, fromEnum b), nat 1)
971+ then ((fromEnum a, fromEnum b), nat 1)
964 else ((fromEnum a, fromEnum b), nat 0)) $ combinations
972 else ((fromEnum a, fromEnum b), nat 0)) $ combinations
965 mList = buildList combAp rrows
973 mList = buildList combAp rrows
966 in tr $ fromLists mList
974 in tr $ fromLists mList
src/LAoP/Matrix/Nat.hs+194−187
@@ -1,3 +1,4 @@
1+{-# LANGUAGE ConstraintKinds #-}
1{-# LANGUAGE AllowAmbiguousTypes #-}
2{-# LANGUAGE AllowAmbiguousTypes #-}
2{-# LANGUAGE DataKinds #-}
3{-# LANGUAGE DataKinds #-}
3{-# LANGUAGE DerivingVia #-}
4{-# LANGUAGE DerivingVia #-}
@@ -53,11 +54,22 @@ module LAoP.Matrix.Nat
53 -- * Type safe matrix representation
54 -- * Type safe matrix representation
54 Matrix (..),
55 Matrix (..),
55
56
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+
56 -- * Primitives
69 -- * Primitives
57− empty,
58 one,
70 one,
59− junc,
71+ join,
60− split,
72+ fork,
61
73
62 -- * Auxiliary type families
74 -- * Auxiliary type families
63 I.FromNat,
75 I.FromNat,
@@ -65,11 +77,11 @@ module LAoP.Matrix.Nat
65 I.Normalize,
77 I.Normalize,
66
78
67 -- * Matrix construction and conversion
79 -- * Matrix construction and conversion
68− I.FromLists,
80+ I.FL,
69 fromLists,
81 fromLists,
70 toLists,
82 toLists,
71 toList,
83 toList,
72− matrixBuilder,
84+ matrixBuilder',
73 row,
85 row,
74 col,
86 col,
75 zeros,
87 zeros,
@@ -85,6 +97,10 @@ module LAoP.Matrix.Nat
85 -- ** Matrix Transposition
97 -- ** Matrix Transposition
86 tr,
98 tr,
87
99
100+ -- ** Scalar multiplication/division of matrices
101+ (.|),
102+ (./),
103+
88 -- ** Selective operator
104 -- ** Selective operator
89 select,
105 select,
90
106
@@ -92,16 +108,19 @@ module LAoP.Matrix.Nat
92 cond,
108 cond,
93
109
94 -- ** Matrix "abiding"
110 -- ** Matrix "abiding"
95− abideJS,
111+ abideJF,
96− abideSJ,
112+ abideFJ,
113+
114+ -- ** Zip Matrices
115+ zipWithM,
97
116
98 -- * Biproduct approach
117 -- * Biproduct approach
99− -- ** Split
118+ -- ** Fork
100 (===),
119 (===),
101 -- *** Projections
120 -- *** Projections
102 p1,
121 p1,
103 p2,
122 p2,
104− -- ** Junc
123+ -- ** Join
105 (|||),
124 (|||),
106 -- *** Injections
125 -- *** Injections
107 i1,
126 i1,
@@ -115,11 +134,11 @@ module LAoP.Matrix.Nat
115 -- | Note that given the restrictions imposed it is not possible to
134 -- | Note that given the restrictions imposed it is not possible to
116 -- implement the standard type classes present in standard Haskell.
135 -- implement the standard type classes present in standard Haskell.
117 -- *** Matrix pairing projections
136 -- *** Matrix pairing projections
118− kp1,
137+ fstM,
119− kp2,
138+ sndM,
120
139
121 -- *** Matrix pairing
140 -- *** Matrix pairing
122− khatri,
141+ kr,
123
142
124 -- * Matrix composition and lifting
143 -- * Matrix composition and lifting
125
144
@@ -127,10 +146,10 @@ module LAoP.Matrix.Nat
127
146
128 -- | Note that given the restrictions imposed it is not possible to
147 -- | Note that given the restrictions imposed it is not possible to
129 -- implement the standard type classes present in standard Haskell.
148 -- implement the standard type classes present in standard Haskell.
130− identity,
149+ iden,
131 comp,
150 comp,
132− fromF,
133 fromF',
151 fromF',
152+ fromF,
134
153
135 -- * Matrix printing
154 -- * Matrix printing
136 pretty,
155 pretty,
@@ -141,107 +160,95 @@ where
141import Data.Proxy
160import Data.Proxy
142import GHC.TypeLits
161import GHC.TypeLits
143import Control.DeepSeq
162import Control.DeepSeq
144−import qualified Control.Category as C
145import qualified LAoP.Matrix.Internal as I
163import qualified LAoP.Matrix.Internal as I
146
164
147newtype Matrix e (cols :: Nat) (rows :: Nat) = M (I.Matrix e (I.FromNat cols) (I.FromNat rows))
165newtype Matrix e (cols :: Nat) (rows :: Nat) = M (I.Matrix e (I.FromNat cols) (I.FromNat rows))
148 deriving (Show, Num, Eq, Ord, NFData) via (I.Matrix e (I.FromNat cols) (I.FromNat rows))
166 deriving (Show, Num, Eq, Ord, NFData) via (I.Matrix e (I.FromNat cols) (I.FromNat rows))
149
167
150−-- | It isn't possible to implement the 'id' function so it's
168+-- | Constraint type synonyms to keep the type signatures less convoluted
151−-- implementation is 'undefined'. However 'comp' can be and this partial
169+type Countable a = KnownNat (I.Count a)
152−-- class implementation exists just to make the code more readable.
170+type CountableDims a b = (Countable a, Countable b)
153−--
171+type CountableN a = KnownNat (I.Count (I.FromNat a))
154−-- Please use 'identity' instead.
172+type CountableNz a = KnownNat (I.Count (I.Normalize a))
155−instance (Num e) => C.Category (Matrix e) where
173+type CountableDimsN a b = (CountableN a, CountableN b)
156− id = undefined
174+type FLN e a b = I.FL (I.FromNat a) (I.FromNat b)
157− (.) = comp
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))
158
179
159-- Primitives
180-- Primitives
160
181
161−empty :: Matrix e 0 0
162−empty = M I.Empty
163−
164one :: e -> Matrix e 1 1
182one :: e -> Matrix e 1 1
165one = M . I.One
183one = M . I.One
166
184
167−junc ::
185+join ::
168− (I.FromNat cols3 ~ Either (I.FromNat cols1) (I.FromNat cols2)) =>
186+ (TrivialE a b) =>
169− Matrix e cols1 rows ->
187+ Matrix e a rows ->
170− Matrix e cols2 rows ->
188+ Matrix e b rows ->
171− Matrix e cols3 rows
189+ Matrix e (a + b) rows
172−junc (M a) (M b) = M (I.Junc a b)
190+join (M a) (M b) = M (I.Join a b)
173
191
174infixl 3 |||
192infixl 3 |||
175(|||) ::
193(|||) ::
176− (I.FromNat cols3 ~ Either (I.FromNat cols1) (I.FromNat cols2)) =>
194+ (TrivialE a b) =>
177− Matrix e cols1 rows ->
195+ Matrix e a rows ->
178− Matrix e cols2 rows ->
196+ Matrix e b rows ->
179− Matrix e cols3 rows
197+ Matrix e (a + b) rows
180−(|||) = junc
198+(|||) = join
181−
199+
182−split ::
200+fork ::
183− (I.FromNat rows3 ~ Either (I.FromNat rows1) (I.FromNat rows2)) =>
201+ (TrivialE a b) =>
184− Matrix e cols rows1 ->
202+ Matrix e cols a ->
185− Matrix e cols rows2 ->
203+ Matrix e cols b ->
186− Matrix e cols rows3
204+ Matrix e cols (a + b)
187−split (M a) (M b) = M (I.Split a b)
205+fork (M a) (M b) = M (I.Fork a b)
188
206
189infixl 2 ===
207infixl 2 ===
190(===) ::
208(===) ::
191− (I.FromNat rows3 ~ Either (I.FromNat rows1) (I.FromNat rows2)) =>
209+ (TrivialE a b) =>
192− Matrix e cols rows1 ->
210+ Matrix e cols a ->
193− Matrix e cols rows2 ->
211+ Matrix e cols b ->
194− Matrix e cols rows3
212+ Matrix e cols (a + b)
195−(===) = split
213+(===) = fork
196
214
197-- Construction
215-- Construction
198
216
199−fromLists :: (I.FromLists e (I.FromNat cols) (I.FromNat rows)) => [[e]] -> Matrix e cols rows
217+fromLists :: (FLN e cols rows) => [[e]] -> Matrix e cols rows
200fromLists = M . I.fromLists
218fromLists = M . I.fromLists
201
219
220+-- | Matrix builder function. Constructs a matrix provided with
221+-- a construction function that operates with indices.
202−matrixBuilder ::
222+matrixBuilder' ::
203− (I.FromLists e (I.FromNat cols) (I.FromNat rows), KnownNat (I.Count (I.FromNat cols)), KnownNat (I.Count (I.FromNat rows))) =>
223+ (FLN e cols rows, CountableN cols, CountableN rows)
204− ((Int, Int) -> e) ->
205− Matrix e cols rows
224+ => ((Int, Int) -> e) -> Matrix e cols rows
206−matrixBuilder = M . I.matrixBuilder
225+matrixBuilder' = M . I.matrixBuilder'
207
226
208−col :: (I.FromLists e () (I.FromNat rows)) => [e] -> Matrix e 1 rows
227+col :: (I.FL () (I.FromNat rows)) => [e] -> Matrix e 1 rows
209col = M . I.col
228col = M . I.col
210
229
211−row :: (I.FromLists e (I.FromNat cols) ()) => [e] -> Matrix e cols 1
230+row :: (I.FL (I.FromNat cols) ()) => [e] -> Matrix e cols 1
212row = M . I.row
231row = M . I.row
213
232
214−fromF ::
233+fromF' ::
215− ( Bounded a,
234+ ( Liftable e a b,
216− Bounded b,
235+ CountableN cols,
217− Enum a,
236+ CountableN rows,
218− Enum b,
237+ FLN e rows cols
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)
225 ) =>
238 ) =>
226 (a -> b) ->
239 (a -> b) ->
227 Matrix e cols rows
240 Matrix e cols rows
228−fromF = M . I.fromF
241+fromF' = M . I.fromF'
229
242
230−fromF' ::
243+fromF ::
231− ( Bounded a,
244+ ( Liftable e a b,
232− Bounded b,
245+ CountableNz a,
233− Enum a,
246+ CountableNz b,
234− Enum b,
247+ FLNz e b a
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)
241 ) =>
248 ) =>
242 (a -> b) ->
249 (a -> b) ->
243 Matrix e (I.Count a) (I.Count b)
250 Matrix e (I.Count a) (I.Count b)
244−fromF' = M . I.fromF'
251+fromF = undefined -- M . I.fromF
245
252
246-- Conversion
253-- Conversion
247
254
@@ -254,21 +261,21 @@ toList (M m) = I.toList m
254-- Zeros Matrix
261-- Zeros Matrix
255
262
256zeros ::
263zeros ::
257− (Num e, I.FromLists e (I.FromNat cols) (I.FromNat rows), KnownNat (I.Count (I.FromNat cols)), KnownNat (I.Count (I.FromNat rows))) =>
264+ (Num e, FLN e cols rows, CountableN cols, CountableN rows) =>
258 Matrix e cols rows
265 Matrix e cols rows
259zeros = M I.zeros
266zeros = M I.zeros
260
267
261-- Ones Matrix
268-- Ones Matrix
262
269
263ones ::
270ones ::
264− (Num e, I.FromLists e (I.FromNat cols) (I.FromNat rows), KnownNat (I.Count (I.FromNat cols)), KnownNat (I.Count (I.FromNat rows))) =>
271+ (Num e, FLN e cols rows, CountableN cols, CountableN rows) =>
265 Matrix e cols rows
272 Matrix e cols rows
266ones = M I.ones
273ones = M I.ones
267
274
268-- Const Matrix
275-- Const Matrix
269
276
270constant ::
277constant ::
271− (Num e, I.FromLists e (I.FromNat cols) (I.FromNat rows), KnownNat (I.Count (I.FromNat cols)), KnownNat (I.Count (I.FromNat rows))) =>
278+ (Num e, FLN e cols rows, CountableN cols, CountableN rows) =>
272 e ->
279 e ->
273 Matrix e cols rows
280 Matrix e cols rows
274constant = M . I.constant
281constant = M . I.constant
@@ -277,40 +284,52 @@ constant = M . I.constant
277
284
278bang ::
285bang ::
279 forall e cols.
286 forall e cols.
280− (Num e, Enum e, I.FromLists e (I.FromNat cols) (), KnownNat (I.Count (I.FromNat cols))) =>
287+ (Num e, Enum e, I.FL (I.FromNat cols) (), CountableN cols) =>
281 Matrix e cols 1
288 Matrix e cols 1
282bang = M I.bang
289bang = M I.bang
283
290
284−-- Identity Matrix
291+-- iden Matrix
285
292
286−identity ::
293+iden ::
287− (Num e, I.FromLists e (I.FromNat cols) (I.FromNat cols), KnownNat (I.Count (I.FromNat cols))) =>
294+ (Num e, FLN e cols cols, CountableN cols) =>
288 Matrix e cols cols
295 Matrix e cols cols
289−identity = M I.identity
296+iden = M I.iden
290
297
291-- Matrix composition (MMM)
298-- Matrix composition (MMM)
292
299
293comp :: (Num e) => Matrix e cr rows -> Matrix e cols cr -> Matrix e cols rows
300comp :: (Num e) => Matrix e cr rows -> Matrix e cols cr -> Matrix e cols rows
294comp (M a) (M b) = M (I.comp a b)
301comp (M a) (M b) = M (I.comp a b)
295
302
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+
296p1 ::
317p1 ::
297 ( Num e,
318 ( Num e,
298− KnownNat (I.Count (I.FromNat n)),
319+ CountableDimsN n m,
299− KnownNat (I.Count (I.FromNat m)),
320+ FLN e n m,
300− I.FromLists e (I.FromNat n) (I.FromNat m),
321+ FLN e m m,
301− I.FromLists e (I.FromNat m) (I.FromNat m),
322+ TrivialE m n
302− I.FromNat (m + n) ~ Either (I.FromNat m) (I.FromNat n)
303 ) =>
323 ) =>
304 Matrix e (m + n) m
324 Matrix e (m + n) m
305p1 = M I.p1
325p1 = M I.p1
306
326
307p2 ::
327p2 ::
308 ( Num e,
328 ( Num e,
309− KnownNat (I.Count (I.FromNat n)),
329+ CountableDimsN n m,
310− KnownNat (I.Count (I.FromNat m)),
330+ FLN e m n,
311− I.FromLists e (I.FromNat m) (I.FromNat n),
331+ FLN e n n,
312− I.FromLists e (I.FromNat n) (I.FromNat n),
332+ TrivialE m n
313− I.FromNat (m + n) ~ Either (I.FromNat m) (I.FromNat n)
314 ) =>
333 ) =>
315 Matrix e (m + n) n
334 Matrix e (m + n) n
316p2 = M I.p2
335p2 = M I.p2
@@ -319,138 +338,125 @@ p2 = M I.p2
319
338
320i1 ::
339i1 ::
321 ( Num e,
340 ( Num e,
322− KnownNat (I.Count (I.FromNat n)),
341+ CountableDimsN n rows,
323− KnownNat (I.Count (I.FromNat rows)),
342+ FLN e n rows,
324− I.FromLists e (I.FromNat n) (I.FromNat rows),
343+ FLN e rows rows,
325− I.FromLists e (I.FromNat rows) (I.FromNat rows),
344+ TrivialE rows n
326− I.FromNat (rows + n) ~ Either (I.FromNat rows) (I.FromNat n)
327 ) =>
345 ) =>
328 Matrix e rows (rows + n)
346 Matrix e rows (rows + n)
329i1 = tr p1
347i1 = tr p1
330
348
331i2 ::
349i2 ::
332 ( Num e,
350 ( Num e,
333− KnownNat (I.Count (I.FromNat rows)),
351+ CountableDimsN rows m,
334− KnownNat (I.Count (I.FromNat m)),
352+ FLN e m rows,
335− I.FromLists e (I.FromNat m) (I.FromNat rows),
353+ FLN e rows rows,
336− I.FromLists e (I.FromNat rows) (I.FromNat rows),
354+ TrivialE m rows
337− I.FromNat (m + rows) ~ Either (I.FromNat m) (I.FromNat rows)
338 ) =>
355 ) =>
339 Matrix e rows (m + rows)
356 Matrix e rows (m + rows)
340i2 = tr p2
357i2 = tr p2
341
358
342-- Dimensions
359-- Dimensions
343
360
344−rows :: (KnownNat (I.Count (I.FromNat rows))) => Matrix e cols rows -> Int
361+rows :: (CountableN rows) => Matrix e cols rows -> Int
345rows (M m) = I.rows m
362rows (M m) = I.rows m
346
363
347−columns :: (KnownNat (I.Count (I.FromNat cols))) => Matrix e cols rows -> Int
364+columns :: (CountableN cols) => Matrix e cols rows -> Int
348columns (M m) = I.columns m
365columns (M m) = I.columns m
349
366
350−-- Coproduct Bifunctor
351−
352infixl 5 -|-
367infixl 5 -|-
353
368
369+-- | Coproduct Bifunctor (Direct sum)
354(-|-) ::
370(-|-) ::
355 ( Num e,
371 ( Num e,
356− KnownNat (I.Count (I.FromNat j)),
372+ CountableDimsN j k,
357− KnownNat (I.Count (I.FromNat k)),
373+ FLN e k k,
358− I.FromLists e (I.FromNat k) (I.FromNat k),
374+ FLN e j k,
359− I.FromLists e (I.FromNat j) (I.FromNat k),
375+ FLN e k j,
360− I.FromLists e (I.FromNat k) (I.FromNat j),
376+ FLN e j j,
361− I.FromLists e (I.FromNat j) (I.FromNat j),
377+ TrivialE n m,
362− I.FromNat (n + m) ~ Either (I.FromNat n) (I.FromNat m),
378+ TrivialE k j
363− I.FromNat (k + j) ~ Either (I.FromNat k) (I.FromNat j)
364 ) =>
379 ) =>
365 Matrix e n k ->
380 Matrix e n k ->
366 Matrix e m j ->
381 Matrix e m j ->
367 Matrix e (n + m) (k + j)
382 Matrix e (n + m) (k + j)
368(-|-) (M a) (M b) = M ((I.-|-) a b)
383(-|-) (M a) (M b) = M ((I.-|-) a b)
369
384
370−-- Khatri Rao Product and projections
385+-- | Khatri Rao Product first projection
371−
386+fstM ::
372−kp1 ::
373 forall e m k .
387 forall e m k .
374 ( Num e,
388 ( Num e,
375− KnownNat (I.Count (I.FromNat m)),
389+ CountableDimsN m k,
376− KnownNat (I.Count (I.FromNat k)),
390+ CountableN (m * k),
377− KnownNat (I.Count (I.FromNat (m * k))),
391+ FLN e (m * k) m,
378− I.FromLists e (I.FromNat (m * k)) (I.FromNat m),
392+ TrivialP m k
379− I.FromNat (m * k) ~ I.FromNat (I.Count (I.FromNat m) * I.Count (I.FromNat k))
380 ) => Matrix e (m * k) m
393 ) => Matrix e (m * k) m
381−kp1 = M (I.kp1 @e @(I.FromNat m) @(I.FromNat k))
394+fstM = M (I.fstM @e @(I.FromNat m) @(I.FromNat k))
382
395
383−kp2 ::
396+-- | Khatri Rao Product second projection
397+sndM ::
384 forall e m k.
398 forall e m k.
385 ( Num e,
399 ( Num e,
386− KnownNat (I.Count (I.FromNat k)),
400+ CountableDimsN k m,
387− I.FromLists e (I.FromNat (m * k)) (I.FromNat k),
401+ FLN e (m * k) k,
388− KnownNat (I.Count (I.FromNat m)),
402+ CountableN (m * k),
389− KnownNat (I.Count (I.FromNat (m * k))),
403+ TrivialP m k
390− I.FromNat (m * k) ~ I.FromNat (I.Count (I.FromNat m) * I.Count (I.FromNat k))
391 ) => Matrix e (m * k) k
404 ) => Matrix e (m * k) k
392−kp2 = M (I.kp2 @e @(I.FromNat m) @(I.FromNat k))
405+sndM = M (I.sndM @e @(I.FromNat m) @(I.FromNat k))
393
406
394−khatri ::
407+-- | Khatri Rao Product
408+kr ::
395 forall e cols a b.
409 forall e cols a b.
396 ( Num e,
410 ( Num e,
397− KnownNat (I.Count (I.FromNat a)),
411+ CountableDimsN a b,
398− KnownNat (I.Count (I.FromNat b)),
412+ CountableN (a * b),
399− KnownNat (I.Count (I.FromNat (a * b))),
413+ FLN e (a * b) a,
400− I.FromLists e (I.FromNat (a * b)) (I.FromNat a),
414+ FLN e (a * b) b,
401− I.FromLists e (I.FromNat (a * b)) (I.FromNat b),
415+ TrivialP a b
402− I.FromNat (a * b) ~ I.FromNat (I.Count (I.FromNat a) * I.Count (I.FromNat b))
403 ) => Matrix e cols a -> Matrix e cols b -> Matrix e cols (a * b)
416 ) => Matrix e cols a -> Matrix e cols b -> Matrix e cols (a * b)
404−khatri a b =
417+kr a b =
405− let kp1' = kp1 @e @a @b
418+ let fstM' = fstM @e @a @b
406− kp2' = kp2 @e @a @b
419+ sndM' = sndM @e @a @b
407− in comp (tr kp1') a * comp (tr kp2') b
420+ in comp (tr fstM') a * comp (tr sndM') b
408−
409−-- Product Bifunctor (Kronecker)
410
421
422+-- | Product Bifunctor (Kronecker)
411infixl 4 ><
423infixl 4 ><
412
424
413(><) ::
425(><) ::
414 forall e m p n q.
426 forall e m p n q.
415 ( Num e,
427 ( Num e,
416− KnownNat (I.Count (I.FromNat m)),
428+ CountableDimsN m n,
417− KnownNat (I.Count (I.FromNat n)),
429+ CountableDimsN p q,
418− KnownNat (I.Count (I.FromNat p)),
430+ CountableDimsN (m * n) (p * q),
419− KnownNat (I.Count (I.FromNat q)),
431+ FLN e (m * n) m,
420− KnownNat (I.Count (I.FromNat (m * n))),
432+ FLN e (m * n) n,
421− KnownNat (I.Count (I.FromNat (p * q))),
433+ FLN e (p * q) p,
422− I.FromLists e (I.FromNat (m * n)) (I.FromNat m),
434+ FLN e (p * q) q,
423− I.FromLists e (I.FromNat (m * n)) (I.FromNat n),
435+ TrivialP m n,
424− I.FromLists e (I.FromNat (p * q)) (I.FromNat p),
436+ TrivialP p q
425− I.FromLists e (I.FromNat (p * q)) (I.FromNat q),
426− I.FromNat (m * n) ~ I.FromNat (I.Count (I.FromNat m) * I.Count (I.FromNat n)),
427− I.FromNat (p * q) ~ I.FromNat (I.Count (I.FromNat p) * I.Count (I.FromNat q))
428 ) => Matrix e m p -> Matrix e n q -> Matrix e (m * n) (p * q)
437 ) => Matrix e m p -> Matrix e n q -> Matrix e (m * n) (p * q)
429(><) a b =
438(><) a b =
430− let kp1' = kp1 @e @m @n
439+ let fstM' = fstM @e @m @n
431− kp2' = kp2 @e @m @n
440+ sndM' = sndM @e @m @n
432− in khatri (comp a kp1') (comp b kp2')
441+ in kr (comp a fstM') (comp b sndM')
433−
434−-- Matrix abide Junc Split
435
442
443+-- | Matrix abide Join Fork
436−abideJS :: Matrix e cols rows -> Matrix e cols rows
444+abideJF :: Matrix e cols rows -> Matrix e cols rows
437−abideJS (M m) = M (I.abideJS m)
445+abideJF (M m) = M (I.abideJF m)
438
446
439−-- Matrix abide Split Junc
447+-- | Matrix abide Fork Join
440−
441−abideSJ :: Matrix e cols rows -> Matrix e cols rows
448+abideFJ :: Matrix e cols rows -> Matrix e cols rows
442−abideSJ (M m) = M (I.abideSJ m)
449+abideFJ (M m) = M (I.abideFJ m)
443−
444−-- Matrix transposition
445
450
451+-- | Matrix transposition
446tr :: Matrix e cols rows -> Matrix e rows cols
452tr :: Matrix e cols rows -> Matrix e rows cols
447tr (M m) = M (I.tr m)
453tr (M m) = M (I.tr m)
448
454
449-- Selective 'select' operator
455-- Selective 'select' operator
450select ::
456select ::
451 ( Num e,
457 ( Num e,
452− I.FromLists e (I.FromNat rows1) (I.FromNat rows1),
458+ FLN e rows1 rows1,
453− KnownNat (I.Count (I.FromNat rows1)),
459+ CountableN rows1,
454 I.FromNat rows2 ~ I.FromNat rows1,
460 I.FromNat rows2 ~ I.FromNat rows1,
455 I.FromNat cols1 ~ I.FromNat cols2,
461 I.FromNat cols1 ~ I.FromNat cols2,
456 I.FromNat rows3 ~ Either (I.FromNat cols3) (I.FromNat rows1)
462 I.FromNat rows3 ~ Either (I.FromNat cols3) (I.FromNat rows1)
@@ -461,14 +467,11 @@ select (M m) (M y) = M (I.select m y)
461
467
462cond ::
468cond ::
463 ( I.FromNat (I.Count (I.FromNat cols)) ~ I.FromNat cols,
469 ( I.FromNat (I.Count (I.FromNat cols)) ~ I.FromNat cols,
464− KnownNat (I.Count (I.FromNat cols)),
470+ CountableN cols,
465− I.FromLists e () (I.FromNat cols),
471+ I.FL () (I.FromNat cols),
466− I.FromLists e (I.FromNat cols) (),
472+ I.FL (I.FromNat cols) (),
467− I.FromLists e (I.FromNat cols) (I.FromNat cols),
473+ FLN e cols cols,
468− Bounded a,
474+ Liftable e a Bool
469− Enum a,
470− Num e,
471− Ord e
472 )
475 )
473 =>
476 =>
474 (a -> Bool) -> Matrix e cols rows -> Matrix e cols rows -> Matrix e cols rows
477 (a -> Bool) -> Matrix e cols rows -> Matrix e cols rows -> Matrix e cols rows
@@ -476,8 +479,12 @@ cond p (M a) (M b) = M (I.cond p a b)
476
479
477-- Pretty print
480-- Pretty print
478
481
479−pretty :: (KnownNat (I.Count (I.FromNat cols)), Show e) => Matrix e cols rows -> String
482+pretty :: (CountableDimsN cols rows, Show e) => Matrix e cols rows -> String
480pretty (M m) = I.pretty m
483pretty (M m) = I.pretty m
481
484
482−prettyPrint :: (KnownNat (I.Count (I.FromNat cols)), Show e) => Matrix e cols rows -> IO ()
485+prettyPrint :: (CountableDimsN cols rows, Show e) => Matrix e cols rows -> IO ()
483prettyPrint (M m) = I.prettyPrint m
486prettyPrint (M m) = I.prettyPrint m
487+
488+-- | Zip two matrices with a given binary function
489+zipWithM :: (e -> f -> g) -> Matrix e cols rows -> Matrix f cols rows -> Matrix g cols rows
490+zipWithM f (M a) (M b) = M (I.zipWithM f a b)
src/LAoP/Matrix/Type.hs+283−240
@@ -1,10 +1,11 @@
1+{-# LANGUAGE ConstraintKinds #-}
2+{-# LANGUAGE TypeFamilies #-}
1{-# LANGUAGE AllowAmbiguousTypes #-}
3{-# LANGUAGE AllowAmbiguousTypes #-}
2{-# LANGUAGE DataKinds #-}
4{-# LANGUAGE DataKinds #-}
3{-# LANGUAGE DerivingVia #-}
5{-# LANGUAGE DerivingVia #-}
4{-# LANGUAGE FlexibleContexts #-}
6{-# LANGUAGE FlexibleContexts #-}
5{-# LANGUAGE FlexibleInstances #-}
7{-# LANGUAGE FlexibleInstances #-}
6{-# LANGUAGE GADTs #-}
8{-# LANGUAGE GADTs #-}
7−{-# LANGUAGE KindSignatures #-}
8{-# LANGUAGE MultiParamTypeClasses #-}
9{-# LANGUAGE MultiParamTypeClasses #-}
9{-# LANGUAGE NoStarIsType #-}
10{-# LANGUAGE NoStarIsType #-}
10{-# LANGUAGE RankNTypes #-}
11{-# LANGUAGE RankNTypes #-}
@@ -55,15 +56,24 @@ module LAoP.Matrix.Type
55 -- * Type safe matrix representation
56 -- * Type safe matrix representation
56 Matrix (..),
57 Matrix (..),
57
58
59+ -- * Constraint type aliases
60+ Countable,
61+ CountableDims,
62+ CountableN,
63+ CountableDimsN,
64+ FLN,
65+ Liftable,
66+ Trivial,
67+ TrivialP,
68+
58 -- * Type aliases
69 -- * Type aliases
59 Zero,
70 Zero,
60 One,
71 One,
61
72
62 -- * Primitives
73 -- * Primitives
63− empty,
64 one,
74 one,
65− junc,
75+ join,
66− split,
76+ fork,
67
77
68 -- * Auxiliary type families
78 -- * Auxiliary type families
69 I.FromNat,
79 I.FromNat,
@@ -75,24 +85,27 @@ module LAoP.Matrix.Type
75 fromLists,
85 fromLists,
76 toLists,
86 toLists,
77 toList,
87 toList,
88+ matrixBuilder',
78 matrixBuilder,
89 matrixBuilder,
79 row,
90 row,
80 col,
91 col,
81 zeros,
92 zeros,
82 ones,
93 ones,
83 bang,
94 bang,
95+ point,
84 constant,
96 constant,
85
97
86 -- * Functor instance equivalent function
98 -- * Functor instance equivalent function
87 fmapM,
99 fmapM,
100+ bimapM,
88
101
89 -- * Applicative/Monoidal instance equivalent functions
102 -- * Applicative/Monoidal instance equivalent functions
90 unitM,
103 unitM,
91 multM,
104 multM,
92
105
93 -- * Selective equivalent instance function
106 -- * Selective equivalent instance function
94− selectM,
107+ selectM,
95−
108+
96 -- * Monad equivalent instance function
109 -- * Monad equivalent instance function
97 returnM,
110 returnM,
98 bindM,
111 bindM,
@@ -100,25 +113,34 @@ module LAoP.Matrix.Type
100 -- * Misc
113 -- * Misc
101 -- ** Get dimensions
114 -- ** Get dimensions
102 columns,
115 columns,
116+ columns',
103 rows,
117 rows,
118+ rows',
104
119
105 -- ** Matrix Transposition
120 -- ** Matrix Transposition
106 tr,
121 tr,
107
122
123+ -- ** Scalar multiplication/division of matrices
124+ (.|),
125+ (./),
126+
108 -- ** McCarthy's Conditional
127 -- ** McCarthy's Conditional
109 cond,
128 cond,
110
129
111 -- ** Matrix "abiding"
130 -- ** Matrix "abiding"
112− abideJS,
131+ abideJF,
113− abideSJ,
132+ abideFJ,
133+
134+ -- ** Zip Matrices
135+ zipWithM,
114
136
115 -- * Biproduct approach
137 -- * Biproduct approach
116− -- ** Split
138+ -- ** Fork
117 (===),
139 (===),
118 -- *** Projections
140 -- *** Projections
119 p1,
141 p1,
120 p2,
142 p2,
121− -- ** Junc
143+ -- ** Join
122 (|||),
144 (|||),
123 -- *** Injections
145 -- *** Injections
124 i1,
146 i1,
@@ -132,11 +154,11 @@ module LAoP.Matrix.Type
132 -- | Note that given the restrictions imposed it is not possible to
154 -- | Note that given the restrictions imposed it is not possible to
133 -- implement the standard type classes present in standard Haskell.
155 -- implement the standard type classes present in standard Haskell.
134 -- *** Matrix pairing projections
156 -- *** Matrix pairing projections
135− kp1,
157+ fstM,
136− kp2,
158+ sndM,
137
159
138 -- *** Matrix pairing
160 -- *** Matrix pairing
139− khatri,
161+ kr,
140
162
141 -- * Matrix composition and lifting
163 -- * Matrix composition and lifting
142
164
@@ -144,10 +166,10 @@ module LAoP.Matrix.Type
144
166
145 -- | Note that given the restrictions imposed it is not possible to
167 -- | Note that given the restrictions imposed it is not possible to
146 -- implement the standard type classes present in standard Haskell.
168 -- implement the standard type classes present in standard Haskell.
147− identity,
169+ iden,
148 comp,
170 comp,
149− fromF,
150 fromF',
171 fromF',
172+ fromF,
151
173
152 -- * Relation
174 -- * Relation
153 toRel,
175 toRel,
@@ -161,23 +183,44 @@ where
161import Data.Void
183import Data.Void
162import Data.Proxy
184import Data.Proxy
163import Data.Kind
185import Data.Kind
164−import GHC.TypeLits
186+import GHC.TypeLits
165import Control.DeepSeq
187import Control.DeepSeq
166import LAoP.Utils
188import LAoP.Utils
167−import qualified Control.Category as C
168import qualified LAoP.Matrix.Internal as I
189import qualified LAoP.Matrix.Internal as I
190+import Prelude hiding (id, (.))
169
191
170newtype Matrix e (cols :: Type) (rows :: Type) = M (I.Matrix e (I.Normalize cols) (I.Normalize rows))
192newtype Matrix e (cols :: Type) (rows :: Type) = M (I.Matrix e (I.Normalize cols) (I.Normalize rows))
171 deriving (Show, Num, Eq, Ord, NFData) via (I.Matrix e (I.Normalize cols) (I.Normalize rows))
193 deriving (Show, Num, Eq, Ord, NFData) via (I.Matrix e (I.Normalize cols) (I.Normalize rows))
172
194
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+
173−-- | It isn't possible to implement the 'id' function so it's
207+-- | It is possible to implement a constrained version of the category type
174−-- implementation is 'undefined'. However 'comp' can be and this partial
208+-- class.
175−-- class implementation exists just to make the code more readable.
176−--
177−-- Please use 'identity' instead.
178−instance (Num e) => C.Category (Matrix e) where
209+instance (Num e) => Category (Matrix e) where
179− id = undefined
210+ type Object (Matrix e) a = (FLN a a, CountableN a)
211+ id = iden
180− (.) = comp
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)
181
224
182-- | Zero type alias
225-- | Zero type alias
183type Zero = Void
226type Zero = Void
@@ -187,92 +230,75 @@ type One = ()
187
230
188-- Primitives
231-- Primitives
189
232
190−-- | Empty matrix constructor
191−empty :: Matrix e Zero Zero
192−empty = M I.Empty
193−
194-- | Unit matrix constructor
233-- | Unit matrix constructor
195one :: e -> Matrix e One One
234one :: e -> Matrix e One One
196one = M . I.One
235one = M . I.One
197
236
198−-- | Matrix 'Junc' constructor
237+-- | Matrix 'Join' constructor
199−junc ::
238+join ::
200− (I.Normalize (Either a b) ~ Either (I.Normalize a) (I.Normalize b)) =>
201 Matrix e a rows ->
239 Matrix e a rows ->
202 Matrix e b rows ->
240 Matrix e b rows ->
203 Matrix e (Either a b) rows
241 Matrix e (Either a b) rows
204−junc (M a) (M b) = M (I.Junc a b)
242+join (M a) (M b) = M (I.Join a b)
205
243
206infixl 3 |||
244infixl 3 |||
207−-- | Matrix 'Junc' constructor
245+-- | Matrix 'Join' constructor
208(|||) ::
246(|||) ::
209− (I.Normalize (Either a b) ~ Either (I.Normalize a) (I.Normalize b)) =>
210 Matrix e a rows ->
247 Matrix e a rows ->
211 Matrix e b rows ->
248 Matrix e b rows ->
212 Matrix e (Either a b) rows
249 Matrix e (Either a b) rows
213−(|||) = junc
250+(|||) = join
214
251
215−-- | Matrix 'Split' constructor
252+-- | Matrix 'Fork' constructor
216−split ::
253+fork ::
217− (I.Normalize (Either a b) ~ Either (I.Normalize a) (I.Normalize b)) =>
218 Matrix e cols a ->
254 Matrix e cols a ->
219 Matrix e cols b ->
255 Matrix e cols b ->
220 Matrix e cols (Either a b)
256 Matrix e cols (Either a b)
221−split (M a) (M b) = M (I.Split a b)
257+fork (M a) (M b) = M (I.Fork a b)
222
258
223infixl 2 ===
259infixl 2 ===
224−-- | Matrix 'Split' constructor
260+-- | Matrix 'Fork' constructor
225(===) ::
261(===) ::
226− (I.Normalize (Either a b) ~ Either (I.Normalize a) (I.Normalize b)) =>
227 Matrix e cols a ->
262 Matrix e cols a ->
228 Matrix e cols b ->
263 Matrix e cols b ->
229 Matrix e cols (Either a b)
264 Matrix e cols (Either a b)
230−(===) = split
265+(===) = fork
231
266
232-- Functor hierarchy
267-- Functor hierarchy
233
268
234-- | Functor instance equivalent function
269-- | Functor instance equivalent function
235−fmapM ::
270+fmapM ::
236− ( Bounded a,
271+ ( Liftable e a b,
237− Bounded b,
272+ CountableDimsN a b,
238− Enum a,
273+ FLN b a
239− Enum b,
240− Eq b,
241− Num e,
242− Ord e,
243− KnownNat (I.Count (I.Normalize a)),
244− KnownNat (I.Count (I.Normalize b)),
245− I.FromLists e (I.Normalize b) (I.Normalize a)
246 )
274 )
247 =>
275 =>
248 (a -> b) -> Matrix e c a -> Matrix e c b
276 (a -> b) -> Matrix e c a -> Matrix e c b
249−fmapM f m = fromF' f `comp` m
277+fmapM f m = fromF f . m
250
278
251-- | Applicative instance equivalent 'unit' function,
279-- | Applicative instance equivalent 'unit' function,
252unitM :: (Num e) => Matrix e () ()
280unitM :: (Num e) => Matrix e () ()
253unitM = one 1
281unitM = one 1
254
282
255-- | Applicative instance equivalent 'unit' function,
283-- | Applicative instance equivalent 'unit' function,
256−multM ::
284+multM ::
257− ( KnownNat (I.Count (I.Normalize a)),
285+ ( CountableDimsN a b,
258− KnownNat (I.Count (I.Normalize b)),
286+ CountableN (a, b),
259− KnownNat (I.Count (I.Normalize (a, b))),
260 Num e,
287 Num e,
261− I.FromLists e (I.Normalize (a, b)) (I.Normalize a),
288+ FLN (a, b) a,
262− I.FromLists e (I.Normalize (a, b)) (I.Normalize b),
289+ FLN (a, b) b,
263− I.Normalize (a, b) ~ I.Normalize (I.Normalize a, I.Normalize b)
290+ TrivialP a b
264 ) => Matrix e c a -> Matrix e c b -> Matrix e c (a, b)
291 ) => Matrix e c a -> Matrix e c b -> Matrix e c (a, b)
265−multM a b = khatri a b
292+multM = kr
266−
267
293
268-- | Monad instance equivalent 'return' function,
294-- | Monad instance equivalent 'return' function,
269−returnM ::
295+returnM ::
270− forall e a .
296+ forall e a .
271− ( Num e,
297+ ( Num e,
272− Enum e,
298+ Enum e,
273− Enum a,
299+ Enum a,
274− I.FromLists e () (I.Normalize a),
300+ FLN () a,
275− KnownNat (I.Count a)
301+ Countable a
276 ) => a -> Matrix e One a
302 ) => a -> Matrix e One a
277returnM a = col l
303returnM a = col l
278 where
304 where
@@ -288,73 +314,64 @@ bindM = flip comp
288
314
289-- | Build a matrix out of a list of list of elements. Throws a runtime
315-- | Build a matrix out of a list of list of elements. Throws a runtime
290-- error if the dimensions do not match.
316-- error if the dimensions do not match.
291−fromLists :: (I.FromLists e (I.Normalize cols) (I.Normalize rows)) => [[e]] -> Matrix e cols rows
317+fromLists :: (FLN cols rows) => [[e]] -> Matrix e cols rows
292fromLists = M . I.fromLists
318fromLists = M . I.fromLists
293
319
294-- | Matrix builder function. Constructs a matrix provided with
320-- | Matrix builder function. Constructs a matrix provided with
295−-- a construction function.
321+-- a construction function that operates with indices.
322+matrixBuilder' ::
323+ (FLN cols rows, CountableDimsN cols rows )
324+ => ((Int, Int) -> e) -> Matrix e cols rows
325+matrixBuilder' = M . I.matrixBuilder'
326+
327+-- | Matrix builder function. Constructs a matrix provided with
328+-- a construction function that operates with arbitrary types.
296matrixBuilder ::
329matrixBuilder ::
297− (I.FromLists e (I.Normalize cols) (I.Normalize rows), KnownNat (I.Count (I.Normalize cols)), KnownNat (I.Count (I.Normalize rows))) =>
330+ ( FLN a b,
298− ((Int, Int) -> e) ->
331+ Enum a,
332+ Enum b,
333+ Bounded a,
334+ Bounded b,
335+ Eq a,
336+ Countable b
299− Matrix e cols rows
337+ ) => ((a, b) -> e) -> Matrix e a b
300−matrixBuilder = M . I.matrixBuilder
338+matrixBuilder f = M (I.matrixBuilder f)
301
339
302-- | Constructs a column vector matrix
340-- | Constructs a column vector matrix
303−col :: (I.FromLists e () (I.Normalize rows)) => [e] -> Matrix e One rows
341+col :: (FLN () rows) => [e] -> Matrix e One rows
304col = M . I.col
342col = M . I.col
305
343
306-- | Constructs a row vector matrix
344-- | Constructs a row vector matrix
307−row :: (I.FromLists e (I.Normalize cols) ()) => [e] -> Matrix e cols One
345+row :: (FLN cols ()) => [e] -> Matrix e cols One
308row = M . I.row
346row = M . I.row
309
347
310-- | Lifts functions to matrices with arbitrary dimensions.
348-- | Lifts functions to matrices with arbitrary dimensions.
311--
349--
312-- NOTE: Be careful to not ask for a matrix bigger than the cardinality of
350-- NOTE: Be careful to not ask for a matrix bigger than the cardinality of
313-- types @a@ or @b@ allows.
351-- types @a@ or @b@ allows.
314−fromF ::
352+fromF' ::
315− ( Bounded a,
353+ ( Liftable e a b,
316− Bounded b,
354+ CountableDimsN cols rows,
317− Enum a,
355+ FLN rows cols
318− Enum b,
319− Eq b,
320− Num e,
321− Ord e,
322− KnownNat (I.Count (I.Normalize cols)),
323− KnownNat (I.Count (I.Normalize rows)),
324− I.FromLists e (I.Normalize rows) (I.Normalize cols)
325 ) =>
356 ) =>
326− (a -> b) ->
327− Matrix e cols rows
357+ (a -> b) -> Matrix e cols rows
328−fromF = M . I.fromF
358+fromF' = M . I.fromF'
329
359
330-- | Lifts functions to matrices with dimensions matching @a@ and @b@
360-- | Lifts functions to matrices with dimensions matching @a@ and @b@
331-- cardinality's.
361-- cardinality's.
332−fromF' ::
362+fromF ::
333− ( Bounded a,
363+ ( Liftable e a b,
334− Bounded b,
364+ CountableDimsN a b,
335− Enum a,
365+ FLN b a
336− Enum b,
337− Eq b,
338− Num e,
339− Ord e,
340− KnownNat (I.Count (I.Normalize a)),
341− KnownNat (I.Count (I.Normalize b)),
342− I.FromLists e (I.Normalize b) (I.Normalize a)
343 ) =>
366 ) =>
344− (a -> b) ->
345− Matrix e a b
367+ (a -> b) -> Matrix e a b
346−fromF' = M . I.fromF'
368+fromF = M . I.fromF
347
369
348-- | Lifts relation functions to Boolean Matrix
370-- | Lifts relation functions to Boolean Matrix
349toRel ::
371toRel ::
350− ( Bounded a,
372+ ( Liftable (Natural 0 1) a b,
351− Bounded b,
373+ CountableDims a b,
352− Enum a,
374+ FLN b a
353− Enum b,
354− Eq b,
355− KnownNat (I.Count (I.Normalize a)),
356− KnownNat (I.Count (I.Normalize b)),
357− I.FromLists (Natural 0 1) (I.Normalize b) (I.Normalize a)
358 ) => (a -> b -> Bool) -> Matrix (Natural 0 1) a b
375 ) => (a -> b -> Bool) -> Matrix (Natural 0 1) a b
359toRel = M . I.toRel
376toRel = M . I.toRel
360
377
@@ -372,8 +389,8 @@ toList (M m) = I.toList m
372
389
373-- | The zero matrix. A matrix wholly filled with zeros.
390-- | The zero matrix. A matrix wholly filled with zeros.
374zeros ::
391zeros ::
375− (Num e, I.FromLists e (I.Normalize cols) (I.Normalize rows), KnownNat (I.Count (I.Normalize cols)), KnownNat (I.Count (I.Normalize rows))) =>
392+ (Num e, FLN cols rows, CountableDimsN cols rows)
376− Matrix e cols rows
393+ => Matrix e cols rows
377zeros = M I.zeros
394zeros = M I.zeros
378
395
379-- Ones Matrix
396-- Ones Matrix
@@ -382,8 +399,8 @@ zeros = M I.zeros
382--
399--
383-- Also known as T (Top) matrix.
400-- Also known as T (Top) matrix.
384ones ::
401ones ::
385− (Num e, I.FromLists e (I.Normalize cols) (I.Normalize rows), KnownNat (I.Count (I.Normalize cols)), KnownNat (I.Count (I.Normalize rows))) =>
402+ (Num e, FLN cols rows, CountableDimsN cols rows)
386− Matrix e cols rows
403+ => Matrix e cols rows
387ones = M I.ones
404ones = M I.ones
388
405
389-- Const Matrix
406-- Const Matrix
@@ -391,9 +408,8 @@ ones = M I.ones
391-- | The constant matrix constructor. A matrix wholly filled with a given
408-- | The constant matrix constructor. A matrix wholly filled with a given
392-- value.
409-- value.
393constant ::
410constant ::
394− (Num e, I.FromLists e (I.Normalize cols) (I.Normalize rows), KnownNat (I.Count (I.Normalize cols)), KnownNat (I.Count (I.Normalize rows))) =>
411+ (Num e, FLN cols rows, CountableDimsN cols rows)
395− e ->
396− Matrix e cols rows
412+ => e -> Matrix e cols rows
397constant = M . I.constant
413constant = M . I.constant
398
414
399-- Bang Matrix
415-- Bang Matrix
@@ -401,17 +417,30 @@ constant = M . I.constant
401-- | The T (Top) row vector matrix.
417-- | The T (Top) row vector matrix.
402bang ::
418bang ::
403 forall e cols.
419 forall e cols.
404− (Num e, Enum e, I.FromLists e (I.Normalize cols) (), KnownNat (I.Count (I.Normalize cols))) =>
420+ (Num e, Enum e, FLN cols (), CountableN cols) =>
405 Matrix e cols One
421 Matrix e cols One
406bang = M I.bang
422bang = M I.bang
407
423
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+
408−-- Identity Matrix
436+-- iden Matrix
409
437
410−-- | Identity matrix
438+-- | iden matrix
411−identity ::
439+iden ::
412− (Num e, I.FromLists e (I.Normalize a) (I.Normalize a), KnownNat (I.Count (I.Normalize a))) =>
440+ (Num e, FLN a a, CountableN a) =>
413 Matrix e a a
441 Matrix e a a
414−identity = M I.identity
442+iden = M I.iden
443+{-# NOINLINE iden #-}
415
444
416-- Matrix composition (MMM)
445-- Matrix composition (MMM)
417
446
@@ -421,15 +450,32 @@ identity = M I.identity
421-- from LAoP.
450-- from LAoP.
422comp :: (Num e) => Matrix e cr rows -> Matrix e cols cr -> Matrix e cols rows
451comp :: (Num e) => Matrix e cr rows -> Matrix e cols cr -> Matrix e cols rows
423comp (M a) (M b) = M (I.comp a b)
452comp (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)
424
472
425-- | Biproduct first component projection
473-- | Biproduct first component projection
426p1 ::
474p1 ::
427 ( Num e,
475 ( Num e,
428− KnownNat (I.Count (I.Normalize n)),
476+ CountableDimsN n m,
429− KnownNat (I.Count (I.Normalize m)),
477+ FLN n m,
430− I.FromLists e (I.Normalize n) (I.Normalize m),
478+ FLN m m
431− I.FromLists e (I.Normalize m) (I.Normalize m),
432− I.Normalize (Either m n) ~ Either (I.Normalize m) (I.Normalize n)
433 ) =>
479 ) =>
434 Matrix e (Either m n) m
480 Matrix e (Either m n) m
435p1 = M I.p1
481p1 = M I.p1
@@ -437,11 +483,9 @@ p1 = M I.p1
437-- | Biproduct second component projection
483-- | Biproduct second component projection
438p2 ::
484p2 ::
439 ( Num e,
485 ( Num e,
440− KnownNat (I.Count (I.Normalize n)),
486+ CountableDimsN n m,
441− KnownNat (I.Count (I.Normalize m)),
487+ FLN m n,
442− I.FromLists e (I.Normalize m) (I.Normalize n),
488+ FLN n n
443− I.FromLists e (I.Normalize n) (I.Normalize n),
444− I.Normalize (Either m n) ~ Either (I.Normalize m) (I.Normalize n)
445 ) =>
489 ) =>
446 Matrix e (Either m n) n
490 Matrix e (Either m n) n
447p2 = M I.p2
491p2 = M I.p2
@@ -451,11 +495,9 @@ p2 = M I.p2
451-- | Biproduct first component injection
495-- | Biproduct first component injection
452i1 ::
496i1 ::
453 ( Num e,
497 ( Num e,
454− KnownNat (I.Count (I.Normalize n)),
498+ CountableDimsN n m,
455− KnownNat (I.Count (I.Normalize m)),
499+ FLN n m,
456− I.FromLists e (I.Normalize n) (I.Normalize m),
500+ FLN m m
457− I.FromLists e (I.Normalize m) (I.Normalize m),
458− I.Normalize (Either m n) ~ Either (I.Normalize m) (I.Normalize n)
459 ) =>
501 ) =>
460 Matrix e m (Either m n)
502 Matrix e m (Either m n)
461i1 = tr p1
503i1 = tr p1
@@ -463,11 +505,9 @@ i1 = tr p1
463-- | Biproduct second component injection
505-- | Biproduct second component injection
464i2 ::
506i2 ::
465 ( Num e,
507 ( Num e,
466− KnownNat (I.Count (I.Normalize n)),
508+ CountableDimsN n m,
467− KnownNat (I.Count (I.Normalize m)),
509+ FLN m n,
468− I.FromLists e (I.Normalize m) (I.Normalize n),
510+ FLN n n
469− I.FromLists e (I.Normalize n) (I.Normalize n),
470− I.Normalize (Either m n) ~ Either (I.Normalize m) (I.Normalize n)
471 ) =>
511 ) =>
472 Matrix e n (Either m n)
512 Matrix e n (Either m n)
473i2 = tr p2
513i2 = tr p2
@@ -476,24 +516,34 @@ i2 = tr p2
476
516
477-- | Obtain the number of rows.
517-- | Obtain the number of rows.
478--
518--
479−-- NOTE: The 'KnownNat' constaint is needed in order to obtain the
519+-- NOTE: The 'KnownNat' constraint is needed in order to obtain the
480−-- dimensions in constant time.
520+-- dimensions in constant time. For a version that doesn't require the
481−--
521+-- constraint see 'rows''.
482−-- TODO: A 'rows' function that does not need the 'KnownNat' constraint in
483−-- exchange for performance.
484−rows :: (KnownNat (I.Count (I.Normalize rows))) => Matrix e cols rows -> Int
522+rows :: (CountableN rows) => Matrix e cols rows -> Int
485rows (M m) = I.rows m
523rows (M m) = I.rows m
486
524
525+-- | Obtain the number of rows in an inefficient manner, but without any
526+-- constraints.
527+--
528+-- For a more efficient version see 'rows'.
529+rows' :: Matrix e cols rows -> Int
530+rows' (M m) = I.rows' m
531+
487-- | Obtain the number of columns.
532-- | Obtain the number of columns.
488−--
489−-- NOTE: The 'KnownNat' constaint is needed in order to obtain the
490−-- dimensions in constant time.
491--
533--
492−-- TODO: A 'columns' function that does not need the 'KnownNat' constraint in
534+-- NOTE: The 'KnownNat' constraint is needed in order to obtain the
493−-- exchange for performance.
535+-- dimensions in constant time. For a version that doesn't require the
536+-- constraint see 'columns''.
494−columns :: (KnownNat (I.Count (I.Normalize cols))) => Matrix e cols rows -> Int
537+columns :: (CountableN cols) => Matrix e cols rows -> Int
495columns (M m) = I.columns m
538columns (M m) = I.columns m
496
539
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+
497-- Coproduct Bifunctor
547-- Coproduct Bifunctor
498
548
499infixl 5 -|-
549infixl 5 -|-
@@ -501,14 +551,11 @@ infixl 5 -|-
501-- | Matrix coproduct functor also known as matrix direct sum.
551-- | Matrix coproduct functor also known as matrix direct sum.
502(-|-) ::
552(-|-) ::
503 ( Num e,
553 ( Num e,
504− KnownNat (I.Count (I.Normalize j)),
554+ CountableDimsN j k,
505− KnownNat (I.Count (I.Normalize k)),
555+ FLN k k,
506− I.FromLists e (I.Normalize k) (I.Normalize k),
556+ FLN j k,
507− I.FromLists e (I.Normalize j) (I.Normalize k),
557+ FLN k j,
508− I.FromLists e (I.Normalize k) (I.Normalize j),
558+ FLN j j
509− I.FromLists e (I.Normalize j) (I.Normalize j),
510− I.Normalize (Either n m) ~ Either (I.Normalize n) (I.Normalize m),
511− I.Normalize (Either k j) ~ Either (I.Normalize k) (I.Normalize j)
512 ) =>
559 ) =>
513 Matrix e n k ->
560 Matrix e n k ->
514 Matrix e m j ->
561 Matrix e m j ->
@@ -518,104 +565,98 @@ infixl 5 -|-
518-- Khatri Rao Product and projections
565-- Khatri Rao Product and projections
519
566
520-- | Khatri Rao product first component projection matrix.
567-- | Khatri Rao product first component projection matrix.
521−kp1 ::
568+fstM ::
522 forall e m k .
569 forall e m k .
523 ( Num e,
570 ( Num e,
524− KnownNat (I.Count (I.Normalize m)),
571+ CountableDimsN m k,
525− KnownNat (I.Count (I.Normalize k)),
572+ CountableN (m, k),
526− KnownNat (I.Count (I.Normalize (m, k))),
573+ FLN (m, k) m,
527− I.FromLists e (I.Normalize (m, k)) (I.Normalize m),
574+ TrivialP m k
528− I.Normalize (m, k) ~ I.Normalize (I.Normalize m, I.Normalize k)
529 ) => Matrix e (m, k) m
575 ) => Matrix e (m, k) m
530−kp1 = M (I.kp1 @e @(I.Normalize m) @(I.Normalize k))
576+fstM = M (I.fstM @e @(I.Normalize m) @(I.Normalize k))
531
577
532-- | Khatri Rao product second component projection matrix.
578-- | Khatri Rao product second component projection matrix.
533−kp2 ::
579+sndM ::
534 forall e m k.
580 forall e m k.
535 ( Num e,
581 ( Num e,
536− KnownNat (I.Count (I.Normalize k)),
582+ CountableDimsN k m,
537− KnownNat (I.Count (I.Normalize m)),
583+ CountableN (m, k),
538− KnownNat (I.Count (I.Normalize (m, k))),
584+ FLN (m, k) k,
539− I.FromLists e (I.Normalize (m, k)) (I.Normalize k),
585+ TrivialP m k
540− I.Normalize (m, k) ~ I.Normalize (I.Normalize m, I.Normalize k)
541 ) => Matrix e (m, k) k
586 ) => Matrix e (m, k) k
542−kp2 = M (I.kp2 @e @(I.Normalize m) @(I.Normalize k))
587+sndM = M (I.sndM @e @(I.Normalize m) @(I.Normalize k))
543
588
544-- | Khatri Rao Matrix product also known as matrix pairing.
589-- | Khatri Rao Matrix product also known as matrix pairing.
545--
590--
546-- NOTE: That this is not a true categorical product, see for instance:
591-- NOTE: That this is not a true categorical product, see for instance:
547−--
592+--
548-- @
593-- @
549−-- | kp1 `comp` khatri a b == a
594+-- | fstM . kr a b == a
550−-- khatri a b ==> |
595+-- kr a b ==> |
551−-- | kp2 `comp` khatri a b == b
596+-- | sndM . kr a b == b
552-- @
597-- @
553--
598--
554-- __Emphasis__ on the implication symbol.
599-- __Emphasis__ on the implication symbol.
555−khatri ::
600+kr ::
556 forall e cols a b.
601 forall e cols a b.
557 ( Num e,
602 ( Num e,
558− KnownNat (I.Count (I.Normalize a)),
603+ CountableDimsN a b,
559− KnownNat (I.Count (I.Normalize b)),
604+ CountableN (a, b),
560− KnownNat (I.Count (I.Normalize (a, b))),
605+ FLN (a, b) a,
561− I.FromLists e (I.Normalize (a, b)) (I.Normalize a),
606+ FLN (a, b) b,
562− I.FromLists e (I.Normalize (a, b)) (I.Normalize b),
607+ TrivialP a b
563− I.Normalize (a, b) ~ I.Normalize (I.Normalize a, I.Normalize b)
564 ) => Matrix e cols a -> Matrix e cols b -> Matrix e cols (a, b)
608 ) => Matrix e cols a -> Matrix e cols b -> Matrix e cols (a, b)
565−khatri a b =
609+kr a b =
566− let kp1' = kp1 @e @a @b
610+ let fstM' = fstM @e @a @b
567− kp2' = kp2 @e @a @b
611+ sndM' = sndM @e @a @b
568− in comp (tr kp1') a * comp (tr kp2') b
612+ in comp (tr fstM') a * comp (tr sndM') b
569
613
570-- Product Bifunctor (Kronecker)
614-- Product Bifunctor (Kronecker)
571
615
572infixl 4 ><
616infixl 4 ><
573
617
574−-- | Matrix product functor also known as kronecker product
618+-- | Matrix product functor also known as Kronecker product
575(><) ::
619(><) ::
576 forall e m p n q.
620 forall e m p n q.
577 ( Num e,
621 ( Num e,
578− KnownNat (I.Count (I.Normalize m)),
622+ CountableDimsN m n,
579− KnownNat (I.Count (I.Normalize n)),
623+ CountableDimsN p q,
580− KnownNat (I.Count (I.Normalize p)),
624+ CountableDimsN (m, n) (p, q),
581− KnownNat (I.Count (I.Normalize q)),
625+ FLN (m, n) m,
582− KnownNat (I.Count (I.Normalize (m, n))),
626+ FLN (m, n) n,
583− KnownNat (I.Count (I.Normalize (p, q))),
627+ FLN (p, q) p,
584− I.FromLists e (I.Normalize (m, n)) (I.Normalize m),
628+ FLN (p, q) q,
585− I.FromLists e (I.Normalize (m, n)) (I.Normalize n),
629+ TrivialP m n,
586− I.FromLists e (I.Normalize (p, q)) (I.Normalize p),
630+ TrivialP p q
587− I.FromLists e (I.Normalize (p, q)) (I.Normalize q),
588− I.Normalize (m, n) ~ I.Normalize (I.Normalize m, I.Normalize n),
589− I.Normalize (p, q) ~ I.Normalize (I.Normalize p, I.Normalize q)
590 ) => Matrix e m p -> Matrix e n q -> Matrix e (m, n) (p, q)
631 ) => Matrix e m p -> Matrix e n q -> Matrix e (m, n) (p, q)
591(><) a b =
632(><) a b =
592− let kp1' = kp1 @e @m @n
633+ let fstM' = fstM @e @m @n
593− kp2' = kp2 @e @m @n
634+ sndM' = sndM @e @m @n
594− in khatri (comp a kp1') (comp b kp2')
635+ in kr (comp a fstM') (comp b sndM')
595
636
596−-- Matrix abide Junc Split
637+-- Matrix abide Join Fork
597
638
598−-- | Matrix "abiding" followin the 'Junc'-'Split' abide law.
639+-- | Matrix "abiding" followin the 'Join'-'Fork' abide law.
599−--
640+--
600-- Law:
641-- Law:
601--
642--
602-- @
643-- @
603−-- 'Junc' ('Split' a c) ('Split' b d) == 'Split' ('Junc' a b) ('Junc' c d)
644+-- 'Join' ('Fork' a c) ('Fork' b d) == 'Fork' ('Join' a b) ('Join' c d)
604-- @
645-- @
605−abideJS :: Matrix e cols rows -> Matrix e cols rows
646+abideJF :: Matrix e cols rows -> Matrix e cols rows
606−abideJS (M m) = M (I.abideJS m)
647+abideJF (M m) = M (I.abideJF m)
607
648
608−-- Matrix abide Split Junc
649+-- Matrix abide Fork Join
609
650
610−-- | Matrix "abiding" followin the 'Split'-'Junc' abide law.
651+-- | Matrix "abiding" followin the 'Fork'-'Join' abide law.
611−--
652+--
612-- Law:
653-- Law:
613--
654--
614-- @
655-- @
615−-- 'Split' ('Junc' a b) ('Junc' c d) == 'Junc' ('Split' a c) ('Split' b d)
656+-- 'Fork' ('Join' a b) ('Join' c d) == 'Join' ('Fork' a c) ('Fork' b d)
616-- @
657-- @
617−abideSJ :: Matrix e cols rows -> Matrix e cols rows
658+abideFJ :: Matrix e cols rows -> Matrix e cols rows
618−abideSJ (M m) = M (I.abideSJ m)
659+abideFJ (M m) = M (I.abideFJ m)
619
660
620-- Matrix transposition
661-- Matrix transposition
621
662
@@ -627,11 +668,10 @@ tr (M m) = M (I.tr m)
627
668
628-- | Selective functors 'select' operator equivalent inspired by the
669-- | Selective functors 'select' operator equivalent inspired by the
629-- ArrowMonad solution presented in the paper.
670-- ArrowMonad solution presented in the paper.
630−selectM ::
671+selectM ::
631 ( Num e,
672 ( Num e,
632− I.FromLists e (I.Normalize b) (I.Normalize b),
673+ FLN b b,
633− KnownNat (I.Count (I.Normalize b)),
674+ CountableN b
634− I.Normalize (Either a b) ~ Either (I.Normalize a) (I.Normalize b)
635 ) => Matrix e cols (Either a b) -> Matrix e a b -> Matrix e cols b
675 ) => Matrix e cols (Either a b) -> Matrix e a b -> Matrix e cols b
636selectM (M m) (M y) = M (I.select m y)
676selectM (M m) (M y) = M (I.select m y)
637
677
@@ -639,15 +679,14 @@ selectM (M m) (M y) = M (I.select m y)
639
679
640-- | McCarthy's Conditional expresses probabilistic choice.
680-- | McCarthy's Conditional expresses probabilistic choice.
641cond ::
681cond ::
642− ( I.Normalize (I.Normalize a) ~ I.Normalize a,
682+ ( Trivial a,
643− KnownNat (I.Count (I.Normalize a)),
683+ Trivial2 a,
644− I.FromLists e () (I.Normalize a),
684+ Trivial3 a,
645− I.FromLists e (I.Normalize a) (),
685+ CountableN a,
646− I.FromLists e (I.Normalize a) (I.Normalize a),
686+ FLN () a,
647− Bounded a,
687+ FLN a (),
648− Enum a,
688+ FLN a a,
649− Num e,
689+ Liftable e a Bool
650− Ord e
651 )
690 )
652 =>
691 =>
653 (a -> Bool) -> Matrix e a b -> Matrix e a b -> Matrix e a b
692 (a -> Bool) -> Matrix e a b -> Matrix e a b -> Matrix e a b
@@ -656,9 +695,13 @@ cond p (M a) (M b) = M (I.cond p a b)
656-- Pretty print
695-- Pretty print
657
696
658-- | Matrix pretty printer
697-- | Matrix pretty printer
659−pretty :: (KnownNat (I.Count (I.Normalize cols)), Show e) => Matrix e cols rows -> String
698+pretty :: (CountableDimsN cols rows, Show e) => Matrix e cols rows -> String
660pretty (M m) = I.pretty m
699pretty (M m) = I.pretty m
661
700
662-- | Matrix pretty printer
701-- | Matrix pretty printer
663−prettyPrint :: (KnownNat (I.Count (I.Normalize cols)), Show e) => Matrix e cols rows -> IO ()
702+prettyPrint :: (CountableDimsN cols rows, Show e) => Matrix e cols rows -> IO ()
664prettyPrint (M m) = I.prettyPrint m
703prettyPrint (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+15−6
@@ -30,12 +30,21 @@ module LAoP.Relation
30 Relation (..),
30 Relation (..),
31 Boolean,
31 Boolean,
32
32
33+ -- * Constraint type synonyms
34+ Countable,
35+ CountableDims,
36+ CountableN,
37+ CountableDimsN,
38+ FLN,
39+ Liftable,
40+ Trivial,
41+ TrivialP,
42+
33 -- * Primitives
43 -- * Primitives
34− empty,
35 one,
44 one,
36− junc,
45+ join,
37 (|||),
46 (|||),
38− split,
47+ fork,
39 (===),
48 (===),
40
49
41 -- * Auxiliary type families
50 -- * Auxiliary type families
@@ -98,8 +107,8 @@ module LAoP.Relation
98 splitR,
107 splitR,
99
108
100 -- ** Projections
109 -- ** Projections
101− p1,
110+ fstR,
102− p2,
111+ sndR,
103 -- ** Bifunctor
112 -- ** Bifunctor
104 (><),
113 (><),
105 -- * Relational coproduct
114 -- * Relational coproduct
@@ -138,7 +147,7 @@ module LAoP.Relation
138 cond,
147 cond,
139
148
140 -- * Relational composition and lifting
149 -- * Relational composition and lifting
141− identity,
150+ iden,
142 comp,
151 comp,
143 fromF,
152 fromF,
144 fromF',
153 fromF',
src/LAoP/Relation/Internal.hs+317−352
@@ -1,3 +1,5 @@
1+{-# LANGUAGE TypeFamilies #-}
2+{-# LANGUAGE ConstraintKinds #-}
1{-# LANGUAGE GADTs #-}
3{-# LANGUAGE GADTs #-}
2{-# LANGUAGE UndecidableInstances #-}
4{-# LANGUAGE UndecidableInstances #-}
3{-# LANGUAGE FlexibleContexts #-}
5{-# LANGUAGE FlexibleContexts #-}
@@ -39,12 +41,21 @@ module LAoP.Relation.Internal
39 Relation (..),
41 Relation (..),
40 Boolean,
42 Boolean,
41
43
44+ -- * Constraint type synonyms
45+ Countable,
46+ CountableDims,
47+ CountableN,
48+ CountableDimsN,
49+ FLN,
50+ Liftable,
51+ Trivial,
52+ TrivialP,
53+
42 -- * Primitives
54 -- * Primitives
43− empty,
44 one,
55 one,
45− junc,
56+ join,
46 (|||),
57 (|||),
47− split,
58+ fork,
48 (===),
59 (===),
49
60
50 -- * Auxiliary type families
61 -- * Auxiliary type families
@@ -55,14 +66,15 @@ module LAoP.Relation.Internal
55 -- * Matrix construction and conversion
66 -- * Matrix construction and conversion
56 I.FromLists,
67 I.FromLists,
57 fromLists,
68 fromLists,
58− fromF,
59 fromF',
69 fromF',
70+ fromF,
60 toRel,
71 toRel,
61 toLists,
72 toLists,
62 toList,
73 toList,
63 toBool,
74 toBool,
64 pt,
75 pt,
65 belongs,
76 belongs,
77+ relationBuilder',
66 relationBuilder,
78 relationBuilder,
67 zeros,
79 zeros,
68 ones,
80 ones,
@@ -107,8 +119,8 @@ module LAoP.Relation.Internal
107 splitR,
119 splitR,
108
120
109 -- ** Projections
121 -- ** Projections
110− p1,
122+ fstR,
111− p2,
123+ sndR,
112 -- ** Bifunctor
124 -- ** Bifunctor
113 (><),
125 (><),
114 -- * Relational coproduct
126 -- * Relational coproduct
@@ -147,10 +159,10 @@ module LAoP.Relation.Internal
147 cond,
159 cond,
148
160
149 -- * Relational composition and lifting
161 -- * Relational composition and lifting
150− identity,
162+ iden,
151 comp,
163 comp,
152− fromF,
153 fromF',
164 fromF',
165+ fromF,
154
166
155 -- ** Relational application
167 -- ** Relational application
156 pointAp,
168 pointAp,
@@ -166,12 +178,13 @@ import Data.Void
166import qualified LAoP.Matrix.Internal as I
178import qualified LAoP.Matrix.Internal as I
167import LAoP.Utils.Internal
179import LAoP.Utils.Internal
168import Control.DeepSeq
180import Control.DeepSeq
169−import qualified Control.Category as C
170import Data.Bool
181import Data.Bool
171import GHC.TypeLits
182import GHC.TypeLits
183+import Prelude hiding (id, (.))
172
184
173-- | Boolean type synonym for working with boolean matrices
185-- | Boolean type synonym for working with boolean matrices
174type Boolean = Natural 0 1
186type Boolean = Natural 0 1
187+type Powerset a = List (List a)
175
188
176-- | Relation data type.
189-- | Relation data type.
177newtype Relation a b = R (I.Matrix Boolean (I.Normalize a) (I.Normalize b))
190newtype Relation a b = R (I.Matrix Boolean (I.Normalize a) (I.Normalize b))
@@ -179,23 +192,31 @@ newtype Relation a b = R (I.Matrix Boolean (I.Normalize a) (I.Normalize b))
179
192
180deriving instance (Read (I.Matrix Boolean (I.Normalize a) (I.Normalize b))) => Read (Relation a b)
193deriving instance (Read (I.Matrix Boolean (I.Normalize a) (I.Normalize b))) => Read (Relation a b)
181
194
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+
182−-- | It isn't possible to implement the 'id' function so it's
205+-- | It is possible to implement a constrained version of the category type
183−-- implementation is 'undefined'. However 'comp' can be and this partial
206+-- class.
184−-- class implementation exists just to make the code more readable.
185−--
186−-- Please use 'identity' instead.
187−instance C.Category Relation where
207+instance Category Relation where
188− id = undefined
208+ type Object Relation a = (FLN a a, CountableN a)
209+ id = iden
189− (.) = comp
210+ (.) = comp
190
211
191instance Num (Relation a b) where
212instance Num (Relation a b) where
192− -- | Matrix addition becomes Boolean matrix disjunction
213+ -- | Matrix addition becomes Boolean matrix disjointion
193 (R a) + (R b) = R (I.orM a b)
214 (R a) + (R b) = R (I.orM a b)
194
215
195 -- | Matrix subtraction becomes Relational subtraction
216 -- | Matrix subtraction becomes Relational subtraction
196 (R a) - (R b) = R (I.subM a b)
217 (R a) - (R b) = R (I.subM a b)
197
218
198− -- | Matrix multiplication becomes Boolean matrix conjunction
219+ -- | Matrix multiplication becomes Boolean matrix conjointion
199 (R a) * (R b) = R (I.andM a b)
220 (R a) * (R b) = R (I.andM a b)
200
221
201 -- | Matrix negation becomes Boolean matrix negation
222 -- | Matrix negation becomes Boolean matrix negation
@@ -207,119 +228,103 @@ type One = ()
207
228
208-- Primitives
229-- Primitives
209
230
210−-- | Empty matrix constructor
211−empty :: Relation Zero Zero
212−empty = R I.Empty
213−
214-- | Unit matrix constructor
231-- | Unit matrix constructor
215one :: Boolean -> Relation One One
232one :: Boolean -> Relation One One
216one = R . I.One
233one = R . I.One
217
234
218−-- | Boolean Matrix 'Junc' constructor, also known as relational coproduct.
235+-- | Boolean Matrix 'Join' constructor, also known as relational coproduct.
219--
236--
220-- See 'eitherR'.
237-- See 'eitherR'.
221−junc :: (I.Normalize (Either a b) ~ Either (I.Normalize a) (I.Normalize b))
222− => Relation a c -> Relation b c -> Relation (Either a b) c
238+join :: Relation a c -> Relation b c -> Relation (Either a b) c
223−junc (R a) (R b) = R (I.Junc a b)
239+join (R a) (R b) = R (I.Join a b)
224
240
225infixl 3 |||
241infixl 3 |||
226−-- | Boolean Matrix 'Junc' constructor
242+-- | Boolean Matrix 'Join' constructor
227--
243--
228-- See 'eitherR'.
244-- See 'eitherR'.
229(|||) ::
245(|||) ::
230− (I.Normalize (Either a b) ~ Either (I.Normalize a) (I.Normalize b)) =>
231 Relation a c ->
246 Relation a c ->
232 Relation b c ->
247 Relation b c ->
233 Relation (Either a b) c
248 Relation (Either a b) c
234−(|||) = junc
249+(|||) = join
235
250
236−-- | Boolean Matrix 'Split' constructor, also known as relational product.
251+-- | Boolean Matrix 'Fork' constructor, also known as relational product.
237−split :: (I.Normalize (Either a b) ~ Either (I.Normalize a) (I.Normalize b))
238− => Relation c a -> Relation c b -> Relation c (Either a b)
252+fork :: Relation c a -> Relation c b -> Relation c (Either a b)
239−split (R a) (R b) = R (I.Split a b)
253+fork (R a) (R b) = R (I.Fork a b)
240
254
241infixl 2 ===
255infixl 2 ===
242−-- | Boolean Matrix 'Split' constructor
256+-- | Boolean Matrix 'Fork' constructor
243(===) ::
257(===) ::
244− (I.Normalize (Either a b) ~ Either (I.Normalize a) (I.Normalize b)) =>
245 Relation c a ->
258 Relation c a ->
246 Relation c b ->
259 Relation c b ->
247 Relation c (Either a b)
260 Relation c (Either a b)
248−(===) = split
261+(===) = fork
249
262
250-- Construction
263-- Construction
251
264
252-- | Build a matrix out of a list of list of elements. Throws a runtime
265-- | Build a matrix out of a list of list of elements. Throws a runtime
253-- error if the dimensions do not match.
266-- error if the dimensions do not match.
254−fromLists :: (I.FromLists Boolean (I.Normalize a) (I.Normalize b)) => [[Boolean]] -> Relation a b
267+fromLists :: (FLN a b) => [[Boolean]] -> Relation a b
255fromLists = R . I.fromLists
268fromLists = R . I.fromLists
256
269
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+
257−-- | Matrix builder function. Constructs a matrix provided with
277+-- | Relation builder function. Constructs a relation provided with
258−-- a construction function.
278+-- a construction function that operates with arbitrary types.
259relationBuilder ::
279relationBuilder ::
260− (I.FromLists Boolean (I.Normalize a) (I.Normalize b), KnownNat (I.Count (I.Normalize a)), KnownNat (I.Count (I.Normalize b))) =>
280+ ( FLN a b,
261− ((Int, Int) -> Boolean) ->
281+ Enum a,
282+ Enum b,
283+ Bounded a,
284+ Bounded b,
285+ Eq a,
286+ CountableDims a b
262− Relation a b
287+ ) => ((a, b) -> Boolean) -> Relation a b
263relationBuilder = R . I.matrixBuilder
288relationBuilder = R . I.matrixBuilder
264
289
265-- | Lifts functions to matrices with arbitrary dimensions.
290-- | Lifts functions to matrices with arbitrary dimensions.
266--
291--
267-- NOTE: Be careful to not ask for a matrix bigger than the cardinality of
292-- NOTE: Be careful to not ask for a matrix bigger than the cardinality of
268-- types @a@ or @b@ allows.
293-- types @a@ or @b@ allows.
269−fromF ::
294+fromF' ::
270− ( Bounded a,
295+ ( Liftable a b,
271− Bounded b,
296+ CountableDimsN c d,
272− Enum a,
297+ FLN d c
273− Enum b,
274− Eq b,
275− KnownNat (I.Count (I.Normalize c)),
276− KnownNat (I.Count (I.Normalize d)),
277− I.FromLists Boolean (I.Normalize d) (I.Normalize c)
278 )
298 )
279 => (a -> b) -> Relation c d
299 => (a -> b) -> Relation c d
280−fromF f = R (I.fromFRel f)
300+fromF' f = R (I.fromFRel' f)
281
301
282-- | Lifts functions to matrices with dimensions matching @a@ and @b@
302-- | Lifts functions to matrices with dimensions matching @a@ and @b@
283-- cardinality's.
303-- cardinality's.
284−fromF' ::
304+fromF ::
285− ( Bounded b,
305+ ( Liftable a b,
286− Bounded a,
306+ CountableDimsN a b,
287− Enum a,
307+ FLN b a
288− Enum b,
289− Eq b,
290− KnownNat (I.Count (I.Normalize a)),
291− KnownNat (I.Count (I.Normalize b)),
292− I.FromLists Boolean (I.Normalize b) (I.Normalize a)
293 )
308 )
294 => (a -> b) -> Relation a b
309 => (a -> b) -> Relation a b
295−fromF' f = R (I.fromFRel' f)
310+fromF f = R (I.fromFRel f)
296
311
297-- | Lifts relation functions to 'Relation'
312-- | Lifts relation functions to 'Relation'
298toRel ::
313toRel ::
299− ( Bounded b,
314+ ( Liftable a b,
300− Bounded a,
315+ CountableDims a b,
301− Enum a,
316+ FLN b a
302− Enum b,
303− Eq b,
304− KnownNat (I.Count (I.Normalize a)),
305− KnownNat (I.Count (I.Normalize b)),
306− I.FromLists Boolean (I.Normalize b) (I.Normalize a)
307 )
317 )
308− => (a -> b -> Bool) -> Relation a b
318+ => (a -> b -> Bool) -> Relation a b
309toRel = R . I.toRel
319toRel = R . I.toRel
310
320
311-- | Lowers a 'Relation' to a function
321-- | Lowers a 'Relation' to a function
312fromRel ::
322fromRel ::
313− ( Bounded a,
323+ ( Liftable a b,
314− Bounded b,
315− Enum a,
316− Enum b,
317 Eq a,
324 Eq a,
318− Eq b,
325+ CountableDimsN a b,
319− KnownNat (I.Count (I.Normalize a)),
326+ FLN a One,
320− KnownNat (I.Count (I.Normalize b)),
327+ FLN b One
321− I.FromLists Boolean (I.Normalize a) One,
322− I.FromLists Boolean (I.Normalize b) One
323 )
328 )
324 => Relation a b -> (a -> b -> Bool)
329 => Relation a b -> (a -> b -> Bool)
325fromRel r a b = pointApBool a b r
330fromRel r a b = pointApBool a b r
@@ -343,52 +348,46 @@ toBool r = case toList r of
343-- | Power transpose.
348-- | Power transpose.
344--
349--
345-- Maps a relation to a set valued function.
350-- Maps a relation to a set valued function.
346−pt ::
351+pt ::
347− ( Bounded a,
352+ ( Liftable a b,
348− Bounded b,
349− Enum a,
350− Enum b,
351 Eq a,
353 Eq a,
352− Eq b,
354+ CountableDimsN a b,
353− KnownNat (I.Count (I.Normalize a)),
355+ FLN a One,
354− KnownNat (I.Count (I.Normalize b)),
356+ FLN b One
355− I.FromLists Boolean (I.Normalize a) One,
356− I.FromLists Boolean (I.Normalize b) One
357 )
357 )
358− => Relation a b -> (a -> Powerset b)
358+ => Relation a b -> (a -> List b)
359pt r a =
359pt r a =
360− let (PS lb) = maxBound
360+ let (L lb) = maxBound
361− in PS [ b | b <- lb, toBool (pointAp a b r) ]
361+ in L [ b | b <- lb, toBool (pointAp a b r) ]
362
362
363-- | Belongs relation
363-- | Belongs relation
364belongs ::
364belongs ::
365 ( Bounded a,
365 ( Bounded a,
366 Enum a,
366 Enum a,
367 Eq a,
367 Eq a,
368− KnownNat (I.Count (I.Normalize (Powerset a))),
368+ CountableDims (List a) a,
369− KnownNat (I.Count (I.Normalize a)),
369+ FLN a (List a)
370− I.FromLists Boolean (I.Normalize a) (I.Normalize (Powerset a))
371 )
370 )
372− => Relation (Powerset a) a
371+ => Relation (List a) a
373−belongs = toRel (flip elemR)
372+belongs = toRel elemR
374 where
373 where
375− elemR x (PS l) = x `elem` l
374+ elemR (L l) x = x `elem` l
376
375
377-- Zeros Matrix
376-- Zeros Matrix
378
377
379-- | The zero relation. A relation where no element of type @a@ relates
378-- | The zero relation. A relation where no element of type @a@ relates
380-- with elements of type @b@.
379-- with elements of type @b@.
381--
380--
382−-- Also known as ⊥ (Bottom) Relation or empty Relation.
381+-- Also known as ⊥ (Bottom) Relation.
383--
382--
384-- @
383-- @
385−-- r `'comp'` ⊥ == ⊥ `'comp'` r == ⊥
384+-- r `.` ⊥ == ⊥ `.` r == ⊥
386−-- ⊥ `'sse'` R && R `'sse'` T == True
385+-- ⊥ ``sse`` R && R ``sse`` T == True
387-- @
386-- @
388zeros ::
387zeros ::
389− (I.FromLists Boolean (I.Normalize a) (I.Normalize b), KnownNat (I.Count (I.Normalize a)), KnownNat (I.Count (I.Normalize b))) =>
388+ (FLN a b, CountableDimsN a b) =>
390 Relation a b
389 Relation a b
391−zeros = relationBuilder (const (nat 0))
390+zeros = relationBuilder' (const (nat 0))
392
391
393-- Ones Matrix
392-- Ones Matrix
394
393
@@ -398,47 +397,46 @@ zeros = relationBuilder (const (nat 0))
398-- Also known as T (Top) Relation or universal Relation.
397-- Also known as T (Top) Relation or universal Relation.
399--
398--
400-- @
399-- @
401−-- ⊥ `'sse'` R && R `'sse'` T == True
400+-- ⊥ ``sse`` R && R ``sse`` T == True
402-- @
401-- @
403ones ::
402ones ::
404− (I.FromLists Boolean (I.Normalize a) (I.Normalize b), KnownNat (I.Count (I.Normalize a)), KnownNat (I.Count (I.Normalize b))) =>
403+ (FLN a b, CountableDimsN a b) =>
405 Relation a b
404 Relation a b
406−ones = relationBuilder (const (nat 1))
405+ones = relationBuilder' (const (nat 1))
407
406
408-- Bang Matrix
407-- Bang Matrix
409
408
410-- | The T (Top) row vector relation.
409-- | The T (Top) row vector relation.
411bang ::
410bang ::
412− (I.FromLists Boolean (I.Normalize a) One, KnownNat (I.Count (I.Normalize a))) =>
411+ (FLN a One, CountableN a) =>
413 Relation a One
412 Relation a One
414bang = ones
413bang = ones
415
414
416-- | Point constant relation
415-- | Point constant relation
417−point ::
416+point ::
418 ( Bounded a,
417 ( Bounded a,
419 Enum a,
418 Enum a,
420 Eq a,
419 Eq a,
421− KnownNat (I.Count (I.Normalize a)),
420+ CountableN a,
422− I.FromLists Boolean (I.Normalize a) One
421+ FLN a One
423 ) => a -> Relation One a
422 ) => a -> Relation One a
424−point = fromF' . const
423+point = fromF . const
425
424
426−-- Identity Matrix
425+-- iden Matrix
427
426
428−-- | Identity matrix
427+-- | iden matrix
429--
428--
430-- @
429-- @
431−-- 'identity' `'comp'` r == r == r `'comp'` 'identity'
430+-- 'iden' `.` r == r == r `.` 'iden'
432-- @
431-- @
433−identity ::
432+iden ::
434− (I.FromLists Boolean (I.Normalize a) (I.Normalize a), KnownNat (I.Count (I.Normalize a))) =>
435− Relation a a
433+ (FLN a a, CountableN a) => Relation a a
436−identity = relationBuilder (bool (nat 0) (nat 1) . uncurry (==))
434+iden = relationBuilder' (bool (nat 0) (nat 1) . uncurry (==))
437
435
438-- | Relational composition
436-- | Relational composition
439--
437--
440-- @
438-- @
441−-- r `'comp'` (s `'comp'` p) = (r `'comp'` s) `'comp'` p
439+-- r `.` (s `.` p) = (r `.` s) `.` p
442-- @
440-- @
443comp :: Relation b c -> Relation a b -> Relation a c
441comp :: Relation b c -> Relation a b -> Relation a c
444comp (R a) (R b) = R (I.compRel a b)
442comp (R a) (R b) = R (I.compRel a b)
@@ -469,7 +467,7 @@ divS (R x) (R y) = R (I.divS x y)
469
467
470-- | Relational shrinking.
468-- | Relational shrinking.
471--
469--
472−-- @r `'shrunkBy'` s@ is the largest part of @r@ such that,
470+-- @r ``shrunkBy`` s@ is the largest part of @r@ such that,
473-- if it yields an output for an input @x@, it must be a maximum,
471-- if it yields an output for an input @x@, it must be a maximum,
474-- with respect to @s@, among all possible outputs of @x@ by @r@.
472-- with respect to @s@, among all possible outputs of @x@ by @r@.
475shrunkBy :: Relation b a -> Relation a a -> Relation b a
473shrunkBy :: Relation b a -> Relation a a -> Relation b a
@@ -477,54 +475,44 @@ shrunkBy r s = r `intersection` divR s (conv r)
477
475
478-- | Relational overriding.
476-- | Relational overriding.
479--
477--
480−-- @r `'overriddenBy'` s@ yields the relation which contains the
478+-- @r ``overriddenBy`` s@ yields the relation which contains the
481-- whole of @s@ and that part of @r@ where @s@ is undefined.
479-- whole of @s@ and that part of @r@ where @s@ is undefined.
482--
480--
483-- @
481-- @
484−-- 'zeros' `'overriddenBy'` s == s
482+-- 'zeros' ``overriddenBy`` s == s
485−-- r `'overriddenBy'` 'zeros' == r
483+-- r ``overriddenBy`` 'zeros' == r
486−-- r `'overriddenBy'` r == r
484+-- r ``overriddenBy`` r == r
487-- @
485-- @
488overriddenBy ::
486overriddenBy ::
489− ( I.FromLists Boolean (I.Normalize b) (I.Normalize b),
487+ ( FLN b b,
490− KnownNat (I.Count (I.Normalize b))
488+ CountableN b
491 ) => Relation a b -> Relation a b -> Relation a b
489 ) => Relation a b -> Relation a b -> Relation a b
492overriddenBy r s = s `union` r `intersection` divR zeros (conv s)
490overriddenBy r s = s `union` r `intersection` divR zeros (conv s)
493
491
494-- | Relational application.
492-- | Relational application.
495--
493--
496-- If @a@ and @b@ are related by 'Relation' @r@
494-- If @a@ and @b@ are related by 'Relation' @r@
497−-- then @'pointAp' a b r == 'one' ('Nat' 1)@
495+-- then @'pointAp' a b r == 'one' ('nat' 1)@
498pointAp ::
496pointAp ::
499− ( Bounded a,
497+ ( Liftable a b,
500− Bounded b,
501− Enum a,
502− Enum b,
503 Eq a,
498 Eq a,
504− Eq b,
499+ CountableDimsN a b,
505− KnownNat (I.Count (I.Normalize a)),
500+ FLN a One,
506− KnownNat (I.Count (I.Normalize b)),
501+ FLN b One
507− I.FromLists Boolean (I.Normalize a) One,
508− I.FromLists Boolean (I.Normalize b) One
509 ) => a -> b -> Relation a b -> Relation One One
502 ) => a -> b -> Relation a b -> Relation One One
510−pointAp a b r = conv (point b) `comp` r `comp` point a
503+pointAp a b r = conv (point b) . r . point a
511
504
512-- | Relational application
505-- | Relational application
513--
506--
514-- The same as 'pointAp' but converts 'Boolean' to 'Bool'
507-- The same as 'pointAp' but converts 'Boolean' to 'Bool'
515pointApBool ::
508pointApBool ::
516− ( Bounded a,
509+ ( Liftable a b,
517− Bounded b,
518− Enum a,
519− Enum b,
520 Eq a,
510 Eq a,
521− Eq b,
511+ CountableDimsN a b,
522− KnownNat (I.Count (I.Normalize a)),
512+ FLN a One,
523− KnownNat (I.Count (I.Normalize b)),
513+ FLN b One
524− I.FromLists Boolean (I.Normalize a) One,
525− I.FromLists Boolean (I.Normalize b) One
526 ) => a -> b -> Relation a b -> Bool
514 ) => a -> b -> Relation a b -> Bool
527−pointApBool a b r = toBool $ conv (point b) `comp` r `comp` point a
515+pointApBool a b r = toBool $ conv (point b) . r . point a
528
516
529-- | Relational converse
517-- | Relational converse
530--
518--
@@ -550,24 +538,24 @@ iff r s = r == s
550
538
551-- | Relational intersection
539-- | Relational intersection
552--
540--
553−-- Lifts pointwise conjunction.
541+-- Lifts pointwise conjointion.
554--
542--
555-- @
543-- @
556−-- (r `'intersection'` s) `'intersection'` t == r `'intersection' (s `'intersection'` t)
544+-- (r ``intersection`` s) ``intersection`` t == r ``intersection`` (s ``intersection`` t)
557−-- x `'sse'` r `'intersection'` s == x `'intersection'` r && x `'intersection'` s
545+-- x ``sse`` r ``intersection`` s == x ``intersection`` r && x ``intersection`` s
558-- @
546-- @
559intersection :: Relation a b -> Relation a b -> Relation a b
547intersection :: Relation a b -> Relation a b -> Relation a b
560intersection a b = a * b
548intersection a b = a * b
561
549
562-- | Relational union
550-- | Relational union
563--
551--
564−-- Lifts pointwise disjunction.
552+-- Lifts pointwise disjointion.
565--
553--
566-- @
554-- @
567−-- (r `'union'` s) `'union'` t == r `'union' (s `'union'` t)
555+-- (r ``union`` s) ``union`` t == r `'union' (s ``union`` t)
568−-- r `'union'` s `'sse'` x == r `'sse'` x && s `'sse'` x
556+-- r ``union`` s ``sse`` x == r ``sse`` x && s ``sse`` x
569−-- r `'comp'` (s `'union'` t) == (r `'comp'` s) `'union'` (r `'comp'` t)
557+-- r `.` (s ``union`` t) == (r `.` s) ``union`` (r `.` t)
570−-- (s `'union'` t) `'comp'` r == (s `'comp'` r) `'union'` (t `'comp'` r)
558+-- (s ``union`` t) `.` r == (s `.` r) ``union`` (t `.` r)
571-- @
559-- @
572union :: Relation a b -> Relation a b -> Relation a b
560union :: Relation a b -> Relation a b -> Relation a b
573union a b = a + b
561union a b = a + b
@@ -575,46 +563,46 @@ union a b = a + b
575-- | Relation Kernel
563-- | Relation Kernel
576--
564--
577-- @
565-- @
578−-- 'ker' r == 'conv' r `'comp'` r
566+-- 'ker' r == 'conv' r `.` r
579-- 'ker' r == 'img' ('conv' r)
567-- 'ker' r == 'img' ('conv' r)
580-- @
568-- @
581ker :: Relation a b -> Relation a a
569ker :: Relation a b -> Relation a a
582−ker r = conv r `comp` r
570+ker r = conv r . r
583
571
584-- | Relation Image
572-- | Relation Image
585--
573--
586-- @
574-- @
587−-- 'img' r == r `'comp'` conv r
575+-- 'img' r == r `.` conv r
588-- 'img' r == 'ker' ('conv' r)
576-- 'img' r == 'ker' ('conv' r)
589-- @
577-- @
590img :: Relation a b -> Relation b b
578img :: Relation a b -> Relation b b
591−img r = r `comp` conv r
579+img r = r . conv r
592
580
593-- | Function division. Special case of 'divS'.
581-- | Function division. Special case of 'divS'.
594--
582--
595-- NOTE: _This is only valid_ if @f@ and @g@ are 'function's, i.e. 'simple' and
583-- NOTE: _This is only valid_ if @f@ and @g@ are 'function's, i.e. 'simple' and
596-- 'entire'.
584-- 'entire'.
597--
585--
598−-- @division f g == conv g `'comp'` f@
586+-- @'divisionF' f g == 'conv' g `.` f@
599divisionF :: Relation a c -> Relation b c -> Relation a b
587divisionF :: Relation a c -> Relation b c -> Relation a b
600−divisionF f g = conv g `comp` f
588+divisionF f g = conv g . f
601
589
602-- Taxonomy of binary relations
590-- Taxonomy of binary relations
603
591
604-- | A 'Relation' @r@ is 'simple' 'iff' @'coreflexive' ('img' r)@
592-- | A 'Relation' @r@ is 'simple' 'iff' @'coreflexive' ('img' r)@
605−simple :: (KnownNat (I.Count (I.Normalize b)), I.FromLists Boolean (I.Normalize b) (I.Normalize b)) => Relation a b -> Bool
593+simple :: (CountableN b, FLN b b) => Relation a b -> Bool
606simple = coreflexive . img
594simple = coreflexive . img
607
595
608-- | A 'Relation' @r@ is 'injective' 'iff' @'coreflexive' ('ker' r)@
596-- | A 'Relation' @r@ is 'injective' 'iff' @'coreflexive' ('ker' r)@
609−injective :: (KnownNat (I.Count (I.Normalize a)), I.FromLists Boolean (I.Normalize a) (I.Normalize a)) => Relation a b -> Bool
597+injective :: (CountableN a, FLN a a) => Relation a b -> Bool
610injective = coreflexive . ker
598injective = coreflexive . ker
611
599
612-- | A 'Relation' @r@ is 'entire' 'iff' @'reflexive' ('ker' r)@
600-- | A 'Relation' @r@ is 'entire' 'iff' @'reflexive' ('ker' r)@
613−entire :: (KnownNat (I.Count (I.Normalize a)), I.FromLists Boolean (I.Normalize a) (I.Normalize a)) => Relation a b -> Bool
601+entire :: (CountableN a, FLN a a) => Relation a b -> Bool
614entire = reflexive . ker
602entire = reflexive . ker
615
603
616-- | A 'Relation' @r@ is 'surjective' 'iff' @'reflexive' ('img' r)@
604-- | A 'Relation' @r@ is 'surjective' 'iff' @'reflexive' ('img' r)@
617−surjective :: (KnownNat (I.Count (I.Normalize b)), I.FromLists Boolean (I.Normalize b) (I.Normalize b)) => Relation a b -> Bool
605+surjective :: (CountableN b, FLN b b) => Relation a b -> Bool
618surjective = reflexive . img
606surjective = reflexive . img
619
607
620-- | A 'Relation' @r@ is a 'function' 'iff' @'simple' r && 'entire' r@
608-- | A 'Relation' @r@ is a 'function' 'iff' @'simple' r && 'entire' r@
@@ -623,118 +611,113 @@ surjective = reflexive . img
623-- relations:
611-- relations:
624--
612--
625-- @
613-- @
626−-- f `'comp'` r `'sse'` s == r `'sse'` f `'comp'` s
614+-- f `.` r ``sse`` s == r ``sse`` f `.` s
627−-- r `'comp'` f `'sse'` s == r `'sse'` s `'comp'` f
615+-- r `.` f ``sse`` s == r ``sse`` s `.` f
628-- @
616-- @
629function ::
617function ::
630− ( KnownNat (I.Count (I.Normalize b)),
618+ ( CountableDimsN a b,
631− KnownNat (I.Count (I.Normalize a)),
619+ FLN a a,
632− I.FromLists Boolean (I.Normalize a) (I.Normalize a),
620+ FLN b b
633− I.FromLists Boolean (I.Normalize b) (I.Normalize b)
634 )
621 )
635 => Relation a b -> Bool
622 => Relation a b -> Bool
636function r = simple r && entire r
623function r = simple r && entire r
637
624
638-- | A 'Relation' @r@ is a 'representation' 'iff' @'injective' r && 'entire' r@
625-- | A 'Relation' @r@ is a 'representation' 'iff' @'injective' r && 'entire' r@
639representation ::
626representation ::
640− ( KnownNat (I.Count (I.Normalize a)),
627+ ( CountableN a,
641− I.FromLists Boolean (I.Normalize a) (I.Normalize a)
628+ FLN a a
642 )
629 )
643 => Relation a b -> Bool
630 => Relation a b -> Bool
644representation r = injective r && entire r
631representation r = injective r && entire r
645
632
646-- | A 'Relation' @r@ is an 'abstraction' 'iff' @'surjective' r && 'simple' r@
633-- | A 'Relation' @r@ is an 'abstraction' 'iff' @'surjective' r && 'simple' r@
647abstraction ::
634abstraction ::
648− ( KnownNat (I.Count (I.Normalize b)),
635+ ( CountableN b,
649− I.FromLists Boolean (I.Normalize b) (I.Normalize b)
636+ FLN b b
650 )
637 )
651 => Relation a b -> Bool
638 => Relation a b -> Bool
652abstraction r = surjective r && simple r
639abstraction r = surjective r && simple r
653
640
654-- | A 'Relation' @r@ is a 'surjection' 'iff' @'function' r && 'abstraction' r@
641-- | A 'Relation' @r@ is a 'surjection' 'iff' @'function' r && 'abstraction' r@
655surjection ::
642surjection ::
656− ( KnownNat (I.Count (I.Normalize b)),
643+ ( CountableDimsN a b,
657− KnownNat (I.Count (I.Normalize a)),
644+ FLN a a,
658− I.FromLists Boolean (I.Normalize a) (I.Normalize a),
645+ FLN b b
659− I.FromLists Boolean (I.Normalize b) (I.Normalize b)
660 )
646 )
661 => Relation a b -> Bool
647 => Relation a b -> Bool
662surjection r = function r && abstraction r
648surjection r = function r && abstraction r
663
649
664-- | A 'Relation' @r@ is a 'injection' 'iff' @'function' r && 'representation' r@
650-- | A 'Relation' @r@ is a 'injection' 'iff' @'function' r && 'representation' r@
665injection ::
651injection ::
666− ( KnownNat (I.Count (I.Normalize b)),
652+ ( CountableDimsN a b,
667− KnownNat (I.Count (I.Normalize a)),
653+ FLN a a,
668− I.FromLists Boolean (I.Normalize a) (I.Normalize a),
654+ FLN b b
669− I.FromLists Boolean (I.Normalize b) (I.Normalize b)
670 )
655 )
671 => Relation a b -> Bool
656 => Relation a b -> Bool
672injection r = function r && representation r
657injection r = function r && representation r
673
658
674-- | A 'Relation' @r@ is an 'bijection' 'iff' @'injection' r && 'surjection' r@
659-- | A 'Relation' @r@ is an 'bijection' 'iff' @'injection' r && 'surjection' r@
675bijection ::
660bijection ::
676− ( KnownNat (I.Count (I.Normalize b)),
661+ ( CountableDimsN a b,
677− KnownNat (I.Count (I.Normalize a)),
662+ FLN b b,
678− I.FromLists Boolean (I.Normalize b) (I.Normalize b),
663+ FLN a a
679− I.FromLists Boolean (I.Normalize a) (I.Normalize a)
680 ) => Relation a b -> Bool
664 ) => Relation a b -> Bool
681bijection r = injection r && surjection r
665bijection r = injection r && surjection r
682
666
683−
684-- Properties of relations
667-- Properties of relations
685
668
686−-- | A 'Relation' @r@ is 'reflexive' 'iff' @'identity' `'sse'` r@
669+-- | A 'Relation' @r@ is 'reflexive' 'iff' @'id' ``sse`` r@
687−reflexive :: (KnownNat (I.Count (I.Normalize a)), I.FromLists Boolean (I.Normalize a) (I.Normalize a)) => Relation a a -> Bool
670+reflexive :: (CountableN a, FLN a a) => Relation a a -> Bool
688−reflexive r = identity <= r
671+reflexive r = id <= r
689
672
690−-- | A 'Relation' @r@ is 'coreflexive' 'iff' @r `'sse'` 'identity'@
673+-- | A 'Relation' @r@ is 'coreflexive' 'iff' @r ``sse`` 'id'@
691−coreflexive :: (KnownNat (I.Count (I.Normalize a)), I.FromLists Boolean (I.Normalize a) (I.Normalize a)) => Relation a a -> Bool
674+coreflexive :: (CountableN a, FLN a a) => Relation a a -> Bool
692−coreflexive r = r <= identity
675+coreflexive r = r <= id
693
676
694−-- | A 'Relation' @r@ is 'transitive' 'iff' @(r `'comp'` r) `'sse'` r@
677+-- | A 'Relation' @r@ is 'transitive' 'iff' @(r `.` r) ``sse`` r@
695transitive :: Relation a a -> Bool
678transitive :: Relation a a -> Bool
696−transitive r = (r `comp` r) `sse` r
679+transitive r = (r . r) `sse` r
697
680
698-- | A 'Relation' @r@ is 'symmetric' 'iff' @r == 'conv' r@
681-- | A 'Relation' @r@ is 'symmetric' 'iff' @r == 'conv' r@
699symmetric :: Relation a a -> Bool
682symmetric :: Relation a a -> Bool
700symmetric r = r == conv r
683symmetric r = r == conv r
701
684
702−-- | A 'Relation' @r@ is anti-symmetric 'iff' @(r `'intersection'` 'conv' r) `'sse'` 'identity'@
685+-- | A 'Relation' @r@ is anti-symmetric 'iff' @(r ``intersection`` 'conv' r) ``sse`` 'id'@
703−antiSymmetric :: (KnownNat (I.Count (I.Normalize a)), I.FromLists Boolean (I.Normalize a) (I.Normalize a)) => Relation a a -> Bool
686+antiSymmetric :: (CountableN a, FLN a a) => Relation a a -> Bool
704−antiSymmetric r = (r `intersection` conv r) `sse` identity
687+antiSymmetric r = (r `intersection` conv r) `sse` id
705
688
706−-- | A 'Relation' @r@ is 'irreflexive' 'iff' @(r `'intersection'` 'identity') == 'zeros'@
689+-- | A 'Relation' @r@ is 'irreflexive' 'iff' @(r ``intersection`` 'id') == 'zeros'@
707−irreflexive :: (KnownNat (I.Count (I.Normalize a)), I.FromLists Boolean (I.Normalize a) (I.Normalize a)) => Relation a a -> Bool
690+irreflexive :: (CountableN a, FLN a a) => Relation a a -> Bool
708−irreflexive r = (r `intersection` identity) == zeros
691+irreflexive r = (r `intersection` id) == zeros
709
692
710−-- | A 'Relation' @r@ is 'connected' 'iff' @(r `'union'` 'conv' r) == 'ones'@
693+-- | A 'Relation' @r@ is 'connected' 'iff' @(r ``union`` 'conv' r) == 'ones'@
711−connected :: (KnownNat (I.Count (I.Normalize a)), I.FromLists Boolean (I.Normalize a) (I.Normalize a)) => Relation a a -> Bool
694+connected :: (CountableN a, FLN a a) => Relation a a -> Bool
712connected r = (r `union` conv r) == ones
695connected r = (r `union` conv r) == ones
713
696
714-- | A 'Relation' @r@ is a 'preorder' 'iff' @'reflexive' r && 'transitive' r@
697-- | A 'Relation' @r@ is a 'preorder' 'iff' @'reflexive' r && 'transitive' r@
715−preorder :: (KnownNat (I.Count (I.Normalize a)), I.FromLists Boolean (I.Normalize a) (I.Normalize a)) => Relation a a -> Bool
698+preorder :: (CountableN a, FLN a a) => Relation a a -> Bool
716preorder r = reflexive r && transitive r
699preorder r = reflexive r && transitive r
717
700
718-- | A 'Relation' @r@ is a partial-order 'iff' @'antiSymmetric' r && 'preorder' r@
701-- | A 'Relation' @r@ is a partial-order 'iff' @'antiSymmetric' r && 'preorder' r@
719−partialOrder :: (KnownNat (I.Count (I.Normalize a)), I.FromLists Boolean (I.Normalize a) (I.Normalize a)) => Relation a a -> Bool
702+partialOrder :: (CountableN a, FLN a a) => Relation a a -> Bool
720partialOrder r = antiSymmetric r && preorder r
703partialOrder r = antiSymmetric r && preorder r
721
704
722-- | A 'Relation' @r@ is a linear-order 'iff' @'connected' r && 'partialOrder' r@
705-- | A 'Relation' @r@ is a linear-order 'iff' @'connected' r && 'partialOrder' r@
723−linearOrder :: (KnownNat (I.Count (I.Normalize a)), I.FromLists Boolean (I.Normalize a) (I.Normalize a)) => Relation a a -> Bool
706+linearOrder :: (CountableN a, FLN a a) => Relation a a -> Bool
724linearOrder r = connected r && partialOrder r
707linearOrder r = connected r && partialOrder r
725
708
726-- | A 'Relation' @r@ is an 'equivalence' 'iff' @'symmetric' r && 'preorder' r@
709-- | A 'Relation' @r@ is an 'equivalence' 'iff' @'symmetric' r && 'preorder' r@
727−equivalence :: (KnownNat (I.Count (I.Normalize a)), I.FromLists Boolean (I.Normalize a) (I.Normalize a)) => Relation a a -> Bool
710+equivalence :: (CountableN a, FLN a a) => Relation a a -> Bool
728equivalence r = symmetric r && preorder r
711equivalence r = symmetric r && preorder r
729
712
730-- | A 'Relation' @r@ is a partial-equivalence 'iff' @'partialOrder' r && 'equivalence' r@
713-- | A 'Relation' @r@ is a partial-equivalence 'iff' @'partialOrder' r && 'equivalence' r@
731−partialEquivalence :: (KnownNat (I.Count (I.Normalize a)), I.FromLists Boolean (I.Normalize a) (I.Normalize a)) => Relation a a -> Bool
714+partialEquivalence :: (CountableN a, FLN a a) => Relation a a -> Bool
732partialEquivalence r = partialOrder r && equivalence r
715partialEquivalence r = partialOrder r && equivalence r
733
716
734-- | A 'Relation' @r@ is 'difunctional' or regular wherever
717-- | A 'Relation' @r@ is 'difunctional' or regular wherever
735−-- @r `comp` 'conv' r `comp` r == r@
718+-- @r `.` 'conv' r `.` r == r@
736difunctional :: Relation a b -> Bool
719difunctional :: Relation a b -> Bool
737−difunctional r = r `comp` conv r `comp` r == r
720+difunctional r = r . conv r . r == r
738
721
739-- Relational pairing
722-- Relational pairing
740
723
@@ -743,64 +726,61 @@ difunctional r = r `comp` conv r `comp` r == r
743-- NOTE: That this is not a true categorical product, see for instance:
726-- NOTE: That this is not a true categorical product, see for instance:
744--
727--
745-- @
728-- @
746−-- | 'p1' `'comp'` 'splitR' a b `'sse'` a
729+-- | 'fstR' `.` 'splitR' a b ``sse`` a
747−-- 'splitR' a b <=> |
730+-- 'splitR' a b <=> |
748−-- | 'p2' `'comp'` 'splitR' a b `'sse'` b
731+-- | 'sndR' `.` 'splitR' a b ``sse`` b
749-- @
732-- @
750--
733--
751-- __Emphasis__ on the 'sse'.
734-- __Emphasis__ on the 'sse'.
752--
735--
753-- @
736-- @
754−-- 'splitR' r s `'comp'` f == 'splitR' (r `'comp'` f) (s `'comp'` f)
737+-- 'splitR' r s `.` f == 'splitR' (r `.` f) (s `.` f)
755−-- (R '><' S) `'comp'` 'splitR' p q == 'splitR' (r `'comp'` p) (s `'comp'` q)
738+-- (R '><' S) `.` 'splitR' p q == 'splitR' (r `.` p) (s `.` q)
756−-- 'conv' ('splitR' r s) `'comp'` 'splitR' x y == ('conv' r `'comp'` x) `'intersection'` ('conv' s `'comp'` y)
739+-- 'conv' ('splitR' r s) `.` 'splitR' x y == ('conv' r `.` x) ``intersection`` ('conv' s `.` y)
757-- @
740-- @
758--
741--
759-- @
742-- @
760-- 'eitherR' ('splitR' r s) ('splitR' t v) == 'splitR' ('eitherR' r t) ('eitherR' s v)
743-- 'eitherR' ('splitR' r s) ('splitR' t v) == 'splitR' ('eitherR' r t) ('eitherR' s v)
761-- @
744-- @
762splitR ::
745splitR ::
763− ( KnownNat (I.Count (I.Normalize a)),
746+ ( CountableDimsN a b,
764− KnownNat (I.Count (I.Normalize b)),
747+ CountableN (a, b),
765− KnownNat (I.Count (I.Normalize (a, b))),
748+ FLN (a, b) a,
766− I.FromLists Boolean (I.Normalize (a, b)) (I.Normalize a),
749+ FLN (a, b) b,
767− I.FromLists Boolean (I.Normalize (a, b)) (I.Normalize b),
750+ TrivialP a b
768− I.Normalize (a, b) ~ I.Normalize (I.Normalize a, I.Normalize b)
769 )
751 )
770 => Relation c a -> Relation c b -> Relation c (a, b)
752 => Relation c a -> Relation c b -> Relation c (a, b)
771−splitR (R f) (R g) = R (I.khatri f g)
753+splitR (R f) (R g) = R (I.kr f g)
772
754
773-- | Relational pairing first component projection
755-- | Relational pairing first component projection
774--
756--
775-- @
757-- @
776−-- 'p1' `'comp'` 'splitR' r s `'sse'` r
758+-- 'fstR' `.` 'splitR' r s ``sse`` r
777-- @
759-- @
778−p1 ::
760+fstR ::
779 forall a b .
761 forall a b .
780− ( KnownNat (I.Count (I.Normalize a)),
762+ ( CountableDimsN a b,
781− KnownNat (I.Count (I.Normalize b)),
763+ CountableN (a, b),
782− KnownNat (I.Count (I.Normalize (a, b))),
764+ FLN (a, b) a,
783− I.FromLists Boolean (I.Normalize (a, b)) (I.Normalize a),
765+ TrivialP a b
784− I.Normalize (a, b) ~ I.Normalize (I.Normalize a, I.Normalize b)
785 )
766 )
786 => Relation (a, b) a
767 => Relation (a, b) a
787−p1 = R (I.kp1 @Boolean @(I.Normalize a) @(I.Normalize b))
768+fstR = R (I.fstM @Boolean @(I.Normalize a) @(I.Normalize b))
788
769
789-- | Relational pairing second component projection
770-- | Relational pairing second component projection
790--
771--
791-- @
772-- @
792−-- 'p2' `'comp'` 'splitR' r s `'sse'` s
773+-- 'sndR' `.` 'splitR' r s ``sse`` s
793-- @
774-- @
794−p2 ::
775+sndR ::
795 forall a b .
776 forall a b .
796− ( KnownNat (I.Count (I.Normalize b)),
777+ ( CountableDimsN a b,
797− KnownNat (I.Count (I.Normalize a)),
778+ CountableN (a, b),
798− KnownNat (I.Count (I.Normalize (a, b))),
779+ FLN (a, b) b,
799− I.FromLists Boolean (I.Normalize (a, b)) (I.Normalize b),
780+ TrivialP a b
800− I.Normalize (a, b) ~ I.Normalize (I.Normalize a, I.Normalize b)
801 )
781 )
802 => Relation (a, b) b
782 => Relation (a, b) b
803−p2 = R (I.kp2 @Boolean @(I.Normalize a) @(I.Normalize b))
783+sndR = R (I.sndM @Boolean @(I.Normalize a) @(I.Normalize b))
804
784
805-- Relational pairing functor
785-- Relational pairing functor
806
786
@@ -808,22 +788,19 @@ infixl 4 ><
808-- | Relational pairing functor
788-- | Relational pairing functor
809--
789--
810-- @
790-- @
811−-- r '><' s == 'splitR' (r `'comp'` p1) (s `'comp'` p2)
791+-- r '><' s == 'splitR' (r `.` fstR) (s `.` sndR)
812−-- (r '><' s) `'comp'` (p '><' q) == (r `'comp'` p) '><' (s `'comp'` q)
792+-- (r '><' s) `.` (p '><' q) == (r `.` p) '><' (s `.` q)
813-- @
793-- @
814(><) ::
794(><) ::
815− ( KnownNat (I.Count (I.Normalize a)),
795+ ( CountableDimsN a b,
816− KnownNat (I.Count (I.Normalize b)),
796+ CountableDimsN c d,
817− KnownNat (I.Count (I.Normalize c)),
797+ CountableDimsN (a, c) (b, d),
818− KnownNat (I.Count (I.Normalize d)),
798+ FLN (a, c) a,
819− KnownNat (I.Count (I.Normalize (a, c))),
799+ FLN (a, c) c,
820− KnownNat (I.Count (I.Normalize (b, d))),
800+ FLN (b, d) b,
821− I.FromLists Boolean (I.Normalize (a, c)) (I.Normalize a),
801+ FLN (b, d) d,
822− I.FromLists Boolean (I.Normalize (a, c)) (I.Normalize c),
802+ TrivialP a c,
823− I.FromLists Boolean (I.Normalize (b, d)) (I.Normalize b),
803+ TrivialP b d
824− I.FromLists Boolean (I.Normalize (b, d)) (I.Normalize d),
825− I.Normalize (a, c) ~ I.Normalize (I.Normalize a, I.Normalize c),
826− I.Normalize (b, d) ~ I.Normalize (I.Normalize b, I.Normalize d)
827 )
804 )
828 => Relation a b -> Relation c d -> Relation (a, c) (b, d)
805 => Relation a b -> Relation c d -> Relation (a, c) (b, d)
829(><) (R a) (R b) = R ((I.><) a b)
806(><) (R a) (R b) = R ((I.><) a b)
@@ -833,35 +810,31 @@ infixl 4 ><
833-- | Relational coproduct.
810-- | Relational coproduct.
834--
811--
835-- @
812-- @
836−-- | 'eitherR' a b `'comp'` 'i1' == a
813+-- | 'eitherR' a b `.` 'i1' == a
837−-- 'eitherR' a b <=> |
814+-- 'eitherR' a b <=> |
838−-- | 'eitherR' a b `'comp'` 'i2' == b
815+-- | 'eitherR' a b `.` 'i2' == b
839-- @
816-- @
840--
817--
841-- @
818-- @
842−-- [R,S]·[T,U]◦= (R·T◦)∪(S·U◦)
843−-- 'eitherR' r s `'comp'` 'conv' ('eitherR' t u) == (r `'comp'` 'conv' t) `'union'` (s `'comp'` 'conv' u)
819+-- 'eitherR' r s `.` 'conv' ('eitherR' t u) == (r `.` 'conv' t) ``union`` (s `.` 'conv' u)
844-- @
820-- @
845--
821--
846-- @
822-- @
847-- 'eitherR' ('splitR' r s) ('splitR' t v) == 'splitR' ('eitherR' r t) ('eitherR' s v)
823-- 'eitherR' ('splitR' r s) ('splitR' t v) == 'splitR' ('eitherR' r t) ('eitherR' s v)
848-- @
824-- @
849−eitherR :: (I.Normalize (Either a b) ~ Either (I.Normalize a) (I.Normalize b))
850− => Relation a c -> Relation b c -> Relation (Either a b) c
825+eitherR :: Relation a c -> Relation b c -> Relation (Either a b) c
851−eitherR = junc
826+eitherR = join
852
827
853-- | Relational coproduct first component injection
828-- | Relational coproduct first component injection
854--
829--
855-- @
830-- @
856−-- 'img' 'i1' `union` 'img' 'i2' == 'identity'
831+-- 'img' 'i1' ``union`` 'img' 'i2' == 'id'
857−-- 'i1' `'comp'` 'i2' = 'zeros'
832+-- 'i1' `.` 'i2' = 'zeros'
858-- @
833-- @
859i1 ::
834i1 ::
860− ( KnownNat (I.Count (I.Normalize b)),
835+ ( CountableDimsN a b,
861− KnownNat (I.Count (I.Normalize a)),
836+ FLN b a,
862− I.FromLists Boolean (I.Normalize b) (I.Normalize a),
837+ FLN a a
863− I.FromLists Boolean (I.Normalize a) (I.Normalize a),
864− I.Normalize (Either a b) ~ Either (I.Normalize a) (I.Normalize b)
865 )
838 )
866 => Relation a (Either a b)
839 => Relation a (Either a b)
867i1 = R I.i1
840i1 = R I.i1
@@ -869,15 +842,13 @@ i1 = R I.i1
869-- | Relational coproduct second component injection
842-- | Relational coproduct second component injection
870--
843--
871-- @
844-- @
872−-- 'img' 'i1' `union` 'img' 'i2' == 'identity'
845+-- 'img' 'i1' ``union`` 'img' 'i2' == 'id'
873−-- 'i1' `'comp'` 'i2' = 'zeros'
846+-- 'i1' `.` 'i2' = 'zeros'
874-- @
847-- @
875i2 ::
848i2 ::
876− ( KnownNat (I.Count (I.Normalize b)),
849+ ( CountableDimsN a b,
877− KnownNat (I.Count (I.Normalize a)),
850+ FLN a b,
878− I.FromLists Boolean (I.Normalize a) (I.Normalize b),
851+ FLN b b
879− I.FromLists Boolean (I.Normalize b) (I.Normalize b),
880− I.Normalize (Either a b) ~ Either (I.Normalize a) (I.Normalize b)
881 )
852 )
882 => Relation b (Either a b)
853 => Relation b (Either a b)
883i2 = R I.i2
854i2 = R I.i2
@@ -887,17 +858,14 @@ infixl 5 -|-
887-- | Relational coproduct functor.
858-- | Relational coproduct functor.
888--
859--
889-- @
860-- @
890−-- r '-|-' s == 'eitherR' ('i1' `'comp'` r) ('i2' `'comp'` s)
861+-- r '-|-' s == 'eitherR' ('i1' `.` r) ('i2' `.` s)
891-- @
862-- @
892(-|-) ::
863(-|-) ::
893− ( KnownNat (I.Count (I.Normalize d)),
864+ ( CountableDimsN b d,
894− KnownNat (I.Count (I.Normalize b)),
865+ FLN b b,
895− I.FromLists Boolean (I.Normalize b) (I.Normalize b),
866+ FLN d b,
896− I.FromLists Boolean (I.Normalize d) (I.Normalize b),
867+ FLN b d,
897− I.FromLists Boolean (I.Normalize b) (I.Normalize d),
868+ FLN d d
898− I.FromLists Boolean (I.Normalize d) (I.Normalize d),
899− I.Normalize (Either a c) ~ Either (I.Normalize a) (I.Normalize c),
900− I.Normalize (Either b d) ~ Either (I.Normalize b) (I.Normalize d)
901 )
869 )
902 => Relation a b -> Relation c d -> Relation (Either a c) (Either b d)
870 => Relation a b -> Relation c d -> Relation (Either a c) (Either b d)
903(-|-) (R a) (R b) = R ((I.-|-) a b)
871(-|-) (R a) (R b) = R ((I.-|-) a b)
@@ -910,22 +878,20 @@ infixl 5 -|-
910-- 'trans'/'untrans';
878-- 'trans'/'untrans';
911-- more-over, where each particular attribute is placed (input/output) is irrelevant.
879-- more-over, where each particular attribute is placed (input/output) is irrelevant.
912trans ::
880trans ::
913− ( KnownNat (I.Count (I.Normalize (a, b))),
881+ ( CountableDimsN a b,
914− KnownNat (I.Count (I.Normalize a)),
882+ CountableN c,
915− KnownNat (I.Count (I.Normalize (c, b))),
883+ CountableDimsN (a, b) (c, b),
916− KnownNat (I.Count (I.Normalize b)),
884+ FLN (c, b) c,
917− KnownNat (I.Count (I.Normalize c)),
885+ FLN (c, b) b,
918− I.FromLists Boolean (I.Normalize (c, b)) (I.FromNat (I.Count c)),
886+ FLN (a, b) a,
919− I.FromLists Boolean (I.Normalize (c, b)) (I.FromNat (I.Count b)),
887+ FLN (a, b) b,
920− I.FromLists Boolean (I.Normalize (a, b)) (I.FromNat (I.Count b)),
888+ Trivial (a, b),
921− I.FromLists Boolean (I.Normalize (a, b)) (I.FromNat (I.Count a)),
889+ Trivial (c, b),
922− I.Normalize (a, b) ~ I.Normalize (I.Normalize (a, b)),
890+ TrivialP a b,
923− I.Normalize (c, b) ~ I.Normalize (I.Normalize (c, b)),
891+ TrivialP c b
924− I.Normalize (I.Normalize a, I.Normalize b) ~ I.FromNat (I.Count (I.Normalize (a, b))),
925− I.Normalize (I.Normalize c, I.Normalize b) ~ I.FromNat (I.Count (I.Normalize (c, b)))
926 )
892 )
927 => Relation (a, b) c -> Relation a (c, b)
893 => Relation (a, b) c -> Relation a (c, b)
928−trans r = splitR r p2 `comp` conv p1
894+trans r = splitR r sndR . conv fstR
929
895
930-- | Relational 'untrans'
896-- | Relational 'untrans'
931--
897--
@@ -933,111 +899,110 @@ trans r = splitR r p2 `comp` conv p1
933-- 'trans'/'untrans';
899-- 'trans'/'untrans';
934-- more-over, where each particular attribute is placed (input/output) is irrelevant.
900-- more-over, where each particular attribute is placed (input/output) is irrelevant.
935untrans ::
901untrans ::
936− ( KnownNat (I.Count (I.Normalize (a, b))),
902+ ( CountableDimsN a b,
937− KnownNat (I.Count (I.Normalize a)),
903+ CountableN c,
938− KnownNat (I.Count (I.Normalize (c, b))),
904+ CountableDimsN (a, b) (c, b),
939− KnownNat (I.Count (I.Normalize b)),
905+ FLN (c, b) c,
940− KnownNat (I.Count (I.Normalize c)),
906+ FLN (c, b) b,
941− I.FromLists Boolean (I.Normalize (c, b)) (I.FromNat (I.Count c)),
907+ FLN (a, b) b,
942− I.FromLists Boolean (I.Normalize (c, b)) (I.FromNat (I.Count b)),
908+ FLN (a, b) a,
943− I.FromLists Boolean (I.Normalize (a, b)) (I.FromNat (I.Count b)),
909+ Trivial (a, b),
944− I.FromLists Boolean (I.Normalize (a, b)) (I.FromNat (I.Count a)),
910+ Trivial (c, b),
945− I.Normalize (a, b) ~ I.Normalize (I.Normalize (a, b)),
911+ TrivialP a b,
946− I.Normalize (c, b) ~ I.Normalize (I.Normalize (c, b)),
912+ TrivialP c b
947− I.Normalize (I.Normalize a, I.Normalize b) ~ I.FromNat (I.Count (I.Normalize (a, b))),
948− I.Normalize (I.Normalize c, I.Normalize b) ~ I.FromNat (I.Count (I.Normalize (c, b)))
949 )
913 )
950 => Relation a (c, b) -> Relation (a, b) c
914 => Relation a (c, b) -> Relation (a, b) c
951−untrans s = p1 `comp` conv (splitR (conv s) p2)
915+untrans s = fstR . conv (splitR (conv s) sndR)
952
916
953-- | Transforms predicate @p@ into a correflexive relation.
917-- | Transforms predicate @p@ into a correflexive relation.
954--
918--
955-- @
919-- @
956−-- 'predR' ('const' True) == 'identity'
920+-- 'predR' ('const' True) == 'id'
957-- 'predR' ('const' False) == 'zeros'
921-- 'predR' ('const' False) == 'zeros'
958-- @
922-- @
959--
923--
960-- @
924-- @
961−-- 'predR' q `'comp'` 'predR' p == 'predR' q `'union'` 'predR' p
925+-- 'predR' q `.` 'predR' p == 'predR' q ``union`` 'predR' p
962-- @
926-- @
963predR ::
927predR ::
964 ( Bounded a,
928 ( Bounded a,
965 Enum a,
929 Enum a,
966− KnownNat (I.Count (I.Normalize a)),
930+ Countable a,
967− I.FromLists Boolean (I.Normalize a) (I.Normalize a),
931+ CountableN a,
968− I.FromLists Boolean (I.Normalize Bool) (I.Normalize a)
932+ FLN a a,
933+ FLN Bool a
969 )
934 )
970− => (a -> Bool) -> Relation a a
935+ => Relation a Bool -> Relation a a
971−predR p = identity `intersection` divisionF (fromF' (const True)) (fromF' p)
936+predR p = id `intersection` divisionF (fromF (const True)) p
972
937
973-- | Equalizes functions @f@ and @g@.
938-- | Equalizes functions @f@ and @g@.
974-- That is, @'equalizer' f g@ is the largest coreflexive
939-- That is, @'equalizer' f g@ is the largest coreflexive
975-- that restricts @g@ so that @f@ and @g@ yield the same outputs.
940-- that restricts @g@ so that @f@ and @g@ yield the same outputs.
976--
941--
977-- @
942-- @
978−-- 'equalizer' r r == 'identity'
943+-- 'equalizer' r r == 'id'
979-- 'equalizer' ('point' True) ('point' False) == 'zeros'
944-- 'equalizer' ('point' True) ('point' False) == 'zeros'
980-- @
945-- @
981equalizer ::
946equalizer ::
982− ( KnownNat (I.Count (I.Normalize a)),
947+ ( CountableN a,
983− I.FromLists Boolean (I.Normalize a) (I.Normalize a)
948+ FLN a a
984 )
949 )
985 => Relation a b -> Relation a b -> Relation a a
950 => Relation a b -> Relation a b -> Relation a a
986−equalizer f g = identity `intersection` divisionF f g
951+equalizer f g = id `intersection` divisionF f g
987
952
988-- | Relational conditional guard.
953-- | Relational conditional guard.
989--
954--
990-- @
955-- @
991−-- 'guard' p = 'i2' `'overriddenBy'` 'i1' `'comp'` 'predR' p
956+-- 'guard' p = 'i2' ``overriddenBy`` 'i1' `.` 'predR' p
992-- @
957-- @
993−guard ::
958+guard ::
994 ( Bounded b,
959 ( Bounded b,
995 Enum b,
960 Enum b,
996− KnownNat (I.Count (I.Normalize b)),
961+ CountableN b,
997− I.FromLists Boolean (I.Normalize b) (I.Normalize b),
962+ Countable b,
998− I.FromLists Boolean (I.Normalize Bool) (I.Normalize b),
963+ FLN b b,
999− I.Normalize (Either b b) ~ Either (I.Normalize b) (I.Normalize b)
964+ FLN Bool b
1000− ) => (b -> Bool) -> Relation b (Either b b)
965+ ) => Relation b Bool -> Relation b (Either b b)
1001−guard p = conv (eitherR (predR p) (predR (not . p)))
966+guard p = conv (eitherR (predR p) (predR (negate p)))
1002
967
1003-- | Relational McCarthy's conditional.
968-- | Relational McCarthy's conditional.
1004−cond ::
969+cond ::
1005 ( Bounded b,
970 ( Bounded b,
1006 Enum b,
971 Enum b,
1007− KnownNat (I.Count (I.Normalize b)),
972+ Countable b,
1008− I.FromLists Boolean (I.Normalize b) (I.Normalize b),
973+ CountableN b,
1009− I.FromLists Boolean (I.Normalize Bool) (I.Normalize b),
974+ FLN b b,
1010− I.Normalize (Either b b) ~ Either (I.Normalize b) (I.Normalize b)
975+ FLN Bool b
1011− )
976+ )
1012− => (b -> Bool) -> Relation b c -> Relation b c -> Relation b c
977+ => Relation b Bool -> Relation b c -> Relation b c -> Relation b c
1013−cond p r s = eitherR r s `comp` guard p
978+cond p r s = eitherR r s . guard p
1014
979
1015-- | Relational domain.
980-- | Relational domain.
1016--
981--
1017-- For injective relations, 'domain' and 'ker'nel coincide,
982-- For injective relations, 'domain' and 'ker'nel coincide,
1018−-- since @'ker' r `'sse'` 'identity'@ in such situations.
983+-- since @'ker' r ``sse`` 'id'@ in such situations.
1019domain ::
984domain ::
1020− ( KnownNat (I.Count (I.Normalize a)),
985+ ( CountableN a,
1021− I.FromLists Boolean (I.Normalize a) (I.Normalize a)
986+ FLN a a
1022 ) => Relation a b -> Relation a a
987 ) => Relation a b -> Relation a a
1023−domain r = ker r `intersection` identity
988+domain r = ker r `intersection` id
1024
989
1025-- | Relational range.
990-- | Relational range.
1026--
991--
1027-- For functions, 'range' and 'img' (image) coincide,
992-- For functions, 'range' and 'img' (image) coincide,
1028−-- since@'img' f `'sse'` 'identity'@ for any @f@.
993+-- since @'img' f ``sse`` id@ for any @f@.
1029range ::
994range ::
1030− ( I.FromLists Boolean (I.Normalize b) (I.Normalize b),
995+ ( CountableN b,
1031− KnownNat (I.Count (I.Normalize b))
996+ FLN b b
1032 ) => Relation a b -> Relation b b
997 ) => Relation a b -> Relation b b
1033−range r = img r `intersection` identity
998+range r = img r `intersection` id
1034
999
1035-- Relation pretty print
1000-- Relation pretty print
1036
1001
1037-- | Relation pretty printing
1002-- | Relation pretty printing
1038−pretty :: (KnownNat (I.Count (I.Normalize a))) => Relation a b -> String
1003+pretty :: (CountableDimsN a b) => Relation a b -> String
1039pretty (R a) = I.pretty a
1004pretty (R a) = I.pretty a
1040
1005
1041-- | Relation pretty printing
1006-- | Relation pretty printing
1042−prettyPrint :: (KnownNat (I.Count (I.Normalize a))) => Relation a b -> IO ()
1007+prettyPrint :: (CountableDimsN a b) => Relation a b -> IO ()
1043prettyPrint (R a) = I.prettyPrint a
1008prettyPrint (R a) = I.prettyPrint a
src/LAoP/Utils.hs+5−2
@@ -95,8 +95,11 @@ module LAoP.Utils
95 coerceNat2,
95 coerceNat2,
96 coerceNat3,
96 coerceNat3,
97
97
98− -- * Powerset data type
98+ -- * List data type
99− Powerset (..)
99+ List (..),
100+
101+ -- * Category type-class
102+ Category(..)
100 )
103 )
101where
104where
102
105
src/LAoP/Utils/Internal.hs+41−83
@@ -1,82 +1,13 @@
1+{-# LANGUAGE TypeFamilies #-}
2+{-# LANGUAGE DeriveGeneric #-}
1{-# LANGUAGE TypeApplications #-}
3{-# LANGUAGE TypeApplications #-}
2{-# LANGUAGE DataKinds #-}
4{-# LANGUAGE DataKinds #-}
3{-# LANGUAGE FlexibleInstances #-}
5{-# LANGUAGE FlexibleInstances #-}
4{-# LANGUAGE GeneralizedNewtypeDeriving #-}
6{-# LANGUAGE GeneralizedNewtypeDeriving #-}
5−{-# LANGUAGE KindSignatures #-}
6{-# LANGUAGE ScopedTypeVariables #-}
7{-# LANGUAGE ScopedTypeVariables #-}
7
8
8module LAoP.Utils.Internal
9module LAoP.Utils.Internal
9− ( -- | This is an internal module and it is not meant to be imported.
10+ (
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− --
80 -- * 'Natural' data type
11 -- * 'Natural' data type
81 Natural(..),
12 Natural(..),
82 nat,
13 nat,
@@ -87,8 +18,11 @@ module LAoP.Utils.Internal
87 coerceNat2,
18 coerceNat2,
88 coerceNat3,
19 coerceNat3,
89
20
90− -- * Powerset data type
21+ -- * 'List' data type
91− Powerset (..)
22+ List (..),
23+
24+ -- * Category type class
25+ Category(..)
92 )
26 )
93where
27where
94
28
@@ -98,12 +32,16 @@ import Data.List
98import Data.Maybe
32import Data.Maybe
99import GHC.TypeLits
33import GHC.TypeLits
100import Control.DeepSeq
34import Control.DeepSeq
35+import GHC.Generics
36+import Data.Kind
37+import Prelude hiding (id, (.))
38+import qualified Prelude
101
39
102-- | Wrapper around 'Int's that have a restrictive semantic associated.
40-- | Wrapper around 'Int's that have a restrictive semantic associated.
103-- A value of type @'Natural' n m@ can only be instanciated with some 'Int'
41-- A value of type @'Natural' n m@ can only be instanciated with some 'Int'
104-- @i@ that's @n <= i <= m@.
42-- @i@ that's @n <= i <= m@.
105newtype Natural (start :: Nat) (end :: Nat) = Nat Int
43newtype Natural (start :: Nat) (end :: Nat) = Nat Int
106− deriving (Show, Read, Eq, Ord, NFData)
44+ deriving (Show, Read, Eq, Ord, NFData, Generic)
107
45
108-- | Throws a runtime error if any of the operations overflows or
46-- | Throws a runtime error if any of the operations overflows or
109-- underflows.
47-- underflows.
@@ -207,7 +145,7 @@ instance
207--
145--
208-- This data type is a newtype wrapper around '[]'. This exists in order to
146-- This data type is a newtype wrapper around '[]'. This exists in order to
209-- implement an 'Enum' and 'Bounded' instance that cannot be harmful for the outside.
147-- implement an 'Enum' and 'Bounded' instance that cannot be harmful for the outside.
210−newtype Powerset a = PS [a]
148+newtype List a = L [a]
211 deriving (Eq, Show, Read)
149 deriving (Eq, Show, Read)
212
150
213powerset :: [a] -> [[a]]
151powerset :: [a] -> [[a]]
@@ -217,22 +155,42 @@ powerset (x:xs) = powerset xs ++ [x:ps | ps <- powerset xs]
217instance
155instance
218 ( Enum a,
156 ( Enum a,
219 Bounded a
157 Bounded a
220− ) => Bounded (Powerset a)
158+ ) => Bounded (List a)
221 where
159 where
222− minBound = PS []
160+ minBound = L []
223− maxBound = PS [minBound .. maxBound]
161+ maxBound = L [minBound .. maxBound]
224
162
225instance
163instance
226 ( Bounded a,
164 ( Bounded a,
227 Enum a,
165 Enum a,
228 Eq a
166 Eq a
229− ) => Enum (Powerset a)
167+ ) => Enum (List a)
230 where
168 where
231 toEnum i =
169 toEnum i =
232 let as = [minBound .. maxBound]
170 let as = [minBound .. maxBound]
233− in PS (powerset as !! i)
171+ in L (powerset as !! i)
234
172
235− fromEnum (PS []) = 0
173+ fromEnum (L []) = 0
236− fromEnum (PS x) =
174+ fromEnum (L x) =
237 let as = [minBound .. maxBound]
175 let as = [minBound .. maxBound]
238 in fromMaybe (error "Does not exist") $ elemIndex x (powerset as)
176 in fromMaybe (error "Does not exist") $ elemIndex x (powerset as)
177+
178+-- | Constrained category instance
179+class Category k where
180+ type Object k o :: Constraint
181+ type Object k o = ()
182+ id :: Object k a => k a a
183+ (.) :: k b c -> k a b -> k a c
184+
185+{-# RULES
186+"identity/left" forall p .
187+ id . p = p
188+"identity/right" forall p .
189+ p . id = p
190+"association" forall p q r .
191+ (p . q) . r = p . (q . r)
192+ #-}
193+
194+instance Category (->) where
195+ id = Prelude.id
196+ (.) = (Prelude..)
stack-8.8.3.yamlnew file+1
@@ -0,0 +1 @@
1+resolver: lts-15.5
stack.yaml+1−66
@@ -1,66 +1 @@
1−# This file was automatically generated by 'stack init'
2−#
3−# Some commonly used options have been documented as comments in this file.
4−# For advanced use and comprehensive documentation of the format, please see:
5−# https://docs.haskellstack.org/en/stable/yaml_configuration/
6−
7−# Resolver to choose a 'specific' stackage snapshot or a compiler version.
8−# A snapshot resolver dictates the compiler version and the set of packages
9−# to be used for project dependencies. For example:
10−#
11−# resolver: lts-3.5
12−# resolver: nightly-2015-09-21
13−# resolver: ghc-7.10.2
14−#
15−# The location of a snapshot can be provided as a file or url. Stack assumes
16−# a snapshot provided as a file might change, whereas a url resource does not.
17−#
18−# resolver: ./custom-snapshot.yaml
19−# resolver: https://example.com/snapshots/2018-01-01.yaml
20−resolver: lts-14.18
1+resolver: lts-14.3
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 @@
6packages: []
6packages: []
7snapshots:
7snapshots:
8- completed:
8- completed:
9− size: 524789
9+ size: 523878
10− url: https://raw.githubusercontent.com/commercialhaskell/stackage-snapshots/master/lts/14/18.yaml
10+ url: https://raw.githubusercontent.com/commercialhaskell/stackage-snapshots/master/lts/14/3.yaml
11− sha256: 646be71223e08234131c6989912e6011e01b9767bc447b6d466a35e14360bdf2
11+ sha256: 470c46c27746a48c7c50f829efc0cf00112787a7804ee4ac7a27754658f6d92c
12− original: lts-14.18
12+ original: lts-14.3
test/Examples/Quantum.hsnew file+31
@@ -0,0 +1,31 @@
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)
app/Main.hs → test/Examples/Readme.hsrenamed+61−33
@@ -1,10 +1,13 @@
1+{-# LANGUAGE GADTs #-}
1{-# LANGUAGE DeriveGeneric #-}
2{-# LANGUAGE DeriveGeneric #-}
2{-# LANGUAGE FlexibleContexts #-}
3{-# LANGUAGE FlexibleContexts #-}
3−{-# LANGUAGE TypeOperators #-}
4{-# LANGUAGE TypeApplications #-}
4{-# LANGUAGE TypeApplications #-}
5{-# LANGUAGE DataKinds #-}
5{-# LANGUAGE DataKinds #-}
6
6
7+module Examples.Readme
8+ ( exec
9+ )
7−module Main where
10+ where
8
11
9import LAoP.Matrix.Type
12import LAoP.Matrix.Type
10import qualified LAoP.Relation as R
13import qualified LAoP.Relation as R
@@ -12,13 +15,12 @@ import LAoP.Utils
12import LAoP.Dist
15import LAoP.Dist
13import GHC.TypeLits
16import GHC.TypeLits
14import Data.Coerce
17import Data.Coerce
15−import GHC.Generics
18+import qualified GHC.Generics as G
16−import Control.Category hiding (id)
19+import Prelude hiding (id, (.))
17−import Prelude hiding ((.))
18
20
19-- Monty Hall Problem
21-- Monty Hall Problem
20data Outcome = Win | Lose
22data Outcome = Win | Lose
21− deriving (Bounded, Enum, Eq, Show, Generic)
23+ deriving (Bounded, Enum, Eq, Show, G.Generic)
22
24
23switch :: Outcome -> Outcome
25switch :: Outcome -> Outcome
24switch Win = Lose
26switch Win = Lose
@@ -28,7 +30,7 @@ firstChoice :: Matrix Double () Outcome
28firstChoice = col [1/3, 2/3]
30firstChoice = col [1/3, 2/3]
29
31
30secondChoice :: Matrix Double Outcome Outcome
32secondChoice :: Matrix Double Outcome Outcome
31−secondChoice = fromF' switch
33+secondChoice = fromF switch
32
34
33-- Dice sum
35-- Dice sum
34
36
@@ -37,7 +39,7 @@ type SS = Natural 1 6 -- Sample Space
37sumSS :: SS -> SS -> Natural 2 12
39sumSS :: SS -> SS -> Natural 2 12
38sumSS = coerceNat (+)
40sumSS = coerceNat (+)
39
41
40−sumSSM = fromF' (uncurry sumSS)
42+sumSSM = fromF (uncurry sumSS)
41
43
42condition :: (Int, Int) -> Int -> Int
44condition :: (Int, Int) -> Int -> Int
43condition (fst, snd) thrd = if fst == snd
45condition (fst, snd) thrd = if fst == snd
@@ -47,38 +49,64 @@ condition (fst, snd) thrd = if fst == snd
47conditionSS :: (SS, SS) -> SS -> Natural 3 18
49conditionSS :: (SS, SS) -> SS -> Natural 3 18
48conditionSS = coerceNat2 condition
50conditionSS = coerceNat2 condition
49
51
50−conditionalThrows = fromF' (uncurry conditionSS) . khatri (khatri die die) die
52+conditionalThrows = fromF (uncurry conditionSS) . kr (kr die die) die
51
53
52die :: Matrix Double () SS
54die :: Matrix Double () SS
53die = col $ map (const (1/6)) [nat @1 @6 1 .. nat 6]
55die = col $ map (const (1/6)) [nat @1 @6 1 .. nat 6]
54
56
55-- Sprinkler
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)
56
63
64+data R = No | Yes
65+ deriving (Bounded, Enum, Eq, Show, G.Generic)
66+
57−rain :: Matrix Double () Bool
67+rain :: Matrix Double () R
58−rain = col [0.8, 0.2]
68+rain = matrixBuilder gen
69+ where
70+ gen (_, No) = 0.8
71+ gen (_, Yes) = 0.2
59
72
60−sprinkler :: Matrix Double Bool Bool
73+sprinkler :: Matrix Double R S
61−sprinkler = fromLists [[0.6, 0.99], [0.4, 0.01]]
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
62
92
63−grass :: Matrix Double (Bool, Bool) Bool
93+tag f = kr f id
64−grass = fromLists [[1, 0.2, 0.1, 0.01], [0, 0.8, 0.9, 0.99]]
65
94
66−state :: Matrix Double () (Bool, (Bool, Bool))
95+state g s r = tag g . tag s . r
67−state = khatri grass identity . khatri sprinkler identity . rain
68
96
69−grass_wet :: Matrix Double (Bool, (Bool, Bool)) One
97+grass_wet :: Matrix Double () (G, (S, R)) -> Matrix Double One One
70−grass_wet = row [0,1] . kp1
98+grass_wet state = row [0,1] . fstM . state
71
99
72−rainning :: Matrix Double (Bool, (Bool, Bool)) One
100+rainning :: Matrix Double (G, (S, R)) One
73−rainning = row [0,1] . kp2 . kp2
101+rainning = row [0,1] . sndM . sndM
74
102
75-- Alcuin Puzzle
103-- Alcuin Puzzle
76
104
77data Being = Farmer | Fox | Goose | Beans
105data Being = Farmer | Fox | Goose | Beans
78− deriving (Bounded, Enum, Eq, Show, Generic)
106+ deriving (Bounded, Enum, Eq, Show, G.Generic)
79
107
80data Bank = LeftB | RightB
108data Bank = LeftB | RightB
81− deriving (Bounded, Enum, Eq, Show, Generic)
109+ deriving (Bounded, Enum, Eq, Show, G.Generic)
82
110
83eats :: Being -> Being -> Bool
111eats :: Being -> Being -> Bool
84eats Fox Goose = True
112eats Fox Goose = True
@@ -93,21 +121,21 @@ cross LeftB = RightB
93cross RightB = LeftB
121cross RightB = LeftB
94
122
95crossR :: R.Relation Bank Bank
123crossR :: R.Relation Bank Bank
96−crossR = R.fromF' cross
124+crossR = R.fromF cross
97
125
98-- | Initial state, everyone in the left bank
126-- | Initial state, everyone in the left bank
99locationLeft :: Being -> Bank
127locationLeft :: Being -> Bank
100locationLeft _ = LeftB
128locationLeft _ = LeftB
101
129
102locationLeftR :: R.Relation Being Bank
130locationLeftR :: R.Relation Being Bank
103−locationLeftR = R.fromF' locationLeft
131+locationLeftR = R.fromF locationLeft
104
132
105-- | Initial state, everyone in the right bank
133-- | Initial state, everyone in the right bank
106locationRight :: Being -> Bank
134locationRight :: Being -> Bank
107locationRight _ = RightB
135locationRight _ = RightB
108
136
109locationRightR :: R.Relation Being Bank
137locationRightR :: R.Relation Being Bank
110−locationRightR = R.fromF' locationRight
138+locationRightR = R.fromF locationRight
111
139
112-- Properties
140-- Properties
113
141
@@ -124,7 +152,7 @@ inv :: R.Relation Being Bank -> Bool
124inv w = (w `R.comp` canEat w) `R.sse` (w `R.comp` farmer)
152inv w = (w `R.comp` canEat w) `R.sse` (w `R.comp` farmer)
125 where
153 where
126 farmer :: R.Relation Being Being
154 farmer :: R.Relation Being Being
127− farmer = R.fromF' (const Farmer)
155+ farmer = R.fromF (const Farmer)
128
156
129-- Arbitrary state
157-- Arbitrary state
130bankState :: Being -> Bank -> Bool
158bankState :: Being -> Bank -> Bool
@@ -138,19 +166,19 @@ bankStateR :: R.Relation Being Bank
138bankStateR = R.toRel bankState
166bankStateR = R.toRel bankState
139
167
140-- Main
168-- Main
141−main :: IO ()
169+exec :: IO ()
142−main = do
170+exec = do
143 putStrLn "Monty Hall Problem solution:"
171 putStrLn "Monty Hall Problem solution:"
144 prettyPrint (secondChoice . firstChoice)
172 prettyPrint (secondChoice . firstChoice)
145 putStrLn "\n Sum of dices probability:"
173 putStrLn "\n Sum of dices probability:"
146− prettyPrint (sumSSM `comp` khatri die die)
174+ prettyPrint (sumSSM . kr die die)
147 putStrLn "\n Conditional dice throw:"
175 putStrLn "\n Conditional dice throw:"
148 prettyPrint conditionalThrows
176 prettyPrint conditionalThrows
149 putStrLn "\n Checking that the last result is indeed a distribution: "
177 putStrLn "\n Checking that the last result is indeed a distribution: "
150− prettyPrint (bang . sumSSM . khatri die die)
178+ prettyPrint (bang . sumSSM . kr die die)
151 putStrLn "\n Probability of grass being wet:"
179 putStrLn "\n Probability of grass being wet:"
152− prettyPrint (grass_wet . state)
180+ prettyPrint (grass_wet (state grass sprinkler rain))
153 putStrLn "\n Probability of rain:"
181 putStrLn "\n Probability of rain:"
154− prettyPrint (rainning . state)
182+ prettyPrint (rainning . state grass sprinkler rain)
155 putStrLn "\n Is the arbitrary state a valid state? (Alcuin Puzzle)"
183 putStrLn "\n Is the arbitrary state a valid state? (Alcuin Puzzle)"
156 print (inv bankStateR)
184 print (inv bankStateR)
test/Examples/Spreadsheets.hsnew file+47
@@ -0,0 +1,47 @@
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+7−1
@@ -1,2 +1,8 @@
1+module Main (main) where
2+
3+import qualified Examples.Readme as RD
4+
1main :: IO ()
5main :: IO ()
2−main = putStrLn "Test suite not yet implemented"
6+main = do
7+ putStrLn ("Testing if README works" :: String)
8+ RD.exec