{-# LANGUAGE StrictData #-}
{-# LANGUAGE TypeFamilyDependencies #-}
{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE InstanceSigs #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE NoStarIsType #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE StandaloneDeriving #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}

-----------------------------------------------------------------------------
-- |
-- Module     : LAoP.Matrix.Internal
-- Copyright  : (c) Armando Santos 2019-2020
-- Maintainer : armandoifsantos@gmail.com
-- Stability  : experimental
--
-- The LAoP discipline generalises relations and functions treating them as
-- Boolean matrices and in turn consider these as arrows.
--
-- __LAoP__ is a library for algebraic (inductive) construction and manipulation of matrices
-- in Haskell. See <https://github.com/bolt12/master-thesis my Msc Thesis> for the
-- motivation behind the library, the underlying theory, and implementation details.
--
-- This module offers many of the combinators mentioned in the work of
-- Macedo (2012) and Oliveira (2012).
--
-- This is an Internal module and it is no supposed to be imported.
--
-----------------------------------------------------------------------------

module LAoP.Matrix.Internal
  ( -- | This definition makes use of the fact that 'Void' is
    -- isomorphic to 0 and '()' to 1 and captures matrix
    -- dimensions as stacks of 'Either's.
    --
    -- There exists two type families that make it easier to write
    -- matrix dimensions: 'FromNat' and 'Count'. This approach
    -- leads to a very straightforward implementation
    -- of LAoP combinators.

    -- * Type safe matrix representation
    Matrix (..),

    -- * Constraint type aliases
    Countable,
    CountableDims,
    CountableN,
    CountableDimsN,
    FL,
    FLN,
    Liftable,
    Trivial,

    -- * Primitives
    one,
    join,
    fork,

    -- * Auxiliary type families
    FromNat,
    Count,
    Normalize,

    -- * Matrix construction and conversion
    FromLists,
    fromLists,
    toLists,
    toList,
    matrixBuilder,
    matrixBuilder',
    row,
    col,
    zeros,
    ones,
    bang,
    constant,

    -- * Misc
    -- ** Get dimensions
    columns,
    columns',
    rows,
    rows',

    -- ** Matrix Transposition
    tr,

    -- ** Scalar multiplication/division of matrices
    (.|),
    (./),

    -- ** Selective operator
    select,
    branch,

    -- ** McCarthy's Conditional
    cond,

    -- ** Matrix "abiding"
    abideJF,
    abideFJ,

    -- ** Zip matrices
    zipWithM,

    -- * Biproduct approach
    -- ** Fork
    (===),
    -- *** Projections
    p1,
    p2,
    -- ** Join
    (|||),
    -- *** Injections
    i1,
    i2,
    -- ** Bifunctors
    (-|-),
    (><),

    -- ** Applicative matrix combinators

    -- | Note that given the restrictions imposed it is not possible to
    -- implement the standard type classes present in standard Haskell.

    -- *** Matrix pairing projections
    fstM,
    sndM,

    -- *** Matrix pairing
    kr,

    -- * Matrix composition and lifting

    -- ** Arrow matrix combinators

    -- | Note that given the restrictions imposed it is not possible to
    -- implement the standard type classes present in standard Haskell.
    iden,
    comp,
    fromF',
    fromF,

    -- * Matrix printing
    pretty,
    prettyPrint,

    -- * Other
    toBool,
    fromBool,
    compRel,
    divR,
    divL,
    divS,
    fromFRel,
    fromFRel',
    toRel,
    negateM,
    orM,
    andM,
    subM
  )
    where

import LAoP.Utils.Internal
import Data.Bool
import Data.Kind
import Data.List
import Data.Maybe
import Data.Proxy
import Data.Typeable
import Data.Void
import GHC.TypeLits
import Data.Type.Equality
import GHC.Generics
import Control.DeepSeq
import Prelude hiding (id, (.))
import qualified Prelude (id, (.))

-- | LAoP (Linear Algebra of Programming) Inductive Matrix definition.
data Matrix e cols rows where
  One :: e -> Matrix e () ()
  Join :: Matrix e a rows -> Matrix e b rows -> Matrix e (Either a b) rows
  Fork :: Matrix e cols a -> Matrix e cols b -> Matrix e cols (Either a b)

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

-- | Type family that computes the cardinality of a given type dimension.
--
--   It can also count the cardinality of custom types that implement the
-- 'Generic' instance.
type family Count (d :: Type) :: Nat where
  Count (Natural n m) = (m - n) + 1
  Count (List a)      = (^) 2 (Count a)
  Count (Either a b)  = (+) (Count a) (Count b)
  Count (a, b)        = (*) (Count a) (Count b)
  Count (a -> b)      = (^) (Count b) (Count a)
  -- Generics
  Count (M1 _ _ f p)  = Count (f p)
  Count (K1 _ _ _)    = 1
  Count (V1 _)        = 0
  Count (U1 _)        = 1
  Count ((:*:) a b p) = Count (a p) * Count (b p)
  Count ((:+:) a b p) = Count (a p) + Count (b p)
  Count d             = Count (Rep d R)

-- | Type family that computes of a given type dimension from a given natural
--
--   Thanks to Li-Yao Xia this type family is super fast.
type family FromNat (n :: Nat) :: Type where
  FromNat 1 = ()
  FromNat n = FromNat' (Mod n 2 == 0) (FromNat (Div n 2))

type family FromNat' (b :: Bool) (m :: Type) :: Type where
  FromNat' 'True m  = Either m m
  FromNat' 'False m = Either () (Either m m)

-- | Type family that normalizes the representation of a given data
-- structure
type family Normalize (d :: Type) :: Type where
  Normalize (Either a b) = Either (Normalize a) (Normalize b)
  Normalize d            = FromNat (Count d)

-- | Constraint type synonyms to keep the type signatures less convoluted
type Countable a = KnownNat (Count a)
type CountableN a = KnownNat (Count (Normalize a))
type CountableDims a b = (Countable a, Countable b)
type CountableDimsN a b = (CountableN a, CountableN b)
type FL a b = FromLists a b
type FLN a b = FromLists (Normalize a) (Normalize b)
type Liftable e a b = (Bounded a, Bounded b, Enum a, Enum b, Eq b, Num e, Ord e)
type Trivial a = FromNat (Count a) ~ a

-- | It is possible to implement a constrained version of the category type
-- class.
instance (Num e) => Category (Matrix e) where
  type Object (Matrix e) a = (FL a a, Countable a)
  id :: Matrix e a a
id = Matrix e a a
forall e cols.
(Num e, FL cols cols, Countable cols) =>
Matrix e cols cols
iden
  . :: Matrix e b c -> Matrix e a b -> Matrix e a c
(.) = Matrix e b c -> Matrix e a b -> Matrix e a c
forall e cr rows cols.
Num e =>
Matrix e cr rows -> Matrix e cols cr -> Matrix e cols rows
comp

instance NFData e => NFData (Matrix e cols rows) where
    rnf :: Matrix e cols rows -> ()
rnf (One e
e)    = e -> ()
forall a. NFData a => a -> ()
rnf e
e
    rnf (Join Matrix e a rows
a Matrix e b rows
b) = Matrix e a rows -> ()
forall a. NFData a => a -> ()
rnf Matrix e a rows
a () -> () -> ()
`seq` Matrix e b rows -> ()
forall a. NFData a => a -> ()
rnf Matrix e b rows
b
    rnf (Fork Matrix e cols a
a Matrix e cols b
b) = Matrix e cols a -> ()
forall a. NFData a => a -> ()
rnf Matrix e cols a
a () -> () -> ()
`seq` Matrix e cols b -> ()
forall a. NFData a => a -> ()
rnf Matrix e cols b
b

instance Eq e => Eq (Matrix e cols rows) where
  (One e
a) == :: Matrix e cols rows -> Matrix e cols rows -> Bool
== (One e
b)           = e
a e -> e -> Bool
forall a. Eq a => a -> a -> Bool
== e
b
  (Join Matrix e a rows
a Matrix e b rows
b) == (Join Matrix e a rows
c Matrix e b rows
d)     = Matrix e a rows
a Matrix e a rows -> Matrix e a rows -> Bool
forall a. Eq a => a -> a -> Bool
== Matrix e a rows
Matrix e a rows
c Bool -> Bool -> Bool
&& Matrix e b rows
b Matrix e b rows -> Matrix e b rows -> Bool
forall a. Eq a => a -> a -> Bool
== Matrix e b rows
Matrix e b rows
d
  (Fork Matrix e cols a
a Matrix e cols b
b) == (Fork Matrix e cols a
c Matrix e cols b
d)     = Matrix e cols a
a Matrix e cols a -> Matrix e cols a -> Bool
forall a. Eq a => a -> a -> Bool
== Matrix e cols a
Matrix e cols a
c Bool -> Bool -> Bool
&& Matrix e cols b
b Matrix e cols b -> Matrix e cols b -> Bool
forall a. Eq a => a -> a -> Bool
== Matrix e cols b
Matrix e cols b
d
  x :: Matrix e cols rows
x@(Fork Matrix e cols a
_ Matrix e cols b
_) == y :: Matrix e cols rows
y@(Join Matrix e a rows
_ Matrix e b rows
_) = Matrix e cols rows
x Matrix e cols rows -> Matrix e cols rows -> Bool
forall a. Eq a => a -> a -> Bool
== Matrix e cols rows -> Matrix e cols rows
forall e cols rows. Matrix e cols rows -> Matrix e cols rows
abideJF Matrix e cols rows
y
  x :: Matrix e cols rows
x@(Join Matrix e a rows
_ Matrix e b rows
_) == y :: Matrix e cols rows
y@(Fork Matrix e cols a
_ Matrix e cols b
_) = Matrix e cols rows -> Matrix e cols rows
forall e cols rows. Matrix e cols rows -> Matrix e cols rows
abideJF Matrix e cols rows
x Matrix e cols rows -> Matrix e cols rows -> Bool
forall a. Eq a => a -> a -> Bool
== Matrix e cols rows
y

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

  Matrix e cols rows
a + :: Matrix e cols rows -> Matrix e cols rows -> Matrix e cols rows
+ Matrix e cols rows
b = (e -> e -> e)
-> Matrix e cols rows -> Matrix e cols rows -> Matrix e cols rows
forall e f g cols rows.
(e -> f -> g)
-> Matrix e cols rows -> Matrix f cols rows -> Matrix g cols rows
zipWithM e -> e -> e
forall a. Num a => a -> a -> a
(+) Matrix e cols rows
a Matrix e cols rows
b

  Matrix e cols rows
a - :: Matrix e cols rows -> Matrix e cols rows -> Matrix e cols rows
- Matrix e cols rows
b = (e -> e -> e)
-> Matrix e cols rows -> Matrix e cols rows -> Matrix e cols rows
forall e f g cols rows.
(e -> f -> g)
-> Matrix e cols rows -> Matrix f cols rows -> Matrix g cols rows
zipWithM (-) Matrix e cols rows
a Matrix e cols rows
b

  Matrix e cols rows
a * :: Matrix e cols rows -> Matrix e cols rows -> Matrix e cols rows
* Matrix e cols rows
b = (e -> e -> e)
-> Matrix e cols rows -> Matrix e cols rows -> Matrix e cols rows
forall e f g cols rows.
(e -> f -> g)
-> Matrix e cols rows -> Matrix f cols rows -> Matrix g cols rows
zipWithM e -> e -> e
forall a. Num a => a -> a -> a
(*) Matrix e cols rows
a Matrix e cols rows
b

  abs :: Matrix e cols rows -> Matrix e cols rows
abs (One e
a)    = e -> Matrix e () ()
forall e. e -> Matrix e () ()
One (e -> e
forall a. Num a => a -> a
abs e
a)
  abs (Join Matrix e a rows
a Matrix e b rows
b) = Matrix e a rows -> Matrix e b rows -> Matrix e (Either a b) rows
forall e a rows b.
Matrix e a rows -> Matrix e b rows -> Matrix e (Either a b) rows
Join (Matrix e a rows -> Matrix e a rows
forall a. Num a => a -> a
abs Matrix e a rows
a) (Matrix e b rows -> Matrix e b rows
forall a. Num a => a -> a
abs Matrix e b rows
b)
  abs (Fork Matrix e cols a
a Matrix e cols b
b) = Matrix e cols a -> Matrix e cols b -> Matrix e cols (Either a b)
forall e cols a b.
Matrix e cols a -> Matrix e cols b -> Matrix e cols (Either a b)
Fork (Matrix e cols a -> Matrix e cols a
forall a. Num a => a -> a
abs Matrix e cols a
a) (Matrix e cols b -> Matrix e cols b
forall a. Num a => a -> a
abs Matrix e cols b
b)

  signum :: Matrix e cols rows -> Matrix e cols rows
signum (One e
a)    = e -> Matrix e () ()
forall e. e -> Matrix e () ()
One (e -> e
forall a. Num a => a -> a
signum e
a)
  signum (Join Matrix e a rows
a Matrix e b rows
b) = Matrix e a rows -> Matrix e b rows -> Matrix e (Either a b) rows
forall e a rows b.
Matrix e a rows -> Matrix e b rows -> Matrix e (Either a b) rows
Join (Matrix e a rows -> Matrix e a rows
forall a. Num a => a -> a
signum Matrix e a rows
a) (Matrix e b rows -> Matrix e b rows
forall a. Num a => a -> a
signum Matrix e b rows
b)
  signum (Fork Matrix e cols a
a Matrix e cols b
b) = Matrix e cols a -> Matrix e cols b -> Matrix e cols (Either a b)
forall e cols a b.
Matrix e cols a -> Matrix e cols b -> Matrix e cols (Either a b)
Fork (Matrix e cols a -> Matrix e cols a
forall a. Num a => a -> a
signum Matrix e cols a
a) (Matrix e cols b -> Matrix e cols b
forall a. Num a => a -> a
signum Matrix e cols b
b)

instance Ord e => Ord (Matrix e cols rows) where
    (One e
a) <= :: Matrix e cols rows -> Matrix e cols rows -> Bool
<= (One e
b)           = e
a e -> e -> Bool
forall a. Ord a => a -> a -> Bool
<= e
b
    (Join Matrix e a rows
a Matrix e b rows
b) <= (Join Matrix e a rows
c Matrix e b rows
d)     = (Matrix e a rows
a Matrix e a rows -> Matrix e a rows -> Bool
forall a. Ord a => a -> a -> Bool
<= Matrix e a rows
Matrix e a rows
c) Bool -> Bool -> Bool
&& (Matrix e b rows
b Matrix e b rows -> Matrix e b rows -> Bool
forall a. Ord a => a -> a -> Bool
<= Matrix e b rows
Matrix e b rows
d)
    (Fork Matrix e cols a
a Matrix e cols b
b) <= (Fork Matrix e cols a
c Matrix e cols b
d)     = (Matrix e cols a
a Matrix e cols a -> Matrix e cols a -> Bool
forall a. Ord a => a -> a -> Bool
<= Matrix e cols a
Matrix e cols a
c) Bool -> Bool -> Bool
&& (Matrix e cols b
b Matrix e cols b -> Matrix e cols b -> Bool
forall a. Ord a => a -> a -> Bool
<= Matrix e cols b
Matrix e cols b
d)
    x :: Matrix e cols rows
x@(Fork Matrix e cols a
_ Matrix e cols b
_) <= y :: Matrix e cols rows
y@(Join Matrix e a rows
_ Matrix e b rows
_) = Matrix e cols rows
x Matrix e cols rows -> Matrix e cols rows -> Bool
forall a. Ord a => a -> a -> Bool
<= Matrix e cols rows -> Matrix e cols rows
forall e cols rows. Matrix e cols rows -> Matrix e cols rows
abideJF Matrix e cols rows
y
    x :: Matrix e cols rows
x@(Join Matrix e a rows
_ Matrix e b rows
_) <= y :: Matrix e cols rows
y@(Fork Matrix e cols a
_ Matrix e cols b
_) = Matrix e cols rows -> Matrix e cols rows
forall e cols rows. Matrix e cols rows -> Matrix e cols rows
abideJF Matrix e cols rows
x Matrix e cols rows -> Matrix e cols rows -> Bool
forall a. Ord a => a -> a -> Bool
<= Matrix e cols rows
y

-- Primitives

-- | Unit matrix constructor
one :: e -> Matrix e () ()
one :: e -> Matrix e () ()
one = e -> Matrix e () ()
forall e. e -> Matrix e () ()
One

-- | Matrix 'Join' constructor
join :: Matrix e a rows -> Matrix e b rows -> Matrix e (Either a b) rows
join :: Matrix e a rows -> Matrix e b rows -> Matrix e (Either a b) rows
join = Matrix e a rows -> Matrix e b rows -> Matrix e (Either a b) rows
forall e a rows b.
Matrix e a rows -> Matrix e b rows -> Matrix e (Either a b) rows
Join

infixl 3 |||

-- | Matrix 'Join' constructor
(|||) :: Matrix e a rows -> Matrix e b rows -> Matrix e (Either a b) rows
||| :: Matrix e a rows -> Matrix e b rows -> Matrix e (Either a b) rows
(|||) = Matrix e a rows -> Matrix e b rows -> Matrix e (Either a b) rows
forall e a rows b.
Matrix e a rows -> Matrix e b rows -> Matrix e (Either a b) rows
Join

-- | Matrix 'Fork' constructor
fork :: Matrix e cols a -> Matrix e cols b -> Matrix e cols (Either a b)
fork :: Matrix e cols a -> Matrix e cols b -> Matrix e cols (Either a b)
fork = Matrix e cols a -> Matrix e cols b -> Matrix e cols (Either a b)
forall e cols a b.
Matrix e cols a -> Matrix e cols b -> Matrix e cols (Either a b)
Fork

infixl 2 ===

-- | Matrix 'Fork' constructor
(===) :: Matrix e cols a -> Matrix e cols b -> Matrix e cols (Either a b)
=== :: Matrix e cols a -> Matrix e cols b -> Matrix e cols (Either a b)
(===) = Matrix e cols a -> Matrix e cols b -> Matrix e cols (Either a b)
forall e cols a b.
Matrix e cols a -> Matrix e cols b -> Matrix e cols (Either a b)
Fork

-- Construction

-- | Type class for defining the 'fromList' conversion function.
--
--   Given that it is not possible to branch on types at the term level type
-- classes are needed very much like an inductive definition but on types.
class FromLists cols rows where
  -- | Build a matrix out of a list of list of elements. Throws a runtime
  -- error if the dimensions do not match.
  fromLists :: [[e]] -> Matrix e cols rows

instance FromLists () () where
  fromLists :: [[e]] -> Matrix e () ()
fromLists [[e
e]] = e -> Matrix e () ()
forall e. e -> Matrix e () ()
One e
e
  fromLists [[e]]
_     = String -> Matrix e () ()
forall a. HasCallStack => String -> a
error String
"Wrong dimensions"

instance (FromLists cols ()) => FromLists (Either () cols) () where
  fromLists :: [[e]] -> Matrix e (Either () cols) ()
fromLists [e
h : [e]
t] = Matrix e () () -> Matrix e cols () -> Matrix e (Either () cols) ()
forall e a rows b.
Matrix e a rows -> Matrix e b rows -> Matrix e (Either a b) rows
Join (e -> Matrix e () ()
forall e. e -> Matrix e () ()
One e
h) ([[e]] -> Matrix e cols ()
forall cols rows e.
FromLists cols rows =>
[[e]] -> Matrix e cols rows
fromLists [[e]
t])
  fromLists [[e]]
_       = String -> Matrix e (Either () cols) ()
forall a. HasCallStack => String -> a
error String
"Wrong dimensions"

instance {-# OVERLAPPABLE #-} (FromLists a (), FromLists b (), Countable a) => FromLists (Either a b) () where
  fromLists :: [[e]] -> Matrix e (Either a b) ()
fromLists [[e]
l] =
      let rowsA :: Int
rowsA = Integer -> Int
forall a. Num a => Integer -> a
fromInteger (Proxy (Count a) -> Integer
forall (n :: Nat) (proxy :: Nat -> Type).
KnownNat n =>
proxy n -> Integer
natVal (Proxy (Count a)
forall k (t :: k). Proxy t
Proxy :: Proxy (Count a)))
       in Matrix e a () -> Matrix e b () -> Matrix e (Either a b) ()
forall e a rows b.
Matrix e a rows -> Matrix e b rows -> Matrix e (Either a b) rows
Join ([[e]] -> Matrix e a ()
forall cols rows e.
FromLists cols rows =>
[[e]] -> Matrix e cols rows
fromLists [Int -> [e] -> [e]
forall a. Int -> [a] -> [a]
take Int
rowsA [e]
l]) ([[e]] -> Matrix e b ()
forall cols rows e.
FromLists cols rows =>
[[e]] -> Matrix e cols rows
fromLists [Int -> [e] -> [e]
forall a. Int -> [a] -> [a]
drop Int
rowsA [e]
l])
  fromLists [[e]]
_       = String -> Matrix e (Either a b) ()
forall a. HasCallStack => String -> a
error String
"Wrong dimensions"

instance (FromLists () rows) => FromLists () (Either () rows) where
  fromLists :: [[e]] -> Matrix e () (Either () rows)
fromLists ([e
h] : [[e]]
t) = Matrix e () () -> Matrix e () rows -> Matrix e () (Either () rows)
forall e cols a b.
Matrix e cols a -> Matrix e cols b -> Matrix e cols (Either a b)
Fork (e -> Matrix e () ()
forall e. e -> Matrix e () ()
One e
h) ([[e]] -> Matrix e () rows
forall cols rows e.
FromLists cols rows =>
[[e]] -> Matrix e cols rows
fromLists [[e]]
t)
  fromLists [[e]]
_         = String -> Matrix e () (Either () rows)
forall a. HasCallStack => String -> a
error String
"Wrong dimensions"

instance {-# OVERLAPPABLE #-} (FromLists () a, FromLists () b, Countable a) => FromLists () (Either a b) where
  fromLists :: [[e]] -> Matrix e () (Either a b)
fromLists l :: [[e]]
l@([e
_] : [[e]]
_) =
      let rowsA :: Int
rowsA = Integer -> Int
forall a. Num a => Integer -> a
fromInteger (Proxy (Count a) -> Integer
forall (n :: Nat) (proxy :: Nat -> Type).
KnownNat n =>
proxy n -> Integer
natVal (Proxy (Count a)
forall k (t :: k). Proxy t
Proxy :: Proxy (Count a)))
       in Matrix e () a -> Matrix e () b -> Matrix e () (Either a b)
forall e cols a b.
Matrix e cols a -> Matrix e cols b -> Matrix e cols (Either a b)
Fork ([[e]] -> Matrix e () a
forall cols rows e.
FromLists cols rows =>
[[e]] -> Matrix e cols rows
fromLists (Int -> [[e]] -> [[e]]
forall a. Int -> [a] -> [a]
take Int
rowsA [[e]]
l)) ([[e]] -> Matrix e () b
forall cols rows e.
FromLists cols rows =>
[[e]] -> Matrix e cols rows
fromLists (Int -> [[e]] -> [[e]]
forall a. Int -> [a] -> [a]
drop Int
rowsA [[e]]
l))
  fromLists [[e]]
_         = String -> Matrix e () (Either a b)
forall a. HasCallStack => String -> a
error String
"Wrong dimensions"

instance (FromLists (Either a b) c, FromLists (Either a b) d, Countable c) => FromLists (Either a b) (Either c d) where
  fromLists :: [[e]] -> Matrix e (Either a b) (Either c d)
fromLists l :: [[e]]
l@([e]
h : [[e]]
t) =
    let lh :: Int
lh        = [e] -> Int
forall (t :: Type -> Type) a. Foldable t => t a -> Int
length [e]
h
        rowsC :: Int
rowsC     = Integer -> Int
forall a. Num a => Integer -> a
fromInteger (Proxy (Count c) -> Integer
forall (n :: Nat) (proxy :: Nat -> Type).
KnownNat n =>
proxy n -> Integer
natVal (Proxy (Count c)
forall k (t :: k). Proxy t
Proxy :: Proxy (Count c)))
        condition :: Bool
condition = ([e] -> Bool) -> [[e]] -> Bool
forall (t :: Type -> Type) a.
Foldable t =>
(a -> Bool) -> t a -> Bool
all ((Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
lh) (Int -> Bool) -> ([e] -> Int) -> [e] -> Bool
forall (k :: Type -> Type -> Type) b c a.
Category k =>
k b c -> k a b -> k a c
. [e] -> Int
forall (t :: Type -> Type) a. Foldable t => t a -> Int
length) [[e]]
t
     in if Int
lh Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
0 Bool -> Bool -> Bool
&& Bool
condition
          then Matrix e (Either a b) c
-> Matrix e (Either a b) d -> Matrix e (Either a b) (Either c d)
forall e cols a b.
Matrix e cols a -> Matrix e cols b -> Matrix e cols (Either a b)
Fork ([[e]] -> Matrix e (Either a b) c
forall cols rows e.
FromLists cols rows =>
[[e]] -> Matrix e cols rows
fromLists (Int -> [[e]] -> [[e]]
forall a. Int -> [a] -> [a]
take Int
rowsC [[e]]
l)) ([[e]] -> Matrix e (Either a b) d
forall cols rows e.
FromLists cols rows =>
[[e]] -> Matrix e cols rows
fromLists (Int -> [[e]] -> [[e]]
forall a. Int -> [a] -> [a]
drop Int
rowsC [[e]]
l))
          else String -> Matrix e (Either a b) (Either c d)
forall a. HasCallStack => String -> a
error String
"Not all rows have the same length"

-- | Matrix builder function. Constructs a matrix provided with
-- a construction function that operates with indices.
matrixBuilder' ::
  forall e cols rows.
  ( FL cols rows,
    CountableDims cols rows
  ) => ((Int, Int) -> e) -> Matrix e cols rows
matrixBuilder' :: ((Int, Int) -> e) -> Matrix e cols rows
matrixBuilder' (Int, Int) -> e
f =
  let c :: Int
c         = Integer -> Int
forall a. Num a => Integer -> a
fromInteger (Integer -> Int) -> Integer -> Int
forall a b. (a -> b) -> a -> b
$ Proxy (Count cols) -> Integer
forall (n :: Nat) (proxy :: Nat -> Type).
KnownNat n =>
proxy n -> Integer
natVal (Proxy (Count cols)
forall k (t :: k). Proxy t
Proxy :: Proxy (Count cols))
      r :: Int
r         = Integer -> Int
forall a. Num a => Integer -> a
fromInteger (Integer -> Int) -> Integer -> Int
forall a b. (a -> b) -> a -> b
$ Proxy (Count rows) -> Integer
forall (n :: Nat) (proxy :: Nat -> Type).
KnownNat n =>
proxy n -> Integer
natVal (Proxy (Count rows)
forall k (t :: k). Proxy t
Proxy :: Proxy (Count rows))
      positions :: [(Int, Int)]
positions = [(Int
a, Int
b) | Int
a <- [Int
0 .. (Int
r Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1)], Int
b <- [Int
0 .. (Int
c Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1)]]
   in [[e]] -> Matrix e cols rows
forall cols rows e.
FromLists cols rows =>
[[e]] -> Matrix e cols rows
fromLists ([[e]] -> Matrix e cols rows)
-> ([[(Int, Int)]] -> [[e]])
-> [[(Int, Int)]]
-> Matrix e cols rows
forall (k :: Type -> Type -> Type) b c a.
Category k =>
k b c -> k a b -> k a c
. ([(Int, Int)] -> [e]) -> [[(Int, Int)]] -> [[e]]
forall a b. (a -> b) -> [a] -> [b]
map (((Int, Int) -> e) -> [(Int, Int)] -> [e]
forall a b. (a -> b) -> [a] -> [b]
map (Int, Int) -> e
f) ([[(Int, Int)]] -> Matrix e cols rows)
-> ([(Int, Int)] -> [[(Int, Int)]])
-> [(Int, Int)]
-> Matrix e cols rows
forall (k :: Type -> Type -> Type) b c a.
Category k =>
k b c -> k a b -> k a c
. ((Int, Int) -> (Int, Int) -> Bool)
-> [(Int, Int)] -> [[(Int, Int)]]
forall a. (a -> a -> Bool) -> [a] -> [[a]]
groupBy (\(Int
x, Int
_) (Int
w, Int
_) -> Int
x Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
w) ([(Int, Int)] -> Matrix e cols rows)
-> [(Int, Int)] -> Matrix e cols rows
forall a b. (a -> b) -> a -> b
$ [(Int, Int)]
positions

-- | Matrix builder function. Constructs a matrix provided with
-- a construction function that operates with arbitrary types.
matrixBuilder ::
  forall e a b.
  ( FLN a b,
    CountableN b,
    Enum a,
    Enum b,
    Bounded a,
    Bounded b,
    Eq a,
    CountableDimsN a b
  ) => ((a, b) -> e) -> Matrix e (Normalize a) (Normalize b)
matrixBuilder :: ((a, b) -> e) -> Matrix e (Normalize a) (Normalize b)
matrixBuilder (a, b) -> e
f =
  let r :: Int
r         = Integer -> Int
forall a. Num a => Integer -> a
fromInteger (Integer -> Int) -> Integer -> Int
forall a b. (a -> b) -> a -> b
$ Proxy (Count (Normalize b)) -> Integer
forall (n :: Nat) (proxy :: Nat -> Type).
KnownNat n =>
proxy n -> Integer
natVal (Proxy (Count (Normalize b))
forall k (t :: k). Proxy t
Proxy :: Proxy (Count (Normalize b)))
      positions :: [(a, b)]
positions = [(a
a, b
b) | a
a <- [a
forall a. Bounded a => a
minBound .. a
forall a. Bounded a => a
maxBound], b
b <- [b
forall a. Bounded a => a
minBound .. b
forall a. Bounded a => a
maxBound]]
   in [[e]] -> Matrix e (Normalize a) (Normalize b)
forall cols rows e.
FromLists cols rows =>
[[e]] -> Matrix e cols rows
fromLists ([[e]] -> Matrix e (Normalize a) (Normalize b))
-> ([[(a, b)]] -> [[e]])
-> [[(a, b)]]
-> Matrix e (Normalize a) (Normalize b)
forall (k :: Type -> Type -> Type) b c a.
Category k =>
k b c -> k a b -> k a c
. ([(a, b)] -> [e]) -> [[(a, b)]] -> [[e]]
forall a b. (a -> b) -> [a] -> [b]
map (((a, b) -> e) -> [(a, b)] -> [e]
forall a b. (a -> b) -> [a] -> [b]
map (a, b) -> e
f) ([[(a, b)]] -> Matrix e (Normalize a) (Normalize b))
-> ([[(a, b)]] -> [[(a, b)]])
-> [[(a, b)]]
-> Matrix e (Normalize a) (Normalize b)
forall (k :: Type -> Type -> Type) b c a.
Category k =>
k b c -> k a b -> k a c
. [[(a, b)]] -> [[(a, b)]]
forall a. [[a]] -> [[a]]
transpose ([[(a, b)]] -> Matrix e (Normalize a) (Normalize b))
-> ([(a, b)] -> [[(a, b)]])
-> [(a, b)]
-> Matrix e (Normalize a) (Normalize b)
forall (k :: Type -> Type -> Type) b c a.
Category k =>
k b c -> k a b -> k a c
. Int -> [(a, b)] -> [[(a, b)]]
forall a. Int -> [a] -> [[a]]
buildList Int
r ([(a, b)] -> Matrix e (Normalize a) (Normalize b))
-> [(a, b)] -> Matrix e (Normalize a) (Normalize b)
forall a b. (a -> b) -> a -> b
$ [(a, b)]
positions
  where
    buildList :: Int -> [a] -> [[a]]
buildList Int
_ [] = []
    buildList Int
r [a]
l  = Int -> [a] -> [a]
forall a. Int -> [a] -> [a]
take Int
r [a]
l [a] -> [[a]] -> [[a]]
forall a. a -> [a] -> [a]
: Int -> [a] -> [[a]]
buildList Int
r (Int -> [a] -> [a]
forall a. Int -> [a] -> [a]
drop Int
r [a]
l)

-- | Constructs a column vector matrix
col :: (FL () rows) => [e] -> Matrix e () rows
col :: [e] -> Matrix e () rows
col = [[e]] -> Matrix e () rows
forall cols rows e.
FromLists cols rows =>
[[e]] -> Matrix e cols rows
fromLists ([[e]] -> Matrix e () rows)
-> ([e] -> [[e]]) -> [e] -> Matrix e () rows
forall (k :: Type -> Type -> Type) b c a.
Category k =>
k b c -> k a b -> k a c
. (e -> [e]) -> [e] -> [[e]]
forall a b. (a -> b) -> [a] -> [b]
map (e -> [e] -> [e]
forall a. a -> [a] -> [a]
: [])

-- | Constructs a row vector matrix
row :: (FL cols ()) => [e] -> Matrix e cols ()
row :: [e] -> Matrix e cols ()
row = [[e]] -> Matrix e cols ()
forall cols rows e.
FromLists cols rows =>
[[e]] -> Matrix e cols rows
fromLists ([[e]] -> Matrix e cols ())
-> ([e] -> [[e]]) -> [e] -> Matrix e cols ()
forall (k :: Type -> Type -> Type) b c a.
Category k =>
k b c -> k a b -> k a c
. ([e] -> [[e]] -> [[e]]
forall a. a -> [a] -> [a]
: [])

-- | Lifts functions to matrices with arbitrary dimensions.
--
--   NOTE: Be careful to not ask for a matrix bigger than the cardinality of
-- types @a@ or @b@ allows.
fromF' ::
  forall a b cols rows e.
  ( Liftable e a b,
    CountableDims cols rows,
    FL rows cols
  ) =>
  (a -> b) ->
  Matrix e cols rows
fromF' :: (a -> b) -> Matrix e cols rows
fromF' a -> b
f =
  let minA :: a
minA         = Bounded a => a
forall a. Bounded a => a
minBound @a
      maxA :: a
maxA         = Bounded a => a
forall a. Bounded a => a
maxBound @a
      minB :: b
minB         = Bounded b => b
forall a. Bounded a => a
minBound @b
      maxB :: b
maxB         = Bounded b => b
forall a. Bounded a => a
maxBound @b
      ccols :: Int
ccols        = Integer -> Int
forall a. Num a => Integer -> a
fromInteger (Integer -> Int) -> Integer -> Int
forall a b. (a -> b) -> a -> b
$ Proxy (Count cols) -> Integer
forall (n :: Nat) (proxy :: Nat -> Type).
KnownNat n =>
proxy n -> Integer
natVal (Proxy (Count cols)
forall k (t :: k). Proxy t
Proxy :: Proxy (Count cols))
      rrows :: Int
rrows        = Integer -> Int
forall a. Num a => Integer -> a
fromInteger (Integer -> Int) -> Integer -> Int
forall a b. (a -> b) -> a -> b
$ Proxy (Count rows) -> Integer
forall (n :: Nat) (proxy :: Nat -> Type).
KnownNat n =>
proxy n -> Integer
natVal (Proxy (Count rows)
forall k (t :: k). Proxy t
Proxy :: Proxy (Count rows))
      elementsA :: [a]
elementsA    = Int -> [a] -> [a]
forall a. Int -> [a] -> [a]
take Int
ccols [a
minA .. a
maxA]
      elementsB :: [b]
elementsB    = Int -> [b] -> [b]
forall a. Int -> [a] -> [a]
take Int
rrows [b
minB .. b
maxB]
      combinations :: [(a, b)]
combinations = (,) (a -> b -> (a, b)) -> [a] -> [b -> (a, b)]
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> [a]
elementsA [b -> (a, b)] -> [b] -> [(a, b)]
forall (f :: Type -> Type) a b.
Applicative f =>
f (a -> b) -> f a -> f b
<*> [b]
elementsB
      combAp :: [e]
combAp       = (((Int, Int), e) -> e) -> [((Int, Int), e)] -> [e]
forall a b. (a -> b) -> [a] -> [b]
map ((Int, Int), e) -> e
forall a b. (a, b) -> b
snd ([((Int, Int), e)] -> [e])
-> ([((Int, Int), e)] -> [((Int, Int), e)])
-> [((Int, Int), e)]
-> [e]
forall (k :: Type -> Type -> Type) b c a.
Category k =>
k b c -> k a b -> k a c
. [((Int, Int), e)] -> [((Int, Int), e)]
forall a. Ord a => [a] -> [a]
sort ([((Int, Int), e)] -> [e])
-> ([(a, b)] -> [((Int, Int), e)]) -> [(a, b)] -> [e]
forall (k :: Type -> Type -> Type) b c a.
Category k =>
k b c -> k a b -> k a c
. ((a, b) -> ((Int, Int), e)) -> [(a, b)] -> [((Int, Int), e)]
forall a b. (a -> b) -> [a] -> [b]
map (\(a
a, b
b) -> if a -> b
f a
a b -> b -> Bool
forall a. Eq a => a -> a -> Bool
== b
b
                                                         then ((a -> Int
forall a. Enum a => a -> Int
fromEnum a
a, b -> Int
forall a. Enum a => a -> Int
fromEnum b
b), e
1)
                                                         else ((a -> Int
forall a. Enum a => a -> Int
fromEnum a
a, b -> Int
forall a. Enum a => a -> Int
fromEnum b
b), e
0)) ([(a, b)] -> [e]) -> [(a, b)] -> [e]
forall a b. (a -> b) -> a -> b
$ [(a, b)]
combinations
      mList :: [[e]]
mList        = [e] -> Int -> [[e]]
forall a. [a] -> Int -> [[a]]
buildList [e]
combAp Int
rrows
   in Matrix e rows cols -> Matrix e cols rows
forall e cols rows. Matrix e cols rows -> Matrix e rows cols
tr (Matrix e rows cols -> Matrix e cols rows)
-> Matrix e rows cols -> Matrix e cols rows
forall a b. (a -> b) -> a -> b
$ [[e]] -> Matrix e rows cols
forall cols rows e.
FromLists cols rows =>
[[e]] -> Matrix e cols rows
fromLists [[e]]
mList
  where
    buildList :: [a] -> Int -> [[a]]
buildList [] Int
_ = []
    buildList [a]
l Int
r  = Int -> [a] -> [a]
forall a. Int -> [a] -> [a]
take Int
r [a]
l [a] -> [[a]] -> [[a]]
forall a. a -> [a] -> [a]
: [a] -> Int -> [[a]]
buildList (Int -> [a] -> [a]
forall a. Int -> [a] -> [a]
drop Int
r [a]
l) Int
r

-- | Lifts functions to matrices with dimensions matching @a@ and @b@
-- cardinality's.
fromF ::
  forall a b e.
  ( Liftable e a b,
    CountableDimsN a b,
    FLN b a
  ) =>
  (a -> b) ->
  Matrix e (Normalize a) (Normalize b)
fromF :: (a -> b) -> Matrix e (Normalize a) (Normalize b)
fromF a -> b
f =
  let minA :: a
minA         = Bounded a => a
forall a. Bounded a => a
minBound @a
      maxA :: a
maxA         = Bounded a => a
forall a. Bounded a => a
maxBound @a
      minB :: b
minB         = Bounded b => b
forall a. Bounded a => a
minBound @b
      maxB :: b
maxB         = Bounded b => b
forall a. Bounded a => a
maxBound @b
      ccols :: Int
ccols        = Integer -> Int
forall a. Num a => Integer -> a
fromInteger (Integer -> Int) -> Integer -> Int
forall a b. (a -> b) -> a -> b
$ Proxy (Count (Normalize a)) -> Integer
forall (n :: Nat) (proxy :: Nat -> Type).
KnownNat n =>
proxy n -> Integer
natVal (Proxy (Count (Normalize a))
forall k (t :: k). Proxy t
Proxy :: Proxy (Count (Normalize a)))
      rrows :: Int
rrows        = Integer -> Int
forall a. Num a => Integer -> a
fromInteger (Integer -> Int) -> Integer -> Int
forall a b. (a -> b) -> a -> b
$ Proxy (Count (Normalize b)) -> Integer
forall (n :: Nat) (proxy :: Nat -> Type).
KnownNat n =>
proxy n -> Integer
natVal (Proxy (Count (Normalize b))
forall k (t :: k). Proxy t
Proxy :: Proxy (Count (Normalize b)))
      elementsA :: [a]
elementsA    = Int -> [a] -> [a]
forall a. Int -> [a] -> [a]
take Int
ccols [a
minA .. a
maxA]
      elementsB :: [b]
elementsB    = Int -> [b] -> [b]
forall a. Int -> [a] -> [a]
take Int
rrows [b
minB .. b
maxB]
      combinations :: [(a, b)]
combinations = (,) (a -> b -> (a, b)) -> [a] -> [b -> (a, b)]
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> [a]
elementsA [b -> (a, b)] -> [b] -> [(a, b)]
forall (f :: Type -> Type) a b.
Applicative f =>
f (a -> b) -> f a -> f b
<*> [b]
elementsB
      combAp :: [e]
combAp       = (((Int, Int), e) -> e) -> [((Int, Int), e)] -> [e]
forall a b. (a -> b) -> [a] -> [b]
map ((Int, Int), e) -> e
forall a b. (a, b) -> b
snd ([((Int, Int), e)] -> [e])
-> ([((Int, Int), e)] -> [((Int, Int), e)])
-> [((Int, Int), e)]
-> [e]
forall (k :: Type -> Type -> Type) b c a.
Category k =>
k b c -> k a b -> k a c
. [((Int, Int), e)] -> [((Int, Int), e)]
forall a. Ord a => [a] -> [a]
sort ([((Int, Int), e)] -> [e])
-> ([(a, b)] -> [((Int, Int), e)]) -> [(a, b)] -> [e]
forall (k :: Type -> Type -> Type) b c a.
Category k =>
k b c -> k a b -> k a c
. ((a, b) -> ((Int, Int), e)) -> [(a, b)] -> [((Int, Int), e)]
forall a b. (a -> b) -> [a] -> [b]
map (\(a
a, b
b) -> if a -> b
f a
a b -> b -> Bool
forall a. Eq a => a -> a -> Bool
== b
b
                                                         then ((a -> Int
forall a. Enum a => a -> Int
fromEnum a
a, b -> Int
forall a. Enum a => a -> Int
fromEnum b
b), e
1)
                                                         else ((a -> Int
forall a. Enum a => a -> Int
fromEnum a
a, b -> Int
forall a. Enum a => a -> Int
fromEnum b
b), e
0)) ([(a, b)] -> [e]) -> [(a, b)] -> [e]
forall a b. (a -> b) -> a -> b
$ [(a, b)]
combinations
      mList :: [[e]]
mList        = [e] -> Int -> [[e]]
forall a. [a] -> Int -> [[a]]
buildList [e]
combAp Int
rrows
   in Matrix e (Normalize b) (Normalize a)
-> Matrix e (Normalize a) (Normalize b)
forall e cols rows. Matrix e cols rows -> Matrix e rows cols
tr (Matrix e (Normalize b) (Normalize a)
 -> Matrix e (Normalize a) (Normalize b))
-> Matrix e (Normalize b) (Normalize a)
-> Matrix e (Normalize a) (Normalize b)
forall a b. (a -> b) -> a -> b
$ [[e]] -> Matrix e (Normalize b) (Normalize a)
forall cols rows e.
FromLists cols rows =>
[[e]] -> Matrix e cols rows
fromLists [[e]]
mList
  where
    buildList :: [a] -> Int -> [[a]]
buildList [] Int
_ = []
    buildList [a]
l Int
r  = Int -> [a] -> [a]
forall a. Int -> [a] -> [a]
take Int
r [a]
l [a] -> [[a]] -> [[a]]
forall a. a -> [a] -> [a]
: [a] -> Int -> [[a]]
buildList (Int -> [a] -> [a]
forall a. Int -> [a] -> [a]
drop Int
r [a]
l) Int
r

-- Conversion

-- | Converts a matrix to a list of lists of elements.
toLists :: Matrix e cols rows -> [[e]]
toLists :: Matrix e cols rows -> [[e]]
toLists (One e
e)     = [[e
e]]
toLists (Fork Matrix e cols a
l Matrix e cols b
r) = Matrix e cols a -> [[e]]
forall e cols rows. Matrix e cols rows -> [[e]]
toLists Matrix e cols a
l [[e]] -> [[e]] -> [[e]]
forall a. [a] -> [a] -> [a]
++ Matrix e cols b -> [[e]]
forall e cols rows. Matrix e cols rows -> [[e]]
toLists Matrix e cols b
r
toLists (Join Matrix e a rows
l Matrix e b rows
r)  = ([e] -> [e] -> [e]) -> [[e]] -> [[e]] -> [[e]]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith [e] -> [e] -> [e]
forall a. [a] -> [a] -> [a]
(++) (Matrix e a rows -> [[e]]
forall e cols rows. Matrix e cols rows -> [[e]]
toLists Matrix e a rows
l) (Matrix e b rows -> [[e]]
forall e cols rows. Matrix e cols rows -> [[e]]
toLists Matrix e b rows
r)

-- | Converts a matrix to a list of elements.
toList :: Matrix e cols rows -> [e]
toList :: Matrix e cols rows -> [e]
toList = [[e]] -> [e]
forall (t :: Type -> Type) a. Foldable t => t [a] -> [a]
concat ([[e]] -> [e])
-> (Matrix e cols rows -> [[e]]) -> Matrix e cols rows -> [e]
forall (k :: Type -> Type -> Type) b c a.
Category k =>
k b c -> k a b -> k a c
. Matrix e cols rows -> [[e]]
forall e cols rows. Matrix e cols rows -> [[e]]
toLists

-- Zeros Matrix

-- | The zero matrix. A matrix wholly filled with zeros.
zeros :: (Num e, FL cols rows, CountableDims cols rows) => Matrix e cols rows
zeros :: Matrix e cols rows
zeros = ((Int, Int) -> e) -> Matrix e cols rows
forall e cols rows.
(FL cols rows, CountableDims cols rows) =>
((Int, Int) -> e) -> Matrix e cols rows
matrixBuilder' (e -> (Int, Int) -> e
forall a b. a -> b -> a
const e
0)

-- Ones Matrix

-- | The ones matrix. A matrix wholly filled with ones.
--
--   Also known as T (Top) matrix.
ones :: (Num e, FL cols rows, CountableDims cols rows) => Matrix e cols rows
ones :: Matrix e cols rows
ones = ((Int, Int) -> e) -> Matrix e cols rows
forall e cols rows.
(FL cols rows, CountableDims cols rows) =>
((Int, Int) -> e) -> Matrix e cols rows
matrixBuilder' (e -> (Int, Int) -> e
forall a b. a -> b -> a
const e
1)

-- Const Matrix

-- | The constant matrix constructor. A matrix wholly filled with a given
-- value.
constant :: (Num e, FL cols rows, CountableDims cols rows) => e -> Matrix e cols rows
constant :: e -> Matrix e cols rows
constant e
e = ((Int, Int) -> e) -> Matrix e cols rows
forall e cols rows.
(FL cols rows, CountableDims cols rows) =>
((Int, Int) -> e) -> Matrix e cols rows
matrixBuilder' (e -> (Int, Int) -> e
forall a b. a -> b -> a
const e
e)

-- Bang Matrix

-- | The T (Top) row vector matrix.
bang :: forall e cols. (Num e, Enum e, FL cols (), Countable cols) => Matrix e cols ()
bang :: Matrix e cols ()
bang =
  let c :: Int
c = Integer -> Int
forall a. Num a => Integer -> a
fromInteger (Integer -> Int) -> Integer -> Int
forall a b. (a -> b) -> a -> b
$ Proxy (Count cols) -> Integer
forall (n :: Nat) (proxy :: Nat -> Type).
KnownNat n =>
proxy n -> Integer
natVal (Proxy (Count cols)
forall k (t :: k). Proxy t
Proxy :: Proxy (Count cols))
   in [[e]] -> Matrix e cols ()
forall cols rows e.
FromLists cols rows =>
[[e]] -> Matrix e cols rows
fromLists [Int -> [e] -> [e]
forall a. Int -> [a] -> [a]
take Int
c [e
1, e
1 ..]]

-- iden Matrix

-- | iden matrix.
iden :: forall e cols . (Num e, FL cols cols, Countable cols) => Matrix e cols cols
iden :: Matrix e cols cols
iden = ((Int, Int) -> e) -> Matrix e cols cols
forall e cols rows.
(FL cols rows, CountableDims cols rows) =>
((Int, Int) -> e) -> Matrix e cols rows
matrixBuilder' (e -> e -> Bool -> e
forall a. a -> a -> Bool -> a
bool e
0 e
1 (Bool -> e) -> ((Int, Int) -> Bool) -> (Int, Int) -> e
forall (k :: Type -> Type -> Type) b c a.
Category k =>
k b c -> k a b -> k a c
. (Int -> Int -> Bool) -> (Int, Int) -> Bool
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
(==))
{-# NOINLINE iden #-}

-- Matrix composition (MMM)

-- | Matrix composition. Equivalent to matrix-matrix multiplication.
--
--   This definition takes advantage of divide-and-conquer and fusion laws
-- from LAoP.
comp :: (Num e) => Matrix e cr rows -> Matrix e cols cr -> Matrix e cols rows
comp :: Matrix e cr rows -> Matrix e cols cr -> Matrix e cols rows
comp (One e
a) (One e
b)       = e -> Matrix e () ()
forall e. e -> Matrix e () ()
One (e
a e -> e -> e
forall a. Num a => a -> a -> a
* e
b)
comp (Join Matrix e a rows
a Matrix e b rows
b) (Fork Matrix e cols a
c Matrix e cols b
d) = Matrix e a rows -> Matrix e cols a -> Matrix e cols rows
forall e cr rows cols.
Num e =>
Matrix e cr rows -> Matrix e cols cr -> Matrix e cols rows
comp Matrix e a rows
a Matrix e cols a
Matrix e cols a
c Matrix e cols rows -> Matrix e cols rows -> Matrix e cols rows
forall a. Num a => a -> a -> a
+ Matrix e b rows -> Matrix e cols b -> Matrix e cols rows
forall e cr rows cols.
Num e =>
Matrix e cr rows -> Matrix e cols cr -> Matrix e cols rows
comp Matrix e b rows
b Matrix e cols b
Matrix e cols b
d         -- Divide-and-conquer law
comp (Fork Matrix e cr a
a Matrix e cr b
b) Matrix e cols cr
c          = Matrix e cols a -> Matrix e cols b -> Matrix e cols (Either a b)
forall e cols a b.
Matrix e cols a -> Matrix e cols b -> Matrix e cols (Either a b)
Fork (Matrix e cr a -> Matrix e cols cr -> Matrix e cols a
forall e cr rows cols.
Num e =>
Matrix e cr rows -> Matrix e cols cr -> Matrix e cols rows
comp Matrix e cr a
a Matrix e cols cr
c) (Matrix e cr b -> Matrix e cols cr -> Matrix e cols b
forall e cr rows cols.
Num e =>
Matrix e cr rows -> Matrix e cols cr -> Matrix e cols rows
comp Matrix e cr b
b Matrix e cols cr
c) -- Fork fusion law
comp Matrix e cr rows
c (Join Matrix e a cr
a Matrix e b cr
b)          = Matrix e a rows -> Matrix e b rows -> Matrix e (Either a b) rows
forall e a rows b.
Matrix e a rows -> Matrix e b rows -> Matrix e (Either a b) rows
Join (Matrix e cr rows -> Matrix e a cr -> Matrix e a rows
forall e cr rows cols.
Num e =>
Matrix e cr rows -> Matrix e cols cr -> Matrix e cols rows
comp Matrix e cr rows
c Matrix e a cr
a) (Matrix e cr rows -> Matrix e b cr -> Matrix e b rows
forall e cr rows cols.
Num e =>
Matrix e cr rows -> Matrix e cols cr -> Matrix e cols rows
comp Matrix e cr rows
c Matrix e b cr
b)  -- Join fusion law
{-# NOINLINE comp #-}
{-# RULES
   "comp/iden1" forall m. comp m iden = m ;
   "comp/iden2" forall m. comp iden m = m
#-}

-- Scalar multiplication of matrices

infixl 7 .|
-- | Scalar multiplication of matrices.
(.|) :: Num e => e -> Matrix e cols rows -> Matrix e cols rows
.| :: e -> Matrix e cols rows -> Matrix e cols rows
(.|) e
e (One e
a) = e -> Matrix e () ()
forall e. e -> Matrix e () ()
One (e
e e -> e -> e
forall a. Num a => a -> a -> a
* e
a)
(.|) e
e (Join Matrix e a rows
a Matrix e b rows
b) = Matrix e a rows -> Matrix e b rows -> Matrix e (Either a b) rows
forall e a rows b.
Matrix e a rows -> Matrix e b rows -> Matrix e (Either a b) rows
Join (e
e e -> Matrix e a rows -> Matrix e a rows
forall e cols rows.
Num e =>
e -> Matrix e cols rows -> Matrix e cols rows
.| Matrix e a rows
a) (e
e e -> Matrix e b rows -> Matrix e b rows
forall e cols rows.
Num e =>
e -> Matrix e cols rows -> Matrix e cols rows
.| Matrix e b rows
b)
(.|) e
e (Fork Matrix e cols a
a Matrix e cols b
b) = Matrix e cols a -> Matrix e cols b -> Matrix e cols (Either a b)
forall e cols a b.
Matrix e cols a -> Matrix e cols b -> Matrix e cols (Either a b)
Fork (e
e e -> Matrix e cols a -> Matrix e cols a
forall e cols rows.
Num e =>
e -> Matrix e cols rows -> Matrix e cols rows
.| Matrix e cols a
a) (e
e e -> Matrix e cols b -> Matrix e cols b
forall e cols rows.
Num e =>
e -> Matrix e cols rows -> Matrix e cols rows
.| Matrix e cols b
b)

-- Scalar division of matrices

infixl 7 ./
-- | Scalar multiplication of matrices.
(./) :: Fractional e => Matrix e cols rows -> e -> Matrix e cols rows
./ :: Matrix e cols rows -> e -> Matrix e cols rows
(./) (One e
a) e
e = e -> Matrix e () ()
forall e. e -> Matrix e () ()
One (e
a e -> e -> e
forall a. Fractional a => a -> a -> a
/ e
e)
(./) (Join Matrix e a rows
a Matrix e b rows
b) e
e = Matrix e a rows -> Matrix e b rows -> Matrix e (Either a b) rows
forall e a rows b.
Matrix e a rows -> Matrix e b rows -> Matrix e (Either a b) rows
Join (Matrix e a rows
a Matrix e a rows -> e -> Matrix e a rows
forall e cols rows.
Fractional e =>
Matrix e cols rows -> e -> Matrix e cols rows
./ e
e) (Matrix e b rows
b Matrix e b rows -> e -> Matrix e b rows
forall e cols rows.
Fractional e =>
Matrix e cols rows -> e -> Matrix e cols rows
./ e
e)
(./) (Fork Matrix e cols a
a Matrix e cols b
b) e
e = Matrix e cols a -> Matrix e cols b -> Matrix e cols (Either a b)
forall e cols a b.
Matrix e cols a -> Matrix e cols b -> Matrix e cols (Either a b)
Fork (Matrix e cols a
a Matrix e cols a -> e -> Matrix e cols a
forall e cols rows.
Fractional e =>
Matrix e cols rows -> e -> Matrix e cols rows
./ e
e) (Matrix e cols b
b Matrix e cols b -> e -> Matrix e cols b
forall e cols rows.
Fractional e =>
Matrix e cols rows -> e -> Matrix e cols rows
./ e
e)

-- Projections

-- | Biproduct first component projection
p1 :: (Num e, CountableDims n m, FL n m, FL m m) => Matrix e (Either m n) m
p1 :: Matrix e (Either m n) m
p1 = Matrix e m m -> Matrix e n m -> Matrix e (Either m n) m
forall e a rows b.
Matrix e a rows -> Matrix e b rows -> Matrix e (Either a b) rows
join Matrix e m m
forall (k :: Type -> Type -> Type) a.
(Category k, Object k a) =>
k a a
id Matrix e n m
forall e cols rows.
(Num e, FL cols rows, CountableDims cols rows) =>
Matrix e cols rows
zeros

-- | Biproduct second component projection
p2 :: (Num e, CountableDims n m, FL m n, FL n n) => Matrix e (Either m n) n
p2 :: Matrix e (Either m n) n
p2 = Matrix e m n -> Matrix e n n -> Matrix e (Either m n) n
forall e a rows b.
Matrix e a rows -> Matrix e b rows -> Matrix e (Either a b) rows
join Matrix e m n
forall e cols rows.
(Num e, FL cols rows, CountableDims cols rows) =>
Matrix e cols rows
zeros Matrix e n n
forall (k :: Type -> Type -> Type) a.
(Category k, Object k a) =>
k a a
id

-- Injections

-- | Biproduct first component injection
i1 :: (Num e, CountableDims n m, FL n m, FL m m) => Matrix e m (Either m n)
i1 :: Matrix e m (Either m n)
i1 = Matrix e (Either m n) m -> Matrix e m (Either m n)
forall e cols rows. Matrix e cols rows -> Matrix e rows cols
tr Matrix e (Either m n) m
forall e n m.
(Num e, CountableDims n m, FL n m, FL m m) =>
Matrix e (Either m n) m
p1

-- | Biproduct second component injection
i2 :: (Num e, CountableDims n m, FL m n, FL n n) => Matrix e n (Either m n)
i2 :: Matrix e n (Either m n)
i2 = Matrix e (Either m n) n -> Matrix e n (Either m n)
forall e cols rows. Matrix e cols rows -> Matrix e rows cols
tr Matrix e (Either m n) n
forall e n m.
(Num e, CountableDims n m, FL m n, FL n n) =>
Matrix e (Either m n) n
p2

-- Dimensions

-- | Obtain the number of rows.
--
--   NOTE: The 'KnownNat' constraint is needed in order to obtain the
-- dimensions in constant time. For a version that doesn't require the
-- constraint see 'rows''.
rows :: forall e cols rows. (Countable rows) => Matrix e cols rows -> Int
rows :: Matrix e cols rows -> Int
rows Matrix e cols rows
_ = Integer -> Int
forall a. Num a => Integer -> a
fromInteger (Integer -> Int) -> Integer -> Int
forall a b. (a -> b) -> a -> b
$ Proxy (Count rows) -> Integer
forall (n :: Nat) (proxy :: Nat -> Type).
KnownNat n =>
proxy n -> Integer
natVal (Proxy (Count rows)
forall k (t :: k). Proxy t
Proxy :: Proxy (Count rows))

-- | Obtain the number of rows in an inefficient manner, but without any
-- constraints.
--
-- For a more efficient version see 'rows'.
rows' :: Matrix e cols rows -> Int
rows' :: Matrix e cols rows -> Int
rows' (One e
_) = Int
1
rows' (Join Matrix e a rows
lhs Matrix e b rows
_) = Matrix e a rows -> Int
forall e cols rows. Matrix e cols rows -> Int
rows' Matrix e a rows
lhs
rows' (Fork Matrix e cols a
top Matrix e cols b
bottom) = Matrix e cols a -> Int
forall e cols rows. Matrix e cols rows -> Int
rows' Matrix e cols a
top Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Matrix e cols b -> Int
forall e cols rows. Matrix e cols rows -> Int
rows' Matrix e cols b
bottom

-- | Obtain the number of columns.
--
--   NOTE: The 'KnownNat' constraint is needed in order to obtain the
-- dimensions in constant time. For a version that doesn't require the
-- constraint see 'columns''.
columns :: forall e cols rows. (Countable cols) => Matrix e cols rows -> Int
columns :: Matrix e cols rows -> Int
columns Matrix e cols rows
_ = Integer -> Int
forall a. Num a => Integer -> a
fromInteger (Integer -> Int) -> Integer -> Int
forall a b. (a -> b) -> a -> b
$ Proxy (Count cols) -> Integer
forall (n :: Nat) (proxy :: Nat -> Type).
KnownNat n =>
proxy n -> Integer
natVal (Proxy (Count cols)
forall k (t :: k). Proxy t
Proxy :: Proxy (Count cols))

-- | Obtain the number of columns in an inefficient manner, but without any
-- constraints.
--
-- For a more efficient version see 'columns'.
columns' :: Matrix e cols rows -> Int
columns' :: Matrix e cols rows -> Int
columns' (One e
_) = Int
1
columns' (Join Matrix e a rows
lhs Matrix e b rows
rhs) = Matrix e a rows -> Int
forall e cols rows. Matrix e cols rows -> Int
columns' Matrix e a rows
lhs Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Matrix e b rows -> Int
forall e cols rows. Matrix e cols rows -> Int
columns' Matrix e b rows
rhs
columns' (Fork Matrix e cols a
top Matrix e cols b
_) = Matrix e cols a -> Int
forall e cols rows. Matrix e cols rows -> Int
columns' Matrix e cols a
top

