git.iko.soy/laop
on master help sign in
swap
eea623179 ahead, 0 behind
29 files changed+2869−1339
since splitsnapshots
unifiedsplit
.github/workflows/ci.yml+43 .gitignore+54−2 .travis.yml+47 CHANGELOG.md+17 ChangeLog.md−3 LICENSE+17−26 README.md+107−24 Setup.hs−2 app/Main.hs−87 appveyor.yml+34 benchmark/Main.hs+175 laop.cabal+89 package.yaml−48 src/LAoP/Dist.hs+10 src/LAoP/Dist/Internal.hs+87−36 src/LAoP/Matrix/Internal.hs+487−412 src/LAoP/Matrix/Nat.hs+194−187 src/LAoP/Matrix/Type.hs+292−232 src/LAoP/Relation.hs+80−6 src/LAoP/Relation/Internal.hs+761−129 src/LAoP/Utils.hs+6 src/LAoP/Utils/Internal.hs+94−74 stack-8.8.3.yaml+1 stack.yaml+1−66 stack.yaml.lock+4−4 test/Examples/Quantum.hs+31 test/Examples/Readme.hs+184 test/Examples/Spreadsheets.hs+47 test/Spec.hs+7−1
.github/workflows/ci.ymlnew file+43
@@ -0,0 +1,43 @@
1+name: CI
2+
3+# Trigger the workflow on push or pull request, but only for the master branch
4+on:
5+ pull_request:
6+ push:
7+ branches: [master]
8+
9+jobs:
10+ build:
11+ name: ghc ${{ matrix.ghc }}
12+ runs-on: ubuntu-16.04
13+ strategy:
14+ matrix:
15+ cabal: ["3.0"]
16+ ghc:
17+ - "8.6.5"
18+ - "8.8.3"
19+
20+ steps:
21+ - uses: actions/checkout@v2
22+ if: github.event.action == 'opened' || github.event.action == 'synchronize' || github.event.ref == 'refs/heads/master'
23+
24+ - uses: actions/setup-haskell@v1
25+ name: Setup Haskell
26+ with:
27+ ghc-version: ${{ matrix.ghc }}
28+ cabal-version: ${{ matrix.cabal }}
29+
30+ - uses: actions/cache@v1
31+ name: Cache ~/.cabal/store
32+ with:
33+ path: ~/.cabal/store
34+ key: ${{ runner.os }}-${{ matrix.ghc }}-cabal
35+
36+ - name: Build
37+ run: |
38+ cabal v2-update
39+ cabal v2-build --enable-tests --enable-benchmarks
40+
41+ - name: Test
42+ run: |
43+ cabal v2-test --enable-tests
.gitignore+54−2
@@ -1,3 +1,55 @@
1+### Haskell
2+dist
3+dist-*
4+cabal-dev
5+*.o
6+*.hi
7+*.chi
8+*.chs.h
9+*.dyn_o
10+*.dyn_hi
11+*.prof
12+*.aux
13+*.hp
14+*.eventlog
15+.virtualenv
16+.hsenv
17+.hpc
18+.cabal-sandbox/
19+cabal.sandbox.config
20+cabal.config
21+cabal.project.local
22+.ghc.environment.*
23+.HTF/
24+# Stack
125.stack-work/
2−laop.cabal
3−*~
26+stack.yaml.lock
27+
28+### IDE/support
29+# Vim
30+[._]*.s[a-v][a-z]
31+[._]*.sw[a-p]
32+[._]s[a-v][a-z]
33+[._]sw[a-p]
34+*~
35+tags
36+
37+# IntellijIDEA
38+.idea/
39+.ideaHaskellLib/
40+*.iml
41+
42+# Atom
43+.haskell-ghc-mod.json
44+
45+# VS
46+.vscode/
47+
48+# Emacs
49+*#
50+.dir-locals.el
51+TAGS
52+
53+# other
54+.DS_Store
55+hackage.sh
.travis.ymlnew file+47
@@ -0,0 +1,47 @@
1+sudo: true
2+language: haskell
3+
4+git:
5+ depth: 5
6+
7+cabal: "3.0"
8+
9+cache:
10+ directories:
11+ - "$HOME/.cabal/store"
12+ - "$HOME/.stack"
13+ - "$TRAVIS_BUILD_DIR/.stack-work"
14+
15+matrix:
16+ include:
17+ - ghc: 8.6.5
18+ - ghc: 8.8.3
19+
20+ - ghc: 8.8.3
21+ env: STACK_YAML="$TRAVIS_BUILD_DIR/stack-8.8.3.yaml"
22+
23+ - ghc: 8.6.5
24+ env: STACK_YAML="$TRAVIS_BUILD_DIR/stack.yaml"
25+
26+
27+install:
28+ - |
29+ if [ -z "$STACK_YAML" ]; then
30+ cabal v2-update
31+ cabal v2-build --enable-tests --enable-benchmarks
32+ else
33+ curl -sSL https://get.haskellstack.org/ | sh
34+ stack --version
35+ stack build --system-ghc --test --bench --no-run-tests --no-run-benchmarks
36+ fi
37+
38+script:
39+ - |
40+ if [ -z "$STACK_YAML" ]; then
41+ cabal v2-test --enable-tests
42+ else
43+ stack test --system-ghc
44+ fi
45+
46+notifications:
47+ email: false
CHANGELOG.mdnew file+17
@@ -0,0 +1,17 @@
1+# Changelog
2+
3+`laop` uses [PVP Versioning][1].
4+The changelog is available [on GitHub][2].
5+
6+## 0.1.1.1
7+
8+* Bump base version to work with cabal
9+
10+## 0.1.1.0
11+
12+* Package is more organized and now has tests and benchmarks separated
13+* Repository is more organized and clean
14+* Added CI
15+
16+[1]: https://pvp.haskell.org
17+[2]: https://github.com/bolt12/laop2/releases
ChangeLog.mddeleted−3
@@ -1,3 +0,0 @@
1−# Changelog for laop
2−
3−## Unreleased changes
LICENSE+17−26
@@ -1,30 +1,21 @@
1−Copyright Armando Santos (c) 2019
1+MIT License
22
3−All rights reserved.
3+Copyright (c) 2020 Armando Santos
44
5−Redistribution and use in source and binary forms, with or without
6−modification, are permitted provided that the following conditions are met:
5+Permission is hereby granted, free of charge, to any person obtaining a copy
6+of this software and associated documentation files (the "Software"), to deal
7+in the Software without restriction, including without limitation the rights
8+to use, copy, modify, merge, publish, distribute, sublicense, and/or sell
9+copies of the Software, and to permit persons to whom the Software is
10+furnished to do so, subject to the following conditions:
711
8− * Redistributions of source code must retain the above copyright
9− notice, this list of conditions and the following disclaimer.
12+The above copyright notice and this permission notice shall be included in all
13+copies or substantial portions of the Software.
1014
11− * Redistributions in binary form must reproduce the above
12− copyright notice, this list of conditions and the following
13− disclaimer in the documentation and/or other materials provided
14− with the distribution.
15−
16− * Neither the name of Armando Santos nor the names of other
17− contributors may be used to endorse or promote products derived
18− from this software without specific prior written permission.
19−
20−THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS
21−"AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT
22−LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR
23−A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT
24−OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL,
25−SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT
26−LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE,
27−DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY
28−THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT
29−(INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE
30−OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
15+THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR
16+IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY,
17+FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE
18+AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER
19+LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM,
20+OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE
21+SOFTWARE.
README.md+107−24
@@ -1,5 +1,11 @@
11# laop - Linear Algebra of Programming library
22
3+[![GitHub CI](https://github.com/bolt12/laop/workflows/CI/badge.svg)](https://github.com/bolt12/laop/actions)
4+[![Build status](https://img.shields.io/travis/bolt12/laop.svg?logo=travis)](https://travis-ci.org/bolt12/laop)
5+[![Hackage](https://img.shields.io/hackage/v/laop.svg?logo=haskell)](https://hackage.haskell.org/package/laop)
6+[![Stackage Lts](http://stackage.org/package/laop/badge/lts)](http://stackage.org/lts/package/laop)
7+[![Stackage Nightly](http://stackage.org/package/laop/badge/nightly)](http://stackage.org/nightly/package/laop)
8+
39The LAoP discipline generalises relations and functions treating them as
410Boolean matrices and in turn consider these as arrows.
511
@@ -10,33 +16,38 @@ motivation behind the library, the underlying theory, and implementation details
1016This module offers many of the combinators mentioned in the work of
1117[Macedo (2012)](https://repositorium.sdum.uminho.pt/handle/1822/22894) and [Oliveira (2012)](https://pdfs.semanticscholar.org/ccf5/27fa9179081223bffe8067edd81948644fc0.pdf).
1218
13−See the candidate package in hackage [here](https://hackage.haskell.org/package/laop-0.1.0.0/candidate)
19+See the package in hackage [here](https://hackage.haskell.org/package/laop-0.1.1.0)
20+
21+A Functional Pearl has been written and can be regarded as the [reference document](https://github.com/bolt12/tymfgg-pearl) for this library.
1422
1523## Features
1624
17−This library offers:
18−
19−- An internal representation that uses normal datatypes (`Void`, `()`, `Either`) for matrix dimensions and two
20− type families `FromNat` and `Count` to make it easier to work with these type of matrices.
21−- A module that uses generalised types for the dimensions and is just a newtype wrapper
22− around the internal matrix data type.
23−- Other that uses type level naturals for the dimensions and is just a newtype wrapper
24− around the internal matrix data type.
25−- A very simple Probabilistic Programming module and several functions and data types to
26− make it easier to deal with sample space.
27−
28−Given this, this new matrix formulation compared to other libraries one has much more advantages, such as:
29−
30−- Has an inductive definition enabling writing matrix manipulation functions in a much more elegant and calculational way;
31−- Statically typed dimensions;
32−- Polymorphic data type dimensions;
33−- Polymorphic matrix content;
34−- Awesome dimension type inference;
35−- Fast type natural conversion via `FromNat` type family;
36−- Matrix `Junc` and `Split`-ing in O(1);
37−- Matrix composition takes advantage of divide-and-conquer and fusion laws.
38−
39−Unfortunately, this approach does not solve the issue of type dimensions being in some way constrainted making it impossible to write Arrow instances, for example. Type inference isn't perfect, when it comes to infer the types of matrices which dimensions are computed using type level naturals multiplication, the compiler needs type annotations in order to succeed.
25+This library offers 3 main matrix programming modules:
26+
27+- One in which matrices are typed with type level natural numbers;
28+- One in which matrices are typed with arbitrary generic data types;
29+- One in which matrices are regarded as relations, i.e. boolean matrices;
30+
31+There's also an experimental module that uses matrices to represent probability
32+distributions.
33+
34+The most interesting feature is that matrices are represented as an inductive data type.
35+Given this formulation, matrix algorithms can be expressed in a much more elegant and
36+calculational style than the traditional vector of vectors representation. This data type
37+guarantees that a matrix will always have valid dimensions. It can also express block matrix
38+computations naturally, which leads to total, efficient and statically typed manipulation
39+and transformation functions.
40+
41+Like matrix multiplication, other common operations, such as matrix transposition, benefit from a block-oriented structure that leads to a simple and natural divide-and-conquer algorithmic solution. Performance wise, this means that without much effort we can obtain optimal cache-oblivious algorithms.
42+
43+Given this, this new matrix formulation compared to other libraries:
44+
45+- Is more compositional and polymorphic and does not have partial matrix manipulation functions (hence less chances for usage errors);
46+- Our implementation of matrices enables simple manipulation of submatrices, making it particularly suitable for formal verification and equation reasoning, using the mathematical framework defined by the linear algebra of programming. Furthermore, the data type constructors ensure that the matrices of this kind are sound, i.e. malformed matrices with incorrect dimensions of the sort, can not be constructed.
47+
48+## Known issues
49+
50+Unfortunately, due to the use of type-level programming features, this approach sometimes requires type dimensions to be constrainted, in some way, impossible to write idiomatic Arrow instances, for example. Type inference isn't perfect, when it comes to infer the types of matrices which dimensions are computed using type level naturals multiplication, the compiler needs type annotations in order to succeed. And not all kinds of programs can be modeled using matrices, namely programs that deal with arbitrary infinite data types such as lists or integers (although there are some workarounds).
4051
4152## Notes
4253
@@ -118,6 +129,73 @@ grass_wet = row [0,1] . kp1
118129rainning :: Matrix Double (Bool, (Bool, Bool)) One
119130rainning = row [0,1] . kp2 . kp2
120131
132+-- Alcuin Puzzle
133+
134+data Being = Farmer | Fox | Goose | Beans
135+ deriving (Bounded, Enum, Eq, Show, Generic)
136+
137+data Bank = LeftB | RightB
138+ deriving (Bounded, Enum, Eq, Show, Generic)
139+
140+eats :: Being -> Being -> Bool
141+eats Fox Goose = True
142+eats Goose Beans = True
143+eats _ _ = False
144+
145+eatsR :: R.Relation Being Being
146+eatsR = R.toRel eats
147+
148+cross :: Bank -> Bank
149+cross LeftB = RightB
150+cross RightB = LeftB
151+
152+crossR :: R.Relation Bank Bank
153+crossR = R.fromF' cross
154+
155+-- | Initial state, everyone in the left bank
156+locationLeft :: Being -> Bank
157+locationLeft _ = LeftB
158+
159+locationLeftR :: R.Relation Being Bank
160+locationLeftR = R.fromF' locationLeft
161+
162+-- | Initial state, everyone in the right bank
163+locationRight :: Being -> Bank
164+locationRight _ = RightB
165+
166+locationRightR :: R.Relation Being Bank
167+locationRightR = R.fromF' locationRight
168+
169+-- Properties
170+
171+-- Being at the same bank
172+sameBank :: R.Relation Being Bank -> R.Relation Being Being
173+sameBank = R.ker
174+
175+-- Risk of somebody eating somebody else
176+canEat :: R.Relation Being Bank -> R.Relation Being Being
177+canEat w = sameBank w `R.intersection` eatsR
178+
179+-- "Starvation" property.
180+inv :: R.Relation Being Bank -> Bool
181+inv w = (w `R.comp` canEat w) `R.sse` (w `R.comp` farmer)
182+ where
183+ farmer :: R.Relation Being Being
184+ farmer = R.fromF' (const Farmer)
185+
186+-- Arbitrary state
187+bankState :: Being -> Bank -> Bool
188+bankState Farmer LeftB = True
189+bankState Fox LeftB = True
190+bankState Goose RightB = True
191+bankState Beans RightB = True
192+bankState _ _ = False
193+
194+bankStateR :: R.Relation Being Bank
195+bankStateR = R.toRel bankState
196+
197+-- Main
198+
121199main :: IO ()
122200main = do
123201 putStrLn "Monty Hall Problem solution:"
@@ -132,6 +210,8 @@ main = do
132210 prettyPrint (grass_wet . state)
133211 putStrLn "\n Probability of rain:"
134212 prettyPrint (rainning . state)
213+ putStrLn "\n Is the arbitrary state a valid state? (Alcuin Puzzle)"
214+ print (inv bankStateR)
135215```
136216
137217```Shell
@@ -190,4 +270,7 @@ Monty Hall Problem solution:
190270┌ ┐
191271│ 0.2 │
192272└ ┘
273+
274+Is the arbitrary state a valid state? (Alcuin Puzzle)
275+False
193276```
Setup.hsdeleted−2
@@ -1,2 +0,0 @@
1−import Distribution.Simple
2−main = defaultMain
app/Main.hsdeleted−87
@@ -1,87 +0,0 @@
1−{-# LANGUAGE DeriveGeneric #-}
2−{-# LANGUAGE FlexibleContexts #-}
3−{-# LANGUAGE TypeOperators #-}
4−{-# LANGUAGE TypeApplications #-}
5−{-# LANGUAGE DataKinds #-}
6−
7−module Main where
8−
9−import LAoP.Matrix.Type
10−import LAoP.Utils
11−import LAoP.Dist
12−import GHC.TypeLits
13−import Data.Coerce
14−import GHC.Generics
15−import Control.Category hiding (id)
16−import Prelude hiding ((.))
17−
18−-- Monty Hall Problem
19−data Outcome = Win | Lose
20− deriving (Bounded, Enum, Eq, Show, Generic)
21−
22−switch :: Outcome -> Outcome
23−switch Win = Lose
24−switch Lose = Win
25−
26−firstChoice :: Matrix Double () Outcome
27−firstChoice = col [1/3, 2/3]
28−
29−secondChoice :: Matrix Double Outcome Outcome
30−secondChoice = fromF' switch
31−
32−-- Dice sum
33−
34−type SS = Natural 1 6 -- Sample Space
35−
36−sumSS :: SS -> SS -> Natural 2 12
37−sumSS = coerceNat (+)
38−
39−sumSSM = fromF' (uncurry sumSS)
40−
41−condition :: (Int, Int) -> Int -> Int
42−condition (fst, snd) thrd = if fst == snd
43− then fst * 3
44− else fst + snd + thrd
45−
46−conditionSS :: (SS, SS) -> SS -> Natural 3 18
47−conditionSS = coerceNat2 condition
48−
49−conditionalThrows = fromF' (uncurry conditionSS) . khatri (khatri die die) die
50−
51−die :: Matrix Double () SS
52−die = col $ map (const (1/6)) [nat @1 @6 1 .. nat 6]
53−
54−-- Sprinkler
55−
56−rain :: Matrix Double () Bool
57−rain = col [0.8, 0.2]
58−
59−sprinkler :: Matrix Double Bool Bool
60−sprinkler = fromLists [[0.6, 0.99], [0.4, 0.01]]
61−
62−grass :: Matrix Double (Bool, Bool) Bool
63−grass = fromLists [[1, 0.2, 0.1, 0.01], [0, 0.8, 0.9, 0.99]]
64−
65−state :: Matrix Double () (Bool, (Bool, Bool))
66−state = khatri grass identity . khatri sprinkler identity . rain
67−
68−grass_wet :: Matrix Double (Bool, (Bool, Bool)) One
69−grass_wet = row [0,1] . kp1
70−
71−rainning :: Matrix Double (Bool, (Bool, Bool)) One
72−rainning = row [0,1] . kp2 . kp2
73−
74−main :: IO ()
75−main = do
76− putStrLn "Monty Hall Problem solution:"
77− prettyPrint (secondChoice . firstChoice)
78− putStrLn "\n Sum of dices probability:"
79− prettyPrint (sumSSM `comp` khatri die die)
80− putStrLn "\n Conditional dice throw:"
81− prettyPrint conditionalThrows
82− putStrLn "\n Checking that the last result is indeed a distribution: "
83− prettyPrint (bang . sumSSM . khatri die die)
84− putStrLn "\n Probability of grass being wet:"
85− prettyPrint (grass_wet . state)
86− putStrLn "\n Probability of rain:"
87− prettyPrint (rainning . state)
appveyor.ymlnew file+34
@@ -0,0 +1,34 @@
1+clone_folder: "c:\\WORK"
2+clone_depth: 5
3+
4+# Do not build feature branch with open Pull Requests
5+skip_branch_with_pr: true
6+
7+platform:
8+ - x86_64
9+
10+cache:
11+ - "C:\\SR"
12+ - dist-newstyle
13+
14+environment:
15+ global:
16+ CABOPTS: --store-dir=C:\\SR
17+
18+ matrix:
19+ - GHCVER: 8.6.5
20+
21+install:
22+ - choco source add -n mistuke -s https://www.myget.org/F/mistuke/api/v2
23+ - choco install -y cabal --version 2.4.1.0
24+ - choco install -y ghc --version 8.6.3
25+ - refreshenv
26+
27+before_build:
28+ - cabal --version
29+ - ghc --version
30+ - cabal %CABOPTS% v2-update
31+
32+build_script:
33+ - cabal %CABOPTS% v2-build --enable-tests
34+ - cabal %CABOPTS% v2-test --enable-tests
benchmark/Main.hsnew file+175
@@ -0,0 +1,175 @@
1+{-# LANGUAGE KindSignatures #-}
2+{-# LANGUAGE GeneralizedNewtypeDeriving #-}
3+{-# LANGUAGE DerivingVia #-}
4+{-# LANGUAGE DataKinds #-}
5+{-# LANGUAGE BangPatterns #-}
6+{-# LANGUAGE TypeApplications #-}
7+{-# LANGUAGE FlexibleContexts #-}
8+{-# LANGUAGE AllowAmbiguousTypes #-}
9+{-# LANGUAGE ScopedTypeVariables #-}
10+
11+module Main (main) where
12+
13+import LAoP.Dist.Internal
14+import LAoP.Utils
15+import LAoP.Matrix.Type hiding (CountableN, Countable, FLN)
16+import qualified LAoP.Matrix.Type as T (FLN)
17+import Criterion.Main
18+import Control.DeepSeq
19+import Test.QuickCheck
20+import GHC.TypeLits
21+import Data.Proxy
22+import Prelude hiding (id, (.))
23+
24+selectM2 ::
25+ ( Num e,
26+ T.FLN b b,
27+ CountableN b
28+ ) => Matrix e cols (Either a b) -> Matrix e a b -> Matrix e cols b
29+selectM2 m y = join y iden `comp` m
30+
31+selectD2 ::
32+ ( FLN b b,
33+ CountableN b
34+ ) => Dist (Either a b) -> Matrix Prob a b -> Dist b
35+selectD2 (D d) m = D (join m iden `comp` d)
36+
37+-- Composition with iden
38+compId m = comp iden m
39+
40+randomDist :: forall a . (Countable a, FLN () a) => Gen (Dist a)
41+randomDist = do
42+ let size = fromInteger (natVal (Proxy :: Proxy (Count a)))
43+ l <- vectorOf size (arbitrary :: Gen Prob)
44+ let ln = normalize l
45+ lr = map (:[]) ln
46+ m = fromLists lr
47+ return (D m)
48+
49+randomMatrix :: forall a b . (CountableDims a b, FLN a b) => Gen (Matrix Prob a b)
50+randomMatrix = do
51+ let cols = fromInteger (natVal (Proxy :: Proxy (Count a)))
52+ rows = fromInteger (natVal (Proxy :: Proxy (Count b)))
53+ l <- vectorOf (cols * rows) arbitrary
54+ let lr = buildList l cols
55+ m = fromLists lr
56+ return m
57+
58+buildList [] _ = []
59+buildList l r = take r l : buildList (drop r l) r
60+
61+normalize :: [Prob] -> [Prob]
62+normalize l = let l' = map abs l
63+ s = sum l'
64+ in map (/ s) l'
65+
66+-- Probability
67+newtype Probability = P Double
68+ deriving (Num, Show, Fractional, NFData) via Double
69+newtype Dist' a = D' { unD :: [(a,Probability)] }
70+ deriving (Show, NFData)
71+
72+instance Functor Dist' where
73+ fmap f (D' d) = D' [(f x,p) | (x,p) <- d]
74+
75+instance Applicative Dist' where
76+ pure x = D' [(x, 1)]
77+ fm <*> m = D' [(f x,q*p) | (f,p) <- unD fm, (x,q) <- unD m]
78+
79+class Applicative f => Selective f where
80+ select :: f (Either a b) -> f (a -> b) -> f b
81+
82+instance Selective Dist' where
83+ select x y = (\e f -> either f id e) <$> x <*> y -- selectA
84+
85+instance Monad Dist' where
86+ return = pure
87+ (D' d) >>= f = D' [(y,q*p) | (x,p) <- d, (y,q) <- unD (f x)]
88+
89+normalize2 :: forall a . (Enum a, Bounded a) => [Probability] -> [(a, Probability)]
90+normalize2 l = let l' = map abs l
91+ as = [minBound .. maxBound]
92+ s = sum l'
93+ probs = map (/ s) l'
94+ in zip as probs
95+
96+randomDist2 :: forall a . (Countable a, Enum a, Bounded a) => Gen (Dist' a)
97+randomDist2 = do
98+ let size = fromInteger (natVal (Proxy :: Proxy (Count a)))
99+ l <- vectorOf size (arbitrary :: Gen Prob)
100+ let ln = normalize2 @a (map P l)
101+ return (D' ln)
102+
103+normalize3 :: forall a . [a] -> [Probability] -> [(a, Probability)]
104+normalize3 as l = let s = sum l
105+ probs = map (/ s) l
106+ in zip as probs
107+
108+randomDistF :: forall a b . (CountableDims a b, CoArbitrary a, Arbitrary b) => Gen (Dist' (a -> b))
109+randomDistF = do
110+ let a = fromInteger (natVal (Proxy :: Proxy (Count a)))
111+ b = fromInteger (natVal (Proxy :: Proxy (Count b)))
112+ size = a * b
113+ l <- vectorOf size (arbitrary :: Gen Prob)
114+ l2 <- vectorOf size (arbitrary :: Gen (a -> b))
115+ let !ln = normalize3 l2 (map P l)
116+ return (D' ln)
117+
118+instance CoArbitrary (Natural a b)
119+
120+instance forall (a :: Nat) (b :: Nat). (KnownNat a, KnownNat b) => Arbitrary (Natural a b)
121+ where
122+ arbitrary =
123+ let bottom = fromInteger (natVal (Proxy :: Proxy a))
124+ top = fromInteger (natVal (Proxy :: Proxy b))
125+ in do
126+ x <- arbitrary `suchThat` (\n -> n >= bottom && n <= top)
127+ return (nat x)
128+
129+setupEnv = do
130+ m11 <- generate (resize 1 (randomMatrix @(Natural 0 10) @(Natural 0 10) ))
131+ m12 <- generate (resize 1 (randomMatrix @(Natural 0 10) @(Natural 0 10) ))
132+ m21 <- generate (resize 1 (randomMatrix @(Natural 0 100) @(Natural 0 100) ))
133+ m22 <- generate (resize 1 (randomMatrix @(Natural 0 100) @(Natural 0 100) ))
134+ m31 <- generate (resize 1 (randomMatrix @(Natural 0 200) @(Natural 0 200) ))
135+ m32 <- generate (resize 1 (randomMatrix @(Natural 0 200) @(Natural 0 200) ))
136+ return (m11, m12, m21, m22, m31, m32)
137+
138+setupEnv2 = do
139+ m21 <- generate (resize 1 (randomMatrix @(Natural 0 100) @(Natural 0 100) ))
140+ m40 <- generate (resize 1 (randomMatrix @(Natural 0 100) @(Either (Natural 0 100) (Natural 0 100) )))
141+ dist <- generate (resize 1 (randomDist @(Either (Natural 0 100) (Natural 0 100)) ))
142+ dist2 <- generate (resize 1 (randomMatrix @(Natural 0 100) @(Natural 0 100) ))
143+ distList1 <- generate (resize 1 (randomDist2 @(Either (Natural 0 100) (Natural 0 100))))
144+ distList2 <- generate (resize 1 (randomDistF @(Natural 0 100) @(Natural 0 100)))
145+ return (m21, m40, dist, dist2, distList1, distList2)
146+
147+main :: IO ()
148+main = defaultMain [
149+ env setupEnv $ \ ~(m11, m12, m21, m22, m31, m32) -> bgroup "Matrix Composition" [
150+ bgroup "10x10" [
151+ bench "WHNF - 10x10" $ whnf (comp m11) m12
152+ , bench "NF - 10x10" $ nf (comp m11) m12
153+ ],
154+ bgroup "100x100" [
155+ bench "WHNF - 100x100" $ whnf (comp m21) m22
156+ , bench "NF - 100x100" $ nf (comp m21) m22
157+ ],
158+ bgroup "200x200" [
159+ bench "WHNF - 200x200" $ whnf (comp m31) m32
160+ , bench "NF - 200x200" $ nf (comp m31) m32
161+ ],
162+ bgroup "200x200 - RULES" [
163+ bench "No rules - 200x200" $ nf (comp m21) iden
164+ , bench "Rules - 200x200" $ nf compId m21
165+ ] ],
166+ env setupEnv2 $ \ ~(m21, m40, dist, dist2, dl1, dl2) -> bgroup "Matrix vs List - `select`" [
167+ bgroup "Distribution `select` - 100+100 / 100x100" [
168+ bench "List Distribution - Applicative version" $ nf (select dl1) dl2
169+ , bench "Matrix Distribution - Applicative version" $ nf (selectD2 dist) dist2
170+ , bench "Matrix Distribution - Selective version" $ nf (selectD dist) dist2
171+ ],
172+ bgroup "Matrix `select` - 100x(100+100) / 100x100" [
173+ bench "Applicative version" $ nf (selectM2 m40) m21
174+ , bench "Selective version" $ nf (selectM m40) m21
175+ ] ] ]
laop.cabalnew file+89
@@ -0,0 +1,89 @@
1+cabal-version: 2.4
2+name: laop
3+version: 0.1.1.1
4+synopsis: Matrix programming library
5+description: Matrix programming library that uses a type-safe inductive definition
6+ inspired by the Linear Algebra of Programming
7+homepage: https://github.com/bolt12/laop
8+bug-reports: https://github.com/bolt12/laop/issues
9+license: MIT
10+license-file: LICENSE
11+author: Armando Santos
12+maintainer: Armando Santos <armandoifsantos@gmail.com>
13+copyright: 2020 Armando Santos
14+category: Data
15+build-type: Simple
16+extra-doc-files: README.md
17+ CHANGELOG.md
18+tested-with: GHC == 8.6.5
19+ GHC == 8.8.3
20+
21+source-repository head
22+ type: git
23+ location: https://github.com/bolt12/laop.git
24+
25+common common-options
26+ build-depends: base >= 4.12.0.0 && < 5,
27+ deepseq
28+
29+ ghc-options: -Wall
30+ -Wcompat
31+ -Widentities
32+ -Wincomplete-uni-patterns
33+ -Wincomplete-record-updates
34+ if impl(ghc >= 8.0)
35+ ghc-options: -Wredundant-constraints
36+ if impl(ghc >= 8.2)
37+ ghc-options: -fhide-source-paths
38+ if impl(ghc >= 8.4)
39+ ghc-options: -Wmissing-export-lists
40+ -Wpartial-fields
41+ if impl(ghc >= 8.8)
42+ ghc-options: -Wmissing-deriving-strategies
43+
44+ default-language: Haskell2010
45+
46+library
47+ import: common-options
48+ hs-source-dirs: src
49+ exposed-modules: LAoP.Dist
50+ LAoP.Dist.Internal
51+ LAoP.Matrix.Internal
52+ LAoP.Matrix.Nat
53+ LAoP.Matrix.Type
54+ LAoP.Relation
55+ LAoP.Relation.Internal
56+ LAoP.Utils
57+ LAoP.Utils.Internal
58+
59+test-suite laop-test
60+ import: common-options
61+ type: exitcode-stdio-1.0
62+ hs-source-dirs: test
63+ other-modules: Examples.Readme
64+ main-is: Spec.hs
65+ build-depends: laop
66+ ghc-options: -threaded
67+ -rtsopts
68+ -with-rtsopts=-N
69+ -funfolding-use-threshold=16
70+ -fexcess-precision
71+ -optc-O3
72+ -optc-ffast-math
73+
74+benchmark laop-benchmark
75+ import: common-options
76+ type: exitcode-stdio-1.0
77+ hs-source-dirs: benchmark
78+ main-is: Main.hs
79+ build-depends: criterion
80+ , QuickCheck
81+ , deepseq
82+ , laop
83+ ghc-options: -threaded
84+ -rtsopts
85+ -with-rtsopts=-N
86+ -funfolding-use-threshold=16
87+ -fexcess-precision
88+ -optc-O3
89+ -optc-ffast-math
package.yamldeleted−48
@@ -1,48 +0,0 @@
1−name: laop
2−version: 0.1.0.0
3−github: "bolt12/laop"
4−license: BSD3
5−author: "Armando Santos"
6−maintainer: "armandoifsantos@gmail.com"
7−copyright: "MIT"
8−
9−extra-source-files:
10−- README.md
11−- ChangeLog.md
12−
13−# Metadata used when publishing your package
14−# synopsis: Short description of your package
15−# category: Web
16−
17−# To avoid duplicated efforts in documentation and dealing with the
18−# complications of embedding Haddock markup inside cabal files, it is
19−# common to point users to the README.md file.
20−description: Please see the README on GitHub at <https://github.com/bolt12/laop#readme>
21−
22−dependencies:
23−- base >= 4.7 && < 5
24−
25−library:
26− source-dirs: src
27−
28−executables:
29− laop-exe:
30− main: Main.hs
31− source-dirs: app
32− ghc-options:
33− - -threaded
34− - -rtsopts
35− - -with-rtsopts=-N
36− dependencies:
37− - laop
38−
39−tests:
40− laop-test:
41− main: Spec.hs
42− source-dirs: test
43− ghc-options:
44− - -threaded
45− - -rtsopts
46− - -with-rtsopts=-N
47− dependencies:
48− - laop
src/LAoP/Dist.hs+10
@@ -36,6 +36,14 @@ module LAoP.Dist
3636 Dist (..),
3737 Prob,
3838
39+ -- * Constraint type synonyms
40+ Countable,
41+ CountableN,
42+ CountableDimsN,
43+ FLN,
44+ Liftable,
45+ TrivialP,
46+
3947 -- * Functor instance equivalent functions
4048 fmapD,
4149
@@ -45,6 +53,8 @@ module LAoP.Dist
4553
4654 -- * Selective equivalent functions
4755 selectD,
56+ branchD,
57+ ifD,
4858
4959 -- * Monad equivalent functions
5060 returnD,
src/LAoP/Dist/Internal.hs+87−36
@@ -1,3 +1,5 @@
1+{-# LANGUAGE DerivingVia #-}
2+{-# LANGUAGE ConstraintKinds #-}
13{-# LANGUAGE GADTs #-}
24{-# LANGUAGE AllowAmbiguousTypes #-}
35{-# LANGUAGE TypeApplications #-}
@@ -8,18 +10,27 @@
810{-# LANGUAGE RankNTypes #-}
911
1012module LAoP.Dist.Internal
11− (
13+ (
1214 Dist(..),
1315 Prob,
1416
17+ Countable,
18+ CountableN,
19+ CountableDimsN,
20+ FLN,
21+ Liftable,
22+ TrivialP,
23+
1524 fmapD,
1625 unitD,
1726 multD,
1827 selectD,
28+ branchD,
29+ ifD,
1930 returnD,
2031 bindD,
2132 (??),
22−
33+
2334 choose,
2435 shape,
2536 linear,
@@ -32,11 +43,15 @@ module LAoP.Dist.Internal
3243 )
3344 where
3445
35−import LAoP.Matrix.Type
46+import LAoP.Matrix.Type hiding (TrivialP, Countable, CountableDims, CountableN, CountableDimsN, Liftable, FLN)
47+import Prelude hiding (id, (.))
48+import qualified LAoP.Matrix.Internal as I
3649import LAoP.Utils
3750import GHC.TypeLits
3851import Data.Proxy
3952import Data.List (sortBy)
53+import Control.DeepSeq
54+import Data.Bool
4055
4156-- | Type synonym for probability value
4257type Prob = Double
@@ -44,17 +59,21 @@ type Prob = Double
4459-- | Type synonym for column vector matrices. This represents a probability
4560-- distribution.
4661newtype Dist a = D (Matrix Prob () a)
62+ deriving (Show, Num, Eq, Ord, NFData) via (Matrix Prob () a)
63+
64+-- | Constraint type synonyms to keep the type signatures less convoluted
65+type Countable a = KnownNat (I.Count a)
66+type CountableN a = KnownNat (I.Count (I.Normalize a))
67+type CountableDimsN a b = (CountableN a, CountableN b)
68+type FLN a b = I.FL (I.Normalize a) (I.Normalize b)
69+type Liftable a b = (Bounded a, Bounded b, Enum a, Enum b, Eq b, Num Prob, Ord Prob)
70+type TrivialP a b = Normalize (a, b) ~ Normalize (Normalize a, Normalize b)
4771
4872-- | Functor instance
4973fmapD ::
50− ( Bounded a,
51− Bounded b,
52− Enum a,
53− Enum b,
54− Eq b,
55− KnownNat (Count (Normalize a)),
56− KnownNat (Count (Normalize b)),
57− FromLists Prob (Normalize b) (Normalize a)
74+ ( Liftable a b,
75+ CountableDimsN a b,
76+ FLN b a
5877 )
5978 =>
6079 (a -> b) -> Dist a -> Dist b
@@ -66,26 +85,58 @@ unitD = D (one 1)
6685
6786-- | Applicative/Monoidal instance 'mult' function
6887multD ::
69− ( KnownNat (Count (Normalize a)),
70− KnownNat (Count (Normalize b)),
71− KnownNat (Count (Normalize (a, b))),
72− FromLists Prob (Normalize (a, b)) (Normalize a),
73− FromLists Prob (Normalize (a, b)) (Normalize b),
74− Normalize (a, b) ~ Normalize (Normalize a, Normalize b)
88+ ( CountableDimsN a b,
89+ CountableN (a, b),
90+ FLN (a, b) a,
91+ FLN (a, b) b,
92+ TrivialP a b
7593 ) => Dist a -> Dist b -> Dist (a, b)
76−multD (D a) (D b) = D (khatri a b)
94+multD (D a) (D b) = D (kr a b)
7795
7896-- | Selective instance function
7997selectD ::
80− ( Normalize (Either a b) ~ Either (Normalize a) (Normalize b),
81− FromLists Prob (Normalize b) (Normalize b),
82− KnownNat (Count (Normalize b))
98+ ( FLN b b,
99+ CountableN b
83100 ) => Dist (Either a b) -> Matrix Prob a b -> Dist b
84−selectD (D d) m = D (junc m identity `comp` d)
85−
101+selectD (D d) m = D (selectM d m)
102+
103+-- | Chooses which of the two given effectful
104+-- functions to apply to a given argument;
105+branchD ::
106+ ( Num e,
107+ CountableDimsN a b,
108+ CountableDimsN c (Either b c),
109+ FLN c b,
110+ FLN a b,
111+ FLN a a,
112+ FLN b b,
113+ FLN c c,
114+ FLN b a,
115+ FLN b c,
116+ FLN (Either b c) b,
117+ FLN (Either b c) c
118+ )
119+ => Dist (Either a b) -> Matrix Prob a c -> Matrix Prob b c -> Dist c
120+branchD x l r = f x `selectD` g l `selectD` r
121+ where
122+ f (D m) = D (fork (tr i1) (i1 `comp` tr i2) `comp` m)
123+ g m = i2 `comp` m
124+
125+-- | Branch on a Boolean value, skipping unnecessary computations.
126+ifD ::
127+ ( CountableDimsN a (Either () a),
128+ FLN a a,
129+ FLN a (),
130+ FLN () a,
131+ FLN (Either () a) a
132+ )
133+ => Dist Bool -> Dist a -> Dist a -> Dist a
134+ifD x (D t) (D e) = branchD x' t e
135+ where
136+ x' = bool (Right ()) (Left ()) `fmapD` x
86137
87138-- | Monad instance 'return' function
88−returnD :: forall a . (Enum a, FromLists Prob () (Normalize a), KnownNat (Count a)) => a -> Dist a
139+returnD :: forall a . (Enum a, FLN () a, Countable a) => a -> Dist a
89140returnD a = D (col l)
90141 where
91142 i = fromInteger $ natVal (Proxy :: Proxy (Count a))
@@ -99,8 +150,8 @@ bindD (D d) m = D (m `comp` d)
99150-- | Extract probabilities given an Event.
100151(??) ::
101152 ( Enum a,
102− KnownNat (Count a),
103− FromLists Prob () (Normalize a)
153+ Countable a,
154+ FLN () a
104155 ) => (a -> Bool) -> Dist a -> Prob
105156(??) p d =
106157 let l = toValues d
@@ -110,11 +161,11 @@ bindD (D d) m = D (m `comp` d)
110161-- Distribution Construction
111162
112163-- | Constructs a Bernoulli distribution
113−choose :: (FromLists Prob () (Normalize a)) => Prob -> Dist a
164+choose :: (FLN () a) => Prob -> Dist a
114165choose prob = D (col [prob, 1 - prob])
115166
116167-- | Creates a distribution given a shape function
117−shape :: (FromLists Prob () (Normalize a)) => (Prob -> Prob) -> [a] -> Dist a
168+shape :: (FLN () a) => (Prob -> Prob) -> [a] -> Dist a
118169shape _ [] = error "Probability.shape: empty list"
119170shape f xs =
120171 let incr = 1 / fromIntegral (length xs - 1)
@@ -122,23 +173,23 @@ shape f xs =
122173 in fromFreqs (zip xs ps)
123174
124175-- | Constructs a Linear distribution
125−linear :: (FromLists Prob () (Normalize a)) => [a] -> Dist a
176+linear :: (FLN () a) => [a] -> Dist a
126177linear = shape id
127178
128179-- | Constructs an Uniform distribution
129−uniform :: (FromLists Prob () (Normalize a)) => [a] -> Dist a
180+uniform :: (FLN () a) => [a] -> Dist a
130181uniform = shape (const 1)
131182
132183-- | Constructs an Negative Exponential distribution
133−negExp :: (FromLists Prob () (Normalize a)) => [a] -> Dist a
184+negExp :: (FLN () a) => [a] -> Dist a
134185negExp = shape (\x -> exp (-x))
135186
136187-- | Constructs an Normal distribution
137−normal :: (FromLists Prob () (Normalize a)) => [a] -> Dist a
188+normal :: (FLN () a) => [a] -> Dist a
138189normal = shape (normalCurve 0.5 0.5)
139190
140191-- | Transforms a 'Dist' into a list of pairs.
141−toValues :: forall a . (Enum a, KnownNat (Count a), FromLists Prob () (Normalize a)) => Dist a -> [(a, Prob)]
192+toValues :: forall a . (Enum a, Countable a, FLN () a) => Dist a -> [(a, Prob)]
142193toValues (D d) =
143194 let rows = fromInteger (natVal (Proxy :: Proxy (Count a)))
144195 probs = toList d
@@ -146,7 +197,7 @@ toValues (D d) =
146197 in res
147198
148199-- | Pretty a distribution
149−prettyDist :: forall a. (Show a, Enum a, KnownNat (Count a), FromLists Prob () (Normalize a)) => Dist a -> String
200+prettyDist :: forall a. (Show a, Enum a, Countable a, FLN () a) => Dist a -> String
150201prettyDist d =
151202 let values = sortBy (\(a, p1) (b, p2) -> compare p2 p1) (toValues @a d)
152203 w = maximum (map (length . show . fst) values)
@@ -158,12 +209,12 @@ prettyDist d =
158209 showR n x = show x ++ " "
159210
160211-- | Pretty Print a distribution
161−prettyPrintDist :: forall a . (Show a, Enum a, KnownNat (Count a), FromLists Prob () (Normalize a)) => Dist a -> IO ()
212+prettyPrintDist :: forall a . (Show a, Enum a, Countable a, FLN () a) => Dist a -> IO ()
162213prettyPrintDist = putStrLn . prettyDist @a
163214
164215-- Auxiliary functions
165216
166−fromFreqs :: (FromLists Prob () (Normalize a)) => [(a,Prob)] -> Dist a
217+fromFreqs :: (FLN () a) => [(a,Prob)] -> Dist a
167218fromFreqs xs = D (col (map (\(x,p) -> p/q) xs))
168219 where q = sum $ map snd xs
169220
src/LAoP/Matrix/Internal.hs+487−412
@@ -1,3 +1,6 @@
1+{-# LANGUAGE StrictData #-}
2+{-# LANGUAGE TypeFamilyDependencies #-}
3+{-# LANGUAGE ConstraintKinds #-}
14{-# LANGUAGE AllowAmbiguousTypes #-}
25{-# LANGUAGE DataKinds #-}
36{-# LANGUAGE FlexibleContexts #-}
@@ -9,7 +12,6 @@
912{-# LANGUAGE ScopedTypeVariables #-}
1013{-# LANGUAGE StandaloneDeriving #-}
1114{-# LANGUAGE TypeApplications #-}
12−{-# LANGUAGE TypeFamilies #-}
1315{-# LANGUAGE TypeOperators #-}
1416{-# LANGUAGE UndecidableInstances #-}
1517
@@ -28,7 +30,7 @@
2830-- motivation behind the library, the underlying theory, and implementation details.
2931--
3032-- This module offers many of the combinators mentioned in the work of
31−-- Macedo (2012) and Oliveira (2012).
33+-- Macedo (2012) and Oliveira (2012).
3234--
3335-- This is an Internal module and it is no supposed to be imported.
3436--
@@ -41,17 +43,26 @@ module LAoP.Matrix.Internal
4143 --
4244 -- There exists two type families that make it easier to write
4345 -- matrix dimensions: 'FromNat' and 'Count'. This approach
44− -- leads to a very straightforward implementation
45− -- of LAoP combinators.
46+ -- leads to a very straightforward implementation
47+ -- of LAoP combinators.
4648
4749 -- * Type safe matrix representation
4850 Matrix (..),
4951
52+ -- * Constraint type aliases
53+ Countable,
54+ CountableDims,
55+ CountableN,
56+ CountableDimsN,
57+ FL,
58+ FLN,
59+ Liftable,
60+ Trivial,
61+
5062 -- * Primitives
51− empty,
5263 one,
53− junc,
54− split,
64+ join,
65+ fork,
5566
5667 -- * Auxiliary type families
5768 FromNat,
@@ -64,6 +75,7 @@ module LAoP.Matrix.Internal
6475 toLists,
6576 toList,
6677 matrixBuilder,
78+ matrixBuilder',
6779 row,
6880 col,
6981 zeros,
@@ -74,28 +86,38 @@ module LAoP.Matrix.Internal
7486 -- * Misc
7587 -- ** Get dimensions
7688 columns,
89+ columns',
7790 rows,
91+ rows',
7892
7993 -- ** Matrix Transposition
8094 tr,
8195
96+ -- ** Scalar multiplication/division of matrices
97+ (.|),
98+ (./),
99+
82100 -- ** Selective operator
83− select,
101+ select,
102+ branch,
84103
85104 -- ** McCarthy's Conditional
86105 cond,
87106
88107 -- ** Matrix "abiding"
89− abideJS,
90− abideSJ,
108+ abideJF,
109+ abideFJ,
110+
111+ -- ** Zip matrices
112+ zipWithM,
91113
92114 -- * Biproduct approach
93− -- ** Split
115+ -- ** Fork
94116 (===),
95117 -- *** Projections
96118 p1,
97119 p2,
98− -- ** Junc
120+ -- ** Join
99121 (|||),
100122 -- *** Injections
101123 i1,
@@ -108,12 +130,13 @@ module LAoP.Matrix.Internal
108130
109131 -- | Note that given the restrictions imposed it is not possible to
110132 -- implement the standard type classes present in standard Haskell.
133+
111134 -- *** Matrix pairing projections
112− kp1,
113− kp2,
135+ fstM,
136+ sndM,
114137
115138 -- *** Matrix pairing
116− khatri,
139+ kr,
117140
118141 -- * Matrix composition and lifting
119142
@@ -121,10 +144,10 @@ module LAoP.Matrix.Internal
121144
122145 -- | Note that given the restrictions imposed it is not possible to
123146 -- implement the standard type classes present in standard Haskell.
124− identity,
147+ iden,
125148 comp,
126− fromF,
127149 fromF',
150+ fromF,
128151
129152 -- * Matrix printing
130153 pretty,
@@ -134,33 +157,39 @@ module LAoP.Matrix.Internal
134157 toBool,
135158 fromBool,
136159 compRel,
160+ divR,
161+ divL,
162+ divS,
137163 fromFRel,
138164 fromFRel',
165+ toRel,
166+ negateM,
139167 orM,
140168 andM,
141169 subM
142170 )
143171 where
144172
145−import LAoP.Utils
173+import LAoP.Utils.Internal
146174import Data.Bool
147175import Data.Kind
148176import Data.List
177+import Data.Maybe
149178import Data.Proxy
179+import Data.Typeable
150180import Data.Void
151181import GHC.TypeLits
152182import Data.Type.Equality
153183import GHC.Generics
154184import Control.DeepSeq
155−import Control.Category
156−import Prelude hiding ((.))
185+import Prelude hiding (id, (.))
186+import qualified Prelude (id, (.))
157187
158188-- | LAoP (Linear Algebra of Programming) Inductive Matrix definition.
159189data Matrix e cols rows where
160− Empty :: Matrix e Void Void
161190 One :: e -> Matrix e () ()
162− Junc :: Matrix e a rows -> Matrix e b rows -> Matrix e (Either a b) rows
163− Split :: Matrix e cols a -> Matrix e cols b -> Matrix e cols (Either a b)
191+ Join :: Matrix e a rows -> Matrix e b rows -> Matrix e (Either a b) rows
192+ Fork :: Matrix e cols a -> Matrix e cols b -> Matrix e cols (Either a b)
164193
165194deriving instance (Show e) => Show (Matrix e cols rows)
166195
@@ -170,221 +199,214 @@ deriving instance (Show e) => Show (Matrix e cols rows)
170199-- 'Generic' instance.
171200type family Count (d :: Type) :: Nat where
172201 Count (Natural n m) = (m - n) + 1
173− Count (Either a b) = (+) (Count a) (Count b)
174− Count (a, b) = (*) (Count a) (Count b)
175− Count (a -> b) = (^) (Count b) (Count a)
202+ Count (List a) = (^) 2 (Count a)
203+ Count (Either a b) = (+) (Count a) (Count b)
204+ Count (a, b) = (*) (Count a) (Count b)
205+ Count (a -> b) = (^) (Count b) (Count a)
176206 -- Generics
177− Count (M1 _ _ f p) = Count (f p)
178− Count (K1 _ _ _) = 1
179− Count (V1 _) = 0
180− Count (U1 _) = 1
207+ Count (M1 _ _ f p) = Count (f p)
208+ Count (K1 _ _ _) = 1
209+ Count (V1 _) = 0
210+ Count (U1 _) = 1
181211 Count ((:*:) a b p) = Count (a p) * Count (b p)
182212 Count ((:+:) a b p) = Count (a p) + Count (b p)
183− Count d = Count (Rep d R)
213+ Count d = Count (Rep d R)
184214
185215-- | Type family that computes of a given type dimension from a given natural
186216--
187217-- Thanks to Li-Yao Xia this type family is super fast.
188218type family FromNat (n :: Nat) :: Type where
189− FromNat 0 = Void
190219 FromNat 1 = ()
191220 FromNat n = FromNat' (Mod n 2 == 0) (FromNat (Div n 2))
192221
193222type family FromNat' (b :: Bool) (m :: Type) :: Type where
194− FromNat' 'True m = Either m m
223+ FromNat' 'True m = Either m m
195224 FromNat' 'False m = Either () (Either m m)
196225
197226-- | Type family that normalizes the representation of a given data
198227-- structure
199228type family Normalize (d :: Type) :: Type where
200− Normalize d = FromNat (Count d)
201−
202−-- | It isn't possible to implement the 'id' function so it's
203−-- implementation is 'undefined'. However 'comp' can be and this partial
204−-- class implementation exists just to make the code more readable.
205−--
206−-- Please use 'identity' instead.
229+ Normalize (Either a b) = Either (Normalize a) (Normalize b)
230+ Normalize d = FromNat (Count d)
231+
232+-- | Constraint type synonyms to keep the type signatures less convoluted
233+type Countable a = KnownNat (Count a)
234+type CountableN a = KnownNat (Count (Normalize a))
235+type CountableDims a b = (Countable a, Countable b)
236+type CountableDimsN a b = (CountableN a, CountableN b)
237+type FL a b = FromLists a b
238+type FLN a b = FromLists (Normalize a) (Normalize b)
239+type Liftable e a b = (Bounded a, Bounded b, Enum a, Enum b, Eq b, Num e, Ord e)
240+type Trivial a = FromNat (Count a) ~ a
241+
242+-- | It is possible to implement a constrained version of the category type
243+-- class.
207244instance (Num e) => Category (Matrix e) where
208− id = undefined
209− (.) = comp
245+ type Object (Matrix e) a = (FL a a, Countable a)
246+ id = iden
247+ (.) = comp
210248
211249instance NFData e => NFData (Matrix e cols rows) where
212− rnf Empty = ()
213− rnf (One e) = rnf e
214− rnf (Junc a b) = rnf a `seq` rnf b
215− rnf (Split a b) = rnf a `seq` rnf b
250+ rnf (One e) = rnf e
251+ rnf (Join a b) = rnf a `seq` rnf b
252+ rnf (Fork a b) = rnf a `seq` rnf b
216253
217254instance Eq e => Eq (Matrix e cols rows) where
218− Empty == Empty = True
219− (One a) == (One b) = a == b
220− (Junc a b) == (Junc c d) = a == c && b == d
221− (Split a b) == (Split c d) = a == c && b == d
222− x@(Split _ _) == y@(Junc _ _) = x == abideJS y
223− x@(Junc _ _) == y@(Split _ _) = abideJS x == y
255+ (One a) == (One b) = a == b
256+ (Join a b) == (Join c d) = a == c && b == d
257+ (Fork a b) == (Fork c d) = a == c && b == d
258+ x@(Fork _ _) == y@(Join _ _) = x == abideJF y
259+ x@(Join _ _) == y@(Fork _ _) = abideJF x == y
224260
225261instance 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
226267
227− Empty + Empty = Empty
228− (One a) + (One b) = One (a + b)
229− (Junc a b) + (Junc c d) = Junc (a + c) (b + d)
230− (Split a b) + (Split c d) = Split (a + c) (b + d)
231− x@(Split _ _) + y@(Junc _ _) = x + abideJS y
232− x@(Junc _ _) + y@(Split _ _) = abideJS x + y
233−
234− Empty - Empty = Empty
235− (One a) - (One b) = One (a - b)
236− (Junc a b) - (Junc c d) = Junc (a - c) (b - d)
237− (Split a b) - (Split c d) = Split (a - c) (b - d)
238− x@(Split _ _) - y@(Junc _ _) = x - abideJS y
239− x@(Junc _ _) - y@(Split _ _) = abideJS x - y
240−
241− Empty * Empty = Empty
242− (One a) * (One b) = One (a * b)
243− (Junc a b) * (Junc c d) = Junc (a * c) (b * d)
244− (Split a b) * (Split c d) = Split (a * c) (b * d)
245− x@(Split _ _) * y@(Junc _ _) = x * abideJS y
246− x@(Junc _ _) * y@(Split _ _) = abideJS x * y
247−
248− abs Empty = Empty
249− abs (One a) = One (abs a)
250− abs (Junc a b) = Junc (abs a) (abs b)
251− abs (Split a b) = Split (abs a) (abs b)
252−
253− signum Empty = Empty
254− signum (One a) = One (signum a)
255− signum (Junc a b) = Junc (signum a) (signum b)
256− signum (Split a b) = Split (signum a) (signum b)
268+ abs (One a) = One (abs a)
269+ abs (Join a b) = Join (abs a) (abs b)
270+ abs (Fork a b) = Fork (abs a) (abs b)
271+
272+ signum (One a) = One (signum a)
273+ signum (Join a b) = Join (signum a) (signum b)
274+ signum (Fork a b) = Fork (signum a) (signum b)
257275
258276instance Ord e => Ord (Matrix e cols rows) where
259− Empty <= Empty = True
260− (One a) <= (One b) = a <= b
261− (Junc a b) <= (Junc c d) = (a <= c) && (b <= d)
262− (Split a b) <= (Split c d) = (a <= c) && (b <= d)
263− x@(Split _ _) <= y@(Junc _ _) = x <= abideJS y
264− x@(Junc _ _) <= y@(Split _ _) = abideJS x <= y
277+ (One a) <= (One b) = a <= b
278+ (Join a b) <= (Join c d) = (a <= c) && (b <= d)
279+ (Fork a b) <= (Fork c d) = (a <= c) && (b <= d)
280+ x@(Fork _ _) <= y@(Join _ _) = x <= abideJF y
281+ x@(Join _ _) <= y@(Fork _ _) = abideJF x <= y
265282
266283-- Primitives
267284
268−-- | Empty matrix constructor
269−empty :: Matrix e Void Void
270−empty = Empty
271−
272285-- | Unit matrix constructor
273286one :: e -> Matrix e () ()
274287one = One
275288
276−-- | Matrix 'Junc' constructor
277−junc :: Matrix e a rows -> Matrix e b rows -> Matrix e (Either a b) rows
278−junc = Junc
289+-- | Matrix 'Join' constructor
290+join :: Matrix e a rows -> Matrix e b rows -> Matrix e (Either a b) rows
291+join = Join
279292
280293infixl 3 |||
281294
282−-- | Matrix 'Junc' constructor
295+-- | Matrix 'Join' constructor
283296(|||) :: Matrix e a rows -> Matrix e b rows -> Matrix e (Either a b) rows
284−(|||) = Junc
297+(|||) = Join
285298
286−-- | Matrix 'Split' constructor
287−split :: Matrix e cols a -> Matrix e cols b -> Matrix e cols (Either a b)
288−split = Split
299+-- | Matrix 'Fork' constructor
300+fork :: Matrix e cols a -> Matrix e cols b -> Matrix e cols (Either a b)
301+fork = Fork
289302
290303infixl 2 ===
291304
292−-- | Matrix 'Split' constructor
305+-- | Matrix 'Fork' constructor
293306(===) :: Matrix e cols a -> Matrix e cols b -> Matrix e cols (Either a b)
294−(===) = Split
307+(===) = Fork
295308
296309-- Construction
297310
298311-- | Type class for defining the 'fromList' conversion function.
299312--
300313-- Given that it is not possible to branch on types at the term level type
301−-- classes are needed bery much like an inductive definition but on types.
302−class FromLists e cols rows where
314+-- classes are needed very much like an inductive definition but on types.
315+class FromLists cols rows where
303316 -- | Build a matrix out of a list of list of elements. Throws a runtime
304317 -- error if the dimensions do not match.
305318 fromLists :: [[e]] -> Matrix e cols rows
306319
307−instance FromLists e Void Void where
308− fromLists [] = Empty
309− fromLists _ = error "Wrong dimensions"
310−
311−instance {-# OVERLAPPING #-} FromLists e () () where
320+instance FromLists () () where
312321 fromLists [[e]] = One e
313322 fromLists _ = error "Wrong dimensions"
314323
315−instance {-# OVERLAPPING #-} (FromLists e cols ()) => FromLists e (Either () cols) () where
316− fromLists [h : t] = Junc (One h) (fromLists [t])
324+instance (FromLists cols ()) => FromLists (Either () cols) () where
325+ fromLists [h : t] = Join (One h) (fromLists [t])
317326 fromLists _ = error "Wrong dimensions"
318327
319−instance {-# OVERLAPPABLE #-} (FromLists e a (), FromLists e b (), KnownNat (Count a)) => FromLists e (Either a b) () where
320− fromLists [l] =
328+instance {-# OVERLAPPABLE #-}
329+ (FromLists a (), FromLists b (), Countable a) => FromLists (Either a b) () where
330+ fromLists [l] =
321331 let rowsA = fromInteger (natVal (Proxy :: Proxy (Count a)))
322− in Junc (fromLists [take rowsA l]) (fromLists [drop rowsA l])
332+ in Join (fromLists [take rowsA l]) (fromLists [drop rowsA l])
323333 fromLists _ = error "Wrong dimensions"
324334
325−instance {-# OVERLAPPING #-} (FromLists e () rows) => FromLists e () (Either () rows) where
326− fromLists ([h] : t) = Split (One h) (fromLists t)
335+instance (FromLists () rows) => FromLists () (Either () rows) where
336+ fromLists ([h] : t) = Fork (One h) (fromLists t)
327337 fromLists _ = error "Wrong dimensions"
328338
329−instance {-# OVERLAPPABLE #-} (FromLists e () a, FromLists e () b, KnownNat (Count a)) => FromLists e () (Either a b) where
330− fromLists l@([_] : _) =
339+instance {-# OVERLAPPABLE #-}
340+ (FromLists () a, FromLists () b, Countable a) => FromLists () (Either a b) where
341+ fromLists l@([_] : _) =
331342 let rowsA = fromInteger (natVal (Proxy :: Proxy (Count a)))
332− in Split (fromLists (take rowsA l)) (fromLists (drop rowsA l))
343+ in Fork (fromLists (take rowsA l)) (fromLists (drop rowsA l))
333344 fromLists _ = error "Wrong dimensions"
334345
335−instance {-# OVERLAPPABLE #-} (FromLists e (Either a b) c, FromLists e (Either a b) d, KnownNat (Count c)) => FromLists e (Either a b) (Either c d) where
346+instance (FromLists (Either a b) c, FromLists (Either a b) d, Countable c)
347+ => FromLists (Either a b) (Either c d) where
336348 fromLists l@(h : t) =
337349 let lh = length h
338350 rowsC = fromInteger (natVal (Proxy :: Proxy (Count c)))
339− condition = all (== lh) (map length t)
351+ condition = all ((== lh) . length) t
340352 in if lh > 0 && condition
341− then Split (fromLists (take rowsC l)) (fromLists (drop rowsC l))
353+ then Fork (fromLists (take rowsC l)) (fromLists (drop rowsC l))
342354 else error "Not all rows have the same length"
343355
344356-- | Matrix builder function. Constructs a matrix provided with
345−-- a construction function.
346−matrixBuilder ::
357+-- a construction function that operates with indices.
358+matrixBuilder' ::
347359 forall e cols rows.
348− ( FromLists e cols rows,
349− KnownNat (Count cols),
350− KnownNat (Count rows)
351− ) =>
352− ((Int, Int) -> e) ->
353− Matrix e cols rows
354−matrixBuilder f =
360+ ( FL cols rows,
361+ CountableDims cols rows
362+ ) => ((Int, Int) -> e) -> Matrix e cols rows
363+matrixBuilder' f =
355364 let c = fromInteger $ natVal (Proxy :: Proxy (Count cols))
356365 r = fromInteger $ natVal (Proxy :: Proxy (Count rows))
357366 positions = [(a, b) | a <- [0 .. (r - 1)], b <- [0 .. (c - 1)]]
358367 in fromLists . map (map f) . groupBy (\(x, _) (w, _) -> x == w) $ positions
359368
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+
360389-- | Constructs a column vector matrix
361−col :: (FromLists e () rows) => [e] -> Matrix e () rows
390+col :: (FL () rows) => [e] -> Matrix e () rows
362391col = fromLists . map (: [])
363392
364393-- | Constructs a row vector matrix
365−row :: (FromLists e cols ()) => [e] -> Matrix e cols ()
394+row :: (FL cols ()) => [e] -> Matrix e cols ()
366395row = fromLists . (: [])
367396
368397-- | Lifts functions to matrices with arbitrary dimensions.
369398--
370399-- NOTE: Be careful to not ask for a matrix bigger than the cardinality of
371400-- types @a@ or @b@ allows.
372−fromF ::
401+fromF' ::
373402 forall a b cols rows e.
374− ( Bounded a,
375− Bounded b,
376− Enum a,
377− Enum b,
378− Eq b,
379− Num e,
380− Ord e,
381− KnownNat (Count cols),
382− KnownNat (Count rows),
383− FromLists e rows cols
403+ ( Liftable e a b,
404+ CountableDims cols rows,
405+ FL rows cols
384406 ) =>
385407 (a -> b) ->
386408 Matrix e cols rows
387−fromF f =
409+fromF' f =
388410 let minA = minBound @a
389411 maxA = maxBound @a
390412 minB = minBound @b
@@ -394,8 +416,8 @@ fromF f =
394416 elementsA = take ccols [minA .. maxA]
395417 elementsB = take rrows [minB .. maxB]
396418 combinations = (,) <$> elementsA <*> elementsB
397− combAp = map snd . sort . map (\(a, b) -> if f a == b
398− then ((fromEnum a, fromEnum b), 1)
419+ combAp = map snd . sort . map (\(a, b) -> if f a == b
420+ then ((fromEnum a, fromEnum b), 1)
399421 else ((fromEnum a, fromEnum b), 0)) $ combinations
400422 mList = buildList combAp rrows
401423 in tr $ fromLists mList
@@ -405,48 +427,23 @@ fromF f =
405427
406428-- | Lifts functions to matrices with dimensions matching @a@ and @b@
407429-- cardinality's.
408−fromF' ::
430+fromF ::
409431 forall a b e.
410− ( Bounded a,
411− Bounded b,
412− Enum a,
413− Enum b,
414− Eq b,
415− Num e,
416− Ord e,
417− KnownNat (Count (Normalize a)),
418− KnownNat (Count (Normalize b)),
419− FromLists e (Normalize b) (Normalize a)
432+ ( Liftable e a b,
433+ CountableDimsN a b,
434+ FLN b a
420435 ) =>
421436 (a -> b) ->
422437 Matrix e (Normalize a) (Normalize b)
423−fromF' f =
424− let minA = minBound @a
425− maxA = maxBound @a
426− minB = minBound @b
427− maxB = maxBound @b
428− ccols = fromInteger $ natVal (Proxy :: Proxy (Count (Normalize a)))
429− rrows = fromInteger $ natVal (Proxy :: Proxy (Count (Normalize b)))
430− elementsA = take ccols [minA .. maxA]
431− elementsB = take rrows [minB .. maxB]
432− combinations = (,) <$> elementsA <*> elementsB
433− combAp = map snd . sort . map (\(a, b) -> if f a == b
434− then ((fromEnum a, fromEnum b), 1)
435− else ((fromEnum a, fromEnum b), 0)) $ combinations
436− mList = buildList combAp rrows
437− in tr $ fromLists mList
438− where
439− buildList [] _ = []
440− buildList l r = take r l : buildList (drop r l) r
438+fromF = fromF'
441439
442440-- Conversion
443441
444442-- | Converts a matrix to a list of lists of elements.
445443toLists :: Matrix e cols rows -> [[e]]
446−toLists Empty = []
447444toLists (One e) = [[e]]
448−toLists (Split l r) = toLists l ++ toLists r
449−toLists (Junc l r) = zipWith (++) (toLists l) (toLists r)
445+toLists (Fork l r) = toLists l ++ toLists r
446+toLists (Join l r) = zipWith (++) (toLists l) (toLists r)
450447
451448-- | Converts a matrix to a list of elements.
452449toList :: Matrix e cols rows -> [e]
@@ -455,37 +452,38 @@ toList = concat . toLists
455452-- Zeros Matrix
456453
457454-- | The zero matrix. A matrix wholly filled with zeros.
458−zeros :: (Num e, FromLists e cols rows, KnownNat (Count cols), KnownNat (Count rows)) => Matrix e cols rows
459−zeros = matrixBuilder (const 0)
455+zeros :: (Num e, FL cols rows, CountableDims cols rows) => Matrix e cols rows
456+zeros = matrixBuilder' (const 0)
460457
461458-- Ones Matrix
462459
463460-- | The ones matrix. A matrix wholly filled with ones.
464461--
465462-- Also known as T (Top) matrix.
466−ones :: (Num e, FromLists e cols rows, KnownNat (Count cols), KnownNat (Count rows)) => Matrix e cols rows
467−ones = matrixBuilder (const 1)
463+ones :: (Num e, FL cols rows, CountableDims cols rows) => Matrix e cols rows
464+ones = matrixBuilder' (const 1)
468465
469466-- Const Matrix
470467
471468-- | The constant matrix constructor. A matrix wholly filled with a given
472469-- value.
473−constant :: (Num e, FromLists e cols rows, KnownNat (Count cols), KnownNat (Count rows)) => e -> Matrix e cols rows
474−constant e = matrixBuilder (const e)
470+constant :: (Num e, FL cols rows, CountableDims cols rows) => e -> Matrix e cols rows
471+constant e = matrixBuilder' (const e)
475472
476473-- Bang Matrix
477474
478475-- | The T (Top) row vector matrix.
479−bang :: forall e cols. (Num e, Enum e, FromLists e cols (), KnownNat (Count cols)) => Matrix e cols ()
476+bang :: forall e cols. (Num e, Enum e, FL cols (), Countable cols) => Matrix e cols ()
480477bang =
481478 let c = fromInteger $ natVal (Proxy :: Proxy (Count cols))
482479 in fromLists [take c [1, 1 ..]]
483480
484−-- Identity Matrix
481+-- iden Matrix
485482
486−-- | Identity matrix.
487−identity :: (Num e, FromLists e cols cols, KnownNat (Count cols)) => Matrix e cols cols
488−identity = matrixBuilder (bool 0 1 . uncurry (==))
483+-- | iden matrix.
484+iden :: forall e cols . (Num e, FL cols cols, Countable cols) => Matrix e cols cols
485+iden = matrixBuilder' (bool 0 1 . uncurry (==))
486+{-# NOINLINE iden #-}
489487
490488-- Matrix composition (MMM)
491489
@@ -494,60 +492,90 @@ identity = matrixBuilder (bool 0 1 . uncurry (==))
494492-- This definition takes advantage of divide-and-conquer and fusion laws
495493-- from LAoP.
496494comp :: (Num e) => Matrix e cr rows -> Matrix e cols cr -> Matrix e cols rows
497−comp Empty Empty = Empty
498−comp (One a) (One b) = One (a * b)
499−comp (Junc a b) (Split c d) = comp a c + comp b d -- Divide-and-conquer law
500−comp (Split a b) c = Split (comp a c) (comp b c) -- Split fusion law
501−comp c (Junc a b) = Junc (comp c a) (comp c b) -- Junc fusion law
495+comp (One a) (One b) = One (a * b)
496+comp (Join a b) (Fork c d) = comp a c + comp b d -- Divide-and-conquer law
497+comp (Fork a b) c = Fork (comp a c) (comp b c) -- Fork fusion law
498+comp c (Join a b) = Join (comp c a) (comp c b) -- Join fusion law
499+{-# NOINLINE comp #-}
500+{-# RULES
501+ "comp/iden1" forall m. comp m iden = m ;
502+ "comp/iden2" forall m. comp iden m = m
503+#-}
504+
505+-- Scalar multiplication of matrices
506+
507+infixl 7 .|
508+-- | Scalar multiplication of matrices.
509+(.|) :: Num e => e -> Matrix e cols rows -> Matrix e cols rows
510+(.|) e (One a) = One (e * a)
511+(.|) e (Join a b) = Join (e .| a) (e .| b)
512+(.|) e (Fork a b) = Fork (e .| a) (e .| b)
513+
514+-- Scalar division of matrices
515+
516+infixl 7 ./
517+-- | Scalar multiplication of matrices.
518+(./) :: Fractional e => Matrix e cols rows -> e -> Matrix e cols rows
519+(./) (One a) e = One (a / e)
520+(./) (Join a b) e = Join (a ./ e) (b ./ e)
521+(./) (Fork a b) e = Fork (a ./ e) (b ./ e)
502522
503523-- Projections
504524
505525-- | Biproduct first component projection
506−p1 :: forall e m n. (Num e, KnownNat (Count n), KnownNat (Count m), FromLists e n m, FromLists e m m) => Matrix e (Either m n) m
507−p1 =
508− let iden = identity :: Matrix e m m
509− zero = zeros :: Matrix e n m
510− in junc iden zero
526+p1 :: (Num e, CountableDims n m, FL n m, FL m m) => Matrix e (Either m n) m
527+p1 = join id zeros
511528
512529-- | Biproduct second component projection
513−p2 :: forall e m n. (Num e, KnownNat (Count n), KnownNat (Count m), FromLists e m n, FromLists e n n) => Matrix e (Either m n) n
514−p2 =
515− let iden = identity :: Matrix e n n
516− zero = zeros :: Matrix e m n
517− in junc zero iden
530+p2 :: (Num e, CountableDims n m, FL m n, FL n n) => Matrix e (Either m n) n
531+p2 = join zeros id
518532
519533-- Injections
520534
521535-- | Biproduct first component injection
522−i1 :: (Num e, KnownNat (Count n), KnownNat (Count m), FromLists e n m, FromLists e m m) => Matrix e m (Either m n)
536+i1 :: (Num e, CountableDims n m, FL n m, FL m m) => Matrix e m (Either m n)
523537i1 = tr p1
524538
525539-- | Biproduct second component injection
526−i2 :: (Num e, KnownNat (Count n), KnownNat (Count m), FromLists e m n, FromLists e n n) => Matrix e n (Either m n)
540+i2 :: (Num e, CountableDims n m, FL m n, FL n n) => Matrix e n (Either m n)
527541i2 = tr p2
528542
529543-- Dimensions
530544
531545-- | Obtain the number of rows.
532546--
533−-- NOTE: The 'KnownNat' constaint is needed in order to obtain the
534−-- dimensions in constant time.
535−--
536−-- TODO: A 'rows' function that does not need the 'KnownNat' constraint in
537−-- exchange for performance.
538−rows :: forall e cols rows. (KnownNat (Count rows)) => Matrix e cols rows -> Int
547+-- NOTE: The 'KnownNat' constraint is needed in order to obtain the
548+-- dimensions in constant time. For a version that doesn't require the
549+-- constraint see 'rows''.
550+rows :: forall e cols rows. (Countable rows) => Matrix e cols rows -> Int
539551rows _ = fromInteger $ natVal (Proxy :: Proxy (Count rows))
540552
553+-- | Obtain the number of rows in an inefficient manner, but without any
554+-- constraints.
555+--
556+-- For a more efficient version see 'rows'.
557+rows' :: Matrix e cols rows -> Int
558+rows' (One _) = 1
559+rows' (Join lhs _) = rows' lhs
560+rows' (Fork top bottom) = rows' top + rows' bottom
561+
541562-- | Obtain the number of columns.
542−--
543−-- NOTE: The 'KnownNat' constaint is needed in order to obtain the
544−-- dimensions in constant time.
545563--
546−-- TODO: A 'columns' function that does not need the 'KnownNat' constraint in
547−-- exchange for performance.
548−columns :: forall e cols rows. (KnownNat (Count cols)) => Matrix e cols rows -> Int
564+-- NOTE: The 'KnownNat' constraint is needed in order to obtain the
565+-- dimensions in constant time. For a version that doesn't require the
566+-- constraint see 'columns''.
567+columns :: forall e cols rows. (Countable cols) => Matrix e cols rows -> Int
549568columns _ = fromInteger $ natVal (Proxy :: Proxy (Count cols))
550569
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+
551579-- Coproduct Bifunctor
552580
553581infixl 5 -|-
@@ -556,157 +584,172 @@ infixl 5 -|-
556584(-|-) ::
557585 forall e n k m j.
558586 ( Num e,
559− KnownNat (Count j),
560− KnownNat (Count k),
561− FromLists e k k,
562− FromLists e j k,
563− FromLists e k j,
564− FromLists e j j
587+ CountableDims j k,
588+ FL k k,
589+ FL j k,
590+ FL k j,
591+ FL j j
565592 ) =>
566593 Matrix e n k ->
567594 Matrix e m j ->
568595 Matrix e (Either n m) (Either k j)
569−(-|-) a b = Junc (i1 . a) (i2 . b)
596+(-|-) a b = Join (i1 . a) (i2 . b)
570597
571598-- Khatri Rao Product and projections
572599
573600-- | Khatri Rao product first component projection matrix.
574−kp1 ::
601+fstM ::
575602 forall e m k .
576603 ( Num e,
577− KnownNat (Count k),
578− FromLists e (FromNat (Count m * Count k)) m,
579− KnownNat (Count m),
580− KnownNat (Count (Normalize (m, k)))
604+ CountableDims k m,
605+ FL (Normalize (m, k)) m,
606+ CountableN (m, k)
581607 ) => Matrix e (Normalize (m, k)) m
582−kp1 = matrixBuilder f
608+fstM = matrixBuilder' f
583609 where
584610 offset = fromInteger (natVal (Proxy :: Proxy (Count k)))
585611 f (x, y)
586612 | y >= (x * offset) && y <= (x * offset + offset - 1) = 1
587− | otherwise = 0
613+ | otherwise = 0
588614
589615-- | Khatri Rao product second component projection matrix.
590−kp2 ::
616+sndM ::
591617 forall e m k .
592618 ( Num e,
593− KnownNat (Count k),
594− FromLists e (FromNat (Count m * Count k)) k,
595− KnownNat (Count m),
596− KnownNat (Count (Normalize (m, k)))
619+ CountableDims k m,
620+ FL (Normalize (m, k)) k,
621+ CountableN (m, k)
597622 ) => Matrix e (Normalize (m, k)) k
598−kp2 = matrixBuilder f
623+sndM = matrixBuilder' f
599624 where
600625 offset = fromInteger (natVal (Proxy :: Proxy (Count k)))
601626 f (x, y)
602627 | x == y || mod (y - x) offset == 0 = 1
603− | otherwise = 0
628+ | otherwise = 0
604629
605630-- | Khatri Rao Matrix product also known as matrix pairing.
606631--
607632-- NOTE: That this is not a true categorical product, see for instance:
608−--
633+--
609634-- @
610−-- | kp1 . khatri a b == a
611−-- khatri a b ==> |
612−-- | kp2 . khatri a b == b
635+-- | fstM . kr a b == a
636+-- kr a b ==> |
637+-- | sndM . kr a b == b
613638-- @
614639--
615640-- __Emphasis__ on the implication symbol.
616−khatri ::
617− forall e cols a b.
641+kr ::
642+ forall e cols a b.
618643 ( Num e,
619− KnownNat (Count a),
620− KnownNat (Count b),
621− KnownNat (Count (Normalize (a, b))),
622− FromLists e (Normalize (a, b)) a,
623− FromLists e (Normalize (a, b)) b
644+ CountableDims a b,
645+ CountableN (a, b),
646+ FL (Normalize (a, b)) a,
647+ FL (Normalize (a, b)) b
624648 ) => Matrix e cols a -> Matrix e cols b -> Matrix e cols (Normalize (a, b))
625−khatri a b =
626− let kp1' = kp1 @e @a @b
627− kp2' = kp2 @e @a @b
628− in (tr kp1') . a * (tr kp2') . b
649+kr a b =
650+ let fstM' = fstM @e @a @b
651+ sndM' = sndM @e @a @b
652+ in (tr fstM' . a) * (tr sndM' . b)
629653
630654-- Product Bifunctor (Kronecker)
631655
632656infixl 4 ><
633657
634658-- | Matrix product functor also known as kronecker product
635−(><) ::
636− forall e m p n q.
659+(><) ::
660+ forall e m p n q.
637661 ( Num e,
638− KnownNat (Count m),
639− KnownNat (Count n),
640− KnownNat (Count p),
641− KnownNat (Count q),
642− KnownNat (Count (Normalize (m, n))),
643− FromLists e (Normalize (m, n)) m,
644− FromLists e (Normalize (m, n)) n,
645− KnownNat (Count (Normalize (p, q))),
646− FromLists e (Normalize (p, q)) p,
647− FromLists e (Normalize (p, q)) q
648− )
662+ CountableDims m n,
663+ CountableDims p q,
664+ CountableDimsN (m, n) (p, q),
665+ FL (Normalize (m, n)) m,
666+ FL (Normalize (m, n)) n,
667+ FL (Normalize (p, q)) p,
668+ FL (Normalize (p, q)) q
669+ )
649670 => Matrix e m p -> Matrix e n q -> Matrix e (Normalize (m, n)) (Normalize (p, q))
650671(><) a b =
651− let kp1' = kp1 @e @m @n
652− kp2' = kp2 @e @m @n
653− in khatri (a . kp1') (b . kp2')
672+ let fstM' = fstM @e @m @n
673+ sndM' = sndM @e @m @n
674+ in kr (a . fstM') (b . sndM')
654675
655−-- Matrix abide Junc Split
676+-- Matrix abide Join Fork
656677
657−-- | Matrix "abiding" followin the 'Junc'-'Split' abide law.
658−--
678+-- | Matrix "abiding" following the 'Join'-'Fork' exchange law.
679+--
659680-- Law:
660681--
661682-- @
662−-- 'Junc' ('Split' a c) ('Split' b d) == 'Split' ('Junc' a b) ('Junc' c d)
683+-- 'Join' ('Fork' a c) ('Fork' b d) == 'Fork' ('Join' a b) ('Join' c d)
663684-- @
664−abideJS :: Matrix e cols rows -> Matrix e cols rows
665−abideJS (Junc (Split a c) (Split b d)) = Split (Junc (abideJS a) (abideJS b)) (Junc (abideJS c) (abideJS d)) -- Junc-Split abide law
666−abideJS Empty = Empty
667−abideJS (One e) = One e
668−abideJS (Junc a b) = Junc (abideJS a) (abideJS b)
669−abideJS (Split a b) = Split (abideJS a) (abideJS b)
685+abideJF :: Matrix e cols rows -> Matrix e cols rows
686+abideJF (Join (Fork a c) (Fork b d)) = Fork (Join (abideJF a) (abideJF b)) (Join (abideJF c) (abideJF d)) -- Join-Fork abide law
687+abideJF (One e) = One e
688+abideJF (Join a b) = Join (abideJF a) (abideJF b)
689+abideJF (Fork a b) = Fork (abideJF a) (abideJF b)
670690
671−-- Matrix abide Split Junc
691+-- Matrix abide Fork Join
672692
673−-- | Matrix "abiding" followin the 'Split'-'Junc' abide law.
674−--
693+-- | Matrix "abiding" followin the 'Fork'-'Join' abide law.
694+--
675695-- @
676−-- 'Split' ('Junc' a b) ('Junc' c d) == 'Junc' ('Split' a c) ('Split' b d)
696+-- 'Fork' ('Join' a b) ('Join' c d) == 'Join' ('Fork' a c) ('Fork' b d)
677697-- @
678−abideSJ :: Matrix e cols rows -> Matrix e cols rows
679−abideSJ (Split (Junc a b) (Junc c d)) = Junc (Split (abideSJ a) (abideSJ c)) (Split (abideSJ b) (abideSJ d)) -- Split-Junc abide law
680−abideSJ Empty = Empty
681−abideSJ (One e) = One e
682−abideSJ (Junc a b) = Junc (abideSJ a) (abideSJ b)
683−abideSJ (Split a b) = Split (abideSJ a) (abideSJ b)
698+abideFJ :: Matrix e cols rows -> Matrix e cols rows
699+abideFJ (Fork (Join a b) (Join c d)) = Join (Fork (abideFJ a) (abideFJ c)) (Fork (abideFJ b) (abideFJ d)) -- Fork-Join abide law
700+abideFJ (One e) = One e
701+abideFJ (Join a b) = Join (abideFJ a) (abideFJ b)
702+abideFJ (Fork a b) = Fork (abideFJ a) (abideFJ b)
684703
685704-- Matrix transposition
686705
687706-- | Matrix transposition.
688707tr :: Matrix e cols rows -> Matrix e rows cols
689−tr Empty = Empty
690−tr (One e) = One e
691−tr (Junc a b) = Split (tr a) (tr b)
692−tr (Split a b) = Junc (tr a) (tr b)
708+tr (One e) = One e
709+tr (Join a b) = Fork (tr a) (tr b)
710+tr (Fork a b) = Join (tr a) (tr b)
693711
694712-- Selective 'select' operator
695713
696714-- | Selective functors 'select' operator equivalent inspired by the
697715-- ArrowMonad solution presented in the paper.
698−select :: (Num e, FromLists e b b, KnownNat (Count b)) => Matrix e cols (Either a b) -> Matrix e a b -> Matrix e cols b
699−select m y = junc y identity . m
716+select :: (Num e, FL b b, Countable b) => Matrix e cols (Either a b) -> Matrix e a b -> Matrix e cols b
717+select (Fork a b) y = y . a + b -- Divide-and-conquer law
718+select (Join (Fork a c) (Fork b d)) y = join (y . a + c) (y . b + d) -- Pattern matching + DnC law
719+select m y = join y id . m
720+
721+branch ::
722+ ( Num e,
723+ CountableDims a b,
724+ CountableDims c (Either b c),
725+ FL c b,
726+ FL a b,
727+ FL a a,
728+ FL b b,
729+ FL c c,
730+ FL b a,
731+ FL b c,
732+ FL (Either b c) b,
733+ FL (Either b c) c
734+ )
735+ => Matrix e cols (Either a b) -> Matrix e a c -> Matrix e b c -> Matrix e cols c
736+branch x l r = f x `select` g l `select` r
737+ where
738+ f :: (Num e, Countable a, CountableDims b c, FL a b, FL c b, FL b b, FL b a, FL a a)
739+ => Matrix e cols (Either a b) -> Matrix e cols (Either a (Either b c))
740+ f m = fork (tr i1) (i1 . tr i2) . m
741+ g :: (Num e, CountableDims b c, FL b c, FL c c) => Matrix e a c -> Matrix e a (Either b c)
742+ g m = i2 . m
700743
701744-- McCarthy's Conditional
702745
703746-- | McCarthy's Conditional expresses probabilistic choice.
704747cond ::
705− ( cols ~ FromNat (Count cols),
706− KnownNat (Count cols),
707− FromLists e () cols,
708− FromLists e cols (),
709− FromLists e cols cols,
748+ ( Trivial cols,
749+ Countable cols,
750+ FL () cols,
751+ FL cols (),
752+ FL cols cols,
710753 Bounded a,
711754 Enum a,
712755 Num e,
@@ -714,14 +757,14 @@ cond ::
714757 )
715758 =>
716759 (a -> Bool) -> Matrix e cols rows -> Matrix e cols rows -> Matrix e cols rows
717−cond p f g = junc f g . grd p
718−
719−grd ::
720− ( q ~ FromNat (Count q),
721− KnownNat (Count q),
722− FromLists e () q,
723− FromLists e q (),
724− FromLists e q q,
760+cond p f g = join f g . grd p
761+
762+grd ::
763+ ( Trivial q,
764+ Countable q,
765+ FL () q,
766+ FL q (),
767+ FL q q,
725768 Bounded a,
726769 Enum a,
727770 Num e,
@@ -729,62 +772,88 @@ grd ::
729772 )
730773 =>
731774 (a -> Bool) -> Matrix e q (Either q q)
732−grd f = split (corr f) (corr (not . f))
733−
734−corr ::
735− forall e a q .
736− ( q ~ FromNat (Count q),
737− KnownNat (Count q),
738− FromLists e () q,
739− FromLists e q (),
740− FromLists e q q,
741− Bounded a,
742− Enum a,
743− Num e,
744− Ord e
745− )
775+grd f = fork (corr f) (corr (not . f))
776+
777+corr ::
778+ forall e a q .
779+ ( Trivial q,
780+ Countable q,
781+ FL () q,
782+ FL q (),
783+ FL q q,
784+ Liftable e a Bool
785+ )
746786 => (a -> Bool) -> Matrix e q q
747−corr p = let f = fromF p :: Matrix e q ()
748− in khatri f (identity :: Matrix e q q)
787+corr p = let f = fromF' p :: Matrix e q ()
788+ in kr f (id :: Matrix e q q)
749789
750790-- Pretty print
751791
752792prettyAux :: Show e => [[e]] -> [[e]] -> String
753793prettyAux [] _ = ""
754−prettyAux [[e]] m = "│ " ++ fill (show e) ++ " │\n"
794+prettyAux [[e]] m = "│ " ++ fill (show e) ++ " │\n"
755795 where
756796 v = fmap show m
757797 widest = maximum $ fmap length v
758798 fill str = replicate (widest - length str - 2) ' ' ++ str
759−prettyAux [h] m = "│ " ++ fill (unwords $ map show h) ++ " │\n"
799+prettyAux [h] m = "│ " ++ fill (unwords $ map show h) ++ " │\n"
760800 where
761− v = fmap show m
762− widest = maximum $ fmap length v
801+ v = fmap show m
802+ widest = maximum $ fmap length v
763803 fill str = replicate (widest - length str - 2) ' ' ++ str
764−prettyAux (h : t) l = "│ " ++ fill (unwords $ map show h) ++ " │\n" ++
804+prettyAux (h : t) l = "│ " ++ fill (unwords $ map show h) ++ " │\n" ++
765805 prettyAux t l
766806 where
767− v = fmap show l
768− widest = maximum $ fmap length v
807+ v = fmap show l
808+ widest = maximum $ fmap length v
769809 fill str = replicate (widest - length str - 2) ' ' ++ str
770810
771811-- | Matrix pretty printer
772−pretty :: (KnownNat (Count cols), Show e) => Matrix e cols rows -> String
773−pretty m = "┌ " ++ unwords (replicate (columns m) blank) ++ " ┐\n" ++
774− prettyAux (toLists m) (toLists m) ++
775− "└ " ++ unwords (replicate (columns m) blank) ++ " ┘"
776− where
777− v = fmap show (toList m)
778− widest = maximum $ fmap length v
812+pretty :: (CountableDims cols rows, Show e) => Matrix e cols rows -> String
813+pretty m = concat
814+ [ "┌ ", unwords (replicate (columns m) blank), " ┐\n"
815+ , unlines
816+ [ "│ " ++ unwords (fmap (\j -> fill $ show $ getElem i j m) [1..columns m]) ++ " │" | i <- [1..rows m] ]
817+ , "└ ", unwords (replicate (columns m) blank), " ┘"
818+ ]
819+ where
820+ strings = map show (toList m)
821+ widest = maximum $ map length strings
779822 fill str = replicate (widest - length str) ' ' ++ str
780− blank = fill ""
823+ blank = fill ""
824+ safeGet i j m
825+ | i > rows m || j > columns m || i < 1 || j < 1 = Nothing
826+ | otherwise = Just $ unsafeGet i j m (toList m)
827+ unsafeGet i j m l = l !! encode (columns m) (i,j)
828+ encode m (i,j) = (i-1)*m + j - 1
829+ getElem i j m =
830+ fromMaybe
831+ (error $
832+ "getElem: Trying to get the "
833+ ++ show (i, j)
834+ ++ " element from a "
835+ ++ show (rows m) ++ "x" ++ show (columns m)
836+ ++ " matrix."
837+ )
838+ (safeGet i j m)
781839
782840-- | Matrix pretty printer
783−prettyPrint :: (KnownNat (Count cols), Show e) => Matrix e cols rows -> IO ()
841+prettyPrint :: (CountableDims cols rows, Show e) => Matrix e cols rows -> IO ()
784842prettyPrint = putStrLn . pretty
785843
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+
786852-- Relational operators functions
787853
854+type Boolean = Natural 0 1
855+type Relation a b = Matrix Boolean a b
856+
788857-- | Helper conversion function
789858toBool :: (Num e, Eq e) => e -> Bool
790859toBool n
@@ -796,104 +865,110 @@ fromBool :: Bool -> Natural 0 1
796865fromBool True = nat 1
797866fromBool False = nat 0
798867
868+-- | Relational negation
869+negateM :: Relation cols rows -> Relation cols rows
870+negateM (One (Nat p)) = One (Nat (negate p))
871+negateM (Join a b) = Join (negateM a) (negateM b)
872+negateM (Fork a b) = Fork (negateM a) (negateM b)
873+
799874-- | Relational addition
800−orM :: Matrix (Natural 0 1) cols rows -> Matrix (Natural 0 1) cols rows -> Matrix (Natural 0 1) cols rows
801−orM Empty Empty = Empty
802−orM (One a) (One b) = One (fromBool (toBool a || toBool b))
803−orM (Junc a b) (Junc c d) = Junc (orM a c) (orM b d)
804−orM (Split a b) (Split c d) = Split (orM a c) (orM b d)
805−orM x@(Split _ _) y@(Junc _ _) = orM x (abideJS y)
806−orM x@(Junc _ _) y@(Split _ _) = orM (abideJS x) y
875+orM :: Relation cols rows -> Relation cols rows -> Relation cols rows
876+orM (One a) (One b) = One (fromBool (toBool a || toBool b))
877+orM (Join a b) (Join c d) = Join (orM a c) (orM b d)
878+orM (Fork a b) (Fork c d) = Fork (orM a c) (orM b d)
879+orM x@(Fork _ _) y@(Join _ _) = orM x (abideJF y)
880+orM x@(Join _ _) y@(Fork _ _) = orM (abideJF x) y
807881
808882-- | Relational multiplication
809−andM :: Matrix (Natural 0 1) cols rows -> Matrix (Natural 0 1) cols rows -> Matrix (Natural 0 1) cols rows
810−andM Empty Empty = Empty
811−andM (One a) (One b) = One (fromBool (toBool a && toBool b))
812−andM (Junc a b) (Junc c d) = Junc (andM a c) (andM b d)
813−andM (Split a b) (Split c d) = Split (andM a c) (andM b d)
814−andM x@(Split _ _) y@(Junc _ _) = andM x (abideJS y)
815−andM x@(Junc _ _) y@(Split _ _) = andM (abideJS x) y
883+andM :: Relation cols rows -> Relation cols rows -> Relation cols rows
884+andM (One a) (One b) = One (fromBool (toBool a && toBool b))
885+andM (Join a b) (Join c d) = Join (andM a c) (andM b d)
886+andM (Fork a b) (Fork c d) = Fork (andM a c) (andM b d)
887+andM x@(Fork _ _) y@(Join _ _) = andM x (abideJF y)
888+andM x@(Join _ _) y@(Fork _ _) = andM (abideJF x) y
816889
817890-- | Relational subtraction
818−subM :: Matrix (Natural 0 1) cols rows -> Matrix (Natural 0 1) cols rows -> Matrix (Natural 0 1) cols rows
819−subM Empty Empty = Empty
820−subM (One a) (One b) = if a - b < nat 0 then One (nat 0) else One (a - b)
821−subM (Junc a b) (Junc c d) = Junc (subM a c) (subM b d)
822−subM (Split a b) (Split c d) = Split (subM a c) (subM b d)
823−subM x@(Split _ _) y@(Junc _ _) = subM x (abideJS y)
824−subM x@(Junc _ _) y@(Split _ _) = subM (abideJS x) y
891+subM :: Relation cols rows -> Relation cols rows -> Relation cols rows
892+subM (One a) (One b) = if a - b < nat 0 then One (nat 0) else One (a - b)
893+subM (Join a b) (Join c d) = Join (subM a c) (subM b d)
894+subM (Fork a b) (Fork c d) = Fork (subM a c) (subM b d)
895+subM x@(Fork _ _) y@(Join _ _) = subM x (abideJF y)
896+subM x@(Join _ _) y@(Fork _ _) = subM (abideJF x) y
825897
826898-- | Matrix relational composition.
827−compRel :: Matrix (Natural 0 1) cr rows -> Matrix (Natural 0 1) cols cr -> Matrix (Natural 0 1) cols rows
828−compRel Empty Empty = Empty
829−compRel (One a) (One b) = One (fromBool (toBool a && toBool b))
830−compRel (Junc a b) (Split c d) = orM (compRel a c) (compRel b d) -- Divide-and-conquer law
831−compRel (Split a b) c = Split (compRel a c) (compRel b c) -- Split fusion law
832−compRel c (Junc a b) = Junc (compRel c a) (compRel c b) -- Junc fusion law
899+compRel :: Relation cr rows -> Relation cols cr -> Relation cols rows
900+compRel (One a) (One b) = One (fromBool (toBool a && toBool b))
901+compRel (Join a b) (Fork c d) = orM (compRel a c) (compRel b d) -- Divide-and-conquer law
902+compRel (Fork a b) c = Fork (compRel a c) (compRel b c) -- Fork fusion law
903+compRel c (Join a b) = Join (compRel c a) (compRel c b) -- Join fusion law
904+
905+-- | Matrix relational right division
906+divR :: Relation b c -> Relation b a -> Relation a c
907+divR (One a) (One b) = One (fromBool (not (toBool b) || toBool a)) -- b implies a
908+divR (Join a b) (Join c d) = andM (divR a c) (divR b d)
909+divR (Fork a b) c = Fork (divR a c) (divR b c)
910+divR c (Fork a b) = Join (divR c a) (divR c b)
911+
912+-- | Matrix relational left division
913+divL :: Relation c b -> Relation a b -> Relation a c
914+divL x y = tr (divR (tr y) (tr x))
915+
916+-- | Matrix relational symmetric division
917+divS :: Relation c a -> Relation b a -> Relation c b
918+divS s r = divL r s `intersection` divR (tr r) (tr s)
919+ where
920+ intersection = andM
833921
834922-- | Lifts functions to relations with arbitrary dimensions.
835923--
836924-- NOTE: Be careful to not ask for a relation bigger than the cardinality of
837925-- types @a@ or @b@ allows.
838−fromFRel ::
926+fromFRel' ::
839927 forall a b cols rows.
840− ( Bounded a,
841− Bounded b,
842− Enum a,
843− Enum b,
844− Eq b,
845− KnownNat (Count cols),
846− KnownNat (Count rows),
847− FromLists (Natural 0 1) rows cols
928+ ( Liftable Boolean a b,
929+ CountableDims cols rows,
930+ FL rows cols
848931 ) =>
849932 (a -> b) ->
850− Matrix (Natural 0 1) cols rows
851−fromFRel f =
852− let minA = minBound @a
853− maxA = maxBound @a
854− minB = minBound @b
855− maxB = maxBound @b
856− ccols = fromInteger $ natVal (Proxy :: Proxy (Count cols))
857− rrows = fromInteger $ natVal (Proxy :: Proxy (Count rows))
858− elementsA = take ccols [minA .. maxA]
859− elementsB = take rrows [minB .. maxB]
860− combinations = (,) <$> elementsA <*> elementsB
861− combAp = map snd . sort . map (\(a, b) -> if f a == b
862− then ((fromEnum a, fromEnum b), nat 1)
863− else ((fromEnum a, fromEnum b), nat 0)) $ combinations
864− mList = buildList combAp rrows
865− in tr $ fromLists mList
866− where
867− buildList [] _ = []
868− buildList l r = take r l : buildList (drop r l) r
933+ Relation cols rows
934+fromFRel' = fromF'
869935
870936-- | Lifts functions to relations with dimensions matching @a@ and @b@
871937-- cardinality's.
872−fromFRel' ::
938+fromFRel ::
873939 forall a b.
874− ( Bounded a,
875− Bounded b,
876− Enum a,
877− Enum b,
878− Eq b,
879− KnownNat (Count (Normalize a)),
880− KnownNat (Count (Normalize b)),
881− FromLists (Natural 0 1) (Normalize b) (Normalize a)
940+ ( Liftable Boolean a b,
941+ CountableDimsN a b,
942+ FLN b a
882943 ) =>
883944 (a -> b) ->
884− Matrix (Natural 0 1) (Normalize a) (Normalize b)
885−fromFRel' f =
945+ Relation (Normalize a) (Normalize b)
946+fromFRel = fromFRel'
947+
948+-- | Lifts a relation function to a Boolean Matrix
949+toRel ::
950+ forall a b.
951+ ( Bounded a,
952+ Bounded b,
953+ Enum a,
954+ Enum b,
955+ Eq b,
956+ CountableDims a b,
957+ FLN b a
958+ )
959+ => (a -> b -> Bool) -> Relation (Normalize a) (Normalize b)
960+toRel f =
886961 let minA = minBound @a
887962 maxA = maxBound @a
888963 minB = minBound @b
889964 maxB = maxBound @b
890− ccols = fromInteger $ natVal (Proxy :: Proxy (Count (Normalize a)))
891− rrows = fromInteger $ natVal (Proxy :: Proxy (Count (Normalize b)))
965+ ccols = fromInteger $ natVal (Proxy :: Proxy (Count a))
966+ rrows = fromInteger $ natVal (Proxy :: Proxy (Count b))
892967 elementsA = take ccols [minA .. maxA]
893968 elementsB = take rrows [minB .. maxB]
894969 combinations = (,) <$> elementsA <*> elementsB
895− combAp = map snd . sort . map (\(a, b) -> if f a == b
896− then ((fromEnum a, fromEnum b), nat 1)
970+ combAp = map snd . sort . map (\(a, b) -> if uncurry f (a, b)
971+ then ((fromEnum a, fromEnum b), nat 1)
897972 else ((fromEnum a, fromEnum b), nat 0)) $ combinations
898973 mList = buildList combAp rrows
899974 in tr $ fromLists mList
src/LAoP/Matrix/Nat.hs+194−187
@@ -1,3 +1,4 @@
1+{-# LANGUAGE ConstraintKinds #-}
12{-# LANGUAGE AllowAmbiguousTypes #-}
23{-# LANGUAGE DataKinds #-}
34{-# LANGUAGE DerivingVia #-}
@@ -53,11 +54,22 @@ module LAoP.Matrix.Nat
5354 -- * Type safe matrix representation
5455 Matrix (..),
5556
57+ -- * Constraint type synonyms
58+ Countable,
59+ CountableDims,
60+ CountableN,
61+ CountableNz,
62+ CountableDimsN,
63+ FLN,
64+ FLNz,
65+ Liftable,
66+ TrivialE,
67+ TrivialP,
68+
5669 -- * Primitives
57− empty,
5870 one,
59− junc,
60− split,
71+ join,
72+ fork,
6173
6274 -- * Auxiliary type families
6375 I.FromNat,
@@ -65,11 +77,11 @@ module LAoP.Matrix.Nat
6577 I.Normalize,
6678
6779 -- * Matrix construction and conversion
68− I.FromLists,
80+ I.FL,
6981 fromLists,
7082 toLists,
7183 toList,
72− matrixBuilder,
84+ matrixBuilder',
7385 row,
7486 col,
7587 zeros,
@@ -85,6 +97,10 @@ module LAoP.Matrix.Nat
8597 -- ** Matrix Transposition
8698 tr,
8799
100+ -- ** Scalar multiplication/division of matrices
101+ (.|),
102+ (./),
103+
88104 -- ** Selective operator
89105 select,
90106
@@ -92,16 +108,19 @@ module LAoP.Matrix.Nat
92108 cond,
93109
94110 -- ** Matrix "abiding"
95− abideJS,
96− abideSJ,
111+ abideJF,
112+ abideFJ,
113+
114+ -- ** Zip Matrices
115+ zipWithM,
97116
98117 -- * Biproduct approach
99− -- ** Split
118+ -- ** Fork
100119 (===),
101120 -- *** Projections
102121 p1,
103122 p2,
104− -- ** Junc
123+ -- ** Join
105124 (|||),
106125 -- *** Injections
107126 i1,
@@ -115,11 +134,11 @@ module LAoP.Matrix.Nat
115134 -- | Note that given the restrictions imposed it is not possible to
116135 -- implement the standard type classes present in standard Haskell.
117136 -- *** Matrix pairing projections
118− kp1,
119− kp2,
137+ fstM,
138+ sndM,
120139
121140 -- *** Matrix pairing
122− khatri,
141+ kr,
123142
124143 -- * Matrix composition and lifting
125144
@@ -127,10 +146,10 @@ module LAoP.Matrix.Nat
127146
128147 -- | Note that given the restrictions imposed it is not possible to
129148 -- implement the standard type classes present in standard Haskell.
130− identity,
149+ iden,
131150 comp,
132− fromF,
133151 fromF',
152+ fromF,
134153
135154 -- * Matrix printing
136155 pretty,
@@ -141,107 +160,95 @@ where
141160import Data.Proxy
142161import GHC.TypeLits
143162import Control.DeepSeq
144−import qualified Control.Category as C
145163import qualified LAoP.Matrix.Internal as I
146164
147165newtype Matrix e (cols :: Nat) (rows :: Nat) = M (I.Matrix e (I.FromNat cols) (I.FromNat rows))
148166 deriving (Show, Num, Eq, Ord, NFData) via (I.Matrix e (I.FromNat cols) (I.FromNat rows))
149167
150−-- | It isn't possible to implement the 'id' function so it's
151−-- implementation is 'undefined'. However 'comp' can be and this partial
152−-- class implementation exists just to make the code more readable.
153−--
154−-- Please use 'identity' instead.
155−instance (Num e) => C.Category (Matrix e) where
156− id = undefined
157− (.) = comp
168+-- | Constraint type synonyms to keep the type signatures less convoluted
169+type Countable a = KnownNat (I.Count a)
170+type CountableDims a b = (Countable a, Countable b)
171+type CountableN a = KnownNat (I.Count (I.FromNat a))
172+type CountableNz a = KnownNat (I.Count (I.Normalize a))
173+type CountableDimsN a b = (CountableN a, CountableN b)
174+type FLN e a b = I.FL (I.FromNat a) (I.FromNat b)
175+type FLNz e a b = I.FL (I.Normalize a) (I.Normalize b)
176+type Liftable e a b = (Bounded a, Bounded b, Enum a, Enum b, Eq b, Num e, Ord e)
177+type TrivialE a b = I.FromNat (a + b) ~ Either (I.FromNat a) (I.FromNat b)
178+type TrivialP a b = I.FromNat (a * b) ~ I.FromNat (I.Count (I.FromNat a) * I.Count (I.FromNat b))
158179
159180-- Primitives
160181
161−empty :: Matrix e 0 0
162−empty = M I.Empty
163−
164182one :: e -> Matrix e 1 1
165183one = M . I.One
166184
167−junc ::
168− (I.FromNat cols3 ~ Either (I.FromNat cols1) (I.FromNat cols2)) =>
169− Matrix e cols1 rows ->
170− Matrix e cols2 rows ->
171− Matrix e cols3 rows
172−junc (M a) (M b) = M (I.Junc a b)
185+join ::
186+ (TrivialE a b) =>
187+ Matrix e a rows ->
188+ Matrix e b rows ->
189+ Matrix e (a + b) rows
190+join (M a) (M b) = M (I.Join a b)
173191
174192infixl 3 |||
175193(|||) ::
176− (I.FromNat cols3 ~ Either (I.FromNat cols1) (I.FromNat cols2)) =>
177− Matrix e cols1 rows ->
178− Matrix e cols2 rows ->
179− Matrix e cols3 rows
180−(|||) = junc
181−
182−split ::
183− (I.FromNat rows3 ~ Either (I.FromNat rows1) (I.FromNat rows2)) =>
184− Matrix e cols rows1 ->
185− Matrix e cols rows2 ->
186− Matrix e cols rows3
187−split (M a) (M b) = M (I.Split a b)
194+ (TrivialE a b) =>
195+ Matrix e a rows ->
196+ Matrix e b rows ->
197+ Matrix e (a + b) rows
198+(|||) = join
199+
200+fork ::
201+ (TrivialE a b) =>
202+ Matrix e cols a ->
203+ Matrix e cols b ->
204+ Matrix e cols (a + b)
205+fork (M a) (M b) = M (I.Fork a b)
188206
189207infixl 2 ===
190208(===) ::
191− (I.FromNat rows3 ~ Either (I.FromNat rows1) (I.FromNat rows2)) =>
192− Matrix e cols rows1 ->
193− Matrix e cols rows2 ->
194− Matrix e cols rows3
195−(===) = split
209+ (TrivialE a b) =>
210+ Matrix e cols a ->
211+ Matrix e cols b ->
212+ Matrix e cols (a + b)
213+(===) = fork
196214
197215-- Construction
198216
199−fromLists :: (I.FromLists e (I.FromNat cols) (I.FromNat rows)) => [[e]] -> Matrix e cols rows
217+fromLists :: (FLN e cols rows) => [[e]] -> Matrix e cols rows
200218fromLists = M . I.fromLists
201219
202−matrixBuilder ::
203− (I.FromLists e (I.FromNat cols) (I.FromNat rows), KnownNat (I.Count (I.FromNat cols)), KnownNat (I.Count (I.FromNat rows))) =>
204− ((Int, Int) -> e) ->
205− Matrix e cols rows
206−matrixBuilder = M . I.matrixBuilder
220+-- | Matrix builder function. Constructs a matrix provided with
221+-- a construction function that operates with indices.
222+matrixBuilder' ::
223+ (FLN e cols rows, CountableN cols, CountableN rows)
224+ => ((Int, Int) -> e) -> Matrix e cols rows
225+matrixBuilder' = M . I.matrixBuilder'
207226
208−col :: (I.FromLists e () (I.FromNat rows)) => [e] -> Matrix e 1 rows
227+col :: (I.FL () (I.FromNat rows)) => [e] -> Matrix e 1 rows
209228col = M . I.col
210229
211−row :: (I.FromLists e (I.FromNat cols) ()) => [e] -> Matrix e cols 1
230+row :: (I.FL (I.FromNat cols) ()) => [e] -> Matrix e cols 1
212231row = M . I.row
213232
214−fromF ::
215− ( Bounded a,
216− Bounded b,
217− Enum a,
218− Enum b,
219− Eq b,
220− Num e,
221− Ord e,
222− KnownNat (I.Count (I.FromNat cols)),
223− KnownNat (I.Count (I.FromNat rows)),
224− I.FromLists e (I.FromNat rows) (I.FromNat cols)
233+fromF' ::
234+ ( Liftable e a b,
235+ CountableN cols,
236+ CountableN rows,
237+ FLN e rows cols
225238 ) =>
226239 (a -> b) ->
227240 Matrix e cols rows
228−fromF = M . I.fromF
241+fromF' = M . I.fromF'
229242
230−fromF' ::
231− ( Bounded a,
232− Bounded b,
233− Enum a,
234− Enum b,
235− Eq b,
236− Num e,
237− Ord e,
238− KnownNat (I.Count (I.Normalize a)),
239− KnownNat (I.Count (I.Normalize b)),
240− I.FromLists e (I.Normalize b) (I.Normalize a)
243+fromF ::
244+ ( Liftable e a b,
245+ CountableNz a,
246+ CountableNz b,
247+ FLNz e b a
241248 ) =>
242249 (a -> b) ->
243250 Matrix e (I.Count a) (I.Count b)
244−fromF' = M . I.fromF'
251+fromF = undefined -- M . I.fromF
245252
246253-- Conversion
247254
@@ -254,21 +261,21 @@ toList (M m) = I.toList m
254261-- Zeros Matrix
255262
256263zeros ::
257− (Num e, I.FromLists e (I.FromNat cols) (I.FromNat rows), KnownNat (I.Count (I.FromNat cols)), KnownNat (I.Count (I.FromNat rows))) =>
264+ (Num e, FLN e cols rows, CountableN cols, CountableN rows) =>
258265 Matrix e cols rows
259266zeros = M I.zeros
260267
261268-- Ones Matrix
262269
263270ones ::
264− (Num e, I.FromLists e (I.FromNat cols) (I.FromNat rows), KnownNat (I.Count (I.FromNat cols)), KnownNat (I.Count (I.FromNat rows))) =>
271+ (Num e, FLN e cols rows, CountableN cols, CountableN rows) =>
265272 Matrix e cols rows
266273ones = M I.ones
267274
268275-- Const Matrix
269276
270277constant ::
271− (Num e, I.FromLists e (I.FromNat cols) (I.FromNat rows), KnownNat (I.Count (I.FromNat cols)), KnownNat (I.Count (I.FromNat rows))) =>
278+ (Num e, FLN e cols rows, CountableN cols, CountableN rows) =>
272279 e ->
273280 Matrix e cols rows
274281constant = M . I.constant
@@ -277,40 +284,52 @@ constant = M . I.constant
277284
278285bang ::
279286 forall e cols.
280− (Num e, Enum e, I.FromLists e (I.FromNat cols) (), KnownNat (I.Count (I.FromNat cols))) =>
287+ (Num e, Enum e, I.FL (I.FromNat cols) (), CountableN cols) =>
281288 Matrix e cols 1
282289bang = M I.bang
283290
284−-- Identity Matrix
291+-- iden Matrix
285292
286−identity ::
287− (Num e, I.FromLists e (I.FromNat cols) (I.FromNat cols), KnownNat (I.Count (I.FromNat cols))) =>
293+iden ::
294+ (Num e, FLN e cols cols, CountableN cols) =>
288295 Matrix e cols cols
289−identity = M I.identity
296+iden = M I.iden
290297
291298-- Matrix composition (MMM)
292299
293300comp :: (Num e) => Matrix e cr rows -> Matrix e cols cr -> Matrix e cols rows
294301comp (M a) (M b) = M (I.comp a b)
295302
303+-- Scalar multiplication of matrices
304+
305+infixl 7 .|
306+-- | Scalar multiplication of matrices.
307+(.|) :: Num e => e -> Matrix e cols rows -> Matrix e cols rows
308+(.|) e (M m) = M (e I..| m)
309+
310+-- Scalar division of matrices
311+
312+infixl 7 ./
313+-- | Scalar multiplication of matrices.
314+(./) :: Fractional e => Matrix e cols rows -> e -> Matrix e cols rows
315+(./) (M m) e = M (m I../ e)
316+
296317p1 ::
297318 ( Num e,
298− KnownNat (I.Count (I.FromNat n)),
299− KnownNat (I.Count (I.FromNat m)),
300− I.FromLists e (I.FromNat n) (I.FromNat m),
301− I.FromLists e (I.FromNat m) (I.FromNat m),
302− I.FromNat (m + n) ~ Either (I.FromNat m) (I.FromNat n)
319+ CountableDimsN n m,
320+ FLN e n m,
321+ FLN e m m,
322+ TrivialE m n
303323 ) =>
304324 Matrix e (m + n) m
305325p1 = M I.p1
306326
307327p2 ::
308328 ( Num e,
309− KnownNat (I.Count (I.FromNat n)),
310− KnownNat (I.Count (I.FromNat m)),
311− I.FromLists e (I.FromNat m) (I.FromNat n),
312− I.FromLists e (I.FromNat n) (I.FromNat n),
313− I.FromNat (m + n) ~ Either (I.FromNat m) (I.FromNat n)
329+ CountableDimsN n m,
330+ FLN e m n,
331+ FLN e n n,
332+ TrivialE m n
314333 ) =>
315334 Matrix e (m + n) n
316335p2 = M I.p2
@@ -319,138 +338,125 @@ p2 = M I.p2
319338
320339i1 ::
321340 ( Num e,
322− KnownNat (I.Count (I.FromNat n)),
323− KnownNat (I.Count (I.FromNat rows)),
324− I.FromLists e (I.FromNat n) (I.FromNat rows),
325− I.FromLists e (I.FromNat rows) (I.FromNat rows),
326− I.FromNat (rows + n) ~ Either (I.FromNat rows) (I.FromNat n)
341+ CountableDimsN n rows,
342+ FLN e n rows,
343+ FLN e rows rows,
344+ TrivialE rows n
327345 ) =>
328346 Matrix e rows (rows + n)
329347i1 = tr p1
330348
331349i2 ::
332350 ( Num e,
333− KnownNat (I.Count (I.FromNat rows)),
334− KnownNat (I.Count (I.FromNat m)),
335− I.FromLists e (I.FromNat m) (I.FromNat rows),
336− I.FromLists e (I.FromNat rows) (I.FromNat rows),
337− I.FromNat (m + rows) ~ Either (I.FromNat m) (I.FromNat rows)
351+ CountableDimsN rows m,
352+ FLN e m rows,
353+ FLN e rows rows,
354+ TrivialE m rows
338355 ) =>
339356 Matrix e rows (m + rows)
340357i2 = tr p2
341358
342359-- Dimensions
343360
344−rows :: (KnownNat (I.Count (I.FromNat rows))) => Matrix e cols rows -> Int
361+rows :: (CountableN rows) => Matrix e cols rows -> Int
345362rows (M m) = I.rows m
346363
347−columns :: (KnownNat (I.Count (I.FromNat cols))) => Matrix e cols rows -> Int
364+columns :: (CountableN cols) => Matrix e cols rows -> Int
348365columns (M m) = I.columns m
349366
350−-- Coproduct Bifunctor
351−
352367infixl 5 -|-
353368
369+-- | Coproduct Bifunctor (Direct sum)
354370(-|-) ::
355371 ( Num e,
356− KnownNat (I.Count (I.FromNat j)),
357− KnownNat (I.Count (I.FromNat k)),
358− I.FromLists e (I.FromNat k) (I.FromNat k),
359− I.FromLists e (I.FromNat j) (I.FromNat k),
360− I.FromLists e (I.FromNat k) (I.FromNat j),
361− I.FromLists e (I.FromNat j) (I.FromNat j),
362− I.FromNat (n + m) ~ Either (I.FromNat n) (I.FromNat m),
363− I.FromNat (k + j) ~ Either (I.FromNat k) (I.FromNat j)
372+ CountableDimsN j k,
373+ FLN e k k,
374+ FLN e j k,
375+ FLN e k j,
376+ FLN e j j,
377+ TrivialE n m,
378+ TrivialE k j
364379 ) =>
365380 Matrix e n k ->
366381 Matrix e m j ->
367382 Matrix e (n + m) (k + j)
368383(-|-) (M a) (M b) = M ((I.-|-) a b)
369384
370−-- Khatri Rao Product and projections
371−
372−kp1 ::
385+-- | Khatri Rao Product first projection
386+fstM ::
373387 forall e m k .
374388 ( Num e,
375− KnownNat (I.Count (I.FromNat m)),
376− KnownNat (I.Count (I.FromNat k)),
377− KnownNat (I.Count (I.FromNat (m * k))),
378− I.FromLists e (I.FromNat (m * k)) (I.FromNat m),
379− I.FromNat (m * k) ~ I.FromNat (I.Count (I.FromNat m) * I.Count (I.FromNat k))
389+ CountableDimsN m k,
390+ CountableN (m * k),
391+ FLN e (m * k) m,
392+ TrivialP m k
380393 ) => Matrix e (m * k) m
381−kp1 = M (I.kp1 @e @(I.FromNat m) @(I.FromNat k))
394+fstM = M (I.fstM @e @(I.FromNat m) @(I.FromNat k))
382395
383−kp2 ::
396+-- | Khatri Rao Product second projection
397+sndM ::
384398 forall e m k.
385399 ( Num e,
386− KnownNat (I.Count (I.FromNat k)),
387− I.FromLists e (I.FromNat (m * k)) (I.FromNat k),
388− KnownNat (I.Count (I.FromNat m)),
389− KnownNat (I.Count (I.FromNat (m * k))),
390− I.FromNat (m * k) ~ I.FromNat (I.Count (I.FromNat m) * I.Count (I.FromNat k))
400+ CountableDimsN k m,
401+ FLN e (m * k) k,
402+ CountableN (m * k),
403+ TrivialP m k
391404 ) => Matrix e (m * k) k
392−kp2 = M (I.kp2 @e @(I.FromNat m) @(I.FromNat k))
405+sndM = M (I.sndM @e @(I.FromNat m) @(I.FromNat k))
393406
394−khatri ::
407+-- | Khatri Rao Product
408+kr ::
395409 forall e cols a b.
396410 ( Num e,
397− KnownNat (I.Count (I.FromNat a)),
398− KnownNat (I.Count (I.FromNat b)),
399− KnownNat (I.Count (I.FromNat (a * b))),
400− I.FromLists e (I.FromNat (a * b)) (I.FromNat a),
401− I.FromLists e (I.FromNat (a * b)) (I.FromNat b),
402− I.FromNat (a * b) ~ I.FromNat (I.Count (I.FromNat a) * I.Count (I.FromNat b))
411+ CountableDimsN a b,
412+ CountableN (a * b),
413+ FLN e (a * b) a,
414+ FLN e (a * b) b,
415+ TrivialP a b
403416 ) => Matrix e cols a -> Matrix e cols b -> Matrix e cols (a * b)
404−khatri a b =
405− let kp1' = kp1 @e @a @b
406− kp2' = kp2 @e @a @b
407− in comp (tr kp1') a * comp (tr kp2') b
408−
409−-- Product Bifunctor (Kronecker)
417+kr a b =
418+ let fstM' = fstM @e @a @b
419+ sndM' = sndM @e @a @b
420+ in comp (tr fstM') a * comp (tr sndM') b
410421
422+-- | Product Bifunctor (Kronecker)
411423infixl 4 ><
412424
413425(><) ::
414426 forall e m p n q.
415427 ( Num e,
416− KnownNat (I.Count (I.FromNat m)),
417− KnownNat (I.Count (I.FromNat n)),
418− KnownNat (I.Count (I.FromNat p)),
419− KnownNat (I.Count (I.FromNat q)),
420− KnownNat (I.Count (I.FromNat (m * n))),
421− KnownNat (I.Count (I.FromNat (p * q))),
422− I.FromLists e (I.FromNat (m * n)) (I.FromNat m),
423− I.FromLists e (I.FromNat (m * n)) (I.FromNat n),
424− I.FromLists e (I.FromNat (p * q)) (I.FromNat p),
425− I.FromLists e (I.FromNat (p * q)) (I.FromNat q),
426− I.FromNat (m * n) ~ I.FromNat (I.Count (I.FromNat m) * I.Count (I.FromNat n)),
427− I.FromNat (p * q) ~ I.FromNat (I.Count (I.FromNat p) * I.Count (I.FromNat q))
428+ CountableDimsN m n,
429+ CountableDimsN p q,
430+ CountableDimsN (m * n) (p * q),
431+ FLN e (m * n) m,
432+ FLN e (m * n) n,
433+ FLN e (p * q) p,
434+ FLN e (p * q) q,
435+ TrivialP m n,
436+ TrivialP p q
428437 ) => Matrix e m p -> Matrix e n q -> Matrix e (m * n) (p * q)
429438(><) a b =
430− let kp1' = kp1 @e @m @n
431− kp2' = kp2 @e @m @n
432− in khatri (comp a kp1') (comp b kp2')
433−
434−-- Matrix abide Junc Split
439+ let fstM' = fstM @e @m @n
440+ sndM' = sndM @e @m @n
441+ in kr (comp a fstM') (comp b sndM')
435442
436−abideJS :: Matrix e cols rows -> Matrix e cols rows
437−abideJS (M m) = M (I.abideJS m)
443+-- | Matrix abide Join Fork
444+abideJF :: Matrix e cols rows -> Matrix e cols rows
445+abideJF (M m) = M (I.abideJF m)
438446
439−-- Matrix abide Split Junc
440−
441−abideSJ :: Matrix e cols rows -> Matrix e cols rows
442−abideSJ (M m) = M (I.abideSJ m)
443−
444−-- Matrix transposition
447+-- | Matrix abide Fork Join
448+abideFJ :: Matrix e cols rows -> Matrix e cols rows
449+abideFJ (M m) = M (I.abideFJ m)
445450
451+-- | Matrix transposition
446452tr :: Matrix e cols rows -> Matrix e rows cols
447453tr (M m) = M (I.tr m)
448454
449455-- Selective 'select' operator
450456select ::
451457 ( Num e,
452− I.FromLists e (I.FromNat rows1) (I.FromNat rows1),
453− KnownNat (I.Count (I.FromNat rows1)),
458+ FLN e rows1 rows1,
459+ CountableN rows1,
454460 I.FromNat rows2 ~ I.FromNat rows1,
455461 I.FromNat cols1 ~ I.FromNat cols2,
456462 I.FromNat rows3 ~ Either (I.FromNat cols3) (I.FromNat rows1)
@@ -461,14 +467,11 @@ select (M m) (M y) = M (I.select m y)
461467
462468cond ::
463469 ( I.FromNat (I.Count (I.FromNat cols)) ~ I.FromNat cols,
464− KnownNat (I.Count (I.FromNat cols)),
465− I.FromLists e () (I.FromNat cols),
466− I.FromLists e (I.FromNat cols) (),
467− I.FromLists e (I.FromNat cols) (I.FromNat cols),
468− Bounded a,
469− Enum a,
470− Num e,
471− Ord e
470+ CountableN cols,
471+ I.FL () (I.FromNat cols),
472+ I.FL (I.FromNat cols) (),
473+ FLN e cols cols,
474+ Liftable e a Bool
472475 )
473476 =>
474477 (a -> Bool) -> Matrix e cols rows -> Matrix e cols rows -> Matrix e cols rows
@@ -476,8 +479,12 @@ cond p (M a) (M b) = M (I.cond p a b)
476479
477480-- Pretty print
478481
479−pretty :: (KnownNat (I.Count (I.FromNat cols)), Show e) => Matrix e cols rows -> String
482+pretty :: (CountableDimsN cols rows, Show e) => Matrix e cols rows -> String
480483pretty (M m) = I.pretty m
481484
482−prettyPrint :: (KnownNat (I.Count (I.FromNat cols)), Show e) => Matrix e cols rows -> IO ()
485+prettyPrint :: (CountableDimsN cols rows, Show e) => Matrix e cols rows -> IO ()
483486prettyPrint (M m) = I.prettyPrint m
487+
488+-- | Zip two matrices with a given binary function
489+zipWithM :: (e -> f -> g) -> Matrix e cols rows -> Matrix f cols rows -> Matrix g cols rows
490+zipWithM f (M a) (M b) = M (I.zipWithM f a b)
src/LAoP/Matrix/Type.hs+292−232
@@ -1,10 +1,11 @@
1+{-# LANGUAGE ConstraintKinds #-}
2+{-# LANGUAGE TypeFamilies #-}
13{-# LANGUAGE AllowAmbiguousTypes #-}
24{-# LANGUAGE DataKinds #-}
35{-# LANGUAGE DerivingVia #-}
46{-# LANGUAGE FlexibleContexts #-}
57{-# LANGUAGE FlexibleInstances #-}
68{-# LANGUAGE GADTs #-}
7−{-# LANGUAGE KindSignatures #-}
89{-# LANGUAGE MultiParamTypeClasses #-}
910{-# LANGUAGE NoStarIsType #-}
1011{-# LANGUAGE RankNTypes #-}
@@ -55,15 +56,24 @@ module LAoP.Matrix.Type
5556 -- * Type safe matrix representation
5657 Matrix (..),
5758
59+ -- * Constraint type aliases
60+ Countable,
61+ CountableDims,
62+ CountableN,
63+ CountableDimsN,
64+ FLN,
65+ Liftable,
66+ Trivial,
67+ TrivialP,
68+
5869 -- * Type aliases
5970 Zero,
6071 One,
6172
6273 -- * Primitives
63− empty,
6474 one,
65− junc,
66− split,
75+ join,
76+ fork,
6777
6878 -- * Auxiliary type families
6979 I.FromNat,
@@ -75,24 +85,27 @@ module LAoP.Matrix.Type
7585 fromLists,
7686 toLists,
7787 toList,
88+ matrixBuilder',
7889 matrixBuilder,
7990 row,
8091 col,
8192 zeros,
8293 ones,
8394 bang,
95+ point,
8496 constant,
8597
8698 -- * Functor instance equivalent function
8799 fmapM,
100+ bimapM,
88101
89102 -- * Applicative/Monoidal instance equivalent functions
90103 unitM,
91104 multM,
92105
93106 -- * Selective equivalent instance function
94− selectM,
95−
107+ selectM,
108+
96109 -- * Monad equivalent instance function
97110 returnM,
98111 bindM,
@@ -100,25 +113,34 @@ module LAoP.Matrix.Type
100113 -- * Misc
101114 -- ** Get dimensions
102115 columns,
116+ columns',
103117 rows,
118+ rows',
104119
105120 -- ** Matrix Transposition
106121 tr,
107122
123+ -- ** Scalar multiplication/division of matrices
124+ (.|),
125+ (./),
126+
108127 -- ** McCarthy's Conditional
109128 cond,
110129
111130 -- ** Matrix "abiding"
112− abideJS,
113− abideSJ,
131+ abideJF,
132+ abideFJ,
133+
134+ -- ** Zip Matrices
135+ zipWithM,
114136
115137 -- * Biproduct approach
116− -- ** Split
138+ -- ** Fork
117139 (===),
118140 -- *** Projections
119141 p1,
120142 p2,
121− -- ** Junc
143+ -- ** Join
122144 (|||),
123145 -- *** Injections
124146 i1,
@@ -132,11 +154,11 @@ module LAoP.Matrix.Type
132154 -- | Note that given the restrictions imposed it is not possible to
133155 -- implement the standard type classes present in standard Haskell.
134156 -- *** Matrix pairing projections
135− kp1,
136− kp2,
157+ fstM,
158+ sndM,
137159
138160 -- *** Matrix pairing
139− khatri,
161+ kr,
140162
141163 -- * Matrix composition and lifting
142164
@@ -144,10 +166,13 @@ module LAoP.Matrix.Type
144166
145167 -- | Note that given the restrictions imposed it is not possible to
146168 -- implement the standard type classes present in standard Haskell.
147− identity,
169+ iden,
148170 comp,
149− fromF,
150171 fromF',
172+ fromF,
173+
174+ -- * Relation
175+ toRel,
151176
152177 -- * Matrix printing
153178 pretty,
@@ -158,22 +183,44 @@ where
158183import Data.Void
159184import Data.Proxy
160185import Data.Kind
161−import GHC.TypeLits
186+import GHC.TypeLits
162187import Control.DeepSeq
163−import qualified Control.Category as C
188+import LAoP.Utils
164189import qualified LAoP.Matrix.Internal as I
190+import Prelude hiding (id, (.))
165191
166192newtype Matrix e (cols :: Type) (rows :: Type) = M (I.Matrix e (I.Normalize cols) (I.Normalize rows))
167193 deriving (Show, Num, Eq, Ord, NFData) via (I.Matrix e (I.Normalize cols) (I.Normalize rows))
168194
169−-- | It isn't possible to implement the 'id' function so it's
170−-- implementation is 'undefined'. However 'comp' can be and this partial
171−-- class implementation exists just to make the code more readable.
172−--
173−-- Please use 'identity' instead.
174−instance (Num e) => C.Category (Matrix e) where
175− id = undefined
176− (.) = comp
195+-- | Constraint type synonyms to keep the type signatures less convoluted
196+type Countable a = KnownNat (I.Count a)
197+type CountableDims a b = (Countable a, Countable b)
198+type CountableN a = KnownNat (I.Count (I.Normalize a))
199+type CountableDimsN a b = (CountableN a, CountableN b)
200+type FLN a b = I.FromLists (I.Normalize a) (I.Normalize b)
201+type Liftable e a b = (Bounded a, Bounded b, Enum a, Enum b, Eq b, Num e, Ord e)
202+type Trivial a = I.Normalize (I.Normalize a) ~ I.Normalize (I.Normalize (I.Normalize a))
203+type Trivial2 a = I.Normalize a ~ I.Normalize (I.Normalize a)
204+type Trivial3 a = I.FromNat (I.Count (I.Normalize (I.Normalize a))) ~ I.Normalize (I.Normalize a)
205+type TrivialP a b = I.Normalize (a, b) ~ I.Normalize (I.Normalize a, I.Normalize b)
206+
207+-- | It is possible to implement a constrained version of the category type
208+-- class.
209+instance (Num e) => Category (Matrix e) where
210+ type Object (Matrix e) a = (FLN a a, CountableN a)
211+ id = iden
212+ (.) = comp
213+
214+-- | Bifunctor equivalent function
215+bimapM ::
216+ ( Liftable e a b,
217+ Liftable e c d,
218+ CountableDimsN a c,
219+ CountableDimsN b d,
220+ FLN d c,
221+ FLN b a
222+ ) => (a -> b) -> (c -> d) -> Matrix e a c -> Matrix e b d
223+bimapM f g m = fromF g . m . tr (fromF f)
177224
178225-- | Zero type alias
179226type Zero = Void
@@ -183,92 +230,75 @@ type One = ()
183230
184231-- Primitives
185232
186−-- | Empty matrix constructor
187−empty :: Matrix e Zero Zero
188−empty = M I.Empty
189−
190233-- | Unit matrix constructor
191234one :: e -> Matrix e One One
192235one = M . I.One
193236
194−-- | Matrix 'Junc' constructor
195−junc ::
196− (I.Normalize (Either a b) ~ Either (I.Normalize a) (I.Normalize b)) =>
237+-- | Matrix 'Join' constructor
238+join ::
197239 Matrix e a rows ->
198240 Matrix e b rows ->
199241 Matrix e (Either a b) rows
200−junc (M a) (M b) = M (I.Junc a b)
242+join (M a) (M b) = M (I.Join a b)
201243
202244infixl 3 |||
203−-- | Matrix 'Junc' constructor
245+-- | Matrix 'Join' constructor
204246(|||) ::
205− (I.Normalize (Either a b) ~ Either (I.Normalize a) (I.Normalize b)) =>
206247 Matrix e a rows ->
207248 Matrix e b rows ->
208249 Matrix e (Either a b) rows
209−(|||) = junc
250+(|||) = join
210251
211−-- | Matrix 'Split' constructor
212−split ::
213− (I.Normalize (Either a b) ~ Either (I.Normalize a) (I.Normalize b)) =>
252+-- | Matrix 'Fork' constructor
253+fork ::
214254 Matrix e cols a ->
215255 Matrix e cols b ->
216256 Matrix e cols (Either a b)
217−split (M a) (M b) = M (I.Split a b)
257+fork (M a) (M b) = M (I.Fork a b)
218258
219259infixl 2 ===
220−-- | Matrix 'Split' constructor
260+-- | Matrix 'Fork' constructor
221261(===) ::
222− (I.Normalize (Either a b) ~ Either (I.Normalize a) (I.Normalize b)) =>
223262 Matrix e cols a ->
224263 Matrix e cols b ->
225264 Matrix e cols (Either a b)
226−(===) = split
265+(===) = fork
227266
228267-- Functor hierarchy
229268
230269-- | Functor instance equivalent function
231−fmapM ::
232− ( Bounded a,
233− Bounded b,
234− Enum a,
235− Enum b,
236− Eq b,
237− Num e,
238− Ord e,
239− KnownNat (I.Count (I.Normalize a)),
240− KnownNat (I.Count (I.Normalize b)),
241− I.FromLists e (I.Normalize b) (I.Normalize a)
270+fmapM ::
271+ ( Liftable e a b,
272+ CountableDimsN a b,
273+ FLN b a
242274 )
243275 =>
244276 (a -> b) -> Matrix e c a -> Matrix e c b
245−fmapM f m = fromF' f `comp` m
277+fmapM f m = fromF f . m
246278
247279-- | Applicative instance equivalent 'unit' function,
248280unitM :: (Num e) => Matrix e () ()
249281unitM = one 1
250282
251283-- | Applicative instance equivalent 'unit' function,
252−multM ::
253− ( KnownNat (I.Count (I.Normalize a)),
254− KnownNat (I.Count (I.Normalize b)),
255− KnownNat (I.Count (I.Normalize (a, b))),
284+multM ::
285+ ( CountableDimsN a b,
286+ CountableN (a, b),
256287 Num e,
257− I.FromLists e (I.Normalize (a, b)) (I.Normalize a),
258− I.FromLists e (I.Normalize (a, b)) (I.Normalize b),
259− I.Normalize (a, b) ~ I.Normalize (I.Normalize a, I.Normalize b)
288+ FLN (a, b) a,
289+ FLN (a, b) b,
290+ TrivialP a b
260291 ) => Matrix e c a -> Matrix e c b -> Matrix e c (a, b)
261−multM a b = khatri a b
262−
292+multM = kr
263293
264294-- | Monad instance equivalent 'return' function,
265−returnM ::
266− forall e a .
267− ( Num e,
268− Enum e,
269− Enum a,
270− I.FromLists e () (I.Normalize a),
271− KnownNat (I.Count a)
295+returnM ::
296+ forall e a .
297+ ( Num e,
298+ Enum e,
299+ Enum a,
300+ FLN () a,
301+ Countable a
272302 ) => a -> Matrix e One a
273303returnM a = col l
274304 where
@@ -284,62 +314,66 @@ bindM = flip comp
284314
285315-- | Build a matrix out of a list of list of elements. Throws a runtime
286316-- error if the dimensions do not match.
287−fromLists :: (I.FromLists e (I.Normalize cols) (I.Normalize rows)) => [[e]] -> Matrix e cols rows
317+fromLists :: (FLN cols rows) => [[e]] -> Matrix e cols rows
288318fromLists = M . I.fromLists
289319
290320-- | Matrix builder function. Constructs a matrix provided with
291−-- a construction function.
321+-- a construction function that operates with indices.
322+matrixBuilder' ::
323+ (FLN cols rows, CountableDimsN cols rows )
324+ => ((Int, Int) -> e) -> Matrix e cols rows
325+matrixBuilder' = M . I.matrixBuilder'
326+
327+-- | Matrix builder function. Constructs a matrix provided with
328+-- a construction function that operates with arbitrary types.
292329matrixBuilder ::
293− (I.FromLists e (I.Normalize cols) (I.Normalize rows), KnownNat (I.Count (I.Normalize cols)), KnownNat (I.Count (I.Normalize rows))) =>
294− ((Int, Int) -> e) ->
295− Matrix e cols rows
296−matrixBuilder = M . I.matrixBuilder
330+ ( FLN a b,
331+ Enum a,
332+ Enum b,
333+ Bounded a,
334+ Bounded b,
335+ Eq a,
336+ Countable b
337+ ) => ((a, b) -> e) -> Matrix e a b
338+matrixBuilder f = M (I.matrixBuilder f)
297339
298340-- | Constructs a column vector matrix
299−col :: (I.FromLists e () (I.Normalize rows)) => [e] -> Matrix e One rows
341+col :: (FLN () rows) => [e] -> Matrix e One rows
300342col = M . I.col
301343
302344-- | Constructs a row vector matrix
303−row :: (I.FromLists e (I.Normalize cols) ()) => [e] -> Matrix e cols One
345+row :: (FLN cols ()) => [e] -> Matrix e cols One
304346row = M . I.row
305347
306348-- | Lifts functions to matrices with arbitrary dimensions.
307349--
308350-- NOTE: Be careful to not ask for a matrix bigger than the cardinality of
309351-- types @a@ or @b@ allows.
310−fromF ::
311− ( Bounded a,
312− Bounded b,
313− Enum a,
314− Enum b,
315− Eq b,
316− Num e,
317− Ord e,
318− KnownNat (I.Count (I.Normalize cols)),
319− KnownNat (I.Count (I.Normalize rows)),
320− I.FromLists e (I.Normalize rows) (I.Normalize cols)
352+fromF' ::
353+ ( Liftable e a b,
354+ CountableDimsN cols rows,
355+ FLN rows cols
321356 ) =>
322− (a -> b) ->
323− Matrix e cols rows
324−fromF = M . I.fromF
357+ (a -> b) -> Matrix e cols rows
358+fromF' = M . I.fromF'
325359
326360-- | Lifts functions to matrices with dimensions matching @a@ and @b@
327361-- cardinality's.
328−fromF' ::
329− ( Bounded a,
330− Bounded b,
331− Enum a,
332− Enum b,
333− Eq b,
334− Num e,
335− Ord e,
336− KnownNat (I.Count (I.Normalize a)),
337− KnownNat (I.Count (I.Normalize b)),
338− I.FromLists e (I.Normalize b) (I.Normalize a)
362+fromF ::
363+ ( Liftable e a b,
364+ CountableDimsN a b,
365+ FLN b a
339366 ) =>
340− (a -> b) ->
341− Matrix e a b
342−fromF' = M . I.fromF'
367+ (a -> b) -> Matrix e a b
368+fromF = M . I.fromF
369+
370+-- | Lifts relation functions to Boolean Matrix
371+toRel ::
372+ ( Liftable (Natural 0 1) a b,
373+ CountableDims a b,
374+ FLN b a
375+ ) => (a -> b -> Bool) -> Matrix (Natural 0 1) a b
376+toRel = M . I.toRel
343377
344378-- Conversion
345379
@@ -355,8 +389,8 @@ toList (M m) = I.toList m
355389
356390-- | The zero matrix. A matrix wholly filled with zeros.
357391zeros ::
358− (Num e, I.FromLists e (I.Normalize cols) (I.Normalize rows), KnownNat (I.Count (I.Normalize cols)), KnownNat (I.Count (I.Normalize rows))) =>
359− Matrix e cols rows
392+ (Num e, FLN cols rows, CountableDimsN cols rows)
393+ => Matrix e cols rows
360394zeros = M I.zeros
361395
362396-- Ones Matrix
@@ -365,8 +399,8 @@ zeros = M I.zeros
365399--
366400-- Also known as T (Top) matrix.
367401ones ::
368− (Num e, I.FromLists e (I.Normalize cols) (I.Normalize rows), KnownNat (I.Count (I.Normalize cols)), KnownNat (I.Count (I.Normalize rows))) =>
369− Matrix e cols rows
402+ (Num e, FLN cols rows, CountableDimsN cols rows)
403+ => Matrix e cols rows
370404ones = M I.ones
371405
372406-- Const Matrix
@@ -374,9 +408,8 @@ ones = M I.ones
374408-- | The constant matrix constructor. A matrix wholly filled with a given
375409-- value.
376410constant ::
377− (Num e, I.FromLists e (I.Normalize cols) (I.Normalize rows), KnownNat (I.Count (I.Normalize cols)), KnownNat (I.Count (I.Normalize rows))) =>
378− e ->
379− Matrix e cols rows
411+ (Num e, FLN cols rows, CountableDimsN cols rows)
412+ => e -> Matrix e cols rows
380413constant = M . I.constant
381414
382415-- Bang Matrix
@@ -384,17 +417,30 @@ constant = M . I.constant
384417-- | The T (Top) row vector matrix.
385418bang ::
386419 forall e cols.
387− (Num e, Enum e, I.FromLists e (I.Normalize cols) (), KnownNat (I.Count (I.Normalize cols))) =>
420+ (Num e, Enum e, FLN cols (), CountableN cols) =>
388421 Matrix e cols One
389422bang = M I.bang
390423
391−-- Identity Matrix
424+-- | Point constant relation
425+point ::
426+ ( Bounded a,
427+ Enum a,
428+ Eq a,
429+ Num e,
430+ Ord e,
431+ CountableN a,
432+ FLN a One
433+ ) => a -> Matrix e One a
434+point = fromF . const
435+
436+-- iden Matrix
392437
393−-- | Identity matrix
394−identity ::
395− (Num e, I.FromLists e (I.Normalize a) (I.Normalize a), KnownNat (I.Count (I.Normalize a))) =>
438+-- | iden matrix
439+iden ::
440+ (Num e, FLN a a, CountableN a) =>
396441 Matrix e a a
397−identity = M I.identity
442+iden = M I.iden
443+{-# NOINLINE iden #-}
398444
399445-- Matrix composition (MMM)
400446
@@ -404,15 +450,32 @@ identity = M I.identity
404450-- from LAoP.
405451comp :: (Num e) => Matrix e cr rows -> Matrix e cols cr -> Matrix e cols rows
406452comp (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)
407472
408473-- | Biproduct first component projection
409474p1 ::
410475 ( Num e,
411− KnownNat (I.Count (I.Normalize n)),
412− KnownNat (I.Count (I.Normalize m)),
413− I.FromLists e (I.Normalize n) (I.Normalize m),
414− I.FromLists e (I.Normalize m) (I.Normalize m),
415− I.Normalize (Either m n) ~ Either (I.Normalize m) (I.Normalize n)
476+ CountableDimsN n m,
477+ FLN n m,
478+ FLN m m
416479 ) =>
417480 Matrix e (Either m n) m
418481p1 = M I.p1
@@ -420,11 +483,9 @@ p1 = M I.p1
420483-- | Biproduct second component projection
421484p2 ::
422485 ( Num e,
423− KnownNat (I.Count (I.Normalize n)),
424− KnownNat (I.Count (I.Normalize m)),
425− I.FromLists e (I.Normalize m) (I.Normalize n),
426− I.FromLists e (I.Normalize n) (I.Normalize n),
427− I.Normalize (Either m n) ~ Either (I.Normalize m) (I.Normalize n)
486+ CountableDimsN n m,
487+ FLN m n,
488+ FLN n n
428489 ) =>
429490 Matrix e (Either m n) n
430491p2 = M I.p2
@@ -434,11 +495,9 @@ p2 = M I.p2
434495-- | Biproduct first component injection
435496i1 ::
436497 ( Num e,
437− KnownNat (I.Count (I.Normalize n)),
438− KnownNat (I.Count (I.Normalize m)),
439− I.FromLists e (I.Normalize n) (I.Normalize m),
440− I.FromLists e (I.Normalize m) (I.Normalize m),
441− I.Normalize (Either m n) ~ Either (I.Normalize m) (I.Normalize n)
498+ CountableDimsN n m,
499+ FLN n m,
500+ FLN m m
442501 ) =>
443502 Matrix e m (Either m n)
444503i1 = tr p1
@@ -446,11 +505,9 @@ i1 = tr p1
446505-- | Biproduct second component injection
447506i2 ::
448507 ( Num e,
449− KnownNat (I.Count (I.Normalize n)),
450− KnownNat (I.Count (I.Normalize m)),
451− I.FromLists e (I.Normalize m) (I.Normalize n),
452− I.FromLists e (I.Normalize n) (I.Normalize n),
453− I.Normalize (Either m n) ~ Either (I.Normalize m) (I.Normalize n)
508+ CountableDimsN n m,
509+ FLN m n,
510+ FLN n n
454511 ) =>
455512 Matrix e n (Either m n)
456513i2 = tr p2
@@ -459,24 +516,34 @@ i2 = tr p2
459516
460517-- | Obtain the number of rows.
461518--
462−-- NOTE: The 'KnownNat' constaint is needed in order to obtain the
463−-- dimensions in constant time.
464−--
465−-- TODO: A 'rows' function that does not need the 'KnownNat' constraint in
466−-- exchange for performance.
467−rows :: (KnownNat (I.Count (I.Normalize rows))) => Matrix e cols rows -> Int
519+-- NOTE: The 'KnownNat' constraint is needed in order to obtain the
520+-- dimensions in constant time. For a version that doesn't require the
521+-- constraint see 'rows''.
522+rows :: (CountableN rows) => Matrix e cols rows -> Int
468523rows (M m) = I.rows m
469524
525+-- | Obtain the number of rows in an inefficient manner, but without any
526+-- constraints.
527+--
528+-- For a more efficient version see 'rows'.
529+rows' :: Matrix e cols rows -> Int
530+rows' (M m) = I.rows' m
531+
470532-- | Obtain the number of columns.
471−--
472−-- NOTE: The 'KnownNat' constaint is needed in order to obtain the
473−-- dimensions in constant time.
474533--
475−-- TODO: A 'columns' function that does not need the 'KnownNat' constraint in
476−-- exchange for performance.
477−columns :: (KnownNat (I.Count (I.Normalize cols))) => Matrix e cols rows -> Int
534+-- NOTE: The 'KnownNat' constraint is needed in order to obtain the
535+-- dimensions in constant time. For a version that doesn't require the
536+-- constraint see 'columns''.
537+columns :: (CountableN cols) => Matrix e cols rows -> Int
478538columns (M m) = I.columns m
479539
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+
480547-- Coproduct Bifunctor
481548
482549infixl 5 -|-
@@ -484,14 +551,11 @@ infixl 5 -|-
484551-- | Matrix coproduct functor also known as matrix direct sum.
485552(-|-) ::
486553 ( Num e,
487− KnownNat (I.Count (I.Normalize j)),
488− KnownNat (I.Count (I.Normalize k)),
489− I.FromLists e (I.Normalize k) (I.Normalize k),
490− I.FromLists e (I.Normalize j) (I.Normalize k),
491− I.FromLists e (I.Normalize k) (I.Normalize j),
492− I.FromLists e (I.Normalize j) (I.Normalize j),
493− I.Normalize (Either n m) ~ Either (I.Normalize n) (I.Normalize m),
494− I.Normalize (Either k j) ~ Either (I.Normalize k) (I.Normalize j)
554+ CountableDimsN j k,
555+ FLN k k,
556+ FLN j k,
557+ FLN k j,
558+ FLN j j
495559 ) =>
496560 Matrix e n k ->
497561 Matrix e m j ->
@@ -501,104 +565,98 @@ infixl 5 -|-
501565-- Khatri Rao Product and projections
502566
503567-- | Khatri Rao product first component projection matrix.
504−kp1 ::
568+fstM ::
505569 forall e m k .
506570 ( Num e,
507− KnownNat (I.Count (I.Normalize m)),
508− KnownNat (I.Count (I.Normalize k)),
509− KnownNat (I.Count (I.Normalize (m, k))),
510− I.FromLists e (I.Normalize (m, k)) (I.Normalize m),
511− I.Normalize (m, k) ~ I.Normalize (I.Normalize m, I.Normalize k)
571+ CountableDimsN m k,
572+ CountableN (m, k),
573+ FLN (m, k) m,
574+ TrivialP m k
512575 ) => Matrix e (m, k) m
513−kp1 = M (I.kp1 @e @(I.Normalize m) @(I.Normalize k))
576+fstM = M (I.fstM @e @(I.Normalize m) @(I.Normalize k))
514577
515578-- | Khatri Rao product second component projection matrix.
516−kp2 ::
579+sndM ::
517580 forall e m k.
518581 ( Num e,
519− KnownNat (I.Count (I.Normalize k)),
520− KnownNat (I.Count (I.Normalize m)),
521− KnownNat (I.Count (I.Normalize (m, k))),
522− I.FromLists e (I.Normalize (m, k)) (I.Normalize k),
523− I.Normalize (m, k) ~ I.Normalize (I.Normalize m, I.Normalize k)
582+ CountableDimsN k m,
583+ CountableN (m, k),
584+ FLN (m, k) k,
585+ TrivialP m k
524586 ) => Matrix e (m, k) k
525−kp2 = M (I.kp2 @e @(I.Normalize m) @(I.Normalize k))
587+sndM = M (I.sndM @e @(I.Normalize m) @(I.Normalize k))
526588
527589-- | Khatri Rao Matrix product also known as matrix pairing.
528590--
529591-- NOTE: That this is not a true categorical product, see for instance:
530−--
592+--
531593-- @
532−-- | kp1 `comp` khatri a b == a
533−-- khatri a b ==> |
534−-- | kp2 `comp` khatri a b == b
594+-- | fstM . kr a b == a
595+-- kr a b ==> |
596+-- | sndM . kr a b == b
535597-- @
536598--
537599-- __Emphasis__ on the implication symbol.
538−khatri ::
600+kr ::
539601 forall e cols a b.
540602 ( Num e,
541− KnownNat (I.Count (I.Normalize a)),
542− KnownNat (I.Count (I.Normalize b)),
543− KnownNat (I.Count (I.Normalize (a, b))),
544− I.FromLists e (I.Normalize (a, b)) (I.Normalize a),
545− I.FromLists e (I.Normalize (a, b)) (I.Normalize b),
546− I.Normalize (a, b) ~ I.Normalize (I.Normalize a, I.Normalize b)
603+ CountableDimsN a b,
604+ CountableN (a, b),
605+ FLN (a, b) a,
606+ FLN (a, b) b,
607+ TrivialP a b
547608 ) => Matrix e cols a -> Matrix e cols b -> Matrix e cols (a, b)
548−khatri a b =
549− let kp1' = kp1 @e @a @b
550− kp2' = kp2 @e @a @b
551− in comp (tr kp1') a * comp (tr kp2') b
609+kr a b =
610+ let fstM' = fstM @e @a @b
611+ sndM' = sndM @e @a @b
612+ in comp (tr fstM') a * comp (tr sndM') b
552613
553614-- Product Bifunctor (Kronecker)
554615
555616infixl 4 ><
556617
557−-- | Matrix product functor also known as kronecker product
618+-- | Matrix product functor also known as Kronecker product
558619(><) ::
559620 forall e m p n q.
560621 ( Num e,
561− KnownNat (I.Count (I.Normalize m)),
562− KnownNat (I.Count (I.Normalize n)),
563− KnownNat (I.Count (I.Normalize p)),
564− KnownNat (I.Count (I.Normalize q)),
565− KnownNat (I.Count (I.Normalize (m, n))),
566− KnownNat (I.Count (I.Normalize (p, q))),
567− I.FromLists e (I.Normalize (m, n)) (I.Normalize m),
568− I.FromLists e (I.Normalize (m, n)) (I.Normalize n),
569− I.FromLists e (I.Normalize (p, q)) (I.Normalize p),
570− I.FromLists e (I.Normalize (p, q)) (I.Normalize q),
571− I.Normalize (m, n) ~ I.Normalize (I.Normalize m, I.Normalize n),
572− I.Normalize (p, q) ~ I.Normalize (I.Normalize p, I.Normalize q)
622+ CountableDimsN m n,
623+ CountableDimsN p q,
624+ CountableDimsN (m, n) (p, q),
625+ FLN (m, n) m,
626+ FLN (m, n) n,
627+ FLN (p, q) p,
628+ FLN (p, q) q,
629+ TrivialP m n,
630+ TrivialP p q
573631 ) => Matrix e m p -> Matrix e n q -> Matrix e (m, n) (p, q)
574632(><) a b =
575− let kp1' = kp1 @e @m @n
576− kp2' = kp2 @e @m @n
577− in khatri (comp a kp1') (comp b kp2')
633+ let fstM' = fstM @e @m @n
634+ sndM' = sndM @e @m @n
635+ in kr (comp a fstM') (comp b sndM')
578636
579−-- Matrix abide Junc Split
637+-- Matrix abide Join Fork
580638
581−-- | Matrix "abiding" followin the 'Junc'-'Split' abide law.
582−--
639+-- | Matrix "abiding" followin the 'Join'-'Fork' abide law.
640+--
583641-- Law:
584642--
585643-- @
586−-- 'Junc' ('Split' a c) ('Split' b d) == 'Split' ('Junc' a b) ('Junc' c d)
644+-- 'Join' ('Fork' a c) ('Fork' b d) == 'Fork' ('Join' a b) ('Join' c d)
587645-- @
588−abideJS :: Matrix e cols rows -> Matrix e cols rows
589−abideJS (M m) = M (I.abideJS m)
646+abideJF :: Matrix e cols rows -> Matrix e cols rows
647+abideJF (M m) = M (I.abideJF m)
590648
591−-- Matrix abide Split Junc
649+-- Matrix abide Fork Join
592650
593−-- | Matrix "abiding" followin the 'Split'-'Junc' abide law.
594−--
651+-- | Matrix "abiding" followin the 'Fork'-'Join' abide law.
652+--
595653-- Law:
596654--
597655-- @
598−-- 'Split' ('Junc' a b) ('Junc' c d) == 'Junc' ('Split' a c) ('Split' b d)
656+-- 'Fork' ('Join' a b) ('Join' c d) == 'Join' ('Fork' a c) ('Fork' b d)
599657-- @
600−abideSJ :: Matrix e cols rows -> Matrix e cols rows
601−abideSJ (M m) = M (I.abideSJ m)
658+abideFJ :: Matrix e cols rows -> Matrix e cols rows
659+abideFJ (M m) = M (I.abideFJ m)
602660
603661-- Matrix transposition
604662
@@ -610,11 +668,10 @@ tr (M m) = M (I.tr m)
610668
611669-- | Selective functors 'select' operator equivalent inspired by the
612670-- ArrowMonad solution presented in the paper.
613−selectM ::
671+selectM ::
614672 ( Num e,
615− I.FromLists e (I.Normalize b) (I.Normalize b),
616− KnownNat (I.Count (I.Normalize b)),
617− I.Normalize (Either a b) ~ Either (I.Normalize a) (I.Normalize b)
673+ FLN b b,
674+ CountableN b
618675 ) => Matrix e cols (Either a b) -> Matrix e a b -> Matrix e cols b
619676selectM (M m) (M y) = M (I.select m y)
620677
@@ -622,15 +679,14 @@ selectM (M m) (M y) = M (I.select m y)
622679
623680-- | McCarthy's Conditional expresses probabilistic choice.
624681cond ::
625− ( I.Normalize (I.Normalize a) ~ I.Normalize a,
626− KnownNat (I.Count (I.Normalize a)),
627− I.FromLists e () (I.Normalize a),
628− I.FromLists e (I.Normalize a) (),
629− I.FromLists e (I.Normalize a) (I.Normalize a),
630− Bounded a,
631− Enum a,
632− Num e,
633− Ord e
682+ ( Trivial a,
683+ Trivial2 a,
684+ Trivial3 a,
685+ CountableN a,
686+ FLN () a,
687+ FLN a (),
688+ FLN a a,
689+ Liftable e a Bool
634690 )
635691 =>
636692 (a -> Bool) -> Matrix e a b -> Matrix e a b -> Matrix e a b
@@ -639,9 +695,13 @@ cond p (M a) (M b) = M (I.cond p a b)
639695-- Pretty print
640696
641697-- | Matrix pretty printer
642−pretty :: (KnownNat (I.Count (I.Normalize cols)), Show e) => Matrix e cols rows -> String
698+pretty :: (CountableDimsN cols rows, Show e) => Matrix e cols rows -> String
643699pretty (M m) = I.pretty m
644700
645701-- | Matrix pretty printer
646−prettyPrint :: (KnownNat (I.Count (I.Normalize cols)), Show e) => Matrix e cols rows -> IO ()
702+prettyPrint :: (CountableDimsN cols rows, Show e) => Matrix e cols rows -> IO ()
647703prettyPrint (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+80−6
@@ -30,11 +30,22 @@ module LAoP.Relation
3030 Relation (..),
3131 Boolean,
3232
33+ -- * Constraint type synonyms
34+ Countable,
35+ CountableDims,
36+ CountableN,
37+ CountableDimsN,
38+ FLN,
39+ Liftable,
40+ Trivial,
41+ TrivialP,
42+
3343 -- * Primitives
34− empty,
3544 one,
36− junc,
37− split,
45+ join,
46+ (|||),
47+ fork,
48+ (===),
3849
3950 -- * Auxiliary type families
4051 FromNat,
@@ -44,21 +55,74 @@ module LAoP.Relation
4455 -- * Matrix construction and conversion
4556 FromLists,
4657 fromLists,
58+ fromF,
59+ fromF',
60+ toRel,
4761 toLists,
4862 toList,
49− matrixBuilder,
63+ toBool,
64+ pt,
65+ belongs,
66+ relationBuilder,
5067 zeros,
5168 ones,
5269 bang,
70+ point,
5371
5472 -- * Relational operations
5573 conv,
5674 intersection,
5775 union,
5876 sse,
77+ implies,
78+ iff,
5979 ker,
6080 img,
6181
82+ -- * Taxonomy of binary relations
83+ injective,
84+ entire,
85+ simple,
86+ surjective,
87+ representation,
88+ function,
89+ abstraction,
90+ injection,
91+ surjection,
92+ bijection,
93+ domain,
94+ range,
95+
96+ -- * Function division
97+ divisionF,
98+
99+ -- * Relation division
100+ divR,
101+ divL,
102+ divS,
103+ shrunkBy,
104+ overriddenBy,
105+
106+ -- * Relational pairing
107+ splitR,
108+
109+ -- ** Projections
110+ fstR,
111+ sndR,
112+ -- ** Bifunctor
113+ (><),
114+ -- * Relational coproduct
115+ eitherR,
116+ -- ** Injections
117+ i1,
118+ i2,
119+ -- ** Bifunctor
120+ (-|-),
121+
122+ -- * Relational "currying"
123+ trans,
124+ untrans,
125+
62126 -- * (Endo-)Relational properties
63127 reflexive,
64128 coreflexive,
@@ -72,16 +136,26 @@ module LAoP.Relation
72136 linearOrder,
73137 equivalence,
74138 partialEquivalence,
139+ difunctional,
140+
141+ -- * Conditionals
142+ equalizer,
75143
76144 -- ** McCarthy's Conditional
77− -- cond,
145+ predR,
146+ guard,
147+ cond,
78148
79149 -- * Relational composition and lifting
80− identity,
150+ iden,
81151 comp,
82152 fromF,
83153 fromF',
84154
155+ -- ** Relational application
156+ pointAp,
157+ pointApBool,
158+
85159 -- * Matrix printing
86160 pretty,
87161 prettyPrint
src/LAoP/Relation/Internal.hs+761−129
@@ -1,6 +1,9 @@
1+{-# LANGUAGE TypeFamilies #-}
2+{-# LANGUAGE ConstraintKinds #-}
13{-# LANGUAGE GADTs #-}
24{-# LANGUAGE UndecidableInstances #-}
35{-# LANGUAGE FlexibleContexts #-}
6+{-# LANGUAGE TypeApplications #-}
47{-# LANGUAGE ScopedTypeVariables #-}
58{-# LANGUAGE StandaloneDeriving #-}
69{-# LANGUAGE DerivingVia #-}
@@ -26,7 +29,7 @@
2629
2730module LAoP.Relation.Internal
2831 ( -- | This definition makes use of the fact that 'Void' is
29− -- isomorphic to 0 and '()' to 1 and captures matrix
32+ -- isomorphic to 0 and 'One' to 1 and captures matrix
3033 -- dimensions as stacks of 'Either's.
3134 --
3235 -- There exists two type families that make it easier to write
@@ -38,11 +41,22 @@ module LAoP.Relation.Internal
3841 Relation (..),
3942 Boolean,
4043
44+ -- * Constraint type synonyms
45+ Countable,
46+ CountableDims,
47+ CountableN,
48+ CountableDimsN,
49+ FLN,
50+ Liftable,
51+ Trivial,
52+ TrivialP,
53+
4154 -- * Primitives
42− empty,
4355 one,
44− junc,
45− split,
56+ join,
57+ (|||),
58+ fork,
59+ (===),
4660
4761 -- * Auxiliary type families
4862 I.FromNat,
@@ -52,21 +66,75 @@ module LAoP.Relation.Internal
5266 -- * Matrix construction and conversion
5367 I.FromLists,
5468 fromLists,
69+ fromF',
70+ fromF,
71+ toRel,
5572 toLists,
5673 toList,
57− matrixBuilder,
74+ toBool,
75+ pt,
76+ belongs,
77+ relationBuilder',
78+ relationBuilder,
5879 zeros,
5980 ones,
6081 bang,
82+ point,
6183
6284 -- * Relational operations
6385 conv,
6486 intersection,
6587 union,
6688 sse,
89+ implies,
90+ iff,
6791 ker,
6892 img,
6993
94+ -- * Taxonomy of binary relations
95+ injective,
96+ entire,
97+ simple,
98+ surjective,
99+ representation,
100+ function,
101+ abstraction,
102+ injection,
103+ surjection,
104+ bijection,
105+ domain,
106+ range,
107+
108+ -- * Function division
109+ divisionF,
110+
111+ -- * Relation division
112+ divR,
113+ divL,
114+ divS,
115+ shrunkBy,
116+ overriddenBy,
117+
118+ -- * Relational pairing
119+ splitR,
120+
121+ -- ** Projections
122+ fstR,
123+ sndR,
124+ -- ** Bifunctor
125+ (><),
126+ -- * Relational coproduct
127+ eitherR,
128+ -- ** Injections
129+ i1,
130+ i2,
131+ -- ** Bifunctor
132+ (-|-),
133+
134+ -- * Relational "currying"
135+ trans,
136+ untrans,
137+
70138 -- * (Endo-)Relational properties
71139 reflexive,
72140 coreflexive,
@@ -80,15 +148,25 @@ module LAoP.Relation.Internal
80148 linearOrder,
81149 equivalence,
82150 partialEquivalence,
151+ difunctional,
152+
153+ -- * Conditionals
154+ equalizer,
83155
84156 -- ** McCarthy's Conditional
85− -- cond,
157+ predR,
158+ guard,
159+ cond,
86160
87161 -- * Relational composition and lifting
88− identity,
162+ iden,
89163 comp,
90− fromF,
91164 fromF',
165+ fromF,
166+
167+ -- ** Relational application
168+ pointAp,
169+ pointApBool,
92170
93171 -- * Matrix printing
94172 pretty,
@@ -98,15 +176,15 @@ module LAoP.Relation.Internal
98176
99177import Data.Void
100178import qualified LAoP.Matrix.Internal as I
101−import LAoP.Utils
179+import LAoP.Utils.Internal
102180import Control.DeepSeq
103−import qualified Control.Category as C
104−import Data.Coerce
105181import Data.Bool
106182import GHC.TypeLits
183+import Prelude hiding (id, (.))
107184
108185-- | Boolean type synonym for working with boolean matrices
109186type Boolean = Natural 0 1
187+type Powerset a = List (List a)
110188
111189-- | Relation data type.
112190newtype Relation a b = R (I.Matrix Boolean (I.Normalize a) (I.Normalize b))
@@ -114,113 +192,142 @@ newtype Relation a b = R (I.Matrix Boolean (I.Normalize a) (I.Normalize b))
114192
115193deriving instance (Read (I.Matrix Boolean (I.Normalize a) (I.Normalize b))) => Read (Relation a b)
116194
117−-- | It isn't possible to implement the 'id' function so it's
118−-- implementation is 'undefined'. However 'comp' can be and this partial
119−-- class implementation exists just to make the code more readable.
120−--
121−-- Please use 'identity' instead.
122−instance C.Category Relation where
123− id = undefined
124− (.) = comp
195+-- | Constraint type synonyms to keep the type signatures less convoluted
196+type Countable a = KnownNat (I.Count a)
197+type CountableDims a b = (Countable a, Countable b)
198+type CountableN a = KnownNat (I.Count (I.Normalize a))
199+type CountableDimsN a b = (CountableN a, CountableN b)
200+type FLN a b = I.FromLists (I.Normalize a) (I.Normalize b)
201+type Liftable a b = (Bounded a, Bounded b, Enum a, Enum b, Eq b, Num Boolean, Ord Boolean)
202+type Trivial a = I.Normalize a ~ I.Normalize (I.Normalize a)
203+type TrivialP a b = I.Normalize (a, b) ~ I.Normalize (I.Normalize a, I.Normalize b)
204+
205+-- | It is possible to implement a constrained version of the category type
206+-- class.
207+instance Category Relation where
208+ type Object Relation a = (FLN a a, CountableN a)
209+ id = iden
210+ (.) = comp
125211
126212instance Num (Relation a b) where
127− -- | Matrix addition becomes Boolean matrix disjunction
213+ -- | Matrix addition becomes Boolean matrix disjointion
128214 (R a) + (R b) = R (I.orM a b)
129215
130216 -- | Matrix subtraction becomes Relational subtraction
131217 (R a) - (R b) = R (I.subM a b)
132218
133− -- | Matrix multiplication becomes Boolean matrix conjunction
219+ -- | Matrix multiplication becomes Boolean matrix conjointion
134220 (R a) * (R b) = R (I.andM a b)
135221
222+ -- | Matrix negation becomes Boolean matrix negation
223+ negate (R a) = R (I.negateM a)
224+
136225-- Type alias
137226type Zero = Void
138227type One = ()
139228
140229-- Primitives
141230
142−-- | Empty matrix constructor
143−empty :: Relation Zero Zero
144−empty = R I.Empty
145−
146231-- | Unit matrix constructor
147232one :: Boolean -> Relation One One
148233one = R . I.One
149234
150−-- | Boolean Matrix 'Junc' constructor
151−junc :: (I.Normalize (Either a b) ~ Either (I.Normalize a) (I.Normalize b))
152− => Relation a c -> Relation b c -> Relation (Either a b) c
153−junc (R a) (R b) = R (I.Junc a b)
235+-- | Boolean Matrix 'Join' constructor, also known as relational coproduct.
236+--
237+-- See 'eitherR'.
238+join :: Relation a c -> Relation b c -> Relation (Either a b) c
239+join (R a) (R b) = R (I.Join a b)
154240
155241infixl 3 |||
156−-- | Boolean Matrix 'Junc' constructor
242+-- | Boolean Matrix 'Join' constructor
243+--
244+-- See 'eitherR'.
157245(|||) ::
158− (I.Normalize (Either a b) ~ Either (I.Normalize a) (I.Normalize b)) =>
159246 Relation a c ->
160247 Relation b c ->
161248 Relation (Either a b) c
162−(|||) = junc
249+(|||) = join
163250
164−-- | Boolean Matrix 'Split' constructor
165−split :: (I.Normalize (Either a b) ~ Either (I.Normalize a) (I.Normalize b))
166− => Relation c a -> Relation c b -> Relation c (Either a b)
167−split (R a) (R b) = R (I.Split a b)
251+-- | Boolean Matrix 'Fork' constructor, also known as relational product.
252+fork :: Relation c a -> Relation c b -> Relation c (Either a b)
253+fork (R a) (R b) = R (I.Fork a b)
168254
169255infixl 2 ===
170−-- | Boolean Matrix 'Split' constructor
256+-- | Boolean Matrix 'Fork' constructor
171257(===) ::
172− (I.Normalize (Either a b) ~ Either (I.Normalize a) (I.Normalize b)) =>
173258 Relation c a ->
174259 Relation c b ->
175260 Relation c (Either a b)
176−(===) = split
261+(===) = fork
177262
178263-- Construction
179264
180265-- | Build a matrix out of a list of list of elements. Throws a runtime
181266-- error if the dimensions do not match.
182−fromLists :: (I.FromLists Boolean (I.Normalize a) (I.Normalize b)) => [[Boolean]] -> Relation a b
267+fromLists :: (FLN a b) => [[Boolean]] -> Relation a b
183268fromLists = R . I.fromLists
184269
185−-- | Matrix builder function. Constructs a matrix provided with
186−-- a construction function.
187−matrixBuilder ::
188− (I.FromLists Boolean (I.Normalize a) (I.Normalize b), KnownNat (I.Count (I.Normalize a)), KnownNat (I.Count (I.Normalize b))) =>
189− ((Int, Int) -> Boolean) ->
190− Relation a b
191−matrixBuilder = R . I.matrixBuilder
270+-- | Relation builder function. Constructs a relation provided with
271+-- a construction function that operates with indices.
272+relationBuilder' ::
273+ (FLN a b, CountableDimsN a b) =>
274+ ((Int, Int) -> Boolean) -> Relation a b
275+relationBuilder' = R . I.matrixBuilder'
276+
277+-- | Relation builder function. Constructs a relation provided with
278+-- a construction function that operates with arbitrary types.
279+relationBuilder ::
280+ ( FLN a b,
281+ Enum a,
282+ Enum b,
283+ Bounded a,
284+ Bounded b,
285+ Eq a,
286+ CountableDims a b
287+ ) => ((a, b) -> Boolean) -> Relation a b
288+relationBuilder = R . I.matrixBuilder
192289
193290-- | Lifts functions to matrices with arbitrary dimensions.
194291--
195292-- NOTE: Be careful to not ask for a matrix bigger than the cardinality of
196293-- types @a@ or @b@ allows.
197−fromF ::
198− ( Bounded a,
199− Bounded b,
200− Enum a,
201− Enum b,
202− Eq b,
203− KnownNat (I.Count (I.Normalize c)),
204− KnownNat (I.Count (I.Normalize d)),
205− I.FromLists Boolean (I.Normalize d) (I.Normalize c)
294+fromF' ::
295+ ( Liftable a b,
296+ CountableDimsN c d,
297+ FLN d c
206298 )
207299 => (a -> b) -> Relation c d
208−fromF f = R (I.fromFRel f)
300+fromF' f = R (I.fromFRel' f)
209301
210302-- | Lifts functions to matrices with dimensions matching @a@ and @b@
211303-- cardinality's.
212−fromF' ::
213− ( Bounded b,
214− Bounded a,
215− Enum a,
216− Enum b,
217− Eq b,
218− KnownNat (I.Count (I.Normalize a)),
219− KnownNat (I.Count (I.Normalize b)),
220− I.FromLists Boolean (I.Normalize b) (I.Normalize a)
304+fromF ::
305+ ( Liftable a b,
306+ CountableDimsN a b,
307+ FLN b a
221308 )
222309 => (a -> b) -> Relation a b
223−fromF' f = R (I.fromFRel' f)
310+fromF f = R (I.fromFRel f)
311+
312+-- | Lifts relation functions to 'Relation'
313+toRel ::
314+ ( Liftable a b,
315+ CountableDims a b,
316+ FLN b a
317+ )
318+ => (a -> b -> Bool) -> Relation a b
319+toRel = R . I.toRel
320+
321+-- | Lowers a 'Relation' to a function
322+fromRel ::
323+ ( Liftable a b,
324+ Eq a,
325+ CountableDimsN a b,
326+ FLN a One,
327+ FLN b One
328+ )
329+ => Relation a b -> (a -> b -> Bool)
330+fromRel r a b = pointApBool a b r
224331
225332-- Conversion
226333
@@ -232,46 +339,188 @@ toLists (R m) = I.toLists m
232339toList :: Relation a b -> [Boolean]
233340toList (R m) = I.toList m
234341
342+-- | Converts a well typed 'Relation' to 'Bool'.
343+toBool :: Relation One One -> Bool
344+toBool r = case toList r of
345+ [Nat 0] -> False
346+ _ -> True
347+
348+-- | Power transpose.
349+--
350+-- Maps a relation to a set valued function.
351+pt ::
352+ ( Liftable a b,
353+ Eq a,
354+ CountableDimsN a b,
355+ FLN a One,
356+ FLN b One
357+ )
358+ => Relation a b -> (a -> List b)
359+pt r a =
360+ let (L lb) = maxBound
361+ in L [ b | b <- lb, toBool (pointAp a b r) ]
362+
363+-- | Belongs relation
364+belongs ::
365+ ( Bounded a,
366+ Enum a,
367+ Eq a,
368+ CountableDims (List a) a,
369+ FLN a (List a)
370+ )
371+ => Relation (List a) a
372+belongs = toRel elemR
373+ where
374+ elemR (L l) x = x `elem` l
375+
235376-- Zeros Matrix
236377
237−-- | The zero matrix. A matrix wholly filled with zeros.
378+-- | The zero relation. A relation where no element of type @a@ relates
379+-- with elements of type @b@.
380+--
381+-- Also known as ⊥ (Bottom) Relation.
382+--
383+-- @
384+-- r `.` ⊥ == ⊥ `.` r == ⊥
385+-- ⊥ ``sse`` R && R ``sse`` T == True
386+-- @
238387zeros ::
239− (I.FromLists Boolean (I.Normalize a) (I.Normalize b), KnownNat (I.Count (I.Normalize a)), KnownNat (I.Count (I.Normalize b))) =>
388+ (FLN a b, CountableDimsN a b) =>
240389 Relation a b
241−zeros = matrixBuilder (const (nat 0))
390+zeros = relationBuilder' (const (nat 0))
242391
243392-- Ones Matrix
244393
245−-- | The ones matrix. A matrix wholly filled with ones.
394+-- | The ones relation. A relation where every element of type @a@ relates
395+-- with every element of type @b@.
246396--
247−-- Also known as T (Top) matrix.
397+-- Also known as T (Top) Relation or universal Relation.
398+--
399+-- @
400+-- ⊥ ``sse`` R && R ``sse`` T == True
401+-- @
248402ones ::
249− (I.FromLists Boolean (I.Normalize a) (I.Normalize b), KnownNat (I.Count (I.Normalize a)), KnownNat (I.Count (I.Normalize b))) =>
403+ (FLN a b, CountableDimsN a b) =>
250404 Relation a b
251−ones = matrixBuilder (const (nat 1))
405+ones = relationBuilder' (const (nat 1))
252406
253407-- Bang Matrix
254408
255−-- | The T (Top) row vector matrix.
409+-- | The T (Top) row vector relation.
256410bang ::
257− forall e a.
258− (I.FromLists Boolean (I.Normalize a) (), KnownNat (I.Count (I.Normalize a))) =>
411+ (FLN a One, CountableN a) =>
259412 Relation a One
260413bang = ones
261414
262−-- Identity Matrix
415+-- | Point constant relation
416+point ::
417+ ( Bounded a,
418+ Enum a,
419+ Eq a,
420+ CountableN a,
421+ FLN a One
422+ ) => a -> Relation One a
423+point = fromF . const
424+
425+-- iden Matrix
263426
264−-- | Identity matrix
265−identity ::
266− (I.FromLists Boolean (I.Normalize a) (I.Normalize a), KnownNat (I.Count (I.Normalize a))) =>
267− Relation a a
268−identity = matrixBuilder (bool (nat 0) (nat 1) . uncurry (==))
427+-- | iden matrix
428+--
429+-- @
430+-- 'iden' `.` r == r == r `.` 'iden'
431+-- @
432+iden ::
433+ (FLN a a, CountableN a) => Relation a a
434+iden = relationBuilder' (bool (nat 0) (nat 1) . uncurry (==))
269435
270436-- | Relational composition
271−comp :: forall a b c . Relation b c -> Relation a b -> Relation a c
437+--
438+-- @
439+-- r `.` (s `.` p) = (r `.` s) `.` p
440+-- @
441+comp :: Relation b c -> Relation a b -> Relation a c
272442comp (R a) (R b) = R (I.compRel a b)
273443
444+-- | Relational right division
445+--
446+-- @'divR' x y@ is the largest relation @z@ which,
447+-- pre-composed with @y@, approximates @x@.
448+divR :: Relation b c -> Relation b a -> Relation a c
449+divR (R x) (R y) = R (I.divR x y)
450+
451+-- | Relational left division
452+--
453+-- The dual division operator:
454+--
455+-- @
456+-- 'divL' y x == 'conv' ('divR' ('conv' x) ('conv' y)
457+-- @
458+divL :: Relation c b -> Relation a b -> Relation a c
459+divL (R x) (R y) = R (I.divL x y)
460+
461+-- | Relational symmetric division
462+--
463+-- @'pointAp' c b ('divS' s r)@ means that @b@ and @c@
464+-- are related to exactly the same outputs by @r@ and by @s@.
465+divS :: Relation c a -> Relation b a -> Relation c b
466+divS (R x) (R y) = R (I.divS x y)
467+
468+-- | Relational shrinking.
469+--
470+-- @r ``shrunkBy`` s@ is the largest part of @r@ such that,
471+-- if it yields an output for an input @x@, it must be a maximum,
472+-- with respect to @s@, among all possible outputs of @x@ by @r@.
473+shrunkBy :: Relation b a -> Relation a a -> Relation b a
474+shrunkBy r s = r `intersection` divR s (conv r)
475+
476+-- | Relational overriding.
477+--
478+-- @r ``overriddenBy`` s@ yields the relation which contains the
479+-- whole of @s@ and that part of @r@ where @s@ is undefined.
480+--
481+-- @
482+-- 'zeros' ``overriddenBy`` s == s
483+-- r ``overriddenBy`` 'zeros' == r
484+-- r ``overriddenBy`` r == r
485+-- @
486+overriddenBy ::
487+ ( FLN b b,
488+ CountableN b
489+ ) => Relation a b -> Relation a b -> Relation a b
490+overriddenBy r s = s `union` r `intersection` divR zeros (conv s)
491+
492+-- | Relational application.
493+--
494+-- If @a@ and @b@ are related by 'Relation' @r@
495+-- then @'pointAp' a b r == 'one' ('nat' 1)@
496+pointAp ::
497+ ( Liftable a b,
498+ Eq a,
499+ CountableDimsN a b,
500+ FLN a One,
501+ FLN b One
502+ ) => a -> b -> Relation a b -> Relation One One
503+pointAp a b r = conv (point b) . r . point a
504+
505+-- | Relational application
506+--
507+-- The same as 'pointAp' but converts 'Boolean' to 'Bool'
508+pointApBool ::
509+ ( Liftable a b,
510+ Eq a,
511+ CountableDimsN a b,
512+ FLN a One,
513+ FLN b One
514+ ) => a -> b -> Relation a b -> Bool
515+pointApBool a b r = toBool $ conv (point b) . r . point a
516+
274517-- | 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
275524conv :: Relation a b -> Relation b a
276525conv (R a) = R (I.tr a)
277526
@@ -279,98 +528,481 @@ conv (R a) = R (I.tr a)
279528sse :: Relation a b -> Relation a b -> Bool
280529sse a b = a <= b
281530
531+-- | Relational implication (the same as @'sse'@)
532+implies :: Relation a b -> Relation a b -> Relation a b
533+implies r s = negate r `union` s
534+
535+-- | Relational bi-implication
536+iff :: Relation a b -> Relation a b -> Bool
537+iff r s = r == s
538+
282539-- | Relational intersection
283540--
284−-- @M `inter` N = M * N@
541+-- Lifts pointwise conjointion.
542+--
543+-- @
544+-- (r ``intersection`` s) ``intersection`` t == r ``intersection`` (s ``intersection`` t)
545+-- x ``sse`` r ``intersection`` s == x ``intersection`` r && x ``intersection`` s
546+-- @
285547intersection :: Relation a b -> Relation a b -> Relation a b
286548intersection a b = a * b
287549
288550-- | Relational union
289551--
290−-- @M `union` N = M + N - M * N
552+-- Lifts pointwise disjointion.
553+--
554+-- @
555+-- (r ``union`` s) ``union`` t == r `'union' (s ``union`` t)
556+-- r ``union`` s ``sse`` x == r ``sse`` x && s ``sse`` x
557+-- r `.` (s ``union`` t) == (r `.` s) ``union`` (r `.` t)
558+-- (s ``union`` t) `.` r == (s `.` r) ``union`` (t `.` r)
559+-- @
291560union :: Relation a b -> Relation a b -> Relation a b
292−union a b = a + b - a * b
561+union a b = a + b
293562
294563-- | Relation Kernel
564+--
565+-- @
566+-- 'ker' r == 'conv' r `.` r
567+-- 'ker' r == 'img' ('conv' r)
568+-- @
295569ker :: Relation a b -> Relation a a
296−ker r = conv r `comp` r
570+ker r = conv r . r
297571
298572-- | Relation Image
573+--
574+-- @
575+-- 'img' r == r `.` conv r
576+-- 'img' r == 'ker' ('conv' r)
577+-- @
299578img :: Relation a b -> Relation b b
300−img r = r `comp` conv r
301−
302−-- | Properties of relations
579+img r = r . conv r
303580
304−-- | A 'Relation' @r@ is reflexive iff @'identity' `'sse'` r@
305−reflexive :: (KnownNat (I.Count (I.Normalize a)), I.FromLists Boolean (I.Normalize a) (I.Normalize a)) => Relation a a -> Bool
306−reflexive r = identity <= r
581+-- | Function division. Special case of 'divS'.
582+--
583+-- NOTE: _This is only valid_ if @f@ and @g@ are 'function's, i.e. 'simple' and
584+-- 'entire'.
585+--
586+-- @'divisionF' f g == 'conv' g `.` f@
587+divisionF :: Relation a c -> Relation b c -> Relation a b
588+divisionF f g = conv g . f
307589
308−-- | A 'Relation' @r@ is coreflexive iff @r `'sse'` 'identity'@
309−coreflexive :: (KnownNat (I.Count (I.Normalize a)), I.FromLists Boolean (I.Normalize a) (I.Normalize a)) => Relation a a -> Bool
310−coreflexive r = r <= identity
590+-- Taxonomy of binary relations
311591
312−-- | A 'Relation' @r@ is simple iff @'coreflexive' ('img' r)@
313−simple :: (KnownNat (I.Count (I.Normalize b)), I.FromLists Boolean (I.Normalize b) (I.Normalize b)) => Relation a b -> Bool
592+-- | A 'Relation' @r@ is 'simple' 'iff' @'coreflexive' ('img' r)@
593+simple :: (CountableN b, FLN b b) => Relation a b -> Bool
314594simple = coreflexive . img
315595
316−-- | A 'Relation' @r@ is injective iff @'coreflexive' ('ker' r)@
317−injective :: (KnownNat (I.Count (I.Normalize a)), I.FromLists Boolean (I.Normalize a) (I.Normalize a)) => Relation a b -> Bool
596+-- | A 'Relation' @r@ is 'injective' 'iff' @'coreflexive' ('ker' r)@
597+injective :: (CountableN a, FLN a a) => Relation a b -> Bool
318598injective = coreflexive . ker
319599
320−-- | A 'Relation' @r@ is entire iff @'reflexive' ('ker' r)@
321−entire :: (KnownNat (I.Count (I.Normalize a)), I.FromLists Boolean (I.Normalize a) (I.Normalize a)) => Relation a b -> Bool
600+-- | A 'Relation' @r@ is 'entire' 'iff' @'reflexive' ('ker' r)@
601+entire :: (CountableN a, FLN a a) => Relation a b -> Bool
322602entire = reflexive . ker
323603
324−-- | A 'Relation' @r@ is surjective iff @'reflexive' ('img' r)@
325−surjective :: (KnownNat (I.Count (I.Normalize b)), I.FromLists Boolean (I.Normalize b) (I.Normalize b)) => Relation a b -> Bool
604+-- | A 'Relation' @r@ is 'surjective' 'iff' @'reflexive' ('img' r)@
605+surjective :: (CountableN b, FLN b b) => Relation a b -> Bool
326606surjective = reflexive . img
327607
328−-- | A 'Relation' @r@ is transitive iff @(r `'comp'` r) `'sse'` r@
608+-- | A 'Relation' @r@ is a 'function' 'iff' @'simple' r && 'entire' r@
609+--
610+-- A 'function' @f@ enjoys the following properties, where @r@ and @s@ are binary
611+-- relations:
612+--
613+-- @
614+-- f `.` r ``sse`` s == r ``sse`` f `.` s
615+-- r `.` f ``sse`` s == r ``sse`` s `.` f
616+-- @
617+function ::
618+ ( CountableDimsN a b,
619+ FLN a a,
620+ FLN b b
621+ )
622+ => Relation a b -> Bool
623+function r = simple r && entire r
624+
625+-- | A 'Relation' @r@ is a 'representation' 'iff' @'injective' r && 'entire' r@
626+representation ::
627+ ( CountableN a,
628+ FLN a a
629+ )
630+ => Relation a b -> Bool
631+representation r = injective r && entire r
632+
633+-- | A 'Relation' @r@ is an 'abstraction' 'iff' @'surjective' r && 'simple' r@
634+abstraction ::
635+ ( CountableN b,
636+ FLN b b
637+ )
638+ => Relation a b -> Bool
639+abstraction r = surjective r && simple r
640+
641+-- | A 'Relation' @r@ is a 'surjection' 'iff' @'function' r && 'abstraction' r@
642+surjection ::
643+ ( CountableDimsN a b,
644+ FLN a a,
645+ FLN b b
646+ )
647+ => Relation a b -> Bool
648+surjection r = function r && abstraction r
649+
650+-- | A 'Relation' @r@ is a 'injection' 'iff' @'function' r && 'representation' r@
651+injection ::
652+ ( CountableDimsN a b,
653+ FLN a a,
654+ FLN b b
655+ )
656+ => Relation a b -> Bool
657+injection r = function r && representation r
658+
659+-- | A 'Relation' @r@ is an 'bijection' 'iff' @'injection' r && 'surjection' r@
660+bijection ::
661+ ( CountableDimsN a b,
662+ FLN b b,
663+ FLN a a
664+ ) => Relation a b -> Bool
665+bijection r = injection r && surjection r
666+
667+-- Properties of relations
668+
669+-- | A 'Relation' @r@ is 'reflexive' 'iff' @'id' ``sse`` r@
670+reflexive :: (CountableN a, FLN a a) => Relation a a -> Bool
671+reflexive r = id <= r
672+
673+-- | A 'Relation' @r@ is 'coreflexive' 'iff' @r ``sse`` 'id'@
674+coreflexive :: (CountableN a, FLN a a) => Relation a a -> Bool
675+coreflexive r = r <= id
676+
677+-- | A 'Relation' @r@ is 'transitive' 'iff' @(r `.` r) ``sse`` r@
329678transitive :: Relation a a -> Bool
330−transitive r = (r `comp` r) `sse` r
679+transitive r = (r . r) `sse` r
331680
332−-- | A 'Relation' @r@ is symmetric iff @r == r@
681+-- | A 'Relation' @r@ is 'symmetric' 'iff' @r == 'conv' r@
333682symmetric :: Relation a a -> Bool
334−symmetric r = r == r
683+symmetric r = r == conv r
335684
336−-- | A 'Relation' @r@ is anti-symmetric iff @(r `'intersection'` 'conv' r) `'sse'` 'identity'@
337−antiSymmetric :: (KnownNat (I.Count (I.Normalize a)), I.FromLists Boolean (I.Normalize a) (I.Normalize a)) => Relation a a -> Bool
338−antiSymmetric r = (r `intersection` conv r) `sse` identity
685+-- | A 'Relation' @r@ is anti-symmetric 'iff' @(r ``intersection`` 'conv' r) ``sse`` 'id'@
686+antiSymmetric :: (CountableN a, FLN a a) => Relation a a -> Bool
687+antiSymmetric r = (r `intersection` conv r) `sse` id
339688
340−-- | A 'Relation' @r@ is irreflexive iff @(r `'intersection'` identity) == 'zeros'@
341−irreflexive :: (KnownNat (I.Count (I.Normalize a)), I.FromLists Boolean (I.Normalize a) (I.Normalize a)) => Relation a a -> Bool
342−irreflexive r = (r `intersection` identity) == zeros
689+-- | A 'Relation' @r@ is 'irreflexive' 'iff' @(r ``intersection`` 'id') == 'zeros'@
690+irreflexive :: (CountableN a, FLN a a) => Relation a a -> Bool
691+irreflexive r = (r `intersection` id) == zeros
343692
344−-- | A 'Relation' @r@ is connected iff @(r `'union'` 'conv' r) == 'ones'@
345−connected :: (KnownNat (I.Count (I.Normalize a)), I.FromLists Boolean (I.Normalize a) (I.Normalize a)) => Relation a a -> Bool
693+-- | A 'Relation' @r@ is 'connected' 'iff' @(r ``union`` 'conv' r) == 'ones'@
694+connected :: (CountableN a, FLN a a) => Relation a a -> Bool
346695connected r = (r `union` conv r) == ones
347696
348−-- | A 'Relation @r@ is a preorder iff @'reflexive' r && 'transitive' r@
349−preorder :: (KnownNat (I.Count (I.Normalize a)), I.FromLists Boolean (I.Normalize a) (I.Normalize a)) => Relation a a -> Bool
697+-- | A 'Relation' @r@ is a 'preorder' 'iff' @'reflexive' r && 'transitive' r@
698+preorder :: (CountableN a, FLN a a) => Relation a a -> Bool
350699preorder r = reflexive r && transitive r
351700
352−-- | A 'Relation @r@ is a partial order iff @'antiSymmetric' r && 'preorder' r@
353−partialOrder :: (KnownNat (I.Count (I.Normalize a)), I.FromLists Boolean (I.Normalize a) (I.Normalize a)) => Relation a a -> Bool
701+-- | A 'Relation' @r@ is a partial-order 'iff' @'antiSymmetric' r && 'preorder' r@
702+partialOrder :: (CountableN a, FLN a a) => Relation a a -> Bool
354703partialOrder r = antiSymmetric r && preorder r
355704
356−-- | A 'Relation @r@ is a linear order iff @'connected' r && 'partialOrder' r@
357−linearOrder :: (KnownNat (I.Count (I.Normalize a)), I.FromLists Boolean (I.Normalize a) (I.Normalize a)) => Relation a a -> Bool
705+-- | A 'Relation' @r@ is a linear-order 'iff' @'connected' r && 'partialOrder' r@
706+linearOrder :: (CountableN a, FLN a a) => Relation a a -> Bool
358707linearOrder r = connected r && partialOrder r
359708
360−-- | A 'Relation @r@ is an equivalence iff @'symmetric' r && 'preorder' r@
361−equivalence :: (KnownNat (I.Count (I.Normalize a)), I.FromLists Boolean (I.Normalize a) (I.Normalize a)) => Relation a a -> Bool
709+-- | A 'Relation' @r@ is an 'equivalence' 'iff' @'symmetric' r && 'preorder' r@
710+equivalence :: (CountableN a, FLN a a) => Relation a a -> Bool
362711equivalence r = symmetric r && preorder r
363712
364−-- | A 'Relation @r@ is a partial equivalence iff @'partialOrder' r && 'equivalence' r@
365−partialEquivalence :: (KnownNat (I.Count (I.Normalize a)), I.FromLists Boolean (I.Normalize a) (I.Normalize a)) => Relation a a -> Bool
713+-- | A 'Relation' @r@ is a partial-equivalence 'iff' @'partialOrder' r && 'equivalence' r@
714+partialEquivalence :: (CountableN a, FLN a a) => Relation a a -> Bool
366715partialEquivalence r = partialOrder r && equivalence r
367716
717+-- | A 'Relation' @r@ is 'difunctional' or regular wherever
718+-- @r `.` 'conv' r `.` r == r@
719+difunctional :: Relation a b -> Bool
720+difunctional r = r . conv r . r == r
721+
722+-- Relational pairing
723+
724+-- | Relational pairing.
725+--
726+-- NOTE: That this is not a true categorical product, see for instance:
727+--
728+-- @
729+-- | 'fstR' `.` 'splitR' a b ``sse`` a
730+-- 'splitR' a b <=> |
731+-- | 'sndR' `.` 'splitR' a b ``sse`` b
732+-- @
733+--
734+-- __Emphasis__ on the 'sse'.
735+--
736+-- @
737+-- 'splitR' r s `.` f == 'splitR' (r `.` f) (s `.` f)
738+-- (R '><' S) `.` 'splitR' p q == 'splitR' (r `.` p) (s `.` q)
739+-- 'conv' ('splitR' r s) `.` 'splitR' x y == ('conv' r `.` x) ``intersection`` ('conv' s `.` y)
740+-- @
741+--
742+-- @
743+-- 'eitherR' ('splitR' r s) ('splitR' t v) == 'splitR' ('eitherR' r t) ('eitherR' s v)
744+-- @
745+splitR ::
746+ ( CountableDimsN a b,
747+ CountableN (a, b),
748+ FLN (a, b) a,
749+ FLN (a, b) b,
750+ TrivialP a b
751+ )
752+ => Relation c a -> Relation c b -> Relation c (a, b)
753+splitR (R f) (R g) = R (I.kr f g)
754+
755+-- | Relational pairing first component projection
756+--
757+-- @
758+-- 'fstR' `.` 'splitR' r s ``sse`` r
759+-- @
760+fstR ::
761+ forall a b .
762+ ( CountableDimsN a b,
763+ CountableN (a, b),
764+ FLN (a, b) a,
765+ TrivialP a b
766+ )
767+ => Relation (a, b) a
768+fstR = R (I.fstM @Boolean @(I.Normalize a) @(I.Normalize b))
769+
770+-- | Relational pairing second component projection
771+--
772+-- @
773+-- 'sndR' `.` 'splitR' r s ``sse`` s
774+-- @
775+sndR ::
776+ forall a b .
777+ ( CountableDimsN a b,
778+ CountableN (a, b),
779+ FLN (a, b) b,
780+ TrivialP a b
781+ )
782+ => Relation (a, b) b
783+sndR = R (I.sndM @Boolean @(I.Normalize a) @(I.Normalize b))
784+
785+-- Relational pairing functor
786+
787+infixl 4 ><
788+-- | Relational pairing functor
789+--
790+-- @
791+-- r '><' s == 'splitR' (r `.` fstR) (s `.` sndR)
792+-- (r '><' s) `.` (p '><' q) == (r `.` p) '><' (s `.` q)
793+-- @
794+(><) ::
795+ ( CountableDimsN a b,
796+ CountableDimsN c d,
797+ CountableDimsN (a, c) (b, d),
798+ FLN (a, c) a,
799+ FLN (a, c) c,
800+ FLN (b, d) b,
801+ FLN (b, d) d,
802+ TrivialP a c,
803+ TrivialP b d
804+ )
805+ => Relation a b -> Relation c d -> Relation (a, c) (b, d)
806+(><) (R a) (R b) = R ((I.><) a b)
807+
808+-- Relational co-products
809+
810+-- | Relational coproduct.
811+--
812+-- @
813+-- | 'eitherR' a b `.` 'i1' == a
814+-- 'eitherR' a b <=> |
815+-- | 'eitherR' a b `.` 'i2' == b
816+-- @
817+--
818+-- @
819+-- 'eitherR' r s `.` 'conv' ('eitherR' t u) == (r `.` 'conv' t) ``union`` (s `.` 'conv' u)
820+-- @
821+--
822+-- @
823+-- 'eitherR' ('splitR' r s) ('splitR' t v) == 'splitR' ('eitherR' r t) ('eitherR' s v)
824+-- @
825+eitherR :: Relation a c -> Relation b c -> Relation (Either a b) c
826+eitherR = join
827+
828+-- | Relational coproduct first component injection
829+--
830+-- @
831+-- 'img' 'i1' ``union`` 'img' 'i2' == 'id'
832+-- 'i1' `.` 'i2' = 'zeros'
833+-- @
834+i1 ::
835+ ( CountableDimsN a b,
836+ FLN b a,
837+ FLN a a
838+ )
839+ => Relation a (Either a b)
840+i1 = R I.i1
841+
842+-- | Relational coproduct second component injection
843+--
844+-- @
845+-- 'img' 'i1' ``union`` 'img' 'i2' == 'id'
846+-- 'i1' `.` 'i2' = 'zeros'
847+-- @
848+i2 ::
849+ ( CountableDimsN a b,
850+ FLN a b,
851+ FLN b b
852+ )
853+ => Relation b (Either a b)
854+i2 = R I.i2
855+
856+infixl 5 -|-
857+
858+-- | Relational coproduct functor.
859+--
860+-- @
861+-- r '-|-' s == 'eitherR' ('i1' `.` r) ('i2' `.` s)
862+-- @
863+(-|-) ::
864+ ( CountableDimsN b d,
865+ FLN b b,
866+ FLN d b,
867+ FLN b d,
868+ FLN d d
869+ )
870+ => Relation a b -> Relation c d -> Relation (Either a c) (Either b d)
871+(-|-) (R a) (R b) = R ((I.-|-) a b)
872+
873+-- Relational "Currying"
874+
875+-- | Relational 'trans'
876+--
877+-- Every n-ary relation can be expressed as a binary relation through
878+-- 'trans'/'untrans';
879+-- more-over, where each particular attribute is placed (input/output) is irrelevant.
880+trans ::
881+ ( CountableDimsN a b,
882+ CountableN c,
883+ CountableDimsN (a, b) (c, b),
884+ FLN (c, b) c,
885+ FLN (c, b) b,
886+ FLN (a, b) a,
887+ FLN (a, b) b,
888+ Trivial (a, b),
889+ Trivial (c, b),
890+ TrivialP a b,
891+ TrivialP c b
892+ )
893+ => Relation (a, b) c -> Relation a (c, b)
894+trans r = splitR r sndR . conv fstR
895+
896+-- | Relational 'untrans'
897+--
898+-- Every n-ary relation can be expressed as a binary relation through
899+-- 'trans'/'untrans';
900+-- more-over, where each particular attribute is placed (input/output) is irrelevant.
901+untrans ::
902+ ( CountableDimsN a b,
903+ CountableN c,
904+ CountableDimsN (a, b) (c, b),
905+ FLN (c, b) c,
906+ FLN (c, b) b,
907+ FLN (a, b) b,
908+ FLN (a, b) a,
909+ Trivial (a, b),
910+ Trivial (c, b),
911+ TrivialP a b,
912+ TrivialP c b
913+ )
914+ => Relation a (c, b) -> Relation (a, b) c
915+untrans s = fstR . conv (splitR (conv s) sndR)
916+
917+-- | Transforms predicate @p@ into a correflexive relation.
918+--
919+-- @
920+-- 'predR' ('const' True) == 'id'
921+-- 'predR' ('const' False) == 'zeros'
922+-- @
923+--
924+-- @
925+-- 'predR' q `.` 'predR' p == 'predR' q ``union`` 'predR' p
926+-- @
927+predR ::
928+ ( Bounded a,
929+ Enum a,
930+ Countable a,
931+ CountableN a,
932+ FLN a a,
933+ FLN Bool a
934+ )
935+ => Relation a Bool -> Relation a a
936+predR p = id `intersection` divisionF (fromF (const True)) p
937+
938+-- | Equalizes functions @f@ and @g@.
939+-- That is, @'equalizer' f g@ is the largest coreflexive
940+-- that restricts @g@ so that @f@ and @g@ yield the same outputs.
941+--
942+-- @
943+-- 'equalizer' r r == 'id'
944+-- 'equalizer' ('point' True) ('point' False) == 'zeros'
945+-- @
946+equalizer ::
947+ ( CountableN a,
948+ FLN a a
949+ )
950+ => Relation a b -> Relation a b -> Relation a a
951+equalizer f g = id `intersection` divisionF f g
952+
953+-- | Relational conditional guard.
954+--
955+-- @
956+-- 'guard' p = 'i2' ``overriddenBy`` 'i1' `.` 'predR' p
957+-- @
958+guard ::
959+ ( Bounded b,
960+ Enum b,
961+ CountableN b,
962+ Countable b,
963+ FLN b b,
964+ FLN Bool b
965+ ) => Relation b Bool -> Relation b (Either b b)
966+guard p = conv (eitherR (predR p) (predR (negate p)))
967+
968+-- | Relational McCarthy's conditional.
969+cond ::
970+ ( Bounded b,
971+ Enum b,
972+ Countable b,
973+ CountableN b,
974+ FLN b b,
975+ FLN Bool b
976+ )
977+ => Relation b Bool -> Relation b c -> Relation b c -> Relation b c
978+cond p r s = eitherR r s . guard p
979+
980+-- | Relational domain.
981+--
982+-- For injective relations, 'domain' and 'ker'nel coincide,
983+-- since @'ker' r ``sse`` 'id'@ in such situations.
984+domain ::
985+ ( CountableN a,
986+ FLN a a
987+ ) => Relation a b -> Relation a a
988+domain r = ker r `intersection` id
989+
990+-- | Relational range.
991+--
992+-- For functions, 'range' and 'img' (image) coincide,
993+-- since @'img' f ``sse`` id@ for any @f@.
994+range ::
995+ ( CountableN b,
996+ FLN b b
997+ ) => Relation a b -> Relation b b
998+range r = img r `intersection` id
999+
3681000-- Relation pretty print
3691001
3701002-- | Relation pretty printing
371−pretty :: (KnownNat (I.Count (I.Normalize a))) => Relation a b -> String
1003+pretty :: (CountableDimsN a b) => Relation a b -> String
3721004pretty (R a) = I.pretty a
3731005
3741006-- | Relation pretty printing
375−prettyPrint :: (KnownNat (I.Count (I.Normalize a))) => Relation a b -> IO ()
1007+prettyPrint :: (CountableDimsN a b) => Relation a b -> IO ()
3761008prettyPrint (R a) = I.prettyPrint a
src/LAoP/Utils.hs+6
@@ -94,6 +94,12 @@ module LAoP.Utils
9494 coerceNat,
9595 coerceNat2,
9696 coerceNat3,
97+
98+ -- * List data type
99+ List (..),
100+
101+ -- * Category type-class
102+ Category(..)
97103 )
98104where
99105
src/LAoP/Utils/Internal.hs+94−74
@@ -1,84 +1,15 @@
1+{-# LANGUAGE TypeFamilies #-}
2+{-# LANGUAGE DeriveGeneric #-}
13{-# LANGUAGE TypeApplications #-}
24{-# LANGUAGE DataKinds #-}
35{-# LANGUAGE FlexibleInstances #-}
46{-# LANGUAGE GeneralizedNewtypeDeriving #-}
5−{-# LANGUAGE KindSignatures #-}
67{-# LANGUAGE ScopedTypeVariables #-}
78
89module LAoP.Utils.Internal
9− ( -- | This is an internal module and it is not meant to be imported.
10− --
11− -- Utility module that provides the 'Natural' data type.
12− -- The semantic associated with this data type is that
13− -- it's meant to be a restricted 'Int' value. For example
14− -- the type @Natural 6@ can only be instanciated with @Nat n@
15− -- where @0 <= n <= 6@. Why, You might ask, because with normal
16− -- 'Int's it is not possible to have a decent @Enum (Int, Int)@
17− -- instance. See the following probabilistic programming model as and
18− -- example:
19− --
20− -- We want to calculate the probability of the sum of two dice throws.
21− -- To do this we start by defining the sample space:
22− --
23− -- @
24− -- type SampleSpace = Int -- We think 'Int' are enough
25− --
26− -- die :: Dist Int 6
27− -- die = unifrom [1..6]
28− --
29− -- -- Promote 'Int' addition to a matrix
30− -- addM = fromF (uncurry (+)) -- Impossible
31− -- @
32− --
33− -- The last line is impossible because @(Int, Int)@ does not have
34− -- a good 'Enum' instance: @[(0, 1), (0, 2), .. (0, maxBound), (1, 0),
35− -- ..]@. And we'd like the addition matrix to be of 36 columns by 12
36− -- rows but limited to integers up to @6@!
37− --
38− -- One way to solve this issue is by defining and auxilary data type to
39− -- represent the sample space:
40− --
41− -- @
42− -- data SampleSpace = S1 | S2 | S3 | S4 | S5 | S6
43− -- deriving (Show, Eq, Enum, Bounded) -- Enum and Bounded are
44− -- important
45− -- @
46− --
47− -- And write the sample space addition function:
48− --
49− -- @
50− -- ssAdd :: SampleSpace -> SampleSpace -> Int
51− -- ssAdd a b = (fromEnum a + 1) + (fromEnum b + 1)
52− -- @
53− --
54− -- And then promote that function to matrix and everything is alright:
55− --
56− -- @
57− -- ssAddM = fromF' (uncurry ssAdd)
58− --
59− -- dieSumProb = ssAddM `comp` (khatri die die)
60− -- @
61− --
62− -- This is a nice solution for small sample spaces. But for larger ones
63− -- it is not feasible to write a data type with hundreds of constructors
64− -- and then write manipulation functions that need to deal with them.
65− -- To mitigate this limitation the 'Natural' type comes a long way and
66− -- allows one to model the sample in an easier way. See for instance:
67− --
68− -- @
69− -- ssAdd :: Natural 6 -> Natural 6 -> Natural 12
70− -- ssAdd = coerceNat (+)
71− --
72− -- ssAddM = fromF' (uncurry sumSS)
73− --
74− -- die :: Dist (Natural 6) 6
75− -- die = uniform [nat @6 1 .. nat 6]
76− --
77− -- dieSumProb = ssAddM `comp` (khatri die die)
78− -- @
79− --
10+ (
8011 -- * 'Natural' data type
81− Natural,
12+ Natural(..),
8213 nat,
8314
8415 -- * Coerce auxiliar functions to help promote 'Int' typed functions to
@@ -86,19 +17,31 @@ module LAoP.Utils.Internal
8617 coerceNat,
8718 coerceNat2,
8819 coerceNat3,
20+
21+ -- * 'List' data type
22+ List (..),
23+
24+ -- * Category type class
25+ Category(..)
8926 )
9027where
9128
9229import Data.Coerce
9330import Data.Proxy
31+import Data.List
32+import Data.Maybe
9433import GHC.TypeLits
9534import Control.DeepSeq
35+import GHC.Generics
36+import Data.Kind
37+import Prelude hiding (id, (.))
38+import qualified Prelude
9639
9740-- | Wrapper around 'Int's that have a restrictive semantic associated.
9841-- A value of type @'Natural' n m@ can only be instanciated with some 'Int'
9942-- @i@ that's @n <= i <= m@.
10043newtype Natural (start :: Nat) (end :: Nat) = Nat Int
101− deriving (Show, Read, Eq, Ord, NFData)
44+ deriving (Show, Read, Eq, Ord, NFData, Generic)
10245
10346-- | Throws a runtime error if any of the operations overflows or
10447-- underflows.
@@ -174,3 +117,80 @@ instance
174117 fstI = fromEnum a
175118 sndI = fromEnum b
176119 in fstI * lengthB + sndI
120+
121+instance
122+ ( Bounded a,
123+ Bounded b
124+ ) => Bounded (Either a b)
125+ where
126+ minBound = Left (minBound :: a)
127+ maxBound = Right (maxBound :: b)
128+
129+instance
130+ ( Enum a,
131+ Bounded a,
132+ Enum b,
133+ Bounded b
134+ ) => Enum (Either a b)
135+ where
136+ toEnum i =
137+ let la = fmap Left ([minBound..maxBound] :: [a])
138+ lb = fmap Right ([minBound..maxBound] :: [b])
139+ in (la ++ lb) !! i
140+
141+ fromEnum (Left a) = fromEnum a
142+ fromEnum (Right b) = fromEnum (maxBound :: a) + fromEnum b + 1
143+
144+-- | Powerset data type.
145+--
146+-- This data type is a newtype wrapper around '[]'. This exists in order to
147+-- implement an 'Enum' and 'Bounded' instance that cannot be harmful for the outside.
148+newtype List a = L [a]
149+ deriving (Eq, Show, Read)
150+
151+powerset :: [a] -> [[a]]
152+powerset [] = [[]]
153+powerset (x:xs) = powerset xs ++ [x:ps | ps <- powerset xs]
154+
155+instance
156+ ( Enum a,
157+ Bounded a
158+ ) => Bounded (List a)
159+ where
160+ minBound = L []
161+ maxBound = L [minBound .. maxBound]
162+
163+instance
164+ ( Bounded a,
165+ Enum a,
166+ Eq a
167+ ) => Enum (List a)
168+ where
169+ toEnum i =
170+ let as = [minBound .. maxBound]
171+ in L (powerset as !! i)
172+
173+ fromEnum (L []) = 0
174+ fromEnum (L x) =
175+ let as = [minBound .. maxBound]
176+ in fromMaybe (error "Does not exist") $ elemIndex x (powerset as)
177+
178+-- | Constrained category instance
179+class Category k where
180+ type Object k o :: Constraint
181+ type Object k o = ()
182+ id :: Object k a => k a a
183+ (.) :: k b c -> k a b -> k a c
184+
185+{-# RULES
186+"identity/left" forall p .
187+ id . p = p
188+"identity/right" forall p .
189+ p . id = p
190+"association" forall p q r .
191+ (p . q) . r = p . (q . r)
192+ #-}
193+
194+instance Category (->) where
195+ id = Prelude.id
196+ (.) = (Prelude..)
stack-8.8.3.yamlnew file+1
@@ -0,0 +1 @@
1+resolver: lts-15.5
stack.yaml+1−66
@@ -1,66 +1 @@
1−# This file was automatically generated by 'stack init'
2−#
3−# Some commonly used options have been documented as comments in this file.
4−# For advanced use and comprehensive documentation of the format, please see:
5−# https://docs.haskellstack.org/en/stable/yaml_configuration/
6−
7−# Resolver to choose a 'specific' stackage snapshot or a compiler version.
8−# A snapshot resolver dictates the compiler version and the set of packages
9−# to be used for project dependencies. For example:
10−#
11−# resolver: lts-3.5
12−# resolver: nightly-2015-09-21
13−# resolver: ghc-7.10.2
14−#
15−# The location of a snapshot can be provided as a file or url. Stack assumes
16−# a snapshot provided as a file might change, whereas a url resource does not.
17−#
18−# resolver: ./custom-snapshot.yaml
19−# resolver: https://example.com/snapshots/2018-01-01.yaml
20−resolver: lts-14.18
21−
22−# User packages to be built.
23−# Various formats can be used as shown in the example below.
24−#
25−# packages:
26−# - some-directory
27−# - https://example.com/foo/bar/baz-0.0.2.tar.gz
28−# subdirs:
29−# - auto-update
30−# - wai
31−packages:
32−- .
33−# Dependency packages to be pulled from upstream that are not in the resolver.
34−# These entries can reference officially published versions as well as
35−# forks / in-progress versions pinned to a git hash. For example:
36−#
37−# extra-deps:
38−# - acme-missiles-0.3
39−# - git: https://github.com/commercialhaskell/stack.git
40−# commit: e7b331f14bcffb8367cd58fbfc8b40ec7642100a
41−#
42−# extra-deps: []
43−
44−# Override default flag values for local packages and extra-deps
45−# flags: {}
46−
47−# Extra package databases containing global packages
48−# extra-package-dbs: []
49−
50−# Control whether we use the GHC we find on the path
51−# system-ghc: true
52−#
53−# Require a specific version of stack, using version ranges
54−# require-stack-version: -any # Default
55−# require-stack-version: ">=2.1"
56−#
57−# Override the architecture used by stack, especially useful on Windows
58−# arch: i386
59−# arch: x86_64
60−#
61−# Extra directories used by stack for building
62−# extra-include-dirs: [/path/to/dir]
63−# extra-lib-dirs: [/path/to/dir]
64−#
65−# Allow a newer minor version of GHC than the snapshot specifies
66−# compiler-check: newer-minor
1+resolver: lts-14.3
stack.yaml.lock+4−4
@@ -6,7 +6,7 @@
66packages: []
77snapshots:
88- completed:
9− size: 524789
10− url: https://raw.githubusercontent.com/commercialhaskell/stackage-snapshots/master/lts/14/18.yaml
11− sha256: 646be71223e08234131c6989912e6011e01b9767bc447b6d466a35e14360bdf2
12− original: lts-14.18
9+ size: 523878
10+ url: https://raw.githubusercontent.com/commercialhaskell/stackage-snapshots/master/lts/14/3.yaml
11+ sha256: 470c46c27746a48c7c50f829efc0cf00112787a7804ee4ac7a27754658f6d92c
12+ original: lts-14.3
test/Examples/Quantum.hsnew file+31
@@ -0,0 +1,31 @@
1+{-# LANGUAGE StandaloneDeriving #-}
2+module Examples.Quantum where
3+
4+import LAoP.Utils
5+import LAoP.Matrix.Type
6+import Data.Complex
7+import Prelude hiding (id, (.))
8+
9+deriving instance Ord a => Ord (Complex a)
10+
11+xor :: (Bool, Bool) -> Bool
12+xor (False, b) = b
13+xor (True, b) = not b
14+
15+ker :: Num e => Matrix e a b -> Matrix e a a
16+ker m = tr m . m
17+
18+cnot :: Matrix (Complex Double) (Bool, Bool) (Bool, Bool)
19+cnot = kr fstM (fromF xor)
20+
21+ccnot :: (Num e, Ord e) => Matrix e ((Bool, Bool), Bool) ((Bool, Bool), Bool)
22+ccnot = kr fstM (fromF f)
23+ where
24+ f = xor . tp (uncurry (&&)) id
25+ tp f g (a,b) = (f a, g b)
26+
27+had :: Matrix (Complex Double) Bool Bool
28+had = (1/sqrt 2) .| fromLists [[1, 1], [1, -1]]
29+
30+bell :: Matrix (Complex Double) (Bool, Bool) (Bool, Bool)
31+bell = cnot . (had >< iden)
test/Examples/Readme.hsnew file+184
@@ -0,0 +1,184 @@
1+{-# LANGUAGE GADTs #-}
2+{-# LANGUAGE DeriveGeneric #-}
3+{-# LANGUAGE FlexibleContexts #-}
4+{-# LANGUAGE TypeApplications #-}
5+{-# LANGUAGE DataKinds #-}
6+
7+module Examples.Readme
8+ ( exec
9+ )
10+ where
11+
12+import LAoP.Matrix.Type
13+import qualified LAoP.Relation as R
14+import LAoP.Utils
15+import LAoP.Dist
16+import GHC.TypeLits
17+import Data.Coerce
18+import qualified GHC.Generics as G
19+import Prelude hiding (id, (.))
20+
21+-- Monty Hall Problem
22+data Outcome = Win | Lose
23+ deriving (Bounded, Enum, Eq, Show, G.Generic)
24+
25+switch :: Outcome -> Outcome
26+switch Win = Lose
27+switch Lose = Win
28+
29+firstChoice :: Matrix Double () Outcome
30+firstChoice = col [1/3, 2/3]
31+
32+secondChoice :: Matrix Double Outcome Outcome
33+secondChoice = fromF switch
34+
35+-- Dice sum
36+
37+type SS = Natural 1 6 -- Sample Space
38+
39+sumSS :: SS -> SS -> Natural 2 12
40+sumSS = coerceNat (+)
41+
42+sumSSM = fromF (uncurry sumSS)
43+
44+condition :: (Int, Int) -> Int -> Int
45+condition (fst, snd) thrd = if fst == snd
46+ then fst * 3
47+ else fst + snd + thrd
48+
49+conditionSS :: (SS, SS) -> SS -> Natural 3 18
50+conditionSS = coerceNat2 condition
51+
52+conditionalThrows = fromF (uncurry conditionSS) . kr (kr die die) die
53+
54+die :: Matrix Double () SS
55+die = col $ map (const (1/6)) [nat @1 @6 1 .. nat 6]
56+
57+-- Sprinkler
58+data G = Dry | Wet
59+ deriving (Bounded, Enum, Eq, Show, G.Generic)
60+
61+data S = Off | On
62+ deriving (Bounded, Enum, Eq, Show, G.Generic)
63+
64+data R = No | Yes
65+ deriving (Bounded, Enum, Eq, Show, G.Generic)
66+
67+rain :: Matrix Double () R
68+rain = matrixBuilder gen
69+ where
70+ gen (_, No) = 0.8
71+ gen (_, Yes) = 0.2
72+
73+sprinkler :: Matrix Double R S
74+sprinkler = matrixBuilder gen
75+ where
76+ gen (No, Off) = 0.6
77+ gen (No, On) = 0.4
78+ gen (Yes, Off) = 0.99
79+ gen (Yes, On) = 0.01
80+
81+grass :: Matrix Double (S, R) G
82+grass = matrixBuilder gen
83+ where
84+ gen ((Off, No), Dry) = 1
85+ gen ((Off, Yes), Dry) = 0.2
86+ gen ((On, No), Dry) = 0.1
87+ gen ((On, Yes), Dry) = 0.01
88+ gen ((Off, No), Wet) = 0
89+ gen ((Off, Yes), Wet) = 0.8
90+ gen ((On, No), Wet) = 0.9
91+ gen ((On, Yes), Wet) = 0.99
92+
93+tag f = kr f id
94+
95+state g s r = tag g . tag s . r
96+
97+grass_wet :: Matrix Double () (G, (S, R)) -> Matrix Double One One
98+grass_wet state = row [0,1] . fstM . state
99+
100+rainning :: Matrix Double (G, (S, R)) One
101+rainning = row [0,1] . sndM . sndM
102+
103+-- Alcuin Puzzle
104+
105+data Being = Farmer | Fox | Goose | Beans
106+ deriving (Bounded, Enum, Eq, Show, G.Generic)
107+
108+data Bank = LeftB | RightB
109+ deriving (Bounded, Enum, Eq, Show, G.Generic)
110+
111+eats :: Being -> Being -> Bool
112+eats Fox Goose = True
113+eats Goose Beans = True
114+eats _ _ = False
115+
116+eatsR :: R.Relation Being Being
117+eatsR = R.toRel eats
118+
119+cross :: Bank -> Bank
120+cross LeftB = RightB
121+cross RightB = LeftB
122+
123+crossR :: R.Relation Bank Bank
124+crossR = R.fromF cross
125+
126+-- | Initial state, everyone in the left bank
127+locationLeft :: Being -> Bank
128+locationLeft _ = LeftB
129+
130+locationLeftR :: R.Relation Being Bank
131+locationLeftR = R.fromF locationLeft
132+
133+-- | Initial state, everyone in the right bank
134+locationRight :: Being -> Bank
135+locationRight _ = RightB
136+
137+locationRightR :: R.Relation Being Bank
138+locationRightR = R.fromF locationRight
139+
140+-- Properties
141+
142+-- Being at the same bank
143+sameBank :: R.Relation Being Bank -> R.Relation Being Being
144+sameBank = R.ker
145+
146+-- Risk of somebody eating somebody else
147+canEat :: R.Relation Being Bank -> R.Relation Being Being
148+canEat w = sameBank w `R.intersection` eatsR
149+
150+-- "Starvation" property.
151+inv :: R.Relation Being Bank -> Bool
152+inv w = (w `R.comp` canEat w) `R.sse` (w `R.comp` farmer)
153+ where
154+ farmer :: R.Relation Being Being
155+ farmer = R.fromF (const Farmer)
156+
157+-- Arbitrary state
158+bankState :: Being -> Bank -> Bool
159+bankState Farmer LeftB = True
160+bankState Fox LeftB = True
161+bankState Goose RightB = True
162+bankState Beans RightB = True
163+bankState _ _ = False
164+
165+bankStateR :: R.Relation Being Bank
166+bankStateR = R.toRel bankState
167+
168+-- Main
169+exec :: IO ()
170+exec = do
171+ putStrLn "Monty Hall Problem solution:"
172+ prettyPrint (secondChoice . firstChoice)
173+ putStrLn "\n Sum of dices probability:"
174+ prettyPrint (sumSSM . kr die die)
175+ putStrLn "\n Conditional dice throw:"
176+ prettyPrint conditionalThrows
177+ putStrLn "\n Checking that the last result is indeed a distribution: "
178+ prettyPrint (bang . sumSSM . kr die die)
179+ putStrLn "\n Probability of grass being wet:"
180+ prettyPrint (grass_wet (state grass sprinkler rain))
181+ putStrLn "\n Probability of rain:"
182+ prettyPrint (rainning . state grass sprinkler rain)
183+ putStrLn "\n Is the arbitrary state a valid state? (Alcuin Puzzle)"
184+ print (inv bankStateR)
test/Examples/Spreadsheets.hsnew file+47
@@ -0,0 +1,47 @@
1+{-# LANGUAGE DeriveGeneric #-}
2+
3+module Examples.Spreadsheets
4+
5+import LAoP.Utils
6+import LAoP.Matrix.Type
7+import GHC.Generics
8+import Prelude hiding (id, (.))
9+
10+data Student = Student1 | Student2 | Student3 | Student4
11+ deriving (Eq, Show, Enum, Bounded, Generic)
12+
13+data Question = Question1 | Question2 | Question3 | Question4
14+ deriving (Eq, Show, Enum, Bounded, Generic)
15+
16+data Results = Exam | Test | Final
17+ deriving (Eq, Show, Enum, Bounded, Generic)
18+
19+test :: Matrix Float One Results
20+test = point Test
21+
22+exam :: Matrix Float One Results
23+exam = point Exam
24+
25+final :: Matrix Float One Results
26+final = point Final
27+
28+m :: Matrix Float Question Student
29+m = fromLists [[95, 90, 100, 40], [20, 90, 90, 0], [30, 20, 95, 0], [50, 80, 100, 30]]
30+
31+w :: Matrix Float Question One
32+w = fromLists [[0.2, 0.3, 0.2, 0.3]]
33+
34+xls :: Matrix Float Question One
35+ -> Matrix Float Question Student
36+ -> Matrix Float Student One
37+ -> Matrix Float (Either Question Results) (Either One Student)
38+xls w m t = join (fork w m) (fork zeros r)
39+ where
40+ rExam = m . tr w
41+ rTest = tr t
42+ rFinal = rTest `maxPW` rExam
43+ r = (rExam . tr exam) + (rTest . tr test) + (rFinal . tr final)
44+
45+-- | Overloaded, point-wise 'max' function
46+maxPW :: Ord e => Matrix e a b -> Matrix e a b -> Matrix e a b
47+maxPW = zipWithM max
test/Spec.hs+7−1
@@ -1,2 +1,8 @@
1+module Main (main) where
2+
3+import qualified Examples.Readme as RD
4+
15main :: IO ()
2−main = putStrLn "Test suite not yet implemented"
6+main = do
7+ putStrLn ("Testing if README works" :: String)
8+ RD.exec