{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE DerivingVia #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE NoStarIsType #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}

-----------------------------------------------------------------------------
-- |
-- Module     : LAoP.Matrix.Nat
-- 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 a newtype wrapper around 'Matrix.Type.Matrix' that
-- uses type level naturals instead of standard data types for the matrices
-- dimensions.
--
-----------------------------------------------------------------------------

module LAoP.Matrix.Nat
  ( -- | LAoP (Linear Algebra of Programming) Inductive Matrix definition.
    --
    --         LAoP generalises relations and functions treating them as
    --         Boolean matrices and in turn consider these as arrows.
    --         This library offers many of the combinators mentioned in the work of
    --         Macedo (2012) and Oliveira (2012).
    --
    --         This definition is a wrapper around 'Matrix.Type' but
    --         dimensions are type level Naturals. Type inference might not
    --         be as desired.
    --
    --         There exists two type families that make it easier to write
    --         matrix dimensions: 'FromNat' and 'Count'. This approach
    --         leads to a very straightforward implementation 
    --         of LAoP combinators. 

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

    -- * Constraint type synonyms
    Countable,
    CountableDims,
    CountableN,
    CountableNz,
    CountableDimsN,
    FLN,
    FLNz,
    Liftable,
    TrivialE,
    TrivialP,

    -- * Primitives
    one,
    join,
    fork,

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

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

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

    -- ** Matrix Transposition
    tr,

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

    -- ** Selective operator
    select, 

    -- ** McCarthy's Conditional
    cond,

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

    -- ** Zip Matrices
    zipWithM,

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

    -- ** Applicative matrix combinators

    -- | Note that given the restrictions imposed it is not possible to
    -- implement the standard type classes present in standard Haskell.
    -- *** Matrix pairing projections
    fstM,
    sndM,

    -- *** Matrix pairing
    kr,

    -- * Matrix composition and lifting

    -- ** Arrow matrix combinators

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

    -- * Matrix printing
    pretty,
    prettyPrint
  )
where

import Data.Proxy
import GHC.TypeLits
import Control.DeepSeq
import qualified LAoP.Matrix.Internal as I

newtype Matrix e (cols :: Nat) (rows :: Nat) = M (I.Matrix e (I.FromNat cols) (I.FromNat rows))
  deriving (Int -> Matrix e cols rows -> ShowS
[Matrix e cols rows] -> ShowS
Matrix e cols rows -> String
(Int -> Matrix e cols rows -> ShowS)
-> (Matrix e cols rows -> String)
-> ([Matrix e cols rows] -> ShowS)
-> Show (Matrix e cols rows)
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
forall e (cols :: Nat) (rows :: Nat).
Show e =>
Int -> Matrix e cols rows -> ShowS
forall e (cols :: Nat) (rows :: Nat).
Show e =>
[Matrix e cols rows] -> ShowS
forall e (cols :: Nat) (rows :: Nat).
Show e =>
Matrix e cols rows -> String
showList :: [Matrix e cols rows] -> ShowS
$cshowList :: forall e (cols :: Nat) (rows :: Nat).
Show e =>
[Matrix e cols rows] -> ShowS
show :: Matrix e cols rows -> String
$cshow :: forall e (cols :: Nat) (rows :: Nat).
Show e =>
Matrix e cols rows -> String
showsPrec :: Int -> Matrix e cols rows -> ShowS
$cshowsPrec :: forall e (cols :: Nat) (rows :: Nat).
Show e =>
Int -> Matrix e cols rows -> ShowS
Show, Integer -> Matrix e cols rows
Matrix e cols rows -> Matrix e cols rows
Matrix e cols rows -> Matrix e cols rows -> Matrix e cols rows
(Matrix e cols rows -> Matrix e cols rows -> Matrix e cols rows)
-> (Matrix e cols rows -> Matrix e cols rows -> Matrix e cols rows)
-> (Matrix e cols rows -> Matrix e cols rows -> Matrix e cols rows)
-> (Matrix e cols rows -> Matrix e cols rows)
-> (Matrix e cols rows -> Matrix e cols rows)
-> (Matrix e cols rows -> Matrix e cols rows)
-> (Integer -> Matrix e cols rows)
-> Num (Matrix e cols rows)
forall a.
(a -> a -> a)
-> (a -> a -> a)
-> (a -> a -> a)
-> (a -> a)
-> (a -> a)
-> (a -> a)
-> (Integer -> a)
-> Num a
forall e (cols :: Nat) (rows :: Nat).
Num e =>
Integer -> Matrix e cols rows
forall e (cols :: Nat) (rows :: Nat).
Num e =>
Matrix e cols rows -> Matrix e cols rows
forall e (cols :: Nat) (rows :: Nat).
Num e =>
Matrix e cols rows -> Matrix e cols rows -> Matrix e cols rows
fromInteger :: Integer -> Matrix e cols rows
$cfromInteger :: forall e (cols :: Nat) (rows :: Nat).
Num e =>
Integer -> Matrix e cols rows
signum :: Matrix e cols rows -> Matrix e cols rows
$csignum :: forall e (cols :: Nat) (rows :: Nat).
Num e =>
Matrix e cols rows -> Matrix e cols rows
abs :: Matrix e cols rows -> Matrix e cols rows
$cabs :: forall e (cols :: Nat) (rows :: Nat).
Num e =>
Matrix e cols rows -> Matrix e cols rows
negate :: Matrix e cols rows -> Matrix e cols rows
$cnegate :: forall e (cols :: Nat) (rows :: Nat).
Num e =>
Matrix e cols rows -> Matrix e cols rows
* :: Matrix e cols rows -> Matrix e cols rows -> Matrix e cols rows
$c* :: forall e (cols :: Nat) (rows :: Nat).
Num e =>
Matrix e cols rows -> Matrix e cols rows -> Matrix e cols rows
- :: Matrix e cols rows -> Matrix e cols rows -> Matrix e cols rows
$c- :: forall e (cols :: Nat) (rows :: Nat).
Num e =>
Matrix e cols rows -> Matrix e cols rows -> Matrix e cols rows
+ :: Matrix e cols rows -> Matrix e cols rows -> Matrix e cols rows
$c+ :: forall e (cols :: Nat) (rows :: Nat).
Num e =>
Matrix e cols rows -> Matrix e cols rows -> Matrix e cols rows
Num, Matrix e cols rows -> Matrix e cols rows -> Bool
(Matrix e cols rows -> Matrix e cols rows -> Bool)
-> (Matrix e cols rows -> Matrix e cols rows -> Bool)
-> Eq (Matrix e cols rows)
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
forall e (cols :: Nat) (rows :: Nat).
Eq e =>
Matrix e cols rows -> Matrix e cols rows -> Bool
/= :: Matrix e cols rows -> Matrix e cols rows -> Bool
$c/= :: forall e (cols :: Nat) (rows :: Nat).
Eq e =>
Matrix e cols rows -> Matrix e cols rows -> Bool
== :: Matrix e cols rows -> Matrix e cols rows -> Bool
$c== :: forall e (cols :: Nat) (rows :: Nat).
Eq e =>
Matrix e cols rows -> Matrix e cols rows -> Bool
Eq, Eq (Matrix e cols rows)
Eq (Matrix e cols rows)
-> (Matrix e cols rows -> Matrix e cols rows -> Ordering)
-> (Matrix e cols rows -> Matrix e cols rows -> Bool)
-> (Matrix e cols rows -> Matrix e cols rows -> Bool)
-> (Matrix e cols rows -> Matrix e cols rows -> Bool)
-> (Matrix e cols rows -> Matrix e cols rows -> Bool)
-> (Matrix e cols rows -> Matrix e cols rows -> Matrix e cols rows)
-> (Matrix e cols rows -> Matrix e cols rows -> Matrix e cols rows)
-> Ord (Matrix e cols rows)
Matrix e cols rows -> Matrix e cols rows -> Bool
Matrix e cols rows -> Matrix e cols rows -> Ordering
Matrix e cols rows -> Matrix e cols rows -> Matrix e cols rows
forall a.
Eq a
-> (a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
forall e (cols :: Nat) (rows :: Nat).
Ord e =>
Eq (Matrix e cols rows)
forall e (cols :: Nat) (rows :: Nat).
Ord e =>
Matrix e cols rows -> Matrix e cols rows -> Bool
forall e (cols :: Nat) (rows :: Nat).
Ord e =>
Matrix e cols rows -> Matrix e cols rows -> Ordering
forall e (cols :: Nat) (rows :: Nat).
Ord e =>
Matrix e cols rows -> Matrix e cols rows -> Matrix e cols rows
min :: Matrix e cols rows -> Matrix e cols rows -> Matrix e cols rows
$cmin :: forall e (cols :: Nat) (rows :: Nat).
Ord e =>
Matrix e cols rows -> Matrix e cols rows -> Matrix e cols rows
max :: Matrix e cols rows -> Matrix e cols rows -> Matrix e cols rows
$cmax :: forall e (cols :: Nat) (rows :: Nat).
Ord e =>
Matrix e cols rows -> Matrix e cols rows -> Matrix e cols rows
>= :: Matrix e cols rows -> Matrix e cols rows -> Bool
$c>= :: forall e (cols :: Nat) (rows :: Nat).
Ord e =>
Matrix e cols rows -> Matrix e cols rows -> Bool
> :: Matrix e cols rows -> Matrix e cols rows -> Bool
$c> :: forall e (cols :: Nat) (rows :: Nat).
Ord e =>
Matrix e cols rows -> Matrix e cols rows -> Bool
<= :: Matrix e cols rows -> Matrix e cols rows -> Bool
$c<= :: forall e (cols :: Nat) (rows :: Nat).
Ord e =>
Matrix e cols rows -> Matrix e cols rows -> Bool
< :: Matrix e cols rows -> Matrix e cols rows -> Bool
$c< :: forall e (cols :: Nat) (rows :: Nat).
Ord e =>
Matrix e cols rows -> Matrix e cols rows -> Bool
compare :: Matrix e cols rows -> Matrix e cols rows -> Ordering
$ccompare :: forall e (cols :: Nat) (rows :: Nat).
Ord e =>
Matrix e cols rows -> Matrix e cols rows -> Ordering
$cp1Ord :: forall e (cols :: Nat) (rows :: Nat).
Ord e =>
Eq (Matrix e cols rows)
Ord, Matrix e cols rows -> ()
(Matrix e cols rows -> ()) -> NFData (Matrix e cols rows)
forall a. (a -> ()) -> NFData a
forall e (cols :: Nat) (rows :: Nat).
NFData e =>
Matrix e cols rows -> ()
rnf :: Matrix e cols rows -> ()
$crnf :: forall e (cols :: Nat) (rows :: Nat).
NFData e =>
Matrix e cols rows -> ()
NFData) via (I.Matrix e (I.FromNat cols) (I.FromNat rows))

-- | Constraint type synonyms to keep the type signatures less convoluted
type Countable a        = KnownNat (I.Count a)
type CountableDims a b  = (Countable a, Countable b)
type CountableN a       = KnownNat (I.Count (I.FromNat a))
type CountableNz a      = KnownNat (I.Count (I.Normalize a))
type CountableDimsN a b = (CountableN a, CountableN b)
type FLN e a b          = I.FL (I.FromNat a) (I.FromNat b)
type FLNz e a b         = I.FL (I.Normalize a) (I.Normalize b)
type Liftable e a b     = (Bounded a, Bounded b, Enum a, Enum b, Eq b, Num e, Ord e)
type TrivialE a b       = I.FromNat (a + b) ~ Either (I.FromNat a) (I.FromNat b)
type TrivialP a b       = I.FromNat (a * b) ~ I.FromNat (I.Count (I.FromNat a) * I.Count (I.FromNat b))

-- Primitives

one :: e -> Matrix e 1 1
one :: e -> Matrix e 1 1
one = Matrix e () () -> Matrix e 1 1
forall e (cols :: Nat) (rows :: Nat).
Matrix e (FromNat cols) (FromNat rows) -> Matrix e cols rows
M (Matrix e () () -> Matrix e 1 1)
-> (e -> Matrix e () ()) -> e -> Matrix e 1 1
forall b c a. (b -> c) -> (a -> b) -> a -> c
. e -> Matrix e () ()
forall e. e -> Matrix e () ()
I.One

join ::
  (TrivialE a b) =>
  Matrix e a rows ->
  Matrix e b rows ->
  Matrix e (a + b) rows
join :: Matrix e a rows -> Matrix e b rows -> Matrix e (a + b) rows
join (M Matrix e (FromNat a) (FromNat rows)
a) (M Matrix e (FromNat b) (FromNat rows)
b) = Matrix e (FromNat (a + b)) (FromNat rows) -> Matrix e (a + b) rows
forall e (cols :: Nat) (rows :: Nat).
Matrix e (FromNat cols) (FromNat rows) -> Matrix e cols rows
M (Matrix e (FromNat a) (FromNat rows)
-> Matrix e (FromNat b) (FromNat rows)
-> Matrix e (Either (FromNat a) (FromNat b)) (FromNat rows)
forall e a rows b.
Matrix e a rows -> Matrix e b rows -> Matrix e (Either a b) rows
I.Join Matrix e (FromNat a) (FromNat rows)
a Matrix e (FromNat b) (FromNat rows)
b)

infixl 3 |||
(|||) ::
  (TrivialE a b) =>
  Matrix e a rows ->
  Matrix e b rows ->
  Matrix e (a + b) rows
||| :: Matrix e a rows -> Matrix e b rows -> Matrix e (a + b) rows
(|||) = Matrix e a rows -> Matrix e b rows -> Matrix e (a + b) rows
forall (a :: Nat) (b :: Nat) e (rows :: Nat).
TrivialE a b =>
Matrix e a rows -> Matrix e b rows -> Matrix e (a + b) rows
join

fork ::
  (TrivialE a b) =>
  Matrix e cols a ->
  Matrix e cols b ->
  Matrix e cols (a + b)
fork :: Matrix e cols a -> Matrix e cols b -> Matrix e cols (a + b)
fork (M Matrix e (FromNat cols) (FromNat a)
a) (M Matrix e (FromNat cols) (FromNat b)
b) = Matrix e (FromNat cols) (FromNat (a + b)) -> Matrix e cols (a + b)
forall e (cols :: Nat) (rows :: Nat).
Matrix e (FromNat cols) (FromNat rows) -> Matrix e cols rows
M (Matrix e (FromNat cols) (FromNat a)
-> Matrix e (FromNat cols) (FromNat b)
-> Matrix e (FromNat cols) (Either (FromNat a) (FromNat b))
forall e cols a b.
Matrix e cols a -> Matrix e cols b -> Matrix e cols (Either a b)
I.Fork Matrix e (FromNat cols) (FromNat a)
a Matrix e (FromNat cols) (FromNat b)
b)

infixl 2 ===
(===) ::
  (TrivialE a b) =>
  Matrix e cols a ->
  Matrix e cols b ->
  Matrix e cols (a + b)
=== :: Matrix e cols a -> Matrix e cols b -> Matrix e cols (a + b)
(===) = Matrix e cols a -> Matrix e cols b -> Matrix e cols (a + b)
forall (a :: Nat) (b :: Nat) e (cols :: Nat).
TrivialE a b =>
Matrix e cols a -> Matrix e cols b -> Matrix e cols (a + b)
fork

-- Construction

fromLists :: (FLN e cols rows) => [[e]] -> Matrix e cols rows
fromLists :: [[e]] -> Matrix e cols rows
fromLists = Matrix e (FromNat cols) (FromNat rows) -> Matrix e cols rows
forall e (cols :: Nat) (rows :: Nat).
Matrix e (FromNat cols) (FromNat rows) -> Matrix e cols rows
M (Matrix e (FromNat cols) (FromNat rows) -> Matrix e cols rows)
-> ([[e]] -> Matrix e (FromNat cols) (FromNat rows))
-> [[e]]
-> Matrix e cols rows
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [[e]] -> Matrix e (FromNat cols) (FromNat rows)
forall cols rows e.
FromLists cols rows =>
[[e]] -> Matrix e cols rows
I.fromLists

-- | Matrix builder function. Constructs a matrix provided with
-- a construction function that operates with indices.
matrixBuilder' ::
  (FLN e cols rows, CountableN cols, CountableN rows) 
  => ((Int, Int) -> e) -> Matrix e cols rows
matrixBuilder' :: ((Int, Int) -> e) -> Matrix e cols rows
matrixBuilder' = Matrix e (FromNat cols) (FromNat rows) -> Matrix e cols rows
forall e (cols :: Nat) (rows :: Nat).
Matrix e (FromNat cols) (FromNat rows) -> Matrix e cols rows
M (Matrix e (FromNat cols) (FromNat rows) -> Matrix e cols rows)
-> (((Int, Int) -> e) -> Matrix e (FromNat cols) (FromNat rows))
-> ((Int, Int) -> e)
-> Matrix e cols rows
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ((Int, Int) -> e) -> Matrix e (FromNat cols) (FromNat rows)
forall e cols rows.
(FL cols rows, CountableDims cols rows) =>
((Int, Int) -> e) -> Matrix e cols rows
I.matrixBuilder'

col :: (I.FL () (I.FromNat rows)) => [e] -> Matrix e 1 rows
col :: [e] -> Matrix e 1 rows
col = Matrix e () (FromNat rows) -> Matrix e 1 rows
forall e (cols :: Nat) (rows :: Nat).
Matrix e (FromNat cols) (FromNat rows) -> Matrix e cols rows
M (Matrix e () (FromNat rows) -> Matrix e 1 rows)
-> ([e] -> Matrix e () (FromNat rows)) -> [e] -> Matrix e 1 rows
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [e] -> Matrix e () (FromNat rows)
forall rows e. FL () rows => [e] -> Matrix e () rows
I.col

row :: (I.FL (I.FromNat cols) ()) => [e] -> Matrix e cols 1
row :: [e] -> Matrix e cols 1
row = Matrix e (FromNat cols) () -> Matrix e cols 1
forall e (cols :: Nat) (rows :: Nat).
Matrix e (FromNat cols) (FromNat rows) -> Matrix e cols rows
M (Matrix e (FromNat cols) () -> Matrix e cols 1)
-> ([e] -> Matrix e (FromNat cols) ()) -> [e] -> Matrix e cols 1
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [e] -> Matrix e (FromNat cols) ()
forall cols e. FL cols () => [e] -> Matrix e cols ()
I.row

fromF' ::
  ( Liftable e a b,
    CountableN cols,
    CountableN rows,
    FLN e rows cols
  ) =>
  (a -> b) ->
  Matrix e cols rows
fromF' :: (a -> b) -> Matrix e cols rows
fromF' = Matrix e (FromNat cols) (FromNat rows) -> Matrix e cols rows
forall e (cols :: Nat) (rows :: Nat).
Matrix e (FromNat cols) (FromNat rows) -> Matrix e cols rows
M (Matrix e (FromNat cols) (FromNat rows) -> Matrix e cols rows)
-> ((a -> b) -> Matrix e (FromNat cols) (FromNat rows))
-> (a -> b)
-> Matrix e cols rows
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (a -> b) -> Matrix e (FromNat cols) (FromNat rows)
forall a b cols rows e.
(Liftable e a b, CountableDims cols rows, FL rows cols) =>
(a -> b) -> Matrix e cols rows
I.fromF'

fromF ::
  ( Liftable e a b,
    CountableNz a,
    CountableNz b,
    FLNz e b a
  ) =>
  (a -> b) ->
  Matrix e (I.Count a) (I.Count b)
fromF :: (a -> b) -> Matrix e (Count a) (Count b)
fromF = (a -> b) -> Matrix e (Count a) (Count b)
forall a. HasCallStack => a
undefined -- M . I.fromF

-- Conversion

toLists :: Matrix e cols rows -> [[e]]
toLists :: Matrix e cols rows -> [[e]]
toLists (M Matrix e (FromNat cols) (FromNat rows)
m) = Matrix e (FromNat cols) (FromNat rows) -> [[e]]
forall e cols rows. Matrix e cols rows -> [[e]]
I.toLists Matrix e (FromNat cols) (FromNat rows)
m

toList :: Matrix e cols rows -> [e]
toList :: Matrix e cols rows -> [e]
toList (M Matrix e (FromNat cols) (FromNat rows)
m) = Matrix e (FromNat cols) (FromNat rows) -> [e]
forall e cols rows. Matrix e cols rows -> [e]
I.toList Matrix e (FromNat cols) (FromNat rows)
m

-- Zeros Matrix

zeros ::
  (Num e, FLN e cols rows, CountableN cols, CountableN rows) =>
  Matrix e cols rows
zeros :: Matrix e cols rows
zeros = Matrix e (FromNat cols) (FromNat rows) -> Matrix e cols rows
forall e (cols :: Nat) (rows :: Nat).
Matrix e (FromNat cols) (FromNat rows) -> Matrix e cols rows
M Matrix e (FromNat cols) (FromNat rows)
forall e cols rows.
(Num e, FL cols rows, CountableDims cols rows) =>
Matrix e cols rows
I.zeros

-- Ones Matrix

ones ::
  (Num e, FLN e cols rows, CountableN cols, CountableN rows) =>
  Matrix e cols rows
ones :: Matrix e cols rows
ones = Matrix e (FromNat cols) (FromNat rows) -> Matrix e cols rows
forall e (cols :: Nat) (rows :: Nat).
Matrix e (FromNat cols) (FromNat rows) -> Matrix e cols rows
M Matrix e (FromNat cols) (FromNat rows)
forall e cols rows.
(Num e, FL cols rows, CountableDims cols rows) =>
Matrix e cols rows
I.ones

-- Const Matrix

constant ::
  (Num e, FLN e cols rows, CountableN cols, CountableN rows) =>
  e ->
  Matrix e cols rows
constant :: e -> Matrix e cols rows
constant = Matrix e (FromNat cols) (FromNat rows) -> Matrix e cols rows
forall e (cols :: Nat) (rows :: Nat).
Matrix e (FromNat cols) (FromNat rows) -> Matrix e cols rows
M (Matrix e (FromNat cols) (FromNat rows) -> Matrix e cols rows)
-> (e -> Matrix e (FromNat cols) (FromNat rows))
-> e
-> Matrix e cols rows
forall b c a. (b -> c) -> (a -> b) -> a -> c
. e -> Matrix e (FromNat cols) (FromNat rows)
forall e cols rows.
(Num e, FL cols rows, CountableDims cols rows) =>
e -> Matrix e cols rows
I.constant

-- Bang Matrix

bang ::
  forall e cols.
  (Num e, Enum e, I.FL (I.FromNat cols) (), CountableN cols) =>
  Matrix e cols 1
bang :: Matrix e cols 1
bang = Matrix e (FromNat cols) (FromNat 1) -> Matrix e cols 1
forall e (cols :: Nat) (rows :: Nat).
Matrix e (FromNat cols) (FromNat rows) -> Matrix e cols rows
M Matrix e (FromNat cols) (FromNat 1)
forall e cols.
(Num e, Enum e, FL cols (), Countable cols) =>
Matrix e cols ()
I.bang

-- iden Matrix

iden ::
  (Num e, FLN e cols cols, CountableN cols) =>
  Matrix e cols cols
iden :: Matrix e cols cols
iden = Matrix e (FromNat cols) (FromNat cols) -> Matrix e cols cols
forall e (cols :: Nat) (rows :: Nat).
Matrix e (FromNat cols) (FromNat rows) -> Matrix e cols rows
M Matrix e (FromNat cols) (FromNat cols)
forall e cols.
(Num e, FL cols cols, Countable cols) =>
Matrix e cols cols
I.iden

-- Matrix composition (MMM)

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 (M Matrix e (FromNat cr) (FromNat rows)
a) (M Matrix e (FromNat cols) (FromNat cr)
b) = Matrix e (FromNat cols) (FromNat rows) -> Matrix e cols rows
forall e (cols :: Nat) (rows :: Nat).
Matrix e (FromNat cols) (FromNat rows) -> Matrix e cols rows
M (Matrix e (FromNat cr) (FromNat rows)
-> Matrix e (FromNat cols) (FromNat cr)
-> Matrix e (FromNat cols) (FromNat rows)
forall e cr rows cols.
Num e =>
Matrix e cr rows -> Matrix e cols cr -> Matrix e cols rows
I.comp Matrix e (FromNat cr) (FromNat rows)
a Matrix e (FromNat cols) (FromNat cr)
b)

-- Scalar multiplication of matrices

infixl 7 .|
-- | Scalar multiplication of matrices.
(.|) :: Num e => e -> Matrix e cols rows -> Matrix e cols rows
.| :: e -> Matrix e cols rows -> Matrix e cols rows
(.|) e
e (M Matrix e (FromNat cols) (FromNat rows)
m) = Matrix e (FromNat cols) (FromNat rows) -> Matrix e cols rows
forall e (cols :: Nat) (rows :: Nat).
Matrix e (FromNat cols) (FromNat rows) -> Matrix e cols rows
M (e
e e
-> Matrix e (FromNat cols) (FromNat rows)
-> Matrix e (FromNat cols) (FromNat rows)
forall e cols rows.
Num e =>
e -> Matrix e cols rows -> Matrix e cols rows
I..| Matrix e (FromNat cols) (FromNat rows)
m)

-- Scalar division of matrices

infixl 7 ./
-- | Scalar multiplication of matrices.
(./) :: Fractional e => Matrix e cols rows -> e -> Matrix e cols rows
./ :: Matrix e cols rows -> e -> Matrix e cols rows
(./) (M Matrix e (FromNat cols) (FromNat rows)
m) e
e = Matrix e (FromNat cols) (FromNat rows) -> Matrix e cols rows
forall e (cols :: Nat) (rows :: Nat).
Matrix e (FromNat cols) (FromNat rows) -> Matrix e cols rows
M (Matrix e (FromNat cols) (FromNat rows)
m Matrix e (FromNat cols) (FromNat rows)
-> e -> Matrix e (FromNat cols) (FromNat rows)
forall e cols rows.
Fractional e =>
Matrix e cols rows -> e -> Matrix e cols rows
I../ e
e)

p1 ::
  ( Num e,
    CountableDimsN n m,
    FLN e n m,
    FLN e m m,
    TrivialE m n
  ) =>
  Matrix e (m + n) m
p1 :: Matrix e (m + n) m
p1 = Matrix e (FromNat (m + n)) (FromNat m) -> Matrix e (m + n) m
forall e (cols :: Nat) (rows :: Nat).
Matrix e (FromNat cols) (FromNat rows) -> Matrix e cols rows
M Matrix e (FromNat (m + n)) (FromNat m)
forall e n m.
(Num e, CountableDims n m, FL n m, FL m m) =>
Matrix e (Either m n) m
I.p1

p2 ::
  ( Num e,
    CountableDimsN n m,
    FLN e m n,
    FLN e n n,
    TrivialE m n
  ) =>
  Matrix e (m + n) n
p2 :: Matrix e (m + n) n
p2 = Matrix e (FromNat (m + n)) (FromNat n) -> Matrix e (m + n) n
forall e (cols :: Nat) (rows :: Nat).
Matrix e (FromNat cols) (FromNat rows) -> Matrix e cols rows
M Matrix e (FromNat (m + n)) (FromNat n)
forall e n m.
(Num e, CountableDims n m, FL m n, FL n n) =>
Matrix e (Either m n) n
I.p2

-- Injections

i1 ::
  ( Num e,
    CountableDimsN n rows,
    FLN e n rows,
    FLN e rows rows,
    TrivialE rows n
  ) =>
  Matrix e rows (rows + n)
i1 :: Matrix e rows (rows + n)
i1 = Matrix e (rows + n) rows -> Matrix e rows (rows + n)
forall e (cols :: Nat) (rows :: Nat).
Matrix e cols rows -> Matrix e rows cols
tr Matrix e (rows + n) rows
forall e (n :: Nat) (m :: Nat).
(Num e, CountableDimsN n m, FLN e n m, FLN e m m, TrivialE m n) =>
Matrix e (m + n) m
p1

i2 ::
  ( Num e,
    CountableDimsN rows m,
    FLN e m rows,
    FLN e rows rows,
    TrivialE m rows
  ) =>
  Matrix e rows (m + rows)
i2 :: Matrix e rows (m + rows)
i2 = Matrix e (m + rows) rows -> Matrix e rows (m + rows)
forall e (cols :: Nat) (rows :: Nat).
Matrix e cols rows -> Matrix e rows cols
tr Matrix e (m + rows) rows
forall e (n :: Nat) (m :: Nat).
(Num e, CountableDimsN n m, FLN e m n, FLN e n n, TrivialE m n) =>
Matrix e (m + n) n
p2

-- Dimensions

rows :: (CountableN rows) => Matrix e cols rows -> Int
rows :: Matrix e cols rows -> Int
rows (M Matrix e (FromNat cols) (FromNat rows)
m) = Matrix e (FromNat cols) (FromNat rows) -> Int
forall e cols rows. Countable rows => Matrix e cols rows -> Int
I.rows Matrix e (FromNat cols) (FromNat rows)
m

columns :: (CountableN cols) => Matrix e cols rows -> Int
columns :: Matrix e cols rows -> Int
columns (M Matrix e (FromNat cols) (FromNat rows)
m) = Matrix e (FromNat cols) (FromNat rows) -> Int
forall e cols rows. Countable cols => Matrix e cols rows -> Int
I.columns Matrix e (FromNat cols) (FromNat rows)
m

infixl 5 -|-

-- | Coproduct Bifunctor (Direct sum)
(-|-) ::
  ( Num e,
    CountableDimsN j k,
    FLN e k k,
    FLN e j k,
    FLN e k j,
    FLN e j j,
    TrivialE n m,
    TrivialE k j
  ) =>
  Matrix e n k ->
  Matrix e m j ->
  Matrix e (n + m) (k + j)
-|- :: Matrix e n k -> Matrix e m j -> Matrix e (n + m) (k + j)
(-|-) (M Matrix e (FromNat n) (FromNat k)
a) (M Matrix e (FromNat m) (FromNat j)
b) = Matrix e (FromNat (n + m)) (FromNat (k + j))
-> Matrix e (n + m) (k + j)
forall e (cols :: Nat) (rows :: Nat).
Matrix e (FromNat cols) (FromNat rows) -> Matrix e cols rows
M (Matrix e (FromNat n) (FromNat k)
-> Matrix e (FromNat m) (FromNat j)
-> Matrix
     e (Either (FromNat n) (FromNat m)) (Either (FromNat k) (FromNat j))
forall e n k m j.
(Num e, CountableDims j k, FL k k, FL j k, FL k j, FL j j) =>
Matrix e n k -> Matrix e m j -> Matrix e (Either n m) (Either k j)
(I.-|-) Matrix e (FromNat n) (FromNat k)
a Matrix e (FromNat m) (FromNat j)
b)

-- | Khatri Rao Product first projection
fstM ::
  forall e m k .
  ( Num e,
    CountableDimsN m k,
    CountableN (m * k),
    FLN e (m * k) m,
    TrivialP m k
  ) => Matrix e (m * k) m
fstM :: Matrix e (m * k) m
fstM = Matrix e (FromNat (m * k)) (FromNat m) -> Matrix e (m * k) m
forall e (cols :: Nat) (rows :: Nat).
Matrix e (FromNat cols) (FromNat rows) -> Matrix e cols rows
M ((Num e, CountableDims (FromNat k) (FromNat m),
 FL (Normalize (FromNat m, FromNat k)) (FromNat m),
 CountableN (FromNat m, FromNat k)) =>
Matrix e (Normalize (FromNat m, FromNat k)) (FromNat m)
forall e m k.
(Num e, CountableDims k m, FL (Normalize (m, k)) m,
 CountableN (m, k)) =>
Matrix e (Normalize (m, k)) m
I.fstM @e @(I.FromNat m) @(I.FromNat k))

-- | Khatri Rao Product second projection
sndM ::
    forall e m k.
    ( Num e,
      CountableDimsN k m,
      FLN e (m * k) k,
      CountableN (m * k),
      TrivialP m k
    ) => Matrix e (m * k) k
sndM :: Matrix e (m * k) k
sndM = Matrix e (FromNat (m * k)) (FromNat k) -> Matrix e (m * k) k
forall e (cols :: Nat) (rows :: Nat).
Matrix e (FromNat cols) (FromNat rows) -> Matrix e cols rows
M ((Num e, CountableDims (FromNat k) (FromNat m),
 FL (Normalize (FromNat m, FromNat k)) (FromNat k),
 CountableN (FromNat m, FromNat k)) =>
Matrix e (Normalize (FromNat m, FromNat k)) (FromNat k)
forall e m k.
(Num e, CountableDims k m, FL (Normalize (m, k)) k,
 CountableN (m, k)) =>
Matrix e (Normalize (m, k)) k
I.sndM @e @(I.FromNat m) @(I.FromNat k))

-- | Khatri Rao Product
kr ::
  forall e cols a b.
  ( Num e,
    CountableDimsN a b,
    CountableN (a * b),
    FLN e (a * b) a,
    FLN e (a * b) b,
    TrivialP a b
  ) => Matrix e cols a -> Matrix e cols b -> Matrix e cols (a * b)
kr :: Matrix e cols a -> Matrix e cols b -> Matrix e cols (a * b)
kr Matrix e cols a
a Matrix e cols b
b =
  let fstM' :: Matrix e (a * b) a
fstM' = (Num e, CountableDimsN a b, CountableN (a * b), FLN e (a * b) a,
 TrivialP a b) =>
Matrix e (a * b) a
forall e (m :: Nat) (k :: Nat).
(Num e, CountableDimsN m k, CountableN (m * k), FLN e (m * k) m,
 TrivialP m k) =>
Matrix e (m * k) m
fstM @e @a @b
      sndM' :: Matrix e (a * b) b
sndM' = (Num e, CountableDimsN b a, FLN e (a * b) b, CountableN (a * b),
 TrivialP a b) =>