-- Coproduct Bifunctor

infixl 5 -|-

-- | Matrix coproduct functor also known as matrix direct sum.
(-|-) ::
  forall e n k m j.
  ( Num e,
    CountableDims j k,
    FL k k,
    FL j k,
    FL k j,
    FL j j
  ) =>
  Matrix e n k ->
  Matrix e m j ->
  Matrix e (Either n m) (Either k j)
-|- :: Matrix e n k -> Matrix e m j -> Matrix e (Either n m) (Either k j)
(-|-) Matrix e n k
a Matrix e m j
b = Matrix e n (Either k j)
-> Matrix e m (Either k j) -> Matrix e (Either n m) (Either k j)
forall e a rows b.
Matrix e a rows -> Matrix e b rows -> Matrix e (Either a b) rows
Join (Matrix e k (Either k j)
forall e n m.
(Num e, CountableDims n m, FL n m, FL m m) =>
Matrix e m (Either m n)
i1 Matrix e k (Either k j) -> Matrix e n k -> Matrix e n (Either k j)
forall (k :: Type -> Type -> Type) b c a.
Category k =>
k b c -> k a b -> k a c
. Matrix e n k
a) (Matrix e j (Either k j)
forall e n m.
(Num e, CountableDims n m, FL m n, FL n n) =>
Matrix e n (Either m n)
i2 Matrix e j (Either k j) -> Matrix e m j -> Matrix e m (Either k j)
forall (k :: Type -> Type -> Type) b c a.
Category k =>
k b c -> k a b -> k a c
. Matrix e m j
b)

