{-# 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 (..),

    -- * Primitives
    empty,
    one,
    junc,
    split,

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

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

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

    -- ** Matrix Transposition
    tr,

    -- ** Selective operator
    select,
    branch,

    -- ** McCarthy's Conditional
    cond,

    -- ** Matrix "abiding"
    abideJS,
    abideSJ,

    -- ** Zip matrices
    zipWithM,

    -- * Biproduct approach
    -- ** Split
    (===),
    -- *** Projections
    p1,
    p2,
    -- ** Junc
    (|||),
    -- *** 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
    kp1,
    kp2,

    -- *** Matrix pairing
    khatri,

    -- * 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.
    identity,
    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.Void
import GHC.TypeLits
import Data.Type.Equality
import GHC.Generics
import Control.DeepSeq
import Control.Category
import Prelude hiding ((.))

-- | LAoP (Linear Algebra of Programming) Inductive Matrix definition.
data Matrix e cols rows where
  Empty :: Matrix e Void Void
  One :: e -> Matrix e () ()
  Junc :: Matrix e a rows -> Matrix e b rows -> Matrix e (Either a b) rows
  Split :: 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 0 = Void
  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 CountableDimensions a b = (Countable a, Countable b)
type CountableDimensionsN a b = (CountableN a, CountableN b)
type FromListsN e a b = FromLists e (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 isn't possible to implement the 'id' function so it's
-- implementation is 'undefined'. However 'comp' can be and this partial
-- class implementation exists just to make the code more readable.
--
-- Please use 'identity' instead.
instance (Num e) => Category (Matrix e) where
    id :: Matrix e a a
id = Matrix e a a
forall a. HasCallStack => a
undefined
    . :: 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 Empty = ()
    rnf (One e :: e
e) = e -> ()
forall a. NFData a => a -> ()
rnf e
e
    rnf (Junc a :: Matrix e a rows
a b :: Matrix e b rows
b) = Matrix e a rows -> ()
forall a. NFData a => a -> ()
rnf Matrix e a rows
a () -> () -> ()
forall a b. a -> b -> b
`seq` Matrix e b rows -> ()
forall a. NFData a => a -> ()
rnf Matrix e b rows
b
    rnf (Split a :: Matrix e cols a
a b :: Matrix e cols b
b) = Matrix e cols a -> ()
forall a. NFData a => a -> ()
rnf Matrix e cols a
a () -> () -> ()
forall a b. a -> b -> b
`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
  Empty == :: Matrix e cols rows -> Matrix e cols rows -> Bool
== Empty                = Bool
True
  (One a :: e
a) == (One b :: e
b)            = e
a e -> e -> Bool
forall a. Eq a => a -> a -> Bool
== e
b
  (Junc a :: Matrix e a rows
a b :: Matrix e b rows
b) == (Junc c :: Matrix e a rows
c d :: 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
  (Split a :: Matrix e cols a
a b :: Matrix e cols b
b) == (Split c :: Matrix e cols a
c d :: 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@(Split _ _) == y :: Matrix e cols rows
y@(Junc _ _) = 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
abideJS Matrix e cols rows
y
  x :: Matrix e cols rows
x@(Junc _ _) == y :: Matrix e cols rows
y@(Split _ _) = Matrix e cols rows -> Matrix e cols rows
forall e cols rows. Matrix e cols rows -> Matrix e cols rows
abideJS 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

  a :: Matrix e cols rows
a + :: Matrix e cols rows -> Matrix e cols rows -> Matrix e cols rows
+ b :: 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

  a :: Matrix e cols rows
a - :: Matrix e cols rows -> Matrix e cols rows -> Matrix e cols rows
- b :: 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

  a :: Matrix e cols rows
a * :: Matrix e cols rows -> Matrix e cols rows -> Matrix e cols rows
* b :: 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 Empty       = Matrix e cols rows
forall e. Matrix e Void Void
Empty
  abs (One a :: e
a)     = e -> Matrix e () ()
forall e. e -> Matrix e () ()
One (e -> e
forall a. Num a => a -> a
abs e
a)
  abs (Junc a :: Matrix e a rows
a b :: 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
Junc (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 (Split a :: Matrix e cols a
a b :: 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)
Split (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 Empty       = Matrix e cols rows
forall e. Matrix e Void Void
Empty
  signum (One a :: e
a)     = e -> Matrix e () ()
forall e. e -> Matrix e () ()
One (e -> e
forall a. Num a => a -> a
signum e
a)
  signum (Junc a :: Matrix e a rows
a b :: 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
Junc (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 (Split a :: Matrix e cols a
a b :: 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)
Split (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
    Empty <= :: Matrix e cols rows -> Matrix e cols rows -> Bool
<= Empty                = Bool
True
    (One a :: e
a) <= (One b :: e
b)            = e
a e -> e -> Bool
forall a. Ord a => a -> a -> Bool
<= e
b
    (Junc a :: Matrix e a rows
a b :: Matrix e b rows
b) <= (Junc c :: Matrix e a rows
c d :: 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)
    (Split a :: Matrix e cols a
a b :: Matrix e cols b
b) <= (Split c :: Matrix e cols a
c d :: 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@(Split _ _) <= y :: Matrix e cols rows
y@(Junc _ _) = 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
abideJS Matrix e cols rows
y
    x :: Matrix e cols rows
x@(Junc _ _) <= y :: Matrix e cols rows
y@(Split _ _) = Matrix e cols rows -> Matrix e cols rows
forall e cols rows. Matrix e cols rows -> Matrix e cols rows
abideJS 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

-- | Empty matrix constructor
empty :: Matrix e Void Void
empty :: Matrix e Void Void
empty = Matrix e Void Void
forall e. Matrix e Void Void
Empty

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

-- | Matrix 'Junc' constructor
junc :: Matrix e a rows -> Matrix e b rows -> Matrix e (Either a b) rows
junc :: Matrix e a rows -> Matrix e b rows -> Matrix e (Either a b) rows
junc = 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
Junc

infixl 3 |||

-- | Matrix 'Junc' 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
Junc

-- | Matrix 'Split' constructor
split :: Matrix e cols a -> Matrix e cols b -> Matrix e cols (Either a b)
split :: Matrix e cols a -> Matrix e cols b -> Matrix e cols (Either a b)
split = 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)
Split

infixl 2 ===

-- | Matrix 'Split' 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)
Split

-- 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 e 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 e Void Void where
  fromLists :: [[e]] -> Matrix e Void Void
fromLists [] = Matrix e Void Void
forall e. Matrix e Void Void
Empty
  fromLists _  = String -> Matrix e Void Void
forall a. HasCallStack => String -> a
error "Wrong dimensions"

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

instance {-# OVERLAPPING #-} (FromLists e cols ()) => FromLists e (Either () cols) () where
  fromLists :: [[e]] -> Matrix e (Either () cols) ()
fromLists [h :: e
h : t :: [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
Junc (e -> Matrix e () ()
forall e. e -> Matrix e () ()
One e
h) ([[e]] -> Matrix e cols ()
forall e cols rows.
FromLists e cols rows =>
[[e]] -> Matrix e cols rows
fromLists [[e]
t])
  fromLists _       = String -> Matrix e (Either () cols) ()
forall a. HasCallStack => String -> a
error "Wrong dimensions"

instance {-# OVERLAPPABLE #-} (FromLists e a (), FromLists e b (), Countable a) => FromLists e (Either a b) () where
  fromLists :: [[e]] -> Matrix e (Either a b) ()
fromLists [l :: [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
Junc ([[e]] -> Matrix e a ()
forall e cols rows.
FromLists e 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 e cols rows.
FromLists e cols rows =>
[[e]] -> Matrix e cols rows
fromLists [Int -> [e] -> [e]
forall a. Int -> [a] -> [a]
drop Int
rowsA [e]
l])
  fromLists _       = String -> Matrix e (Either a b) ()
forall a. HasCallStack => String -> a
error "Wrong dimensions"

instance {-# OVERLAPPING #-} (FromLists e () rows) => FromLists e () (Either () rows) where
  fromLists :: [[e]] -> Matrix e () (Either () rows)
fromLists ([h :: e
h] : t :: [[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)
Split (e -> Matrix e () ()
forall e. e -> Matrix e () ()
One e
h) ([[e]] -> Matrix e () rows
forall e cols rows.
FromLists e cols rows =>
[[e]] -> Matrix e cols rows
fromLists [[e]]
t)
  fromLists _         = String -> Matrix e () (Either () rows)
forall a. HasCallStack => String -> a
error "Wrong dimensions"

instance {-# OVERLAPPABLE #-} (FromLists e () a, FromLists e () b, Countable a) => FromLists e () (Either a b) where
  fromLists :: [[e]] -> Matrix e () (Either a b)
fromLists l :: [[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 cols a b.
Matrix e cols a -> Matrix e cols b -> Matrix e cols (Either a b)
Split ([[e]] -> Matrix e () a
forall e cols rows.
FromLists e 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 e cols rows.
FromLists e cols rows =>
[[e]] -> Matrix e cols rows
fromLists (Int -> [[e]] -> [[e]]
forall a. Int -> [a] -> [a]
drop Int
rowsA [[e]]
l))
  fromLists _         = String -> Matrix e () (Either a b)
forall a. HasCallStack => String -> a
error "Wrong dimensions"

instance {-# OVERLAPPABLE #-} (FromLists e (Either a b) c, FromLists e (Either a b) d, Countable c) => FromLists e (Either a b) (Either c d) where
  fromLists :: [[e]] -> Matrix e (Either a b) (Either c d)
fromLists l :: [[e]]
l@(h :: [e]
h : t :: [[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 = (Int -> Bool) -> [Int] -> 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) (([e] -> Int) -> [[e]] -> [Int]
forall a b. (a -> b) -> [a] -> [b]
map [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
> 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)
Split ([[e]] -> Matrix e (Either a b) c
forall e cols rows.
FromLists e 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 e cols rows.
FromLists e 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 "Not all rows have the same length"

-- | Matrix builder function. Constructs a matrix provided with
-- a construction function.
matrixBuilder ::
  forall e cols rows.
  ( FromLists e cols rows,
    CountableDimensions cols rows
  ) =>
  ((Int, Int) -> e) ->
  Matrix e cols rows
matrixBuilder :: ((Int, Int) -> e) -> Matrix e cols rows
matrixBuilder f :: (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 <- [0 .. (Int
r Int -> Int -> Int
forall a. Num a => a -> a -> a
- 1)], Int
b <- [0 .. (Int
c Int -> Int -> Int
forall a. Num a => a -> a -> a
- 1)]]
   in [[e]] -> Matrix e cols rows
forall e cols rows.
FromLists e cols rows =>
[[e]] -> Matrix e cols rows
fromLists ([[e]] -> Matrix e cols rows)
-> ([(Int, Int)] -> [[e]]) -> [(Int, Int)] -> Matrix e cols rows
forall k (cat :: k -> k -> Type) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat 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)]] -> [[e]])
-> ([(Int, Int)] -> [[(Int, Int)]]) -> [(Int, Int)] -> [[e]]
forall k (cat :: k -> k -> Type) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. ((Int, Int) -> (Int, Int) -> Bool)
-> [(Int, Int)] -> [[(Int, Int)]]
forall a. (a -> a -> Bool) -> [a] -> [[a]]
groupBy (\(x :: Int
x, _) (w :: Int
w, _) -> 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

-- | Constructs a column vector matrix
col :: (FromLists e () rows) => [e] -> Matrix e () rows
col :: [e] -> Matrix e () rows
col = [[e]] -> Matrix e () rows
forall e cols rows.
FromLists e cols rows =>
[[e]] -> Matrix e cols rows
fromLists ([[e]] -> Matrix e () rows)
-> ([e] -> [[e]]) -> [e] -> Matrix e () rows
forall k (cat :: k -> k -> Type) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat 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 :: (FromLists e cols ()) => [e] -> Matrix e cols ()
row :: [e] -> Matrix e cols ()
row = [[e]] -> Matrix e cols ()
forall e cols rows.
FromLists e cols rows =>
[[e]] -> Matrix e cols rows
fromLists ([[e]] -> Matrix e cols ())
-> ([e] -> [[e]]) -> [e] -> Matrix e cols ()
forall k (cat :: k -> k -> Type) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat 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,
    CountableDimensions cols rows,
    FromLists e rows cols
  ) =>
  (a -> b) ->
  Matrix e cols rows
fromF :: (a -> b) -> Matrix e cols rows
fromF f :: 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])
-> ([(a, b)] -> [((Int, Int), e)]) -> [(a, b)] -> [e]
forall k (cat :: k -> k -> Type) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. [((Int, Int), e)] -> [((Int, Int), e)]
forall a. Ord a => [a] -> [a]
sort ([((Int, Int), e)] -> [((Int, Int), e)])
-> ([(a, b)] -> [((Int, Int), e)]) -> [(a, b)] -> [((Int, Int), e)]
forall k (cat :: k -> k -> Type) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. ((a, b) -> ((Int, Int), e)) -> [(a, b)] -> [((Int, Int), e)]
forall a b. (a -> b) -> [a] -> [b]
map (\(a :: a
a, b :: 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), 1) 
                                                         else ((a -> Int
forall a. Enum a => a -> Int
fromEnum a
a, b -> Int
forall a. Enum a => a -> Int
fromEnum b
b), 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 e cols rows.
FromLists e cols rows =>
[[e]] -> Matrix e cols rows
fromLists [[e]]
mList
  where
    buildList :: [a] -> Int -> [[a]]
buildList [] _ = []
    buildList l :: [a]
l r :: 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,
    CountableDimensionsN a b,
    FromListsN e b a
  ) =>
  (a -> b) ->
  Matrix e (Normalize a) (Normalize b)
fromF' :: (a -> b) -> Matrix e (Normalize a) (Normalize b)
fromF' f :: 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])
-> ([(a, b)] -> [((Int, Int), e)]) -> [(a, b)] -> [e]
forall k (cat :: k -> k -> Type) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. [((Int, Int), e)] -> [((Int, Int), e)]
forall a. Ord a => [a] -> [a]
sort ([((Int, Int), e)] -> [((Int, Int), e)])
-> ([(a, b)] -> [((Int, Int), e)]) -> [(a, b)] -> [((Int, Int), e)]
forall k (cat :: k -> k -> Type) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. ((a, b) -> ((Int, Int), e)) -> [(a, b)] -> [((Int, Int), e)]
forall a b. (a -> b) -> [a] -> [b]
map (\(a :: a
a, b :: 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), 1) 
                                                         else ((a -> Int
forall a. Enum a => a -> Int
fromEnum a
a, b -> Int
forall a. Enum a => a -> Int
fromEnum b
b), 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 e cols rows.
FromLists e cols rows =>
[[e]] -> Matrix e cols rows
fromLists [[e]]
mList
  where
    buildList :: [a] -> Int -> [[a]]
buildList [] _ = []
    buildList l :: [a]
l r :: 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 Empty       = []
toLists (One e :: e
e)     = [[e
e]]
toLists (Split l :: Matrix e cols a
l r :: 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 (Junc l :: Matrix e a rows
l r :: 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 (cat :: k -> k -> Type) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat 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, FromLists e cols rows, CountableDimensions cols rows) => Matrix e cols rows
zeros :: Matrix e cols rows
zeros = ((Int, Int) -> e) -> Matrix e cols rows
forall e cols rows.
(FromLists e cols rows, CountableDimensions cols rows) =>
((Int, Int) -> e) -> Matrix e cols rows
matrixBuilder (e -> (Int, Int) -> e
forall a b. a -> b -> a
const 0)

-- Ones Matrix

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

-- Const Matrix

-- | The constant matrix constructor. A matrix wholly filled with a given
-- value.
constant :: (Num e, FromLists e cols rows, CountableDimensions cols rows) => e -> Matrix e cols rows
constant :: e -> Matrix e cols rows
constant e :: e
e = ((Int, Int) -> e) -> Matrix e cols rows
forall e cols rows.
(FromLists e cols rows, CountableDimensions 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, FromLists e 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 e cols rows.
FromLists e cols rows =>
[[e]] -> Matrix e cols rows
fromLists [Int -> [e] -> [e]
forall a. Int -> [a] -> [a]
take Int
c [1, 1 ..]]

-- Identity Matrix

-- | Identity matrix.
identity :: (Num e, FromLists e cols cols, Countable cols) => Matrix e cols cols
identity :: Matrix e cols cols
identity = ((Int, Int) -> e) -> Matrix e cols cols
forall e cols rows.
(FromLists e cols rows, CountableDimensions cols rows) =>
((Int, Int) -> e) -> Matrix e cols rows
matrixBuilder (e -> e -> Bool -> e
forall a. a -> a -> Bool -> a
bool 0 1 (Bool -> e) -> ((Int, Int) -> Bool) -> (Int, Int) -> e
forall k (cat :: k -> k -> Type) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat 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 identity #-}

-- 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 Empty Empty            = Matrix e cols rows
forall e. Matrix e Void Void
Empty
comp (One a :: e
a) (One b :: 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 (Junc a :: Matrix e a rows
a b :: Matrix e b rows
b) (Split c :: Matrix e cols a
c d :: 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 (Split a :: Matrix e cr a
a b :: Matrix e cr b
b) c :: 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)
Split (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) -- Split fusion law
comp c :: Matrix e cr rows
c (Junc a :: Matrix e a cr
a b :: 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
Junc (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)  -- Junc fusion law
{-# NOINLINE comp #-}
{-# RULES 
   "comp/identity1" forall m. comp m identity = m ;
   "comp/identity2" forall m. comp identity m = m
#-}

-- Projections

-- | Biproduct first component projection
p1 :: forall e m n. (Num e, CountableDimensions n m, FromLists e n m, FromLists e m m) => Matrix e (Either m n) m
p1 :: Matrix e (Either m n) m
p1 =
  let iden :: Matrix e m m
iden = Matrix e m m
forall e cols.
(Num e, FromLists e cols cols, Countable cols) =>
Matrix e cols cols
identity :: Matrix e m m
      zero :: Matrix e n m
zero = Matrix e n m
forall e cols rows.
(Num e, FromLists e cols rows, CountableDimensions cols rows) =>
Matrix e cols rows
zeros :: Matrix e n m
   in 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
junc Matrix e m m
iden Matrix e n m
zero

-- | Biproduct second component projection
p2 :: forall e m n. (Num e, CountableDimensions n m, FromLists e m n, FromLists e n n) => Matrix e (Either m n) n
p2 :: Matrix e (Either m n) n
p2 =
  let iden :: Matrix e n n
iden = Matrix e n n
forall e cols.
(Num e, FromLists e cols cols, Countable cols) =>
Matrix e cols cols
identity :: Matrix e n n
      zero :: Matrix e m n
zero = Matrix e m n
forall e cols rows.
(Num e, FromLists e cols rows, CountableDimensions cols rows) =>
Matrix e cols rows
zeros :: Matrix e m n
   in 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
junc Matrix e m n
zero Matrix e n n
iden

-- Injections

-- | Biproduct first component injection
i1 :: (Num e, CountableDimensions n m, FromLists e n m, FromLists e 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 m n.
(Num e, CountableDimensions n m, FromLists e n m,
 FromLists e m m) =>
Matrix e (Either m n) m
p1

-- | Biproduct second component injection
i2 :: (Num e, CountableDimensions n m, FromLists e m n, FromLists e 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 m n.
(Num e, CountableDimensions n m, FromLists e m n,
 FromLists e n n) =>
Matrix e (Either m n) n
p2

-- Dimensions

-- | Obtain the number of rows.
--
--   NOTE: The 'KnownNat' constaint is needed in order to obtain the
-- dimensions in constant time.
--
-- TODO: A 'rows' function that does not need the 'KnownNat' constraint in
-- exchange for performance.
rows :: forall e cols rows. (Countable rows) => Matrix e cols rows -> Int
rows :: Matrix e cols rows -> Int
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 columns.
-- 
--   NOTE: The 'KnownNat' constaint is needed in order to obtain the
-- dimensions in constant time.
--
-- TODO: A 'columns' function that does not need the 'KnownNat' constraint in
-- exchange for performance.
columns :: forall e cols rows. (Countable cols) => Matrix e cols rows -> Int
columns :: Matrix e cols rows -> Int
columns _ = 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))

-- Coproduct Bifunctor

infixl 5 -|-

-- | Matrix coproduct functor also known as matrix direct sum.
(-|-) ::
  forall e n k m j.
  ( Num e,
    CountableDimensions j k,
    FromLists e k k,
    FromLists e j k,
    FromLists e k j,
    FromLists e 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)
(-|-) a :: Matrix e n k
a b :: 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
Junc (Matrix e k (Either k j)
forall e n m.
(Num e, CountableDimensions n m, FromLists e n m,
 FromLists e 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 (cat :: k -> k -> Type) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. Matrix e n k
a) (Matrix e j (Either k j)
forall e n m.
(Num e, CountableDimensions n m, FromLists e m n,
 FromLists e 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 (cat :: k -> k -> Type) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. Matrix e m j
b)

-- Khatri Rao Product and projections

-- | Khatri Rao product first component projection matrix.
kp1 :: 
  forall e m k .
  ( Num e,
    CountableDimensions k m,
    FromLists e (Normalize (m, k)) m,
    CountableN (m, k)
  ) => Matrix e (Normalize (m, k)) m
kp1 :: Matrix e (Normalize (m, k)) m
kp1 = ((Int, Int) -> e) -> Matrix e (FromNat (Count m * Count k)) m
forall e cols rows.
(FromLists e cols rows, CountableDimensions 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 (x :: Int
x, y :: 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
- 1) = 1
      | Bool
otherwise = 0

-- | Khatri Rao product second component projection matrix.
kp2 :: 
    forall e m k .
    ( Num e,
      CountableDimensions k m,
      FromLists e (Normalize (m, k)) k,
      CountableN (m, k)
    ) => Matrix e (Normalize (m, k)) k
kp2 :: Matrix e (Normalize (m, k)) k
kp2 = ((Int, Int) -> e) -> Matrix e (FromNat (Count m * Count k)) k
forall e cols rows.
(FromLists e cols rows, CountableDimensions 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 (x :: Int
x, y :: 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
== 0 = 1
      | Bool
otherwise                         = 0

-- | Khatri Rao Matrix product also known as matrix pairing.
--
--   NOTE: That this is not a true categorical product, see for instance:
-- 
-- @
--                | kp1 . khatri a b == a 
-- khatri a b ==> |
--                | kp2 . khatri a b == b
-- @
--
-- __Emphasis__ on the implication symbol.
khatri :: 
       forall e cols a b. 
       ( Num e,
         CountableDimensions a b,
         CountableN (a, b),
         FromLists e (Normalize (a, b)) a,
         FromLists e (Normalize (a, b)) b
       ) => Matrix e cols a -> Matrix e cols b -> Matrix e cols (Normalize (a, b))
khatri :: Matrix e cols a
-> Matrix e cols b -> Matrix e cols (Normalize (a, b))
khatri a :: Matrix e cols a
a b :: Matrix e cols b
b =
  let kp1' :: Matrix e (Normalize (a, b)) a
kp1' = (Num e, CountableDimensions b a, FromLists e (Normalize (a, b)) a,
 CountableN (a, b)) =>
Matrix e (Normalize (a, b)) a
forall e m k.
(Num e, CountableDimensions k m, FromLists e (Normalize (m, k)) m,
 CountableN (m, k)) =>
Matrix e (Normalize (m, k)) m
kp1 @e @a @b
      kp2' :: Matrix e (Normalize (a, b)) b
kp2' = (Num e, CountableDimensions b a, FromLists e (Normalize (a, b)) b,
 CountableN (a, b)) =>
Matrix e (Normalize (a, b)) b
forall e m k.
(Num e, CountableDimensions k m, FromLists e (Normalize (m, k)) k,
 CountableN (m, k)) =>
Matrix e (Normalize (m, k)) k
kp2 @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
kp1') Matrix e a (FromNat (Count a * Count b))
-> Matrix e cols a -> Matrix e cols (FromNat (Count a * Count b))
forall k (cat :: k -> k -> Type) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat 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
kp2') Matrix e b (FromNat (Count a * Count b))
-> Matrix e cols b -> Matrix e cols (FromNat (Count a * Count b))
forall k (cat :: k -> k -> Type) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat 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,
       CountableDimensions m n,
       CountableDimensions p q,
       CountableDimensionsN (m, n) (p, q),
       FromLists e (Normalize (m, n)) m,
       FromLists e (Normalize (m, n)) n,
       FromLists e (Normalize (p, q)) p,
       FromLists e (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))
(><) a :: Matrix e m p
a b :: Matrix e n q
b =
  let kp1' :: Matrix e (Normalize (m, n)) m
kp1' = (Num e, CountableDimensions n m, FromLists e (Normalize (m, n)) m,
 CountableN (m, n)) =>
Matrix e (Normalize (m, n)) m
forall e m k.
(Num e, CountableDimensions k m, FromLists e (Normalize (m, k)) m,
 CountableN (m, k)) =>
Matrix e (Normalize (m, k)) m
kp1 @e @m @n
      kp2' :: Matrix e (Normalize (m, n)) n
kp2' = (Num e, CountableDimensions n m, FromLists e (Normalize (m, n)) n,
 CountableN (m, n)) =>
Matrix e (Normalize (m, n)) n
forall e m k.
(Num e, CountableDimensions k m, FromLists e (Normalize (m, k)) k,
 CountableN (m, k)) =>
Matrix e (Normalize (m, k)) k
kp2 @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, CountableDimensions a b, CountableN (a, b),
 FromLists e (Normalize (a, b)) a,
 FromLists e (Normalize (a, b)) b) =>
Matrix e cols a
-> Matrix e cols b -> Matrix e cols (Normalize (a, b))
khatri (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 (cat :: k -> k -> Type) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. Matrix e (Normalize (m, n)) m
Matrix e (FromNat (Count m * Count n)) m
kp1') (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 (cat :: k -> k -> Type) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. Matrix e (Normalize (m, n)) n
Matrix e (FromNat (Count m * Count n)) n
kp2')

-- Matrix abide Junc Split

-- | Matrix "abiding" followin the 'Junc'-'Split' abide law.
-- 
-- Law:
--
-- @
-- 'Junc' ('Split' a c) ('Split' b d) == 'Split' ('Junc' a b) ('Junc' c d)
-- @
abideJS :: Matrix e cols rows -> Matrix e cols rows
abideJS :: Matrix e cols rows -> Matrix e cols rows
abideJS (Junc (Split a :: Matrix e a a
a c :: Matrix e a b
c) (Split b :: Matrix e b a
b d :: 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)
Split (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
Junc (Matrix e a a -> Matrix e a a
forall e cols rows. Matrix e cols rows -> Matrix e cols rows
abideJS 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
abideJS 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
Junc (Matrix e a b -> Matrix e a b
forall e cols rows. Matrix e cols rows -> Matrix e cols rows
abideJS 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
abideJS Matrix e b b
d)) -- Junc-Split abide law
abideJS Empty                          = Matrix e cols rows
forall e. Matrix e Void Void
Empty
abideJS (One e :: e
e)                        = e -> Matrix e () ()
forall e. e -> Matrix e () ()
One e
e
abideJS (Junc a :: Matrix e a rows
a b :: 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
Junc (Matrix e a rows -> Matrix e a rows
forall e cols rows. Matrix e cols rows -> Matrix e cols rows
abideJS 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
abideJS Matrix e b rows
b)
abideJS (Split a :: Matrix e cols a
a b :: 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)
Split (Matrix e cols a -> Matrix e cols a
forall e cols rows. Matrix e cols rows -> Matrix e cols rows
abideJS 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
abideJS Matrix e cols b
b)

-- Matrix abide Split Junc

-- | Matrix "abiding" followin the 'Split'-'Junc' abide law.
-- 
-- @
-- 'Split' ('Junc' a b) ('Junc' c d) == 'Junc' ('Split' a c) ('Split' b d)
-- @
abideSJ :: Matrix e cols rows -> Matrix e cols rows
abideSJ :: Matrix e cols rows -> Matrix e cols rows
abideSJ (Split (Junc a :: Matrix e a a
a b :: Matrix e b a
b) (Junc c :: Matrix e a b
c d :: 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
Junc (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)
Split (Matrix e a a -> Matrix e a a
forall e cols rows. Matrix e cols rows -> Matrix e cols rows
abideSJ 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
abideSJ 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)
Split (Matrix e b a -> Matrix e b a
forall e cols rows. Matrix e cols rows -> Matrix e cols rows
abideSJ 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
abideSJ Matrix e b b
d)) -- Split-Junc abide law
abideSJ Empty                         = Matrix e cols rows
forall e. Matrix e Void Void
Empty
abideSJ (One e :: e
e)                       = e -> Matrix e () ()
forall e. e -> Matrix e () ()
One e
e
abideSJ (Junc a :: Matrix e a rows
a b :: 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
Junc (Matrix e a rows -> Matrix e a rows
forall e cols rows. Matrix e cols rows -> Matrix e cols rows
abideSJ 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
abideSJ Matrix e b rows
b)
abideSJ (Split a :: Matrix e cols a
a b :: 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)
Split (Matrix e cols a -> Matrix e cols a
forall e cols rows. Matrix e cols rows -> Matrix e cols rows
abideSJ 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
abideSJ 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 Empty       = Matrix e rows cols
forall e. Matrix e Void Void
Empty
tr (One e :: e
e)     = e -> Matrix e () ()
forall e. e -> Matrix e () ()
One e
e
tr (Junc a :: Matrix e a rows
a b :: 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)
Split (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 (Split a :: Matrix e cols a
a b :: 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
Junc (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, FromLists e 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 (Split a :: Matrix e cols a
a b :: Matrix e cols b
b) y :: Matrix e a b
y                    = Matrix e a b
y Matrix e a b -> Matrix e cols a -> Matrix e cols b
forall k (cat :: k -> k -> Type) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat 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 (Junc (Split a :: Matrix e a a
a c :: Matrix e a b
c) (Split b :: Matrix e b a
b d :: Matrix e b b
d)) y :: 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
junc (Matrix e a b
y Matrix e a b -> Matrix e a a -> Matrix e a b
forall k (cat :: k -> k -> Type) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat 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 (cat :: k -> k -> Type) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat 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 m :: Matrix e cols (Either a b)
m y :: 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
junc Matrix e a b
y Matrix e b b
forall e cols.
(Num e, FromLists e cols cols, Countable cols) =>
Matrix e cols cols
identity Matrix e (Either a b) b
-> Matrix e cols (Either a b) -> Matrix e cols b
forall k (cat :: k -> k -> Type) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. Matrix e cols (Either a b)
m

branch ::
       ( Num e,
         CountableDimensions a b,
         CountableDimensions c (Either b c),
         FromLists e c b,
         FromLists e a b,
         FromLists e a a,
         FromLists e b b,
         FromLists e c c,
         FromLists e b a,
         FromLists e b c,
         FromLists e (Either b c) b,
         FromLists e (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 x :: Matrix e cols (Either a b)
x l :: Matrix e a c
l r :: 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, CountableDimensions b c, FromLists e a b,
 FromLists e c b, FromLists e b b, FromLists e b a,
 FromLists e 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, FromLists e 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, CountableDimensions b c, FromLists e b c,
 FromLists e 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, FromLists e 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, CountableDimensions b c, FromLists e a b, FromLists e c b, FromLists e b b, FromLists e b a, FromLists e 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 m :: 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)
split (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, CountableDimensions n m, FromLists e n m,
 FromLists e m m) =>
Matrix e m (Either m n)
i1) (Matrix e b (Either b c)
forall e n m.
(Num e, CountableDimensions n m, FromLists e n m,
 FromLists e 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 (cat :: k -> k -> Type) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat 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, CountableDimensions n m, FromLists e m n,
 FromLists e 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 (cat :: k -> k -> Type) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. Matrix e cols (Either a b)
m
    g :: (Num e, CountableDimensions b c, FromLists e b c, FromLists e c c) => Matrix e a c -> Matrix e a (Either b c)
    g :: Matrix e a c -> Matrix e a (Either b c)
g m :: Matrix e a c
m = Matrix e c (Either b c)
forall e n m.
(Num e, CountableDimensions n m, FromLists e m n,
 FromLists e 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 (cat :: k -> k -> Type) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. Matrix e a c
m

-- McCarthy's Conditional

-- | McCarthy's Conditional expresses probabilistic choice.
cond ::
     ( Trivial cols,
       Countable cols,
       FromLists e () cols,
       FromLists e cols (),
       FromLists e 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 p :: a -> Bool
p f :: Matrix e cols rows
f g :: 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
junc 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 (cat :: k -> k -> Type) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. (a -> Bool) -> Matrix e cols (Either cols cols)
forall q e a.
(Trivial q, Countable q, FromLists e () q, FromLists e q (),
 FromLists e 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,
      FromLists e () q,
      FromLists e q (),
      FromLists e 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 f :: 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)
split ((a -> Bool) -> Matrix e q q
forall e a q.
(Trivial q, Countable q, FromLists e () q, FromLists e q (),
 FromLists e 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, FromLists e () q, FromLists e q (),
 FromLists e q q, Liftable e a Bool) =>
(a -> Bool) -> Matrix e q q
corr (Bool -> Bool
not (Bool -> Bool) -> (a -> Bool) -> a -> Bool
forall k (cat :: k -> k -> Type) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. a -> Bool
f))

corr :: 
    forall e a q . 
    ( Trivial q,
      Countable q,
      FromLists e () q,
      FromLists e q (),
      FromLists e q q,
      Liftable e a Bool
    ) 
     => (a -> Bool) -> Matrix e q q
corr :: (a -> Bool) -> Matrix e q q
corr p :: a -> Bool
p = let f :: Matrix e q ()
f = (a -> Bool) -> Matrix e q ()
forall a b cols rows e.
(Liftable e a b, CountableDimensions cols rows,
 FromLists e 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, CountableDimensions a b, CountableN (a, b),
 FromLists e (Normalize (a, b)) a,
 FromLists e (Normalize (a, b)) b) =>
Matrix e cols a
-> Matrix e cols b -> Matrix e cols (Normalize (a, b))
khatri Matrix e q ()
f (Matrix e q q
forall e cols.
(Num e, FromLists e cols cols, Countable cols) =>
Matrix e cols cols
identity :: Matrix e q q)

-- Pretty print

prettyAux :: Show e => [[e]] -> [[e]] -> String
prettyAux :: [[e]] -> [[e]] -> String
prettyAux [] _     = ""
prettyAux [[e :: e
e]] m :: [[e]]
m   = "│ " 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]
++ " │\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 str :: 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
- 2) ' ' String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
str
prettyAux [h :: [e]
h] m :: [[e]]
m     = "│ " 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]
++ " │\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 str :: 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
- 2) ' ' String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
str
prettyAux (h :: [e]
h : t :: [[e]]
t) l :: [[e]]
l = "│ " 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]
++ " │\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 str :: 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
- 2) ' ' String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
str

-- | Matrix pretty printer
pretty :: (CountableDimensions cols rows, Show e) => Matrix e cols rows -> String
pretty :: Matrix e cols rows -> String
pretty m :: Matrix e cols rows
m = [String] -> String
forall (t :: Type -> Type) a. Foldable t => t [a] -> [a]
concat
   [ "┌ ", [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), " ┐\n"
   , [String] -> String
unlines
   [ "│ " 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 (\j :: 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) [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]
++ " │" | Int
i <- [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
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), " ┘"
   ]
 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 str :: 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) ' ' String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
str
   blank :: String
blank = ShowS
fill ""
   safeGet :: Int -> Int -> Matrix a cols rows -> Maybe a
safeGet i :: Int
i j :: Int
j m :: 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
< 1 Bool -> Bool -> Bool
|| Int
j Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< 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 i :: Int
i j :: Int
j m :: Matrix e cols rows
m l :: [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 m :: a
m (i :: a
i,j :: a
j) = (a
ia -> a -> a
forall a. Num 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
- 1
   getElem :: Int -> Int -> Matrix a cols rows -> a
getElem i :: Int
i j :: Int
j m :: 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
$
          "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]
++ " 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]
++ "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]
++ " 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 :: (CountableDimensions 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 (cat :: k -> k -> Type) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. Matrix e cols rows -> String
forall cols rows e.
(CountableDimensions 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 f :: e -> f -> g
f Empty Empty                = Matrix g cols rows
forall e. Matrix e Void Void
Empty
zipWithM f :: e -> f -> g
f (One a :: e
a) (One b :: f
b)            = g -> Matrix g () ()
forall e. e -> Matrix e () ()
One (e -> f -> g
f e
a f
b)
zipWithM f :: e -> f -> g
f (Junc a :: Matrix e a rows
a b :: Matrix e b rows
b) (Junc c :: Matrix f a rows
c d :: 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
Junc ((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 f :: e -> f -> g
f (Split a :: Matrix e cols a
a b :: Matrix e cols b
b) (Split c :: Matrix f cols a
c d :: 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)
Split ((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 f :: e -> f -> g
f x :: Matrix e cols rows
x@(Split _ _) y :: Matrix f cols rows
y@(Junc _ _) = (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
abideJS Matrix f cols rows
y)
zipWithM f :: e -> f -> g
f x :: Matrix e cols rows
x@(Junc _ _) y :: Matrix f cols rows
y@(Split _ _) = (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
abideJS 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 n :: e
n
  | e
n e -> e -> Bool
forall a. Eq a => a -> a -> Bool
== 0 = Bool
False
  | e
n e -> e -> Bool
forall a. Eq a => a -> a -> Bool
== 1 = Bool
True

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

-- | Relational negation
negateM :: Relation cols rows -> Relation cols rows
negateM :: Relation cols rows -> Relation cols rows
negateM Empty         = Relation cols rows
forall e. Matrix e Void Void
Empty
negateM (One (Nat 0)) = 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 1)
negateM (One (Nat 1)) = 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 0)
negateM (Junc a :: Matrix (Natural 0 1) a rows
a b :: 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
Junc (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 (Split a :: Matrix (Natural 0 1) cols a
a b :: 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)
Split (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 Empty Empty                = Relation cols rows
forall e. Matrix e Void Void
Empty
orM (One a :: Natural 0 1
a) (One b :: 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 (Junc a :: Matrix (Natural 0 1) a rows
a b :: Matrix (Natural 0 1) b rows
b) (Junc c :: Matrix (Natural 0 1) a rows
c d :: 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
Junc (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 (Split a :: Matrix (Natural 0 1) cols a
a b :: Matrix (Natural 0 1) cols b
b) (Split c :: Matrix (Natural 0 1) cols a
c d :: 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)
Split (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@(Split _ _) y :: Relation cols rows
y@(Junc _ _) = 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
abideJS Relation cols rows
y)
orM x :: Relation cols rows
x@(Junc _ _) y :: Relation cols rows
y@(Split _ _) = 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
abideJS 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 Empty Empty                = Relation cols rows
forall e. Matrix e Void Void
Empty
andM (One a :: Natural 0 1
a) (One b :: 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 (Junc a :: Matrix (Natural 0 1) a rows
a b :: Matrix (Natural 0 1) b rows
b) (Junc c :: Matrix (Natural 0 1) a rows
c d :: 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
Junc (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 (Split a :: Matrix (Natural 0 1) cols a
a b :: Matrix (Natural 0 1) cols b
b) (Split c :: Matrix (Natural 0 1) cols a
c d :: 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)
Split (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@(Split _ _) y :: Relation cols rows
y@(Junc _ _) = 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
abideJS Relation cols rows
y)
andM x :: Relation cols rows
x@(Junc _ _) y :: Relation cols rows
y@(Split _ _) = 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
abideJS 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 Empty Empty                = Relation cols rows
forall e. Matrix e Void Void
Empty
subM (One a :: Natural 0 1
a) (One b :: 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 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 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 (Junc a :: Matrix (Natural 0 1) a rows
a b :: Matrix (Natural 0 1) b rows
b) (Junc c :: Matrix (Natural 0 1) a rows
c d :: 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
Junc (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 (Split a :: Matrix (Natural 0 1) cols a
a b :: Matrix (Natural 0 1) cols b
b) (Split c :: Matrix (Natural 0 1) cols a
c d :: 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)
Split (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@(Split _ _) y :: Relation cols rows
y@(Junc _ _) = 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
abideJS Relation cols rows
y)
subM x :: Relation cols rows
x@(Junc _ _) y :: Relation cols rows
y@(Split _ _) = 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
abideJS 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 Empty Empty            = Relation cols rows
forall e. Matrix e Void Void
Empty
compRel (One a :: Natural 0 1
a) (One b :: 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 (Junc a :: Matrix (Natural 0 1) a rows
a b :: Matrix (Natural 0 1) b rows
b) (Split c :: Matrix (Natural 0 1) cols a
c d :: 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 (Split a :: Matrix (Natural 0 1) cr a
a b :: Matrix (Natural 0 1) cr b
b) c :: 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)
Split (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) -- Split fusion law
compRel c :: Relation cr rows
c (Junc a :: Matrix (Natural 0 1) a cr
a b :: 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
Junc (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)  -- Junc 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 Empty Empty           = Relation a c
forall e. Matrix e Void Void
Empty
divR (One a :: Natural 0 1
a) (One b :: 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 (Junc a :: Matrix (Natural 0 1) a c
a b :: Matrix (Natural 0 1) b c
b) (Junc c :: Matrix (Natural 0 1) a a
c d :: 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 (Split a :: Matrix (Natural 0 1) b a
a b :: Matrix (Natural 0 1) b b
b) c :: 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)
Split (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 c :: Relation b c
c (Split a :: Matrix (Natural 0 1) b a
a b :: 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
Junc (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 x :: Relation c b
x y :: 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 s :: Relation c a
s r :: 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,
    CountableDimensions cols rows,
    FromLists Boolean rows cols
  ) =>
  (a -> b) ->
  Relation cols rows
fromFRel :: (a -> b) -> Relation cols rows
fromFRel f :: 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])
-> ([(a, b)] -> [((Int, Int), Natural 0 1)])
-> [(a, b)]
-> [Natural 0 1]
forall k (cat :: k -> k -> Type) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. [((Int, Int), Natural 0 1)] -> [((Int, Int), Natural 0 1)]
forall a. Ord a => [a] -> [a]
sort ([((Int, Int), Natural 0 1)] -> [((Int, Int), Natural 0 1)])
-> ([(a, b)] -> [((Int, Int), Natural 0 1)])
-> [(a, b)]
-> [((Int, Int), Natural 0 1)]
forall k (cat :: k -> k -> Type) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat 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
a, b :: 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 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 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 e cols rows.
FromLists e cols rows =>
[[e]] -> Matrix e cols rows
fromLists [[Natural 0 1]]
mList
  where
    buildList :: [a] -> Int -> [[a]]
buildList [] _ = []
    buildList l :: [a]
l r :: 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,
    CountableDimensionsN a b,
    FromLists Boolean (Normalize b) (Normalize a)
  ) =>
  (a -> b) ->
  Relation (Normalize a) (Normalize b)
fromFRel' :: (a -> b) -> Relation (Normalize a) (Normalize b)
fromFRel' f :: 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])
-> ([(a, b)] -> [((Int, Int), Natural 0 1)])
-> [(a, b)]
-> [Natural 0 1]
forall k (cat :: k -> k -> Type) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. [((Int, Int), Natural 0 1)] -> [((Int, Int), Natural 0 1)]
forall a. Ord a => [a] -> [a]
sort ([((Int, Int), Natural 0 1)] -> [((Int, Int), Natural 0 1)])
-> ([(a, b)] -> [((Int, Int), Natural 0 1)])
-> [(a, b)]
-> [((Int, Int), Natural 0 1)]
forall k (cat :: k -> k -> Type) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat 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
a, b :: 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 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 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 e cols rows.
FromLists e cols rows =>
[[e]] -> Matrix e cols rows
fromLists [[Natural 0 1]]
mList
  where
    buildList :: [a] -> Int -> [[a]]
buildList [] _ = []
    buildList l :: [a]
l r :: 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,
        CountableDimensionsN a b,
        FromListsN Boolean b a
      ) 
      => (a -> b -> Bool) -> Relation (Normalize a) (Normalize b)
toRel :: (a -> b -> Bool) -> Relation (Normalize a) (Normalize b)
toRel f :: 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])
-> ([(a, b)] -> [((Int, Int), Natural 0 1)])
-> [(a, b)]
-> [Natural 0 1]
forall k (cat :: k -> k -> Type) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. [((Int, Int), Natural 0 1)] -> [((Int, Int), Natural 0 1)]
forall a. Ord a => [a] -> [a]
sort ([((Int, Int), Natural 0 1)] -> [((Int, Int), Natural 0 1)])
-> ([(a, b)] -> [((Int, Int), Natural 0 1)])
-> [(a, b)]
-> [((Int, Int), Natural 0 1)]
forall k (cat :: k -> k -> Type) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat 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
a, b :: 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 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 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 e cols rows.
FromLists e cols rows =>
[[e]] -> Matrix e cols rows
fromLists [[Natural 0 1]]
mList
  where
    buildList :: [a] -> Int -> [[a]]
buildList [] _ = []
    buildList l :: [a]
l r :: 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