Matrix e (a * b) b
forall e (m :: Nat) (k :: Nat).
(Num e, CountableDimsN k m, FLN e (m * k) k, CountableN (m * k),
 TrivialP m k) =>
Matrix e (m * k) k
sndM @e @a @b
   in Matrix e a (a * b) -> Matrix e cols a -> Matrix e cols (a * b)
forall e (cr :: Nat) (rows :: Nat) (cols :: Nat).
Num e =>
Matrix e cr rows -> Matrix e cols cr -> Matrix e cols rows
comp (Matrix e (a * b) a -> Matrix e a (a * b)
forall e (cols :: Nat) (rows :: Nat).
Matrix e cols rows -> Matrix e rows cols
tr Matrix e (a * b) a
fstM') Matrix e cols a
a Matrix e cols (a * b)
-> Matrix e cols (a * b) -> Matrix e cols (a * b)
forall a. Num a => a -> a -> a
* Matrix e b (a * b) -> Matrix e cols b -> Matrix e cols (a * b)
forall e (cr :: Nat) (rows :: Nat) (cols :: Nat).
Num e =>
Matrix e cr rows -> Matrix e cols cr -> Matrix e cols rows
comp (Matrix e (a * b) b -> Matrix e b (a * b)
forall e (cols :: Nat) (rows :: Nat).
Matrix e cols rows -> Matrix e rows cols
tr Matrix e (a * b) b
sndM') Matrix e cols b
b

-- | Product Bifunctor (Kronecker)
infixl 4 ><

(><) ::
  forall e m p n q.
  ( Num e,
    CountableDimsN m n,
    CountableDimsN p q,
    CountableDimsN (m * n) (p * q),
    FLN e (m * n) m,
    FLN e (m * n) n,
    FLN e (p * q) p,
    FLN e (p * q) q,
    TrivialP m n,
    TrivialP p q
  ) => Matrix e m p -> Matrix e n q -> Matrix e (m * n) (p * q)
>< :: Matrix e m p -> Matrix e n q -> Matrix e (m * n) (p * q)
(><) Matrix e m p
a Matrix e n q
b =
  let fstM' :: Matrix e (m * n) m
fstM' = (Num e, CountableDimsN m n, CountableN (m * n), FLN e (m * n) m,
 TrivialP m n) =>
Matrix e (m * n) m
forall e (m :: Nat) (k :: Nat).
(Num e, CountableDimsN m k, CountableN (m * k), FLN e (m * k) m,
 TrivialP m k) =>
Matrix e (m * k) m
fstM @e @m @n
      sndM' :: Matrix e (m * n) n
sndM' = (Num e, CountableDimsN n m, FLN e (m * n) n, CountableN (m * n),
 TrivialP m n) =>