-- Khatri Rao Product and projections

-- | Khatri Rao product first component projection matrix.
fstM ::
  forall e m k .
  ( Num e,
    CountableDims k m,
    FL (Normalize (m, k)) m,
    CountableN (m, k)
  ) => Matrix e (Normalize (m, k)) m
fstM :: Matrix e (Normalize (m, k)) m
fstM = ((Int, Int) -> e) -> Matrix e (FromNat (Count m * Count k)) m
forall e cols rows.
(FL cols rows, CountableDims cols rows) =>
((Int, Int) -> e) -> Matrix e cols rows
matrixBuilder' (Int, Int) -> e
f
  where
    offset :: Int
offset = Integer -> Int
forall a. Num a => Integer -> a
fromInteger (Proxy (Count k) -> Integer
forall (n :: Nat) (proxy :: Nat -> Type).
KnownNat n =>
proxy n -> Integer
natVal (Proxy (Count k)
forall k (t :: k). Proxy t
Proxy :: Proxy (Count k)))
    f :: (Int, Int) -> e
f (Int
x, Int
y)
      | Int
y Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
>= (Int
x Int -> Int -> Int
forall a. Num a => a -> a -> a
* Int
offset) Bool -> Bool -> Bool
&& Int
y Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
<= (Int
x Int -> Int -> Int
forall a. Num a => a -> a -> a
* Int
offset Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
offset Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1) = e
1
      | Bool
