git.iko.soy/laop
on 59f3ebc help sign in
eea6231
swap
0 ahead, 70 behind
.github/workflows/ci.ymldeleted−43
since splitsnapshots
unifiedsplit
@@ -1,43 +0,0 @@
1−name: CI
2−
3−# Trigger the workflow on push or pull request, but only for the master branch
4−on:
5− pull_request:
6− push:
7− branches: [master]
8−
9−jobs:
10− build:
11− name: ghc ${{ matrix.ghc }}
12− runs-on: ubuntu-16.04
13− strategy:
14− matrix:
15− cabal: ["3.0"]
16− ghc:
17− - "8.6.5"
18− - "8.8.3"
19−
20− steps:
21− - uses: actions/checkout@v2
22− if: github.event.action == 'opened' || github.event.action == 'synchronize' || github.event.ref == 'refs/heads/master'
23−
24− - uses: actions/setup-haskell@v1
25− name: Setup Haskell
26− with:
27− ghc-version: ${{ matrix.ghc }}
28− cabal-version: ${{ matrix.cabal }}
29−
30− - uses: actions/cache@v1
31− name: Cache ~/.cabal/store
32− with:
33− path: ~/.cabal/store
34− key: ${{ runner.os }}-${{ matrix.ghc }}-cabal
35−
36− - name: Build
37− run: |
38− cabal v2-update
39− cabal v2-build --enable-tests --enable-benchmarks
40−
41− - name: Test
42− run: |
43− cabal v2-test --enable-tests
.gitignore+2−54
@@ -1,55 +1,3 @@
1−### Haskell
2−dist
3−dist-*
4−cabal-dev
5−*.o
6−*.hi
7−*.chi
8−*.chs.h
9−*.dyn_o
10−*.dyn_hi
11−*.prof
12−*.aux
13−*.hp
14−*.eventlog
15−.virtualenv
16−.hsenv
17−.hpc
18−.cabal-sandbox/
19−cabal.sandbox.config
20−cabal.config
21−cabal.project.local
22−.ghc.environment.*
23−.HTF/
24−# Stack
25.stack-work/
1.stack-work/
26−stack.yaml.lock
2+laop.cabal
27−
28−### IDE/support
29−# Vim
30−[._]*.s[a-v][a-z]
31−[._]*.sw[a-p]
32−[._]s[a-v][a-z]
33−[._]sw[a-p]
34−*~
3+*~
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.ymldeleted−47
@@ -1,47 +0,0 @@
1−sudo: true
2−language: haskell
3−
4−git:
5− depth: 5
6−
7−cabal: "3.0"
8−
9−cache:
10− directories:
11− - "$HOME/.cabal/store"
12− - "$HOME/.stack"
13− - "$TRAVIS_BUILD_DIR/.stack-work"
14−
15−matrix:
16− include:
17− - ghc: 8.6.5
18− - ghc: 8.8.3
19−
20− - ghc: 8.8.3
21− env: STACK_YAML="$TRAVIS_BUILD_DIR/stack-8.8.3.yaml"
22−
23− - ghc: 8.6.5
24− env: STACK_YAML="$TRAVIS_BUILD_DIR/stack.yaml"
25−
26−
27−install:
28− - |
29− if [ -z "$STACK_YAML" ]; then
30− cabal v2-update
31− cabal v2-build --enable-tests --enable-benchmarks
32− else
33− curl -sSL https://get.haskellstack.org/ | sh
34− stack --version
35− stack build --system-ghc --test --bench --no-run-tests --no-run-benchmarks
36− fi
37−
38−script:
39− - |
40− if [ -z "$STACK_YAML" ]; then
41− cabal v2-test --enable-tests
42− else
43− stack test --system-ghc
44− fi
45−
46−notifications:
47− email: false
CHANGELOG.mddeleted−17
@@ -1,17 +0,0 @@
1−# Changelog
2−
3−`laop` uses [PVP Versioning][1].
4−The changelog is available [on GitHub][2].
5−
6−## 0.1.1.1
7−
8−* Bump base version to work with cabal
9−
10−## 0.1.1.0
11−
12−* Package is more organized and now has tests and benchmarks separated
13−* Repository is more organized and clean
14−* Added CI
15−
16−[1]: https://pvp.haskell.org
17−[2]: https://github.com/bolt12/laop2/releases
ChangeLog.mdnew file+3
@@ -0,0 +1,3 @@
1+# Changelog for laop
2+
3+## Unreleased changes
LICENSE+26−17
@@ -1,21 +1,30 @@
1−MIT License
1+Copyright Armando Santos (c) 2019
2
2
3−Copyright (c) 2020 Armando Santos
3+All rights reserved.
4
4
5−Permission is hereby granted, free of charge, to any person obtaining a copy
5+Redistribution and use in source and binary forms, with or without
6−of this software and associated documentation files (the "Software"), to deal
7−in the Software without restriction, including without limitation the rights
8−to use, copy, modify, merge, publish, distribute, sublicense, and/or sell
9−copies of the Software, and to permit persons to whom the Software is
10−furnished to do so, subject to the following conditions:
6+modification, are permitted provided that the following conditions are met:
11
7
12−The above copyright notice and this permission notice shall be included in all
8+ * Redistributions of source code must retain the above copyright
13−copies or substantial portions of the Software.
9+ notice, this list of conditions and the following disclaimer.
14
10
15−THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR
11+ * Redistributions in binary form must reproduce the above
12+ copyright notice, this list of conditions and the following
13+ disclaimer in the documentation and/or other materials provided
14+ with the distribution.
15+
16+ * Neither the name of Armando Santos nor the names of other
17+ contributors may be used to endorse or promote products derived
18+ from this software without specific prior written permission.
19+
20+THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS
21+"AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT
16−IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY,
22+LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR
17−FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE
23+A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT
18−AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER
24+OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL,
25+SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT
26+LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE,
27+DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY
19−LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM,
28+THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT
20−OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE
29+(INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE
21−SOFTWARE.
30+OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
README.md+24−107
@@ -1,11 +1,5 @@
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−
9The LAoP discipline generalises relations and functions treating them as
3The LAoP discipline generalises relations and functions treating them as
10Boolean matrices and in turn consider these as arrows.
4Boolean matrices and in turn consider these as arrows.
11
5
@@ -16,38 +10,33 @@ motivation behind the library, the underlying theory, and implementation details
16This module offers many of the combinators mentioned in the work of
10This module offers many of the combinators mentioned in the work of
17[Macedo (2012)](https://repositorium.sdum.uminho.pt/handle/1822/22894) and [Oliveira (2012)](https://pdfs.semanticscholar.org/ccf5/27fa9179081223bffe8067edd81948644fc0.pdf).
11[Macedo (2012)](https://repositorium.sdum.uminho.pt/handle/1822/22894) and [Oliveira (2012)](https://pdfs.semanticscholar.org/ccf5/27fa9179081223bffe8067edd81948644fc0.pdf).
18
12
19−See the package in hackage [here](https://hackage.haskell.org/package/laop-0.1.1.0)
13+See the candidate package in hackage [here](https://hackage.haskell.org/package/laop-0.1.0.0/candidate)
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.
22
14
23## Features
15## Features
24
16
25−This library offers 3 main matrix programming modules:
17+This library offers:
26−
18+
27−- One in which matrices are typed with type level natural numbers;
19+- An internal representation that uses normal datatypes (`Void`, `()`, `Either`) for matrix dimensions and two
28−- One in which matrices are typed with arbitrary generic data types;
20+ type families `FromNat` and `Count` to make it easier to work with these type of matrices.
29−- One in which matrices are regarded as relations, i.e. boolean matrices;
21+- A module that uses generalised types for the dimensions and is just a newtype wrapper
30−
22+ around the internal matrix data type.
31−There's also an experimental module that uses matrices to represent probability
23+- Other that uses type level naturals for the dimensions and is just a newtype wrapper
32−distributions.
24+ around the internal matrix data type.
33−
25+- A very simple Probabilistic Programming module and several functions and data types to
34−The most interesting feature is that matrices are represented as an inductive data type.
26+ make it easier to deal with sample space.
35−Given this formulation, matrix algorithms can be expressed in a much more elegant and
27+
36−calculational style than the traditional vector of vectors representation. This data type
28+Given this, this new matrix formulation compared to other libraries one has much more advantages, such as:
37−guarantees that a matrix will always have valid dimensions. It can also express block matrix
29+
38−computations naturally, which leads to total, efficient and statically typed manipulation
30+- Has an inductive definition enabling writing matrix manipulation functions in a much more elegant and calculational way;
39−and transformation functions.
31+- Statically typed dimensions;
40−
32+- Polymorphic data type dimensions;
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.
33+- Polymorphic matrix content;
42−
34+- Awesome dimension type inference;
43−Given this, this new matrix formulation compared to other libraries:
35+- Fast type natural conversion via `FromNat` type family;
44−
36+- Matrix `Junc` and `Split`-ing in O(1);
45−- Is more compositional and polymorphic and does not have partial matrix manipulation functions (hence less chances for usage errors);
37+- Matrix composition takes advantage of divide-and-conquer and fusion laws.
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.
38+
47−
48−## Known issues
49−
50−Unfortunately, due to the use of type-level programming features, this approach sometimes requires type dimensions to be constrainted, in some way, impossible to write idiomatic Arrow instances, for example. Type inference isn't perfect, when it comes to infer the types of matrices which dimensions are computed using type level naturals multiplication, the compiler needs type annotations in order to succeed. And not all kinds of programs can be modeled using matrices, namely programs that deal with arbitrary infinite data types such as lists or integers (although there are some workarounds).
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.
51
40
52## Notes
41## Notes
53
42
@@ -129,73 +118,6 @@ grass_wet = row [0,1] . kp1
129rainning :: Matrix Double (Bool, (Bool, Bool)) One
118rainning :: Matrix Double (Bool, (Bool, Bool)) One
130rainning = row [0,1] . kp2 . kp2
119rainning = row [0,1] . kp2 . kp2
131
120
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−
199main :: IO ()
121main :: IO ()
200main = do
122main = do
201 putStrLn "Monty Hall Problem solution:"
123 putStrLn "Monty Hall Problem solution:"
@@ -210,8 +132,6 @@ main = do
210 prettyPrint (grass_wet . state)
132 prettyPrint (grass_wet . state)
211 putStrLn "\n Probability of rain:"
133 putStrLn "\n Probability of rain:"
212 prettyPrint (rainning . state)
134 prettyPrint (rainning . state)
213− putStrLn "\n Is the arbitrary state a valid state? (Alcuin Puzzle)"
214− print (inv bankStateR)
215```
135```
216
136
217```Shell
137```Shell
@@ -270,7 +190,4 @@ Monty Hall Problem solution:
270┌ ┐
190┌ ┐
271│ 0.2 │
191│ 0.2 │
272└ ┘
192└ ┘
273−
274−Is the arbitrary state a valid state? (Alcuin Puzzle)
275−False
276```
193```
Setup.hsnew file+2
@@ -0,0 +1,2 @@
1+import Distribution.Simple
2+main = defaultMain
test/Examples/Readme.hs → app/Main.hsrenamed+33−61
@@ -1,13 +1,10 @@
1−{-# LANGUAGE GADTs #-}
2{-# LANGUAGE DeriveGeneric #-}
1{-# LANGUAGE DeriveGeneric #-}
3{-# LANGUAGE FlexibleContexts #-}
2{-# 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− )
10− where
7+module Main where
11
8
12import LAoP.Matrix.Type
9import LAoP.Matrix.Type
13import qualified LAoP.Relation as R
10import qualified LAoP.Relation as R
@@ -15,12 +12,13 @@ import LAoP.Utils
15import LAoP.Dist
12import LAoP.Dist
16import GHC.TypeLits
13import GHC.TypeLits
17import Data.Coerce
14import Data.Coerce
18−import qualified GHC.Generics as G
15+import GHC.Generics
16+import Control.Category hiding (id)
19−import Prelude hiding (id, (.))
17+import Prelude hiding ((.))
20
18
21-- Monty Hall Problem
19-- Monty Hall Problem
22data Outcome = Win | Lose
20data Outcome = Win | Lose
23− deriving (Bounded, Enum, Eq, Show, G.Generic)
21+ deriving (Bounded, Enum, Eq, Show, Generic)
24
22
25switch :: Outcome -> Outcome
23switch :: Outcome -> Outcome
26switch Win = Lose
24switch Win = Lose
@@ -30,7 +28,7 @@ firstChoice :: Matrix Double () Outcome
30firstChoice = col [1/3, 2/3]
28firstChoice = col [1/3, 2/3]
31
29
32secondChoice :: Matrix Double Outcome Outcome
30secondChoice :: Matrix Double Outcome Outcome
33−secondChoice = fromF switch
31+secondChoice = fromF' switch
34
32
35-- Dice sum
33-- Dice sum
36
34
@@ -39,7 +37,7 @@ type SS = Natural 1 6 -- Sample Space
39sumSS :: SS -> SS -> Natural 2 12
37sumSS :: SS -> SS -> Natural 2 12
40sumSS = coerceNat (+)
38sumSS = coerceNat (+)
41
39
42−sumSSM = fromF (uncurry sumSS)
40+sumSSM = fromF' (uncurry sumSS)
43
41
44condition :: (Int, Int) -> Int -> Int
42condition :: (Int, Int) -> Int -> Int
45condition (fst, snd) thrd = if fst == snd
43condition (fst, snd) thrd = if fst == snd
@@ -49,64 +47,38 @@ condition (fst, snd) thrd = if fst == snd
49conditionSS :: (SS, SS) -> SS -> Natural 3 18
47conditionSS :: (SS, SS) -> SS -> Natural 3 18
50conditionSS = coerceNat2 condition
48conditionSS = coerceNat2 condition
51
49
52−conditionalThrows = fromF (uncurry conditionSS) . kr (kr die die) die
50+conditionalThrows = fromF' (uncurry conditionSS) . khatri (khatri die die) die
53
51
54die :: Matrix Double () SS
52die :: Matrix Double () SS
55die = col $ map (const (1/6)) [nat @1 @6 1 .. nat 6]
53die = col $ map (const (1/6)) [nat @1 @6 1 .. nat 6]
56
54
57-- Sprinkler
55-- Sprinkler
58−data G = Dry | Wet
59− deriving (Bounded, Enum, Eq, Show, G.Generic)
60−
61−data S = Off | On
62− deriving (Bounded, Enum, Eq, Show, G.Generic)
63
56
64−data R = No | Yes
65− deriving (Bounded, Enum, Eq, Show, G.Generic)
66−
67−rain :: Matrix Double () R
57+rain :: Matrix Double () Bool
68−rain = matrixBuilder gen
58+rain = col [0.8, 0.2]
69− where
70− gen (_, No) = 0.8
71− gen (_, Yes) = 0.2
72
59
73−sprinkler :: Matrix Double R S
60+sprinkler :: Matrix Double Bool Bool
74−sprinkler = matrixBuilder gen
61+sprinkler = fromLists [[0.6, 0.99], [0.4, 0.01]]
75− where
76− gen (No, Off) = 0.6
77− gen (No, On) = 0.4
78− gen (Yes, Off) = 0.99
79− gen (Yes, On) = 0.01
80−
81−grass :: Matrix Double (S, R) G
82−grass = matrixBuilder gen
83− where
84− gen ((Off, No), Dry) = 1
85− gen ((Off, Yes), Dry) = 0.2
86− gen ((On, No), Dry) = 0.1
87− gen ((On, Yes), Dry) = 0.01
88− gen ((Off, No), Wet) = 0
89− gen ((Off, Yes), Wet) = 0.8
90− gen ((On, No), Wet) = 0.9
91− gen ((On, Yes), Wet) = 0.99
92
62
93−tag f = kr f id
63+grass :: Matrix Double (Bool, Bool) Bool
64+grass = fromLists [[1, 0.2, 0.1, 0.01], [0, 0.8, 0.9, 0.99]]
94
65
95−state g s r = tag g . tag s . r
66+state :: Matrix Double () (Bool, (Bool, Bool))
67+state = khatri grass identity . khatri sprinkler identity . rain
96
68
97−grass_wet :: Matrix Double () (G, (S, R)) -> Matrix Double One One
69+grass_wet :: Matrix Double (Bool, (Bool, Bool)) One
98−grass_wet state = row [0,1] . fstM . state
70+grass_wet = row [0,1] . kp1
99
71
100−rainning :: Matrix Double (G, (S, R)) One
72+rainning :: Matrix Double (Bool, (Bool, Bool)) One
101−rainning = row [0,1] . sndM . sndM
73+rainning = row [0,1] . kp2 . kp2
102
74
103-- Alcuin Puzzle
75-- Alcuin Puzzle
104
76
105data Being = Farmer | Fox | Goose | Beans
77data Being = Farmer | Fox | Goose | Beans
106− deriving (Bounded, Enum, Eq, Show, G.Generic)
78+ deriving (Bounded, Enum, Eq, Show, Generic)
107
79
108data Bank = LeftB | RightB
80data Bank = LeftB | RightB
109− deriving (Bounded, Enum, Eq, Show, G.Generic)
81+ deriving (Bounded, Enum, Eq, Show, Generic)
110
82
111eats :: Being -> Being -> Bool
83eats :: Being -> Being -> Bool
112eats Fox Goose = True
84eats Fox Goose = True
@@ -121,21 +93,21 @@ cross LeftB = RightB
121cross RightB = LeftB
93cross RightB = LeftB
122
94
123crossR :: R.Relation Bank Bank
95crossR :: R.Relation Bank Bank
124−crossR = R.fromF cross
96+crossR = R.fromF' cross
125
97
126-- | Initial state, everyone in the left bank
98-- | Initial state, everyone in the left bank
127locationLeft :: Being -> Bank
99locationLeft :: Being -> Bank
128locationLeft _ = LeftB
100locationLeft _ = LeftB
129
101
130locationLeftR :: R.Relation Being Bank
102locationLeftR :: R.Relation Being Bank
131−locationLeftR = R.fromF locationLeft
103+locationLeftR = R.fromF' locationLeft
132
104
133-- | Initial state, everyone in the right bank
105-- | Initial state, everyone in the right bank
134locationRight :: Being -> Bank
106locationRight :: Being -> Bank
135locationRight _ = RightB
107locationRight _ = RightB
136
108
137locationRightR :: R.Relation Being Bank
109locationRightR :: R.Relation Being Bank
138−locationRightR = R.fromF locationRight
110+locationRightR = R.fromF' locationRight
139
111
140-- Properties
112-- Properties
141
113
@@ -152,7 +124,7 @@ inv :: R.Relation Being Bank -> Bool
152inv w = (w `R.comp` canEat w) `R.sse` (w `R.comp` farmer)
124inv w = (w `R.comp` canEat w) `R.sse` (w `R.comp` farmer)
153 where
125 where
154 farmer :: R.Relation Being Being
126 farmer :: R.Relation Being Being
155− farmer = R.fromF (const Farmer)
127+ farmer = R.fromF' (const Farmer)
156
128
157-- Arbitrary state
129-- Arbitrary state
158bankState :: Being -> Bank -> Bool
130bankState :: Being -> Bank -> Bool
@@ -166,19 +138,19 @@ bankStateR :: R.Relation Being Bank
166bankStateR = R.toRel bankState
138bankStateR = R.toRel bankState
167
139
168-- Main
140-- Main
169−exec :: IO ()
141+main :: IO ()
170−exec = do
142+main = do
171 putStrLn "Monty Hall Problem solution:"
143 putStrLn "Monty Hall Problem solution:"
172 prettyPrint (secondChoice . firstChoice)
144 prettyPrint (secondChoice . firstChoice)
173 putStrLn "\n Sum of dices probability:"
145 putStrLn "\n Sum of dices probability:"
174− prettyPrint (sumSSM . kr die die)
146+ prettyPrint (sumSSM `comp` khatri die die)
175 putStrLn "\n Conditional dice throw:"
147 putStrLn "\n Conditional dice throw:"
176 prettyPrint conditionalThrows
148 prettyPrint conditionalThrows
177 putStrLn "\n Checking that the last result is indeed a distribution: "
149 putStrLn "\n Checking that the last result is indeed a distribution: "
178− prettyPrint (bang . sumSSM . kr die die)
150+ prettyPrint (bang . sumSSM . khatri die die)
179 putStrLn "\n Probability of grass being wet:"
151 putStrLn "\n Probability of grass being wet:"
180− prettyPrint (grass_wet (state grass sprinkler rain))
152+ prettyPrint (grass_wet . state)
181 putStrLn "\n Probability of rain:"
153 putStrLn "\n Probability of rain:"
182− prettyPrint (rainning . state grass sprinkler rain)
154+ prettyPrint (rainning . state)
183 putStrLn "\n Is the arbitrary state a valid state? (Alcuin Puzzle)"
155 putStrLn "\n Is the arbitrary state a valid state? (Alcuin Puzzle)"
184 print (inv bankStateR)
156 print (inv bankStateR)
appveyor.ymldeleted−34
@@ -1,34 +0,0 @@
1−clone_folder: "c:\\WORK"
2−clone_depth: 5
3−
4−# Do not build feature branch with open Pull Requests
5−skip_branch_with_pr: true
6−
7−platform:
8− - x86_64
9−
10−cache:
11− - "C:\\SR"
12− - dist-newstyle
13−
14−environment:
15− global:
16− CABOPTS: --store-dir=C:\\SR
17−
18− matrix:
19− - GHCVER: 8.6.5
20−
21−install:
22− - choco source add -n mistuke -s https://www.myget.org/F/mistuke/api/v2
23− - choco install -y cabal --version 2.4.1.0
24− - choco install -y ghc --version 8.6.3
25− - refreshenv
26−
27−before_build:
28− - cabal --version
29− - ghc --version
30− - cabal %CABOPTS% v2-update
31−
32−build_script:
33− - cabal %CABOPTS% v2-build --enable-tests
34− - cabal %CABOPTS% v2-test --enable-tests
benchmark/Main.hsdeleted−175
@@ -1,175 +0,0 @@
1−{-# LANGUAGE KindSignatures #-}
2−{-# LANGUAGE GeneralizedNewtypeDeriving #-}
3−{-# LANGUAGE DerivingVia #-}
4−{-# LANGUAGE DataKinds #-}
5−{-# LANGUAGE BangPatterns #-}
6−{-# LANGUAGE TypeApplications #-}
7−{-# LANGUAGE FlexibleContexts #-}
8−{-# LANGUAGE AllowAmbiguousTypes #-}
9−{-# LANGUAGE ScopedTypeVariables #-}
10−
11−module Main (main) where
12−
13−import LAoP.Dist.Internal
14−import LAoP.Utils
15−import LAoP.Matrix.Type hiding (CountableN, Countable, FLN)
16−import qualified LAoP.Matrix.Type as T (FLN)
17−import Criterion.Main
18−import Control.DeepSeq
19−import Test.QuickCheck
20−import GHC.TypeLits
21−import Data.Proxy
22−import Prelude hiding (id, (.))
23−
24−selectM2 ::
25− ( Num e,
26− T.FLN b b,
27− CountableN b
28− ) => Matrix e cols (Either a b) -> Matrix e a b -> Matrix e cols b
29−selectM2 m y = join y iden `comp` m
30−
31−selectD2 ::
32− ( FLN b b,
33− CountableN b
34− ) => Dist (Either a b) -> Matrix Prob a b -> Dist b
35−selectD2 (D d) m = D (join m iden `comp` d)
36−
37−-- Composition with iden
38−compId m = comp iden m
39−
40−randomDist :: forall a . (Countable a, FLN () a) => Gen (Dist a)
41−randomDist = do
42− let size = fromInteger (natVal (Proxy :: Proxy (Count a)))
43− l <- vectorOf size (arbitrary :: Gen Prob)
44− let ln = normalize l
45− lr = map (:[]) ln
46− m = fromLists lr
47− return (D m)
48−
49−randomMatrix :: forall a b . (CountableDims a b, FLN a b) => Gen (Matrix Prob a b)
50−randomMatrix = do
51− let cols = fromInteger (natVal (Proxy :: Proxy (Count a)))
52− rows = fromInteger (natVal (Proxy :: Proxy (Count b)))
53− l <- vectorOf (cols * rows) arbitrary
54− let lr = buildList l cols
55− m = fromLists lr
56− return m
57−
58−buildList [] _ = []
59−buildList l r = take r l : buildList (drop r l) r
60−
61−normalize :: [Prob] -> [Prob]
62−normalize l = let l' = map abs l
63− s = sum l'
64− in map (/ s) l'
65−
66−-- Probability
67−newtype Probability = P Double
68− deriving (Num, Show, Fractional, NFData) via Double
69−newtype Dist' a = D' { unD :: [(a,Probability)] }
70− deriving (Show, NFData)
71−
72−instance Functor Dist' where
73− fmap f (D' d) = D' [(f x,p) | (x,p) <- d]
74−
75−instance Applicative Dist' where
76− pure x = D' [(x, 1)]
77− fm <*> m = D' [(f x,q*p) | (f,p) <- unD fm, (x,q) <- unD m]
78−
79−class Applicative f => Selective f where
80− select :: f (Either a b) -> f (a -> b) -> f b
81−
82−instance Selective Dist' where
83− select x y = (\e f -> either f id e) <$> x <*> y -- selectA
84−
85−instance Monad Dist' where
86− return = pure
87− (D' d) >>= f = D' [(y,q*p) | (x,p) <- d, (y,q) <- unD (f x)]
88−
89−normalize2 :: forall a . (Enum a, Bounded a) => [Probability] -> [(a, Probability)]
90−normalize2 l = let l' = map abs l
91− as = [minBound .. maxBound]
92− s = sum l'
93− probs = map (/ s) l'
94− in zip as probs
95−
96−randomDist2 :: forall a . (Countable a, Enum a, Bounded a) => Gen (Dist' a)
97−randomDist2 = do
98− let size = fromInteger (natVal (Proxy :: Proxy (Count a)))
99− l <- vectorOf size (arbitrary :: Gen Prob)
100− let ln = normalize2 @a (map P l)
101− return (D' ln)
102−
103−normalize3 :: forall a . [a] -> [Probability] -> [(a, Probability)]
104−normalize3 as l = let s = sum l
105− probs = map (/ s) l
106− in zip as probs
107−
108−randomDistF :: forall a b . (CountableDims a b, CoArbitrary a, Arbitrary b) => Gen (Dist' (a -> b))
109−randomDistF = do
110− let a = fromInteger (natVal (Proxy :: Proxy (Count a)))
111− b = fromInteger (natVal (Proxy :: Proxy (Count b)))
112− size = a * b
113− l <- vectorOf size (arbitrary :: Gen Prob)
114− l2 <- vectorOf size (arbitrary :: Gen (a -> b))
115− let !ln = normalize3 l2 (map P l)
116− return (D' ln)
117−
118−instance CoArbitrary (Natural a b)
119−
120−instance forall (a :: Nat) (b :: Nat). (KnownNat a, KnownNat b) => Arbitrary (Natural a b)
121− where
122− arbitrary =
123− let bottom = fromInteger (natVal (Proxy :: Proxy a))
124− top = fromInteger (natVal (Proxy :: Proxy b))
125− in do
126− x <- arbitrary `suchThat` (\n -> n >= bottom && n <= top)
127− return (nat x)
128−
129−setupEnv = do
130− m11 <- generate (resize 1 (randomMatrix @(Natural 0 10) @(Natural 0 10) ))
131− m12 <- generate (resize 1 (randomMatrix @(Natural 0 10) @(Natural 0 10) ))
132− m21 <- generate (resize 1 (randomMatrix @(Natural 0 100) @(Natural 0 100) ))
133− m22 <- generate (resize 1 (randomMatrix @(Natural 0 100) @(Natural 0 100) ))
134− m31 <- generate (resize 1 (randomMatrix @(Natural 0 200) @(Natural 0 200) ))
135− m32 <- generate (resize 1 (randomMatrix @(Natural 0 200) @(Natural 0 200) ))
136− return (m11, m12, m21, m22, m31, m32)
137−
138−setupEnv2 = do
139− m21 <- generate (resize 1 (randomMatrix @(Natural 0 100) @(Natural 0 100) ))
140− m40 <- generate (resize 1 (randomMatrix @(Natural 0 100) @(Either (Natural 0 100) (Natural 0 100) )))
141− dist <- generate (resize 1 (randomDist @(Either (Natural 0 100) (Natural 0 100)) ))
142− dist2 <- generate (resize 1 (randomMatrix @(Natural 0 100) @(Natural 0 100) ))
143− distList1 <- generate (resize 1 (randomDist2 @(Either (Natural 0 100) (Natural 0 100))))
144− distList2 <- generate (resize 1 (randomDistF @(Natural 0 100) @(Natural 0 100)))
145− return (m21, m40, dist, dist2, distList1, distList2)
146−
147−main :: IO ()
148−main = defaultMain [
149− env setupEnv $ \ ~(m11, m12, m21, m22, m31, m32) -> bgroup "Matrix Composition" [
150− bgroup "10x10" [
151− bench "WHNF - 10x10" $ whnf (comp m11) m12
152− , bench "NF - 10x10" $ nf (comp m11) m12
153− ],
154− bgroup "100x100" [
155− bench "WHNF - 100x100" $ whnf (comp m21) m22
156− , bench "NF - 100x100" $ nf (comp m21) m22
157− ],
158− bgroup "200x200" [
159− bench "WHNF - 200x200" $ whnf (comp m31) m32
160− , bench "NF - 200x200" $ nf (comp m31) m32
161− ],
162− bgroup "200x200 - RULES" [
163− bench "No rules - 200x200" $ nf (comp m21) iden
164− , bench "Rules - 200x200" $ nf compId m21
165− ] ],
166− env setupEnv2 $ \ ~(m21, m40, dist, dist2, dl1, dl2) -> bgroup "Matrix vs List - `select`" [
167− bgroup "Distribution `select` - 100+100 / 100x100" [
168− bench "List Distribution - Applicative version" $ nf (select dl1) dl2
169− , bench "Matrix Distribution - Applicative version" $ nf (selectD2 dist) dist2
170− , bench "Matrix Distribution - Selective version" $ nf (selectD dist) dist2
171− ],
172− bgroup "Matrix `select` - 100x(100+100) / 100x100" [
173− bench "Applicative version" $ nf (selectM2 m40) m21
174− , bench "Selective version" $ nf (selectM m40) m21
175− ] ] ]
laop.cabaldeleted−89
@@ -1,89 +0,0 @@
1−cabal-version: 2.4
2−name: laop
3−version: 0.1.1.1
4−synopsis: Matrix programming library
5−description: Matrix programming library that uses a type-safe inductive definition
6− inspired by the Linear Algebra of Programming
7−homepage: https://github.com/bolt12/laop
8−bug-reports: https://github.com/bolt12/laop/issues
9−license: MIT
10−license-file: LICENSE
11−author: Armando Santos
12−maintainer: Armando Santos <armandoifsantos@gmail.com>
13−copyright: 2020 Armando Santos
14−category: Data
15−build-type: Simple
16−extra-doc-files: README.md
17− CHANGELOG.md
18−tested-with: GHC == 8.6.5
19− GHC == 8.8.3
20−
21−source-repository head
22− type: git
23− location: https://github.com/bolt12/laop.git
24−
25−common common-options
26− build-depends: base >= 4.12.0.0 && < 5,
27− deepseq
28−
29− ghc-options: -Wall
30− -Wcompat
31− -Widentities
32− -Wincomplete-uni-patterns
33− -Wincomplete-record-updates
34− if impl(ghc >= 8.0)
35− ghc-options: -Wredundant-constraints
36− if impl(ghc >= 8.2)
37− ghc-options: -fhide-source-paths
38− if impl(ghc >= 8.4)
39− ghc-options: -Wmissing-export-lists
40− -Wpartial-fields
41− if impl(ghc >= 8.8)
42− ghc-options: -Wmissing-deriving-strategies
43−
44− default-language: Haskell2010
45−
46−library
47− import: common-options
48− hs-source-dirs: src
49− exposed-modules: LAoP.Dist
50− LAoP.Dist.Internal
51− LAoP.Matrix.Internal
52− LAoP.Matrix.Nat
53− LAoP.Matrix.Type
54− LAoP.Relation
55− LAoP.Relation.Internal
56− LAoP.Utils
57− LAoP.Utils.Internal
58−
59−test-suite laop-test
60− import: common-options
61− type: exitcode-stdio-1.0
62− hs-source-dirs: test
63− other-modules: Examples.Readme
64− main-is: Spec.hs
65− build-depends: laop
66− ghc-options: -threaded
67− -rtsopts
68− -with-rtsopts=-N
69− -funfolding-use-threshold=16
70− -fexcess-precision
71− -optc-O3
72− -optc-ffast-math
73−
74−benchmark laop-benchmark
75− import: common-options
76− type: exitcode-stdio-1.0
77− hs-source-dirs: benchmark
78− main-is: Main.hs
79− build-depends: criterion
80− , QuickCheck
81− , deepseq
82− , laop
83− ghc-options: -threaded
84− -rtsopts
85− -with-rtsopts=-N
86− -funfolding-use-threshold=16
87− -fexcess-precision
88− -optc-O3
89− -optc-ffast-math
package.yamlnew file+48
@@ -0,0 +1,48 @@
1+name: laop
2+version: 0.1.0.0
3+github: "bolt12/laop"
4+license: BSD3
5+author: "Armando Santos"
6+maintainer: "armandoifsantos@gmail.com"
7+copyright: "MIT"
8+
9+extra-source-files:
10+- README.md
11+- ChangeLog.md
12+
13+# Metadata used when publishing your package
14+# synopsis: Short description of your package
15+# category: Web
16+
17+# To avoid duplicated efforts in documentation and dealing with the
18+# complications of embedding Haddock markup inside cabal files, it is
19+# common to point users to the README.md file.
20+description: Please see the README on GitHub at <https://github.com/bolt12/laop#readme>
21+
22+dependencies:
23+- base >= 4.7 && < 5
24+
25+library:
26+ source-dirs: src
27+
28+executables:
29+ laop-exe:
30+ main: Main.hs
31+ source-dirs: app
32+ ghc-options:
33+ - -threaded
34+ - -rtsopts
35+ - -with-rtsopts=-N
36+ dependencies:
37+ - laop
38+
39+tests:
40+ laop-test:
41+ main: Spec.hs
42+ source-dirs: test
43+ ghc-options:
44+ - -threaded
45+ - -rtsopts
46+ - -with-rtsopts=-N
47+ dependencies:
48+ - laop
src/LAoP/Dist.hs−10
@@ -36,14 +36,6 @@ module LAoP.Dist
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−
47 -- * Functor instance equivalent functions
39 -- * Functor instance equivalent functions
48 fmapD,
40 fmapD,
49
41
@@ -53,8 +45,6 @@ module LAoP.Dist
53
45
54 -- * Selective equivalent functions
46 -- * Selective equivalent functions
55 selectD,
47 selectD,
56− branchD,
57− ifD,
58
48
59 -- * Monad equivalent functions
49 -- * Monad equivalent functions
60 returnD,
50 returnD,
src/LAoP/Dist/Internal.hs+36−87
@@ -1,5 +1,3 @@
1−{-# LANGUAGE DerivingVia #-}
2−{-# LANGUAGE ConstraintKinds #-}
3{-# LANGUAGE GADTs #-}
1{-# LANGUAGE GADTs #-}
4{-# LANGUAGE AllowAmbiguousTypes #-}
2{-# LANGUAGE AllowAmbiguousTypes #-}
5{-# LANGUAGE TypeApplications #-}
3{-# LANGUAGE TypeApplications #-}
@@ -10,27 +8,18 @@
10{-# LANGUAGE RankNTypes #-}
8{-# LANGUAGE RankNTypes #-}
11
9
12module LAoP.Dist.Internal
10module LAoP.Dist.Internal
13− (
11+ (
14 Dist(..),
12 Dist(..),
15 Prob,
13 Prob,
16
14
17− Countable,
18− CountableN,
19− CountableDimsN,
20− FLN,
21− Liftable,
22− TrivialP,
23−
24 fmapD,
15 fmapD,
25 unitD,
16 unitD,
26 multD,
17 multD,
27 selectD,
18 selectD,
28− branchD,
29− ifD,
30 returnD,
19 returnD,
31 bindD,
20 bindD,
32 (??),
21 (??),
33−
22+
34 choose,
23 choose,
35 shape,
24 shape,
36 linear,
25 linear,
@@ -43,15 +32,11 @@ module LAoP.Dist.Internal
43 )
32 )
44 where
33 where
45
34
46−import LAoP.Matrix.Type hiding (TrivialP, Countable, CountableDims, CountableN, CountableDimsN, Liftable, FLN)
35+import LAoP.Matrix.Type
47−import Prelude hiding (id, (.))
48−import qualified LAoP.Matrix.Internal as I
49import LAoP.Utils
36import LAoP.Utils
50import GHC.TypeLits
37import GHC.TypeLits
51import Data.Proxy
38import Data.Proxy
52import Data.List (sortBy)
39import Data.List (sortBy)
53−import Control.DeepSeq
54−import Data.Bool
55
40
56-- | Type synonym for probability value
41-- | Type synonym for probability value
57type Prob = Double
42type Prob = Double
@@ -59,21 +44,17 @@ type Prob = Double
59-- | Type synonym for column vector matrices. This represents a probability
44-- | Type synonym for column vector matrices. This represents a probability
60-- distribution.
45-- distribution.
61newtype Dist a = D (Matrix Prob () a)
46newtype 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)
71
47
72-- | Functor instance
48-- | Functor instance
73fmapD ::
49fmapD ::
74− ( Liftable a b,
50+ ( Bounded a,
75− CountableDimsN a b,
51+ Bounded b,
76− FLN b a
52+ Enum a,
53+ Enum b,
54+ Eq b,
55+ KnownNat (Count (Normalize a)),
56+ KnownNat (Count (Normalize b)),
57+ FromLists Prob (Normalize b) (Normalize a)
77 )
58 )
78 =>
59 =>
79 (a -> b) -> Dist a -> Dist b
60 (a -> b) -> Dist a -> Dist b
@@ -85,58 +66,26 @@ unitD = D (one 1)
85
66
86-- | Applicative/Monoidal instance 'mult' function
67-- | Applicative/Monoidal instance 'mult' function
87multD ::
68multD ::
88− ( CountableDimsN a b,
69+ ( KnownNat (Count (Normalize a)),
89− CountableN (a, b),
70+ KnownNat (Count (Normalize b)),
90− FLN (a, b) a,
71+ KnownNat (Count (Normalize (a, b))),
91− FLN (a, b) b,
72+ FromLists Prob (Normalize (a, b)) (Normalize a),
92− TrivialP a b
73+ FromLists Prob (Normalize (a, b)) (Normalize b),
74+ Normalize (a, b) ~ Normalize (Normalize a, Normalize b)
93 ) => Dist a -> Dist b -> Dist (a, b)
75 ) => Dist a -> Dist b -> Dist (a, b)
94−multD (D a) (D b) = D (kr a b)
76+multD (D a) (D b) = D (khatri a b)
95
77
96-- | Selective instance function
78-- | Selective instance function
97selectD ::
79selectD ::
98− ( FLN b b,
80+ ( Normalize (Either a b) ~ Either (Normalize a) (Normalize b),
99− CountableN b
81+ FromLists Prob (Normalize b) (Normalize b),
82+ KnownNat (Count (Normalize b))
100 ) => Dist (Either a b) -> Matrix Prob a b -> Dist b
83 ) => Dist (Either a b) -> Matrix Prob a b -> Dist b
101−selectD (D d) m = D (selectM d m)
84+selectD (D d) m = D (junc m identity `comp` d)
102−
85+
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
137
86
138-- | Monad instance 'return' function
87-- | Monad instance 'return' function
139−returnD :: forall a . (Enum a, FLN () a, Countable a) => a -> Dist a
88+returnD :: forall a . (Enum a, FromLists Prob () (Normalize a), KnownNat (Count a)) => a -> Dist a
140returnD a = D (col l)
89returnD a = D (col l)
141 where
90 where
142 i = fromInteger $ natVal (Proxy :: Proxy (Count a))
91 i = fromInteger $ natVal (Proxy :: Proxy (Count a))
@@ -150,8 +99,8 @@ bindD (D d) m = D (m `comp` d)
150-- | Extract probabilities given an Event.
99-- | Extract probabilities given an Event.
151(??) ::
100(??) ::
152 ( Enum a,
101 ( Enum a,
153− Countable a,
102+ KnownNat (Count a),
154− FLN () a
103+ FromLists Prob () (Normalize a)
155 ) => (a -> Bool) -> Dist a -> Prob
104 ) => (a -> Bool) -> Dist a -> Prob
156(??) p d =
105(??) p d =
157 let l = toValues d
106 let l = toValues d
@@ -161,11 +110,11 @@ bindD (D d) m = D (m `comp` d)
161-- Distribution Construction
110-- Distribution Construction
162
111
163-- | Constructs a Bernoulli distribution
112-- | Constructs a Bernoulli distribution
164−choose :: (FLN () a) => Prob -> Dist a
113+choose :: (FromLists Prob () (Normalize a)) => Prob -> Dist a
165choose prob = D (col [prob, 1 - prob])
114choose prob = D (col [prob, 1 - prob])
166
115
167-- | Creates a distribution given a shape function
116-- | Creates a distribution given a shape function
168−shape :: (FLN () a) => (Prob -> Prob) -> [a] -> Dist a
117+shape :: (FromLists Prob () (Normalize a)) => (Prob -> Prob) -> [a] -> Dist a
169shape _ [] = error "Probability.shape: empty list"
118shape _ [] = error "Probability.shape: empty list"
170shape f xs =
119shape f xs =
171 let incr = 1 / fromIntegral (length xs - 1)
120 let incr = 1 / fromIntegral (length xs - 1)
@@ -173,23 +122,23 @@ shape f xs =
173 in fromFreqs (zip xs ps)
122 in fromFreqs (zip xs ps)
174
123
175-- | Constructs a Linear distribution
124-- | Constructs a Linear distribution
176−linear :: (FLN () a) => [a] -> Dist a
125+linear :: (FromLists Prob () (Normalize a)) => [a] -> Dist a
177linear = shape id
126linear = shape id
178
127
179-- | Constructs an Uniform distribution
128-- | Constructs an Uniform distribution
180−uniform :: (FLN () a) => [a] -> Dist a
129+uniform :: (FromLists Prob () (Normalize a)) => [a] -> Dist a
181uniform = shape (const 1)
130uniform = shape (const 1)
182
131
183-- | Constructs an Negative Exponential distribution
132-- | Constructs an Negative Exponential distribution
184−negExp :: (FLN () a) => [a] -> Dist a
133+negExp :: (FromLists Prob () (Normalize a)) => [a] -> Dist a
185negExp = shape (\x -> exp (-x))
134negExp = shape (\x -> exp (-x))
186
135
187-- | Constructs an Normal distribution
136-- | Constructs an Normal distribution
188−normal :: (FLN () a) => [a] -> Dist a
137+normal :: (FromLists Prob () (Normalize a)) => [a] -> Dist a
189normal = shape (normalCurve 0.5 0.5)
138normal = shape (normalCurve 0.5 0.5)
190
139
191-- | Transforms a 'Dist' into a list of pairs.
140-- | Transforms a 'Dist' into a list of pairs.
192−toValues :: forall a . (Enum a, Countable a, FLN () a) => Dist a -> [(a, Prob)]
141+toValues :: forall a . (Enum a, KnownNat (Count a), FromLists Prob () (Normalize a)) => Dist a -> [(a, Prob)]
193toValues (D d) =
142toValues (D d) =
194 let rows = fromInteger (natVal (Proxy :: Proxy (Count a)))
143 let rows = fromInteger (natVal (Proxy :: Proxy (Count a)))
195 probs = toList d
144 probs = toList d
@@ -197,7 +146,7 @@ toValues (D d) =
197 in res
146 in res
198
147
199-- | Pretty a distribution
148-- | Pretty a distribution
200−prettyDist :: forall a. (Show a, Enum a, Countable a, FLN () a) => Dist a -> String
149+prettyDist :: forall a. (Show a, Enum a, KnownNat (Count a), FromLists Prob () (Normalize a)) => Dist a -> String
201prettyDist d =
150prettyDist d =
202 let values = sortBy (\(a, p1) (b, p2) -> compare p2 p1) (toValues @a d)
151 let values = sortBy (\(a, p1) (b, p2) -> compare p2 p1) (toValues @a d)
203 w = maximum (map (length . show . fst) values)
152 w = maximum (map (length . show . fst) values)
@@ -209,12 +158,12 @@ prettyDist d =
209 showR n x = show x ++ " "
158 showR n x = show x ++ " "
210
159
211-- | Pretty Print a distribution
160-- | Pretty Print a distribution
212−prettyPrintDist :: forall a . (Show a, Enum a, Countable a, FLN () a) => Dist a -> IO ()
161+prettyPrintDist :: forall a . (Show a, Enum a, KnownNat (Count a), FromLists Prob () (Normalize a)) => Dist a -> IO ()
213prettyPrintDist = putStrLn . prettyDist @a
162prettyPrintDist = putStrLn . prettyDist @a
214
163
215-- Auxiliary functions
164-- Auxiliary functions
216
165
217−fromFreqs :: (FLN () a) => [(a,Prob)] -> Dist a
166+fromFreqs :: (FromLists Prob () (Normalize a)) => [(a,Prob)] -> Dist a
218fromFreqs xs = D (col (map (\(x,p) -> p/q) xs))
167fromFreqs xs = D (col (map (\(x,p) -> p/q) xs))
219 where q = sum $ map snd xs
168 where q = sum $ map snd xs
220
169
src/LAoP/Matrix/Internal.hs+436−445
@@ -1,6 +1,4 @@
1−{-# LANGUAGE StrictData #-}
2{-# LANGUAGE TypeFamilyDependencies #-}
1{-# LANGUAGE TypeFamilyDependencies #-}
3−{-# LANGUAGE ConstraintKinds #-}
4{-# LANGUAGE AllowAmbiguousTypes #-}
2{-# LANGUAGE AllowAmbiguousTypes #-}
5{-# LANGUAGE DataKinds #-}
3{-# LANGUAGE DataKinds #-}
6{-# LANGUAGE FlexibleContexts #-}
4{-# LANGUAGE FlexibleContexts #-}
@@ -30,7 +28,7 @@
30-- motivation behind the library, the underlying theory, and implementation details.
28-- motivation behind the library, the underlying theory, and implementation details.
31--
29--
32-- This module offers many of the combinators mentioned in the work of
30-- This module offers many of the combinators mentioned in the work of
33−-- Macedo (2012) and Oliveira (2012).
31+-- Macedo (2012) and Oliveira (2012).
34--
32--
35-- This is an Internal module and it is no supposed to be imported.
33-- This is an Internal module and it is no supposed to be imported.
36--
34--
@@ -43,26 +41,17 @@ module LAoP.Matrix.Internal
43 --
41 --
44 -- There exists two type families that make it easier to write
42 -- There exists two type families that make it easier to write
45 -- matrix dimensions: 'FromNat' and 'Count'. This approach
43 -- matrix dimensions: 'FromNat' and 'Count'. This approach
46− -- leads to a very straightforward implementation
44+ -- leads to a very straightforward implementation
47− -- of LAoP combinators.
45+ -- of LAoP combinators.
48
46
49 -- * Type safe matrix representation
47 -- * Type safe matrix representation
50 Matrix (..),
48 Matrix (..),
51
49
52− -- * Constraint type aliases
53− Countable,
54− CountableDims,
55− CountableN,
56− CountableDimsN,
57− FL,
58− FLN,
59− Liftable,
60− Trivial,
61−
62 -- * Primitives
50 -- * Primitives
51+ empty,
63 one,
52 one,
64− join,
53+ junc,
65− fork,
54+ split,
66
55
67 -- * Auxiliary type families
56 -- * Auxiliary type families
68 FromNat,
57 FromNat,
@@ -75,7 +64,6 @@ module LAoP.Matrix.Internal
75 toLists,
64 toLists,
76 toList,
65 toList,
77 matrixBuilder,
66 matrixBuilder,
78− matrixBuilder',
79 row,
67 row,
80 col,
68 col,
81 zeros,
69 zeros,
@@ -86,38 +74,28 @@ module LAoP.Matrix.Internal
86 -- * Misc
74 -- * Misc
87 -- ** Get dimensions
75 -- ** Get dimensions
88 columns,
76 columns,
89− columns',
90 rows,
77 rows,
91− rows',
92
78
93 -- ** Matrix Transposition
79 -- ** Matrix Transposition
94 tr,
80 tr,
95
81
96− -- ** Scalar multiplication/division of matrices
97− (.|),
98− (./),
99−
100 -- ** Selective operator
82 -- ** Selective operator
101− select,
83+ select,
102− branch,
103
84
104 -- ** McCarthy's Conditional
85 -- ** McCarthy's Conditional
105 cond,
86 cond,
106
87
107 -- ** Matrix "abiding"
88 -- ** Matrix "abiding"
108− abideJF,
89+ abideJS,
109− abideFJ,
90+ abideSJ,
110−
111− -- ** Zip matrices
112− zipWithM,
113
91
114 -- * Biproduct approach
92 -- * Biproduct approach
115− -- ** Fork
93+ -- ** Split
116 (===),
94 (===),
117 -- *** Projections
95 -- *** Projections
118 p1,
96 p1,
119 p2,
97 p2,
120− -- ** Join
98+ -- ** Junc
121 (|||),
99 (|||),
122 -- *** Injections
100 -- *** Injections
123 i1,
101 i1,
@@ -130,13 +108,12 @@ module LAoP.Matrix.Internal
130
108
131 -- | Note that given the restrictions imposed it is not possible to
109 -- | Note that given the restrictions imposed it is not possible to
132 -- implement the standard type classes present in standard Haskell.
110 -- implement the standard type classes present in standard Haskell.
133−
134 -- *** Matrix pairing projections
111 -- *** Matrix pairing projections
135− fstM,
112+ kp1,
136− sndM,
113+ kp2,
137
114
138 -- *** Matrix pairing
115 -- *** Matrix pairing
139− kr,
116+ khatri,
140
117
141 -- * Matrix composition and lifting
118 -- * Matrix composition and lifting
142
119
@@ -144,10 +121,10 @@ module LAoP.Matrix.Internal
144
121
145 -- | Note that given the restrictions imposed it is not possible to
122 -- | Note that given the restrictions imposed it is not possible to
146 -- implement the standard type classes present in standard Haskell.
123 -- implement the standard type classes present in standard Haskell.
147− iden,
124+ identity,
148 comp,
125 comp,
149− fromF',
150 fromF,
126 fromF,
127+ fromF',
151
128
152 -- * Matrix printing
129 -- * Matrix printing
153 pretty,
130 pretty,
@@ -174,22 +151,21 @@ import LAoP.Utils.Internal
174import Data.Bool
151import Data.Bool
175import Data.Kind
152import Data.Kind
176import Data.List
153import Data.List
177−import Data.Maybe
178import Data.Proxy
154import Data.Proxy
179−import Data.Typeable
180import Data.Void
155import Data.Void
181import GHC.TypeLits
156import GHC.TypeLits
182import Data.Type.Equality
157import Data.Type.Equality
183import GHC.Generics
158import GHC.Generics
184import Control.DeepSeq
159import Control.DeepSeq
160+import Control.Category
185−import Prelude hiding (id, (.))
161+import Prelude hiding ((.))
186−import qualified Prelude (id, (.))
187
162
188-- | LAoP (Linear Algebra of Programming) Inductive Matrix definition.
163-- | LAoP (Linear Algebra of Programming) Inductive Matrix definition.
189data Matrix e cols rows where
164data Matrix e cols rows where
165+ Empty :: Matrix e Void Void
190 One :: e -> Matrix e () ()
166 One :: e -> Matrix e () ()
191− Join :: Matrix e a rows -> Matrix e b rows -> Matrix e (Either a b) rows
167+ Junc :: Matrix e a rows -> Matrix e b rows -> Matrix e (Either a b) rows
192− Fork :: Matrix e cols a -> Matrix e cols b -> Matrix e cols (Either a b)
168+ Split :: Matrix e cols a -> Matrix e cols b -> Matrix e cols (Either a b)
193
169
194deriving instance (Show e) => Show (Matrix e cols rows)
170deriving instance (Show e) => Show (Matrix e cols rows)
195
171
@@ -199,214 +175,221 @@ deriving instance (Show e) => Show (Matrix e cols rows)
199-- 'Generic' instance.
175-- 'Generic' instance.
200type family Count (d :: Type) :: Nat where
176type family Count (d :: Type) :: Nat where
201 Count (Natural n m) = (m - n) + 1
177 Count (Natural n m) = (m - n) + 1
202− Count (List a) = (^) 2 (Count a)
203− Count (Either a b) = (+) (Count a) (Count b)
178+ Count (Either a b) = (+) (Count a) (Count b)
204− Count (a, b) = (*) (Count a) (Count b)
179+ Count (a, b) = (*) (Count a) (Count b)
205− Count (a -> b) = (^) (Count b) (Count a)
180+ Count (a -> b) = (^) (Count b) (Count a)
206 -- Generics
181 -- Generics
207− Count (M1 _ _ f p) = Count (f p)
182+ Count (M1 _ _ f p) = Count (f p)
208− Count (K1 _ _ _) = 1
183+ Count (K1 _ _ _) = 1
209− Count (V1 _) = 0
184+ Count (V1 _) = 0
210− Count (U1 _) = 1
185+ Count (U1 _) = 1
211 Count ((:*:) a b p) = Count (a p) * Count (b p)
186 Count ((:*:) a b p) = Count (a p) * Count (b p)
212 Count ((:+:) a b p) = Count (a p) + Count (b p)
187 Count ((:+:) a b p) = Count (a p) + Count (b p)
213− Count d = Count (Rep d R)
188+ Count d = Count (Rep d R)
214
189
215-- | Type family that computes of a given type dimension from a given natural
190-- | Type family that computes of a given type dimension from a given natural
216--
191--
217-- Thanks to Li-Yao Xia this type family is super fast.
192-- Thanks to Li-Yao Xia this type family is super fast.
218type family FromNat (n :: Nat) :: Type where
193type family FromNat (n :: Nat) :: Type where
194+ FromNat 0 = Void
219 FromNat 1 = ()
195 FromNat 1 = ()
220 FromNat n = FromNat' (Mod n 2 == 0) (FromNat (Div n 2))
196 FromNat n = FromNat' (Mod n 2 == 0) (FromNat (Div n 2))
221
197
222type family FromNat' (b :: Bool) (m :: Type) :: Type where
198type family FromNat' (b :: Bool) (m :: Type) :: Type where
223− FromNat' 'True m = Either m m
199+ FromNat' 'True m = Either m m
224 FromNat' 'False m = Either () (Either m m)
200 FromNat' 'False m = Either () (Either m m)
225
201
226-- | Type family that normalizes the representation of a given data
202-- | Type family that normalizes the representation of a given data
227-- structure
203-- structure
228type family Normalize (d :: Type) :: Type where
204type family Normalize (d :: Type) :: Type where
229− Normalize (Either a b) = Either (Normalize a) (Normalize b)
230− Normalize d = FromNat (Count d)
205+ Normalize d = FromNat (Count d)
231−
206+
232−-- | Constraint type synonyms to keep the type signatures less convoluted
233−type Countable a = KnownNat (Count a)
234−type CountableN a = KnownNat (Count (Normalize a))
235−type CountableDims a b = (Countable a, Countable b)
236−type CountableDimsN a b = (CountableN a, CountableN b)
237−type FL a b = FromLists a b
238−type FLN a b = FromLists (Normalize a) (Normalize b)
239−type Liftable e a b = (Bounded a, Bounded b, Enum a, Enum b, Eq b, Num e, Ord e)
240−type Trivial a = FromNat (Count a) ~ a
241−
242−-- | It is possible to implement a constrained version of the category type
207+-- | It isn't possible to implement the 'id' function so it's
243−-- class.
208+-- implementation is 'undefined'. However 'comp' can be and this partial
209+-- class implementation exists just to make the code more readable.
210+--
211+-- Please use 'identity' instead.
244instance (Num e) => Category (Matrix e) where
212instance (Num e) => Category (Matrix e) where
245− type Object (Matrix e) a = (FL a a, Countable a)
213+ id = undefined
246− id = iden
247− (.) = comp
214+ (.) = comp
248
215
249instance NFData e => NFData (Matrix e cols rows) where
216instance NFData e => NFData (Matrix e cols rows) where
217+ rnf Empty = ()
250− rnf (One e) = rnf e
218+ rnf (One e) = rnf e
251− rnf (Join a b) = rnf a `seq` rnf b
219+ rnf (Junc a b) = rnf a `seq` rnf b
252− rnf (Fork a b) = rnf a `seq` rnf b
220+ rnf (Split a b) = rnf a `seq` rnf b
253
221
254instance Eq e => Eq (Matrix e cols rows) where
222instance Eq e => Eq (Matrix e cols rows) where
223+ Empty == Empty = True
255− (One a) == (One b) = a == b
224+ (One a) == (One b) = a == b
256− (Join a b) == (Join c d) = a == c && b == d
225+ (Junc a b) == (Junc c d) = a == c && b == d
257− (Fork a b) == (Fork c d) = a == c && b == d
226+ (Split a b) == (Split c d) = a == c && b == d
258− x@(Fork _ _) == y@(Join _ _) = x == abideJF y
227+ x@(Split _ _) == y@(Junc _ _) = x == abideJS y
259− x@(Join _ _) == y@(Fork _ _) = abideJF x == y
228+ x@(Junc _ _) == y@(Split _ _) = abideJS x == y
260
229
261instance Num e => Num (Matrix e cols rows) where
230instance 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)
271
231
232+ Empty + Empty = Empty
233+ (One a) + (One b) = One (a + b)
234+ (Junc a b) + (Junc c d) = Junc (a + c) (b + d)
235+ (Split a b) + (Split c d) = Split (a + c) (b + d)
236+ x@(Split _ _) + y@(Junc _ _) = x + abideJS y
237+ x@(Junc _ _) + y@(Split _ _) = abideJS x + y
238+
239+ Empty - Empty = Empty
240+ (One a) - (One b) = One (a - b)
241+ (Junc a b) - (Junc c d) = Junc (a - c) (b - d)
242+ (Split a b) - (Split c d) = Split (a - c) (b - d)
243+ x@(Split _ _) - y@(Junc _ _) = x - abideJS y
244+ x@(Junc _ _) - y@(Split _ _) = abideJS x - y
245+
246+ Empty * Empty = Empty
247+ (One a) * (One b) = One (a * b)
248+ (Junc a b) * (Junc c d) = Junc (a * c) (b * d)
249+ (Split a b) * (Split c d) = Split (a * c) (b * d)
250+ x@(Split _ _) * y@(Junc _ _) = x * abideJS y
251+ x@(Junc _ _) * y@(Split _ _) = abideJS x * y
252+
253+ abs Empty = Empty
254+ abs (One a) = One (abs a)
255+ abs (Junc a b) = Junc (abs a) (abs b)
256+ abs (Split a b) = Split (abs a) (abs b)
257+
258+ signum Empty = Empty
272− signum (One a) = One (signum a)
259+ signum (One a) = One (signum a)
273− signum (Join a b) = Join (signum a) (signum b)
260+ signum (Junc a b) = Junc (signum a) (signum b)
274− signum (Fork a b) = Fork (signum a) (signum b)
261+ signum (Split a b) = Split (signum a) (signum b)
275
262
276instance Ord e => Ord (Matrix e cols rows) where
263instance Ord e => Ord (Matrix e cols rows) where
264+ Empty <= Empty = True
277− (One a) <= (One b) = a <= b
265+ (One a) <= (One b) = a <= b
278− (Join a b) <= (Join c d) = (a <= c) && (b <= d)
266+ (Junc a b) <= (Junc c d) = (a <= c) && (b <= d)
279− (Fork a b) <= (Fork c d) = (a <= c) && (b <= d)
267+ (Split a b) <= (Split c d) = (a <= c) && (b <= d)
280− x@(Fork _ _) <= y@(Join _ _) = x <= abideJF y
268+ x@(Split _ _) <= y@(Junc _ _) = x <= abideJS y
281− x@(Join _ _) <= y@(Fork _ _) = abideJF x <= y
269+ x@(Junc _ _) <= y@(Split _ _) = abideJS x <= y
282
270
283-- Primitives
271-- Primitives
284
272
273+-- | Empty matrix constructor
274+empty :: Matrix e Void Void
275+empty = Empty
276+
285-- | Unit matrix constructor
277-- | Unit matrix constructor
286one :: e -> Matrix e () ()
278one :: e -> Matrix e () ()
287one = One
279one = One
288
280
289−-- | Matrix 'Join' constructor
281+-- | Matrix 'Junc' constructor
290−join :: Matrix e a rows -> Matrix e b rows -> Matrix e (Either a b) rows
282+junc :: Matrix e a rows -> Matrix e b rows -> Matrix e (Either a b) rows
291−join = Join
283+junc = Junc
292
284
293infixl 3 |||
285infixl 3 |||
294
286
295−-- | Matrix 'Join' constructor
287+-- | Matrix 'Junc' constructor
296(|||) :: Matrix e a rows -> Matrix e b rows -> Matrix e (Either a b) rows
288(|||) :: Matrix e a rows -> Matrix e b rows -> Matrix e (Either a b) rows
297−(|||) = Join
289+(|||) = Junc
298
290
299−-- | Matrix 'Fork' constructor
291+-- | Matrix 'Split' constructor
300−fork :: Matrix e cols a -> Matrix e cols b -> Matrix e cols (Either a b)
292+split :: Matrix e cols a -> Matrix e cols b -> Matrix e cols (Either a b)
301−fork = Fork
293+split = Split
302
294
303infixl 2 ===
295infixl 2 ===
304
296
305−-- | Matrix 'Fork' constructor
297+-- | Matrix 'Split' constructor
306(===) :: Matrix e cols a -> Matrix e cols b -> Matrix e cols (Either a b)
298(===) :: Matrix e cols a -> Matrix e cols b -> Matrix e cols (Either a b)
307−(===) = Fork
299+(===) = Split
308
300
309-- Construction
301-- Construction
310
302
311-- | Type class for defining the 'fromList' conversion function.
303-- | Type class for defining the 'fromList' conversion function.
312--
304--
313-- Given that it is not possible to branch on types at the term level type
305-- Given that it is not possible to branch on types at the term level type
314−-- classes are needed very much like an inductive definition but on types.
306+-- classes are needed bery much like an inductive definition but on types.
315−class FromLists cols rows where
307+class FromLists e cols rows where
316 -- | Build a matrix out of a list of list of elements. Throws a runtime
308 -- | Build a matrix out of a list of list of elements. Throws a runtime
317 -- error if the dimensions do not match.
309 -- error if the dimensions do not match.
318 fromLists :: [[e]] -> Matrix e cols rows
310 fromLists :: [[e]] -> Matrix e cols rows
319
311
320−instance FromLists () () where
312+instance FromLists e Void Void where
313+ fromLists [] = Empty
314+ fromLists _ = error "Wrong dimensions"
315+
316+instance {-# OVERLAPPING #-} FromLists e () () where
321 fromLists [[e]] = One e
317 fromLists [[e]] = One e
322 fromLists _ = error "Wrong dimensions"
318 fromLists _ = error "Wrong dimensions"
323
319
324−instance (FromLists cols ()) => FromLists (Either () cols) () where
320+instance {-# OVERLAPPING #-} (FromLists e cols ()) => FromLists e (Either () cols) () where
325− fromLists [h : t] = Join (One h) (fromLists [t])
321+ fromLists [h : t] = Junc (One h) (fromLists [t])
326 fromLists _ = error "Wrong dimensions"
322 fromLists _ = error "Wrong dimensions"
327
323
328−instance {-# OVERLAPPABLE #-}
329− (FromLists a (), FromLists b (), Countable a) => FromLists (Either a b) () where
324+instance {-# OVERLAPPABLE #-} (FromLists e a (), FromLists e b (), KnownNat (Count a)) => FromLists e (Either a b) () where
330− fromLists [l] =
325+ fromLists [l] =
331 let rowsA = fromInteger (natVal (Proxy :: Proxy (Count a)))
326 let rowsA = fromInteger (natVal (Proxy :: Proxy (Count a)))
332− in Join (fromLists [take rowsA l]) (fromLists [drop rowsA l])
327+ in Junc (fromLists [take rowsA l]) (fromLists [drop rowsA l])
333 fromLists _ = error "Wrong dimensions"
328 fromLists _ = error "Wrong dimensions"
334
329
335−instance (FromLists () rows) => FromLists () (Either () rows) where
330+instance {-# OVERLAPPING #-} (FromLists e () rows) => FromLists e () (Either () rows) where
336− fromLists ([h] : t) = Fork (One h) (fromLists t)
331+ fromLists ([h] : t) = Split (One h) (fromLists t)
337 fromLists _ = error "Wrong dimensions"
332 fromLists _ = error "Wrong dimensions"
338
333
339−instance {-# OVERLAPPABLE #-}
340− (FromLists () a, FromLists () b, Countable a) => FromLists () (Either a b) where
334+instance {-# OVERLAPPABLE #-} (FromLists e () a, FromLists e () b, KnownNat (Count a)) => FromLists e () (Either a b) where
341− fromLists l@([_] : _) =
335+ fromLists l@([_] : _) =
342 let rowsA = fromInteger (natVal (Proxy :: Proxy (Count a)))
336 let rowsA = fromInteger (natVal (Proxy :: Proxy (Count a)))
343− in Fork (fromLists (take rowsA l)) (fromLists (drop rowsA l))
337+ in Split (fromLists (take rowsA l)) (fromLists (drop rowsA l))
344 fromLists _ = error "Wrong dimensions"
338 fromLists _ = error "Wrong dimensions"
345
339
346−instance (FromLists (Either a b) c, FromLists (Either a b) d, Countable c)
340+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
347− => FromLists (Either a b) (Either c d) where
348 fromLists l@(h : t) =
341 fromLists l@(h : t) =
349 let lh = length h
342 let lh = length h
350 rowsC = fromInteger (natVal (Proxy :: Proxy (Count c)))
343 rowsC = fromInteger (natVal (Proxy :: Proxy (Count c)))
351− condition = all ((== lh) . length) t
344+ condition = all (== lh) (map length t)
352 in if lh > 0 && condition
345 in if lh > 0 && condition
353− then Fork (fromLists (take rowsC l)) (fromLists (drop rowsC l))
346+ then Split (fromLists (take rowsC l)) (fromLists (drop rowsC l))
354 else error "Not all rows have the same length"
347 else error "Not all rows have the same length"
355
348
356-- | Matrix builder function. Constructs a matrix provided with
349-- | Matrix builder function. Constructs a matrix provided with
357−-- a construction function that operates with indices.
350+-- a construction function.
358−matrixBuilder' ::
351+matrixBuilder ::
359 forall e cols rows.
352 forall e cols rows.
360− ( FL cols rows,
353+ ( FromLists e cols rows,
361− CountableDims cols rows
354+ KnownNat (Count cols),
355+ KnownNat (Count rows)
356+ ) =>
357+ ((Int, Int) -> e) ->
362− ) => ((Int, Int) -> e) -> Matrix e cols rows
358+ Matrix e cols rows
363−matrixBuilder' f =
359+matrixBuilder f =
364 let c = fromInteger $ natVal (Proxy :: Proxy (Count cols))
360 let c = fromInteger $ natVal (Proxy :: Proxy (Count cols))
365 r = fromInteger $ natVal (Proxy :: Proxy (Count rows))
361 r = fromInteger $ natVal (Proxy :: Proxy (Count rows))
366 positions = [(a, b) | a <- [0 .. (r - 1)], b <- [0 .. (c - 1)]]
362 positions = [(a, b) | a <- [0 .. (r - 1)], b <- [0 .. (c - 1)]]
367 in fromLists . map (map f) . groupBy (\(x, _) (w, _) -> x == w) $ positions
363 in fromLists . map (map f) . groupBy (\(x, _) (w, _) -> x == w) $ positions
368
364
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−
389-- | Constructs a column vector matrix
365-- | Constructs a column vector matrix
390−col :: (FL () rows) => [e] -> Matrix e () rows
366+col :: (FromLists e () rows) => [e] -> Matrix e () rows
391col = fromLists . map (: [])
367col = fromLists . map (: [])
392
368
393-- | Constructs a row vector matrix
369-- | Constructs a row vector matrix
394−row :: (FL cols ()) => [e] -> Matrix e cols ()
370+row :: (FromLists e cols ()) => [e] -> Matrix e cols ()
395row = fromLists . (: [])
371row = fromLists . (: [])
396
372
397-- | Lifts functions to matrices with arbitrary dimensions.
373-- | Lifts functions to matrices with arbitrary dimensions.
398--
374--
399-- NOTE: Be careful to not ask for a matrix bigger than the cardinality of
375-- NOTE: Be careful to not ask for a matrix bigger than the cardinality of
400-- types @a@ or @b@ allows.
376-- types @a@ or @b@ allows.
401−fromF' ::
377+fromF ::
402 forall a b cols rows e.
378 forall a b cols rows e.
403− ( Liftable e a b,
379+ ( Bounded a,
404− CountableDims cols rows,
380+ Bounded b,
381+ Enum a,
382+ Enum b,
383+ Eq b,
384+ Num e,
385+ Ord e,
386+ KnownNat (Count cols),
387+ KnownNat (Count rows),
405− FL rows cols
388+ FromLists e rows cols
406 ) =>
389 ) =>
407 (a -> b) ->
390 (a -> b) ->
408 Matrix e cols rows
391 Matrix e cols rows
409−fromF' f =
392+fromF f =
410 let minA = minBound @a
393 let minA = minBound @a
411 maxA = maxBound @a
394 maxA = maxBound @a
412 minB = minBound @b
395 minB = minBound @b
@@ -416,8 +399,8 @@ fromF' f =
416 elementsA = take ccols [minA .. maxA]
399 elementsA = take ccols [minA .. maxA]
417 elementsB = take rrows [minB .. maxB]
400 elementsB = take rrows [minB .. maxB]
418 combinations = (,) <$> elementsA <*> elementsB
401 combinations = (,) <$> elementsA <*> elementsB
419− combAp = map snd . sort . map (\(a, b) -> if f a == b
402+ combAp = map snd . sort . map (\(a, b) -> if f a == b
420− then ((fromEnum a, fromEnum b), 1)
403+ then ((fromEnum a, fromEnum b), 1)
421 else ((fromEnum a, fromEnum b), 0)) $ combinations
404 else ((fromEnum a, fromEnum b), 0)) $ combinations
422 mList = buildList combAp rrows
405 mList = buildList combAp rrows
423 in tr $ fromLists mList
406 in tr $ fromLists mList
@@ -427,23 +410,48 @@ fromF' f =
427
410
428-- | Lifts functions to matrices with dimensions matching @a@ and @b@
411-- | Lifts functions to matrices with dimensions matching @a@ and @b@
429-- cardinality's.
412-- cardinality's.
430−fromF ::
413+fromF' ::
431 forall a b e.
414 forall a b e.
432− ( Liftable e a b,
415+ ( Bounded a,
433− CountableDimsN a b,
416+ Bounded b,
434− FLN b a
417+ Enum a,
418+ Enum b,
419+ Eq b,
420+ Num e,
421+ Ord e,
422+ KnownNat (Count (Normalize a)),
423+ KnownNat (Count (Normalize b)),
424+ FromLists e (Normalize b) (Normalize a)
435 ) =>
425 ) =>
436 (a -> b) ->
426 (a -> b) ->
437 Matrix e (Normalize a) (Normalize b)
427 Matrix e (Normalize a) (Normalize b)
438−fromF = fromF'
428+fromF' f =
429+ let minA = minBound @a
430+ maxA = maxBound @a
431+ minB = minBound @b
432+ maxB = maxBound @b
433+ ccols = fromInteger $ natVal (Proxy :: Proxy (Count (Normalize a)))
434+ rrows = fromInteger $ natVal (Proxy :: Proxy (Count (Normalize b)))
435+ elementsA = take ccols [minA .. maxA]
436+ elementsB = take rrows [minB .. maxB]
437+ combinations = (,) <$> elementsA <*> elementsB
438+ combAp = map snd . sort . map (\(a, b) -> if f a == b
439+ then ((fromEnum a, fromEnum b), 1)
440+ else ((fromEnum a, fromEnum b), 0)) $ combinations
441+ mList = buildList combAp rrows
442+ in tr $ fromLists mList
443+ where
444+ buildList [] _ = []
445+ buildList l r = take r l : buildList (drop r l) r
439
446
440-- Conversion
447-- Conversion
441
448
442-- | Converts a matrix to a list of lists of elements.
449-- | Converts a matrix to a list of lists of elements.
443toLists :: Matrix e cols rows -> [[e]]
450toLists :: Matrix e cols rows -> [[e]]
451+toLists Empty = []
444toLists (One e) = [[e]]
452toLists (One e) = [[e]]
445−toLists (Fork l r) = toLists l ++ toLists r
453+toLists (Split l r) = toLists l ++ toLists r
446−toLists (Join l r) = zipWith (++) (toLists l) (toLists r)
454+toLists (Junc l r) = zipWith (++) (toLists l) (toLists r)
447
455
448-- | Converts a matrix to a list of elements.
456-- | Converts a matrix to a list of elements.
449toList :: Matrix e cols rows -> [e]
457toList :: Matrix e cols rows -> [e]
@@ -452,38 +460,37 @@ toList = concat . toLists
452-- Zeros Matrix
460-- Zeros Matrix
453
461
454-- | The zero matrix. A matrix wholly filled with zeros.
462-- | The zero matrix. A matrix wholly filled with zeros.
455−zeros :: (Num e, FL cols rows, CountableDims cols rows) => Matrix e cols rows
463+zeros :: (Num e, FromLists e cols rows, KnownNat (Count cols), KnownNat (Count rows)) => Matrix e cols rows
456−zeros = matrixBuilder' (const 0)
464+zeros = matrixBuilder (const 0)
457
465
458-- Ones Matrix
466-- Ones Matrix
459
467
460-- | The ones matrix. A matrix wholly filled with ones.
468-- | The ones matrix. A matrix wholly filled with ones.
461--
469--
462-- Also known as T (Top) matrix.
470-- Also known as T (Top) matrix.
463−ones :: (Num e, FL cols rows, CountableDims cols rows) => Matrix e cols rows
471+ones :: (Num e, FromLists e cols rows, KnownNat (Count cols), KnownNat (Count rows)) => Matrix e cols rows
464−ones = matrixBuilder' (const 1)
472+ones = matrixBuilder (const 1)
465
473
466-- Const Matrix
474-- Const Matrix
467
475
468-- | The constant matrix constructor. A matrix wholly filled with a given
476-- | The constant matrix constructor. A matrix wholly filled with a given
469-- value.
477-- value.
470−constant :: (Num e, FL cols rows, CountableDims cols rows) => e -> Matrix e cols rows
478+constant :: (Num e, FromLists e cols rows, KnownNat (Count cols), KnownNat (Count rows)) => e -> Matrix e cols rows
471−constant e = matrixBuilder' (const e)
479+constant e = matrixBuilder (const e)
472
480
473-- Bang Matrix
481-- Bang Matrix
474
482
475-- | The T (Top) row vector matrix.
483-- | The T (Top) row vector matrix.
476−bang :: forall e cols. (Num e, Enum e, FL cols (), Countable cols) => Matrix e cols ()
484+bang :: forall e cols. (Num e, Enum e, FromLists e cols (), KnownNat (Count cols)) => Matrix e cols ()
477bang =
485bang =
478 let c = fromInteger $ natVal (Proxy :: Proxy (Count cols))
486 let c = fromInteger $ natVal (Proxy :: Proxy (Count cols))
479 in fromLists [take c [1, 1 ..]]
487 in fromLists [take c [1, 1 ..]]
480
488
481−-- iden Matrix
489+-- Identity Matrix
482
490
483−-- | iden matrix.
491+-- | Identity matrix.
484−iden :: forall e cols . (Num e, FL cols cols, Countable cols) => Matrix e cols cols
492+identity :: (Num e, FromLists e cols cols, KnownNat (Count cols)) => Matrix e cols cols
485−iden = matrixBuilder' (bool 0 1 . uncurry (==))
493+identity = matrixBuilder (bool 0 1 . uncurry (==))
486−{-# NOINLINE iden #-}
487
494
488-- Matrix composition (MMM)
495-- Matrix composition (MMM)
489
496
@@ -492,90 +499,60 @@ iden = matrixBuilder' (bool 0 1 . uncurry (==))
492-- This definition takes advantage of divide-and-conquer and fusion laws
499-- This definition takes advantage of divide-and-conquer and fusion laws
493-- from LAoP.
500-- from LAoP.
494comp :: (Num e) => Matrix e cr rows -> Matrix e cols cr -> Matrix e cols rows
501comp :: (Num e) => Matrix e cr rows -> Matrix e cols cr -> Matrix e cols rows
502+comp Empty Empty = Empty
495−comp (One a) (One b) = One (a * b)
503+comp (One a) (One b) = One (a * b)
496−comp (Join a b) (Fork c d) = comp a c + comp b d -- Divide-and-conquer law
504+comp (Junc a b) (Split c d) = comp a c + comp b d -- Divide-and-conquer law
497−comp (Fork a b) c = Fork (comp a c) (comp b c) -- Fork fusion law
505+comp (Split a b) c = Split (comp a c) (comp b c) -- Split fusion law
498−comp c (Join a b) = Join (comp c a) (comp c b) -- Join fusion law
506+comp c (Junc a b) = Junc (comp c a) (comp c b) -- Junc 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)
522
507
523-- Projections
508-- Projections
524
509
525-- | Biproduct first component projection
510-- | Biproduct first component projection
526−p1 :: (Num e, CountableDims n m, FL n m, FL m m) => Matrix e (Either m n) m
511+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
527−p1 = join id zeros
512+p1 =
513+ let iden = identity :: Matrix e m m
514+ zero = zeros :: Matrix e n m
515+ in junc iden zero
528
516
529-- | Biproduct second component projection
517-- | Biproduct second component projection
530−p2 :: (Num e, CountableDims n m, FL m n, FL n n) => Matrix e (Either m n) n
518+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
531−p2 = join zeros id
519+p2 =
520+ let iden = identity :: Matrix e n n
521+ zero = zeros :: Matrix e m n
522+ in junc zero iden
532
523
533-- Injections
524-- Injections
534
525
535-- | Biproduct first component injection
526-- | Biproduct first component injection
536−i1 :: (Num e, CountableDims n m, FL n m, FL m m) => Matrix e m (Either m n)
527+i1 :: (Num e, KnownNat (Count n), KnownNat (Count m), FromLists e n m, FromLists e m m) => Matrix e m (Either m n)
537i1 = tr p1
528i1 = tr p1
538
529
539-- | Biproduct second component injection
530-- | Biproduct second component injection
540−i2 :: (Num e, CountableDims n m, FL m n, FL n n) => Matrix e n (Either m n)
531+i2 :: (Num e, KnownNat (Count n), KnownNat (Count m), FromLists e m n, FromLists e n n) => Matrix e n (Either m n)
541i2 = tr p2
532i2 = tr p2
542
533
543-- Dimensions
534-- Dimensions
544
535
545-- | Obtain the number of rows.
536-- | Obtain the number of rows.
546--
537--
547−-- NOTE: The 'KnownNat' constraint is needed in order to obtain the
538+-- NOTE: The 'KnownNat' constaint is needed in order to obtain the
548−-- dimensions in constant time. For a version that doesn't require the
539+-- dimensions in constant time.
549−-- constraint see 'rows''.
550−rows :: forall e cols rows. (Countable rows) => Matrix e cols rows -> Int
551−rows _ = fromInteger $ natVal (Proxy :: Proxy (Count rows))
552−
553−-- | Obtain the number of rows in an inefficient manner, but without any
554−-- constraints.
555--
540--
556−-- For a more efficient version see 'rows'.
541+-- TODO: A 'rows' function that does not need the 'KnownNat' constraint in
542+-- exchange for performance.
557−rows' :: Matrix e cols rows -> Int
543+rows :: forall e cols rows. (KnownNat (Count rows)) => Matrix e cols rows -> Int
558−rows' (One _) = 1
544+rows _ = fromInteger $ natVal (Proxy :: Proxy (Count rows))
559−rows' (Join lhs _) = rows' lhs
560−rows' (Fork top bottom) = rows' top + rows' bottom
561
545
562-- | Obtain the number of columns.
546-- | Obtain the number of columns.
547+--
548+-- NOTE: The 'KnownNat' constaint is needed in order to obtain the
549+-- dimensions in constant time.
563--
550--
564−-- NOTE: The 'KnownNat' constraint is needed in order to obtain the
551+-- TODO: A 'columns' function that does not need the 'KnownNat' constraint in
565−-- dimensions in constant time. For a version that doesn't require the
552+-- exchange for performance.
566−-- constraint see 'columns''.
567−columns :: forall e cols rows. (Countable cols) => Matrix e cols rows -> Int
553+columns :: forall e cols rows. (KnownNat (Count cols)) => Matrix e cols rows -> Int
568columns _ = fromInteger $ natVal (Proxy :: Proxy (Count cols))
554columns _ = fromInteger $ natVal (Proxy :: Proxy (Count cols))
569
555
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−
579-- Coproduct Bifunctor
556-- Coproduct Bifunctor
580
557
581infixl 5 -|-
558infixl 5 -|-
@@ -584,172 +561,157 @@ infixl 5 -|-
584(-|-) ::
561(-|-) ::
585 forall e n k m j.
562 forall e n k m j.
586 ( Num e,
563 ( Num e,
587− CountableDims j k,
564+ KnownNat (Count j),
588− FL k k,
565+ KnownNat (Count k),
589− FL j k,
566+ FromLists e k k,
590− FL k j,
567+ FromLists e j k,
591− FL j j
568+ FromLists e k j,
569+ FromLists e j j
592 ) =>
570 ) =>
593 Matrix e n k ->
571 Matrix e n k ->
594 Matrix e m j ->
572 Matrix e m j ->
595 Matrix e (Either n m) (Either k j)
573 Matrix e (Either n m) (Either k j)
596−(-|-) a b = Join (i1 . a) (i2 . b)
574+(-|-) a b = Junc (i1 . a) (i2 . b)
597
575
598-- Khatri Rao Product and projections
576-- Khatri Rao Product and projections
599
577
600-- | Khatri Rao product first component projection matrix.
578-- | Khatri Rao product first component projection matrix.
601−fstM ::
579+kp1 ::
602 forall e m k .
580 forall e m k .
603 ( Num e,
581 ( Num e,
604− CountableDims k m,
582+ KnownNat (Count k),
583+ FromLists e (FromNat (Count m * Count k)) m,
584+ KnownNat (Count m),
605− FL (Normalize (m, k)) m,
585+ KnownNat (Count (Normalize (m, k)))
606− CountableN (m, k)
607 ) => Matrix e (Normalize (m, k)) m
586 ) => Matrix e (Normalize (m, k)) m
608−fstM = matrixBuilder' f
587+kp1 = matrixBuilder f
609 where
588 where
610 offset = fromInteger (natVal (Proxy :: Proxy (Count k)))
589 offset = fromInteger (natVal (Proxy :: Proxy (Count k)))
611 f (x, y)
590 f (x, y)
612 | y >= (x * offset) && y <= (x * offset + offset - 1) = 1
591 | y >= (x * offset) && y <= (x * offset + offset - 1) = 1
613− | otherwise = 0
592+ | otherwise = 0
614
593
615-- | Khatri Rao product second component projection matrix.
594-- | Khatri Rao product second component projection matrix.
616−sndM ::
595+kp2 ::
617 forall e m k .
596 forall e m k .
618 ( Num e,
597 ( Num e,
619− CountableDims k m,
598+ KnownNat (Count k),
599+ FromLists e (FromNat (Count m * Count k)) k,
600+ KnownNat (Count m),
620− FL (Normalize (m, k)) k,
601+ KnownNat (Count (Normalize (m, k)))
621− CountableN (m, k)
622 ) => Matrix e (Normalize (m, k)) k
602 ) => Matrix e (Normalize (m, k)) k
623−sndM = matrixBuilder' f
603+kp2 = matrixBuilder f
624 where
604 where
625 offset = fromInteger (natVal (Proxy :: Proxy (Count k)))
605 offset = fromInteger (natVal (Proxy :: Proxy (Count k)))
626 f (x, y)
606 f (x, y)
627 | x == y || mod (y - x) offset == 0 = 1
607 | x == y || mod (y - x) offset == 0 = 1
628− | otherwise = 0
608+ | otherwise = 0
629
609
630-- | Khatri Rao Matrix product also known as matrix pairing.
610-- | Khatri Rao Matrix product also known as matrix pairing.
631--
611--
632-- NOTE: That this is not a true categorical product, see for instance:
612-- NOTE: That this is not a true categorical product, see for instance:
633−--
613+--
634-- @
614-- @
635−-- | fstM . kr a b == a
615+-- | kp1 . khatri a b == a
636−-- kr a b ==> |
616+-- khatri a b ==> |
637−-- | sndM . kr a b == b
617+-- | kp2 . khatri a b == b
638-- @
618-- @
639--
619--
640-- __Emphasis__ on the implication symbol.
620-- __Emphasis__ on the implication symbol.
641−kr ::
621+khatri ::
642− forall e cols a b.
622+ forall e cols a b.
643 ( Num e,
623 ( Num e,
644− CountableDims a b,
624+ KnownNat (Count a),
645− CountableN (a, b),
625+ KnownNat (Count b),
626+ KnownNat (Count (Normalize (a, b))),
646− FL (Normalize (a, b)) a,
627+ FromLists e (Normalize (a, b)) a,
647− FL (Normalize (a, b)) b
628+ FromLists e (Normalize (a, b)) b
648 ) => Matrix e cols a -> Matrix e cols b -> Matrix e cols (Normalize (a, b))
629 ) => Matrix e cols a -> Matrix e cols b -> Matrix e cols (Normalize (a, b))
649−kr a b =
630+khatri a b =
650− let fstM' = fstM @e @a @b
631+ let kp1' = kp1 @e @a @b
651− sndM' = sndM @e @a @b
632+ kp2' = kp2 @e @a @b
652− in (tr fstM' . a) * (tr sndM' . b)
633+ in (tr kp1') . a * (tr kp2') . b
653
634
654-- Product Bifunctor (Kronecker)
635-- Product Bifunctor (Kronecker)
655
636
656infixl 4 ><
637infixl 4 ><
657
638
658-- | Matrix product functor also known as kronecker product
639-- | Matrix product functor also known as kronecker product
659−(><) ::
640+(><) ::
660− forall e m p n q.
641+ forall e m p n q.
661 ( Num e,
642 ( Num e,
662− CountableDims m n,
643+ KnownNat (Count m),
663− CountableDims p q,
644+ KnownNat (Count n),
664− CountableDimsN (m, n) (p, q),
645+ KnownNat (Count p),
646+ KnownNat (Count q),
647+ KnownNat (Count (Normalize (m, n))),
665− FL (Normalize (m, n)) m,
648+ FromLists e (Normalize (m, n)) m,
666− FL (Normalize (m, n)) n,
649+ FromLists e (Normalize (m, n)) n,
667− FL (Normalize (p, q)) p,
650+ KnownNat (Count (Normalize (p, q))),
651+ FromLists e (Normalize (p, q)) p,
668− FL (Normalize (p, q)) q
652+ FromLists e (Normalize (p, q)) q
669− )
653+ )
670 => Matrix e m p -> Matrix e n q -> Matrix e (Normalize (m, n)) (Normalize (p, q))
654 => Matrix e m p -> Matrix e n q -> Matrix e (Normalize (m, n)) (Normalize (p, q))
671(><) a b =
655(><) a b =
672− let fstM' = fstM @e @m @n
656+ let kp1' = kp1 @e @m @n
673− sndM' = sndM @e @m @n
657+ kp2' = kp2 @e @m @n
674− in kr (a . fstM') (b . sndM')
658+ in khatri (a . kp1') (b . kp2')
675
659
676−-- Matrix abide Join Fork
660+-- Matrix abide Junc Split
677
661
678−-- | Matrix "abiding" following the 'Join'-'Fork' exchange law.
662+-- | Matrix "abiding" followin the 'Junc'-'Split' abide law.
679−--
663+--
680-- Law:
664-- Law:
681--
665--
682-- @
666-- @
683−-- 'Join' ('Fork' a c) ('Fork' b d) == 'Fork' ('Join' a b) ('Join' c d)
667+-- 'Junc' ('Split' a c) ('Split' b d) == 'Split' ('Junc' a b) ('Junc' c d)
684-- @
668-- @
685−abideJF :: Matrix e cols rows -> Matrix e cols rows
669+abideJS :: Matrix e cols rows -> Matrix e cols rows
686−abideJF (Join (Fork a c) (Fork b d)) = Fork (Join (abideJF a) (abideJF b)) (Join (abideJF c) (abideJF d)) -- Join-Fork abide law
670+abideJS (Junc (Split a c) (Split b d)) = Split (Junc (abideJS a) (abideJS b)) (Junc (abideJS c) (abideJS d)) -- Junc-Split abide law
671+abideJS Empty = Empty
687−abideJF (One e) = One e
672+abideJS (One e) = One e
688−abideJF (Join a b) = Join (abideJF a) (abideJF b)
673+abideJS (Junc a b) = Junc (abideJS a) (abideJS b)
689−abideJF (Fork a b) = Fork (abideJF a) (abideJF b)
674+abideJS (Split a b) = Split (abideJS a) (abideJS b)
690
675
691−-- Matrix abide Fork Join
676+-- Matrix abide Split Junc
692
677
693−-- | Matrix "abiding" followin the 'Fork'-'Join' abide law.
678+-- | Matrix "abiding" followin the 'Split'-'Junc' abide law.
694−--
679+--
695-- @
680-- @
696−-- 'Fork' ('Join' a b) ('Join' c d) == 'Join' ('Fork' a c) ('Fork' b d)
681+-- 'Split' ('Junc' a b) ('Junc' c d) == 'Junc' ('Split' a c) ('Split' b d)
697-- @
682-- @
698−abideFJ :: Matrix e cols rows -> Matrix e cols rows
683+abideSJ :: Matrix e cols rows -> Matrix e cols rows
699−abideFJ (Fork (Join a b) (Join c d)) = Join (Fork (abideFJ a) (abideFJ c)) (Fork (abideFJ b) (abideFJ d)) -- Fork-Join abide law
684+abideSJ (Split (Junc a b) (Junc c d)) = Junc (Split (abideSJ a) (abideSJ c)) (Split (abideSJ b) (abideSJ d)) -- Split-Junc abide law
685+abideSJ Empty = Empty
700−abideFJ (One e) = One e
686+abideSJ (One e) = One e
701−abideFJ (Join a b) = Join (abideFJ a) (abideFJ b)
687+abideSJ (Junc a b) = Junc (abideSJ a) (abideSJ b)
702−abideFJ (Fork a b) = Fork (abideFJ a) (abideFJ b)
688+abideSJ (Split a b) = Split (abideSJ a) (abideSJ b)
703
689
704-- Matrix transposition
690-- Matrix transposition
705
691
706-- | Matrix transposition.
692-- | Matrix transposition.
707tr :: Matrix e cols rows -> Matrix e rows cols
693tr :: Matrix e cols rows -> Matrix e rows cols
694+tr Empty = Empty
708−tr (One e) = One e
695+tr (One e) = One e
709−tr (Join a b) = Fork (tr a) (tr b)
696+tr (Junc a b) = Split (tr a) (tr b)
710−tr (Fork a b) = Join (tr a) (tr b)
697+tr (Split a b) = Junc (tr a) (tr b)
711
698
712-- Selective 'select' operator
699-- Selective 'select' operator
713
700
714-- | Selective functors 'select' operator equivalent inspired by the
701-- | Selective functors 'select' operator equivalent inspired by the
715-- ArrowMonad solution presented in the paper.
702-- ArrowMonad solution presented in the paper.
716−select :: (Num e, FL b b, Countable b) => Matrix e cols (Either a b) -> Matrix e a b -> Matrix e cols b
717−select (Fork a b) y = y . a + b -- Divide-and-conquer law
718−select (Join (Fork a c) (Fork b d)) y = join (y . a + c) (y . b + d) -- Pattern matching + DnC law
719−select m y = join y id . m
720−
721−branch ::
722− ( Num e,
723− CountableDims a b,
724− CountableDims c (Either b c),
725− FL c b,
726− FL a b,
727− FL a a,
728− FL b b,
729− FL c c,
730− FL b a,
731− FL b c,
732− FL (Either b c) b,
733− FL (Either b c) c
734− )
735− => Matrix e cols (Either a b) -> Matrix e a c -> Matrix e b c -> Matrix e cols c
703+select :: (Num e, FromLists e b b, KnownNat (Count b)) => Matrix e cols (Either a b) -> Matrix e a b -> Matrix e cols b
736−branch x l r = f x `select` g l `select` r
704+select m y = junc y identity . m
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
743
705
744-- McCarthy's Conditional
706-- McCarthy's Conditional
745
707
746-- | McCarthy's Conditional expresses probabilistic choice.
708-- | McCarthy's Conditional expresses probabilistic choice.
747cond ::
709cond ::
748− ( Trivial cols,
710+ ( cols ~ FromNat (Count cols),
749− Countable cols,
711+ KnownNat (Count cols),
750− FL () cols,
712+ FromLists e () cols,
751− FL cols (),
713+ FromLists e cols (),
752− FL cols cols,
714+ FromLists e cols cols,
753 Bounded a,
715 Bounded a,
754 Enum a,
716 Enum a,
755 Num e,
717 Num e,
@@ -757,14 +719,14 @@ cond ::
757 )
719 )
758 =>
720 =>
759 (a -> Bool) -> Matrix e cols rows -> Matrix e cols rows -> Matrix e cols rows
721 (a -> Bool) -> Matrix e cols rows -> Matrix e cols rows -> Matrix e cols rows
760−cond p f g = join f g . grd p
722+cond p f g = junc f g . grd p
761−
723+
762−grd ::
724+grd ::
763− ( Trivial q,
725+ ( q ~ FromNat (Count q),
764− Countable q,
726+ KnownNat (Count q),
765− FL () q,
727+ FromLists e () q,
766− FL q (),
728+ FromLists e q (),
767− FL q q,
729+ FromLists e q q,
768 Bounded a,
730 Bounded a,
769 Enum a,
731 Enum a,
770 Num e,
732 Num e,
@@ -772,86 +734,63 @@ grd ::
772 )
734 )
773 =>
735 =>
774 (a -> Bool) -> Matrix e q (Either q q)
736 (a -> Bool) -> Matrix e q (Either q q)
775−grd f = fork (corr f) (corr (not . f))
737+grd f = split (corr f) (corr (not . f))
776−
738+
777−corr ::
739+corr ::
778− forall e a q .
740+ forall e a q .
779− ( Trivial q,
741+ ( q ~ FromNat (Count q),
780− Countable q,
742+ KnownNat (Count q),
781− FL () q,
743+ FromLists e () q,
782− FL q (),
744+ FromLists e q (),
783− FL q q,
745+ FromLists e q q,
784− Liftable e a Bool
746+ Bounded a,
747+ Enum a,
748+ Num e,
749+ Ord e
785− )
750+ )
786 => (a -> Bool) -> Matrix e q q
751 => (a -> Bool) -> Matrix e q q
787−corr p = let f = fromF' p :: Matrix e q ()
752+corr p = let f = fromF p :: Matrix e q ()
788− in kr f (id :: Matrix e q q)
753+ in khatri f (identity :: Matrix e q q)
789
754
790-- Pretty print
755-- Pretty print
791
756
792prettyAux :: Show e => [[e]] -> [[e]] -> String
757prettyAux :: Show e => [[e]] -> [[e]] -> String
793prettyAux [] _ = ""
758prettyAux [] _ = ""
794−prettyAux [[e]] m = "│ " ++ fill (show e) ++ " │\n"
759+prettyAux [[e]] m = "│ " ++ fill (show e) ++ " │\n"
795 where
760 where
796 v = fmap show m
761 v = fmap show m
797 widest = maximum $ fmap length v
762 widest = maximum $ fmap length v
798 fill str = replicate (widest - length str - 2) ' ' ++ str
763 fill str = replicate (widest - length str - 2) ' ' ++ str
799−prettyAux [h] m = "│ " ++ fill (unwords $ map show h) ++ " │\n"
764+prettyAux [h] m = "│ " ++ fill (unwords $ map show h) ++ " │\n"
800 where
765 where
801− v = fmap show m
766+ v = fmap show m
802− widest = maximum $ fmap length v
767+ widest = maximum $ fmap length v
803 fill str = replicate (widest - length str - 2) ' ' ++ str
768 fill str = replicate (widest - length str - 2) ' ' ++ str
804−prettyAux (h : t) l = "│ " ++ fill (unwords $ map show h) ++ " │\n" ++
769+prettyAux (h : t) l = "│ " ++ fill (unwords $ map show h) ++ " │\n" ++
805 prettyAux t l
770 prettyAux t l
806 where
771 where
807− v = fmap show l
772+ v = fmap show l
808− widest = maximum $ fmap length v
773+ widest = maximum $ fmap length v
809 fill str = replicate (widest - length str - 2) ' ' ++ str
774 fill str = replicate (widest - length str - 2) ' ' ++ str
810
775
811-- | Matrix pretty printer
776-- | Matrix pretty printer
812−pretty :: (CountableDims cols rows, Show e) => Matrix e cols rows -> String
777+pretty :: (KnownNat (Count cols), Show e) => Matrix e cols rows -> String
813−pretty m = concat
814− [ "┌ ", unwords (replicate (columns m) blank), " ┐\n"
778+pretty m = "┌ " ++ unwords (replicate (columns m) blank) ++ " ┐\n" ++
815− , unlines
779+ prettyAux (toLists m) (toLists m) ++
816− [ "│ " ++ unwords (fmap (\j -> fill $ show $ getElem i j m) [1..columns m]) ++ " │" | i <- [1..rows m] ]
817− , "└ ", unwords (replicate (columns m) blank), " ┘"
780+ "└ " ++ unwords (replicate (columns m) blank) ++ " ┘"
818− ]
819− where
781+ where
820− strings = map show (toList m)
782+ v = fmap show (toList m)
821− widest = maximum $ map length strings
783+ widest = maximum $ fmap length v
822 fill str = replicate (widest - length str) ' ' ++ str
784 fill str = replicate (widest - length str) ' ' ++ str
823− blank = fill ""
785+ 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)
839
786
840-- | Matrix pretty printer
787-- | Matrix pretty printer
841−prettyPrint :: (CountableDims cols rows, Show e) => Matrix e cols rows -> IO ()
788+prettyPrint :: (KnownNat (Count cols), Show e) => Matrix e cols rows -> IO ()
842prettyPrint = putStrLn . pretty
789prettyPrint = putStrLn . pretty
843
790
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−
852-- Relational operators functions
791-- Relational operators functions
853
792
854−type Boolean = Natural 0 1
793+type Boolean = Natural 0 1
855type Relation a b = Matrix Boolean a b
794type Relation a b = Matrix Boolean a b
856
795
857-- | Helper conversion function
796-- | Helper conversion function
@@ -867,47 +806,54 @@ fromBool False = nat 0
867
806
868-- | Relational negation
807-- | Relational negation
869negateM :: Relation cols rows -> Relation cols rows
808negateM :: Relation cols rows -> Relation cols rows
809+negateM Empty = Empty
870−negateM (One (Nat p)) = One (Nat (negate p))
810+negateM (One (Nat 0)) = One (Nat 1)
811+negateM (One (Nat 1)) = One (Nat 0)
871−negateM (Join a b) = Join (negateM a) (negateM b)
812+negateM (Junc a b) = Junc (negateM a) (negateM b)
872−negateM (Fork a b) = Fork (negateM a) (negateM b)
813+negateM (Split a b) = Split (negateM a) (negateM b)
873
814
874-- | Relational addition
815-- | Relational addition
875orM :: Relation cols rows -> Relation cols rows -> Relation cols rows
816orM :: Relation cols rows -> Relation cols rows -> Relation cols rows
817+orM Empty Empty = Empty
876−orM (One a) (One b) = One (fromBool (toBool a || toBool b))
818+orM (One a) (One b) = One (fromBool (toBool a || toBool b))
877−orM (Join a b) (Join c d) = Join (orM a c) (orM b d)
819+orM (Junc a b) (Junc c d) = Junc (orM a c) (orM b d)
878−orM (Fork a b) (Fork c d) = Fork (orM a c) (orM b d)
820+orM (Split a b) (Split c d) = Split (orM a c) (orM b d)
879−orM x@(Fork _ _) y@(Join _ _) = orM x (abideJF y)
821+orM x@(Split _ _) y@(Junc _ _) = orM x (abideJS y)
880−orM x@(Join _ _) y@(Fork _ _) = orM (abideJF x) y
822+orM x@(Junc _ _) y@(Split _ _) = orM (abideJS x) y
881
823
882-- | Relational multiplication
824-- | Relational multiplication
883andM :: Relation cols rows -> Relation cols rows -> Relation cols rows
825andM :: Relation cols rows -> Relation cols rows -> Relation cols rows
826+andM Empty Empty = Empty
884−andM (One a) (One b) = One (fromBool (toBool a && toBool b))
827+andM (One a) (One b) = One (fromBool (toBool a && toBool b))
885−andM (Join a b) (Join c d) = Join (andM a c) (andM b d)
828+andM (Junc a b) (Junc c d) = Junc (andM a c) (andM b d)
886−andM (Fork a b) (Fork c d) = Fork (andM a c) (andM b d)
829+andM (Split a b) (Split c d) = Split (andM a c) (andM b d)
887−andM x@(Fork _ _) y@(Join _ _) = andM x (abideJF y)
830+andM x@(Split _ _) y@(Junc _ _) = andM x (abideJS y)
888−andM x@(Join _ _) y@(Fork _ _) = andM (abideJF x) y
831+andM x@(Junc _ _) y@(Split _ _) = andM (abideJS x) y
889
832
890-- | Relational subtraction
833-- | Relational subtraction
891subM :: Relation cols rows -> Relation cols rows -> Relation cols rows
834subM :: Relation cols rows -> Relation cols rows -> Relation cols rows
835+subM Empty Empty = Empty
892−subM (One a) (One b) = if a - b < nat 0 then One (nat 0) else One (a - b)
836+subM (One a) (One b) = if a - b < nat 0 then One (nat 0) else One (a - b)
893−subM (Join a b) (Join c d) = Join (subM a c) (subM b d)
837+subM (Junc a b) (Junc c d) = Junc (subM a c) (subM b d)
894−subM (Fork a b) (Fork c d) = Fork (subM a c) (subM b d)
838+subM (Split a b) (Split c d) = Split (subM a c) (subM b d)
895−subM x@(Fork _ _) y@(Join _ _) = subM x (abideJF y)
839+subM x@(Split _ _) y@(Junc _ _) = subM x (abideJS y)
896−subM x@(Join _ _) y@(Fork _ _) = subM (abideJF x) y
840+subM x@(Junc _ _) y@(Split _ _) = subM (abideJS x) y
897
841
898-- | Matrix relational composition.
842-- | Matrix relational composition.
899compRel :: Relation cr rows -> Relation cols cr -> Relation cols rows
843compRel :: Relation cr rows -> Relation cols cr -> Relation cols rows
844+compRel Empty Empty = Empty
900−compRel (One a) (One b) = One (fromBool (toBool a && toBool b))
845+compRel (One a) (One b) = One (fromBool (toBool a && toBool b))
901−compRel (Join a b) (Fork c d) = orM (compRel a c) (compRel b d) -- Divide-and-conquer law
846+compRel (Junc a b) (Split c d) = orM (compRel a c) (compRel b d) -- Divide-and-conquer law
902−compRel (Fork a b) c = Fork (compRel a c) (compRel b c) -- Fork fusion law
847+compRel (Split a b) c = Split (compRel a c) (compRel b c) -- Split fusion law
903−compRel c (Join a b) = Join (compRel c a) (compRel c b) -- Join fusion law
848+compRel c (Junc a b) = Junc (compRel c a) (compRel c b) -- Junc fusion law
904
849
905-- | Matrix relational right division
850-- | Matrix relational right division
906divR :: Relation b c -> Relation b a -> Relation a c
851divR :: Relation b c -> Relation b a -> Relation a c
852+divR Empty Empty = Empty
907divR (One a) (One b) = One (fromBool (not (toBool b) || toBool a)) -- b implies a
853divR (One a) (One b) = One (fromBool (not (toBool b) || toBool a)) -- b implies a
908−divR (Join a b) (Join c d) = andM (divR a c) (divR b d)
854+divR (Junc a b) (Junc c d) = andM (divR a c) (divR b d)
909−divR (Fork a b) c = Fork (divR a c) (divR b c)
855+divR (Split a b) c = Split (divR a c) (divR b c)
910−divR c (Fork a b) = Join (divR c a) (divR c b)
856+divR c (Split a b) = Junc (divR c a) (divR c b)
911
857
912-- | Matrix relational left division
858-- | Matrix relational left division
913divL :: Relation c b -> Relation a b -> Relation a c
859divL :: Relation c b -> Relation a b -> Relation a c
@@ -923,52 +869,97 @@ divS s r = divL r s `intersection` divR (tr r) (tr s)
923--
869--
924-- NOTE: Be careful to not ask for a relation bigger than the cardinality of
870-- NOTE: Be careful to not ask for a relation bigger than the cardinality of
925-- types @a@ or @b@ allows.
871-- types @a@ or @b@ allows.
926−fromFRel' ::
872+fromFRel ::
927 forall a b cols rows.
873 forall a b cols rows.
928− ( Liftable Boolean a b,
874+ ( Bounded a,
929− CountableDims cols rows,
875+ Bounded b,
876+ Enum a,
877+ Enum b,
878+ Eq b,
879+ KnownNat (Count cols),
880+ KnownNat (Count rows),
930− FL rows cols
881+ FromLists (Natural 0 1) rows cols
931 ) =>
882 ) =>
932 (a -> b) ->
883 (a -> b) ->
933 Relation cols rows
884 Relation cols rows
934−fromFRel' = fromF'
885+fromFRel f =
886+ let minA = minBound @a
887+ maxA = maxBound @a
888+ minB = minBound @b
889+ maxB = maxBound @b
890+ ccols = fromInteger $ natVal (Proxy :: Proxy (Count cols))
891+ rrows = fromInteger $ natVal (Proxy :: Proxy (Count rows))
892+ elementsA = take ccols [minA .. maxA]
893+ elementsB = take rrows [minB .. maxB]
894+ combinations = (,) <$> elementsA <*> elementsB
895+ combAp = map snd . sort . map (\(a, b) -> if f a == b
896+ then ((fromEnum a, fromEnum b), nat 1)
897+ else ((fromEnum a, fromEnum b), nat 0)) $ combinations
898+ mList = buildList combAp rrows
899+ in tr $ fromLists mList
900+ where
901+ buildList [] _ = []
902+ buildList l r = take r l : buildList (drop r l) r
935
903
936-- | Lifts functions to relations with dimensions matching @a@ and @b@
904-- | Lifts functions to relations with dimensions matching @a@ and @b@
937-- cardinality's.
905-- cardinality's.
938−fromFRel ::
906+fromFRel' ::
939 forall a b.
907 forall a b.
940− ( Liftable Boolean a b,
908+ ( Bounded a,
941− CountableDimsN a b,
909+ Bounded b,
942− FLN b a
910+ Enum a,
911+ Enum b,
912+ Eq b,
913+ KnownNat (Count (Normalize a)),
914+ KnownNat (Count (Normalize b)),
915+ FromLists (Natural 0 1) (Normalize b) (Normalize a)
943 ) =>
916 ) =>
944 (a -> b) ->
917 (a -> b) ->
945 Relation (Normalize a) (Normalize b)
918 Relation (Normalize a) (Normalize b)
946−fromFRel = fromFRel'
919+fromFRel' f =
920+ let minA = minBound @a
921+ maxA = maxBound @a
922+ minB = minBound @b
923+ maxB = maxBound @b
924+ ccols = fromInteger $ natVal (Proxy :: Proxy (Count (Normalize a)))
925+ rrows = fromInteger $ natVal (Proxy :: Proxy (Count (Normalize b)))
926+ elementsA = take ccols [minA .. maxA]
927+ elementsB = take rrows [minB .. maxB]
928+ combinations = (,) <$> elementsA <*> elementsB
929+ combAp = map snd . sort . map (\(a, b) -> if f a == b
930+ then ((fromEnum a, fromEnum b), nat 1)
931+ else ((fromEnum a, fromEnum b), nat 0)) $ combinations
932+ mList = buildList combAp rrows
933+ in tr $ fromLists mList
934+ where
935+ buildList [] _ = []
936+ buildList l r = take r l : buildList (drop r l) r
947
937
948-- | Lifts a relation function to a Boolean Matrix
938-- | Lifts a relation function to a Boolean Matrix
949−toRel ::
939+toRel ::
950 forall a b.
940 forall a b.
951 ( Bounded a,
941 ( Bounded a,
952 Bounded b,
942 Bounded b,
953 Enum a,
943 Enum a,
954 Enum b,
944 Enum b,
955 Eq b,
945 Eq b,
956− CountableDims a b,
946+ KnownNat (Count (Normalize a)),
957− FLN b a
947+ KnownNat (Count (Normalize b)),
948+ FromLists (Natural 0 1) (Normalize b) (Normalize a)
958− )
949+ )
959 => (a -> b -> Bool) -> Relation (Normalize a) (Normalize b)
950 => (a -> b -> Bool) -> Relation (Normalize a) (Normalize b)
960toRel f =
951toRel f =
961 let minA = minBound @a
952 let minA = minBound @a
962 maxA = maxBound @a
953 maxA = maxBound @a
963 minB = minBound @b
954 minB = minBound @b
964 maxB = maxBound @b
955 maxB = maxBound @b
965− ccols = fromInteger $ natVal (Proxy :: Proxy (Count a))
956+ ccols = fromInteger $ natVal (Proxy :: Proxy (Count (Normalize a)))
966− rrows = fromInteger $ natVal (Proxy :: Proxy (Count b))
957+ rrows = fromInteger $ natVal (Proxy :: Proxy (Count (Normalize b)))
967 elementsA = take ccols [minA .. maxA]
958 elementsA = take ccols [minA .. maxA]
968 elementsB = take rrows [minB .. maxB]
959 elementsB = take rrows [minB .. maxB]
969 combinations = (,) <$> elementsA <*> elementsB
960 combinations = (,) <$> elementsA <*> elementsB
970− combAp = map snd . sort . map (\(a, b) -> if uncurry f (a, b)
961+ combAp = map snd . sort . map (\(a, b) -> if uncurry f (a, b)
971− then ((fromEnum a, fromEnum b), nat 1)
962+ then ((fromEnum a, fromEnum b), nat 1)
972 else ((fromEnum a, fromEnum b), nat 0)) $ combinations
963 else ((fromEnum a, fromEnum b), nat 0)) $ combinations
973 mList = buildList combAp rrows
964 mList = buildList combAp rrows
974 in tr $ fromLists mList
965 in tr $ fromLists mList
src/LAoP/Matrix/Nat.hs+187−194
@@ -1,4 +1,3 @@
1−{-# LANGUAGE ConstraintKinds #-}
2{-# LANGUAGE AllowAmbiguousTypes #-}
1{-# LANGUAGE AllowAmbiguousTypes #-}
3{-# LANGUAGE DataKinds #-}
2{-# LANGUAGE DataKinds #-}
4{-# LANGUAGE DerivingVia #-}
3{-# LANGUAGE DerivingVia #-}
@@ -54,22 +53,11 @@ module LAoP.Matrix.Nat
54 -- * Type safe matrix representation
53 -- * Type safe matrix representation
55 Matrix (..),
54 Matrix (..),
56
55
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−
69 -- * Primitives
56 -- * Primitives
57+ empty,
70 one,
58 one,
71− join,
59+ junc,
72− fork,
60+ split,
73
61
74 -- * Auxiliary type families
62 -- * Auxiliary type families
75 I.FromNat,
63 I.FromNat,
@@ -77,11 +65,11 @@ module LAoP.Matrix.Nat
77 I.Normalize,
65 I.Normalize,
78
66
79 -- * Matrix construction and conversion
67 -- * Matrix construction and conversion
80− I.FL,
68+ I.FromLists,
81 fromLists,
69 fromLists,
82 toLists,
70 toLists,
83 toList,
71 toList,
84− matrixBuilder',
72+ matrixBuilder,
85 row,
73 row,
86 col,
74 col,
87 zeros,
75 zeros,
@@ -97,10 +85,6 @@ module LAoP.Matrix.Nat
97 -- ** Matrix Transposition
85 -- ** Matrix Transposition
98 tr,
86 tr,
99
87
100− -- ** Scalar multiplication/division of matrices
101− (.|),
102− (./),
103−
104 -- ** Selective operator
88 -- ** Selective operator
105 select,
89 select,
106
90
@@ -108,19 +92,16 @@ module LAoP.Matrix.Nat
108 cond,
92 cond,
109
93
110 -- ** Matrix "abiding"
94 -- ** Matrix "abiding"
111− abideJF,
95+ abideJS,
112− abideFJ,
96+ abideSJ,
113−
114− -- ** Zip Matrices
115− zipWithM,
116
97
117 -- * Biproduct approach
98 -- * Biproduct approach
118− -- ** Fork
99+ -- ** Split
119 (===),
100 (===),
120 -- *** Projections
101 -- *** Projections
121 p1,
102 p1,
122 p2,
103 p2,
123− -- ** Join
104+ -- ** Junc
124 (|||),
105 (|||),
125 -- *** Injections
106 -- *** Injections
126 i1,
107 i1,
@@ -134,11 +115,11 @@ module LAoP.Matrix.Nat
134 -- | Note that given the restrictions imposed it is not possible to
115 -- | Note that given the restrictions imposed it is not possible to
135 -- implement the standard type classes present in standard Haskell.
116 -- implement the standard type classes present in standard Haskell.
136 -- *** Matrix pairing projections
117 -- *** Matrix pairing projections
137− fstM,
118+ kp1,
138− sndM,
119+ kp2,
139
120
140 -- *** Matrix pairing
121 -- *** Matrix pairing
141− kr,
122+ khatri,
142
123
143 -- * Matrix composition and lifting
124 -- * Matrix composition and lifting
144
125
@@ -146,10 +127,10 @@ module LAoP.Matrix.Nat
146
127
147 -- | Note that given the restrictions imposed it is not possible to
128 -- | Note that given the restrictions imposed it is not possible to
148 -- implement the standard type classes present in standard Haskell.
129 -- implement the standard type classes present in standard Haskell.
149− iden,
130+ identity,
150 comp,
131 comp,
151− fromF',
152 fromF,
132 fromF,
133+ fromF',
153
134
154 -- * Matrix printing
135 -- * Matrix printing
155 pretty,
136 pretty,
@@ -160,95 +141,107 @@ where
160import Data.Proxy
141import Data.Proxy
161import GHC.TypeLits
142import GHC.TypeLits
162import Control.DeepSeq
143import Control.DeepSeq
144+import qualified Control.Category as C
163import qualified LAoP.Matrix.Internal as I
145import qualified LAoP.Matrix.Internal as I
164
146
165newtype Matrix e (cols :: Nat) (rows :: Nat) = M (I.Matrix e (I.FromNat cols) (I.FromNat rows))
147newtype Matrix e (cols :: Nat) (rows :: Nat) = M (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))
148 deriving (Show, Num, Eq, Ord, NFData) via (I.Matrix e (I.FromNat cols) (I.FromNat rows))
167
149
168−-- | Constraint type synonyms to keep the type signatures less convoluted
150+-- | It isn't possible to implement the 'id' function so it's
169−type Countable a = KnownNat (I.Count a)
151+-- implementation is 'undefined'. However 'comp' can be and this partial
170−type CountableDims a b = (Countable a, Countable b)
152+-- class implementation exists just to make the code more readable.
171−type CountableN a = KnownNat (I.Count (I.FromNat a))
153+--
172−type CountableNz a = KnownNat (I.Count (I.Normalize a))
154+-- Please use 'identity' instead.
173−type CountableDimsN a b = (CountableN a, CountableN b)
155+instance (Num e) => C.Category (Matrix e) where
174−type FLN e a b = I.FL (I.FromNat a) (I.FromNat b)
156+ id = undefined
175−type FLNz e a b = I.FL (I.Normalize a) (I.Normalize b)
157+ (.) = comp
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))
179
158
180-- Primitives
159-- Primitives
181
160
161+empty :: Matrix e 0 0
162+empty = M I.Empty
163+
182one :: e -> Matrix e 1 1
164one :: e -> Matrix e 1 1
183one = M . I.One
165one = M . I.One
184
166
185−join ::
167+junc ::
186− (TrivialE a b) =>
168+ (I.FromNat cols3 ~ Either (I.FromNat cols1) (I.FromNat cols2)) =>
187− Matrix e a rows ->
169+ Matrix e cols1 rows ->
188− Matrix e b rows ->
170+ Matrix e cols2 rows ->
189− Matrix e (a + b) rows
171+ Matrix e cols3 rows
190−join (M a) (M b) = M (I.Join a b)
172+junc (M a) (M b) = M (I.Junc a b)
191
173
192infixl 3 |||
174infixl 3 |||
193(|||) ::
175(|||) ::
194− (TrivialE a b) =>
176+ (I.FromNat cols3 ~ Either (I.FromNat cols1) (I.FromNat cols2)) =>
195− Matrix e a rows ->
177+ Matrix e cols1 rows ->
196− Matrix e b rows ->
178+ Matrix e cols2 rows ->
197− Matrix e (a + b) rows
179+ Matrix e cols3 rows
198−(|||) = join
180+(|||) = junc
199−
181+
200−fork ::
182+split ::
201− (TrivialE a b) =>
183+ (I.FromNat rows3 ~ Either (I.FromNat rows1) (I.FromNat rows2)) =>
202− Matrix e cols a ->
184+ Matrix e cols rows1 ->
203− Matrix e cols b ->
185+ Matrix e cols rows2 ->
204− Matrix e cols (a + b)
186+ Matrix e cols rows3
205−fork (M a) (M b) = M (I.Fork a b)
187+split (M a) (M b) = M (I.Split a b)
206
188
207infixl 2 ===
189infixl 2 ===
208(===) ::
190(===) ::
209− (TrivialE a b) =>
191+ (I.FromNat rows3 ~ Either (I.FromNat rows1) (I.FromNat rows2)) =>
210− Matrix e cols a ->
192+ Matrix e cols rows1 ->
211− Matrix e cols b ->
193+ Matrix e cols rows2 ->
212− Matrix e cols (a + b)
194+ Matrix e cols rows3
213−(===) = fork
195+(===) = split
214
196
215-- Construction
197-- Construction
216
198
217−fromLists :: (FLN e cols rows) => [[e]] -> Matrix e cols rows
199+fromLists :: (I.FromLists e (I.FromNat cols) (I.FromNat rows)) => [[e]] -> Matrix e cols rows
218fromLists = M . I.fromLists
200fromLists = M . I.fromLists
219
201
220−-- | Matrix builder function. Constructs a matrix provided with
221−-- a construction function that operates with indices.
222−matrixBuilder' ::
202+matrixBuilder ::
223− (FLN e cols rows, CountableN cols, CountableN rows)
203+ (I.FromLists e (I.FromNat cols) (I.FromNat rows), KnownNat (I.Count (I.FromNat cols)), KnownNat (I.Count (I.FromNat rows))) =>
204+ ((Int, Int) -> e) ->
224− => ((Int, Int) -> e) -> Matrix e cols rows
205+ Matrix e cols rows
225−matrixBuilder' = M . I.matrixBuilder'
206+matrixBuilder = M . I.matrixBuilder
226
207
227−col :: (I.FL () (I.FromNat rows)) => [e] -> Matrix e 1 rows
208+col :: (I.FromLists e () (I.FromNat rows)) => [e] -> Matrix e 1 rows
228col = M . I.col
209col = M . I.col
229
210
230−row :: (I.FL (I.FromNat cols) ()) => [e] -> Matrix e cols 1
211+row :: (I.FromLists e (I.FromNat cols) ()) => [e] -> Matrix e cols 1
231row = M . I.row
212row = M . I.row
232
213
233−fromF' ::
214+fromF ::
234− ( Liftable e a b,
215+ ( Bounded a,
235− CountableN cols,
216+ Bounded b,
236− CountableN rows,
217+ Enum a,
237− FLN e rows cols
218+ Enum b,
219+ Eq b,
220+ Num e,
221+ Ord e,
222+ KnownNat (I.Count (I.FromNat cols)),
223+ KnownNat (I.Count (I.FromNat rows)),
224+ I.FromLists e (I.FromNat rows) (I.FromNat cols)
238 ) =>
225 ) =>
239 (a -> b) ->
226 (a -> b) ->
240 Matrix e cols rows
227 Matrix e cols rows
241−fromF' = M . I.fromF'
228+fromF = M . I.fromF
242
229
243−fromF ::
230+fromF' ::
244− ( Liftable e a b,
231+ ( Bounded a,
245− CountableNz a,
232+ Bounded b,
246− CountableNz b,
233+ Enum a,
247− FLNz e b a
234+ Enum b,
235+ Eq b,
236+ Num e,
237+ Ord e,
238+ KnownNat (I.Count (I.Normalize a)),
239+ KnownNat (I.Count (I.Normalize b)),
240+ I.FromLists e (I.Normalize b) (I.Normalize a)
248 ) =>
241 ) =>
249 (a -> b) ->
242 (a -> b) ->
250 Matrix e (I.Count a) (I.Count b)
243 Matrix e (I.Count a) (I.Count b)
251−fromF = undefined -- M . I.fromF
244+fromF' = M . I.fromF'
252
245
253-- Conversion
246-- Conversion
254
247
@@ -261,21 +254,21 @@ toList (M m) = I.toList m
261-- Zeros Matrix
254-- Zeros Matrix
262
255
263zeros ::
256zeros ::
264− (Num e, FLN e cols rows, CountableN cols, CountableN rows) =>
257+ (Num e, I.FromLists e (I.FromNat cols) (I.FromNat rows), KnownNat (I.Count (I.FromNat cols)), KnownNat (I.Count (I.FromNat rows))) =>
265 Matrix e cols rows
258 Matrix e cols rows
266zeros = M I.zeros
259zeros = M I.zeros
267
260
268-- Ones Matrix
261-- Ones Matrix
269
262
270ones ::
263ones ::
271− (Num e, FLN e cols rows, CountableN cols, CountableN rows) =>
264+ (Num e, I.FromLists e (I.FromNat cols) (I.FromNat rows), KnownNat (I.Count (I.FromNat cols)), KnownNat (I.Count (I.FromNat rows))) =>
272 Matrix e cols rows
265 Matrix e cols rows
273ones = M I.ones
266ones = M I.ones
274
267
275-- Const Matrix
268-- Const Matrix
276
269
277constant ::
270constant ::
278− (Num e, FLN e cols rows, CountableN cols, CountableN rows) =>
271+ (Num e, I.FromLists e (I.FromNat cols) (I.FromNat rows), KnownNat (I.Count (I.FromNat cols)), KnownNat (I.Count (I.FromNat rows))) =>
279 e ->
272 e ->
280 Matrix e cols rows
273 Matrix e cols rows
281constant = M . I.constant
274constant = M . I.constant
@@ -284,52 +277,40 @@ constant = M . I.constant
284
277
285bang ::
278bang ::
286 forall e cols.
279 forall e cols.
287− (Num e, Enum e, I.FL (I.FromNat cols) (), CountableN cols) =>
280+ (Num e, Enum e, I.FromLists e (I.FromNat cols) (), KnownNat (I.Count (I.FromNat cols))) =>
288 Matrix e cols 1
281 Matrix e cols 1
289bang = M I.bang
282bang = M I.bang
290
283
291−-- iden Matrix
284+-- Identity Matrix
292
285
293−iden ::
286+identity ::
294− (Num e, FLN e cols cols, CountableN cols) =>
287+ (Num e, I.FromLists e (I.FromNat cols) (I.FromNat cols), KnownNat (I.Count (I.FromNat cols))) =>
295 Matrix e cols cols
288 Matrix e cols cols
296−iden = M I.iden
289+identity = M I.identity
297
290
298-- Matrix composition (MMM)
291-- Matrix composition (MMM)
299
292
300comp :: (Num e) => Matrix e cr rows -> Matrix e cols cr -> Matrix e cols rows
293comp :: (Num e) => Matrix e cr rows -> Matrix e cols cr -> Matrix e cols rows
301comp (M a) (M b) = M (I.comp a b)
294comp (M a) (M b) = M (I.comp a b)
302
295
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−
317p1 ::
296p1 ::
318 ( Num e,
297 ( Num e,
319− CountableDimsN n m,
298+ KnownNat (I.Count (I.FromNat n)),
320− FLN e n m,
299+ KnownNat (I.Count (I.FromNat m)),
321− FLN e m m,
300+ I.FromLists e (I.FromNat n) (I.FromNat m),
322− TrivialE m n
301+ I.FromLists e (I.FromNat m) (I.FromNat m),
302+ I.FromNat (m + n) ~ Either (I.FromNat m) (I.FromNat n)
323 ) =>
303 ) =>
324 Matrix e (m + n) m
304 Matrix e (m + n) m
325p1 = M I.p1
305p1 = M I.p1
326
306
327p2 ::
307p2 ::
328 ( Num e,
308 ( Num e,
329− CountableDimsN n m,
309+ KnownNat (I.Count (I.FromNat n)),
330− FLN e m n,
310+ KnownNat (I.Count (I.FromNat m)),
331− FLN e n n,
311+ I.FromLists e (I.FromNat m) (I.FromNat n),
332− TrivialE m n
312+ I.FromLists e (I.FromNat n) (I.FromNat n),
313+ I.FromNat (m + n) ~ Either (I.FromNat m) (I.FromNat n)
333 ) =>
314 ) =>
334 Matrix e (m + n) n
315 Matrix e (m + n) n
335p2 = M I.p2
316p2 = M I.p2
@@ -338,125 +319,138 @@ p2 = M I.p2
338
319
339i1 ::
320i1 ::
340 ( Num e,
321 ( Num e,
341− CountableDimsN n rows,
322+ KnownNat (I.Count (I.FromNat n)),
342− FLN e n rows,
323+ KnownNat (I.Count (I.FromNat rows)),
343− FLN e rows rows,
324+ I.FromLists e (I.FromNat n) (I.FromNat rows),
344− TrivialE rows n
325+ I.FromLists e (I.FromNat rows) (I.FromNat rows),
326+ I.FromNat (rows + n) ~ Either (I.FromNat rows) (I.FromNat n)
345 ) =>
327 ) =>
346 Matrix e rows (rows + n)
328 Matrix e rows (rows + n)
347i1 = tr p1
329i1 = tr p1
348
330
349i2 ::
331i2 ::
350 ( Num e,
332 ( Num e,
351− CountableDimsN rows m,
333+ KnownNat (I.Count (I.FromNat rows)),
352− FLN e m rows,
334+ KnownNat (I.Count (I.FromNat m)),
353− FLN e rows rows,
335+ I.FromLists e (I.FromNat m) (I.FromNat rows),
354− TrivialE m rows
336+ I.FromLists e (I.FromNat rows) (I.FromNat rows),
337+ I.FromNat (m + rows) ~ Either (I.FromNat m) (I.FromNat rows)
355 ) =>
338 ) =>
356 Matrix e rows (m + rows)
339 Matrix e rows (m + rows)
357i2 = tr p2
340i2 = tr p2
358
341
359-- Dimensions
342-- Dimensions
360
343
361−rows :: (CountableN rows) => Matrix e cols rows -> Int
344+rows :: (KnownNat (I.Count (I.FromNat rows))) => Matrix e cols rows -> Int
362rows (M m) = I.rows m
345rows (M m) = I.rows m
363
346
364−columns :: (CountableN cols) => Matrix e cols rows -> Int
347+columns :: (KnownNat (I.Count (I.FromNat cols))) => Matrix e cols rows -> Int
365columns (M m) = I.columns m
348columns (M m) = I.columns m
366
349
350+-- Coproduct Bifunctor
351+
367infixl 5 -|-
352infixl 5 -|-
368
353
369−-- | Coproduct Bifunctor (Direct sum)
370(-|-) ::
354(-|-) ::
371 ( Num e,
355 ( Num e,
372− CountableDimsN j k,
356+ KnownNat (I.Count (I.FromNat j)),
373− FLN e k k,
357+ KnownNat (I.Count (I.FromNat k)),
374− FLN e j k,
358+ I.FromLists e (I.FromNat k) (I.FromNat k),
375− FLN e k j,
359+ I.FromLists e (I.FromNat j) (I.FromNat k),
376− FLN e j j,
360+ I.FromLists e (I.FromNat k) (I.FromNat j),
377− TrivialE n m,
361+ I.FromLists e (I.FromNat j) (I.FromNat j),
378− TrivialE k j
362+ I.FromNat (n + m) ~ Either (I.FromNat n) (I.FromNat m),
363+ I.FromNat (k + j) ~ Either (I.FromNat k) (I.FromNat j)
379 ) =>
364 ) =>
380 Matrix e n k ->
365 Matrix e n k ->
381 Matrix e m j ->
366 Matrix e m j ->
382 Matrix e (n + m) (k + j)
367 Matrix e (n + m) (k + j)
383(-|-) (M a) (M b) = M ((I.-|-) a b)
368(-|-) (M a) (M b) = M ((I.-|-) a b)
384
369
385−-- | Khatri Rao Product first projection
370+-- Khatri Rao Product and projections
386−fstM ::
371+
372+kp1 ::
387 forall e m k .
373 forall e m k .
388 ( Num e,
374 ( Num e,
389− CountableDimsN m k,
375+ KnownNat (I.Count (I.FromNat m)),
390− CountableN (m * k),
376+ KnownNat (I.Count (I.FromNat k)),
391− FLN e (m * k) m,
377+ KnownNat (I.Count (I.FromNat (m * k))),
392− TrivialP m k
378+ I.FromLists e (I.FromNat (m * k)) (I.FromNat m),
379+ I.FromNat (m * k) ~ I.FromNat (I.Count (I.FromNat m) * I.Count (I.FromNat k))
393 ) => Matrix e (m * k) m
380 ) => Matrix e (m * k) m
394−fstM = M (I.fstM @e @(I.FromNat m) @(I.FromNat k))
381+kp1 = M (I.kp1 @e @(I.FromNat m) @(I.FromNat k))
395
382
396−-- | Khatri Rao Product second projection
383+kp2 ::
397−sndM ::
398 forall e m k.
384 forall e m k.
399 ( Num e,
385 ( Num e,
400− CountableDimsN k m,
386+ KnownNat (I.Count (I.FromNat k)),
401− FLN e (m * k) k,
387+ I.FromLists e (I.FromNat (m * k)) (I.FromNat k),
402− CountableN (m * k),
388+ KnownNat (I.Count (I.FromNat m)),
403− TrivialP m k
389+ KnownNat (I.Count (I.FromNat (m * k))),
390+ I.FromNat (m * k) ~ I.FromNat (I.Count (I.FromNat m) * I.Count (I.FromNat k))
404 ) => Matrix e (m * k) k
391 ) => Matrix e (m * k) k
405−sndM = M (I.sndM @e @(I.FromNat m) @(I.FromNat k))
392+kp2 = M (I.kp2 @e @(I.FromNat m) @(I.FromNat k))
406
393
407−-- | Khatri Rao Product
394+khatri ::
408−kr ::
409 forall e cols a b.
395 forall e cols a b.
410 ( Num e,
396 ( Num e,
411− CountableDimsN a b,
397+ KnownNat (I.Count (I.FromNat a)),
412− CountableN (a * b),
398+ KnownNat (I.Count (I.FromNat b)),
413− FLN e (a * b) a,
399+ KnownNat (I.Count (I.FromNat (a * b))),
414− FLN e (a * b) b,
400+ I.FromLists e (I.FromNat (a * b)) (I.FromNat a),
415− TrivialP a b
401+ I.FromLists e (I.FromNat (a * b)) (I.FromNat b),
402+ I.FromNat (a * b) ~ I.FromNat (I.Count (I.FromNat a) * I.Count (I.FromNat b))
416 ) => Matrix e cols a -> Matrix e cols b -> Matrix e cols (a * b)
403 ) => Matrix e cols a -> Matrix e cols b -> Matrix e cols (a * b)
417−kr a b =
404+khatri a b =
418− let fstM' = fstM @e @a @b
405+ let kp1' = kp1 @e @a @b
419− sndM' = sndM @e @a @b
406+ kp2' = kp2 @e @a @b
420− in comp (tr fstM') a * comp (tr sndM') b
407+ in comp (tr kp1') a * comp (tr kp2') b
408+
409+-- Product Bifunctor (Kronecker)
421
410
422−-- | Product Bifunctor (Kronecker)
423infixl 4 ><
411infixl 4 ><
424
412
425(><) ::
413(><) ::
426 forall e m p n q.
414 forall e m p n q.
427 ( Num e,
415 ( Num e,
428− CountableDimsN m n,
416+ KnownNat (I.Count (I.FromNat m)),
429− CountableDimsN p q,
417+ KnownNat (I.Count (I.FromNat n)),
430− CountableDimsN (m * n) (p * q),
418+ KnownNat (I.Count (I.FromNat p)),
431− FLN e (m * n) m,
419+ KnownNat (I.Count (I.FromNat q)),
432− FLN e (m * n) n,
420+ KnownNat (I.Count (I.FromNat (m * n))),
433− FLN e (p * q) p,
421+ KnownNat (I.Count (I.FromNat (p * q))),
434− FLN e (p * q) q,
422+ I.FromLists e (I.FromNat (m * n)) (I.FromNat m),
435− TrivialP m n,
423+ I.FromLists e (I.FromNat (m * n)) (I.FromNat n),
436− TrivialP p q
424+ I.FromLists e (I.FromNat (p * q)) (I.FromNat p),
425+ I.FromLists e (I.FromNat (p * q)) (I.FromNat q),
426+ I.FromNat (m * n) ~ I.FromNat (I.Count (I.FromNat m) * I.Count (I.FromNat n)),
427+ I.FromNat (p * q) ~ I.FromNat (I.Count (I.FromNat p) * I.Count (I.FromNat q))
437 ) => Matrix e m p -> Matrix e n q -> Matrix e (m * n) (p * q)
428 ) => Matrix e m p -> Matrix e n q -> Matrix e (m * n) (p * q)
438(><) a b =
429(><) a b =
439− let fstM' = fstM @e @m @n
430+ let kp1' = kp1 @e @m @n
440− sndM' = sndM @e @m @n
431+ kp2' = kp2 @e @m @n
441− in kr (comp a fstM') (comp b sndM')
432+ in khatri (comp a kp1') (comp b kp2')
433+
434+-- Matrix abide Junc Split
442
435
443−-- | Matrix abide Join Fork
444−abideJF :: Matrix e cols rows -> Matrix e cols rows
436+abideJS :: Matrix e cols rows -> Matrix e cols rows
445−abideJF (M m) = M (I.abideJF m)
437+abideJS (M m) = M (I.abideJS m)
446
438
447−-- | Matrix abide Fork Join
439+-- Matrix abide Split Junc
440+
448−abideFJ :: Matrix e cols rows -> Matrix e cols rows
441+abideSJ :: Matrix e cols rows -> Matrix e cols rows
449−abideFJ (M m) = M (I.abideFJ m)
442+abideSJ (M m) = M (I.abideSJ m)
443+
444+-- Matrix transposition
450
445
451−-- | Matrix transposition
452tr :: Matrix e cols rows -> Matrix e rows cols
446tr :: Matrix e cols rows -> Matrix e rows cols
453tr (M m) = M (I.tr m)
447tr (M m) = M (I.tr m)
454
448
455-- Selective 'select' operator
449-- Selective 'select' operator
456select ::
450select ::
457 ( Num e,
451 ( Num e,
458− FLN e rows1 rows1,
452+ I.FromLists e (I.FromNat rows1) (I.FromNat rows1),
459− CountableN rows1,
453+ KnownNat (I.Count (I.FromNat rows1)),
460 I.FromNat rows2 ~ I.FromNat rows1,
454 I.FromNat rows2 ~ I.FromNat rows1,
461 I.FromNat cols1 ~ I.FromNat cols2,
455 I.FromNat cols1 ~ I.FromNat cols2,
462 I.FromNat rows3 ~ Either (I.FromNat cols3) (I.FromNat rows1)
456 I.FromNat rows3 ~ Either (I.FromNat cols3) (I.FromNat rows1)
@@ -467,11 +461,14 @@ select (M m) (M y) = M (I.select m y)
467
461
468cond ::
462cond ::
469 ( I.FromNat (I.Count (I.FromNat cols)) ~ I.FromNat cols,
463 ( I.FromNat (I.Count (I.FromNat cols)) ~ I.FromNat cols,
470− CountableN cols,
464+ KnownNat (I.Count (I.FromNat cols)),
471− I.FL () (I.FromNat cols),
465+ I.FromLists e () (I.FromNat cols),
472− I.FL (I.FromNat cols) (),
466+ I.FromLists e (I.FromNat cols) (),
473− FLN e cols cols,
467+ I.FromLists e (I.FromNat cols) (I.FromNat cols),
474− Liftable e a Bool
468+ Bounded a,
469+ Enum a,
470+ Num e,
471+ Ord e
475 )
472 )
476 =>
473 =>
477 (a -> Bool) -> Matrix e cols rows -> Matrix e cols rows -> Matrix e cols rows
474 (a -> Bool) -> Matrix e cols rows -> Matrix e cols rows -> Matrix e cols rows
@@ -479,12 +476,8 @@ cond p (M a) (M b) = M (I.cond p a b)
479
476
480-- Pretty print
477-- Pretty print
481
478
482−pretty :: (CountableDimsN cols rows, Show e) => Matrix e cols rows -> String
479+pretty :: (KnownNat (I.Count (I.FromNat cols)), Show e) => Matrix e cols rows -> String
483pretty (M m) = I.pretty m
480pretty (M m) = I.pretty m
484
481
485−prettyPrint :: (CountableDimsN cols rows, Show e) => Matrix e cols rows -> IO ()
482+prettyPrint :: (KnownNat (I.Count (I.FromNat cols)), Show e) => Matrix e cols rows -> IO ()
486prettyPrint (M m) = I.prettyPrint m
483prettyPrint (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+240−283
@@ -1,11 +1,10 @@
1−{-# LANGUAGE ConstraintKinds #-}
2−{-# LANGUAGE TypeFamilies #-}
3{-# LANGUAGE AllowAmbiguousTypes #-}
1{-# LANGUAGE AllowAmbiguousTypes #-}
4{-# LANGUAGE DataKinds #-}
2{-# LANGUAGE DataKinds #-}
5{-# LANGUAGE DerivingVia #-}
3{-# LANGUAGE DerivingVia #-}
6{-# LANGUAGE FlexibleContexts #-}
4{-# LANGUAGE FlexibleContexts #-}
7{-# LANGUAGE FlexibleInstances #-}
5{-# LANGUAGE FlexibleInstances #-}
8{-# LANGUAGE GADTs #-}
6{-# LANGUAGE GADTs #-}
7+{-# LANGUAGE KindSignatures #-}
9{-# LANGUAGE MultiParamTypeClasses #-}
8{-# LANGUAGE MultiParamTypeClasses #-}
10{-# LANGUAGE NoStarIsType #-}
9{-# LANGUAGE NoStarIsType #-}
11{-# LANGUAGE RankNTypes #-}
10{-# LANGUAGE RankNTypes #-}
@@ -56,24 +55,15 @@ module LAoP.Matrix.Type
56 -- * Type safe matrix representation
55 -- * Type safe matrix representation
57 Matrix (..),
56 Matrix (..),
58
57
59− -- * Constraint type aliases
60− Countable,
61− CountableDims,
62− CountableN,
63− CountableDimsN,
64− FLN,
65− Liftable,
66− Trivial,
67− TrivialP,
68−
69 -- * Type aliases
58 -- * Type aliases
70 Zero,
59 Zero,
71 One,
60 One,
72
61
73 -- * Primitives
62 -- * Primitives
63+ empty,
74 one,
64 one,
75− join,
65+ junc,
76− fork,
66+ split,
77
67
78 -- * Auxiliary type families
68 -- * Auxiliary type families
79 I.FromNat,
69 I.FromNat,
@@ -85,27 +75,24 @@ module LAoP.Matrix.Type
85 fromLists,
75 fromLists,
86 toLists,
76 toLists,
87 toList,
77 toList,
88− matrixBuilder',
89 matrixBuilder,
78 matrixBuilder,
90 row,
79 row,
91 col,
80 col,
92 zeros,
81 zeros,
93 ones,
82 ones,
94 bang,
83 bang,
95− point,
96 constant,
84 constant,
97
85
98 -- * Functor instance equivalent function
86 -- * Functor instance equivalent function
99 fmapM,
87 fmapM,
100− bimapM,
101
88
102 -- * Applicative/Monoidal instance equivalent functions
89 -- * Applicative/Monoidal instance equivalent functions
103 unitM,
90 unitM,
104 multM,
91 multM,
105
92
106 -- * Selective equivalent instance function
93 -- * Selective equivalent instance function
107− selectM,
94+ selectM,
108−
95+
109 -- * Monad equivalent instance function
96 -- * Monad equivalent instance function
110 returnM,
97 returnM,
111 bindM,
98 bindM,
@@ -113,34 +100,25 @@ module LAoP.Matrix.Type
113 -- * Misc
100 -- * Misc
114 -- ** Get dimensions
101 -- ** Get dimensions
115 columns,
102 columns,
116− columns',
117 rows,
103 rows,
118− rows',
119
104
120 -- ** Matrix Transposition
105 -- ** Matrix Transposition
121 tr,
106 tr,
122
107
123− -- ** Scalar multiplication/division of matrices
124− (.|),
125− (./),
126−
127 -- ** McCarthy's Conditional
108 -- ** McCarthy's Conditional
128 cond,
109 cond,
129
110
130 -- ** Matrix "abiding"
111 -- ** Matrix "abiding"
131− abideJF,
112+ abideJS,
132− abideFJ,
113+ abideSJ,
133−
134− -- ** Zip Matrices
135− zipWithM,
136
114
137 -- * Biproduct approach
115 -- * Biproduct approach
138− -- ** Fork
116+ -- ** Split
139 (===),
117 (===),
140 -- *** Projections
118 -- *** Projections
141 p1,
119 p1,
142 p2,
120 p2,
143− -- ** Join
121+ -- ** Junc
144 (|||),
122 (|||),
145 -- *** Injections
123 -- *** Injections
146 i1,
124 i1,
@@ -154,11 +132,11 @@ module LAoP.Matrix.Type
154 -- | Note that given the restrictions imposed it is not possible to
132 -- | Note that given the restrictions imposed it is not possible to
155 -- implement the standard type classes present in standard Haskell.
133 -- implement the standard type classes present in standard Haskell.
156 -- *** Matrix pairing projections
134 -- *** Matrix pairing projections
157− fstM,
135+ kp1,
158− sndM,
136+ kp2,
159
137
160 -- *** Matrix pairing
138 -- *** Matrix pairing
161− kr,
139+ khatri,
162
140
163 -- * Matrix composition and lifting
141 -- * Matrix composition and lifting
164
142
@@ -166,10 +144,10 @@ module LAoP.Matrix.Type
166
144
167 -- | Note that given the restrictions imposed it is not possible to
145 -- | Note that given the restrictions imposed it is not possible to
168 -- implement the standard type classes present in standard Haskell.
146 -- implement the standard type classes present in standard Haskell.
169− iden,
147+ identity,
170 comp,
148 comp,
171− fromF',
172 fromF,
149 fromF,
150+ fromF',
173
151
174 -- * Relation
152 -- * Relation
175 toRel,
153 toRel,
@@ -183,44 +161,23 @@ where
183import Data.Void
161import Data.Void
184import Data.Proxy
162import Data.Proxy
185import Data.Kind
163import Data.Kind
186−import GHC.TypeLits
164+import GHC.TypeLits
187import Control.DeepSeq
165import Control.DeepSeq
188import LAoP.Utils
166import LAoP.Utils
167+import qualified Control.Category as C
189import qualified LAoP.Matrix.Internal as I
168import qualified LAoP.Matrix.Internal as I
190−import Prelude hiding (id, (.))
191
169
192newtype Matrix e (cols :: Type) (rows :: Type) = M (I.Matrix e (I.Normalize cols) (I.Normalize rows))
170newtype Matrix e (cols :: Type) (rows :: Type) = M (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))
171 deriving (Show, Num, Eq, Ord, NFData) via (I.Matrix e (I.Normalize cols) (I.Normalize rows))
194
172
195−-- | Constraint type synonyms to keep the type signatures less convoluted
196−type Countable a = KnownNat (I.Count a)
197−type CountableDims a b = (Countable a, Countable b)
198−type CountableN a = KnownNat (I.Count (I.Normalize a))
199−type CountableDimsN a b = (CountableN a, CountableN b)
200−type FLN a b = I.FromLists (I.Normalize a) (I.Normalize b)
201−type Liftable e a b = (Bounded a, Bounded b, Enum a, Enum b, Eq b, Num e, Ord e)
202−type Trivial a = I.Normalize (I.Normalize a) ~ I.Normalize (I.Normalize (I.Normalize a))
203−type Trivial2 a = I.Normalize a ~ I.Normalize (I.Normalize a)
204−type Trivial3 a = I.FromNat (I.Count (I.Normalize (I.Normalize a))) ~ I.Normalize (I.Normalize a)
205−type TrivialP a b = I.Normalize (a, b) ~ I.Normalize (I.Normalize a, I.Normalize b)
206−
207−-- | It is possible to implement a constrained version of the category type
173+-- | It isn't possible to implement the 'id' function so it's
208−-- class.
174+-- implementation is 'undefined'. However 'comp' can be and this partial
175+-- class implementation exists just to make the code more readable.
176+--
177+-- Please use 'identity' instead.
209−instance (Num e) => Category (Matrix e) where
178+instance (Num e) => C.Category (Matrix e) where
210− type Object (Matrix e) a = (FLN a a, CountableN a)
179+ id = undefined
211− id = iden
212− (.) = comp
180+ (.) = 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)
224
181
225-- | Zero type alias
182-- | Zero type alias
226type Zero = Void
183type Zero = Void
@@ -230,75 +187,92 @@ type One = ()
230
187
231-- Primitives
188-- Primitives
232
189
190+-- | Empty matrix constructor
191+empty :: Matrix e Zero Zero
192+empty = M I.Empty
193+
233-- | Unit matrix constructor
194-- | Unit matrix constructor
234one :: e -> Matrix e One One
195one :: e -> Matrix e One One
235one = M . I.One
196one = M . I.One
236
197
237−-- | Matrix 'Join' constructor
198+-- | Matrix 'Junc' constructor
238−join ::
199+junc ::
200+ (I.Normalize (Either a b) ~ Either (I.Normalize a) (I.Normalize b)) =>
239 Matrix e a rows ->
201 Matrix e a rows ->
240 Matrix e b rows ->
202 Matrix e b rows ->
241 Matrix e (Either a b) rows
203 Matrix e (Either a b) rows
242−join (M a) (M b) = M (I.Join a b)
204+junc (M a) (M b) = M (I.Junc a b)
243
205
244infixl 3 |||
206infixl 3 |||
245−-- | Matrix 'Join' constructor
207+-- | Matrix 'Junc' constructor
246(|||) ::
208(|||) ::
209+ (I.Normalize (Either a b) ~ Either (I.Normalize a) (I.Normalize b)) =>
247 Matrix e a rows ->
210 Matrix e a rows ->
248 Matrix e b rows ->
211 Matrix e b rows ->
249 Matrix e (Either a b) rows
212 Matrix e (Either a b) rows
250−(|||) = join
213+(|||) = junc
251
214
252−-- | Matrix 'Fork' constructor
215+-- | Matrix 'Split' constructor
253−fork ::
216+split ::
217+ (I.Normalize (Either a b) ~ Either (I.Normalize a) (I.Normalize b)) =>
254 Matrix e cols a ->
218 Matrix e cols a ->
255 Matrix e cols b ->
219 Matrix e cols b ->
256 Matrix e cols (Either a b)
220 Matrix e cols (Either a b)
257−fork (M a) (M b) = M (I.Fork a b)
221+split (M a) (M b) = M (I.Split a b)
258
222
259infixl 2 ===
223infixl 2 ===
260−-- | Matrix 'Fork' constructor
224+-- | Matrix 'Split' constructor
261(===) ::
225(===) ::
226+ (I.Normalize (Either a b) ~ Either (I.Normalize a) (I.Normalize b)) =>
262 Matrix e cols a ->
227 Matrix e cols a ->
263 Matrix e cols b ->
228 Matrix e cols b ->
264 Matrix e cols (Either a b)
229 Matrix e cols (Either a b)
265−(===) = fork
230+(===) = split
266
231
267-- Functor hierarchy
232-- Functor hierarchy
268
233
269-- | Functor instance equivalent function
234-- | Functor instance equivalent function
270−fmapM ::
235+fmapM ::
271− ( Liftable e a b,
236+ ( Bounded a,
272− CountableDimsN a b,
237+ Bounded b,
273− FLN b a
238+ Enum a,
239+ Enum b,
240+ Eq b,
241+ Num e,
242+ Ord e,
243+ KnownNat (I.Count (I.Normalize a)),
244+ KnownNat (I.Count (I.Normalize b)),
245+ I.FromLists e (I.Normalize b) (I.Normalize a)
274 )
246 )
275 =>
247 =>
276 (a -> b) -> Matrix e c a -> Matrix e c b
248 (a -> b) -> Matrix e c a -> Matrix e c b
277−fmapM f m = fromF f . m
249+fmapM f m = fromF' f `comp` m
278
250
279-- | Applicative instance equivalent 'unit' function,
251-- | Applicative instance equivalent 'unit' function,
280unitM :: (Num e) => Matrix e () ()
252unitM :: (Num e) => Matrix e () ()
281unitM = one 1
253unitM = one 1
282
254
283-- | Applicative instance equivalent 'unit' function,
255-- | Applicative instance equivalent 'unit' function,
284−multM ::
256+multM ::
285− ( CountableDimsN a b,
257+ ( KnownNat (I.Count (I.Normalize a)),
286− CountableN (a, b),
258+ KnownNat (I.Count (I.Normalize b)),
259+ KnownNat (I.Count (I.Normalize (a, b))),
287 Num e,
260 Num e,
288− FLN (a, b) a,
261+ I.FromLists e (I.Normalize (a, b)) (I.Normalize a),
289− FLN (a, b) b,
262+ I.FromLists e (I.Normalize (a, b)) (I.Normalize b),
290− TrivialP a b
263+ I.Normalize (a, b) ~ I.Normalize (I.Normalize a, I.Normalize b)
291 ) => Matrix e c a -> Matrix e c b -> Matrix e c (a, b)
264 ) => Matrix e c a -> Matrix e c b -> Matrix e c (a, b)
292−multM = kr
265+multM a b = khatri a b
266+
293
267
294-- | Monad instance equivalent 'return' function,
268-- | Monad instance equivalent 'return' function,
295−returnM ::
269+returnM ::
296− forall e a .
270+ forall e a .
297− ( Num e,
271+ ( Num e,
298− Enum e,
272+ Enum e,
299− Enum a,
273+ Enum a,
300− FLN () a,
274+ I.FromLists e () (I.Normalize a),
301− Countable a
275+ KnownNat (I.Count a)
302 ) => a -> Matrix e One a
276 ) => a -> Matrix e One a
303returnM a = col l
277returnM a = col l
304 where
278 where
@@ -314,64 +288,73 @@ bindM = flip comp
314
288
315-- | Build a matrix out of a list of list of elements. Throws a runtime
289-- | Build a matrix out of a list of list of elements. Throws a runtime
316-- error if the dimensions do not match.
290-- error if the dimensions do not match.
317−fromLists :: (FLN cols rows) => [[e]] -> Matrix e cols rows
291+fromLists :: (I.FromLists e (I.Normalize cols) (I.Normalize rows)) => [[e]] -> Matrix e cols rows
318fromLists = M . I.fromLists
292fromLists = M . I.fromLists
319
293
320-- | Matrix builder function. Constructs a matrix provided with
294-- | Matrix builder function. Constructs a matrix provided with
321−-- a construction function that operates with indices.
295+-- a construction function.
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.
329matrixBuilder ::
296matrixBuilder ::
330− ( FLN a b,
297+ (I.FromLists e (I.Normalize cols) (I.Normalize rows), KnownNat (I.Count (I.Normalize cols)), KnownNat (I.Count (I.Normalize rows))) =>
331− Enum a,
298+ ((Int, Int) -> e) ->
332− Enum b,
333− Bounded a,
334− Bounded b,
335− Eq a,
336− Countable b
337− ) => ((a, b) -> e) -> Matrix e a b
299+ Matrix e cols rows
338−matrixBuilder f = M (I.matrixBuilder f)
300+matrixBuilder = M . I.matrixBuilder
339
301
340-- | Constructs a column vector matrix
302-- | Constructs a column vector matrix
341−col :: (FLN () rows) => [e] -> Matrix e One rows
303+col :: (I.FromLists e () (I.Normalize rows)) => [e] -> Matrix e One rows
342col = M . I.col
304col = M . I.col
343
305
344-- | Constructs a row vector matrix
306-- | Constructs a row vector matrix
345−row :: (FLN cols ()) => [e] -> Matrix e cols One
307+row :: (I.FromLists e (I.Normalize cols) ()) => [e] -> Matrix e cols One
346row = M . I.row
308row = M . I.row
347
309
348-- | Lifts functions to matrices with arbitrary dimensions.
310-- | Lifts functions to matrices with arbitrary dimensions.
349--
311--
350-- NOTE: Be careful to not ask for a matrix bigger than the cardinality of
312-- NOTE: Be careful to not ask for a matrix bigger than the cardinality of
351-- types @a@ or @b@ allows.
313-- types @a@ or @b@ allows.
352−fromF' ::
314+fromF ::
353− ( Liftable e a b,
315+ ( Bounded a,
354− CountableDimsN cols rows,
316+ Bounded b,
355− FLN rows cols
317+ Enum a,
318+ Enum b,
319+ Eq b,
320+ Num e,
321+ Ord e,
322+ KnownNat (I.Count (I.Normalize cols)),
323+ KnownNat (I.Count (I.Normalize rows)),
324+ I.FromLists e (I.Normalize rows) (I.Normalize cols)
356 ) =>
325 ) =>
326+ (a -> b) ->
357− (a -> b) -> Matrix e cols rows
327+ Matrix e cols rows
358−fromF' = M . I.fromF'
328+fromF = M . I.fromF
359
329
360-- | Lifts functions to matrices with dimensions matching @a@ and @b@
330-- | Lifts functions to matrices with dimensions matching @a@ and @b@
361-- cardinality's.
331-- cardinality's.
362−fromF ::
332+fromF' ::
363− ( Liftable e a b,
333+ ( Bounded a,
364− CountableDimsN a b,
334+ Bounded b,
365− FLN b a
335+ Enum a,
336+ Enum b,
337+ Eq b,
338+ Num e,
339+ Ord e,
340+ KnownNat (I.Count (I.Normalize a)),
341+ KnownNat (I.Count (I.Normalize b)),
342+ I.FromLists e (I.Normalize b) (I.Normalize a)
366 ) =>
343 ) =>
344+ (a -> b) ->
367− (a -> b) -> Matrix e a b
345+ Matrix e a b
368−fromF = M . I.fromF
346+fromF' = M . I.fromF'
369
347
370-- | Lifts relation functions to Boolean Matrix
348-- | Lifts relation functions to Boolean Matrix
371toRel ::
349toRel ::
372− ( Liftable (Natural 0 1) a b,
350+ ( Bounded a,
373− CountableDims a b,
351+ Bounded b,
374− FLN b a
352+ Enum a,
353+ Enum b,
354+ Eq b,
355+ KnownNat (I.Count (I.Normalize a)),
356+ KnownNat (I.Count (I.Normalize b)),
357+ I.FromLists (Natural 0 1) (I.Normalize b) (I.Normalize a)
375 ) => (a -> b -> Bool) -> Matrix (Natural 0 1) a b
358 ) => (a -> b -> Bool) -> Matrix (Natural 0 1) a b
376toRel = M . I.toRel
359toRel = M . I.toRel
377
360
@@ -389,8 +372,8 @@ toList (M m) = I.toList m
389
372
390-- | The zero matrix. A matrix wholly filled with zeros.
373-- | The zero matrix. A matrix wholly filled with zeros.
391zeros ::
374zeros ::
392− (Num e, FLN cols rows, CountableDimsN cols rows)
375+ (Num e, I.FromLists e (I.Normalize cols) (I.Normalize rows), KnownNat (I.Count (I.Normalize cols)), KnownNat (I.Count (I.Normalize rows))) =>
393− => Matrix e cols rows
376+ Matrix e cols rows
394zeros = M I.zeros
377zeros = M I.zeros
395
378
396-- Ones Matrix
379-- Ones Matrix
@@ -399,8 +382,8 @@ zeros = M I.zeros
399--
382--
400-- Also known as T (Top) matrix.
383-- Also known as T (Top) matrix.
401ones ::
384ones ::
402− (Num e, FLN cols rows, CountableDimsN cols rows)
385+ (Num e, I.FromLists e (I.Normalize cols) (I.Normalize rows), KnownNat (I.Count (I.Normalize cols)), KnownNat (I.Count (I.Normalize rows))) =>
403− => Matrix e cols rows
386+ Matrix e cols rows
404ones = M I.ones
387ones = M I.ones
405
388
406-- Const Matrix
389-- Const Matrix
@@ -408,8 +391,9 @@ ones = M I.ones
408-- | The constant matrix constructor. A matrix wholly filled with a given
391-- | The constant matrix constructor. A matrix wholly filled with a given
409-- value.
392-- value.
410constant ::
393constant ::
411− (Num e, FLN cols rows, CountableDimsN cols rows)
394+ (Num e, I.FromLists e (I.Normalize cols) (I.Normalize rows), KnownNat (I.Count (I.Normalize cols)), KnownNat (I.Count (I.Normalize rows))) =>
395+ e ->
412− => e -> Matrix e cols rows
396+ Matrix e cols rows
413constant = M . I.constant
397constant = M . I.constant
414
398
415-- Bang Matrix
399-- Bang Matrix
@@ -417,30 +401,17 @@ constant = M . I.constant
417-- | The T (Top) row vector matrix.
401-- | The T (Top) row vector matrix.
418bang ::
402bang ::
419 forall e cols.
403 forall e cols.
420− (Num e, Enum e, FLN cols (), CountableN cols) =>
404+ (Num e, Enum e, I.FromLists e (I.Normalize cols) (), KnownNat (I.Count (I.Normalize cols))) =>
421 Matrix e cols One
405 Matrix e cols One
422bang = M I.bang
406bang = M I.bang
423
407
424−-- | Point constant relation
425−point ::
426− ( Bounded a,
427− Enum a,
428− Eq a,
429− Num e,
430− Ord e,
431− CountableN a,
432− FLN a One
433− ) => a -> Matrix e One a
434−point = fromF . const
435−
436−-- iden Matrix
408+-- Identity Matrix
437
409
438−-- | iden matrix
410+-- | Identity matrix
439−iden ::
411+identity ::
440− (Num e, FLN a a, CountableN a) =>
412+ (Num e, I.FromLists e (I.Normalize a) (I.Normalize a), KnownNat (I.Count (I.Normalize a))) =>
441 Matrix e a a
413 Matrix e a a
442−iden = M I.iden
414+identity = M I.identity
443−{-# NOINLINE iden #-}
444
415
445-- Matrix composition (MMM)
416-- Matrix composition (MMM)
446
417
@@ -450,32 +421,15 @@ iden = M I.iden
450-- from LAoP.
421-- from LAoP.
451comp :: (Num e) => Matrix e cr rows -> Matrix e cols cr -> Matrix e cols rows
422comp :: (Num e) => Matrix e cr rows -> Matrix e cols cr -> Matrix e cols rows
452comp (M a) (M b) = M (I.comp a b)
423comp (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)
472
424
473-- | Biproduct first component projection
425-- | Biproduct first component projection
474p1 ::
426p1 ::
475 ( Num e,
427 ( Num e,
476− CountableDimsN n m,
428+ KnownNat (I.Count (I.Normalize n)),
477− FLN n m,
429+ KnownNat (I.Count (I.Normalize m)),
478− FLN m m
430+ I.FromLists e (I.Normalize n) (I.Normalize m),
431+ I.FromLists e (I.Normalize m) (I.Normalize m),
432+ I.Normalize (Either m n) ~ Either (I.Normalize m) (I.Normalize n)
479 ) =>
433 ) =>
480 Matrix e (Either m n) m
434 Matrix e (Either m n) m
481p1 = M I.p1
435p1 = M I.p1
@@ -483,9 +437,11 @@ p1 = M I.p1
483-- | Biproduct second component projection
437-- | Biproduct second component projection
484p2 ::
438p2 ::
485 ( Num e,
439 ( Num e,
486− CountableDimsN n m,
440+ KnownNat (I.Count (I.Normalize n)),
487− FLN m n,
441+ KnownNat (I.Count (I.Normalize m)),
488− FLN n n
442+ I.FromLists e (I.Normalize m) (I.Normalize n),
443+ I.FromLists e (I.Normalize n) (I.Normalize n),
444+ I.Normalize (Either m n) ~ Either (I.Normalize m) (I.Normalize n)
489 ) =>
445 ) =>
490 Matrix e (Either m n) n
446 Matrix e (Either m n) n
491p2 = M I.p2
447p2 = M I.p2
@@ -495,9 +451,11 @@ p2 = M I.p2
495-- | Biproduct first component injection
451-- | Biproduct first component injection
496i1 ::
452i1 ::
497 ( Num e,
453 ( Num e,
498− CountableDimsN n m,
454+ KnownNat (I.Count (I.Normalize n)),
499− FLN n m,
455+ KnownNat (I.Count (I.Normalize m)),
500− FLN m m
456+ I.FromLists e (I.Normalize n) (I.Normalize m),
457+ I.FromLists e (I.Normalize m) (I.Normalize m),
458+ I.Normalize (Either m n) ~ Either (I.Normalize m) (I.Normalize n)
501 ) =>
459 ) =>
502 Matrix e m (Either m n)
460 Matrix e m (Either m n)
503i1 = tr p1
461i1 = tr p1
@@ -505,9 +463,11 @@ i1 = tr p1
505-- | Biproduct second component injection
463-- | Biproduct second component injection
506i2 ::
464i2 ::
507 ( Num e,
465 ( Num e,
508− CountableDimsN n m,
466+ KnownNat (I.Count (I.Normalize n)),
509− FLN m n,
467+ KnownNat (I.Count (I.Normalize m)),
510− FLN n n
468+ I.FromLists e (I.Normalize m) (I.Normalize n),
469+ I.FromLists e (I.Normalize n) (I.Normalize n),
470+ I.Normalize (Either m n) ~ Either (I.Normalize m) (I.Normalize n)
511 ) =>
471 ) =>
512 Matrix e n (Either m n)
472 Matrix e n (Either m n)
513i2 = tr p2
473i2 = tr p2
@@ -516,34 +476,24 @@ i2 = tr p2
516
476
517-- | Obtain the number of rows.
477-- | Obtain the number of rows.
518--
478--
519−-- NOTE: The 'KnownNat' constraint is needed in order to obtain the
479+-- NOTE: The 'KnownNat' constaint is needed in order to obtain the
520−-- dimensions in constant time. For a version that doesn't require the
480+-- dimensions in constant time.
521−-- constraint see 'rows''.
522−rows :: (CountableN rows) => Matrix e cols rows -> Int
523−rows (M m) = I.rows m
524−
525−-- | Obtain the number of rows in an inefficient manner, but without any
526−-- constraints.
527--
481--
528−-- For a more efficient version see 'rows'.
482+-- TODO: A 'rows' function that does not need the 'KnownNat' constraint in
483+-- exchange for performance.
529−rows' :: Matrix e cols rows -> Int
484+rows :: (KnownNat (I.Count (I.Normalize rows))) => Matrix e cols rows -> Int
530−rows' (M m) = I.rows' m
485+rows (M m) = I.rows m
531
486
532-- | Obtain the number of columns.
487-- | Obtain the number of columns.
488+--
489+-- NOTE: The 'KnownNat' constaint is needed in order to obtain the
490+-- dimensions in constant time.
533--
491--
534−-- NOTE: The 'KnownNat' constraint is needed in order to obtain the
492+-- TODO: A 'columns' function that does not need the 'KnownNat' constraint in
535−-- dimensions in constant time. For a version that doesn't require the
493+-- exchange for performance.
536−-- constraint see 'columns''.
537−columns :: (CountableN cols) => Matrix e cols rows -> Int
494+columns :: (KnownNat (I.Count (I.Normalize cols))) => Matrix e cols rows -> Int
538columns (M m) = I.columns m
495columns (M m) = I.columns m
539
496
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−
547-- Coproduct Bifunctor
497-- Coproduct Bifunctor
548
498
549infixl 5 -|-
499infixl 5 -|-
@@ -551,11 +501,14 @@ infixl 5 -|-
551-- | Matrix coproduct functor also known as matrix direct sum.
501-- | Matrix coproduct functor also known as matrix direct sum.
552(-|-) ::
502(-|-) ::
553 ( Num e,
503 ( Num e,
554− CountableDimsN j k,
504+ KnownNat (I.Count (I.Normalize j)),
555− FLN k k,
505+ KnownNat (I.Count (I.Normalize k)),
556− FLN j k,
506+ I.FromLists e (I.Normalize k) (I.Normalize k),
557− FLN k j,
507+ I.FromLists e (I.Normalize j) (I.Normalize k),
558− FLN j j
508+ I.FromLists e (I.Normalize k) (I.Normalize j),
509+ I.FromLists e (I.Normalize j) (I.Normalize j),
510+ I.Normalize (Either n m) ~ Either (I.Normalize n) (I.Normalize m),
511+ I.Normalize (Either k j) ~ Either (I.Normalize k) (I.Normalize j)
559 ) =>
512 ) =>
560 Matrix e n k ->
513 Matrix e n k ->
561 Matrix e m j ->
514 Matrix e m j ->
@@ -565,98 +518,104 @@ infixl 5 -|-
565-- Khatri Rao Product and projections
518-- Khatri Rao Product and projections
566
519
567-- | Khatri Rao product first component projection matrix.
520-- | Khatri Rao product first component projection matrix.
568−fstM ::
521+kp1 ::
569 forall e m k .
522 forall e m k .
570 ( Num e,
523 ( Num e,
571− CountableDimsN m k,
524+ KnownNat (I.Count (I.Normalize m)),
572− CountableN (m, k),
525+ KnownNat (I.Count (I.Normalize k)),
573− FLN (m, k) m,
526+ KnownNat (I.Count (I.Normalize (m, k))),
574− TrivialP m k
527+ I.FromLists e (I.Normalize (m, k)) (I.Normalize m),
528+ I.Normalize (m, k) ~ I.Normalize (I.Normalize m, I.Normalize k)
575 ) => Matrix e (m, k) m
529 ) => Matrix e (m, k) m
576−fstM = M (I.fstM @e @(I.Normalize m) @(I.Normalize k))
530+kp1 = M (I.kp1 @e @(I.Normalize m) @(I.Normalize k))
577
531
578-- | Khatri Rao product second component projection matrix.
532-- | Khatri Rao product second component projection matrix.
579−sndM ::
533+kp2 ::
580 forall e m k.
534 forall e m k.
581 ( Num e,
535 ( Num e,
582− CountableDimsN k m,
536+ KnownNat (I.Count (I.Normalize k)),
583− CountableN (m, k),
537+ KnownNat (I.Count (I.Normalize m)),
584− FLN (m, k) k,
538+ KnownNat (I.Count (I.Normalize (m, k))),
585− TrivialP m k
539+ I.FromLists e (I.Normalize (m, k)) (I.Normalize k),
540+ I.Normalize (m, k) ~ I.Normalize (I.Normalize m, I.Normalize k)
586 ) => Matrix e (m, k) k
541 ) => Matrix e (m, k) k
587−sndM = M (I.sndM @e @(I.Normalize m) @(I.Normalize k))
542+kp2 = M (I.kp2 @e @(I.Normalize m) @(I.Normalize k))
588
543
589-- | Khatri Rao Matrix product also known as matrix pairing.
544-- | Khatri Rao Matrix product also known as matrix pairing.
590--
545--
591-- NOTE: That this is not a true categorical product, see for instance:
546-- NOTE: That this is not a true categorical product, see for instance:
592−--
547+--
593-- @
548-- @
594−-- | fstM . kr a b == a
549+-- | kp1 `comp` khatri a b == a
595−-- kr a b ==> |
550+-- khatri a b ==> |
596−-- | sndM . kr a b == b
551+-- | kp2 `comp` khatri a b == b
597-- @
552-- @
598--
553--
599-- __Emphasis__ on the implication symbol.
554-- __Emphasis__ on the implication symbol.
600−kr ::
555+khatri ::
601 forall e cols a b.
556 forall e cols a b.
602 ( Num e,
557 ( Num e,
603− CountableDimsN a b,
558+ KnownNat (I.Count (I.Normalize a)),
604− CountableN (a, b),
559+ KnownNat (I.Count (I.Normalize b)),
605− FLN (a, b) a,
560+ KnownNat (I.Count (I.Normalize (a, b))),
606− FLN (a, b) b,
561+ I.FromLists e (I.Normalize (a, b)) (I.Normalize a),
607− TrivialP a b
562+ I.FromLists e (I.Normalize (a, b)) (I.Normalize b),
563+ I.Normalize (a, b) ~ I.Normalize (I.Normalize a, I.Normalize b)
608 ) => Matrix e cols a -> Matrix e cols b -> Matrix e cols (a, b)
564 ) => Matrix e cols a -> Matrix e cols b -> Matrix e cols (a, b)
609−kr a b =
565+khatri a b =
610− let fstM' = fstM @e @a @b
566+ let kp1' = kp1 @e @a @b
611− sndM' = sndM @e @a @b
567+ kp2' = kp2 @e @a @b
612− in comp (tr fstM') a * comp (tr sndM') b
568+ in comp (tr kp1') a * comp (tr kp2') b
613
569
614-- Product Bifunctor (Kronecker)
570-- Product Bifunctor (Kronecker)
615
571
616infixl 4 ><
572infixl 4 ><
617
573
618−-- | Matrix product functor also known as Kronecker product
574+-- | Matrix product functor also known as kronecker product
619(><) ::
575(><) ::
620 forall e m p n q.
576 forall e m p n q.
621 ( Num e,
577 ( Num e,
622− CountableDimsN m n,
578+ KnownNat (I.Count (I.Normalize m)),
623− CountableDimsN p q,
579+ KnownNat (I.Count (I.Normalize n)),
624− CountableDimsN (m, n) (p, q),
580+ KnownNat (I.Count (I.Normalize p)),
625− FLN (m, n) m,
581+ KnownNat (I.Count (I.Normalize q)),
626− FLN (m, n) n,
582+ KnownNat (I.Count (I.Normalize (m, n))),
627− FLN (p, q) p,
583+ KnownNat (I.Count (I.Normalize (p, q))),
628− FLN (p, q) q,
584+ I.FromLists e (I.Normalize (m, n)) (I.Normalize m),
629− TrivialP m n,
585+ I.FromLists e (I.Normalize (m, n)) (I.Normalize n),
630− TrivialP p q
586+ I.FromLists e (I.Normalize (p, q)) (I.Normalize p),
587+ I.FromLists e (I.Normalize (p, q)) (I.Normalize q),
588+ I.Normalize (m, n) ~ I.Normalize (I.Normalize m, I.Normalize n),
589+ I.Normalize (p, q) ~ I.Normalize (I.Normalize p, I.Normalize q)
631 ) => Matrix e m p -> Matrix e n q -> Matrix e (m, n) (p, q)
590 ) => Matrix e m p -> Matrix e n q -> Matrix e (m, n) (p, q)
632(><) a b =
591(><) a b =
633− let fstM' = fstM @e @m @n
592+ let kp1' = kp1 @e @m @n
634− sndM' = sndM @e @m @n
593+ kp2' = kp2 @e @m @n
635− in kr (comp a fstM') (comp b sndM')
594+ in khatri (comp a kp1') (comp b kp2')
636
595
637−-- Matrix abide Join Fork
596+-- Matrix abide Junc Split
638
597
639−-- | Matrix "abiding" followin the 'Join'-'Fork' abide law.
598+-- | Matrix "abiding" followin the 'Junc'-'Split' abide law.
640−--
599+--
641-- Law:
600-- Law:
642--
601--
643-- @
602-- @
644−-- 'Join' ('Fork' a c) ('Fork' b d) == 'Fork' ('Join' a b) ('Join' c d)
603+-- 'Junc' ('Split' a c) ('Split' b d) == 'Split' ('Junc' a b) ('Junc' c d)
645-- @
604-- @
646−abideJF :: Matrix e cols rows -> Matrix e cols rows
605+abideJS :: Matrix e cols rows -> Matrix e cols rows
647−abideJF (M m) = M (I.abideJF m)
606+abideJS (M m) = M (I.abideJS m)
648
607
649−-- Matrix abide Fork Join
608+-- Matrix abide Split Junc
650
609
651−-- | Matrix "abiding" followin the 'Fork'-'Join' abide law.
610+-- | Matrix "abiding" followin the 'Split'-'Junc' abide law.
652−--
611+--
653-- Law:
612-- Law:
654--
613--
655-- @
614-- @
656−-- 'Fork' ('Join' a b) ('Join' c d) == 'Join' ('Fork' a c) ('Fork' b d)
615+-- 'Split' ('Junc' a b) ('Junc' c d) == 'Junc' ('Split' a c) ('Split' b d)
657-- @
616-- @
658−abideFJ :: Matrix e cols rows -> Matrix e cols rows
617+abideSJ :: Matrix e cols rows -> Matrix e cols rows
659−abideFJ (M m) = M (I.abideFJ m)
618+abideSJ (M m) = M (I.abideSJ m)
660
619
661-- Matrix transposition
620-- Matrix transposition
662
621
@@ -668,10 +627,11 @@ tr (M m) = M (I.tr m)
668
627
669-- | Selective functors 'select' operator equivalent inspired by the
628-- | Selective functors 'select' operator equivalent inspired by the
670-- ArrowMonad solution presented in the paper.
629-- ArrowMonad solution presented in the paper.
671−selectM ::
630+selectM ::
672 ( Num e,
631 ( Num e,
673− FLN b b,
632+ I.FromLists e (I.Normalize b) (I.Normalize b),
674− CountableN b
633+ KnownNat (I.Count (I.Normalize b)),
634+ I.Normalize (Either a b) ~ Either (I.Normalize a) (I.Normalize b)
675 ) => Matrix e cols (Either a b) -> Matrix e a b -> Matrix e cols b
635 ) => Matrix e cols (Either a b) -> Matrix e a b -> Matrix e cols b
676selectM (M m) (M y) = M (I.select m y)
636selectM (M m) (M y) = M (I.select m y)
677
637
@@ -679,14 +639,15 @@ selectM (M m) (M y) = M (I.select m y)
679
639
680-- | McCarthy's Conditional expresses probabilistic choice.
640-- | McCarthy's Conditional expresses probabilistic choice.
681cond ::
641cond ::
682− ( Trivial a,
642+ ( I.Normalize (I.Normalize a) ~ I.Normalize a,
683− Trivial2 a,
643+ KnownNat (I.Count (I.Normalize a)),
684− Trivial3 a,
644+ I.FromLists e () (I.Normalize a),
685− CountableN a,
645+ I.FromLists e (I.Normalize a) (),
686− FLN () a,
646+ I.FromLists e (I.Normalize a) (I.Normalize a),
687− FLN a (),
647+ Bounded a,
688− FLN a a,
648+ Enum a,
689− Liftable e a Bool
649+ Num e,
650+ Ord e
690 )
651 )
691 =>
652 =>
692 (a -> Bool) -> Matrix e a b -> Matrix e a b -> Matrix e a b
653 (a -> Bool) -> Matrix e a b -> Matrix e a b -> Matrix e a b
@@ -695,13 +656,9 @@ cond p (M a) (M b) = M (I.cond p a b)
695-- Pretty print
656-- Pretty print
696
657
697-- | Matrix pretty printer
658-- | Matrix pretty printer
698−pretty :: (CountableDimsN cols rows, Show e) => Matrix e cols rows -> String
659+pretty :: (KnownNat (I.Count (I.Normalize cols)), Show e) => Matrix e cols rows -> String
699pretty (M m) = I.pretty m
660pretty (M m) = I.pretty m
700
661
701-- | Matrix pretty printer
662-- | Matrix pretty printer
702−prettyPrint :: (CountableDimsN cols rows, Show e) => Matrix e cols rows -> IO ()
663+prettyPrint :: (KnownNat (I.Count (I.Normalize cols)), Show e) => Matrix e cols rows -> IO ()
703prettyPrint (M m) = I.prettyPrint m
664prettyPrint (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+7−34
@@ -30,21 +30,12 @@ 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−
43 -- * Primitives
33 -- * Primitives
34+ empty,
44 one,
35 one,
45− join,
36+ junc,
46 (|||),
37 (|||),
47− fork,
38+ split,
48 (===),
39 (===),
49
40
50 -- * Auxiliary type families
41 -- * Auxiliary type families
@@ -62,7 +53,6 @@ module LAoP.Relation
62 toList,
53 toList,
63 toBool,
54 toBool,
64 pt,
55 pt,
65− belongs,
66 relationBuilder,
56 relationBuilder,
67 zeros,
57 zeros,
68 ones,
58 ones,
@@ -90,25 +80,15 @@ module LAoP.Relation
90 injection,
80 injection,
91 surjection,
81 surjection,
92 bijection,
82 bijection,
93− domain,
94− range,
95
83
96 -- * Function division
84 -- * Function division
97 divisionF,
85 divisionF,
98
86
99− -- * Relation division
100− divR,
101− divL,
102− divS,
103− shrunkBy,
104− overriddenBy,
105−
106 -- * Relational pairing
87 -- * Relational pairing
107 splitR,
88 splitR,
108−
109 -- ** Projections
89 -- ** Projections
110− fstR,
90+ p1,
111− sndR,
91+ p2,
112 -- ** Bifunctor
92 -- ** Bifunctor
113 (><),
93 (><),
114 -- * Relational coproduct
94 -- * Relational coproduct
@@ -136,25 +116,18 @@ module LAoP.Relation
136 linearOrder,
116 linearOrder,
137 equivalence,
117 equivalence,
138 partialEquivalence,
118 partialEquivalence,
139− difunctional,
140−
141− -- * Conditionals
142− equalizer,
143
119
144 -- ** McCarthy's Conditional
120 -- ** McCarthy's Conditional
145− predR,
146− guard,
147− cond,
121+ -- cond,
148
122
149 -- * Relational composition and lifting
123 -- * Relational composition and lifting
150− iden,
124+ identity,
151 comp,
125 comp,
152 fromF,
126 fromF,
153 fromF',
127 fromF',
154
128
155 -- ** Relational application
129 -- ** Relational application
156 pointAp,
130 pointAp,
157− pointApBool,
158
131
159 -- * Matrix printing
132 -- * Matrix printing
160 pretty,
133 pretty,
src/LAoP/Relation/Internal.hs+276−540
@@ -1,5 +1,3 @@
1−{-# LANGUAGE TypeFamilies #-}
2−{-# LANGUAGE ConstraintKinds #-}
3{-# LANGUAGE GADTs #-}
1{-# LANGUAGE GADTs #-}
4{-# LANGUAGE UndecidableInstances #-}
2{-# LANGUAGE UndecidableInstances #-}
5{-# LANGUAGE FlexibleContexts #-}
3{-# LANGUAGE FlexibleContexts #-}
@@ -41,21 +39,12 @@ module LAoP.Relation.Internal
41 Relation (..),
39 Relation (..),
42 Boolean,
40 Boolean,
43
41
44− -- * Constraint type synonyms
45− Countable,
46− CountableDims,
47− CountableN,
48− CountableDimsN,
49− FLN,
50− Liftable,
51− Trivial,
52− TrivialP,
53−
54 -- * Primitives
42 -- * Primitives
43+ empty,
55 one,
44 one,
56− join,
45+ junc,
57 (|||),
46 (|||),
58− fork,
47+ split,
59 (===),
48 (===),
60
49
61 -- * Auxiliary type families
50 -- * Auxiliary type families
@@ -66,15 +55,13 @@ module LAoP.Relation.Internal
66 -- * Matrix construction and conversion
55 -- * Matrix construction and conversion
67 I.FromLists,
56 I.FromLists,
68 fromLists,
57 fromLists,
69− fromF',
70 fromF,
58 fromF,
59+ fromF',
71 toRel,
60 toRel,
72 toLists,
61 toLists,
73 toList,
62 toList,
74 toBool,
63 toBool,
75 pt,
64 pt,
76− belongs,
77− relationBuilder',
78 relationBuilder,
65 relationBuilder,
79 zeros,
66 zeros,
80 ones,
67 ones,
@@ -102,8 +89,6 @@ module LAoP.Relation.Internal
102 injection,
89 injection,
103 surjection,
90 surjection,
104 bijection,
91 bijection,
105− domain,
106− range,
107
92
108 -- * Function division
93 -- * Function division
109 divisionF,
94 divisionF,
@@ -112,15 +97,13 @@ module LAoP.Relation.Internal
112 divR,
97 divR,
113 divL,
98 divL,
114 divS,
99 divS,
115− shrunkBy,
116− overriddenBy,
117
100
118 -- * Relational pairing
101 -- * Relational pairing
119 splitR,
102 splitR,
120
103
121 -- ** Projections
104 -- ** Projections
122− fstR,
105+ p1,
123− sndR,
106+ p2,
124 -- ** Bifunctor
107 -- ** Bifunctor
125 (><),
108 (><),
126 -- * Relational coproduct
109 -- * Relational coproduct
@@ -148,25 +131,18 @@ module LAoP.Relation.Internal
148 linearOrder,
131 linearOrder,
149 equivalence,
132 equivalence,
150 partialEquivalence,
133 partialEquivalence,
151− difunctional,
152−
153− -- * Conditionals
154− equalizer,
155
134
156 -- ** McCarthy's Conditional
135 -- ** McCarthy's Conditional
157− predR,
158− guard,
159− cond,
136+ -- cond,
160
137
161 -- * Relational composition and lifting
138 -- * Relational composition and lifting
162− iden,
139+ identity,
163 comp,
140 comp,
164− fromF',
165 fromF,
141 fromF,
142+ fromF',
166
143
167 -- ** Relational application
144 -- ** Relational application
168 pointAp,
145 pointAp,
169− pointApBool,
170
146
171 -- * Matrix printing
147 -- * Matrix printing
172 pretty,
148 pretty,
@@ -178,13 +154,12 @@ import Data.Void
178import qualified LAoP.Matrix.Internal as I
154import qualified LAoP.Matrix.Internal as I
179import LAoP.Utils.Internal
155import LAoP.Utils.Internal
180import Control.DeepSeq
156import Control.DeepSeq
157+import qualified Control.Category as C
181import Data.Bool
158import Data.Bool
182import GHC.TypeLits
159import GHC.TypeLits
183−import Prelude hiding (id, (.))
184
160
185-- | Boolean type synonym for working with boolean matrices
161-- | Boolean type synonym for working with boolean matrices
186type Boolean = Natural 0 1
162type Boolean = Natural 0 1
187−type Powerset a = List (List a)
188
163
189-- | Relation data type.
164-- | Relation data type.
190newtype Relation a b = R (I.Matrix Boolean (I.Normalize a) (I.Normalize b))
165newtype Relation a b = R (I.Matrix Boolean (I.Normalize a) (I.Normalize b))
@@ -192,34 +167,25 @@ newtype Relation a b = R (I.Matrix Boolean (I.Normalize a) (I.Normalize b))
192
167
193deriving instance (Read (I.Matrix Boolean (I.Normalize a) (I.Normalize b))) => Read (Relation a b)
168deriving instance (Read (I.Matrix Boolean (I.Normalize a) (I.Normalize b))) => Read (Relation a b)
194
169
195−-- | Constraint type synonyms to keep the type signatures less convoluted
196−type Countable a = KnownNat (I.Count a)
197−type CountableDims a b = (Countable a, Countable b)
198−type CountableN a = KnownNat (I.Count (I.Normalize a))
199−type CountableDimsN a b = (CountableN a, CountableN b)
200−type FLN a b = I.FromLists (I.Normalize a) (I.Normalize b)
201−type Liftable a b = (Bounded a, Bounded b, Enum a, Enum b, Eq b, Num Boolean, Ord Boolean)
202−type Trivial a = I.Normalize a ~ I.Normalize (I.Normalize a)
203−type TrivialP a b = I.Normalize (a, b) ~ I.Normalize (I.Normalize a, I.Normalize b)
204−
205−-- | It is possible to implement a constrained version of the category type
170+-- | It isn't possible to implement the 'id' function so it's
206−-- class.
171+-- implementation is 'undefined'. However 'comp' can be and this partial
172+-- class implementation exists just to make the code more readable.
173+--
174+-- Please use 'identity' instead.
207−instance Category Relation where
175+instance C.Category Relation where
208− type Object Relation a = (FLN a a, CountableN a)
176+ id = undefined
209− id = iden
210− (.) = comp
177+ (.) = comp
211
178
212instance Num (Relation a b) where
179instance Num (Relation a b) where
213− -- | Matrix addition becomes Boolean matrix disjointion
180+ -- | Matrix addition becomes Boolean matrix disjunction
214 (R a) + (R b) = R (I.orM a b)
181 (R a) + (R b) = R (I.orM a b)
215
182
216 -- | Matrix subtraction becomes Relational subtraction
183 -- | Matrix subtraction becomes Relational subtraction
217 (R a) - (R b) = R (I.subM a b)
184 (R a) - (R b) = R (I.subM a b)
218
185
219− -- | Matrix multiplication becomes Boolean matrix conjointion
186+ -- | Matrix multiplication becomes Boolean matrix conjunction
220 (R a) * (R b) = R (I.andM a b)
187 (R a) * (R b) = R (I.andM a b)
221
188
222− -- | Matrix negation becomes Boolean matrix negation
223 negate (R a) = R (I.negateM a)
189 negate (R a) = R (I.negateM a)
224
190
225-- Type alias
191-- Type alias
@@ -228,107 +194,105 @@ type One = ()
228
194
229-- Primitives
195-- Primitives
230
196
197+-- | Empty matrix constructor
198+empty :: Relation Zero Zero
199+empty = R I.Empty
200+
231-- | Unit matrix constructor
201-- | Unit matrix constructor
232one :: Boolean -> Relation One One
202one :: Boolean -> Relation One One
233one = R . I.One
203one = R . I.One
234
204
235−-- | Boolean Matrix 'Join' constructor, also known as relational coproduct.
205+-- | Boolean Matrix 'Junc' constructor, also known as relational coproduct.
236--
206--
237-- See 'eitherR'.
207-- See 'eitherR'.
208+junc :: (I.Normalize (Either a b) ~ Either (I.Normalize a) (I.Normalize b))
238−join :: Relation a c -> Relation b c -> Relation (Either a b) c
209+ => Relation a c -> Relation b c -> Relation (Either a b) c
239−join (R a) (R b) = R (I.Join a b)
210+junc (R a) (R b) = R (I.Junc a b)
240
211
241infixl 3 |||
212infixl 3 |||
242−-- | Boolean Matrix 'Join' constructor
213+-- | Boolean Matrix 'Junc' constructor
243−--
244−-- See 'eitherR'.
245(|||) ::
214(|||) ::
215+ (I.Normalize (Either a b) ~ Either (I.Normalize a) (I.Normalize b)) =>
246 Relation a c ->
216 Relation a c ->
247 Relation b c ->
217 Relation b c ->
248 Relation (Either a b) c
218 Relation (Either a b) c
249−(|||) = join
219+(|||) = junc
250
220
251−-- | Boolean Matrix 'Fork' constructor, also known as relational product.
221+-- | Boolean Matrix 'Split' constructor, also known as relational product.
222+split :: (I.Normalize (Either a b) ~ Either (I.Normalize a) (I.Normalize b))
252−fork :: Relation c a -> Relation c b -> Relation c (Either a b)
223+ => Relation c a -> Relation c b -> Relation c (Either a b)
253−fork (R a) (R b) = R (I.Fork a b)
224+split (R a) (R b) = R (I.Split a b)
254
225
255infixl 2 ===
226infixl 2 ===
256−-- | Boolean Matrix 'Fork' constructor
227+-- | Boolean Matrix 'Split' constructor
257(===) ::
228(===) ::
229+ (I.Normalize (Either a b) ~ Either (I.Normalize a) (I.Normalize b)) =>
258 Relation c a ->
230 Relation c a ->
259 Relation c b ->
231 Relation c b ->
260 Relation c (Either a b)
232 Relation c (Either a b)
261−(===) = fork
233+(===) = split
262
234
263-- Construction
235-- Construction
264
236
265-- | Build a matrix out of a list of list of elements. Throws a runtime
237-- | Build a matrix out of a list of list of elements. Throws a runtime
266-- error if the dimensions do not match.
238-- error if the dimensions do not match.
267−fromLists :: (FLN a b) => [[Boolean]] -> Relation a b
239+fromLists :: (I.FromLists Boolean (I.Normalize a) (I.Normalize b)) => [[Boolean]] -> Relation a b
268fromLists = R . I.fromLists
240fromLists = R . I.fromLists
269
241
270−-- | Relation builder function. Constructs a relation provided with
242+-- | Matrix builder function. Constructs a matrix provided with
271−-- a construction function that operates with indices.
272−relationBuilder' ::
273− (FLN a b, CountableDimsN a b) =>
274− ((Int, Int) -> Boolean) -> Relation a b
275−relationBuilder' = R . I.matrixBuilder'
276−
277−-- | Relation builder function. Constructs a relation provided with
278−-- a construction function that operates with arbitrary types.
243+-- a construction function.
279relationBuilder ::
244relationBuilder ::
280− ( FLN a b,
245+ (I.FromLists Boolean (I.Normalize a) (I.Normalize b), KnownNat (I.Count (I.Normalize a)), KnownNat (I.Count (I.Normalize b))) =>
281− Enum a,
246+ ((Int, Int) -> Boolean) ->
282− Enum b,
283− Bounded a,
284− Bounded b,
285− Eq a,
286− CountableDims a b
287− ) => ((a, b) -> Boolean) -> Relation a b
247+ Relation a b
288relationBuilder = R . I.matrixBuilder
248relationBuilder = R . I.matrixBuilder
289
249
290-- | Lifts functions to matrices with arbitrary dimensions.
250-- | Lifts functions to matrices with arbitrary dimensions.
291--
251--
292-- NOTE: Be careful to not ask for a matrix bigger than the cardinality of
252-- NOTE: Be careful to not ask for a matrix bigger than the cardinality of
293-- types @a@ or @b@ allows.
253-- types @a@ or @b@ allows.
294−fromF' ::
254+fromF ::
295− ( Liftable a b,
255+ ( Bounded a,
296− CountableDimsN c d,
256+ Bounded b,
297− FLN d c
257+ Enum a,
258+ Enum b,
259+ Eq b,
260+ KnownNat (I.Count (I.Normalize c)),
261+ KnownNat (I.Count (I.Normalize d)),
262+ I.FromLists Boolean (I.Normalize d) (I.Normalize c)
298 )
263 )
299 => (a -> b) -> Relation c d
264 => (a -> b) -> Relation c d
300−fromF' f = R (I.fromFRel' f)
265+fromF f = R (I.fromFRel f)
301
266
302-- | Lifts functions to matrices with dimensions matching @a@ and @b@
267-- | Lifts functions to matrices with dimensions matching @a@ and @b@
303-- cardinality's.
268-- cardinality's.
304−fromF ::
269+fromF' ::
305− ( Liftable a b,
270+ ( Bounded b,
306− CountableDimsN a b,
271+ Bounded a,
307− FLN b a
272+ Enum a,
273+ Enum b,
274+ Eq b,
275+ KnownNat (I.Count (I.Normalize a)),
276+ KnownNat (I.Count (I.Normalize b)),
277+ I.FromLists Boolean (I.Normalize b) (I.Normalize a)
308 )
278 )
309 => (a -> b) -> Relation a b
279 => (a -> b) -> Relation a b
310−fromF f = R (I.fromFRel f)
280+fromF' f = R (I.fromFRel' f)
311
281
312-- | Lifts relation functions to 'Relation'
282-- | Lifts relation functions to 'Relation'
313toRel ::
283toRel ::
314− ( Liftable a b,
284+ ( Bounded b,
315− CountableDims a b,
285+ Bounded a,
316− FLN b a
286+ Enum a,
287+ Enum b,
288+ Eq b,
289+ KnownNat (I.Count (I.Normalize a)),
290+ KnownNat (I.Count (I.Normalize b)),
291+ I.FromLists Boolean (I.Normalize b) (I.Normalize a)
317 )
292 )
318− => (a -> b -> Bool) -> Relation a b
293+ => (a -> b -> Bool) -> Relation a b
319toRel = R . I.toRel
294toRel = R . I.toRel
320
295
321−-- | Lowers a 'Relation' to a function
322−fromRel ::
323− ( Liftable a b,
324− Eq a,
325− CountableDimsN a b,
326− FLN a One,
327− FLN b One
328− )
329− => Relation a b -> (a -> b -> Bool)
330−fromRel r a b = pointApBool a b r
331−
332-- Conversion
296-- Conversion
333
297
334-- | Converts a matrix to a list of lists of elements.
298-- | Converts a matrix to a list of lists of elements.
@@ -339,188 +303,106 @@ toLists (R m) = I.toLists m
339toList :: Relation a b -> [Boolean]
303toList :: Relation a b -> [Boolean]
340toList (R m) = I.toList m
304toList (R m) = I.toList m
341
305
342−-- | Converts a well typed 'Relation' to 'Bool'.
306+-- | Converts a well typed @'Relation'@ to @'Bool'@.
343toBool :: Relation One One -> Bool
307toBool :: Relation One One -> Bool
344toBool r = case toList r of
308toBool r = case toList r of
345 [Nat 0] -> False
309 [Nat 0] -> False
346 _ -> True
310 _ -> True
347
311
348−-- | Power transpose.
312+-- | Power transpose
349−--
350−-- Maps a relation to a set valued function.
351−pt ::
313+pt ::
352− ( Liftable a b,
314+ ( Bounded a,
315+ Bounded b,
316+ Enum a,
317+ Enum b,
353 Eq a,
318 Eq a,
354− CountableDimsN a b,
319+ Eq b,
355− FLN a One,
320+ KnownNat (I.Count (I.Normalize a)),
356− FLN b One
321+ KnownNat (I.Count (I.Normalize b)),
322+ I.FromLists Boolean (I.Normalize a) One,
323+ I.FromLists Boolean (I.Normalize b) One
357 )
324 )
358− => Relation a b -> (a -> List b)
325+ => Relation a b -> (a -> [b])
359pt r a =
326pt r a =
360− let (L lb) = maxBound
327+ let lb = [minBound .. maxBound]
361− in L [ b | b <- lb, toBool (pointAp a b r) ]
328+ in [ b | b <- lb, toBool (pointAp a b r) ]
362−
363−-- | Belongs relation
364−belongs ::
365− ( Bounded a,
366− Enum a,
367− Eq a,
368− CountableDims (List a) a,
369− FLN a (List a)
370− )
371− => Relation (List a) a
372−belongs = toRel elemR
373− where
374− elemR (L l) x = x `elem` l
375
329
376-- Zeros Matrix
330-- Zeros Matrix
377
331
378−-- | The zero relation. A relation where no element of type @a@ relates
332+-- | The zero matrix. A matrix wholly filled with zeros.
379−-- with elements of type @b@.
380−--
381−-- Also known as ⊥ (Bottom) Relation.
382−--
383−-- @
384−-- r `.` ⊥ == ⊥ `.` r == ⊥
385−-- ⊥ ``sse`` R && R ``sse`` T == True
386−-- @
387zeros ::
333zeros ::
388− (FLN a b, CountableDimsN a b) =>
334+ (I.FromLists Boolean (I.Normalize a) (I.Normalize b), KnownNat (I.Count (I.Normalize a)), KnownNat (I.Count (I.Normalize b))) =>
389 Relation a b
335 Relation a b
390−zeros = relationBuilder' (const (nat 0))
336+zeros = relationBuilder (const (nat 0))
391
337
392-- Ones Matrix
338-- Ones Matrix
393
339
394−-- | The ones relation. A relation where every element of type @a@ relates
340+-- | The ones matrix. A matrix wholly filled with ones.
395−-- with every element of type @b@.
396--
341--
397−-- Also known as T (Top) Relation or universal Relation.
342+-- Also known as T (Top) matrix.
398−--
399−-- @
400−-- ⊥ ``sse`` R && R ``sse`` T == True
401−-- @
402ones ::
343ones ::
403− (FLN a b, CountableDimsN a b) =>
344+ (I.FromLists Boolean (I.Normalize a) (I.Normalize b), KnownNat (I.Count (I.Normalize a)), KnownNat (I.Count (I.Normalize b))) =>
404 Relation a b
345 Relation a b
405−ones = relationBuilder' (const (nat 1))
346+ones = relationBuilder (const (nat 1))
406
347
407-- Bang Matrix
348-- Bang Matrix
408
349
409−-- | The T (Top) row vector relation.
350+-- | The T (Top) row vector matrix.
410bang ::
351bang ::
411− (FLN a One, CountableN a) =>
352+ (I.FromLists Boolean (I.Normalize a) One, KnownNat (I.Count (I.Normalize a))) =>
412 Relation a One
353 Relation a One
413bang = ones
354bang = ones
414
355
415-- | Point constant relation
356-- | Point constant relation
416−point ::
357+point ::
417 ( Bounded a,
358 ( Bounded a,
418 Enum a,
359 Enum a,
419 Eq a,
360 Eq a,
420− CountableN a,
361+ KnownNat (I.Count (I.Normalize a)),
421− FLN a One
362+ I.FromLists Boolean (I.Normalize a) One
422 ) => a -> Relation One a
363 ) => a -> Relation One a
423−point = fromF . const
364+point = fromF' . const
424
365
425−-- iden Matrix
366+-- Identity Matrix
426
367
427−-- | iden matrix
368+-- | Identity matrix
428−--
369+identity ::
429−-- @
370+ (I.FromLists Boolean (I.Normalize a) (I.Normalize a), KnownNat (I.Count (I.Normalize a))) =>
430−-- 'iden' `.` r == r == r `.` 'iden'
431−-- @
432−iden ::
433− (FLN a a, CountableN a) => Relation a a
371+ Relation a a
434−iden = relationBuilder' (bool (nat 0) (nat 1) . uncurry (==))
372+identity = relationBuilder (bool (nat 0) (nat 1) . uncurry (==))
435
373
436-- | Relational composition
374-- | Relational composition
437−--
438−-- @
439−-- r `.` (s `.` p) = (r `.` s) `.` p
440−-- @
441comp :: Relation b c -> Relation a b -> Relation a c
375comp :: Relation b c -> Relation a b -> Relation a c
442comp (R a) (R b) = R (I.compRel a b)
376comp (R a) (R b) = R (I.compRel a b)
443
377
444-- | Relational right division
378-- | Relational right division
445−--
446−-- @'divR' x y@ is the largest relation @z@ which,
447−-- pre-composed with @y@, approximates @x@.
448divR :: Relation b c -> Relation b a -> Relation a c
379divR :: Relation b c -> Relation b a -> Relation a c
449divR (R x) (R y) = R (I.divR x y)
380divR (R x) (R y) = R (I.divR x y)
450
381
451-- | Relational left division
382-- | Relational left division
452−--
453−-- The dual division operator:
454−--
455−-- @
456−-- 'divL' y x == 'conv' ('divR' ('conv' x) ('conv' y)
457−-- @
458divL :: Relation c b -> Relation a b -> Relation a c
383divL :: Relation c b -> Relation a b -> Relation a c
459divL (R x) (R y) = R (I.divL x y)
384divL (R x) (R y) = R (I.divL x y)
460
385
461-- | Relational symmetric division
386-- | Relational symmetric division
462−--
463−-- @'pointAp' c b ('divS' s r)@ means that @b@ and @c@
464−-- are related to exactly the same outputs by @r@ and by @s@.
465divS :: Relation c a -> Relation b a -> Relation c b
387divS :: Relation c a -> Relation b a -> Relation c b
466divS (R x) (R y) = R (I.divS x y)
388divS (R x) (R y) = R (I.divS x y)
467
389
468−-- | Relational shrinking.
469−--
470−-- @r ``shrunkBy`` s@ is the largest part of @r@ such that,
471−-- if it yields an output for an input @x@, it must be a maximum,
472−-- with respect to @s@, among all possible outputs of @x@ by @r@.
473−shrunkBy :: Relation b a -> Relation a a -> Relation b a
474−shrunkBy r s = r `intersection` divR s (conv r)
475−
476−-- | Relational overriding.
477−--
478−-- @r ``overriddenBy`` s@ yields the relation which contains the
479−-- whole of @s@ and that part of @r@ where @s@ is undefined.
480−--
481−-- @
482−-- 'zeros' ``overriddenBy`` s == s
483−-- r ``overriddenBy`` 'zeros' == r
484−-- r ``overriddenBy`` r == r
485−-- @
486−overriddenBy ::
487− ( FLN b b,
488− CountableN b
489− ) => Relation a b -> Relation a b -> Relation a b
490−overriddenBy r s = s `union` r `intersection` divR zeros (conv s)
491−
492−-- | Relational application.
390+-- | Relational application
493−--
494−-- If @a@ and @b@ are related by 'Relation' @r@
495−-- then @'pointAp' a b r == 'one' ('nat' 1)@
496pointAp ::
391pointAp ::
497− ( Liftable a b,
392+ ( Bounded a,
393+ Bounded b,
394+ Enum a,
395+ Enum b,
498 Eq a,
396 Eq a,
499− CountableDimsN a b,
397+ Eq b,
500− FLN a One,
398+ KnownNat (I.Count (I.Normalize a)),
501− FLN b One
399+ KnownNat (I.Count (I.Normalize b)),
400+ I.FromLists Boolean (I.Normalize a) One,
401+ I.FromLists Boolean (I.Normalize b) One
502 ) => a -> b -> Relation a b -> Relation One One
402 ) => a -> b -> Relation a b -> Relation One One
503−pointAp a b r = conv (point b) . r . point a
403+pointAp a b r = conv (point b) `comp` r `comp` point a
504−
505−-- | Relational application
506−--
507−-- The same as 'pointAp' but converts 'Boolean' to 'Bool'
508−pointApBool ::
509− ( Liftable a b,
510− Eq a,
511− CountableDimsN a b,
512− FLN a One,
513− FLN b One
514− ) => a -> b -> Relation a b -> Bool
515−pointApBool a b r = toBool $ conv (point b) . r . point a
516
404
517-- | Relational converse
405-- | Relational converse
518−--
519−-- Given binary 'Relation' r, writing @'pointAp' a b r@
520−-- (read: “@b@ is related to @a@ by @r@”) means the same as
521−-- @'pointAp' b a ('conv' r)@, where @'conv' r@ is said to be
522−-- the converse of @r@.
523−-- In terms of grammar, @'conv' r@ corresponds to the passive voice
524conv :: Relation a b -> Relation b a
406conv :: Relation a b -> Relation b a
525conv (R a) = R (I.tr a)
407conv (R a) = R (I.tr a)
526
408
@@ -538,187 +420,165 @@ iff r s = r == s
538
420
539-- | Relational intersection
421-- | Relational intersection
540--
422--
541−-- Lifts pointwise conjointion.
423+-- Lifts pointwise conjunction.
542−--
543−-- @
544−-- (r ``intersection`` s) ``intersection`` t == r ``intersection`` (s ``intersection`` t)
545−-- x ``sse`` r ``intersection`` s == x ``intersection`` r && x ``intersection`` s
546−-- @
547intersection :: Relation a b -> Relation a b -> Relation a b
424intersection :: Relation a b -> Relation a b -> Relation a b
548intersection a b = a * b
425intersection a b = a * b
549
426
550-- | Relational union
427-- | Relational union
551--
428--
552−-- Lifts pointwise disjointion.
429+-- Lifts pointwise disjunction.
553−--
554−-- @
555−-- (r ``union`` s) ``union`` t == r `'union' (s ``union`` t)
556−-- r ``union`` s ``sse`` x == r ``sse`` x && s ``sse`` x
557−-- r `.` (s ``union`` t) == (r `.` s) ``union`` (r `.` t)
558−-- (s ``union`` t) `.` r == (s `.` r) ``union`` (t `.` r)
559−-- @
560union :: Relation a b -> Relation a b -> Relation a b
430union :: Relation a b -> Relation a b -> Relation a b
561union a b = a + b
431union a b = a + b
562
432
563-- | Relation Kernel
433-- | Relation Kernel
564−--
565−-- @
566−-- 'ker' r == 'conv' r `.` r
567−-- 'ker' r == 'img' ('conv' r)
568−-- @
569ker :: Relation a b -> Relation a a
434ker :: Relation a b -> Relation a a
570−ker r = conv r . r
435+ker r = conv r `comp` r
571
436
572-- | Relation Image
437-- | Relation Image
573−--
574−-- @
575−-- 'img' r == r `.` conv r
576−-- 'img' r == 'ker' ('conv' r)
577−-- @
578img :: Relation a b -> Relation b b
438img :: Relation a b -> Relation b b
579−img r = r . conv r
439+img r = r `comp` conv r
580
440
581−-- | Function division. Special case of 'divS'.
441+-- | Function division.
582--
442--
583-- NOTE: _This is only valid_ if @f@ and @g@ are 'function's, i.e. 'simple' and
443-- NOTE: _This is only valid_ if @f@ and @g@ are 'function's, i.e. 'simple' and
584-- 'entire'.
444-- 'entire'.
585--
445--
586−-- @'divisionF' f g == 'conv' g `.` f@
446+-- @division f g == conv g `'comp'` f@
587divisionF :: Relation a c -> Relation b c -> Relation a b
447divisionF :: Relation a c -> Relation b c -> Relation a b
588−divisionF f g = conv g . f
448+divisionF f g = conv g `comp` f
589
449
590-- Taxonomy of binary relations
450-- Taxonomy of binary relations
591
451
592−-- | A 'Relation' @r@ is 'simple' 'iff' @'coreflexive' ('img' r)@
452+-- | A 'Relation' @r@ is simple iff @'coreflexive' ('img' r)@
593−simple :: (CountableN b, FLN b b) => Relation a b -> Bool
453+simple :: (KnownNat (I.Count (I.Normalize b)), I.FromLists Boolean (I.Normalize b) (I.Normalize b)) => Relation a b -> Bool
594simple = coreflexive . img
454simple = coreflexive . img
595
455
596−-- | A 'Relation' @r@ is 'injective' 'iff' @'coreflexive' ('ker' r)@
456+-- | A 'Relation' @r@ is injective iff @'coreflexive' ('ker' r)@
597−injective :: (CountableN a, FLN a a) => Relation a b -> Bool
457+injective :: (KnownNat (I.Count (I.Normalize a)), I.FromLists Boolean (I.Normalize a) (I.Normalize a)) => Relation a b -> Bool
598injective = coreflexive . ker
458injective = coreflexive . ker
599
459
600−-- | A 'Relation' @r@ is 'entire' 'iff' @'reflexive' ('ker' r)@
460+-- | A 'Relation' @r@ is entire iff @'reflexive' ('ker' r)@
601−entire :: (CountableN a, FLN a a) => Relation a b -> Bool
461+entire :: (KnownNat (I.Count (I.Normalize a)), I.FromLists Boolean (I.Normalize a) (I.Normalize a)) => Relation a b -> Bool
602entire = reflexive . ker
462entire = reflexive . ker
603
463
604−-- | A 'Relation' @r@ is 'surjective' 'iff' @'reflexive' ('img' r)@
464+-- | A 'Relation' @r@ is surjective iff @'reflexive' ('img' r)@
605−surjective :: (CountableN b, FLN b b) => Relation a b -> Bool
465+surjective :: (KnownNat (I.Count (I.Normalize b)), I.FromLists Boolean (I.Normalize b) (I.Normalize b)) => Relation a b -> Bool
606surjective = reflexive . img
466surjective = reflexive . img
607
467
608−-- | A 'Relation' @r@ is a 'function' 'iff' @'simple' r && 'entire' r@
468+-- | A 'Relation' @r@ is a function iff @'simple' r && 'entire' r@
609--
469--
610-- A 'function' @f@ enjoys the following properties, where @r@ and @s@ are binary
470-- A 'function' @f@ enjoys the following properties, where @r@ and @s@ are binary
611-- relations:
471-- relations:
612--
472--
613-- @
473-- @
614−-- f `.` r ``sse`` s == r ``sse`` f `.` s
474+-- f `'comp'` r `'sse'` s == r `'sse'` f `'comp'` s
615−-- r `.` f ``sse`` s == r ``sse`` s `.` f
475+-- r `'comp'` f `'sse'` s == r `'sse'` s `'comp'` f
616-- @
476-- @
617function ::
477function ::
618− ( CountableDimsN a b,
478+ ( KnownNat (I.Count (I.Normalize b)),
619− FLN a a,
479+ KnownNat (I.Count (I.Normalize a)),
620− FLN b b
480+ I.FromLists Boolean (I.Normalize a) (I.Normalize a),
481+ I.FromLists Boolean (I.Normalize b) (I.Normalize b)
621 )
482 )
622 => Relation a b -> Bool
483 => Relation a b -> Bool
623function r = simple r && entire r
484function r = simple r && entire r
624
485
625−-- | A 'Relation' @r@ is a 'representation' 'iff' @'injective' r && 'entire' r@
486+-- | A 'Relation' @r@ is a representation iff @'injective' r && 'entire' r@
626representation ::
487representation ::
627− ( CountableN a,
488+ ( KnownNat (I.Count (I.Normalize a)),
628− FLN a a
489+ I.FromLists Boolean (I.Normalize a) (I.Normalize a)
629 )
490 )
630 => Relation a b -> Bool
491 => Relation a b -> Bool
631representation r = injective r && entire r
492representation r = injective r && entire r
632
493
633−-- | A 'Relation' @r@ is an 'abstraction' 'iff' @'surjective' r && 'simple' r@
494+-- | A 'Relation' @r@ is an abstraction iff @'surjective' r && 'simple' r@
634abstraction ::
495abstraction ::
635− ( CountableN b,
496+ ( KnownNat (I.Count (I.Normalize b)),
636− FLN b b
497+ I.FromLists Boolean (I.Normalize b) (I.Normalize b)
637 )
498 )
638 => Relation a b -> Bool
499 => Relation a b -> Bool
639abstraction r = surjective r && simple r
500abstraction r = surjective r && simple r
640
501
641−-- | A 'Relation' @r@ is a 'surjection' 'iff' @'function' r && 'abstraction' r@
502+-- | A 'Relation' @r@ is a surjection iff @'function' r && 'abstraction' r@
642surjection ::
503surjection ::
643− ( CountableDimsN a b,
504+ ( KnownNat (I.Count (I.Normalize b)),
644− FLN a a,
505+ KnownNat (I.Count (I.Normalize a)),
645− FLN b b
506+ I.FromLists Boolean (I.Normalize a) (I.Normalize a),
507+ I.FromLists Boolean (I.Normalize b) (I.Normalize b)
646 )
508 )
647 => Relation a b -> Bool
509 => Relation a b -> Bool
648surjection r = function r && abstraction r
510surjection r = function r && abstraction r
649
511
650−-- | A 'Relation' @r@ is a 'injection' 'iff' @'function' r && 'representation' r@
512+-- | A 'Relation' @r@ is a injection iff @'function' r && 'representation' r@
651injection ::
513injection ::
652− ( CountableDimsN a b,
514+ ( KnownNat (I.Count (I.Normalize b)),
653− FLN a a,
515+ KnownNat (I.Count (I.Normalize a)),
654− FLN b b
516+ I.FromLists Boolean (I.Normalize a) (I.Normalize a),
517+ I.FromLists Boolean (I.Normalize b) (I.Normalize b)
655 )
518 )
656 => Relation a b -> Bool
519 => Relation a b -> Bool
657injection r = function r && representation r
520injection r = function r && representation r
658
521
659−-- | A 'Relation' @r@ is an 'bijection' 'iff' @'injection' r && 'surjection' r@
522+-- | A 'Relation' @r@ is an bijection iff @'injection' r && 'surjection' r@
660bijection ::
523bijection ::
661− ( CountableDimsN a b,
524+ ( KnownNat (I.Count (I.Normalize b)),
662− FLN b b,
525+ KnownNat (I.Count (I.Normalize a)),
663− FLN a a
526+ I.FromLists Boolean (I.Normalize b) (I.Normalize b),
527+ I.FromLists Boolean (I.Normalize a) (I.Normalize a)
664 ) => Relation a b -> Bool
528 ) => Relation a b -> Bool
665bijection r = injection r && surjection r
529bijection r = injection r && surjection r
666
530
531+
667-- Properties of relations
532-- Properties of relations
668
533
669−-- | A 'Relation' @r@ is 'reflexive' 'iff' @'id' ``sse`` r@
534+-- | A 'Relation' @r@ is reflexive iff @'identity' `'sse'` r@
670−reflexive :: (CountableN a, FLN a a) => Relation a a -> Bool
535+reflexive :: (KnownNat (I.Count (I.Normalize a)), I.FromLists Boolean (I.Normalize a) (I.Normalize a)) => Relation a a -> Bool
671−reflexive r = id <= r
536+reflexive r = identity <= r
672
537
673−-- | A 'Relation' @r@ is 'coreflexive' 'iff' @r ``sse`` 'id'@
538+-- | A 'Relation' @r@ is coreflexive iff @r `'sse'` 'identity'@
674−coreflexive :: (CountableN a, FLN a a) => Relation a a -> Bool
539+coreflexive :: (KnownNat (I.Count (I.Normalize a)), I.FromLists Boolean (I.Normalize a) (I.Normalize a)) => Relation a a -> Bool
675−coreflexive r = r <= id
540+coreflexive r = r <= identity
676
541
677−-- | A 'Relation' @r@ is 'transitive' 'iff' @(r `.` r) ``sse`` r@
542+-- | A 'Relation' @r@ is transitive iff @(r `'comp'` r) `'sse'` r@
678transitive :: Relation a a -> Bool
543transitive :: Relation a a -> Bool
679−transitive r = (r . r) `sse` r
544+transitive r = (r `comp` r) `sse` r
680
545
681−-- | A 'Relation' @r@ is 'symmetric' 'iff' @r == 'conv' r@
546+-- | A 'Relation' @r@ is symmetric iff @r == conv r@
682symmetric :: Relation a a -> Bool
547symmetric :: Relation a a -> Bool
683symmetric r = r == conv r
548symmetric r = r == conv r
684
549
685−-- | A 'Relation' @r@ is anti-symmetric 'iff' @(r ``intersection`` 'conv' r) ``sse`` 'id'@
550+-- | A 'Relation' @r@ is anti-symmetric iff @(r `'intersection'` 'conv' r) `'sse'` 'identity'@
686−antiSymmetric :: (CountableN a, FLN a a) => Relation a a -> Bool
551+antiSymmetric :: (KnownNat (I.Count (I.Normalize a)), I.FromLists Boolean (I.Normalize a) (I.Normalize a)) => Relation a a -> Bool
687−antiSymmetric r = (r `intersection` conv r) `sse` id
552+antiSymmetric r = (r `intersection` conv r) `sse` identity
688
553
689−-- | A 'Relation' @r@ is 'irreflexive' 'iff' @(r ``intersection`` 'id') == 'zeros'@
554+-- | A 'Relation' @r@ is irreflexive iff @(r `'intersection'` identity) == 'zeros'@
690−irreflexive :: (CountableN a, FLN a a) => Relation a a -> Bool
555+irreflexive :: (KnownNat (I.Count (I.Normalize a)), I.FromLists Boolean (I.Normalize a) (I.Normalize a)) => Relation a a -> Bool
691−irreflexive r = (r `intersection` id) == zeros
556+irreflexive r = (r `intersection` identity) == zeros
692
557
693−-- | A 'Relation' @r@ is 'connected' 'iff' @(r ``union`` 'conv' r) == 'ones'@
558+-- | A 'Relation' @r@ is connected iff @(r `'union'` 'conv' r) == 'ones'@
694−connected :: (CountableN a, FLN a a) => Relation a a -> Bool
559+connected :: (KnownNat (I.Count (I.Normalize a)), I.FromLists Boolean (I.Normalize a) (I.Normalize a)) => Relation a a -> Bool
695connected r = (r `union` conv r) == ones
560connected r = (r `union` conv r) == ones
696
561
697−-- | A 'Relation' @r@ is a 'preorder' 'iff' @'reflexive' r && 'transitive' r@
562+-- | A 'Relation @r@ is a preorder iff @'reflexive' r && 'transitive' r@
698−preorder :: (CountableN a, FLN a a) => Relation a a -> Bool
563+preorder :: (KnownNat (I.Count (I.Normalize a)), I.FromLists Boolean (I.Normalize a) (I.Normalize a)) => Relation a a -> Bool
699preorder r = reflexive r && transitive r
564preorder r = reflexive r && transitive r
700
565
701−-- | A 'Relation' @r@ is a partial-order 'iff' @'antiSymmetric' r && 'preorder' r@
566+-- | A 'Relation @r@ is a partial order iff @'antiSymmetric' r && 'preorder' r@
702−partialOrder :: (CountableN a, FLN a a) => Relation a a -> Bool
567+partialOrder :: (KnownNat (I.Count (I.Normalize a)), I.FromLists Boolean (I.Normalize a) (I.Normalize a)) => Relation a a -> Bool
703partialOrder r = antiSymmetric r && preorder r
568partialOrder r = antiSymmetric r && preorder r
704
569
705−-- | A 'Relation' @r@ is a linear-order 'iff' @'connected' r && 'partialOrder' r@
570+-- | A 'Relation @r@ is a linear order iff @'connected' r && 'partialOrder' r@
706−linearOrder :: (CountableN a, FLN a a) => Relation a a -> Bool
571+linearOrder :: (KnownNat (I.Count (I.Normalize a)), I.FromLists Boolean (I.Normalize a) (I.Normalize a)) => Relation a a -> Bool
707linearOrder r = connected r && partialOrder r
572linearOrder r = connected r && partialOrder r
708
573
709−-- | A 'Relation' @r@ is an 'equivalence' 'iff' @'symmetric' r && 'preorder' r@
574+-- | A 'Relation @r@ is an equivalence iff @'symmetric' r && 'preorder' r@
710−equivalence :: (CountableN a, FLN a a) => Relation a a -> Bool
575+equivalence :: (KnownNat (I.Count (I.Normalize a)), I.FromLists Boolean (I.Normalize a) (I.Normalize a)) => Relation a a -> Bool
711equivalence r = symmetric r && preorder r
576equivalence r = symmetric r && preorder r
712
577
713−-- | A 'Relation' @r@ is a partial-equivalence 'iff' @'partialOrder' r && 'equivalence' r@
578+-- | A 'Relation @r@ is a partial equivalence iff @'partialOrder' r && 'equivalence' r@
714−partialEquivalence :: (CountableN a, FLN a a) => Relation a a -> Bool
579+partialEquivalence :: (KnownNat (I.Count (I.Normalize a)), I.FromLists Boolean (I.Normalize a) (I.Normalize a)) => Relation a a -> Bool
715partialEquivalence r = partialOrder r && equivalence r
580partialEquivalence r = partialOrder r && equivalence r
716
581
717−-- | A 'Relation' @r@ is 'difunctional' or regular wherever
718−-- @r `.` 'conv' r `.` r == r@
719−difunctional :: Relation a b -> Bool
720−difunctional r = r . conv r . r == r
721−
722-- Relational pairing
582-- Relational pairing
723
583
724-- | Relational pairing.
584-- | Relational pairing.
@@ -726,81 +586,64 @@ difunctional r = r . conv r . r == r
726-- NOTE: That this is not a true categorical product, see for instance:
586-- NOTE: That this is not a true categorical product, see for instance:
727--
587--
728-- @
588-- @
729−-- | 'fstR' `.` 'splitR' a b ``sse`` a
589+-- | 'p1' `'comp'` 'splitR' a b `'sse'` a
730−-- 'splitR' a b <=> |
590+-- 'splitR' a b <=> |
731−-- | 'sndR' `.` 'splitR' a b ``sse`` b
591+-- | 'p2' `'comp'` 'splitR' a b `'sse'` b
732-- @
592-- @
733--
593--
734-- __Emphasis__ on the 'sse'.
594-- __Emphasis__ on the 'sse'.
735−--
736−-- @
737−-- 'splitR' r s `.` f == 'splitR' (r `.` f) (s `.` f)
738−-- (R '><' S) `.` 'splitR' p q == 'splitR' (r `.` p) (s `.` q)
739−-- 'conv' ('splitR' r s) `.` 'splitR' x y == ('conv' r `.` x) ``intersection`` ('conv' s `.` y)
740−-- @
741−--
742−-- @
743−-- 'eitherR' ('splitR' r s) ('splitR' t v) == 'splitR' ('eitherR' r t) ('eitherR' s v)
744−-- @
745splitR ::
595splitR ::
746− ( CountableDimsN a b,
596+ ( KnownNat (I.Count (I.Normalize a)),
747− CountableN (a, b),
597+ KnownNat (I.Count (I.Normalize b)),
748− FLN (a, b) a,
598+ KnownNat (I.Count (I.Normalize (a, b))),
749− FLN (a, b) b,
599+ I.FromLists Boolean (I.Normalize (a, b)) (I.Normalize a),
750− TrivialP a b
600+ I.FromLists Boolean (I.Normalize (a, b)) (I.Normalize b),
601+ I.Normalize (a, b) ~ I.Normalize (I.Normalize a, I.Normalize b)
751 )
602 )
752 => Relation c a -> Relation c b -> Relation c (a, b)
603 => Relation c a -> Relation c b -> Relation c (a, b)
753−splitR (R f) (R g) = R (I.kr f g)
604+splitR (R f) (R g) = R (I.khatri f g)
754
605
755-- | Relational pairing first component projection
606-- | Relational pairing first component projection
756−--
607+p1 ::
757−-- @
758−-- 'fstR' `.` 'splitR' r s ``sse`` r
759−-- @
760−fstR ::
761 forall a b .
608 forall a b .
762− ( CountableDimsN a b,
609+ ( KnownNat (I.Count (I.Normalize a)),
763− CountableN (a, b),
610+ KnownNat (I.Count (I.Normalize b)),
764− FLN (a, b) a,
611+ KnownNat (I.Count (I.Normalize (a, b))),
765− TrivialP a b
612+ I.FromLists Boolean (I.Normalize (a, b)) (I.Normalize a),
613+ I.Normalize (a, b) ~ I.Normalize (I.Normalize a, I.Normalize b)
766 )
614 )
767 => Relation (a, b) a
615 => Relation (a, b) a
768−fstR = R (I.fstM @Boolean @(I.Normalize a) @(I.Normalize b))
616+p1 = R (I.kp1 @Boolean @(I.Normalize a) @(I.Normalize b))
769
617
770-- | Relational pairing second component projection
618-- | Relational pairing second component projection
771−--
619+p2 ::
772−-- @
773−-- 'sndR' `.` 'splitR' r s ``sse`` s
774−-- @
775−sndR ::
776 forall a b .
620 forall a b .
777− ( CountableDimsN a b,
621+ ( KnownNat (I.Count (I.Normalize b)),
778− CountableN (a, b),
622+ KnownNat (I.Count (I.Normalize a)),
779− FLN (a, b) b,
623+ KnownNat (I.Count (I.Normalize (a, b))),
780− TrivialP a b
624+ I.FromLists Boolean (I.Normalize (a, b)) (I.Normalize b),
625+ I.Normalize (a, b) ~ I.Normalize (I.Normalize a, I.Normalize b)
781 )
626 )
782 => Relation (a, b) b
627 => Relation (a, b) b
783−sndR = R (I.sndM @Boolean @(I.Normalize a) @(I.Normalize b))
628+p2 = R (I.kp2 @Boolean @(I.Normalize a) @(I.Normalize b))
784
629
785-- Relational pairing functor
630-- Relational pairing functor
786
631
787infixl 4 ><
632infixl 4 ><
788-- | Relational pairing functor
633-- | Relational pairing functor
789−--
790−-- @
791−-- r '><' s == 'splitR' (r `.` fstR) (s `.` sndR)
792−-- (r '><' s) `.` (p '><' q) == (r `.` p) '><' (s `.` q)
793−-- @
794(><) ::
634(><) ::
795− ( CountableDimsN a b,
635+ ( KnownNat (I.Count (I.Normalize a)),
796− CountableDimsN c d,
636+ KnownNat (I.Count (I.Normalize b)),
797− CountableDimsN (a, c) (b, d),
637+ KnownNat (I.Count (I.Normalize c)),
798− FLN (a, c) a,
638+ KnownNat (I.Count (I.Normalize d)),
799− FLN (a, c) c,
639+ KnownNat (I.Count (I.Normalize (a, c))),
800− FLN (b, d) b,
640+ KnownNat (I.Count (I.Normalize (b, d))),
801− FLN (b, d) d,
641+ I.FromLists Boolean (I.Normalize (a, c)) (I.Normalize a),
802− TrivialP a c,
642+ I.FromLists Boolean (I.Normalize (a, c)) (I.Normalize c),
803− TrivialP b d
643+ I.FromLists Boolean (I.Normalize (b, d)) (I.Normalize b),
644+ I.FromLists Boolean (I.Normalize (b, d)) (I.Normalize d),
645+ I.Normalize (a, c) ~ I.Normalize (I.Normalize a, I.Normalize c),
646+ I.Normalize (b, d) ~ I.Normalize (I.Normalize b, I.Normalize d)
804 )
647 )
805 => Relation a b -> Relation c d -> Relation (a, c) (b, d)
648 => Relation a b -> Relation c d -> Relation (a, c) (b, d)
806(><) (R a) (R b) = R ((I.><) a b)
649(><) (R a) (R b) = R ((I.><) a b)
@@ -808,47 +651,28 @@ infixl 4 ><
808-- Relational co-products
651-- Relational co-products
809
652
810-- | Relational coproduct.
653-- | Relational coproduct.
811−--
654+eitherR :: (I.Normalize (Either a b) ~ Either (I.Normalize a) (I.Normalize b))
812−-- @
813−-- | 'eitherR' a b `.` 'i1' == a
814−-- 'eitherR' a b <=> |
815−-- | 'eitherR' a b `.` 'i2' == b
816−-- @
817−--
818−-- @
819−-- 'eitherR' r s `.` 'conv' ('eitherR' t u) == (r `.` 'conv' t) ``union`` (s `.` 'conv' u)
820−-- @
821−--
822−-- @
823−-- 'eitherR' ('splitR' r s) ('splitR' t v) == 'splitR' ('eitherR' r t) ('eitherR' s v)
824−-- @
825−eitherR :: Relation a c -> Relation b c -> Relation (Either a b) c
655+ => Relation a c -> Relation b c -> Relation (Either a b) c
826−eitherR = join
656+eitherR = junc
827
657
828-- | Relational coproduct first component injection
658-- | Relational coproduct first component injection
829−--
830−-- @
831−-- 'img' 'i1' ``union`` 'img' 'i2' == 'id'
832−-- 'i1' `.` 'i2' = 'zeros'
833−-- @
834i1 ::
659i1 ::
835− ( CountableDimsN a b,
660+ ( KnownNat (I.Count (I.Normalize b)),
836− FLN b a,
661+ KnownNat (I.Count (I.Normalize a)),
837− FLN a a
662+ I.FromLists Boolean (I.Normalize b) (I.Normalize a),
663+ I.FromLists Boolean (I.Normalize a) (I.Normalize a),
664+ I.Normalize (Either a b) ~ Either (I.Normalize a) (I.Normalize b)
838 )
665 )
839 => Relation a (Either a b)
666 => Relation a (Either a b)
840i1 = R I.i1
667i1 = R I.i1
841
668
842-- | Relational coproduct second component injection
669-- | Relational coproduct second component injection
843−--
844−-- @
845−-- 'img' 'i1' ``union`` 'img' 'i2' == 'id'
846−-- 'i1' `.` 'i2' = 'zeros'
847−-- @
848i2 ::
670i2 ::
849− ( CountableDimsN a b,
671+ ( KnownNat (I.Count (I.Normalize b)),
850− FLN a b,
672+ KnownNat (I.Count (I.Normalize a)),
851− FLN b b
673+ I.FromLists Boolean (I.Normalize a) (I.Normalize b),
674+ I.FromLists Boolean (I.Normalize b) (I.Normalize b),
675+ I.Normalize (Either a b) ~ Either (I.Normalize a) (I.Normalize b)
852 )
676 )
853 => Relation b (Either a b)
677 => Relation b (Either a b)
854i2 = R I.i2
678i2 = R I.i2
@@ -856,16 +680,15 @@ i2 = R I.i2
856infixl 5 -|-
680infixl 5 -|-
857
681
858-- | Relational coproduct functor.
682-- | Relational coproduct functor.
859−--
860−-- @
861−-- r '-|-' s == 'eitherR' ('i1' `.` r) ('i2' `.` s)
862−-- @
863(-|-) ::
683(-|-) ::
864− ( CountableDimsN b d,
684+ ( KnownNat (I.Count (I.Normalize d)),
865− FLN b b,
685+ KnownNat (I.Count (I.Normalize b)),
866− FLN d b,
686+ I.FromLists Boolean (I.Normalize b) (I.Normalize b),
867− FLN b d,
687+ I.FromLists Boolean (I.Normalize d) (I.Normalize b),
868− FLN d d
688+ I.FromLists Boolean (I.Normalize b) (I.Normalize d),
689+ I.FromLists Boolean (I.Normalize d) (I.Normalize d),
690+ I.Normalize (Either a c) ~ Either (I.Normalize a) (I.Normalize c),
691+ I.Normalize (Either b d) ~ Either (I.Normalize b) (I.Normalize d)
869 )
692 )
870 => Relation a b -> Relation c d -> Relation (Either a c) (Either b d)
693 => Relation a b -> Relation c d -> Relation (Either a c) (Either b d)
871(-|-) (R a) (R b) = R ((I.-|-) a b)
694(-|-) (R a) (R b) = R ((I.-|-) a b)
@@ -873,136 +696,49 @@ infixl 5 -|-
873-- Relational "Currying"
696-- Relational "Currying"
874
697
875-- | Relational 'trans'
698-- | Relational 'trans'
876−--
877−-- Every n-ary relation can be expressed as a binary relation through
878−-- 'trans'/'untrans';
879−-- more-over, where each particular attribute is placed (input/output) is irrelevant.
880trans ::
699trans ::
881− ( CountableDimsN a b,
700+ ( KnownNat (I.Count (I.Normalize (a, b))),
882− CountableN c,
701+ KnownNat (I.Count (I.Normalize a)),
883− CountableDimsN (a, b) (c, b),
702+ KnownNat (I.Count (I.Normalize (c, b))),
884− FLN (c, b) c,
703+ KnownNat (I.Count (I.Normalize b)),
885− FLN (c, b) b,
704+ KnownNat (I.Count (I.Normalize c)),
886− FLN (a, b) a,
705+ I.FromLists Boolean (I.Normalize (c, b)) (I.FromNat (I.Count c)),
887− FLN (a, b) b,
706+ I.FromLists Boolean (I.Normalize (c, b)) (I.FromNat (I.Count b)),
888− Trivial (a, b),
707+ I.FromLists Boolean (I.Normalize (a, b)) (I.FromNat (I.Count b)),
889− Trivial (c, b),
708+ I.FromLists Boolean (I.Normalize (a, b)) (I.FromNat (I.Count a)),
890− TrivialP a b,
709+ I.Normalize (a, b) ~ I.Normalize (I.Normalize (a, b)),
891− TrivialP c b
710+ I.Normalize (c, b) ~ I.Normalize (I.Normalize (c, b)),
711+ I.Normalize (I.Normalize a, I.Normalize b) ~ I.FromNat (I.Count (I.Normalize (a, b))),
712+ I.Normalize (I.Normalize c, I.Normalize b) ~ I.FromNat (I.Count (I.Normalize (c, b)))
892 )
713 )
893 => Relation (a, b) c -> Relation a (c, b)
714 => Relation (a, b) c -> Relation a (c, b)
894−trans r = splitR r sndR . conv fstR
715+trans r = splitR r p2 `comp` conv p1
895
716
896-- | Relational 'untrans'
717-- | Relational 'untrans'
897−--
898−-- Every n-ary relation can be expressed as a binary relation through
899−-- 'trans'/'untrans';
900−-- more-over, where each particular attribute is placed (input/output) is irrelevant.
901untrans ::
718untrans ::
902− ( CountableDimsN a b,
719+ ( KnownNat (I.Count (I.Normalize (a, b))),
903− CountableN c,
720+ KnownNat (I.Count (I.Normalize a)),
904− CountableDimsN (a, b) (c, b),
721+ KnownNat (I.Count (I.Normalize (c, b))),
905− FLN (c, b) c,
722+ KnownNat (I.Count (I.Normalize b)),
906− FLN (c, b) b,
723+ KnownNat (I.Count (I.Normalize c)),
907− FLN (a, b) b,
724+ I.FromLists Boolean (I.Normalize (c, b)) (I.FromNat (I.Count c)),
908− FLN (a, b) a,
725+ I.FromLists Boolean (I.Normalize (c, b)) (I.FromNat (I.Count b)),
909− Trivial (a, b),
726+ I.FromLists Boolean (I.Normalize (a, b)) (I.FromNat (I.Count b)),
910− Trivial (c, b),
727+ I.FromLists Boolean (I.Normalize (a, b)) (I.FromNat (I.Count a)),
911− TrivialP a b,
728+ I.Normalize (a, b) ~ I.Normalize (I.Normalize (a, b)),
912− TrivialP c b
729+ I.Normalize (c, b) ~ I.Normalize (I.Normalize (c, b)),
730+ I.Normalize (I.Normalize a, I.Normalize b) ~ I.FromNat (I.Count (I.Normalize (a, b))),
731+ I.Normalize (I.Normalize c, I.Normalize b) ~ I.FromNat (I.Count (I.Normalize (c, b)))
913 )
732 )
914 => Relation a (c, b) -> Relation (a, b) c
733 => Relation a (c, b) -> Relation (a, b) c
915−untrans s = fstR . conv (splitR (conv s) sndR)
734+untrans s = p1 `comp` conv (splitR (conv s) p2)
916−
917−-- | Transforms predicate @p@ into a correflexive relation.
918−--
919−-- @
920−-- 'predR' ('const' True) == 'id'
921−-- 'predR' ('const' False) == 'zeros'
922−-- @
923−--
924−-- @
925−-- 'predR' q `.` 'predR' p == 'predR' q ``union`` 'predR' p
926−-- @
927−predR ::
928− ( Bounded a,
929− Enum a,
930− Countable a,
931− CountableN a,
932− FLN a a,
933− FLN Bool a
934− )
935− => Relation a Bool -> Relation a a
936−predR p = id `intersection` divisionF (fromF (const True)) p
937−
938−-- | Equalizes functions @f@ and @g@.
939−-- That is, @'equalizer' f g@ is the largest coreflexive
940−-- that restricts @g@ so that @f@ and @g@ yield the same outputs.
941−--
942−-- @
943−-- 'equalizer' r r == 'id'
944−-- 'equalizer' ('point' True) ('point' False) == 'zeros'
945−-- @
946−equalizer ::
947− ( CountableN a,
948− FLN a a
949− )
950− => Relation a b -> Relation a b -> Relation a a
951−equalizer f g = id `intersection` divisionF f g
952−
953−-- | Relational conditional guard.
954−--
955−-- @
956−-- 'guard' p = 'i2' ``overriddenBy`` 'i1' `.` 'predR' p
957−-- @
958−guard ::
959− ( Bounded b,
960− Enum b,
961− CountableN b,
962− Countable b,
963− FLN b b,
964− FLN Bool b
965− ) => Relation b Bool -> Relation b (Either b b)
966−guard p = conv (eitherR (predR p) (predR (negate p)))
967−
968−-- | Relational McCarthy's conditional.
969−cond ::
970− ( Bounded b,
971− Enum b,
972− Countable b,
973− CountableN b,
974− FLN b b,
975− FLN Bool b
976− )
977− => Relation b Bool -> Relation b c -> Relation b c -> Relation b c
978−cond p r s = eitherR r s . guard p
979−
980−-- | Relational domain.
981−--
982−-- For injective relations, 'domain' and 'ker'nel coincide,
983−-- since @'ker' r ``sse`` 'id'@ in such situations.
984−domain ::
985− ( CountableN a,
986− FLN a a
987− ) => Relation a b -> Relation a a
988−domain r = ker r `intersection` id
989−
990−-- | Relational range.
991−--
992−-- For functions, 'range' and 'img' (image) coincide,
993−-- since @'img' f ``sse`` id@ for any @f@.
994−range ::
995− ( CountableN b,
996− FLN b b
997− ) => Relation a b -> Relation b b
998−range r = img r `intersection` id
999
735
1000-- Relation pretty print
736-- Relation pretty print
1001
737
1002-- | Relation pretty printing
738-- | Relation pretty printing
1003−pretty :: (CountableDimsN a b) => Relation a b -> String
739+pretty :: (KnownNat (I.Count (I.Normalize a))) => Relation a b -> String
1004pretty (R a) = I.pretty a
740pretty (R a) = I.pretty a
1005
741
1006-- | Relation pretty printing
742-- | Relation pretty printing
1007−prettyPrint :: (CountableDimsN a b) => Relation a b -> IO ()
743+prettyPrint :: (KnownNat (I.Count (I.Normalize a))) => Relation a b -> IO ()
1008prettyPrint (R a) = I.prettyPrint a
744prettyPrint (R a) = I.prettyPrint a
src/LAoP/Utils.hs−6
@@ -94,12 +94,6 @@ module LAoP.Utils
94 coerceNat,
94 coerceNat,
95 coerceNat2,
95 coerceNat2,
96 coerceNat3,
96 coerceNat3,
97−
98− -- * List data type
99− List (..),
100−
101− -- * Category type-class
102− Category(..)
103 )
97 )
104where
98where
105
99
src/LAoP/Utils/Internal.hs+73−70
@@ -1,13 +1,82 @@
1−{-# LANGUAGE TypeFamilies #-}
2−{-# LANGUAGE DeriveGeneric #-}
3{-# LANGUAGE TypeApplications #-}
1{-# LANGUAGE TypeApplications #-}
4{-# LANGUAGE DataKinds #-}
2{-# LANGUAGE DataKinds #-}
5{-# LANGUAGE FlexibleInstances #-}
3{-# LANGUAGE FlexibleInstances #-}
6{-# LANGUAGE GeneralizedNewtypeDeriving #-}
4{-# LANGUAGE GeneralizedNewtypeDeriving #-}
5+{-# LANGUAGE KindSignatures #-}
7{-# LANGUAGE ScopedTypeVariables #-}
6{-# LANGUAGE ScopedTypeVariables #-}
8
7
9module LAoP.Utils.Internal
8module LAoP.Utils.Internal
10− (
9+ ( -- | This is an internal module and it is not meant to be imported.
10+ --
11+ -- Utility module that provides the 'Natural' data type.
12+ -- The semantic associated with this data type is that
13+ -- it's meant to be a restricted 'Int' value. For example
14+ -- the type @Natural 6@ can only be instanciated with @Nat n@
15+ -- where @0 <= n <= 6@. Why, You might ask, because with normal
16+ -- 'Int's it is not possible to have a decent @Enum (Int, Int)@
17+ -- instance. See the following probabilistic programming model as and
18+ -- example:
19+ --
20+ -- We want to calculate the probability of the sum of two dice throws.
21+ -- To do this we start by defining the sample space:
22+ --
23+ -- @
24+ -- type SampleSpace = Int -- We think 'Int' are enough
25+ --
26+ -- die :: Dist Int 6
27+ -- die = unifrom [1..6]
28+ --
29+ -- -- Promote 'Int' addition to a matrix
30+ -- addM = fromF (uncurry (+)) -- Impossible
31+ -- @
32+ --
33+ -- The last line is impossible because @(Int, Int)@ does not have
34+ -- a good 'Enum' instance: @[(0, 1), (0, 2), .. (0, maxBound), (1, 0),
35+ -- ..]@. And we'd like the addition matrix to be of 36 columns by 12
36+ -- rows but limited to integers up to @6@!
37+ --
38+ -- One way to solve this issue is by defining and auxilary data type to
39+ -- represent the sample space:
40+ --
41+ -- @
42+ -- data SampleSpace = S1 | S2 | S3 | S4 | S5 | S6
43+ -- deriving (Show, Eq, Enum, Bounded) -- Enum and Bounded are
44+ -- important
45+ -- @
46+ --
47+ -- And write the sample space addition function:
48+ --
49+ -- @
50+ -- ssAdd :: SampleSpace -> SampleSpace -> Int
51+ -- ssAdd a b = (fromEnum a + 1) + (fromEnum b + 1)
52+ -- @
53+ --
54+ -- And then promote that function to matrix and everything is alright:
55+ --
56+ -- @
57+ -- ssAddM = fromF' (uncurry ssAdd)
58+ --
59+ -- dieSumProb = ssAddM `comp` (khatri die die)
60+ -- @
61+ --
62+ -- This is a nice solution for small sample spaces. But for larger ones
63+ -- it is not feasible to write a data type with hundreds of constructors
64+ -- and then write manipulation functions that need to deal with them.
65+ -- To mitigate this limitation the 'Natural' type comes a long way and
66+ -- allows one to model the sample in an easier way. See for instance:
67+ --
68+ -- @
69+ -- ssAdd :: Natural 6 -> Natural 6 -> Natural 12
70+ -- ssAdd = coerceNat (+)
71+ --
72+ -- ssAddM = fromF' (uncurry sumSS)
73+ --
74+ -- die :: Dist (Natural 6) 6
75+ -- die = uniform [nat @6 1 .. nat 6]
76+ --
77+ -- dieSumProb = ssAddM `comp` (khatri die die)
78+ -- @
79+ --
11 -- * 'Natural' data type
80 -- * 'Natural' data type
12 Natural(..),
81 Natural(..),
13 nat,
82 nat,
@@ -17,31 +86,19 @@ module LAoP.Utils.Internal
17 coerceNat,
86 coerceNat,
18 coerceNat2,
87 coerceNat2,
19 coerceNat3,
88 coerceNat3,
20−
21− -- * 'List' data type
22− List (..),
23−
24− -- * Category type class
25− Category(..)
26 )
89 )
27where
90where
28
91
29import Data.Coerce
92import Data.Coerce
30import Data.Proxy
93import Data.Proxy
31−import Data.List
32−import Data.Maybe
33import GHC.TypeLits
94import GHC.TypeLits
34import Control.DeepSeq
95import Control.DeepSeq
35−import GHC.Generics
36−import Data.Kind
37−import Prelude hiding (id, (.))
38−import qualified Prelude
39
96
40-- | Wrapper around 'Int's that have a restrictive semantic associated.
97-- | Wrapper around 'Int's that have a restrictive semantic associated.
41-- A value of type @'Natural' n m@ can only be instanciated with some 'Int'
98-- A value of type @'Natural' n m@ can only be instanciated with some 'Int'
42-- @i@ that's @n <= i <= m@.
99-- @i@ that's @n <= i <= m@.
43newtype Natural (start :: Nat) (end :: Nat) = Nat Int
100newtype Natural (start :: Nat) (end :: Nat) = Nat Int
44− deriving (Show, Read, Eq, Ord, NFData, Generic)
101+ deriving (Show, Read, Eq, Ord, NFData)
45
102
46-- | Throws a runtime error if any of the operations overflows or
103-- | Throws a runtime error if any of the operations overflows or
47-- underflows.
104-- underflows.
@@ -140,57 +197,3 @@ instance
140
197
141 fromEnum (Left a) = fromEnum a
198 fromEnum (Left a) = fromEnum a
142 fromEnum (Right b) = fromEnum (maxBound :: a) + fromEnum b + 1
199 fromEnum (Right b) = fromEnum (maxBound :: a) + fromEnum b + 1
143−
144−-- | Powerset data type.
145−--
146−-- This data type is a newtype wrapper around '[]'. This exists in order to
147−-- implement an 'Enum' and 'Bounded' instance that cannot be harmful for the outside.
148−newtype List a = L [a]
149− deriving (Eq, Show, Read)
150−
151−powerset :: [a] -> [[a]]
152−powerset [] = [[]]
153−powerset (x:xs) = powerset xs ++ [x:ps | ps <- powerset xs]
154−
155−instance
156− ( Enum a,
157− Bounded a
158− ) => Bounded (List a)
159− where
160− minBound = L []
161− maxBound = L [minBound .. maxBound]
162−
163−instance
164− ( Bounded a,
165− Enum a,
166− Eq a
167− ) => Enum (List a)
168− where
169− toEnum i =
170− let as = [minBound .. maxBound]
171− in L (powerset as !! i)
172−
173− fromEnum (L []) = 0
174− fromEnum (L x) =
175− let as = [minBound .. maxBound]
176− in fromMaybe (error "Does not exist") $ elemIndex x (powerset as)
177−
178−-- | Constrained category instance
179−class Category k where
180− type Object k o :: Constraint
181− type Object k o = ()
182− id :: Object k a => k a a
183− (.) :: k b c -> k a b -> k a c
184−
185−{-# RULES
186−"identity/left" forall p .
187− id . p = p
188−"identity/right" forall p .
189− p . id = p
190−"association" forall p q r .
191− (p . q) . r = p . (q . r)
192− #-}
193−
194−instance Category (->) where
195− id = Prelude.id
196− (.) = (Prelude..)
stack-8.8.3.yamldeleted−1
@@ -1 +0,0 @@
1−resolver: lts-15.5
stack.yaml+66−1
@@ -1 +1,66 @@
1+# 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
1−resolver: lts-14.3
20+resolver: lts-14.18
21+
22+# User packages to be built.
23+# Various formats can be used as shown in the example below.
24+#
25+# packages:
26+# - some-directory
27+# - https://example.com/foo/bar/baz-0.0.2.tar.gz
28+# subdirs:
29+# - auto-update
30+# - wai
31+packages:
32+- .
33+# Dependency packages to be pulled from upstream that are not in the resolver.
34+# These entries can reference officially published versions as well as
35+# forks / in-progress versions pinned to a git hash. For example:
36+#
37+# extra-deps:
38+# - acme-missiles-0.3
39+# - git: https://github.com/commercialhaskell/stack.git
40+# commit: e7b331f14bcffb8367cd58fbfc8b40ec7642100a
41+#
42+# extra-deps: []
43+
44+# Override default flag values for local packages and extra-deps
45+# flags: {}
46+
47+# Extra package databases containing global packages
48+# extra-package-dbs: []
49+
50+# Control whether we use the GHC we find on the path
51+# system-ghc: true
52+#
53+# Require a specific version of stack, using version ranges
54+# require-stack-version: -any # Default
55+# require-stack-version: ">=2.1"
56+#
57+# Override the architecture used by stack, especially useful on Windows
58+# arch: i386
59+# arch: x86_64
60+#
61+# Extra directories used by stack for building
62+# extra-include-dirs: [/path/to/dir]
63+# extra-lib-dirs: [/path/to/dir]
64+#
65+# Allow a newer minor version of GHC than the snapshot specifies
66+# compiler-check: newer-minor
stack.yaml.lock+4−4
@@ -6,7 +6,7 @@
6packages: []
6packages: []
7snapshots:
7snapshots:
8- completed:
8- completed:
9− size: 523878
9+ size: 524789
10− url: https://raw.githubusercontent.com/commercialhaskell/stackage-snapshots/master/lts/14/3.yaml
10+ url: https://raw.githubusercontent.com/commercialhaskell/stackage-snapshots/master/lts/14/18.yaml
11− sha256: 470c46c27746a48c7c50f829efc0cf00112787a7804ee4ac7a27754658f6d92c
11+ sha256: 646be71223e08234131c6989912e6011e01b9767bc447b6d466a35e14360bdf2
12− original: lts-14.3
12+ original: lts-14.18
test/Examples/Quantum.hsdeleted−31
@@ -1,31 +0,0 @@
1−{-# LANGUAGE StandaloneDeriving #-}
2−module Examples.Quantum where
3−
4−import LAoP.Utils
5−import LAoP.Matrix.Type
6−import Data.Complex
7−import Prelude hiding (id, (.))
8−
9−deriving instance Ord a => Ord (Complex a)
10−
11−xor :: (Bool, Bool) -> Bool
12−xor (False, b) = b
13−xor (True, b) = not b
14−
15−ker :: Num e => Matrix e a b -> Matrix e a a
16−ker m = tr m . m
17−
18−cnot :: Matrix (Complex Double) (Bool, Bool) (Bool, Bool)
19−cnot = kr fstM (fromF xor)
20−
21−ccnot :: (Num e, Ord e) => Matrix e ((Bool, Bool), Bool) ((Bool, Bool), Bool)
22−ccnot = kr fstM (fromF f)
23− where
24− f = xor . tp (uncurry (&&)) id
25− tp f g (a,b) = (f a, g b)
26−
27−had :: Matrix (Complex Double) Bool Bool
28−had = (1/sqrt 2) .| fromLists [[1, 1], [1, -1]]
29−
30−bell :: Matrix (Complex Double) (Bool, Bool) (Bool, Bool)
31−bell = cnot . (had >< iden)
test/Examples/Spreadsheets.hsdeleted−47
@@ -1,47 +0,0 @@
1−{-# LANGUAGE DeriveGeneric #-}
2−
3−module Examples.Spreadsheets
4−
5−import LAoP.Utils
6−import LAoP.Matrix.Type
7−import GHC.Generics
8−import Prelude hiding (id, (.))
9−
10−data Student = Student1 | Student2 | Student3 | Student4
11− deriving (Eq, Show, Enum, Bounded, Generic)
12−
13−data Question = Question1 | Question2 | Question3 | Question4
14− deriving (Eq, Show, Enum, Bounded, Generic)
15−
16−data Results = Exam | Test | Final
17− deriving (Eq, Show, Enum, Bounded, Generic)
18−
19−test :: Matrix Float One Results
20−test = point Test
21−
22−exam :: Matrix Float One Results
23−exam = point Exam
24−
25−final :: Matrix Float One Results
26−final = point Final
27−
28−m :: Matrix Float Question Student
29−m = fromLists [[95, 90, 100, 40], [20, 90, 90, 0], [30, 20, 95, 0], [50, 80, 100, 30]]
30−
31−w :: Matrix Float Question One
32−w = fromLists [[0.2, 0.3, 0.2, 0.3]]
33−
34−xls :: Matrix Float Question One
35− -> Matrix Float Question Student
36− -> Matrix Float Student One
37− -> Matrix Float (Either Question Results) (Either One Student)
38−xls w m t = join (fork w m) (fork zeros r)
39− where
40− rExam = m . tr w
41− rTest = tr t
42− rFinal = rTest `maxPW` rExam
43− r = (rExam . tr exam) + (rTest . tr test) + (rFinal . tr final)
44−
45−-- | Overloaded, point-wise 'max' function
46−maxPW :: Ord e => Matrix e a b -> Matrix e a b -> Matrix e a b
47−maxPW = zipWithM max
test/Spec.hs+1−7
@@ -1,8 +1,2 @@
1−module Main (main) where
2−
3−import qualified Examples.Readme as RD
4−
5main :: IO ()
1main :: IO ()
6−main = do
2+main = putStrLn "Test suite not yet implemented"
7− putStrLn ("Testing if README works" :: String)
8− RD.exec