Matrix e (m * n) n
forall e (m :: Nat) (k :: Nat).
(Num e, CountableDimsN k m, FLN e (m * k) k, CountableN (m * k),
 TrivialP m k) =>
Matrix e (m * k) k
sndM @e @m @n
   in Matrix e (m * n) p
-> Matrix e (m * n) q -> Matrix e (m * n) (p * q)
forall e (cols :: Nat) (a :: Nat) (b :: Nat).
(Num e, CountableDimsN a b, CountableN (a * b), FLN e (a * b) a,
 FLN e (a * b) b, TrivialP a b) =>
Matrix e cols a -> Matrix e cols b -> Matrix e cols (a * b)
kr (Matrix e m p -> Matrix e (m * n) m -> Matrix e (m * n) p
forall e (cr :: Nat) (rows :: Nat) (cols :: Nat).
Num e =>
Matrix e cr rows -> Matrix e cols cr -> Matrix e cols rows
comp Matrix e m p
a Matrix e (m * n) m
fstM') (Matrix e n q -> Matrix e (m * n) n -> Matrix e (m * n) q
forall e (cr :: Nat) (rows :: Nat) (cols :: Nat).
Num e =>
Matrix e cr rows -> Matrix e cols cr -> Matrix e cols rows
comp Matrix e n q
b Matrix e (m * n) n
sndM')

-- | Matrix abide Join Fork
abideJF :: Matrix e cols rows -> Matrix e cols rows
abideJF :: Matrix e cols rows -> Matrix e cols rows
abideJF (M Matrix e (FromNat cols) (FromNat rows)
m) = Matrix e (FromNat cols) (FromNat rows) -> Matrix e cols rows
forall e (cols :: Nat) (rows :: Nat).
Matrix e (FromNat cols) (FromNat rows) -> Matrix e cols rows
M (Matrix e (FromNat cols) (FromNat rows)
-> Matrix e (FromNat cols) (FromNat rows)
forall e cols rows. Matrix e cols rows -> Matrix e cols rows
I.abideJF Matrix e (FromNat cols) (FromNat rows)
m)

-- | Matrix abide Fork Join
abideFJ :: Matrix e cols rows -> Matrix e cols rows
abideFJ :: Matrix e cols rows -> Matrix e cols rows
abideFJ (M Matrix e (FromNat cols) (FromNat rows)
m) = Matrix e (FromNat cols) (FromNat rows) -> Matrix e cols rows
forall e (cols :: Nat) (rows :: Nat).
Matrix e (FromNat cols) (FromNat rows) -> Matrix e cols rows
M (Matrix e (FromNat cols) (FromNat rows)
-> Matrix e (FromNat cols) (FromNat rows)
forall e cols rows. Matrix e cols rows -> Matrix e cols rows
I.abideFJ Matrix e (FromNat cols) (FromNat rows)
m)

-- | Matrix transposition
tr :: Matrix e cols rows -> Matrix e rows cols
tr :: Matrix e cols rows -> Matrix e rows cols
tr (M Matrix e (FromNat cols) (FromNat rows)
m) = Matrix e (FromNat rows) (FromNat cols) -> Matrix e rows cols
forall e (cols :: Nat) (rows :: Nat).
Matrix e (FromNat cols) (FromNat rows) -> Matrix e cols rows
M (Matrix e (FromNat cols) (FromNat rows)
-> Matrix e (FromNat rows) (FromNat cols)
forall e cols rows. Matrix e cols rows -> Matrix e rows cols
I.tr Matrix e (FromNat cols) (FromNat rows)
m)

-- Selective 'select' operator
select :: 
       ( Num e,
         FLN e rows1 rows1,
         CountableN rows1,
         I.FromNat rows2 ~ I.FromNat rows1,
         I.FromNat cols1 ~ I.FromNat cols2,
         I.FromNat rows3 ~ Either (I.FromNat cols3) (I.FromNat rows1)
       ) => Matrix e cols1 rows3 -> Matrix e cols3 rows1 -> Matrix e cols2 rows2
select :: Matrix e cols1 rows3
-> Matrix e cols3 rows1 -> Matrix e cols2 rows2
select (M Matrix e (FromNat cols1) (FromNat rows3)
m) (M Matrix e (FromNat cols3) (FromNat rows1)
y) = Matrix e (FromNat cols2) (FromNat rows2) -> Matrix e cols2 rows2
forall e (cols :: Nat) (rows :: Nat).
Matrix e (FromNat cols) (FromNat rows) -> Matrix e cols rows
M (Matrix e (FromNat cols2) (Either (FromNat cols3) (FromNat rows1))
-> Matrix e (FromNat cols3) (FromNat rows1)
-> Matrix e (FromNat cols2) (FromNat rows1)
forall e b cols a.
(Num e, FL b b, Countable b) =>
Matrix e cols (Either a b) -> Matrix e a b -> Matrix e cols b
I.select Matrix e (FromNat cols1) (FromNat rows3)
Matrix e (FromNat cols2) (Either (FromNat cols3) (FromNat rows1))
m Matrix e (FromNat cols3) (FromNat rows1)
y)

-- McCarthy's Conditional

cond ::
     ( I.FromNat (I.Count (I.FromNat cols)) ~ I.FromNat cols,
       CountableN cols,
       I.FL () (I.FromNat cols),
       I.FL (I.FromNat cols) (),
       FLN e cols cols,
       Liftable e a Bool
     )
     =>
     (a -> Bool) -> Matrix e cols rows -> Matrix e cols rows -> Matrix e cols rows
cond :: (a -> Bool)
-> Matrix e cols rows -> Matrix e cols rows -> Matrix e cols rows
cond a -> Bool
p (M Matrix e (FromNat cols) (FromNat rows)
a) (M Matrix e (FromNat cols) (FromNat rows)
b) = Matrix e (FromNat cols) (FromNat rows) -> Matrix e cols rows
forall e (cols :: Nat) (rows :: Nat).
Matrix e (FromNat cols) (FromNat rows) -> Matrix e cols rows
M ((a -> Bool)
-> Matrix e (FromNat cols) (FromNat rows)
-> Matrix e (FromNat cols) (FromNat rows)
-> Matrix e (FromNat cols) (FromNat rows)
forall cols a e rows.
(Trivial cols, Countable cols, FL () cols, FL cols (),
 FL cols cols, Bounded a, Enum a, Num e, Ord e) =>
(a -> Bool)
-> Matrix e cols rows -> Matrix e cols rows -> Matrix e cols rows
I.cond a -> Bool
p Matrix e (FromNat cols) (FromNat rows)
a Matrix e (FromNat cols) (FromNat rows)
b)

-- Pretty print

pretty :: (CountableDimsN cols rows, Show e) => Matrix e cols rows -> String
pretty :: Matrix e cols rows -> String
pretty (M Matrix e (FromNat cols) (FromNat rows)
m) = Matrix e (FromNat cols) (FromNat rows) -> String
forall cols rows e.
(CountableDims cols rows, Show e) =>
Matrix e cols rows -> String
I.pretty Matrix e (FromNat cols) (FromNat rows)
m

prettyPrint :: (CountableDimsN cols rows, Show e) => Matrix e cols rows -> IO ()
prettyPrint :: Matrix e cols rows -> IO ()
prettyPrint (M Matrix e (FromNat cols) (FromNat rows)
m) = Matrix e (FromNat cols) (FromNat rows) -> IO ()
forall cols rows e.
(CountableDims cols rows, Show e) =>
Matrix e cols rows -> IO ()
I.prettyPrint Matrix e (FromNat cols) (FromNat rows)
m

-- | Zip two matrices with a given binary function
zipWithM :: (e -> f -> g) -> Matrix e cols rows -> Matrix f cols rows -> Matrix g cols rows
zipWithM :: (e -> f -> g)
-> Matrix e cols rows -> Matrix f cols rows -> Matrix g cols rows
zipWithM e -> f -> g
f (M Matrix e (FromNat cols) (FromNat rows)
a) (M Matrix f (FromNat cols) (FromNat rows)
b) = Matrix g (FromNat cols) (FromNat rows) -> Matrix g cols rows
forall e (cols :: Nat) (rows :: Nat).
Matrix e (FromNat cols) (FromNat rows) -> Matrix e cols rows
M ((e -> f -> g)
-> Matrix e (FromNat cols) (FromNat rows)
-> Matrix f (FromNat cols) (FromNat rows)
-> Matrix g (FromNat cols) (FromNat rows)
forall e f g cols rows.
(e -> f -> g)
-> Matrix e cols rows -> Matrix f cols rows -> Matrix g cols rows
I.zipWithM e -> f -> g
f Matrix e (FromNat cols) (FromNat rows)
a Matrix f (FromNat cols) (FromNat rows)
b)