otherwise                                          = e
0

-- | Khatri Rao product second component projection matrix.
sndM ::
    forall e m k .
    ( Num e,
      CountableDims k m,
      FL (Normalize (m, k)) k,
      CountableN (m, k)
    ) => Matrix e (Normalize (m, k)) k
sndM :: Matrix e (Normalize (m, k)) k
sndM = ((Int, Int) -> e) -> Matrix e (FromNat (Count m * Count k)) k
forall e cols rows.
(FL cols rows, CountableDims cols rows) =>
((Int, Int) -> e) -> Matrix e cols rows
matrixBuilder' (Int, Int) -> e
f
  where
    offset :: Int
offset = Integer -> Int
forall a. Num a => Integer -> a
fromInteger (Proxy (Count k) -> Integer
forall (n :: Nat) (proxy :: Nat -> Type).
KnownNat n =>
proxy n -> Integer
natVal (Proxy (Count k)
forall k (t :: k). Proxy t
Proxy :: Proxy (Count k)))
    f :: (Int, Int) -> e
f (Int
x, Int
y)
      | Int
x Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
y Bool -> Bool -> Bool
|| Int -> Int -> Int
forall a. Integral a => a -> a -> a
mod (Int
y Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
x) Int
offset Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
0 = e
1
      | Bool
otherwise                        = e
0

-- | Khatri Rao Matrix product also known as matrix pairing.
--
--   NOTE: That this is not a true categorical product, see for instance:
--
-- @
--            | fstM . kr a b == a
-- kr a b ==> |
--            | sndM . kr a b == b
-- @
--
-- __Emphasis__ on the implication symbol.
kr ::
       forall e cols a b.
       ( Num e,
         CountableDims a b,
         CountableN (a, b),
         FL (Normalize (a, b)) a,
         FL (Normalize (a, b)) b
       ) => Matrix e cols a -> Matrix e cols b -> Matrix e cols (Normalize (a, b))
kr :: Matrix e cols a
-> Matrix e cols b -> Matrix e cols (Normalize (a, b))
kr Matrix e cols a
a Matrix e cols b
b =
  let fstM' :: Matrix e (Normalize (a, b)) a
fstM' = (Num e, CountableDims b a, FL (Normalize (a, b)) a,
 CountableN (a, b)) =>
Matrix e (Normalize (a, b)) a
forall e m k.
(Num e, CountableDims k m, FL (Normalize (m, k)) m,
 CountableN (m, k)) =>
Matrix e (Normalize (m, k)) m
fstM @e @a @b
      sndM' :: Matrix e (Normalize (a, b)) b
sndM' = (Num e, CountableDims b a, FL (Normalize (a, b)) b,
 CountableN (a, b)) =>
Matrix e (Normalize (a, b)) b
forall e m k.
(Num e, CountableDims k m, FL (Normalize (m, k)) k,
 CountableN (m, k)) =>
Matrix e (Normalize (m, k)) k
sndM @e @a @b
   in (Matrix e (FromNat (Count a * Count b)) a
-> Matrix e a (FromNat (Count a * Count b))
forall e cols rows. Matrix e cols rows -> Matrix e rows cols
tr Matrix e (Normalize (a, b)) a
Matrix e (FromNat (Count a * Count b)) a
fstM' Matrix e a (FromNat (Count a * Count b))
-> Matrix e cols a -> Matrix e cols (FromNat (Count a * Count b))
forall (k :: Type -> Type -> Type) b c a.
Category k =>
k b c -> k a b -> k a c
. Matrix e cols a
a) Matrix e cols (FromNat (Count a * Count b))
-> Matrix e cols (FromNat (Count a * Count b))
-> Matrix e cols (FromNat (Count a * Count b))
forall a. Num a => a -> a -> a
* (Matrix e (FromNat (Count a * Count b)) b
-> Matrix e b (FromNat (Count a * Count b))
forall e cols rows. Matrix e cols rows -> Matrix e rows cols
tr Matrix e (Normalize (a, b)) b
Matrix e (FromNat (Count a * Count b)) b
sndM' Matrix e b (FromNat (Count a * Count b))
-> Matrix e cols b -> Matrix e cols (FromNat (Count a * Count b))
forall (k :: Type -> Type -> Type) b c a.
Category k =>
k b c -> k a b -> k a c
. Matrix e cols b
b)

-- Product Bifunctor (Kronecker)

infixl 4 ><

-- | Matrix product functor also known as kronecker product
(><) ::
     forall e m p n q.
     ( Num e,
       CountableDims m n,
       CountableDims p q,
       CountableDimsN (m, n) (p, q),
       FL (Normalize (m, n)) m,
       FL (Normalize (m, n)) n,
       FL (Normalize (p, q)) p,
       FL (Normalize (p, q)) q
     )
     => Matrix e m p -> Matrix e n q -> Matrix e (Normalize (m, n)) (Normalize (p, q))
>< :: Matrix e m p
-> Matrix e n q -> Matrix e (Normalize (m, n)) (Normalize (p, q))
(><) Matrix e m p
a Matrix e n q
b =
  let fstM' :: Matrix e (Normalize (m, n)) m
fstM' = (Num e, CountableDims n m, FL (Normalize (m, n)) m,
 CountableN (m, n)) =>
Matrix e (Normalize (m, n)) m
forall e m k.
(Num e, CountableDims k m, FL (Normalize (m, k)) m,
 CountableN (m, k)) =>
Matrix e (Normalize (m, k)) m
fstM @e @m @n
      sndM' :: Matrix e (Normalize (m, n)) n
sndM' = (Num e, CountableDims n m, FL (Normalize (m, n)) n,
 CountableN (m, n)) =>
Matrix e (Normalize (m, n)) n
forall e m k.
(Num e, CountableDims k m, FL (Normalize (m, k)) k,
 CountableN (m, k)) =>
Matrix e (Normalize (m, k)) k
sndM @e @m @n
   in Matrix e (FromNat (Count m * Count n)) p
-> Matrix e (FromNat (Count m * Count n)) q
-> Matrix e (FromNat (Count m * Count n)) (Normalize (p, q))
forall e cols a b.
(Num e, CountableDims a b, CountableN (a, b),
 FL (Normalize (a, b)) a, FL (Normalize (a, b)) b) =>
Matrix e cols a
-> Matrix e cols b -> Matrix e cols (Normalize (a, b))
kr (Matrix e m p
a Matrix e m p
-> Matrix e (FromNat (Count m * Count n)) m
-> Matrix e (FromNat (Count m * Count n)) p
forall (k :: Type -> Type -> Type) b c a.
Category k =>
k b c -> k a b -> k a c
. Matrix e (Normalize (m, n)) m
Matrix e (FromNat (Count m * Count n)) m
fstM') (Matrix e n q
b Matrix e n q
-> Matrix e (FromNat (Count m * Count n)) n
-> Matrix e (FromNat (Count m * Count n)) q
forall (k :: Type -> Type -> Type) b c a.
Category k =>
k b c -> k a b -> k a c
. Matrix e (Normalize (m, n)) n
Matrix e (FromNat (Count m * Count n)) n
sndM')

-- Matrix abide Join Fork

-- | Matrix "abiding" following the 'Join'-'Fork' exchange law.
--
-- Law:
--
-- @
-- 'Join' ('Fork' a c) ('Fork' b d) == 'Fork' ('Join' a b) ('Join' c d)
-- @
abideJF :: Matrix e cols rows -> Matrix e cols rows
abideJF :: Matrix e cols rows -> Matrix e cols rows
abideJF (Join (Fork Matrix e a a
a Matrix e a b
c) (Fork Matrix e b a
b Matrix e b b
d)) = Matrix e (Either a b) a
-> Matrix e (Either a b) b -> Matrix e (Either a b) (Either a b)
forall e cols a b.
Matrix e cols a -> Matrix e cols b -> Matrix e cols (Either a b)
Fork (Matrix e a a -> Matrix e b a -> Matrix e (Either a b) a
forall e a rows b.
Matrix e a rows -> Matrix e b rows -> Matrix e (Either a b) rows
Join (Matrix e a a -> Matrix e a a
forall e cols rows. Matrix e cols rows -> Matrix e cols rows
abideJF Matrix e a a
a) (Matrix e b a -> Matrix e b a
forall e cols rows. Matrix e cols rows -> Matrix e cols rows
abideJF Matrix e b a
b)) (Matrix e a b -> Matrix e b b -> Matrix e (Either a b) b
forall e a rows b.
Matrix e a rows -> Matrix e b rows -> Matrix e (Either a b) rows
Join (Matrix e a b -> Matrix e a b
forall e cols rows. Matrix e cols rows -> Matrix e cols rows
abideJF Matrix e a b
c) (Matrix e b b -> Matrix e b b
forall e cols rows. Matrix e cols rows -> Matrix e cols rows
abideJF Matrix e b b
d)) -- Join-Fork abide law
abideJF (One e
e)                      = e -> Matrix e () ()
forall e. e -> Matrix e () ()
One e
e
abideJF (Join Matrix e a rows
a Matrix e b rows
b)                   = Matrix e a rows -> Matrix e b rows -> Matrix e (Either a b) rows
forall e a rows b.
Matrix e a rows -> Matrix e b rows -> Matrix e (Either a b) rows
Join (Matrix e a rows -> Matrix e a rows
forall e cols rows. Matrix e cols rows -> Matrix e cols rows
abideJF Matrix e a rows
a) (Matrix e b rows -> Matrix e b rows
forall e cols rows. Matrix e cols rows -> Matrix e cols rows
abideJF Matrix e b rows
b)
abideJF (Fork Matrix e cols a
a Matrix e cols b
b)                   = Matrix e cols a -> Matrix e cols b -> Matrix e cols (Either a b)
forall e cols a b.
Matrix e cols a -> Matrix e cols b -> Matrix e cols (Either a b)
Fork (Matrix e cols a -> Matrix e cols a
forall e cols rows. Matrix e cols rows -> Matrix e cols rows
abideJF Matrix e cols a
a) (Matrix e cols b -> Matrix e cols b
forall e cols rows. Matrix e cols rows -> Matrix e cols rows
abideJF Matrix e cols b
b)

-- Matrix abide Fork Join

-- | Matrix "abiding" followin the 'Fork'-'Join' abide law.
--
-- @
-- 'Fork' ('Join' a b) ('Join' c d) == 'Join' ('Fork' a c) ('Fork' b d)
-- @
abideFJ :: Matrix e cols rows -> Matrix e cols rows
abideFJ :: Matrix e cols rows -> Matrix e cols rows
abideFJ (Fork (Join Matrix e a a
a Matrix e b a
b) (Join Matrix e a b
c Matrix e b b
d)) = Matrix e a (Either a b)
-> Matrix e b (Either a b) -> Matrix e (Either a b) (Either a b)
forall e a rows b.
Matrix e a rows -> Matrix e b rows -> Matrix e (Either a b) rows
Join (Matrix e a a -> Matrix e a b -> Matrix e a (Either a b)
forall e cols a b.
Matrix e cols a -> Matrix e cols b -> Matrix e cols (Either a b)
Fork (Matrix e a a -> Matrix e a a
forall e cols rows. Matrix e cols rows -> Matrix e cols rows
abideFJ Matrix e a a
a) (Matrix e a b -> Matrix e a b
forall e cols rows. Matrix e cols rows -> Matrix e cols rows
abideFJ Matrix e a b
c)) (Matrix e b a -> Matrix e b b -> Matrix e b (Either a b)
forall e cols a b.
Matrix e cols a -> Matrix e cols b -> Matrix e cols (Either a b)
Fork (Matrix e b a -> Matrix e b a
forall e cols rows. Matrix e cols rows -> Matrix e cols rows
abideFJ Matrix e b a
b) (Matrix e b b -> Matrix e b b
forall e cols rows. Matrix e cols rows -> Matrix e cols rows
abideFJ Matrix e b b
d)) -- Fork-Join abide law
abideFJ (One e
e)                      = e -> Matrix e () ()
forall e. e -> Matrix e () ()
One e
e
abideFJ (Join Matrix e a rows
a Matrix e b rows
b)                   = Matrix e a rows -> Matrix e b rows -> Matrix e (Either a b) rows
forall e a rows b.
Matrix e a rows -> Matrix e b rows -> Matrix e (Either a b) rows
Join (Matrix e a rows -> Matrix e a rows
forall e cols rows. Matrix e cols rows -> Matrix e cols rows
abideFJ Matrix e a rows
a) (Matrix e b rows -> Matrix e b rows
forall e cols rows. Matrix e cols rows -> Matrix e cols rows
abideFJ Matrix e b rows
b)
abideFJ (Fork Matrix e cols a
a Matrix e cols b
b)                   = Matrix e cols a -> Matrix e cols b -> Matrix e cols (Either a b)
forall e cols a b.
Matrix e cols a -> Matrix e cols b -> Matrix e cols (Either a b)
Fork (Matrix e cols a -> Matrix e cols a
forall e cols rows. Matrix e cols rows -> Matrix e cols rows
abideFJ Matrix e cols a
a) (Matrix e cols b -> Matrix e cols b
forall e cols rows. Matrix e cols rows -> Matrix e cols rows
abideFJ Matrix e cols b
b)

-- Matrix transposition

-- | Matrix transposition.
tr :: Matrix e cols rows -> Matrix e rows cols
tr :: Matrix e cols rows -> Matrix e rows cols
tr (One e
e)    = e -> Matrix e () ()
forall e. e -> Matrix e () ()
One e
e
tr (Join Matrix e a rows
a Matrix e b rows
b) = Matrix e rows a -> Matrix e rows b -> Matrix e rows (Either a b)
forall e cols a b.
Matrix e cols a -> Matrix e cols b -> Matrix e cols (Either a b)
Fork (Matrix e a rows -> Matrix e rows a
forall e cols rows. Matrix e cols rows -> Matrix e rows cols
tr Matrix e a rows
a) (Matrix e b rows -> Matrix e rows b
forall e cols rows. Matrix e cols rows -> Matrix e rows cols
tr Matrix e b rows
b)
tr (Fork Matrix e cols a
a Matrix e cols b
b) = Matrix e a cols -> Matrix e b cols -> Matrix e (Either a b) cols
forall e a rows b.
Matrix e a rows -> Matrix e b rows -> Matrix e (Either a b) rows
Join (Matrix e cols a -> Matrix e a cols
forall e cols rows. Matrix e cols rows -> Matrix e rows cols
tr Matrix e cols a
a) (Matrix e cols b -> Matrix e b cols
forall e cols rows. Matrix e cols rows -> Matrix e rows cols
tr Matrix e cols b
b)

-- Selective 'select' operator

-- | Selective functors 'select' operator equivalent inspired by the
-- ArrowMonad solution presented in the paper.
select :: (Num e, FL b b, Countable b) => Matrix e cols (Either a b) -> Matrix e a b -> Matrix e cols b
select :: Matrix e cols (Either a b) -> Matrix e a b -> Matrix e cols b
select (Fork Matrix e cols a
a Matrix e cols b
b) Matrix e a b
y                   = Matrix e a b
y Matrix e a b -> Matrix e cols a -> Matrix e cols b
forall (k :: Type -> Type -> Type) b c a.
Category k =>
k b c -> k a b -> k a c
. Matrix e cols a
Matrix e cols a
a Matrix e cols b -> Matrix e cols b -> Matrix e cols b
forall a. Num a => a -> a -> a
+ Matrix e cols b
Matrix e cols b
b                     -- Divide-and-conquer law
select (Join (Fork Matrix e a a
a Matrix e a b
c) (Fork Matrix e b a
b Matrix e b b
d)) Matrix e a b
y = Matrix e a b -> Matrix e b b -> Matrix e (Either a b) b
forall e a rows b.
Matrix e a rows -> Matrix e b rows -> Matrix e (Either a b) rows
join (Matrix e a b
y Matrix e a b -> Matrix e a a -> Matrix e a b
forall (k :: Type -> Type -> Type) b c a.
Category k =>
k b c -> k a b -> k a c
. Matrix e a a
Matrix e a a
a Matrix e a b -> Matrix e a b -> Matrix e a b
forall a. Num a => a -> a -> a
+ Matrix e a b
Matrix e a b
c) (Matrix e a b
y Matrix e a b -> Matrix e b a -> Matrix e b b
forall (k :: Type -> Type -> Type) b c a.
Category k =>
k b c -> k a b -> k a c
. Matrix e b a
Matrix e b a
b Matrix e b b -> Matrix e b b -> Matrix e b b
forall a. Num a => a -> a -> a
+ Matrix e b b
Matrix e b b
d)  -- Pattern matching + DnC law
select Matrix e cols (Either a b)
m Matrix e a b
y                            = Matrix e a b -> Matrix e b b -> Matrix e (Either a b) b
forall e a rows b.
Matrix e a rows -> Matrix e b rows -> Matrix e (Either a b) rows
join Matrix e a b
y Matrix e b b
forall (k :: Type -> Type -> Type) a.
(Category k, Object k a) =>
k a a
id Matrix e (Either a b) b
-> Matrix e cols (Either a b) -> Matrix e cols b
forall (k :: Type -> Type -> Type) b c a.
Category k =>
k b c -> k a b -> k a c
. Matrix e cols (Either a b)
m

branch ::
       ( Num e,
         CountableDims a b,
         CountableDims c (Either b c),
         FL c b,
         FL a b,
         FL a a,
         FL b b,
         FL c c,
         FL b a,
         FL b c,
         FL (Either b c) b,
         FL (Either b c) c
       )
       => Matrix e cols (Either a b) -> Matrix e a c -> Matrix e b c -> Matrix e cols c
branch :: Matrix e cols (Either a b)
-> Matrix e a c -> Matrix e b c -> Matrix e cols c
branch Matrix e cols (Either a b)
x Matrix e a c
l Matrix e b c
r = Matrix e cols (Either a b) -> Matrix e cols (Either a (Either b c))
forall e a b c cols.
(Num e, Countable a, CountableDims b c, FL a b, FL c b, FL b b,
 FL b a, FL a a) =>
Matrix e cols (Either a b) -> Matrix e cols (Either a (Either b c))
f Matrix e cols (Either a b)
x Matrix e cols (Either a (Either b c))
-> Matrix e a (Either b c) -> Matrix e cols (Either b c)
forall e b cols a.
(Num e, FL b b, Countable b) =>
Matrix e cols (Either a b) -> Matrix e a b -> Matrix e cols b
`select` Matrix e a c -> Matrix e a (Either b c)
forall e b c a.
(Num e, CountableDims b c, FL b c, FL c c) =>
Matrix e a c -> Matrix e a (Either b c)
g Matrix e a c
l Matrix e cols (Either b c) -> Matrix e b c -> Matrix e cols c
forall e b cols a.
(Num e, FL b b, Countable b) =>
Matrix e cols (Either a b) -> Matrix e a b -> Matrix e cols b
`select` Matrix e b c
r
  where
    f :: (Num e, Countable a, CountableDims b c, FL a b, FL c b, FL b b, FL b a, FL a a)
      => Matrix e cols (Either a b) -> Matrix e cols (Either a (Either b c))
    f :: Matrix e cols (Either a b) -> Matrix e cols (Either a (Either b c))
f Matrix e cols (Either a b)
m = Matrix e (Either a b) a
-> Matrix e (Either a b) (Either b c)
-> Matrix e (Either a b) (Either a (Either b c))
forall e cols a b.
Matrix e cols a -> Matrix e cols b -> Matrix e cols (Either a b)
fork (Matrix e a (Either a b) -> Matrix e (Either a b) a
forall e cols rows. Matrix e cols rows -> Matrix e rows cols
tr Matrix e a (Either a b)
forall e n m.
(Num e, CountableDims n m, FL n m, FL m m) =>
Matrix e m (Either m n)
i1) (Matrix e b (Either b c)
forall e n m.
(Num e, CountableDims n m, FL n m, FL m m) =>
Matrix e m (Either m n)
i1 Matrix e b (Either b c)
-> Matrix e (Either a b) b -> Matrix e (Either a b) (Either b c)
forall (k :: Type -> Type -> Type) b c a.
Category k =>
k b c -> k a b -> k a c
. Matrix e b (Either a b) -> Matrix e (Either a b) b
forall e cols rows. Matrix e cols rows -> Matrix e rows cols
tr Matrix e b (Either a b)
forall e n m.
(Num e, CountableDims n m, FL m n, FL n n) =>
Matrix e n (Either m n)
i2) Matrix e (Either a b) (Either a (Either b c))
-> Matrix e cols (Either a b)
-> Matrix e cols (Either a (Either b c))
forall (k :: Type -> Type -> Type) b c a.
Category k =>
k b c -> k a b -> k a c
. Matrix e cols (Either a b)
m
    g :: (Num e, CountableDims b c, FL b c, FL c c) => Matrix e a c -> Matrix e a (Either b c)
    g :: Matrix e a c -> Matrix e a (Either b c)
g Matrix e a c
m = Matrix e c (Either b c)
forall e n m.
(Num e, CountableDims n m, FL m n, FL n n) =>
Matrix e n (Either m n)
i2 Matrix e c (Either b c) -> Matrix e a c -> Matrix e a (Either b c)
forall (k :: Type -> Type -> Type) b c a.
Category k =>
k b c -> k a b -> k a c
. Matrix e a c
m

-- McCarthy's Conditional

-- | McCarthy's Conditional expresses probabilistic choice.
cond ::
     ( Trivial cols,
       Countable cols,
       FL () cols,
       FL cols (),
       FL cols cols,
       Bounded a,
       Enum a,
       Num e,
       Ord e
     )
     =>
     (a -> Bool) -> Matrix e cols rows -> Matrix e cols rows -> Matrix e cols rows
cond :: (a -> Bool)
-> Matrix e cols rows -> Matrix e cols rows -> Matrix e cols rows
cond a -> Bool
p Matrix e cols rows
f Matrix e cols rows
g = Matrix e cols rows
-> Matrix e cols rows -> Matrix e (Either cols cols) rows
forall e a rows b.
Matrix e a rows -> Matrix e b rows -> Matrix e (Either a b) rows
join Matrix e cols rows
f Matrix e cols rows
g Matrix e (Either cols cols) rows
-> Matrix e cols (Either cols cols) -> Matrix e cols rows
forall (k :: Type -> Type -> Type) b c a.
Category k =>
k b c -> k a b -> k a c
. (a -> Bool) -> Matrix e cols (Either cols cols)
forall q a e.
(Trivial q, Countable q, FL () q, FL q (), FL q q, Bounded a,
 Enum a, Num e, Ord e) =>
(a -> Bool) -> Matrix e q (Either q q)
grd a -> Bool
p

grd ::
    ( Trivial q,
      Countable q,
      FL () q,
      FL q (),
      FL q q,
      Bounded a,
      Enum a,
      Num e,
      Ord e
    )
    =>
    (a -> Bool) -> Matrix e q (Either q q)
grd :: (a -> Bool) -> Matrix e q (Either q q)
grd a -> Bool
f = Matrix e q q -> Matrix e q q -> Matrix e q (Either q q)
forall e cols a b.
Matrix e cols a -> Matrix e cols b -> Matrix e cols (Either a b)
fork ((a -> Bool) -> Matrix e q q
forall e a q.
(Trivial q, Countable q, FL () q, FL q (), FL q q,
 Liftable e a Bool) =>
(a -> Bool) -> Matrix e q q
corr a -> Bool
f) ((a -> Bool) -> Matrix e q q
forall e a q.
(Trivial q, Countable q, FL () q, FL q (), FL q q,
 Liftable e a Bool) =>
(a -> Bool) -> Matrix e q q
corr (Bool -> Bool
not (Bool -> Bool) -> (a -> Bool) -> a -> Bool
forall (k :: Type -> Type -> Type) b c a.
Category k =>
k b c -> k a b -> k a c
. a -> Bool
f))

corr ::
    forall e a q .
    ( Trivial q,
      Countable q,
      FL () q,
      FL q (),
      FL q q,
      Liftable e a Bool
    )
     => (a -> Bool) -> Matrix e q q
corr :: (a -> Bool) -> Matrix e q q
corr a -> Bool
p = let f :: Matrix e q ()
f = (a -> Bool) -> Matrix e q ()
forall a b cols rows e.
(Liftable e a b, CountableDims cols rows, FL rows cols) =>
(a -> b) -> Matrix e cols rows
fromF' a -> Bool
p :: Matrix e q ()
          in Matrix e q () -> Matrix e q q -> Matrix e q (Normalize ((), q))
forall e cols a b.
(Num e, CountableDims a b, CountableN (a, b),
 FL (Normalize (a, b)) a, FL (Normalize (a, b)) b) =>
Matrix e cols a
-> Matrix e cols b -> Matrix e cols (Normalize (a, b))
kr Matrix e q ()
f (Matrix e q q
forall (k :: Type -> Type -> Type) a.
(Category k, Object k a) =>
k a a
id :: Matrix e q q)

-- Pretty print

prettyAux :: Show e => [[e]] -> [[e]] -> String
prettyAux :: [[e]] -> [[e]] -> String
prettyAux [] [[e]]
_     = String
""
prettyAux [[e
e]] [[e]]
m  = String
"│ " String -> ShowS
forall a. [a] -> [a] -> [a]
++ ShowS
fill (e -> String
forall a. Show a => a -> String
show e
e) String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" │\n"
  where
   v :: [String]
v  = ([e] -> String) -> [[e]] -> [String]
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
fmap [e] -> String
forall a. Show a => a -> String
show [[e]]
m
   widest :: Int
widest = [Int] -> Int
forall (t :: Type -> Type) a. (Foldable t, Ord a) => t a -> a
maximum ([Int] -> Int) -> [Int] -> Int
forall a b. (a -> b) -> a -> b
$ (String -> Int) -> [String] -> [Int]
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
fmap String -> Int
forall (t :: Type -> Type) a. Foldable t => t a -> Int
length [String]
v
   fill :: ShowS
fill String
str = Int -> Char -> String
forall a. Int -> a -> [a]
replicate (Int
widest Int -> Int -> Int
forall a. Num a => a -> a -> a
- String -> Int
forall (t :: Type -> Type) a. Foldable t => t a -> Int
length String
str Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
2) Char
' ' String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
str
prettyAux [[e]
h] [[e]]
m    = String
"│ " String -> ShowS
forall a. [a] -> [a] -> [a]
++ ShowS
fill ([String] -> String
unwords ([String] -> String) -> [String] -> String
forall a b. (a -> b) -> a -> b
$ (e -> String) -> [e] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map e -> String
forall a. Show a => a -> String
show [e]
h) String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" │\n"
  where
   v :: [String]
v        = ([e] -> String) -> [[e]] -> [String]
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
fmap [e] -> String
forall a. Show a => a -> String
show [[e]]
m
   widest :: Int
widest   = [Int] -> Int
forall (t :: Type -> Type) a. (Foldable t, Ord a) => t a -> a
maximum ([Int] -> Int) -> [Int] -> Int
forall a b. (a -> b) -> a -> b
$ (String -> Int) -> [String] -> [Int]
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
fmap String -> Int
forall (t :: Type -> Type) a. Foldable t => t a -> Int
length [String]
v
   fill :: ShowS
fill String
str = Int -> Char -> String
forall a. Int -> a -> [a]
replicate (Int
widest Int -> Int -> Int
forall a. Num a => a -> a -> a
- String -> Int
forall (t :: Type -> Type) a. Foldable t => t a -> Int
length String
str Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
2) Char
' ' String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
str
prettyAux ([e]
h : [[e]]
t) [[e]]
l = String
"│ " String -> ShowS
forall a. [a] -> [a] -> [a]
++ ShowS
fill ([String] -> String
unwords ([String] -> String) -> [String] -> String
forall a b. (a -> b) -> a -> b
$ (e -> String) -> [e] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map e -> String
forall a. Show a => a -> String
show [e]
h) String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" │\n" String -> ShowS
forall a. [a] -> [a] -> [a]
++
                      [[e]] -> [[e]] -> String
forall e. Show e => [[e]] -> [[e]] -> String
prettyAux [[e]]
t [[e]]
l
  where
   v :: [String]
v        = ([e] -> String) -> [[e]] -> [String]
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
fmap [e] -> String
forall a. Show a => a -> String
show [[e]]
l
   widest :: Int
widest   = [Int] -> Int
forall (t :: Type -> Type) a. (Foldable t, Ord a) => t a -> a
maximum ([Int] -> Int) -> [Int] -> Int
forall a b. (a -> b) -> a -> b
$ (String -> Int) -> [String] -> [Int]
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
fmap String -> Int
forall (t :: Type -> Type) a. Foldable t => t a -> Int
length [String]
v
   fill :: ShowS
fill String
str = Int -> Char -> String
forall a. Int -> a -> [a]
replicate (Int
widest Int -> Int -> Int
forall a. Num a => a -> a -> a
- String -> Int
forall (t :: Type -> Type) a. Foldable t => t a -> Int
length String
str Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
2) Char
' ' String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
str

-- | Matrix pretty printer
pretty :: (CountableDims cols rows, Show e) => Matrix e cols rows -> String
pretty :: Matrix e cols rows -> String
pretty Matrix e cols rows
m = [String] -> String
forall (t :: Type -> Type) a. Foldable t => t [a] -> [a]
concat
   [ String
"┌ ", [String] -> String
unwords (Int -> String -> [String]
forall a. Int -> a -> [a]
replicate (Matrix e cols rows -> Int
forall e cols rows. Countable cols => Matrix e cols rows -> Int
columns Matrix e cols rows
m) String
blank), String
" ┐\n"
   , [String] -> String
unlines
   [ String
"│ " String -> ShowS
forall a. [a] -> [a] -> [a]
++ [String] -> String
unwords ((Int -> String) -> [Int] -> [String]
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
fmap (\Int
j -> ShowS
fill ShowS -> ShowS
forall a b. (a -> b) -> a -> b
$ e -> String
forall a. Show a => a -> String
show (e -> String) -> e -> String
forall a b. (a -> b) -> a -> b
$ Int -> Int -> Matrix e cols rows -> e
forall rows cols a.
(KnownNat (Count rows), KnownNat (Count cols)) =>
Int -> Int -> Matrix a cols rows -> a
getElem Int
i Int
j Matrix e cols rows
m) [Int
1..Matrix e cols rows -> Int
forall e cols rows. Countable cols => Matrix e cols rows -> Int
columns Matrix e cols rows
m]) String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" │" | Int
i <- [Int
1..Matrix e cols rows -> Int
forall e cols rows. Countable rows => Matrix e cols rows -> Int
rows Matrix e cols rows
m] ]
   , String
"└ ", [String] -> String
unwords (Int -> String -> [String]
forall a. Int -> a -> [a]
replicate (Matrix e cols rows -> Int
forall e cols rows. Countable cols => Matrix e cols rows -> Int
columns Matrix e cols rows
m) String
blank), String
" ┘"
   ]
 where
   strings :: [String]
strings  = (e -> String) -> [e] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map e -> String
forall a. Show a => a -> String
show (Matrix e cols rows -> [e]
forall e cols rows. Matrix e cols rows -> [e]
toList Matrix e cols rows
m)
   widest :: Int
widest   = [Int] -> Int
forall (t :: Type -> Type) a. (Foldable t, Ord a) => t a -> a
maximum ([Int] -> Int) -> [Int] -> Int
forall a b. (a -> b) -> a -> b
$ (String -> Int) -> [String] -> [Int]
forall a b. (a -> b) -> [a] -> [b]
map String -> Int
forall (t :: Type -> Type) a. Foldable t => t a -> Int
length [String]
strings
   fill :: ShowS
fill String
str = Int -> Char -> String
forall a. Int -> a -> [a]
replicate (Int
widest Int -> Int -> Int
forall a. Num a => a -> a -> a
- String -> Int
forall (t :: Type -> Type) a. Foldable t => t a -> Int
length String
str) Char
' ' String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
str
   blank :: String
blank    = ShowS
fill String
""
   safeGet :: Int -> Int -> Matrix a cols rows -> Maybe a
safeGet Int
i Int
j Matrix a cols rows
m
    | Int
i Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Matrix a cols rows -> Int
forall e cols rows. Countable rows => Matrix e cols rows -> Int
rows Matrix a cols rows
m Bool -> Bool -> Bool
|| Int
j Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Matrix a cols rows -> Int
forall e cols rows. Countable cols => Matrix e cols rows -> Int
columns Matrix a cols rows
m Bool -> Bool -> Bool
|| Int
i Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< Int
1 Bool -> Bool -> Bool
|| Int
j Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< Int
1 = Maybe a
forall a. Maybe a
Nothing
    | Bool
otherwise = a -> Maybe a
forall a. a -> Maybe a
Just (a -> Maybe a) -> a -> Maybe a
forall a b. (a -> b) -> a -> b
$ Int -> Int -> Matrix a cols rows -> [a] -> a
forall cols e rows a.
KnownNat (Count cols) =>
Int -> Int -> Matrix e cols rows -> [a] -> a
unsafeGet Int
i Int
j Matrix a cols rows
m (Matrix a cols rows -> [a]
forall e cols rows. Matrix e cols rows -> [e]
toList Matrix a cols rows
m)
   unsafeGet :: Int -> Int -> Matrix e cols rows -> [a] -> a
unsafeGet Int
i Int
j Matrix e cols rows
m [a]
l = [a]
l [a] -> Int -> a
forall a. [a] -> Int -> a
!! Int -> (Int, Int) -> Int
forall a. Num a => a -> (a, a) -> a
encode (Matrix e cols rows -> Int
forall e cols rows. Countable cols => Matrix e cols rows -> Int
columns Matrix e cols rows
m) (Int
i,Int
j)
   encode :: a -> (a, a) -> a
encode a
m (a
i,a
j)    = (a
ia -> a -> a
forall a. Num a => a -> a -> a
-a
1)a -> a -> a
forall a. Num a => a -> a -> a
*a
m a -> a -> a
forall a. Num a => a -> a -> a
+ a
j a -> a -> a
forall a. Num a => a -> a -> a
- a
1
   getElem :: Int -> Int -> Matrix a cols rows -> a
getElem Int
i Int
j Matrix a cols rows
m     =
     a -> Maybe a -> a
forall a. a -> Maybe a -> a
fromMaybe
       (String -> a
forall a. HasCallStack => String -> a
error (String -> a) -> String -> a
forall a b. (a -> b) -> a -> b
$
          String
"getElem: Trying to get the "
           String -> ShowS
forall a. [a] -> [a] -> [a]
++ (Int, Int) -> String
forall a. Show a => a -> String
show (Int
i, Int
j)
           String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" element from a "
           String -> ShowS
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show (Matrix a cols rows -> Int
forall e cols rows. Countable rows => Matrix e cols rows -> Int
rows Matrix a cols rows
m) String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"x" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show (Matrix a cols rows -> Int
forall e cols rows. Countable cols => Matrix e cols rows -> Int
columns Matrix a cols rows
m)
           String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" matrix."
       )
       (Int -> Int -> Matrix a cols rows -> Maybe a
forall rows cols a.
(KnownNat (Count rows), KnownNat (Count cols)) =>
Int -> Int -> Matrix a cols rows -> Maybe a
safeGet Int
i Int
j Matrix a cols rows
m)

-- | Matrix pretty printer
prettyPrint :: (CountableDims cols rows, Show e) => Matrix e cols rows -> IO ()
prettyPrint :: Matrix e cols rows -> IO ()
prettyPrint = String -> IO ()
putStrLn (String -> IO ())
-> (Matrix e cols rows -> String) -> Matrix e cols rows -> IO ()
forall (k :: Type -> Type -> Type) b c a.
Category k =>
k b c -> k a b -> k a c
. Matrix e cols rows -> String
forall cols rows e.
(CountableDims cols rows, Show e) =>
Matrix e cols rows -> String
pretty

-- | Zip two matrices with a given binary function
zipWithM :: (e -> f -> g) -> Matrix e cols rows -> Matrix f cols rows -> Matrix g cols rows
zipWithM :: (e -> f -> g)
-> Matrix e cols rows -> Matrix f cols rows -> Matrix g cols rows
zipWithM e -> f -> g
f (One e
a) (One f
b)           = g -> Matrix g () ()
forall e. e -> Matrix e () ()
One (e -> f -> g
f e
a f
b)
zipWithM e -> f -> g
f (Join Matrix e a rows
a Matrix e b rows
b) (Join Matrix f a rows
c Matrix f b rows
d)     = Matrix g a rows -> Matrix g b rows -> Matrix g (Either a b) rows
forall e a rows b.
Matrix e a rows -> Matrix e b rows -> Matrix e (Either a b) rows
Join ((e -> f -> g)
-> Matrix e a rows -> Matrix f a rows -> Matrix g a rows
forall e f g cols rows.
(e -> f -> g)
-> Matrix e cols rows -> Matrix f cols rows -> Matrix g cols rows
zipWithM e -> f -> g
f Matrix e a rows
a Matrix f a rows
Matrix f a rows
c) ((e -> f -> g)
-> Matrix e b rows -> Matrix f b rows -> Matrix g b rows
forall e f g cols rows.
(e -> f -> g)
-> Matrix e cols rows -> Matrix f cols rows -> Matrix g cols rows
zipWithM e -> f -> g
f Matrix e b rows
b Matrix f b rows
Matrix f b rows
d)
zipWithM e -> f -> g
f (Fork Matrix e cols a
a Matrix e cols b
b) (Fork Matrix f cols a
c Matrix f cols b
d)     = Matrix g cols a -> Matrix g cols b -> Matrix g cols (Either a b)
forall e cols a b.
Matrix e cols a -> Matrix e cols b -> Matrix e cols (Either a b)
Fork ((e -> f -> g)
-> Matrix e cols a -> Matrix f cols a -> Matrix g cols a
forall e f g cols rows.
(e -> f -> g)
-> Matrix e cols rows -> Matrix f cols rows -> Matrix g cols rows
zipWithM e -> f -> g
f Matrix e cols a
a Matrix f cols a
Matrix f cols a
c) ((e -> f -> g)
-> Matrix e cols b -> Matrix f cols b -> Matrix g cols b
forall e f g cols rows.
(e -> f -> g)
-> Matrix e cols rows -> Matrix f cols rows -> Matrix g cols rows
zipWithM e -> f -> g
f Matrix e cols b
b Matrix f cols b
Matrix f cols b
d)
zipWithM e -> f -> g
f x :: Matrix e cols rows
x@(Fork Matrix e cols a
_ Matrix e cols b
_) y :: Matrix f cols rows
y@(Join Matrix f a rows
_ Matrix f b rows
_) = (e -> f -> g)
-> Matrix e cols rows -> Matrix f cols rows -> Matrix g cols rows
forall e f g cols rows.
(e -> f -> g)
-> Matrix e cols rows -> Matrix f cols rows -> Matrix g cols rows
zipWithM e -> f -> g
f Matrix e cols rows
x (Matrix f cols rows -> Matrix f cols rows
forall e cols rows. Matrix e cols rows -> Matrix e cols rows
abideJF Matrix f cols rows
y)
zipWithM e -> f -> g
f x :: Matrix e cols rows
x@(Join Matrix e a rows
_ Matrix e b rows
_) y :: Matrix f cols rows
y@(Fork Matrix f cols a
_ Matrix f cols b
_) = (e -> f -> g)
-> Matrix e cols rows -> Matrix f cols rows -> Matrix g cols rows
forall e f g cols rows.
(e -> f -> g)
-> Matrix e cols rows -> Matrix f cols rows -> Matrix g cols rows
zipWithM e -> f -> g
f (Matrix e cols rows -> Matrix e cols rows
forall e cols rows. Matrix e cols rows -> Matrix e cols rows
abideJF Matrix e cols rows
x) Matrix f cols rows
y

-- Relational operators functions

type Boolean      = Natural 0 1
type Relation a b = Matrix Boolean a b

-- | Helper conversion function
toBool :: (Num e, Eq e) => e -> Bool
toBool :: e -> Bool
toBool e
n
  | e
n e -> e -> Bool
forall a. Eq a => a -> a -> Bool
== e
0 = Bool
False
  | e
n e -> e -> Bool
forall a. Eq a => a -> a -> Bool
== e
1 = Bool
True

-- | Helper conversion function
fromBool :: Bool -> Natural 0 1
fromBool :: Bool -> Natural 0 1
fromBool Bool
True  = Int -> Natural 0 1
forall (n :: Nat) (m :: Nat).
(KnownNat n, KnownNat m) =>
Int -> Natural n m
nat Int
1
fromBool Bool
False = Int -> Natural 0 1
forall (n :: Nat) (m :: Nat).
(KnownNat n, KnownNat m) =>
Int -> Natural n m
nat Int
0

-- | Relational negation
negateM :: Relation cols rows -> Relation cols rows
negateM :: Relation cols rows -> Relation cols rows
negateM (One (Nat Int
p)) = Natural 0 1 -> Matrix (Natural 0 1) () ()
forall e. e -> Matrix e () ()
One (Int -> Natural 0 1
forall (start :: Nat) (end :: Nat). Int -> Natural start end
Nat (Int -> Int
forall a. Num a => a -> a
negate Int
p))
negateM (Join Matrix (Natural 0 1) a rows
a Matrix (Natural 0 1) b rows
b)    = Matrix (Natural 0 1) a rows
-> Matrix (Natural 0 1) b rows
-> Matrix (Natural 0 1) (Either a b) rows
forall e a rows b.
Matrix e a rows -> Matrix e b rows -> Matrix e (Either a b) rows
Join (Matrix (Natural 0 1) a rows -> Matrix (Natural 0 1) a rows
forall cols rows. Relation cols rows -> Relation cols rows
negateM Matrix (Natural 0 1) a rows
a) (Matrix (Natural 0 1) b rows -> Matrix (Natural 0 1) b rows
forall cols rows. Relation cols rows -> Relation cols rows
negateM Matrix (Natural 0 1) b rows
b)
negateM (Fork Matrix (Natural 0 1) cols a
a Matrix (Natural 0 1) cols b
b)    = Matrix (Natural 0 1) cols a
-> Matrix (Natural 0 1) cols b
-> Matrix (Natural 0 1) cols (Either a b)
forall e cols a b.
Matrix e cols a -> Matrix e cols b -> Matrix e cols (Either a b)
Fork (Matrix (Natural 0 1) cols a -> Matrix (Natural 0 1) cols a
forall cols rows. Relation cols rows -> Relation cols rows
negateM Matrix (Natural 0 1) cols a
a) (Matrix (Natural 0 1) cols b -> Matrix (Natural 0 1) cols b
forall cols rows. Relation cols rows -> Relation cols rows
negateM Matrix (Natural 0 1) cols b
b)

-- | Relational addition
orM :: Relation cols rows -> Relation cols rows -> Relation cols rows
orM :: Relation cols rows -> Relation cols rows -> Relation cols rows
orM (One Natural 0 1
a) (One Natural 0 1
b)           = Natural 0 1 -> Matrix (Natural 0 1) () ()
forall e. e -> Matrix e () ()
One (Bool -> Natural 0 1
fromBool (Natural 0 1 -> Bool
forall e. (Num e, Eq e) => e -> Bool
toBool Natural 0 1
a Bool -> Bool -> Bool
|| Natural 0 1 -> Bool
forall e. (Num e, Eq e) => e -> Bool
toBool Natural 0 1
b))
orM (Join Matrix (Natural 0 1) a rows
a Matrix (Natural 0 1) b rows
b) (Join Matrix (Natural 0 1) a rows
c Matrix (Natural 0 1) b rows
d)     = Matrix (Natural 0 1) a rows
-> Matrix (Natural 0 1) b rows
-> Matrix (Natural 0 1) (Either a b) rows
forall e a rows b.
Matrix e a rows -> Matrix e b rows -> Matrix e (Either a b) rows
Join (Matrix (Natural 0 1) a rows
-> Matrix (Natural 0 1) a rows -> Matrix (Natural 0 1) a rows
forall cols rows.
Relation cols rows -> Relation cols rows -> Relation cols rows
orM Matrix (Natural 0 1) a rows
a Matrix (Natural 0 1) a rows
Matrix (Natural 0 1) a rows
c) (Matrix (Natural 0 1) b rows
-> Matrix (Natural 0 1) b rows -> Matrix (Natural 0 1) b rows
forall cols rows.
Relation cols rows -> Relation cols rows -> Relation cols rows
orM Matrix (Natural 0 1) b rows
b Matrix (Natural 0 1) b rows
Matrix (Natural 0 1) b rows
d)
orM (Fork Matrix (Natural 0 1) cols a
a Matrix (Natural 0 1) cols b
b) (Fork Matrix (Natural 0 1) cols a
c Matrix (Natural 0 1) cols b
d)     = Matrix (Natural 0 1) cols a
-> Matrix (Natural 0 1) cols b
-> Matrix (Natural 0 1) cols (Either a b)
forall e cols a b.
Matrix e cols a -> Matrix e cols b -> Matrix e cols (Either a b)
Fork (Matrix (Natural 0 1) cols a
-> Matrix (Natural 0 1) cols a -> Matrix (Natural 0 1) cols a
forall cols rows.
Relation cols rows -> Relation cols rows -> Relation cols rows
orM Matrix (Natural 0 1) cols a
a Matrix (Natural 0 1) cols a
Matrix (Natural 0 1) cols a
c) (Matrix (Natural 0 1) cols b
-> Matrix (Natural 0 1) cols b -> Matrix (Natural 0 1) cols b
forall cols rows.
Relation cols rows -> Relation cols rows -> Relation cols rows
orM Matrix (Natural 0 1) cols b
b Matrix (Natural 0 1) cols b
Matrix (Natural 0 1) cols b
d)
orM x :: Relation cols rows
x@(Fork Matrix (Natural 0 1) cols a
_ Matrix (Natural 0 1) cols b
_) y :: Relation cols rows
y@(Join Matrix (Natural 0 1) a rows
_ Matrix (Natural 0 1) b rows
_) = Relation cols rows -> Relation cols rows -> Relation cols rows
forall cols rows.
Relation cols rows -> Relation cols rows -> Relation cols rows
orM Relation cols rows
x (Relation cols rows -> Relation cols rows
forall e cols rows. Matrix e cols rows -> Matrix e cols rows
abideJF Relation cols rows
y)
orM x :: Relation cols rows
x@(Join Matrix (Natural 0 1) a rows
_ Matrix (Natural 0 1) b rows
_) y :: Relation cols rows
y@(Fork Matrix (Natural 0 1) cols a
_ Matrix (Natural 0 1) cols b
_) = Relation cols rows -> Relation cols rows -> Relation cols rows
forall cols rows.
Relation cols rows -> Relation cols rows -> Relation cols rows
orM (Relation cols rows -> Relation cols rows
forall e cols rows. Matrix e cols rows -> Matrix e cols rows
abideJF Relation cols rows
x) Relation cols rows
y

-- | Relational multiplication
andM :: Relation cols rows -> Relation cols rows -> Relation cols rows
andM :: Relation cols rows -> Relation cols rows -> Relation cols rows
andM (One Natural 0 1
a) (One Natural 0 1
b)           = Natural 0 1 -> Matrix (Natural 0 1) () ()
forall e. e -> Matrix e () ()
One (Bool -> Natural 0 1
fromBool (Natural 0 1 -> Bool
forall e. (Num e, Eq e) => e -> Bool
toBool Natural 0 1
a Bool -> Bool -> Bool
&& Natural 0 1 -> Bool
forall e. (Num e, Eq e) => e -> Bool
toBool Natural 0 1
b))
andM (Join Matrix (Natural 0 1) a rows
a Matrix (Natural 0 1) b rows
b) (Join Matrix (Natural 0 1) a rows
c Matrix (Natural 0 1) b rows
d)     = Matrix (Natural 0 1) a rows
-> Matrix (Natural 0 1) b rows
-> Matrix (Natural 0 1) (Either a b) rows
forall e a rows b.
Matrix e a rows -> Matrix e b rows -> Matrix e (Either a b) rows
Join (Matrix (Natural 0 1) a rows
-> Matrix (Natural 0 1) a rows -> Matrix (Natural 0 1) a rows
forall cols rows.
Relation cols rows -> Relation cols rows -> Relation cols rows
andM Matrix (Natural 0 1) a rows
a Matrix (Natural 0 1) a rows
Matrix (Natural 0 1) a rows
c) (Matrix (Natural 0 1) b rows
-> Matrix (Natural 0 1) b rows -> Matrix (Natural 0 1) b rows
forall cols rows.
Relation cols rows -> Relation cols rows -> Relation cols rows
andM Matrix (Natural 0 1) b rows
b Matrix (Natural 0 1) b rows
Matrix (Natural 0 1) b rows
d)
andM (Fork Matrix (Natural 0 1) cols a
a Matrix (Natural 0 1) cols b
b) (Fork Matrix (Natural 0 1) cols a
c Matrix (Natural 0 1) cols b
d)     = Matrix (Natural 0 1) cols a
-> Matrix (Natural 0 1) cols b
-> Matrix (Natural 0 1) cols (Either a b)
forall e cols a b.
Matrix e cols a -> Matrix e cols b -> Matrix e cols (Either a b)
Fork (Matrix (Natural 0 1) cols a
-> Matrix (Natural 0 1) cols a -> Matrix (Natural 0 1) cols a
forall cols rows.
Relation cols rows -> Relation cols rows -> Relation cols rows
andM Matrix (Natural 0 1) cols a
a Matrix (Natural 0 1) cols a
Matrix (Natural 0 1) cols a
c) (Matrix (Natural 0 1) cols b
-> Matrix (Natural 0 1) cols b -> Matrix (Natural 0 1) cols b
forall cols rows.
Relation cols rows -> Relation cols rows -> Relation cols rows
andM Matrix (Natural 0 1) cols b
b Matrix (Natural 0 1) cols b
Matrix (Natural 0 1) cols b
d)
andM x :: Relation cols rows
x@(Fork Matrix (Natural 0 1) cols a
_ Matrix (Natural 0 1) cols b
_) y :: Relation cols rows
y@(Join Matrix (Natural 0 1) a rows
_ Matrix (Natural 0 1) b rows
_) = Relation cols rows -> Relation cols rows -> Relation cols rows
forall cols rows.
Relation cols rows -> Relation cols rows -> Relation cols rows
andM Relation cols rows
x (Relation cols rows -> Relation cols rows
forall e cols rows. Matrix e cols rows -> Matrix e cols rows
abideJF Relation cols rows
y)
andM x :: Relation cols rows
x@(Join Matrix (Natural 0 1) a rows
_ Matrix (Natural 0 1) b rows
_) y :: Relation cols rows
y@(Fork Matrix (Natural 0 1) cols a
_ Matrix (Natural 0 1) cols b
_) = Relation cols rows -> Relation cols rows -> Relation cols rows
forall cols rows.
Relation cols rows -> Relation cols rows -> Relation cols rows
andM (Relation cols rows -> Relation cols rows
forall e cols rows. Matrix e cols rows -> Matrix e cols rows
abideJF Relation cols rows
x) Relation cols rows
y

-- | Relational subtraction
subM :: Relation cols rows -> Relation cols rows -> Relation cols rows
subM :: Relation cols rows -> Relation cols rows -> Relation cols rows
subM (One Natural 0 1
a) (One Natural 0 1
b)           = if Natural 0 1
a Natural 0 1 -> Natural 0 1 -> Natural 0 1
forall a. Num a => a -> a -> a
- Natural 0 1
b Natural 0 1 -> Natural 0 1 -> Bool
forall a. Ord a => a -> a -> Bool
< Int -> Natural 0 1
forall (n :: Nat) (m :: Nat).
(KnownNat n, KnownNat m) =>
Int -> Natural n m
nat Int
0 then Natural 0 1 -> Matrix (Natural 0 1) () ()
forall e. e -> Matrix e () ()
One (Int -> Natural 0 1
forall (n :: Nat) (m :: Nat).
(KnownNat n, KnownNat m) =>
Int -> Natural n m
nat Int
0) else Natural 0 1 -> Matrix (Natural 0 1) () ()
forall e. e -> Matrix e () ()
One (Natural 0 1
a Natural 0 1 -> Natural 0 1 -> Natural 0 1
forall a. Num a => a -> a -> a
- Natural 0 1
b)
subM (Join Matrix (Natural 0 1) a rows
a Matrix (Natural 0 1) b rows
b) (Join Matrix (Natural 0 1) a rows
c Matrix (Natural 0 1) b rows
d)     = Matrix (Natural 0 1) a rows
-> Matrix (Natural 0 1) b rows
-> Matrix (Natural 0 1) (Either a b) rows
forall e a rows b.
Matrix e a rows -> Matrix e b rows -> Matrix e (Either a b) rows
Join (Matrix (Natural 0 1) a rows
-> Matrix (Natural 0 1) a rows -> Matrix (Natural 0 1) a rows
forall cols rows.
Relation cols rows -> Relation cols rows -> Relation cols rows
subM Matrix (Natural 0 1) a rows
a Matrix (Natural 0 1) a rows
Matrix (Natural 0 1) a rows
c) (Matrix (Natural 0 1) b rows
-> Matrix (Natural 0 1) b rows -> Matrix (Natural 0 1) b rows
forall cols rows.
Relation cols rows -> Relation cols rows -> Relation cols rows
subM Matrix (Natural 0 1) b rows
b Matrix (Natural 0 1) b rows
Matrix (Natural 0 1) b rows
d)
subM (Fork Matrix (Natural 0 1) cols a
a Matrix (Natural 0 1) cols b
b) (Fork Matrix (Natural 0 1) cols a
c Matrix (Natural 0 1) cols b
d)     = Matrix (Natural 0 1) cols a
-> Matrix (Natural 0 1) cols b
-> Matrix (Natural 0 1) cols (Either a b)
forall e cols a b.
Matrix e cols a -> Matrix e cols b -> Matrix e cols (Either a b)
Fork (Matrix (Natural 0 1) cols a
-> Matrix (Natural 0 1) cols a -> Matrix (Natural 0 1) cols a
forall cols rows.
Relation cols rows -> Relation cols rows -> Relation cols rows
subM Matrix (Natural 0 1) cols a
a Matrix (Natural 0 1) cols a
Matrix (Natural 0 1) cols a
c) (Matrix (Natural 0 1) cols b
-> Matrix (Natural 0 1) cols b -> Matrix (Natural 0 1) cols b
forall cols rows.
Relation cols rows -> Relation cols rows -> Relation cols rows
subM Matrix (Natural 0 1) cols b
b Matrix (Natural 0 1) cols b
Matrix (Natural 0 1) cols b
d)
subM x :: Relation cols rows
x@(Fork Matrix (Natural 0 1) cols a
_ Matrix (Natural 0 1) cols b
_) y :: Relation cols rows
y@(Join Matrix (Natural 0 1) a rows
_ Matrix (Natural 0 1) b rows
_) = Relation cols rows -> Relation cols rows -> Relation cols rows
forall cols rows.
Relation cols rows -> Relation cols rows -> Relation cols rows
subM Relation cols rows
x (Relation cols rows -> Relation cols rows
forall e cols rows. Matrix e cols rows -> Matrix e cols rows
abideJF Relation cols rows
y)
subM x :: Relation cols rows
x@(Join Matrix (Natural 0 1) a rows
_ Matrix (Natural 0 1) b rows
_) y :: Relation cols rows
y@(Fork Matrix (Natural 0 1) cols a
_ Matrix (Natural 0 1) cols b
_) = Relation cols rows -> Relation cols rows -> Relation cols rows
forall cols rows.
Relation cols rows -> Relation cols rows -> Relation cols rows
subM (Relation cols rows -> Relation cols rows
forall e cols rows. Matrix e cols rows -> Matrix e cols rows
abideJF Relation cols rows
x) Relation cols rows
y

-- | Matrix relational composition.
compRel :: Relation cr rows -> Relation cols cr -> Relation cols rows
compRel :: Relation cr rows -> Relation cols cr -> Relation cols rows
compRel (One Natural 0 1
a) (One Natural 0 1
b)       = Natural 0 1 -> Matrix (Natural 0 1) () ()
forall e. e -> Matrix e () ()
One (Bool -> Natural 0 1
fromBool (Natural 0 1 -> Bool
forall e. (Num e, Eq e) => e -> Bool
toBool Natural 0 1
a Bool -> Bool -> Bool
&& Natural 0 1 -> Bool
forall e. (Num e, Eq e) => e -> Bool
toBool Natural 0 1
b))
compRel (Join Matrix (Natural 0 1) a rows
a Matrix (Natural 0 1) b rows
b) (Fork Matrix (Natural 0 1) cols a
c Matrix (Natural 0 1) cols b
d) = Relation cols rows -> Relation cols rows -> Relation cols rows
forall cols rows.
Relation cols rows -> Relation cols rows -> Relation cols rows
orM (Matrix (Natural 0 1) a rows
-> Relation cols a -> Relation cols rows
forall cr rows cols.
Relation cr rows -> Relation cols cr -> Relation cols rows
compRel Matrix (Natural 0 1) a rows
a Relation cols a
Matrix (Natural 0 1) cols a
c) (Matrix (Natural 0 1) b rows
-> Relation cols b -> Relation cols rows
forall cr rows cols.
Relation cr rows -> Relation cols cr -> Relation cols rows
compRel Matrix (Natural 0 1) b rows
b Relation cols b
Matrix (Natural 0 1) cols b
d)   -- Divide-and-conquer law
compRel (Fork Matrix (Natural 0 1) cr a
a Matrix (Natural 0 1) cr b
b) Relation cols cr
c          = Matrix (Natural 0 1) cols a
-> Matrix (Natural 0 1) cols b
-> Matrix (Natural 0 1) cols (Either a b)
forall e cols a b.
Matrix e cols a -> Matrix e cols b -> Matrix e cols (Either a b)
Fork (Matrix (Natural 0 1) cr a
-> Relation cols cr -> Matrix (Natural 0 1) cols a
forall cr rows cols.
Relation cr rows -> Relation cols cr -> Relation cols rows
compRel Matrix (Natural 0 1) cr a
a Relation cols cr
c) (Matrix (Natural 0 1) cr b
-> Relation cols cr -> Matrix (Natural 0 1) cols b
forall cr rows cols.
Relation cr rows -> Relation cols cr -> Relation cols rows
compRel Matrix (Natural 0 1) cr b
b Relation cols cr
c) -- Fork fusion law
compRel Relation cr rows
c (Join Matrix (Natural 0 1) a cr
a Matrix (Natural 0 1) b cr
b)          = Matrix (Natural 0 1) a rows
-> Matrix (Natural 0 1) b rows
-> Matrix (Natural 0 1) (Either a b) rows
forall e a rows b.
Matrix e a rows -> Matrix e b rows -> Matrix e (Either a b) rows
Join (Relation cr rows
-> Matrix (Natural 0 1) a cr -> Matrix (Natural 0 1) a rows
forall cr rows cols.
Relation cr rows -> Relation cols cr -> Relation cols rows
compRel Relation cr rows
c Matrix (Natural 0 1) a cr
a) (Relation cr rows
-> Matrix (Natural 0 1) b cr -> Matrix (Natural 0 1) b rows
forall cr rows cols.
Relation cr rows -> Relation cols cr -> Relation cols rows
compRel Relation cr rows
c Matrix (Natural 0 1) b cr
b)  -- Join fusion law

-- | Matrix relational right division
divR :: Relation b c -> Relation b a -> Relation a c
divR :: Relation b c -> Relation b a -> Relation a c
divR (One Natural 0 1
a) (One Natural 0 1
b)       = Natural 0 1 -> Matrix (Natural 0 1) () ()
forall e. e -> Matrix e () ()
One (Bool -> Natural 0 1
fromBool (Bool -> Bool
not (Natural 0 1 -> Bool
forall e. (Num e, Eq e) => e -> Bool
toBool Natural 0 1
b) Bool -> Bool -> Bool
|| Natural 0 1 -> Bool
forall e. (Num e, Eq e) => e -> Bool
toBool Natural 0 1
a)) -- b implies a
divR (Join Matrix (Natural 0 1) a c
a Matrix (Natural 0 1) b c
b) (Join Matrix (Natural 0 1) a a
c Matrix (Natural 0 1) b a
d) = Relation a c -> Relation a c -> Relation a c
forall cols rows.
Relation cols rows -> Relation cols rows -> Relation cols rows
andM (Matrix (Natural 0 1) a c -> Relation a a -> Relation a c
forall b c a. Relation b c -> Relation b a -> Relation a c
divR Matrix (Natural 0 1) a c
a Relation a a
Matrix (Natural 0 1) a a
c) (Matrix (Natural 0 1) b c -> Relation b a -> Relation a c
forall b c a. Relation b c -> Relation b a -> Relation a c
divR Matrix (Natural 0 1) b c
b Relation b a
Matrix (Natural 0 1) b a
d)
divR (Fork Matrix (Natural 0 1) b a
a Matrix (Natural 0 1) b b
b) Relation b a
c          = Matrix (Natural 0 1) a a
-> Matrix (Natural 0 1) a b -> Matrix (Natural 0 1) a (Either a b)
forall e cols a b.
Matrix e cols a -> Matrix e cols b -> Matrix e cols (Either a b)
Fork (Matrix (Natural 0 1) b a
-> Relation b a -> Matrix (Natural 0 1) a a
forall b c a. Relation b c -> Relation b a -> Relation a c
divR Matrix (Natural 0 1) b a
a Relation b a
c) (Matrix (Natural 0 1) b b
-> Relation b a -> Matrix (Natural 0 1) a b
forall b c a. Relation b c -> Relation b a -> Relation a c
divR Matrix (Natural 0 1) b b
b Relation b a
c)
divR Relation b c
c (Fork Matrix (Natural 0 1) b a
a Matrix (Natural 0 1) b b
b)          = Matrix (Natural 0 1) a c
-> Matrix (Natural 0 1) b c -> Matrix (Natural 0 1) (Either a b) c
forall e a rows b.
Matrix e a rows -> Matrix e b rows -> Matrix e (Either a b) rows
Join (Relation b c
-> Matrix (Natural 0 1) b a -> Matrix (Natural 0 1) a c
forall b c a. Relation b c -> Relation b a -> Relation a c
divR Relation b c
c Matrix (Natural 0 1) b a
a) (Relation b c
-> Matrix (Natural 0 1) b b -> Matrix (Natural 0 1) b c
forall b c a. Relation b c -> Relation b a -> Relation a c
divR Relation b c
c Matrix (Natural 0 1) b b
b)

-- | Matrix relational left division
divL :: Relation c b -> Relation a b -> Relation a c
divL :: Relation c b -> Relation a b -> Relation a c
divL Relation c b
x Relation a b
y = Matrix (Natural 0 1) c a -> Relation a c
forall e cols rows. Matrix e cols rows -> Matrix e rows cols
tr (Relation b a -> Relation b c -> Matrix (Natural 0 1) c a
forall b c a. Relation b c -> Relation b a -> Relation a c
divR (Relation a b -> Relation b a
forall e cols rows. Matrix e cols rows -> Matrix e rows cols
tr Relation a b
y) (Relation c b -> Relation b c
forall e cols rows. Matrix e cols rows -> Matrix e rows cols
tr Relation c b
x))

-- | Matrix relational symmetric division
divS :: Relation c a -> Relation b a -> Relation c b
divS :: Relation c a -> Relation b a -> Relation c b
divS Relation c a
s Relation b a
r = Relation b a -> Relation c a -> Relation c b
forall c b a. Relation c b -> Relation a b -> Relation a c
divL Relation b a
r Relation c a
s Relation c b -> Relation c b -> Relation c b
forall cols rows.
Relation cols rows -> Relation cols rows -> Relation cols rows
`intersection` Relation a b -> Relation a c -> Relation c b
forall b c a. Relation b c -> Relation b a -> Relation a c
divR (Relation b a -> Relation a b
forall e cols rows. Matrix e cols rows -> Matrix e rows cols
tr Relation b a
r) (Relation c a -> Relation a c
forall e cols rows. Matrix e cols rows -> Matrix e rows cols
tr Relation c a
s)
  where
    intersection :: Relation cols rows -> Relation cols rows -> Relation cols rows
intersection = Relation cols rows -> Relation cols rows -> Relation cols rows
forall cols rows.
Relation cols rows -> Relation cols rows -> Relation cols rows
andM

-- | Lifts functions to relations with arbitrary dimensions.
--
--   NOTE: Be careful to not ask for a relation bigger than the cardinality of
-- types @a@ or @b@ allows.
fromFRel' ::
  forall a b cols rows.
  ( Liftable Boolean a b,
    CountableDims cols rows,
    FL rows cols
  ) =>
  (a -> b) ->
  Relation cols rows
fromFRel' :: (a -> b) -> Relation cols rows
fromFRel' a -> b
f =
  let minA :: a
minA         = Bounded a => a
forall a. Bounded a => a
minBound @a
      maxA :: a
maxA         = Bounded a => a
forall a. Bounded a => a
maxBound @a
      minB :: b
minB         = Bounded b => b
forall a. Bounded a => a
minBound @b
      maxB :: b
maxB         = Bounded b => b
forall a. Bounded a => a
maxBound @b
      ccols :: Int
ccols        = Integer -> Int
forall a. Num a => Integer -> a
fromInteger (Integer -> Int) -> Integer -> Int
forall a b. (a -> b) -> a -> b
$ Proxy (Count cols) -> Integer
forall (n :: Nat) (proxy :: Nat -> Type).
KnownNat n =>
proxy n -> Integer
natVal (Proxy (Count cols)
forall k (t :: k). Proxy t
Proxy :: Proxy (Count cols))
      rrows :: Int
rrows        = Integer -> Int
forall a. Num a => Integer -> a
fromInteger (Integer -> Int) -> Integer -> Int
forall a b. (a -> b) -> a -> b
$ Proxy (Count rows) -> Integer
forall (n :: Nat) (proxy :: Nat -> Type).
KnownNat n =>
proxy n -> Integer
natVal (Proxy (Count rows)
forall k (t :: k). Proxy t
Proxy :: Proxy (Count rows))
      elementsA :: [a]
elementsA    = Int -> [a] -> [a]
forall a. Int -> [a] -> [a]
take Int
ccols [a
minA .. a
maxA]
      elementsB :: [b]
elementsB    = Int -> [b] -> [b]
forall a. Int -> [a] -> [a]
take Int
rrows [b
minB .. b
maxB]
      combinations :: [(a, b)]
combinations = (,) (a -> b -> (a, b)) -> [a] -> [b -> (a, b)]
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> [a]
elementsA [b -> (a, b)] -> [b] -> [(a, b)]
forall (f :: Type -> Type) a b.
Applicative f =>
f (a -> b) -> f a -> f b
<*> [b]
elementsB
      combAp :: [Natural 0 1]
combAp       = (((Int, Int), Natural 0 1) -> Natural 0 1)
-> [((Int, Int), Natural 0 1)] -> [Natural 0 1]
forall a b. (a -> b) -> [a] -> [b]
map ((Int, Int), Natural 0 1) -> Natural 0 1
forall a b. (a, b) -> b
snd ([((Int, Int), Natural 0 1)] -> [Natural 0 1])
-> ([((Int, Int), Natural 0 1)] -> [((Int, Int), Natural 0 1)])
-> [((Int, Int), Natural 0 1)]
-> [Natural 0 1]
forall (k :: Type -> Type -> Type) b c a.
Category k =>
k b c -> k a b -> k a c
. [((Int, Int), Natural 0 1)] -> [((Int, Int), Natural 0 1)]
forall a. Ord a => [a] -> [a]
sort ([((Int, Int), Natural 0 1)] -> [Natural 0 1])
-> ([(a, b)] -> [((Int, Int), Natural 0 1)])
-> [(a, b)]
-> [Natural 0 1]
forall (k :: Type -> Type -> Type) b c a.
Category k =>
k b c -> k a b -> k a c
. ((a, b) -> ((Int, Int), Natural 0 1))
-> [(a, b)] -> [((Int, Int), Natural 0 1)]
forall a b. (a -> b) -> [a] -> [b]
map (\(a
a, b
b) -> if a -> b
f a
a b -> b -> Bool
forall a. Eq a => a -> a -> Bool
== b
b
                                                         then ((a -> Int
forall a. Enum a => a -> Int
fromEnum a
a, b -> Int
forall a. Enum a => a -> Int
fromEnum b
b), Int -> Natural 0 1
forall (n :: Nat) (m :: Nat).
(KnownNat n, KnownNat m) =>
Int -> Natural n m
nat Int
1)
                                                         else ((a -> Int
forall a. Enum a => a -> Int
fromEnum a
a, b -> Int
forall a. Enum a => a -> Int
fromEnum b
b), Int -> Natural 0 1
forall (n :: Nat) (m :: Nat).
(KnownNat n, KnownNat m) =>
Int -> Natural n m
nat Int
0)) ([(a, b)] -> [Natural 0 1]) -> [(a, b)] -> [Natural 0 1]
forall a b. (a -> b) -> a -> b
$ [(a, b)]
combinations
      mList :: [[Natural 0 1]]
mList        = [Natural 0 1] -> Int -> [[Natural 0 1]]
forall a. [a] -> Int -> [[a]]
buildList [Natural 0 1]
combAp Int
rrows
   in Matrix (Natural 0 1) rows cols -> Relation cols rows
forall e cols rows. Matrix e cols rows -> Matrix e rows cols
tr (Matrix (Natural 0 1) rows cols -> Relation cols rows)
-> Matrix (Natural 0 1) rows cols -> Relation cols rows
forall a b. (a -> b) -> a -> b
$ [[Natural 0 1]] -> Matrix (Natural 0 1) rows cols
forall cols rows e.
FromLists cols rows =>
[[e]] -> Matrix e cols rows
fromLists [[Natural 0 1]]
mList
  where
    buildList :: [a] -> Int -> [[a]]
buildList [] Int
_ = []
    buildList [a]
l Int
r  = Int -> [a] -> [a]
forall a. Int -> [a] -> [a]
take Int
r [a]
l [a] -> [[a]] -> [[a]]
forall a. a -> [a] -> [a]
: [a] -> Int -> [[a]]
buildList (Int -> [a] -> [a]
forall a. Int -> [a] -> [a]
drop Int
r [a]
l) Int
r

-- | Lifts functions to relations with dimensions matching @a@ and @b@
-- cardinality's.
fromFRel ::
  forall a b.
  ( Liftable Boolean a b,
    CountableDimsN a b,
    FL (Normalize b) (Normalize a)
  ) =>
  (a -> b) ->
  Relation (Normalize a) (Normalize b)
fromFRel :: (a -> b) -> Relation (Normalize a) (Normalize b)
fromFRel a -> b
f =
  let minA :: a
minA         = Bounded a => a
forall a. Bounded a => a
minBound @a
      maxA :: a
maxA         = Bounded a => a
forall a. Bounded a => a
maxBound @a
      minB :: b
minB         = Bounded b => b
forall a. Bounded a => a
minBound @b
      maxB :: b
maxB         = Bounded b => b
forall a. Bounded a => a
maxBound @b
      ccols :: Int
ccols        = Integer -> Int
forall a. Num a => Integer -> a
fromInteger (Integer -> Int) -> Integer -> Int
forall a b. (a -> b) -> a -> b
$ Proxy (Count (Normalize a)) -> Integer
forall (n :: Nat) (proxy :: Nat -> Type).
KnownNat n =>
proxy n -> Integer
natVal (Proxy (Count (Normalize a))
forall k (t :: k). Proxy t
Proxy :: Proxy (Count (Normalize a)))
      rrows :: Int
rrows        = Integer -> Int
forall a. Num a => Integer -> a
fromInteger (Integer -> Int) -> Integer -> Int
forall a b. (a -> b) -> a -> b
$ Proxy (Count (Normalize b)) -> Integer
forall (n :: Nat) (proxy :: Nat -> Type).
KnownNat n =>
proxy n -> Integer
natVal (Proxy (Count (Normalize b))
forall k (t :: k). Proxy t
Proxy :: Proxy (Count (Normalize b)))
      elementsA :: [a]
elementsA    = Int -> [a] -> [a]
forall a. Int -> [a] -> [a]
take Int
ccols [a
minA .. a
maxA]
      elementsB :: [b]
elementsB    = Int -> [b] -> [b]
forall a. Int -> [a] -> [a]
take Int
rrows [b
minB .. b
maxB]
      combinations :: [(a, b)]
combinations = (,) (a -> b -> (a, b)) -> [a] -> [b -> (a, b)]
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> [a]
elementsA [b -> (a, b)] -> [b] -> [(a, b)]
forall (f :: Type -> Type) a b.
Applicative f =>
f (a -> b) -> f a -> f b
<*> [b]
elementsB
      combAp :: [Natural 0 1]
combAp       = (((Int, Int), Natural 0 1) -> Natural 0 1)
-> [((Int, Int), Natural 0 1)] -> [Natural 0 1]
forall a b. (a -> b) -> [a] -> [b]
map ((Int, Int), Natural 0 1) -> Natural 0 1
forall a b. (a, b) -> b
snd ([((Int, Int), Natural 0 1)] -> [Natural 0 1])
-> ([((Int, Int), Natural 0 1)] -> [((Int, Int), Natural 0 1)])
-> [((Int, Int), Natural 0 1)]
-> [Natural 0 1]
forall (k :: Type -> Type -> Type) b c a.
Category k =>
k b c -> k a b -> k a c
. [((Int, Int), Natural 0 1)] -> [((Int, Int), Natural 0 1)]
forall a. Ord a => [a] -> [a]
sort ([((Int, Int), Natural 0 1)] -> [Natural 0 1])
-> ([(a, b)] -> [((Int, Int), Natural 0 1)])
-> [(a, b)]
-> [Natural 0 1]
forall (k :: Type -> Type -> Type) b c a.
Category k =>
k b c -> k a b -> k a c
. ((a, b) -> ((Int, Int), Natural 0 1))
-> [(a, b)] -> [((Int, Int), Natural 0 1)]
forall a b. (a -> b) -> [a] -> [b]
map (\(a
a, b
b) -> if a -> b
f a
a b -> b -> Bool
forall a. Eq a => a -> a -> Bool
== b
b
                                                         then ((a -> Int
forall a. Enum a => a -> Int
fromEnum a
a, b -> Int
forall a. Enum a => a -> Int
fromEnum b
b), Int -> Natural 0 1
forall (n :: Nat) (m :: Nat).
(KnownNat n, KnownNat m) =>
Int -> Natural n m
nat Int
1)
                                                         else ((a -> Int
forall a. Enum a => a -> Int
fromEnum a
a, b -> Int
forall a. Enum a => a -> Int
fromEnum b
b), Int -> Natural 0 1
forall (n :: Nat) (m :: Nat).
(KnownNat n, KnownNat m) =>
Int -> Natural n m
nat Int
0)) ([(a, b)] -> [Natural 0 1]) -> [(a, b)] -> [Natural 0 1]
forall a b. (a -> b) -> a -> b
$ [(a, b)]
combinations
      mList :: [[Natural 0 1]]
mList        = [Natural 0 1] -> Int -> [[Natural 0 1]]
forall a. [a] -> Int -> [[a]]
buildList [Natural 0 1]
combAp Int
rrows
   in Matrix (Natural 0 1) (Normalize b) (Normalize a)
-> Relation (Normalize a) (Normalize b)
forall e cols rows. Matrix e cols rows -> Matrix e rows cols
tr (Matrix (Natural 0 1) (Normalize b) (Normalize a)
 -> Relation (Normalize a) (Normalize b))
-> Matrix (Natural 0 1) (Normalize b) (Normalize a)
-> Relation (Normalize a) (Normalize b)
forall a b. (a -> b) -> a -> b
$ [[Natural 0 1]] -> Matrix (Natural 0 1) (Normalize b) (Normalize a)
forall cols rows e.
FromLists cols rows =>
[[e]] -> Matrix e cols rows
fromLists [[Natural 0 1]]
mList
  where
    buildList :: [a] -> Int -> [[a]]
buildList [] Int
_ = []
    buildList [a]
l Int
r  = Int -> [a] -> [a]
forall a. Int -> [a] -> [a]
take Int
r [a]
l [a] -> [[a]] -> [[a]]
forall a. a -> [a] -> [a]
: [a] -> Int -> [[a]]
buildList (Int -> [a] -> [a]
forall a. Int -> [a] -> [a]
drop Int
r [a]
l) Int
r

-- | Lifts a relation function to a Boolean Matrix
toRel ::
      forall a b.
      ( Bounded a,
        Bounded b,
        Enum a,
        Enum b,
        Eq b,
        CountableDimsN a b,
        FLN b a
      )
      => (a -> b -> Bool) -> Relation (Normalize a) (Normalize b)
toRel :: (a -> b -> Bool) -> Relation (Normalize a) (Normalize b)
toRel a -> b -> Bool
f =
  let minA :: a
minA         = Bounded a => a
forall a. Bounded a => a
minBound @a
      maxA :: a
maxA         = Bounded a => a
forall a. Bounded a => a
maxBound @a
      minB :: b
minB         = Bounded b => b
forall a. Bounded a => a
minBound @b
      maxB :: b
maxB         = Bounded b => b
forall a. Bounded a => a
maxBound @b
      ccols :: Int
ccols        = Integer -> Int
forall a. Num a => Integer -> a
fromInteger (Integer -> Int) -> Integer -> Int
forall a b. (a -> b) -> a -> b
$ Proxy (Count (Normalize a)) -> Integer
forall (n :: Nat) (proxy :: Nat -> Type).
KnownNat n =>
proxy n -> Integer
natVal (Proxy (Count (Normalize a))
forall k (t :: k). Proxy t
Proxy :: Proxy (Count (Normalize a)))
      rrows :: Int
rrows        = Integer -> Int
forall a. Num a => Integer -> a
fromInteger (Integer -> Int) -> Integer -> Int
forall a b. (a -> b) -> a -> b
$ Proxy (Count (Normalize b)) -> Integer
forall (n :: Nat) (proxy :: Nat -> Type).
KnownNat n =>
proxy n -> Integer
natVal (Proxy (Count (Normalize b))
forall k (t :: k). Proxy t
Proxy :: Proxy (Count (Normalize b)))
      elementsA :: [a]
elementsA    = Int -> [a] -> [a]
forall a. Int -> [a] -> [a]
take Int
ccols [a
minA .. a
maxA]
      elementsB :: [b]
elementsB    = Int -> [b] -> [b]
forall a. Int -> [a] -> [a]
take Int
rrows [b
minB .. b
maxB]
      combinations :: [(a, b)]
combinations = (,) (a -> b -> (a, b)) -> [a] -> [b -> (a, b)]
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> [a]
elementsA [b -> (a, b)] -> [b] -> [(a, b)]
forall (f :: Type -> Type) a b.
Applicative f =>
f (a -> b) -> f a -> f b
<*> [b]
elementsB
      combAp :: [Natural 0 1]
combAp       = (((Int, Int), Natural 0 1) -> Natural 0 1)
-> [((Int, Int), Natural 0 1)] -> [Natural 0 1]
forall a b. (a -> b) -> [a] -> [b]
map ((Int, Int), Natural 0 1) -> Natural 0 1
forall a b. (a, b) -> b
snd ([((Int, Int), Natural 0 1)] -> [Natural 0 1])
-> ([((Int, Int), Natural 0 1)] -> [((Int, Int), Natural 0 1)])
-> [((Int, Int), Natural 0 1)]
-> [Natural 0 1]
forall (k :: Type -> Type -> Type) b c a.
Category k =>
k b c -> k a b -> k a c
. [((Int, Int), Natural 0 1)] -> [((Int, Int), Natural 0 1)]
forall a. Ord a => [a] -> [a]
sort ([((Int, Int), Natural 0 1)] -> [Natural 0 1])
-> ([(a, b)] -> [((Int, Int), Natural 0 1)])
-> [(a, b)]
-> [Natural 0 1]
forall (k :: Type -> Type -> Type) b c a.
Category k =>
k b c -> k a b -> k a c
. ((a, b) -> ((Int, Int), Natural 0 1))
-> [(a, b)] -> [((Int, Int), Natural 0 1)]
forall a b. (a -> b) -> [a] -> [b]
map (\(a
a, b
b) -> if (a -> b -> Bool) -> (a, b) -> Bool
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry a -> b -> Bool
f (a
a, b
b)
                                                         then ((a -> Int
forall a. Enum a => a -> Int
fromEnum a
a, b -> Int
forall a. Enum a => a -> Int
fromEnum b
b), Int -> Natural 0 1
forall (n :: Nat) (m :: Nat).
(KnownNat n, KnownNat m) =>
Int -> Natural n m
nat Int
1)
                                                         else ((a -> Int
forall a. Enum a => a -> Int
fromEnum a
a, b -> Int
forall a. Enum a => a -> Int
fromEnum b
b), Int -> Natural 0 1
forall (n :: Nat) (m :: Nat).
(KnownNat n, KnownNat m) =>
Int -> Natural n m
nat Int
0)) ([(a, b)] -> [Natural 0 1]) -> [(a, b)] -> [Natural 0 1]
forall a b. (a -> b) -> a -> b
$ [(a, b)]
combinations
      mList :: [[Natural 0 1]]
mList        = [Natural 0 1] -> Int -> [[Natural 0 1]]
forall a. [a] -> Int -> [[a]]
buildList [Natural 0 1]
combAp Int
rrows
   in Matrix (Natural 0 1) (Normalize b) (Normalize a)
-> Relation (Normalize a) (Normalize b)
forall e cols rows. Matrix e cols rows -> Matrix e rows cols
tr (Matrix (Natural 0 1) (Normalize b) (Normalize a)
 -> Relation (Normalize a) (Normalize b))
-> Matrix (Natural 0 1) (Normalize b) (Normalize a)
-> Relation (Normalize a) (Normalize b)
forall a b. (a -> b) -> a -> b
$ [[Natural 0 1]] -> Matrix (Natural 0 1) (Normalize b) (Normalize a)
forall cols rows e.
FromLists cols rows =>
[[e]] -> Matrix e cols rows
fromLists [[Natural 0 1]]
mList
  where
    buildList :: [a] -> Int -> [[a]]
buildList [] Int
_ = []
    buildList [a]
l Int
r  = Int -> [a] -> [a]
forall a. Int -> [a] -> [a]
take Int
r [a]
l [a] -> [[a]] -> [[a]]
forall a. a -> [a] -> [a]
: [a] -> Int -> [[a]]
buildList (Int -> [a] -> [a]
forall a. Int -> [a] -> [a]
drop Int
r [a]
l) Int
r