{-# LANGUAGE CPP #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE GeneralizedNewtypeDeriving #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE FunctionalDependencies #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE EmptyDataDecls #-}
{-# LANGUAGE Rank2Types #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE ViewPatterns #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE TypeFamilies #-}

{-# OPTIONS_GHC -fno-warn-missing-signatures #-}
{-# OPTIONS_GHC -fno-warn-orphans #-}

{- |
Module      :  Numeric.LinearAlgebra.Static
Copyright   :  (c) Alberto Ruiz 2014
License     :  BSD3
Stability   :  experimental

Experimental interface with statically checked dimensions.

See code examples at http://dis.um.es/~alberto/hmatrix/static.html.

-}

module Numeric.LinearAlgebra.Static(
    -- * Vector
       ℝ, R,
    vec2, vec3, vec4, (&), (#), split, headTail,
    vector,
    linspace, range, dim,
    -- * Matrix
    L, Sq, build,
    row, col, (|||),(===), splitRows, splitCols,
    unrow, uncol,
    tr,
    eye,
    diag,
    blockAt,
    matrix,
    -- * Complex
    ℂ, C, M, Her, her, 𝑖,
    toComplex,
    fromComplex,
    complex,
    real,
    imag,
    sqMagnitude,
    magnitude,
    -- * Products
    (<>),(#>),(<.>),
    -- * Linear Systems
    linSolve, (<\>),
    -- * Factorizations
    svd, withCompactSVD, svdTall, svdFlat, Eigen(..),
    withNullspace, withOrth, qr, chol,
    -- * Norms
    Normed(..),
    -- * Random arrays
    Seed, RandDist(..),
    randomVector, rand, randn, gaussianSample, uniformSample,
    -- * Misc
    mean, meanCov,
    Disp(..), Domain(..),
    withVector, withMatrix, exactLength, exactDims,
    toRows, toColumns, withRows, withColumns,
    Sized(..), Diag(..), Sym, sym, mTm, unSym, (<·>)
) where


import GHC.TypeLits
import Numeric.LinearAlgebra hiding (
    (<>),(#>),(<.>),Konst(..),diag, disp,(===),(|||),
    row,col,vector,matrix,linspace,toRows,toColumns,
    (<\>),fromList,takeDiag,svd,eig,eigSH,
    eigenvalues,eigenvaluesSH,build,
    qr,size,dot,chol,range,R,C,sym,mTm,unSym,
    randomVector,rand,randn,gaussianSample,uniformSample,meanCov,
    toComplex, fromComplex, complex, real, magnitude
    )
import qualified Numeric.LinearAlgebra as LA
import qualified Numeric.LinearAlgebra.Devel as LA
import Data.Proxy(Proxy(..))
import Internal.Static
import Control.Arrow((***))
import Text.Printf
import Data.Type.Equality ((:~:)(Refl))
import qualified Data.Bifunctor as BF (first)
#if MIN_VERSION_base(4,11,0)
import Prelude hiding ((<>))
#endif

ud1 :: R n -> Vector ℝ
ud1 :: forall (n :: Nat). R n -> Vector ℝ
ud1 (R (Dim Vector ℝ
v)) = Vector ℝ
v


infixl 4 &
(&) :: forall n . KnownNat n
    => R n -> ℝ -> R (n+1)
R n
u & :: forall (n :: Nat). KnownNat n => R n -> ℝ -> R (n + 1)
& ℝ
x = R n
u forall (n :: Nat) (m :: Nat).
(KnownNat n, KnownNat m) =>
R n -> R m -> R (n + m)
# (forall t s (d :: * -> *). Sized t s d => t -> s
konst ℝ
x :: R 1)

infixl 4 #
(#) :: forall n m . (KnownNat n, KnownNat m)
    => R n -> R m -> R (n+m)
(R Dim n (Vector ℝ)
u) # :: forall (n :: Nat) (m :: Nat).
(KnownNat n, KnownNat m) =>
R n -> R m -> R (n + m)
# (R Dim m (Vector ℝ)
v) = forall (n :: Nat). Dim n (Vector ℝ) -> R n
R (forall (n :: Nat) (m :: Nat) t.
(KnownNat n, KnownNat m, Numeric t) =>
V n t -> V m t -> V (n + m) t
vconcat Dim n (Vector ℝ)
u Dim m (Vector ℝ)
v)



vec2 :: ℝ -> ℝ -> R 2
vec2 :: ℝ -> ℝ -> R 2
vec2 ℝ
a ℝ
b = forall (n :: Nat). Dim n (Vector ℝ) -> R n
R (forall t. Storable t => t -> t -> V 2 t
gvec2 ℝ
a ℝ
b)

vec3 :: ℝ -> ℝ -> ℝ -> R 3
vec3 :: ℝ -> ℝ -> ℝ -> R 3
vec3 ℝ
a ℝ
b ℝ
c = forall (n :: Nat). Dim n (Vector ℝ) -> R n
R (forall t. Storable t => t -> t -> t -> V 3 t
gvec3 ℝ
a ℝ
b ℝ
c)


vec4 :: ℝ -> ℝ -> ℝ -> ℝ -> R 4
vec4 :: ℝ -> ℝ -> ℝ -> ℝ -> R 4
vec4 ℝ
a ℝ
b ℝ
c ℝ
d = forall (n :: Nat). Dim n (Vector ℝ) -> R n
R (forall t. Storable t => t -> t -> t -> t -> V 4 t
gvec4 ℝ
a ℝ
b ℝ
c ℝ
d)

vector :: KnownNat n => [ℝ] -> R n
vector :: forall (n :: Nat). KnownNat n => [ℝ] -> R n
vector = forall t s (d :: * -> *). Sized t s d => [t] -> s
fromList

matrix :: (KnownNat m, KnownNat n) => [ℝ] -> L m n
matrix :: forall (m :: Nat) (n :: Nat).
(KnownNat m, KnownNat n) =>
[ℝ] -> L m n
matrix = forall t s (d :: * -> *). Sized t s d => [t] -> s
fromList

linspace :: forall n . KnownNat n => (ℝ,ℝ) -> R n
linspace :: forall (n :: Nat). KnownNat n => (ℝ, ℝ) -> R n
linspace (ℝ
a,ℝ
b) = R n
v
  where
    v :: R n
v = forall (n :: Nat). Vector ℝ -> R n
mkR (forall e.
(Fractional e, Container Vector e) =>
Int -> (e, e) -> Vector e
LA.linspace (forall t s (d :: * -> *). Sized t s d => s -> IndexOf d
size R n
v) (ℝ
a,ℝ
b))

range :: forall n . KnownNat n => R n
range :: forall (n :: Nat). KnownNat n => R n
range = R n
v
  where
    v :: R n
v = forall (n :: Nat). Vector ℝ -> R n
mkR (forall e.
(Fractional e, Container Vector e) =>
Int -> (e, e) -> Vector e
LA.linspace Int
d (ℝ
1,forall a b. (Integral a, Num b) => a -> b
fromIntegral Int
d))
    d :: Int
d = forall t s (d :: * -> *). Sized t s d => s -> IndexOf d
size R n
v

dim :: forall n . KnownNat n => R n
dim :: forall (n :: Nat). KnownNat n => R n
dim = R n
v
  where
    v :: R n
v = forall (n :: Nat). Vector ℝ -> R n
mkR (forall (c :: * -> *) e. Container c e => e -> c e
scalar (forall a b. (Integral a, Num b) => a -> b
fromIntegral forall a b. (a -> b) -> a -> b
$ forall t s (d :: * -> *). Sized t s d => s -> IndexOf d
size R n
v))

--------------------------------------------------------------------------------


ud2 :: L m n -> Matrix ℝ
ud2 :: forall (m :: Nat) (n :: Nat). L m n -> Matrix ℝ
ud2 (L (Dim (Dim Matrix ℝ
x))) = Matrix ℝ
x


--------------------------------------------------------------------------------

diag :: KnownNat n => R n -> Sq n
diag :: forall (n :: Nat). KnownNat n => R n -> Sq n
diag = forall field (vec :: Nat -> *) (mat :: Nat -> Nat -> *) (m :: Nat)
       (n :: Nat) (k :: Nat).
(Domain field vec mat, KnownNat m, KnownNat n, KnownNat k) =>
field -> vec k -> mat m n
diagR ℝ
0

eye :: KnownNat n => Sq n
eye :: forall (n :: Nat). KnownNat n => Sq n
eye = forall (n :: Nat). KnownNat n => R n -> Sq n
diag R n
1

--------------------------------------------------------------------------------

blockAt :: forall m n . (KnownNat m, KnownNat n) =>  ℝ -> Int -> Int -> Matrix Double -> L m n
blockAt :: forall (m :: Nat) (n :: Nat).
(KnownNat m, KnownNat n) =>
ℝ -> Int -> Int -> Matrix ℝ -> L m n
blockAt ℝ
x Int
r Int
c Matrix ℝ
a = L m n
res
  where
    z :: Matrix ℝ
z = forall (c :: * -> *) e. Container c e => e -> c e
scalar ℝ
x
    z1 :: Matrix ℝ
z1 = forall e d (c :: * -> *). Konst e d c => e -> d -> c e
LA.konst ℝ
x (Int
r,Int
c)
    z2 :: Matrix ℝ
z2 = forall e d (c :: * -> *). Konst e d c => e -> d -> c e
LA.konst ℝ
x (forall a. Ord a => a -> a -> a
max Int
0 (Int
m'forall a. Num a => a -> a -> a
-(Int
raforall a. Num a => a -> a -> a
+Int
r)), forall a. Ord a => a -> a -> a
max Int
0 (Int
n'forall a. Num a => a -> a -> a
-(Int
caforall a. Num a => a -> a -> a
+Int
c)))
    ra :: Int
ra = forall a. Ord a => a -> a -> a
min (forall t. Matrix t -> Int
rows Matrix ℝ
a) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Ord a => a -> a -> a
max Int
0 forall a b. (a -> b) -> a -> b
$ Int
m'forall a. Num a => a -> a -> a
-Int
r
    ca :: Int
ca = forall a. Ord a => a -> a -> a
min (forall t. Matrix t -> Int
cols Matrix ℝ
a) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Ord a => a -> a -> a
max Int
0 forall a b. (a -> b) -> a -> b
$ Int
n'forall a. Num a => a -> a -> a
-Int
c
    sa :: Matrix ℝ
sa = forall a.
Element a =>
(Int, Int) -> (Int, Int) -> Matrix a -> Matrix a
subMatrix (Int
0,Int
0) (Int
ra, Int
ca) Matrix ℝ
a
    (Int
m',Int
n') = forall t s (d :: * -> *). Sized t s d => s -> IndexOf d
size L m n
res
    res :: L m n
res = forall (m :: Nat) (n :: Nat). Matrix ℝ -> L m n
mkL forall a b. (a -> b) -> a -> b
$ forall t. Element t => [[Matrix t]] -> Matrix t
fromBlocks [[Matrix ℝ
z1,Matrix ℝ
z,Matrix ℝ
z],[Matrix ℝ
z,Matrix ℝ
sa,Matrix ℝ
z],[Matrix ℝ
z,Matrix ℝ
z,Matrix ℝ
z2]]

--------------------------------------------------------------------------------


row :: R n -> L 1 n
row :: forall (n :: Nat). R n -> L 1 n
row = forall (m :: Nat) (n :: Nat). Matrix ℝ -> L m n
mkL forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Storable a => Vector a -> Matrix a
asRow forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (n :: Nat). R n -> Vector ℝ
ud1

--col :: R n -> L n 1
col :: R n -> L n 1
col R n
v = forall m mt. Transposable m mt => m -> mt
tr forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (n :: Nat). R n -> L 1 n
row forall a b. (a -> b) -> a -> b
$ R n
v

unrow :: L 1 n -> R n
unrow :: forall (n :: Nat). L 1 n -> R n
unrow = forall (n :: Nat). Vector ℝ -> R n
mkR forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. [a] -> a
head forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall t. Element t => Matrix t -> [Vector t]
LA.toRows forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (m :: Nat) (n :: Nat). L m n -> Matrix ℝ
ud2

--uncol :: L n 1 -> R n
uncol :: L n 1 -> R n
uncol L n 1
v = forall (n :: Nat). L 1 n -> R n
unrow forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall m mt. Transposable m mt => m -> mt
tr forall a b. (a -> b) -> a -> b
$ L n 1
v


infixl 2 ===
(===) :: (KnownNat r1, KnownNat r2, KnownNat c) => L r1 c -> L r2 c -> L (r1+r2) c
L r1 c
a === :: forall (r1 :: Nat) (r2 :: Nat) (c :: Nat).
(KnownNat r1, KnownNat r2, KnownNat c) =>
L r1 c -> L r2 c -> L (r1 + r2) c
=== L r2 c
b = forall (m :: Nat) (n :: Nat). Matrix ℝ -> L m n
mkL (forall t s (d :: * -> *). Sized t s d => s -> d t
extract L r1 c
a forall t. Element t => Matrix t -> Matrix t -> Matrix t
LA.=== forall t s (d :: * -> *). Sized t s d => s -> d t
extract L r2 c
b)


infixl 3 |||
-- (|||) :: (KnownNat r, KnownNat c1, KnownNat c2) => L r c1 -> L r c2 -> L r (c1+c2)
L c r1
a ||| :: L c r1 -> L c r2 -> L c (r1 + r2)
||| L c r2
b = forall m mt. Transposable m mt => m -> mt
tr (forall m mt. Transposable m mt => m -> mt
tr L c r1
a forall (r1 :: Nat) (r2 :: Nat) (c :: Nat).
(KnownNat r1, KnownNat r2, KnownNat c) =>
L r1 c -> L r2 c -> L (r1 + r2) c
=== forall m mt. Transposable m mt => m -> mt
tr L c r2
b)


type Sq n  = L n n
--type CSq n = CL n n


type GL = forall n m . (KnownNat n, KnownNat m) => L m n
type GSq = forall n . KnownNat n => Sq n

isKonst :: forall m n . (KnownNat m, KnownNat n) => L m n -> Maybe (ℝ,(Int,Int))
isKonst :: forall (m :: Nat) (n :: Nat).
(KnownNat m, KnownNat n) =>
L m n -> Maybe (ℝ, (Int, Int))
isKonst s :: L m n
s@(forall t s (d :: * -> *). Sized t s d => s -> d t
unwrap -> Matrix ℝ
x)
    | forall {t}. Matrix t -> Bool
singleM Matrix ℝ
x = forall a. a -> Maybe a
Just (Matrix ℝ
x forall (c :: * -> *) e. Container c e => c e -> IndexOf c -> e
`atIndex` (Int
0,Int
0), (forall t s (d :: * -> *). Sized t s d => s -> IndexOf d
size L m n
s))
    | Bool
otherwise = forall a. Maybe a
Nothing


isKonstC :: forall m n . (KnownNat m, KnownNat n) => M m n -> Maybe (ℂ,(Int,Int))
isKonstC :: forall (m :: Nat) (n :: Nat).
(KnownNat m, KnownNat n) =>
M m n -> Maybe (ℂ, (Int, Int))
isKonstC s :: M m n
s@(forall t s (d :: * -> *). Sized t s d => s -> d t
unwrap -> Matrix ℂ
x)
    | forall {t}. Matrix t -> Bool
singleM Matrix ℂ
x = forall a. a -> Maybe a
Just (Matrix ℂ
x forall (c :: * -> *) e. Container c e => c e -> IndexOf c -> e
`atIndex` (Int
0,Int
0), (forall t s (d :: * -> *). Sized t s d => s -> IndexOf d
size M m n
s))
    | Bool
otherwise = forall a. Maybe a
Nothing


infixr 8 <>
(<>) :: forall m k n. (KnownNat m, KnownNat k, KnownNat n) => L m k -> L k n -> L m n
<> :: forall (m :: Nat) (k :: Nat) (n :: Nat).
(KnownNat m, KnownNat k, KnownNat n) =>
L m k -> L k n -> L m n
(<>) = forall (m :: Nat) (k :: Nat) (n :: Nat).
(KnownNat m, KnownNat k, KnownNat n) =>
L m k -> L k n -> L m n
mulR


infixr 8 #>
(#>) :: (KnownNat m, KnownNat n) => L m n -> R n -> R m
#> :: forall (m :: Nat) (n :: Nat).
(KnownNat m, KnownNat n) =>
L m n -> R n -> R m
(#>) = forall (m :: Nat) (n :: Nat).
(KnownNat m, KnownNat n) =>
L m n -> R n -> R m
appR


infixr 8 <·>
(<·>) :: KnownNat n => R n -> R n -> ℝ
<·> :: forall (n :: Nat). KnownNat n => R n -> R n -> ℝ
(<·>) = forall (n :: Nat). KnownNat n => R n -> R n -> ℝ
dotR

infixr 8 <.>
(<.>) :: KnownNat n => R n -> R n -> ℝ
<.> :: forall (n :: Nat). KnownNat n => R n -> R n -> ℝ
(<.>) = forall (n :: Nat). KnownNat n => R n -> R n -> ℝ
dotR

--------------------------------------------------------------------------------

class Diag m d | m -> d
  where
    takeDiag :: m -> d


instance KnownNat n => Diag (L n n) (R n)
  where
    takeDiag :: L n n -> R n
takeDiag L n n
x = forall (n :: Nat). Vector ℝ -> R n
mkR (forall t. Element t => Matrix t -> Vector t
LA.takeDiag (forall t s (d :: * -> *). Sized t s d => s -> d t
extract L n n
x))


instance KnownNat n => Diag (M n n) (C n)
  where
    takeDiag :: M n n -> C n
takeDiag M n n
x = forall (n :: Nat). Vector ℂ -> C n
mkC (forall t. Element t => Matrix t -> Vector t
LA.takeDiag (forall t s (d :: * -> *). Sized t s d => s -> d t
extract M n n
x))

--------------------------------------------------------------------------------


toComplex :: KnownNat n => (R n, R n) -> C n
toComplex :: forall (n :: Nat). KnownNat n => (R n, R n) -> C n
toComplex (R n
r,R n
i) = forall (n :: Nat). Vector ℂ -> C n
mkC forall a b. (a -> b) -> a -> b
$ forall t (c :: * -> *).
(Convert t, Complexable c, RealElement t) =>
(c t, c t) -> c (Complex t)
LA.toComplex (forall (n :: Nat). R n -> Vector ℝ
ud1 R n
r, forall (n :: Nat). R n -> Vector ℝ
ud1 R n
i)

fromComplex :: KnownNat n => C n -> (R n, R n)
fromComplex :: forall (n :: Nat). KnownNat n => C n -> (R n, R n)
fromComplex (C (Dim Vector ℂ
v)) = let (Vector ℝ
r,Vector ℝ
i) = forall t (c :: * -> *).
(Convert t, Complexable c, RealElement t) =>
c (Complex t) -> (c t, c t)
LA.fromComplex Vector ℂ
v in (forall (n :: Nat). Vector ℝ -> R n
mkR Vector ℝ
r, forall (n :: Nat). Vector ℝ -> R n
mkR Vector ℝ
i)

complex :: KnownNat n => R n -> C n
complex :: forall (n :: Nat). KnownNat n => R n -> C n
complex R n
r = forall (n :: Nat). Vector ℂ -> C n
mkC forall a b. (a -> b) -> a -> b
$ forall t (c :: * -> *).
(Convert t, Complexable c, RealElement t) =>
(c t, c t) -> c (Complex t)
LA.toComplex (forall (n :: Nat). R n -> Vector ℝ
ud1 R n
r, forall e d (c :: * -> *). Konst e d c => e -> d -> c e
LA.konst ℝ
0 (forall t s (d :: * -> *). Sized t s d => s -> IndexOf d
size R n
r))

real :: KnownNat n => C n -> R n
real :: forall (n :: Nat). KnownNat n => C n -> R n
real = forall a b. (a, b) -> a
fst forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (n :: Nat). KnownNat n => C n -> (R n, R n)
fromComplex

imag :: KnownNat n => C n -> R n 
imag :: forall (n :: Nat). KnownNat n => C n -> R n
imag = forall a b. (a, b) -> b
snd forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (n :: Nat). KnownNat n => C n -> (R n, R n)
fromComplex

sqMagnitude :: KnownNat n => C n -> R n
sqMagnitude :: forall (n :: Nat). KnownNat n => C n -> R n
sqMagnitude C n
c = let (R n
r,R n
i) = forall (n :: Nat). KnownNat n => C n -> (R n, R n)
fromComplex C n
c in R n
rforall a. Floating a => a -> a -> a
**R n
2 forall a. Num a => a -> a -> a
+ R n
iforall a. Floating a => a -> a -> a
**R n
2

magnitude :: KnownNat n => C n -> R n
magnitude :: forall (n :: Nat). KnownNat n => C n -> R n
magnitude = forall a. Floating a => a -> a
sqrt forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (n :: Nat). KnownNat n => C n -> R n
sqMagnitude

--------------------------------------------------------------------------------

linSolve :: (KnownNat m, KnownNat n) => L m m -> L m n -> Maybe (L m n)
linSolve :: forall (m :: Nat) (n :: Nat).
(KnownNat m, KnownNat n) =>
L m m -> L m n -> Maybe (L m n)
linSolve (forall t s (d :: * -> *). Sized t s d => s -> d t
extract -> Matrix ℝ
a) (forall t s (d :: * -> *). Sized t s d => s -> d t
extract -> Matrix ℝ
b) = forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall (m :: Nat) (n :: Nat). Matrix ℝ -> L m n
mkL (forall {t}. Field t => Matrix t -> Matrix t -> Maybe (Matrix t)
LA.linearSolve Matrix ℝ
a Matrix ℝ
b)

(<\>) :: (KnownNat m, KnownNat n, KnownNat r) => L m n -> L m r -> L n r
(forall t s (d :: * -> *). Sized t s d => s -> d t
extract -> Matrix ℝ
a) <\> :: forall (m :: Nat) (n :: Nat) (r :: Nat).
(KnownNat m, KnownNat n, KnownNat r) =>
L m n -> L m r -> L n r
<\> (forall t s (d :: * -> *). Sized t s d => s -> d t
extract -> Matrix ℝ
b) = forall (m :: Nat) (n :: Nat). Matrix ℝ -> L m n
mkL (Matrix ℝ
a forall (c :: * -> *) t.
(LSDiv c, Field t) =>
Matrix t -> c t -> c t
LA.<\> Matrix ℝ
b)

svd :: (KnownNat m, KnownNat n) => L m n -> (L m m, R n, L n n)
svd :: forall (m :: Nat) (n :: Nat).
(KnownNat m, KnownNat n) =>
L m n -> (L m m, R n, L n n)
svd (forall t s (d :: * -> *). Sized t s d => s -> d t
extract -> Matrix ℝ
m) = (forall (m :: Nat) (n :: Nat). Matrix ℝ -> L m n
mkL Matrix ℝ
u, forall (n :: Nat). Vector ℝ -> R n
mkR Vector ℝ
s', forall (m :: Nat) (n :: Nat). Matrix ℝ -> L m n
mkL Matrix ℝ
v)
  where
    (Matrix ℝ
u,Vector ℝ
s,Matrix ℝ
v) = forall t. Field t => Matrix t -> (Matrix t, Vector ℝ, Matrix t)
LA.svd Matrix ℝ
m
    s' :: Vector ℝ
s' = forall t. Storable t => [Vector t] -> Vector t
vjoin [Vector ℝ
s, Vector ℝ
z]
    z :: Vector ℝ
z = forall e d (c :: * -> *). Konst e d c => e -> d -> c e
LA.konst ℝ
0 (forall a. Ord a => a -> a -> a
max Int
0 (forall t. Matrix t -> Int
cols Matrix ℝ
m forall a. Num a => a -> a -> a
- forall (c :: * -> *) t. Container c t => c t -> IndexOf c
LA.size Vector ℝ
s))


svdTall :: (KnownNat m, KnownNat n, n <= m) => L m n -> (L m n, R n, L n n)
svdTall :: forall (m :: Nat) (n :: Nat).
(KnownNat m, KnownNat n, n <= m) =>
L m n -> (L m n, R n, L n n)
svdTall (forall t s (d :: * -> *). Sized t s d => s -> d t
extract -> Matrix ℝ
m) = (forall (m :: Nat) (n :: Nat). Matrix ℝ -> L m n
mkL Matrix ℝ
u, forall (n :: Nat). Vector ℝ -> R n
mkR Vector ℝ
s, forall (m :: Nat) (n :: Nat). Matrix ℝ -> L m n
mkL Matrix ℝ
v)
  where
    (Matrix ℝ
u,Vector ℝ
s,Matrix ℝ
v) = forall t. Field t => Matrix t -> (Matrix t, Vector ℝ, Matrix t)
LA.thinSVD Matrix ℝ
m


svdFlat :: (KnownNat m, KnownNat n, m <= n) => L m n -> (L m m, R m, L n m)
svdFlat :: forall (m :: Nat) (n :: Nat).
(KnownNat m, KnownNat n, m <= n) =>
L m n -> (L m m, R m, L n m)
svdFlat (forall t s (d :: * -> *). Sized t s d => s -> d t
extract -> Matrix ℝ
m) = (forall (m :: Nat) (n :: Nat). Matrix ℝ -> L m n
mkL Matrix ℝ
u, forall (n :: Nat). Vector ℝ -> R n
mkR Vector ℝ
s, forall (m :: Nat) (n :: Nat). Matrix ℝ -> L m n
mkL Matrix ℝ
v)
  where
    (Matrix ℝ
u,Vector ℝ
s,Matrix ℝ
v) = forall t. Field t => Matrix t -> (Matrix t, Vector ℝ, Matrix t)
LA.thinSVD Matrix ℝ
m

--------------------------------------------------------------------------------

class Eigen m l v | m -> l, m -> v
  where
    eigensystem :: m -> (l,v)
    eigenvalues :: m -> l

newtype Sym n = Sym (Sq n) deriving Int -> Sym n -> ShowS
forall (n :: Nat). KnownNat n => Int -> Sym n -> ShowS
forall (n :: Nat). KnownNat n => [Sym n] -> ShowS
forall (n :: Nat). KnownNat n => Sym n -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Sym n] -> ShowS
$cshowList :: forall (n :: Nat). KnownNat n => [Sym n] -> ShowS
show :: Sym n -> String
$cshow :: forall (n :: Nat). KnownNat n => Sym n -> String
showsPrec :: Int -> Sym n -> ShowS
$cshowsPrec :: forall (n :: Nat). KnownNat n => Int -> Sym n -> ShowS
Show


sym :: KnownNat n => Sq n -> Sym n
sym :: forall (n :: Nat). KnownNat n => Sq n -> Sym n
sym Sq n
m = forall (n :: Nat). Sq n -> Sym n
Sym forall a b. (a -> b) -> a -> b
$ (Sq n
m forall a. Num a => a -> a -> a
+ forall m mt. Transposable m mt => m -> mt
tr Sq n
m)forall a. Fractional a => a -> a -> a
/Sq n
2

mTm :: (KnownNat m, KnownNat n) => L m n -> Sym n
mTm :: forall (m :: Nat) (n :: Nat).
(KnownNat m, KnownNat n) =>
L m n -> Sym n
mTm L m n
x = forall (n :: Nat). Sq n -> Sym n
Sym (forall m mt. Transposable m mt => m -> mt
tr L m n
x forall (m :: Nat) (k :: Nat) (n :: Nat).
(KnownNat m, KnownNat k, KnownNat n) =>
L m k -> L k n -> L m n
<> L m n
x)

unSym :: Sym n -> Sq n
unSym :: forall (n :: Nat). Sym n -> Sq n
unSym (Sym Sq n
x) = Sq n
x


𝑖 :: Sized ℂ s c => s
𝑖 :: forall s (c :: * -> *). Sized ℂ s c => s
𝑖 = forall t s (d :: * -> *). Sized t s d => t -> s
konst ℂ
iC

newtype Her n = Her (M n n)

her :: KnownNat n => M n n -> Her n
her :: forall (n :: Nat). KnownNat n => M n n -> Her n
her M n n
m = forall (n :: Nat). M n n -> Her n
Her forall a b. (a -> b) -> a -> b
$ (M n n
m forall a. Num a => a -> a -> a
+ forall m mt. Transposable m mt => m -> mt
LA.tr M n n
m)forall a. Fractional a => a -> a -> a
/M n n
2


instance (KnownNat n) => Disp (Sym n)
  where
    disp :: Int -> Sym n -> IO ()
disp Int
n (Sym Sq n
x) = do
        let a :: Matrix ℝ
a = forall t s (d :: * -> *). Sized t s d => s -> d t
extract Sq n
x
        let su :: String
su = Int -> Matrix ℝ -> String
LA.dispf Int
n Matrix ℝ
a
        forall r. PrintfType r => String -> r
printf String
"Sym %d" (forall t. Matrix t -> Int
cols Matrix ℝ
a) forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> String -> IO ()
putStr (forall a. (a -> Bool) -> [a] -> [a]
dropWhile (forall a. Eq a => a -> a -> Bool
/=Char
'\n') forall a b. (a -> b) -> a -> b
$ String
su)

instance (KnownNat n) => Disp (Her n)
  where
    disp :: Int -> Her n -> IO ()
disp Int
n (Her M n n
x) = do
        let a :: Matrix ℂ
a = forall t s (d :: * -> *). Sized t s d => s -> d t
extract M n n
x
        let su :: String
su = Int -> Matrix ℂ -> String
LA.dispcf Int
n Matrix ℂ
a
        forall r. PrintfType r => String -> r
printf String
"Her %d" (forall t. Matrix t -> Int
cols Matrix ℂ
a) forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> String -> IO ()
putStr (forall a. (a -> Bool) -> [a] -> [a]
dropWhile (forall a. Eq a => a -> a -> Bool
/=Char
'\n') forall a b. (a -> b) -> a -> b
$ String
su)


instance KnownNat n => Eigen (Sym n) (R n) (L n n)
  where
    eigenvalues :: Sym n -> R n
eigenvalues (Sym (forall t s (d :: * -> *). Sized t s d => s -> d t
extract -> Matrix ℝ
m)) =  forall (n :: Nat). Vector ℝ -> R n
mkR forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall t. Field t => Herm t -> Vector ℝ
LA.eigenvaluesSH forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall t. Matrix t -> Herm t
LA.trustSym forall a b. (a -> b) -> a -> b
$ Matrix ℝ
m
    eigensystem :: Sym n -> (R n, L n n)
eigensystem (Sym (forall t s (d :: * -> *). Sized t s d => s -> d t
extract -> Matrix ℝ
m)) = (forall (n :: Nat). Vector ℝ -> R n
mkR Vector ℝ
l, forall (m :: Nat) (n :: Nat). Matrix ℝ -> L m n
mkL Matrix ℝ
v)
      where
        (Vector ℝ
l,Matrix ℝ
v) = forall t. Field t => Herm t -> (Vector ℝ, Matrix t)
LA.eigSH forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall t. Matrix t -> Herm t
LA.trustSym forall a b. (a -> b) -> a -> b
$ Matrix ℝ
m

instance KnownNat n => Eigen (Sq n) (C n) (M n n)
  where
    eigenvalues :: Sq n -> C n
eigenvalues (forall t s (d :: * -> *). Sized t s d => s -> d t
extract -> Matrix ℝ
m) = forall (n :: Nat). Vector ℂ -> C n
mkC forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall t. Field t => Matrix t -> Vector ℂ
LA.eigenvalues forall a b. (a -> b) -> a -> b
$ Matrix ℝ
m
    eigensystem :: Sq n -> (C n, M n n)
eigensystem (forall t s (d :: * -> *). Sized t s d => s -> d t
extract -> Matrix ℝ
m) = (forall (n :: Nat). Vector ℂ -> C n
mkC Vector ℂ
l, forall (m :: Nat) (n :: Nat). Matrix ℂ -> M m n
mkM Matrix ℂ
v)
      where
        (Vector ℂ
l,Matrix ℂ
v) = forall t. Field t => Matrix t -> (Vector ℂ, Matrix ℂ)
LA.eig Matrix ℝ
m

chol :: KnownNat n => Sym n -> Sq n
chol :: forall (n :: Nat). KnownNat n => Sym n -> Sq n
chol (forall t s (d :: * -> *). Sized t s d => s -> d t
extract forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (n :: Nat). Sym n -> Sq n
unSym -> Matrix ℝ
m) = forall (m :: Nat) (n :: Nat). Matrix ℝ -> L m n
mkL forall a b. (a -> b) -> a -> b
$ forall t. Field t => Herm t -> Matrix t
LA.chol forall a b. (a -> b) -> a -> b
$ forall t. Matrix t -> Herm t
LA.trustSym Matrix ℝ
m

--------------------------------------------------------------------------------

withNullspace
    :: forall m n z . (KnownNat m, KnownNat n)
    => L m n
    -> (forall k . (KnownNat k) => L n k -> z)
    -> z
withNullspace :: forall (m :: Nat) (n :: Nat) z.
(KnownNat m, KnownNat n) =>
L m n -> (forall (k :: Nat). KnownNat k => L n k -> z) -> z
withNullspace (forall {t}. Field t => Matrix t -> Matrix t
LA.nullspace forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall t s (d :: * -> *). Sized t s d => s -> d t
extract -> Matrix ℝ
a) forall (k :: Nat). KnownNat k => L n k -> z
f =
    case Integer -> Maybe SomeNat
someNatVal forall a b. (a -> b) -> a -> b
$ forall a b. (Integral a, Num b) => a -> b
fromIntegral forall a b. (a -> b) -> a -> b
$ forall t. Matrix t -> Int
cols Matrix ℝ
a of
       Maybe SomeNat
Nothing -> forall a. HasCallStack => String -> a
error String
"static/dynamic mismatch"
       Just (SomeNat (Proxy n
_ :: Proxy k)) -> forall (k :: Nat). KnownNat k => L n k -> z
f (forall (m :: Nat) (n :: Nat). Matrix ℝ -> L m n
mkL Matrix ℝ
a :: L n k)

withOrth
    :: forall m n z . (KnownNat m, KnownNat n)
    => L m n
    -> (forall k. (KnownNat k) => L n k -> z)
    -> z
withOrth :: forall (m :: Nat) (n :: Nat) z.
(KnownNat m, KnownNat n) =>
L m n -> (forall (k :: Nat). KnownNat k => L n k -> z) -> z
withOrth (forall {t}. Field t => Matrix t -> Matrix t
LA.orth forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall t s (d :: * -> *). Sized t s d => s -> d t
extract -> Matrix ℝ
a) forall (k :: Nat). KnownNat k => L n k -> z
f =
    case Integer -> Maybe SomeNat
someNatVal forall a b. (a -> b) -> a -> b
$ forall a b. (Integral a, Num b) => a -> b
fromIntegral forall a b. (a -> b) -> a -> b
$ forall t. Matrix t -> Int
cols Matrix ℝ
a of
       Maybe SomeNat
Nothing -> forall a. HasCallStack => String -> a
error String
"static/dynamic mismatch"
       Just (SomeNat (Proxy n
_ :: Proxy k)) -> forall (k :: Nat). KnownNat k => L n k -> z
f (forall (m :: Nat) (n :: Nat). Matrix ℝ -> L m n
mkL Matrix ℝ
a :: L n k)

withCompactSVD
    :: forall m n z . (KnownNat m, KnownNat n)
    => L m n
    -> (forall k . (KnownNat k) => (L m k, R k, L n k) -> z)
    -> z
withCompactSVD :: forall (m :: Nat) (n :: Nat) z.
(KnownNat m, KnownNat n) =>
L m n
-> (forall (k :: Nat). KnownNat k => (L m k, R k, L n k) -> z) -> z
withCompactSVD (forall t. Field t => Matrix t -> (Matrix t, Vector ℝ, Matrix t)
LA.compactSVD forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall t s (d :: * -> *). Sized t s d => s -> d t
extract -> (Matrix ℝ
u,Vector ℝ
s,Matrix ℝ
v)) forall (k :: Nat). KnownNat k => (L m k, R k, L n k) -> z
f =
    case Integer -> Maybe SomeNat
someNatVal forall a b. (a -> b) -> a -> b
$ forall a b. (Integral a, Num b) => a -> b
fromIntegral forall a b. (a -> b) -> a -> b
$ forall (c :: * -> *) t. Container c t => c t -> IndexOf c
LA.size Vector ℝ
s of
       Maybe SomeNat
Nothing -> forall a. HasCallStack => String -> a
error String
"static/dynamic mismatch"
       Just (SomeNat (Proxy n
_ :: Proxy k)) -> forall (k :: Nat). KnownNat k => (L m k, R k, L n k) -> z
f (forall (m :: Nat) (n :: Nat). Matrix ℝ -> L m n
mkL Matrix ℝ
u :: L m k, forall (n :: Nat). Vector ℝ -> R n
mkR Vector ℝ
s :: R k, forall (m :: Nat) (n :: Nat). Matrix ℝ -> L m n
mkL Matrix ℝ
v :: L n k)

--------------------------------------------------------------------------------

qr :: (KnownNat m, KnownNat n) => L m n -> (L m m, L m n)
qr :: forall (m :: Nat) (n :: Nat).
(KnownNat m, KnownNat n) =>
L m n -> (L m m, L m n)
qr (forall t s (d :: * -> *). Sized t s d => s -> d t
extract -> Matrix ℝ
x) = (forall (m :: Nat) (n :: Nat). Matrix ℝ -> L m n
mkL Matrix ℝ
q, forall (m :: Nat) (n :: Nat). Matrix ℝ -> L m n
mkL Matrix ℝ
r)
  where
    (Matrix ℝ
q,Matrix ℝ
r) = forall t. Field t => Matrix t -> (Matrix t, Matrix t)
LA.qr Matrix ℝ
x

-- use qrRaw?

--------------------------------------------------------------------------------

split :: forall p n . (KnownNat p, KnownNat n, p<=n) => R n -> (R p, R (n-p))
split :: forall (p :: Nat) (n :: Nat).
(KnownNat p, KnownNat n, p <= n) =>
R n -> (R p, R (n - p))
split (forall t s (d :: * -> *). Sized t s d => s -> d t
extract -> Vector ℝ
v) = ( forall (n :: Nat). Vector ℝ -> R n
mkR (forall t. Storable t => Int -> Int -> Vector t -> Vector t
subVector Int
0 Int
p' Vector ℝ
v) ,
                         forall (n :: Nat). Vector ℝ -> R n
mkR (forall t. Storable t => Int -> Int -> Vector t -> Vector t
subVector Int
p' (forall (c :: * -> *) t. Container c t => c t -> IndexOf c
LA.size Vector ℝ
v forall a. Num a => a -> a -> a
- Int
p') Vector ℝ
v) )
  where
    p' :: Int
p' = forall a b. (Integral a, Num b) => a -> b
fromIntegral forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (n :: Nat) (proxy :: Nat -> *).
KnownNat n =>
proxy n -> Integer
natVal forall a b. (a -> b) -> a -> b
$ (forall a. HasCallStack => a
undefined :: Proxy p) :: Int


headTail :: (KnownNat n, 1<=n) => R n -> (ℝ, R (n-1))
headTail :: forall (n :: Nat). (KnownNat n, 1 <= n) => R n -> (ℝ, R (n - 1))
headTail = ((forall c t. Indexable c t => c -> Int -> t
! Int
0) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall t s (d :: * -> *). Sized t s d => s -> d t
extract forall (a :: * -> * -> *) b c b' c'.
Arrow a =>
a b c -> a b' c' -> a (b, b') (c, c')
*** forall a. a -> a
id) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (p :: Nat) (n :: Nat).
(KnownNat p, KnownNat n, p <= n) =>
R n -> (R p, R (n - p))
split


splitRows :: forall p m n . (KnownNat p, KnownNat m, KnownNat n, p<=m) => L m n -> (L p n, L (m-p) n)
splitRows :: forall (p :: Nat) (m :: Nat) (n :: Nat).
(KnownNat p, KnownNat m, KnownNat n, p <= m) =>
L m n -> (L p n, L (m - p) n)
splitRows (forall t s (d :: * -> *). Sized t s d => s -> d t
extract -> Matrix ℝ
x) = ( forall (m :: Nat) (n :: Nat). Matrix ℝ -> L m n
mkL (forall t. Element t => Int -> Matrix t -> Matrix t
takeRows Int
p' Matrix ℝ
x) ,
                             forall (m :: Nat) (n :: Nat). Matrix ℝ -> L m n
mkL (forall t. Element t => Int -> Matrix t -> Matrix t
dropRows Int
p' Matrix ℝ
x) )
  where
    p' :: Int
p' = forall a b. (Integral a, Num b) => a -> b
fromIntegral forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (n :: Nat) (proxy :: Nat -> *).
KnownNat n =>
proxy n -> Integer
natVal forall a b. (a -> b) -> a -> b
$ (forall a. HasCallStack => a
undefined :: Proxy p) :: Int

splitCols :: forall p m n. (KnownNat p, KnownNat m, KnownNat n, KnownNat (n-p), p<=n) => L m n -> (L m p, L m (n-p))
splitCols :: forall (p :: Nat) (m :: Nat) (n :: Nat).
(KnownNat p, KnownNat m, KnownNat n, KnownNat (n - p), p <= n) =>
L m n -> (L m p, L m (n - p))
splitCols = (forall m mt. Transposable m mt => m -> mt
tr forall (a :: * -> * -> *) b c b' c'.
Arrow a =>
a b c -> a b' c' -> a (b, b') (c, c')
*** forall m mt. Transposable m mt => m -> mt
tr) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (p :: Nat) (m :: Nat) (n :: Nat).
(KnownNat p, KnownNat m, KnownNat n, p <= m) =>
L m n -> (L p n, L (m - p) n)
splitRows forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall m mt. Transposable m mt => m -> mt
tr


toRows :: forall m n . (KnownNat m, KnownNat n) => L m n -> [R n]
toRows :: forall (m :: Nat) (n :: Nat).
(KnownNat m, KnownNat n) =>
L m n -> [R n]
toRows (forall t. Element t => Matrix t -> [Vector t]
LA.toRows forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall t s (d :: * -> *). Sized t s d => s -> d t
extract -> [Vector ℝ]
vs) = forall a b. (a -> b) -> [a] -> [b]
map forall (n :: Nat). Vector ℝ -> R n
mkR [Vector ℝ]
vs

withRows
    :: forall n z . KnownNat n
    => [R n]
    -> (forall m . KnownNat m => L m n -> z)
    -> z
withRows :: forall (n :: Nat) z.
KnownNat n =>
[R n] -> (forall (m :: Nat). KnownNat m => L m n -> z) -> z
withRows (forall t. Element t => [Vector t] -> Matrix t
LA.fromRows forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a -> b) -> [a] -> [b]
map forall t s (d :: * -> *). Sized t s d => s -> d t
extract -> Matrix ℝ
m) forall (m :: Nat). KnownNat m => L m n -> z
f =
    case Integer -> Maybe SomeNat
someNatVal forall a b. (a -> b) -> a -> b
$ forall a b. (Integral a, Num b) => a -> b
fromIntegral forall a b. (a -> b) -> a -> b
$ forall t. Matrix t -> Int
LA.rows Matrix ℝ
m of
       Maybe SomeNat
Nothing -> forall a. HasCallStack => String -> a
error String
"static/dynamic mismatch"
       Just (SomeNat (Proxy n
_ :: Proxy m)) -> forall (m :: Nat). KnownNat m => L m n -> z
f (forall (m :: Nat) (n :: Nat). Matrix ℝ -> L m n
mkL Matrix ℝ
m :: L m n)

toColumns :: forall m n . (KnownNat m, KnownNat n) => L m n -> [R m]
toColumns :: forall (m :: Nat) (n :: Nat).
(KnownNat m, KnownNat n) =>
L m n -> [R m]
toColumns (forall t. Element t => Matrix t -> [Vector t]
LA.toColumns forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall t s (d :: * -> *). Sized t s d => s -> d t
extract -> [Vector ℝ]
vs) = forall a b. (a -> b) -> [a] -> [b]
map forall (n :: Nat). Vector ℝ -> R n
mkR [Vector ℝ]
vs

withColumns
    :: forall m z . KnownNat m
    => [R m]
    -> (forall n . KnownNat n => L m n -> z)
    -> z
withColumns :: forall (m :: Nat) z.
KnownNat m =>
[R m] -> (forall (n :: Nat). KnownNat n => L m n -> z) -> z
withColumns (forall t. Element t => [Vector t] -> Matrix t
LA.fromColumns forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a -> b) -> [a] -> [b]
map forall t s (d :: * -> *). Sized t s d => s -> d t
extract -> Matrix ℝ
m) forall (n :: Nat). KnownNat n => L m n -> z
f =
    case Integer -> Maybe SomeNat
someNatVal forall a b. (a -> b) -> a -> b
$ forall a b. (Integral a, Num b) => a -> b
fromIntegral forall a b. (a -> b) -> a -> b
$ forall t. Matrix t -> Int
LA.cols Matrix ℝ
m of
       Maybe SomeNat
Nothing -> forall a. HasCallStack => String -> a
error String
"static/dynamic mismatch"
       Just (SomeNat (Proxy n
_ :: Proxy n)) -> forall (n :: Nat). KnownNat n => L m n -> z
f (forall (m :: Nat) (n :: Nat). Matrix ℝ -> L m n
mkL Matrix ℝ
m :: L m n)



--------------------------------------------------------------------------------

build
  :: forall m n . (KnownNat n, KnownNat m)
    => (ℝ -> ℝ -> ℝ)
    -> L m n
build :: forall (m :: Nat) (n :: Nat).
(KnownNat n, KnownNat m) =>
(ℝ -> ℝ -> ℝ) -> L m n
build ℝ -> ℝ -> ℝ
f = L m n
r
  where
    r :: L m n
r = forall (m :: Nat) (n :: Nat). Matrix ℝ -> L m n
mkL forall a b. (a -> b) -> a -> b
$ forall d f (c :: * -> *) e. Build d f c e => d -> f -> c e
LA.build (forall t s (d :: * -> *). Sized t s d => s -> IndexOf d
size L m n
r) ℝ -> ℝ -> ℝ
f

--------------------------------------------------------------------------------

withVector
    :: forall z
     . Vector ℝ
    -> (forall n . (KnownNat n) => R n -> z)
    -> z
withVector :: forall z.
Vector ℝ -> (forall (n :: Nat). KnownNat n => R n -> z) -> z
withVector Vector ℝ
v forall (n :: Nat). KnownNat n => R n -> z
f =
    case Integer -> Maybe SomeNat
someNatVal forall a b. (a -> b) -> a -> b
$ forall a b. (Integral a, Num b) => a -> b
fromIntegral forall a b. (a -> b) -> a -> b
$ forall (c :: * -> *) t. Container c t => c t -> IndexOf c
LA.size Vector ℝ
v of
       Maybe SomeNat
Nothing -> forall a. HasCallStack => String -> a
error String
"static/dynamic mismatch"
       Just (SomeNat (Proxy n
_ :: Proxy m)) -> forall (n :: Nat). KnownNat n => R n -> z
f (forall (n :: Nat). Vector ℝ -> R n
mkR Vector ℝ
v :: R m)

-- | Useful for constraining two dependently typed vectors to match each
-- other in length when they are unknown at compile-time.
exactLength
    :: forall n m . (KnownNat n, KnownNat m)
    => R m
    -> Maybe (R n)
exactLength :: forall (n :: Nat) (m :: Nat).
(KnownNat n, KnownNat m) =>
R m -> Maybe (R n)
exactLength R m
v = do
    n :~: m
Refl <- forall (a :: Nat) (b :: Nat) (proxy1 :: Nat -> *)
       (proxy2 :: Nat -> *).
(KnownNat a, KnownNat b) =>
proxy1 a -> proxy2 b -> Maybe (a :~: b)
sameNat (forall {k} (t :: k). Proxy t
Proxy :: Proxy n) (forall {k} (t :: k). Proxy t
Proxy :: Proxy m)
    forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall (n :: Nat). Vector ℝ -> R n
mkR (forall t s (d :: * -> *). Sized t s d => s -> d t
unwrap R m
v)

withMatrix
    :: forall z
     . Matrix ℝ
    -> (forall m n . (KnownNat m, KnownNat n) => L m n -> z)
    -> z
withMatrix :: forall z.
Matrix ℝ
-> (forall (m :: Nat) (n :: Nat).
    (KnownNat m, KnownNat n) =>
    L m n -> z)
-> z
withMatrix Matrix ℝ
a forall (m :: Nat) (n :: Nat).
(KnownNat m, KnownNat n) =>
L m n -> z
f =
    case Integer -> Maybe SomeNat
someNatVal forall a b. (a -> b) -> a -> b
$ forall a b. (Integral a, Num b) => a -> b
fromIntegral forall a b. (a -> b) -> a -> b
$ forall t. Matrix t -> Int
rows Matrix ℝ
a of
       Maybe SomeNat
Nothing -> forall a. HasCallStack => String -> a
error String
"static/dynamic mismatch"
       Just (SomeNat (Proxy n
_ :: Proxy m)) ->
           case Integer -> Maybe SomeNat
someNatVal forall a b. (a -> b) -> a -> b
$ forall a b. (Integral a, Num b) => a -> b
fromIntegral forall a b. (a -> b) -> a -> b
$ forall t. Matrix t -> Int
cols Matrix ℝ
a of
               Maybe SomeNat
Nothing -> forall a. HasCallStack => String -> a
error String
"static/dynamic mismatch"
               Just (SomeNat (Proxy n
_ :: Proxy n)) ->
                  forall (m :: Nat) (n :: Nat).
(KnownNat m, KnownNat n) =>
L m n -> z
f (forall (m :: Nat) (n :: Nat). Matrix ℝ -> L m n
mkL Matrix ℝ
a :: L m n)

-- | Useful for constraining two dependently typed matrices to match each
-- other in dimensions when they are unknown at compile-time.
exactDims
    :: forall n m j k . (KnownNat n, KnownNat m, KnownNat j, KnownNat k)
    => L m n
    -> Maybe (L j k)
exactDims :: forall (n :: Nat) (m :: Nat) (j :: Nat) (k :: Nat).
(KnownNat n, KnownNat m, KnownNat j, KnownNat k) =>
L m n -> Maybe (L j k)
exactDims L m n
m = do
    m :~: j
Refl <- forall (a :: Nat) (b :: Nat) (proxy1 :: Nat -> *)
       (proxy2 :: Nat -> *).
(KnownNat a, KnownNat b) =>
proxy1 a -> proxy2 b -> Maybe (a :~: b)
sameNat (forall {k} (t :: k). Proxy t
Proxy :: Proxy m) (forall {k} (t :: k). Proxy t
Proxy :: Proxy j)
    n :~: k
Refl <- forall (a :: Nat) (b :: Nat) (proxy1 :: Nat -> *)
       (proxy2 :: Nat -> *).
(KnownNat a, KnownNat b) =>
proxy1 a -> proxy2 b -> Maybe (a :~: b)
sameNat (forall {k} (t :: k). Proxy t
Proxy :: Proxy n) (forall {k} (t :: k). Proxy t
Proxy :: Proxy k)
    forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall (m :: Nat) (n :: Nat). Matrix ℝ -> L m n
mkL (forall t s (d :: * -> *). Sized t s d => s -> d t
unwrap L m n
m)

randomVector
    :: forall n . KnownNat n
    => Seed
    -> RandDist
    -> R n
randomVector :: forall (n :: Nat). KnownNat n => Int -> RandDist -> R n
randomVector Int
s RandDist
d = forall (n :: Nat). Vector ℝ -> R n
mkR (Int -> RandDist -> Int -> Vector ℝ
LA.randomVector Int
s RandDist
d
                          (forall a. Num a => Integer -> a
fromInteger (forall (n :: Nat) (proxy :: Nat -> *).
KnownNat n =>
proxy n -> Integer
natVal (forall {k} (t :: k). Proxy t
Proxy :: Proxy n)))
                       )

rand
    :: forall m n . (KnownNat m, KnownNat n)
    => IO (L m n)
rand :: forall (m :: Nat) (n :: Nat).
(KnownNat m, KnownNat n) =>
IO (L m n)
rand = forall (m :: Nat) (n :: Nat). Matrix ℝ -> L m n
mkL forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Int -> Int -> IO (Matrix ℝ)
LA.rand (forall a. Num a => Integer -> a
fromInteger (forall (n :: Nat) (proxy :: Nat -> *).
KnownNat n =>
proxy n -> Integer
natVal (forall {k} (t :: k). Proxy t
Proxy :: Proxy m)))
                       (forall a. Num a => Integer -> a
fromInteger (forall (n :: Nat) (proxy :: Nat -> *).
KnownNat n =>
proxy n -> Integer
natVal (forall {k} (t :: k). Proxy t
Proxy :: Proxy n)))

randn
    :: forall m n . (KnownNat m, KnownNat n)
    => IO (L m n)
randn :: forall (m :: Nat) (n :: Nat).
(KnownNat m, KnownNat n) =>
IO (L m n)
randn = forall (m :: Nat) (n :: Nat). Matrix ℝ -> L m n
mkL forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Int -> Int -> IO (Matrix ℝ)
LA.randn (forall a. Num a => Integer -> a
fromInteger (forall (n :: Nat) (proxy :: Nat -> *).
KnownNat n =>
proxy n -> Integer
natVal (forall {k} (t :: k). Proxy t
Proxy :: Proxy m)))
                         (forall a. Num a => Integer -> a
fromInteger (forall (n :: Nat) (proxy :: Nat -> *).
KnownNat n =>
proxy n -> Integer
natVal (forall {k} (t :: k). Proxy t
Proxy :: Proxy n)))

gaussianSample
    :: forall m n . (KnownNat m, KnownNat n)
    => Seed
    -> R n
    -> Sym n
    -> L m n
gaussianSample :: forall (m :: Nat) (n :: Nat).
(KnownNat m, KnownNat n) =>
Int -> R n -> Sym n -> L m n
gaussianSample Int
s (forall t s (d :: * -> *). Sized t s d => s -> d t
extract -> Vector ℝ
mu) (Sym (forall t s (d :: * -> *). Sized t s d => s -> d t
extract -> Matrix ℝ
sigma)) =
    forall (m :: Nat) (n :: Nat). Matrix ℝ -> L m n
mkL forall a b. (a -> b) -> a -> b
$ Int -> Int -> Vector ℝ -> Herm ℝ -> Matrix ℝ
LA.gaussianSample Int
s (forall a. Num a => Integer -> a
fromInteger (forall (n :: Nat) (proxy :: Nat -> *).
KnownNat n =>
proxy n -> Integer
natVal (forall {k} (t :: k). Proxy t
Proxy :: Proxy m)))
                            Vector ℝ
mu (forall t. Matrix t -> Herm t
LA.trustSym Matrix ℝ
sigma)

uniformSample
    :: forall m n . (KnownNat m, KnownNat n)
    => Seed
    -> R n    -- ^ minimums of each row
    -> R n    -- ^ maximums of each row
    -> L m n
uniformSample :: forall (m :: Nat) (n :: Nat).
(KnownNat m, KnownNat n) =>
Int -> R n -> R n -> L m n
uniformSample Int
s (forall t s (d :: * -> *). Sized t s d => s -> d t
extract -> Vector ℝ
mins) (forall t s (d :: * -> *). Sized t s d => s -> d t
extract -> Vector ℝ
maxs) =
    forall (m :: Nat) (n :: Nat). Matrix ℝ -> L m n
mkL forall a b. (a -> b) -> a -> b
$ Int -> Int -> [(ℝ, ℝ)] -> Matrix ℝ
LA.uniformSample Int
s (forall a. Num a => Integer -> a
fromInteger (forall (n :: Nat) (proxy :: Nat -> *).
KnownNat n =>
proxy n -> Integer
natVal (forall {k} (t :: k). Proxy t
Proxy :: Proxy m)))
                           (forall a b. [a] -> [b] -> [(a, b)]
zip (forall a. Storable a => Vector a -> [a]
LA.toList Vector ℝ
mins) (forall a. Storable a => Vector a -> [a]
LA.toList Vector ℝ
maxs))

meanCov
    :: forall m n . (KnownNat m, KnownNat n, 1 <= m)
    => L m n
    -> (R n, Sym n)
meanCov :: forall (m :: Nat) (n :: Nat).
(KnownNat m, KnownNat n, 1 <= m) =>
L m n -> (R n, Sym n)
meanCov (forall t s (d :: * -> *). Sized t s d => s -> d t
extract -> Matrix ℝ
vs) = forall (n :: Nat). Vector ℝ -> R n
mkR forall (a :: * -> * -> *) b c b' c'.
Arrow a =>
a b c -> a b' c' -> a (b, b') (c, c')
*** (forall (n :: Nat). Sq n -> Sym n
Sym forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (m :: Nat) (n :: Nat). Matrix ℝ -> L m n
mkL forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall t. Herm t -> Matrix t
LA.unSym) forall a b. (a -> b) -> a -> b
$ Matrix ℝ -> (Vector ℝ, Herm ℝ)
LA.meanCov Matrix ℝ
vs

--------------------------------------------------------------------------------

class Domain field vec mat | mat -> vec field, vec -> mat field, field -> mat vec
  where
    mul :: forall m k n. (KnownNat m, KnownNat k, KnownNat n) => mat m k -> mat k n -> mat m n
    app :: forall m n . (KnownNat m, KnownNat n) => mat m n -> vec n -> vec m
    dot :: forall n . (KnownNat n) => vec n -> vec n -> field
    cross :: vec 3 -> vec 3 -> vec 3
    diagR ::  forall m n k . (KnownNat m, KnownNat n, KnownNat k) => field -> vec k -> mat m n
    dvmap :: forall n. KnownNat n => (field -> field) -> vec n -> vec n
    dmmap :: forall n m. (KnownNat m, KnownNat n) => (field -> field) -> mat n m -> mat n m
    outer :: forall n m. (KnownNat m, KnownNat n) => vec n -> vec m -> mat n m
    zipWithVector :: forall n. KnownNat n => (field -> field -> field) -> vec n -> vec n -> vec n
    det :: forall n. KnownNat n => mat n n -> field
    invlndet :: forall n. KnownNat n => mat n n -> (mat n n, (field, field))
    expm :: forall n. KnownNat n => mat n n -> mat n n
    sqrtm :: forall n. KnownNat n => mat n n -> mat n n
    inv :: forall n. KnownNat n => mat n n -> mat n n


instance Domain ℝ R L
  where
    mul :: forall (m :: Nat) (k :: Nat) (n :: Nat).
(KnownNat m, KnownNat k, KnownNat n) =>
L m k -> L k n -> L m n
mul = forall (m :: Nat) (k :: Nat) (n :: Nat).
(KnownNat m, KnownNat k, KnownNat n) =>
L m k -> L k n -> L m n
mulR
    app :: forall (m :: Nat) (n :: Nat).
(KnownNat m, KnownNat n) =>
L m n -> R n -> R m
app = forall (m :: Nat) (n :: Nat).
(KnownNat m, KnownNat n) =>
L m n -> R n -> R m
appR
    dot :: forall (n :: Nat). KnownNat n => R n -> R n -> ℝ
dot = forall (n :: Nat). KnownNat n => R n -> R n -> ℝ
dotR
    cross :: R 3 -> R 3 -> R 3
cross = R 3 -> R 3 -> R 3
crossR
    diagR :: forall (m :: Nat) (n :: Nat) (k :: Nat).
(KnownNat m, KnownNat n, KnownNat k) =>
ℝ -> R k -> L m n
diagR = forall (m :: Nat) (n :: Nat) (k :: Nat).
(KnownNat m, KnownNat n, KnownNat k) =>
ℝ -> R k -> L m n
diagRectR
    dvmap :: forall (n :: Nat). KnownNat n => (ℝ -> ℝ) -> R n -> R n
dvmap = forall (n :: Nat). KnownNat n => (ℝ -> ℝ) -> R n -> R n
mapR
    dmmap :: forall (n :: Nat) (m :: Nat).
(KnownNat m, KnownNat n) =>
(ℝ -> ℝ) -> L n m -> L n m
dmmap = forall (n :: Nat) (m :: Nat).
(KnownNat n, KnownNat m) =>
(ℝ -> ℝ) -> L n m -> L n m
mapL
    outer :: forall (n :: Nat) (m :: Nat).
(KnownNat m, KnownNat n) =>
R n -> R m -> L n m
outer = forall (m :: Nat) (n :: Nat).
(KnownNat m, KnownNat n) =>
R n -> R m -> L n m
outerR
    zipWithVector :: forall (n :: Nat). KnownNat n => (ℝ -> ℝ -> ℝ) -> R n -> R n -> R n
zipWithVector = forall (n :: Nat). KnownNat n => (ℝ -> ℝ -> ℝ) -> R n -> R n -> R n
zipWithR
    det :: forall (n :: Nat). KnownNat n => L n n -> ℝ
det = forall (n :: Nat). KnownNat n => L n n -> ℝ
detL
    invlndet :: forall (n :: Nat). KnownNat n => L n n -> (L n n, (ℝ, ℝ))
invlndet = forall (n :: Nat). KnownNat n => L n n -> (L n n, (ℝ, ℝ))
invlndetL
    expm :: forall (n :: Nat). KnownNat n => L n n -> L n n
expm = forall (n :: Nat). KnownNat n => L n n -> L n n
expmL
    sqrtm :: forall (n :: Nat). KnownNat n => L n n -> L n n
sqrtm = forall (n :: Nat). KnownNat n => L n n -> L n n
sqrtmL
    inv :: forall (n :: Nat). KnownNat n => L n n -> L n n
inv = forall (n :: Nat). KnownNat n => L n n -> L n n
invL

instance Domain ℂ C M
  where
    mul :: forall (m :: Nat) (k :: Nat) (n :: Nat).
(KnownNat m, KnownNat k, KnownNat n) =>
M m k -> M k n -> M m n
mul = forall (m :: Nat) (k :: Nat) (n :: Nat).
(KnownNat m, KnownNat k, KnownNat n) =>
M m k -> M k n -> M m n
mulC
    app :: forall (m :: Nat) (n :: Nat).
(KnownNat m, KnownNat n) =>
M m n -> C n -> C m
app = forall (m :: Nat) (n :: Nat).
(KnownNat m, KnownNat n) =>
M m n -> C n -> C m
appC
    dot :: forall (n :: Nat). KnownNat n => C n -> C n -> ℂ
dot = forall (n :: Nat). KnownNat n => C n -> C n -> ℂ
dotC
    cross :: C 3 -> C 3 -> C 3
cross = C 3 -> C 3 -> C 3
crossC
    diagR :: forall (m :: Nat) (n :: Nat) (k :: Nat).
(KnownNat m, KnownNat n, KnownNat k) =>
ℂ -> C k -> M m n
diagR = forall (m :: Nat) (n :: Nat) (k :: Nat).
(KnownNat m, KnownNat n, KnownNat k) =>
ℂ -> C k -> M m n
diagRectC
    dvmap :: forall (n :: Nat). KnownNat n => (ℂ -> ℂ) -> C n -> C n
dvmap = forall (n :: Nat). KnownNat n => (ℂ -> ℂ) -> C n -> C n
mapC
    dmmap :: forall (n :: Nat) (m :: Nat).
(KnownNat m, KnownNat n) =>
(ℂ -> ℂ) -> M n m -> M n m
dmmap = forall (n :: Nat) (m :: Nat).
(KnownNat n, KnownNat m) =>
(ℂ -> ℂ) -> M n m -> M n m
mapM'
    outer :: forall (n :: Nat) (m :: Nat).
(KnownNat m, KnownNat n) =>
C n -> C m -> M n m
outer = forall (m :: Nat) (n :: Nat).
(KnownNat m, KnownNat n) =>
C n -> C m -> M n m
outerC
    zipWithVector :: forall (n :: Nat). KnownNat n => (ℂ -> ℂ -> ℂ) -> C n -> C n -> C n
zipWithVector = forall (n :: Nat). KnownNat n => (ℂ -> ℂ -> ℂ) -> C n -> C n -> C n
zipWithC
    det :: forall (n :: Nat). KnownNat n => M n n -> ℂ
det = forall (n :: Nat). KnownNat n => M n n -> ℂ
detM
    invlndet :: forall (n :: Nat). KnownNat n => M n n -> (M n n, (ℂ, ℂ))
invlndet = forall (n :: Nat). KnownNat n => M n n -> (M n n, (ℂ, ℂ))
invlndetM
    expm :: forall (n :: Nat). KnownNat n => M n n -> M n n
expm = forall (n :: Nat). KnownNat n => M n n -> M n n
expmM
    sqrtm :: forall (n :: Nat). KnownNat n => M n n -> M n n
sqrtm = forall (n :: Nat). KnownNat n => M n n -> M n n
sqrtmM
    inv :: forall (n :: Nat). KnownNat n => M n n -> M n n
inv = forall (n :: Nat). KnownNat n => M n n -> M n n
invM

--------------------------------------------------------------------------------

mulR :: forall m k n. (KnownNat m, KnownNat k, KnownNat n) => L m k -> L k n -> L m n

mulR :: forall (m :: Nat) (k :: Nat) (n :: Nat).
(KnownNat m, KnownNat k, KnownNat n) =>
L m k -> L k n -> L m n
mulR (forall (m :: Nat) (n :: Nat).
(KnownNat m, KnownNat n) =>
L m n -> Maybe (ℝ, (Int, Int))
isKonst -> Just (ℝ
a,(Int
_,Int
k))) (forall (m :: Nat) (n :: Nat).
(KnownNat m, KnownNat n) =>
L m n -> Maybe (ℝ, (Int, Int))
isKonst -> Just (ℝ
b,(Int, Int)
_)) = forall t s (d :: * -> *). Sized t s d => t -> s
konst (ℝ
a forall a. Num a => a -> a -> a
* ℝ
b forall a. Num a => a -> a -> a
* forall a b. (Integral a, Num b) => a -> b
fromIntegral Int
k)

mulR (forall (m :: Nat) (n :: Nat).
(KnownNat m, KnownNat n) =>
L m n -> Maybe (ℝ, Vector ℝ, (Int, Int))
isDiag -> Just (ℝ
0,Vector ℝ
a,(Int, Int)
_)) (forall (m :: Nat) (n :: Nat).
(KnownNat m, KnownNat n) =>
L m n -> Maybe (ℝ, Vector ℝ, (Int, Int))
isDiag -> Just (ℝ
0,Vector ℝ
b,(Int, Int)
_)) = forall field (vec :: Nat -> *) (mat :: Nat -> Nat -> *) (m :: Nat)
       (n :: Nat) (k :: Nat).
(Domain field vec mat, KnownNat m, KnownNat n, KnownNat k) =>
field -> vec k -> mat m n
diagR ℝ
0 (forall (n :: Nat). Vector ℝ -> R n
mkR Vector ℝ
v :: R k)
  where
    v :: Vector ℝ
v = Vector ℝ
a' forall a. Num a => a -> a -> a
* Vector ℝ
b'
    n :: Int
n = forall a. Ord a => a -> a -> a
min (forall (c :: * -> *) t. Container c t => c t -> IndexOf c
LA.size Vector ℝ
a) (forall (c :: * -> *) t. Container c t => c t -> IndexOf c
LA.size Vector ℝ
b)
    a' :: Vector ℝ
a' = forall t. Storable t => Int -> Int -> Vector t -> Vector t
subVector Int
0 Int
n Vector ℝ
a
    b' :: Vector ℝ
b' = forall t. Storable t => Int -> Int -> Vector t -> Vector t
subVector Int
0 Int
n Vector ℝ
b

-- mulR (isDiag -> Just (0,a,_)) (extract -> b) = mkL (asColumn a * takeRows (LA.size a) b)

-- mulR (extract -> a) (isDiag -> Just (0,b,_)) = mkL (takeColumns (LA.size b) a * asRow b)

mulR L m k
a L k n
b = forall (m :: Nat) (n :: Nat). Matrix ℝ -> L m n
mkL (forall t s (d :: * -> *). Sized t s d => s -> d t
extract L m k
a forall t. Numeric t => Matrix t -> Matrix t -> Matrix t
LA.<> forall t s (d :: * -> *). Sized t s d => s -> d t
extract L k n
b)


appR :: (KnownNat m, KnownNat n) => L m n -> R n -> R m
appR :: forall (m :: Nat) (n :: Nat).
(KnownNat m, KnownNat n) =>
L m n -> R n -> R m
appR (forall (m :: Nat) (n :: Nat).
(KnownNat m, KnownNat n) =>
L m n -> Maybe (ℝ, Vector ℝ, (Int, Int))
isDiag -> Just (ℝ
0, Vector ℝ
w, (Int, Int)
_)) R n
v = forall (n :: Nat). Vector ℝ -> R n
mkR (Vector ℝ
w forall a. Num a => a -> a -> a
* forall t. Storable t => Int -> Int -> Vector t -> Vector t
subVector Int
0 (forall (c :: * -> *) t. Container c t => c t -> IndexOf c
LA.size Vector ℝ
w) (forall t s (d :: * -> *). Sized t s d => s -> d t
extract R n
v))
appR L m n
m R n
v = forall (n :: Nat). Vector ℝ -> R n
mkR (forall t s (d :: * -> *). Sized t s d => s -> d t
extract L m n
m forall t. Numeric t => Matrix t -> Vector t -> Vector t
LA.#> forall t s (d :: * -> *). Sized t s d => s -> d t
extract R n
v)


dotR :: KnownNat n => R n -> R n -> ℝ
dotR :: forall (n :: Nat). KnownNat n => R n -> R n -> ℝ
dotR (forall t s (d :: * -> *). Sized t s d => s -> d t
extract -> Vector ℝ
u) (forall t s (d :: * -> *). Sized t s d => s -> d t
extract -> Vector ℝ
v) = forall t. Numeric t => Vector t -> Vector t -> t
LA.dot Vector ℝ
u Vector ℝ
v


crossR :: R 3 -> R 3 -> R 3
crossR :: R 3 -> R 3 -> R 3
crossR (forall t s (d :: * -> *). Sized t s d => s -> d t
extract -> Vector ℝ
x) (forall t s (d :: * -> *). Sized t s d => s -> d t
extract -> Vector ℝ
y) = ℝ -> ℝ -> ℝ -> R 3
vec3 ℝ
z1 ℝ
z2 ℝ
z3
  where
    z1 :: ℝ
z1 = Vector ℝ
xforall c t. Indexable c t => c -> Int -> t
!Int
1forall a. Num a => a -> a -> a
*Vector ℝ
yforall c t. Indexable c t => c -> Int -> t
!Int
2forall a. Num a => a -> a -> a
-Vector ℝ
xforall c t. Indexable c t => c -> Int -> t
!Int
2forall a. Num a => a -> a -> a
*Vector ℝ
yforall c t. Indexable c t => c -> Int -> t
!Int
1
    z2 :: ℝ
z2 = Vector ℝ
xforall c t. Indexable c t => c -> Int -> t
!Int
2forall a. Num a => a -> a -> a
*Vector ℝ
yforall c t. Indexable c t => c -> Int -> t
!Int
0forall a. Num a => a -> a -> a
-Vector ℝ
xforall c t. Indexable c t => c -> Int -> t
!Int
0forall a. Num a => a -> a -> a
*Vector ℝ
yforall c t. Indexable c t => c -> Int -> t
!Int
2
    z3 :: ℝ
z3 = Vector ℝ
xforall c t. Indexable c t => c -> Int -> t
!Int
0forall a. Num a => a -> a -> a
*Vector ℝ
yforall c t. Indexable c t => c -> Int -> t
!Int
1forall a. Num a => a -> a -> a
-Vector ℝ
xforall c t. Indexable c t => c -> Int -> t
!Int
1forall a. Num a => a -> a -> a
*Vector ℝ
yforall c t. Indexable c t => c -> Int -> t
!Int
0

outerR :: (KnownNat m, KnownNat n) => R n -> R m -> L n m
outerR :: forall (m :: Nat) (n :: Nat).
(KnownNat m, KnownNat n) =>
R n -> R m -> L n m
outerR (forall t s (d :: * -> *). Sized t s d => s -> d t
extract -> Vector ℝ
x) (forall t s (d :: * -> *). Sized t s d => s -> d t
extract -> Vector ℝ
y) = forall (m :: Nat) (n :: Nat). Matrix ℝ -> L m n
mkL (forall t. Product t => Vector t -> Vector t -> Matrix t
LA.outer Vector ℝ
x Vector ℝ
y)

mapR :: KnownNat n => (ℝ -> ℝ) -> R n -> R n
mapR :: forall (n :: Nat). KnownNat n => (ℝ -> ℝ) -> R n -> R n
mapR ℝ -> ℝ
f (forall t s (d :: * -> *). Sized t s d => s -> d t
unwrap -> Vector ℝ
v) = forall (n :: Nat). Vector ℝ -> R n
mkR (forall b (c :: * -> *) e.
(Element b, Container c e) =>
(e -> b) -> c e -> c b
LA.cmap ℝ -> ℝ
f Vector ℝ
v)

zipWithR :: KnownNat n => (ℝ -> ℝ -> ℝ) -> R n -> R n -> R n
zipWithR :: forall (n :: Nat). KnownNat n => (ℝ -> ℝ -> ℝ) -> R n -> R n -> R n
zipWithR ℝ -> ℝ -> ℝ
f (forall t s (d :: * -> *). Sized t s d => s -> d t
extract -> Vector ℝ
x) (forall t s (d :: * -> *). Sized t s d => s -> d t
extract -> Vector ℝ
y) = forall (n :: Nat). Vector ℝ -> R n
mkR (forall a b c.
(Storable a, Storable b, Storable c) =>
(a -> b -> c) -> Vector a -> Vector b -> Vector c
LA.zipVectorWith ℝ -> ℝ -> ℝ
f Vector ℝ
x Vector ℝ
y)

mapL :: (KnownNat n, KnownNat m) => (ℝ -> ℝ) -> L n m -> L n m
mapL :: forall (n :: Nat) (m :: Nat).
(KnownNat n, KnownNat m) =>
(ℝ -> ℝ) -> L n m -> L n m
mapL ℝ -> ℝ
f = forall (m :: Nat) (n :: Nat).
(KnownNat m, KnownNat n) =>
(Matrix ℝ -> Matrix ℝ) -> L m n -> L m n
overMatL' (forall b (c :: * -> *) e.
(Element b, Container c e) =>
(e -> b) -> c e -> c b
LA.cmap ℝ -> ℝ
f)

detL :: KnownNat n => Sq n -> ℝ
detL :: forall (n :: Nat). KnownNat n => L n n -> ℝ
detL = forall t. Field t => Matrix t -> t
LA.det forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall t s (d :: * -> *). Sized t s d => s -> d t
unwrap

invlndetL :: KnownNat n => Sq n -> (L n n, (ℝ, ℝ))
invlndetL :: forall (n :: Nat). KnownNat n => L n n -> (L n n, (ℝ, ℝ))
invlndetL = forall (p :: * -> * -> *) a b c.
Bifunctor p =>
(a -> b) -> p a c -> p b c
BF.first forall (m :: Nat) (n :: Nat). Matrix ℝ -> L m n
mkL forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall t. Field t => Matrix t -> (Matrix t, (t, t))
LA.invlndet forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall t s (d :: * -> *). Sized t s d => s -> d t
unwrap

expmL :: KnownNat n => Sq n -> Sq n
expmL :: forall (n :: Nat). KnownNat n => L n n -> L n n
expmL = forall (m :: Nat) (n :: Nat).
(KnownNat m, KnownNat n) =>
(Matrix ℝ -> Matrix ℝ) -> L m n -> L m n
overMatL' forall {t}. Field t => Matrix t -> Matrix t
LA.expm

sqrtmL :: KnownNat n => Sq n -> Sq n
sqrtmL :: forall (n :: Nat). KnownNat n => L n n -> L n n
sqrtmL = forall (m :: Nat) (n :: Nat).
(KnownNat m, KnownNat n) =>
(Matrix ℝ -> Matrix ℝ) -> L m n -> L m n
overMatL' forall {t}. Field t => Matrix t -> Matrix t
LA.sqrtm

invL :: KnownNat n => Sq n -> Sq n
invL :: forall (n :: Nat). KnownNat n => L n n -> L n n
invL = forall (m :: Nat) (n :: Nat).
(KnownNat m, KnownNat n) =>
(Matrix ℝ -> Matrix ℝ) -> L m n -> L m n
overMatL' forall {t}. Field t => Matrix t -> Matrix t
LA.inv

--------------------------------------------------------------------------------

mulC :: forall m k n. (KnownNat m, KnownNat k, KnownNat n) => M m k -> M k n -> M m n

mulC :: forall (m :: Nat) (k :: Nat) (n :: Nat).
(KnownNat m, KnownNat k, KnownNat n) =>
M m k -> M k n -> M m n
mulC (forall (m :: Nat) (n :: Nat).
(KnownNat m, KnownNat n) =>
M m n -> Maybe (ℂ, (Int, Int))
isKonstC -> Just (ℂ
a,(Int
_,Int
k))) (forall (m :: Nat) (n :: Nat).
(KnownNat m, KnownNat n) =>
M m n -> Maybe (ℂ, (Int, Int))
isKonstC -> Just (ℂ
b,(Int, Int)
_)) = forall t s (d :: * -> *). Sized t s d => t -> s
konst (ℂ
a forall a. Num a => a -> a -> a
* ℂ
b forall a. Num a => a -> a -> a
* forall a b. (Integral a, Num b) => a -> b
fromIntegral Int
k)

mulC (forall (m :: Nat) (n :: Nat).
(KnownNat m, KnownNat n) =>
M m n -> Maybe (ℂ, Vector ℂ, (Int, Int))
isDiagC -> Just (ℂ
0,Vector ℂ
a,(Int, Int)
_)) (forall (m :: Nat) (n :: Nat).
(KnownNat m, KnownNat n) =>
M m n -> Maybe (ℂ, Vector ℂ, (Int, Int))
isDiagC -> Just (ℂ
0,Vector ℂ
b,(Int, Int)
_)) = forall field (vec :: Nat -> *) (mat :: Nat -> Nat -> *) (m :: Nat)
       (n :: Nat) (k :: Nat).
(Domain field vec mat, KnownNat m, KnownNat n, KnownNat k) =>
field -> vec k -> mat m n
diagR ℂ
0 (forall (n :: Nat). Vector ℂ -> C n
mkC Vector ℂ
v :: C k)
  where
    v :: Vector ℂ
v = Vector ℂ
a' forall a. Num a => a -> a -> a
* Vector ℂ
b'
    n :: Int
n = forall a. Ord a => a -> a -> a
min (forall (c :: * -> *) t. Container c t => c t -> IndexOf c
LA.size Vector ℂ
a) (forall (c :: * -> *) t. Container c t => c t -> IndexOf c
LA.size Vector ℂ
b)
    a' :: Vector ℂ
a' = forall t. Storable t => Int -> Int -> Vector t -> Vector t
subVector Int
0 Int
n Vector ℂ
a
    b' :: Vector ℂ
b' = forall t. Storable t => Int -> Int -> Vector t -> Vector t
subVector Int
0 Int
n Vector ℂ
b

-- mulC (isDiagC -> Just (0,a,_)) (extract -> b) = mkM (asColumn a * takeRows (LA.size a) b)

-- mulC (extract -> a) (isDiagC -> Just (0,b,_)) = mkM (takeColumns (LA.size b) a * asRow b)

mulC M m k
a M k n
b = forall (m :: Nat) (n :: Nat). Matrix ℂ -> M m n
mkM (forall t s (d :: * -> *). Sized t s d => s -> d t
extract M m k
a forall t. Numeric t => Matrix t -> Matrix t -> Matrix t
LA.<> forall t s (d :: * -> *). Sized t s d => s -> d t
extract M k n
b)


appC :: (KnownNat m, KnownNat n) => M m n -> C n -> C m
appC :: forall (m :: Nat) (n :: Nat).
(KnownNat m, KnownNat n) =>
M m n -> C n -> C m
appC (forall (m :: Nat) (n :: Nat).
(KnownNat m, KnownNat n) =>
M m n -> Maybe (ℂ, Vector ℂ, (Int, Int))
isDiagC -> Just (ℂ
0, Vector ℂ
w, (Int, Int)
_)) C n
v = forall (n :: Nat). Vector ℂ -> C n
mkC (Vector ℂ
w forall a. Num a => a -> a -> a
* forall t. Storable t => Int -> Int -> Vector t -> Vector t
subVector Int
0 (forall (c :: * -> *) t. Container c t => c t -> IndexOf c
LA.size Vector ℂ
w) (forall t s (d :: * -> *). Sized t s d => s -> d t
extract C n
v))
appC M m n
m C n
v = forall (n :: Nat). Vector ℂ -> C n
mkC (forall t s (d :: * -> *). Sized t s d => s -> d t
extract M m n
m forall t. Numeric t => Matrix t -> Vector t -> Vector t
LA.#> forall t s (d :: * -> *). Sized t s d => s -> d t
extract C n
v)


dotC :: KnownNat n => C n -> C n -> ℂ
dotC :: forall (n :: Nat). KnownNat n => C n -> C n -> ℂ
dotC (forall t s (d :: * -> *). Sized t s d => s -> d t
extract -> Vector ℂ
u) (forall t s (d :: * -> *). Sized t s d => s -> d t
extract -> Vector ℂ
v) = forall t. Numeric t => Vector t -> Vector t -> t
LA.dot Vector ℂ
u Vector ℂ
v


crossC :: C 3 -> C 3 -> C 3
crossC :: C 3 -> C 3 -> C 3
crossC (forall t s (d :: * -> *). Sized t s d => s -> d t
extract -> Vector ℂ
x) (forall t s (d :: * -> *). Sized t s d => s -> d t
extract -> Vector ℂ
y) = forall (n :: Nat). Vector ℂ -> C n
mkC (forall a. Storable a => [a] -> Vector a
LA.fromList [ℂ
z1, ℂ
z2, ℂ
z3])
  where
    z1 :: ℂ
z1 = Vector ℂ
xforall c t. Indexable c t => c -> Int -> t
!Int
1forall a. Num a => a -> a -> a
*Vector ℂ
yforall c t. Indexable c t => c -> Int -> t
!Int
2forall a. Num a => a -> a -> a
-Vector ℂ
xforall c t. Indexable c t => c -> Int -> t
!Int
2forall a. Num a => a -> a -> a
*Vector ℂ
yforall c t. Indexable c t => c -> Int -> t
!Int
1
    z2 :: ℂ
z2 = Vector ℂ
xforall c t. Indexable c t => c -> Int -> t
!Int
2forall a. Num a => a -> a -> a
*Vector ℂ
yforall c t. Indexable c t => c -> Int -> t
!Int
0forall a. Num a => a -> a -> a
-Vector ℂ
xforall c t. Indexable c t => c -> Int -> t
!Int
0forall a. Num a => a -> a -> a
*Vector ℂ
yforall c t. Indexable c t => c -> Int -> t
!Int
2
    z3 :: ℂ
z3 = Vector ℂ
xforall c t. Indexable c t => c -> Int -> t
!Int
0forall a. Num a => a -> a -> a
*Vector ℂ
yforall c t. Indexable c t => c -> Int -> t
!Int
1forall a. Num a => a -> a -> a
-Vector ℂ
xforall c t. Indexable c t => c -> Int -> t
!Int
1forall a. Num a => a -> a -> a
*Vector ℂ
yforall c t. Indexable c t => c -> Int -> t
!Int
0

outerC :: (KnownNat m, KnownNat n) => C n -> C m -> M n m
outerC :: forall (m :: Nat) (n :: Nat).
(KnownNat m, KnownNat n) =>
C n -> C m -> M n m
outerC (forall t s (d :: * -> *). Sized t s d => s -> d t
extract -> Vector ℂ
x) (forall t s (d :: * -> *). Sized t s d => s -> d t
extract -> Vector ℂ
y) = forall (m :: Nat) (n :: Nat). Matrix ℂ -> M m n
mkM (forall t. Product t => Vector t -> Vector t -> Matrix t
LA.outer Vector ℂ
x Vector ℂ
y)

mapC :: KnownNat n => (ℂ -> ℂ) -> C n -> C n
mapC :: forall (n :: Nat). KnownNat n => (ℂ -> ℂ) -> C n -> C n
mapC ℂ -> ℂ
f (forall t s (d :: * -> *). Sized t s d => s -> d t
unwrap -> Vector ℂ
v) = forall (n :: Nat). Vector ℂ -> C n
mkC (forall b (c :: * -> *) e.
(Element b, Container c e) =>
(e -> b) -> c e -> c b
LA.cmap ℂ -> ℂ
f Vector ℂ
v)

zipWithC :: KnownNat n => (ℂ -> ℂ -> ℂ) -> C n -> C n -> C n
zipWithC :: forall (n :: Nat). KnownNat n => (ℂ -> ℂ -> ℂ) -> C n -> C n -> C n
zipWithC ℂ -> ℂ -> ℂ
f (forall t s (d :: * -> *). Sized t s d => s -> d t
extract -> Vector ℂ
x) (forall t s (d :: * -> *). Sized t s d => s -> d t
extract -> Vector ℂ
y) = forall (n :: Nat). Vector ℂ -> C n
mkC (forall a b c.
(Storable a, Storable b, Storable c) =>
(a -> b -> c) -> Vector a -> Vector b -> Vector c
LA.zipVectorWith ℂ -> ℂ -> ℂ
f Vector ℂ
x Vector ℂ
y)

mapM' :: (KnownNat n, KnownNat m) => (ℂ -> ℂ) -> M n m -> M n m
mapM' :: forall (n :: Nat) (m :: Nat).
(KnownNat n, KnownNat m) =>
(ℂ -> ℂ) -> M n m -> M n m
mapM' ℂ -> ℂ
f = forall (m :: Nat) (n :: Nat).
(KnownNat m, KnownNat n) =>
(Matrix ℂ -> Matrix ℂ) -> M m n -> M m n
overMatM' (forall b (c :: * -> *) e.
(Element b, Container c e) =>
(e -> b) -> c e -> c b
LA.cmap ℂ -> ℂ
f)

detM :: KnownNat n => M n n -> ℂ
detM :: forall (n :: Nat). KnownNat n => M n n -> ℂ
detM = forall t. Field t => Matrix t -> t
LA.det forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall t s (d :: * -> *). Sized t s d => s -> d t
unwrap

invlndetM :: KnownNat n => M n n -> (M n n, (ℂ, ℂ))
invlndetM :: forall (n :: Nat). KnownNat n => M n n -> (M n n, (ℂ, ℂ))
invlndetM = forall (p :: * -> * -> *) a b c.
Bifunctor p =>
(a -> b) -> p a c -> p b c
BF.first forall (m :: Nat) (n :: Nat). Matrix ℂ -> M m n
mkM forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall t. Field t => Matrix t -> (Matrix t, (t, t))
LA.invlndet forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall t s (d :: * -> *). Sized t s d => s -> d t
unwrap

expmM :: KnownNat n => M n n -> M n n
expmM :: forall (n :: Nat). KnownNat n => M n n -> M n n
expmM = forall (m :: Nat) (n :: Nat).
(KnownNat m, KnownNat n) =>
(Matrix ℂ -> Matrix ℂ) -> M m n -> M m n
overMatM' forall {t}. Field t => Matrix t -> Matrix t
LA.expm

sqrtmM :: KnownNat n => M n n -> M n n
sqrtmM :: forall (n :: Nat). KnownNat n => M n n -> M n n
sqrtmM = forall (m :: Nat) (n :: Nat).
(KnownNat m, KnownNat n) =>
(Matrix ℂ -> Matrix ℂ) -> M m n -> M m n
overMatM' forall {t}. Field t => Matrix t -> Matrix t
LA.sqrtm

invM :: KnownNat n => M n n -> M n n
invM :: forall (n :: Nat). KnownNat n => M n n -> M n n
invM = forall (m :: Nat) (n :: Nat).
(KnownNat m, KnownNat n) =>
(Matrix ℂ -> Matrix ℂ) -> M m n -> M m n
overMatM' forall {t}. Field t => Matrix t -> Matrix t
LA.inv

--------------------------------------------------------------------------------

diagRectR :: forall m n k . (KnownNat m, KnownNat n, KnownNat k) => ℝ -> R k -> L m n
diagRectR :: forall (m :: Nat) (n :: Nat) (k :: Nat).
(KnownNat m, KnownNat n, KnownNat k) =>
ℝ -> R k -> L m n
diagRectR ℝ
x R k
v
    | Int
m' forall a. Eq a => a -> a -> Bool
== Int
1 = forall (m :: Nat) (n :: Nat). Matrix ℝ -> L m n
mkL (forall t. Storable t => t -> Vector t -> Int -> Int -> Matrix t
LA.diagRect ℝ
x Vector ℝ
ev Int
m' Int
n')
    | Int
m'forall a. Num a => a -> a -> a
*Int
n' forall a. Ord a => a -> a -> Bool
> Int
0 = L m n
r
    | Bool
otherwise = forall (m :: Nat) (n :: Nat).
(KnownNat m, KnownNat n) =>
[ℝ] -> L m n
matrix []
  where
    r :: L m n
r = forall (m :: Nat) (n :: Nat). Matrix ℝ -> L m n
mkL (forall a. Storable a => Vector a -> Matrix a
asRow (forall t. Storable t => [Vector t] -> Vector t
vjoin [forall (c :: * -> *) e. Container c e => e -> c e
scalar ℝ
x, Vector ℝ
ev, Vector ℝ
zeros]))
    ev :: Vector ℝ
ev = forall t s (d :: * -> *). Sized t s d => s -> d t
extract R k
v
    zeros :: Vector ℝ
zeros = forall e d (c :: * -> *). Konst e d c => e -> d -> c e
LA.konst ℝ
x (forall a. Ord a => a -> a -> a
max Int
0 ((forall a. Ord a => a -> a -> a
min Int
m' Int
n') forall a. Num a => a -> a -> a
- forall (c :: * -> *) t. Container c t => c t -> IndexOf c
LA.size Vector ℝ
ev))
    (Int
m',Int
n') = forall t s (d :: * -> *). Sized t s d => s -> IndexOf d
size L m n
r


diagRectC :: forall m n k . (KnownNat m, KnownNat n, KnownNat k) => ℂ -> C k -> M m n
diagRectC :: forall (m :: Nat) (n :: Nat) (k :: Nat).
(KnownNat m, KnownNat n, KnownNat k) =>
ℂ -> C k -> M m n
diagRectC ℂ
x C k
v
    | Int
m' forall a. Eq a => a -> a -> Bool
== Int
1 = forall (m :: Nat) (n :: Nat). Matrix ℂ -> M m n
mkM (forall t. Storable t => t -> Vector t -> Int -> Int -> Matrix t
LA.diagRect ℂ
x Vector ℂ
ev Int
m' Int
n')
    | Int
m'forall a. Num a => a -> a -> a
*Int
n' forall a. Ord a => a -> a -> Bool
> Int
0 = M m n
r
    | Bool
otherwise = forall t s (d :: * -> *). Sized t s d => [t] -> s
fromList []
  where
    r :: M m n
r = forall (m :: Nat) (n :: Nat). Matrix ℂ -> M m n
mkM (forall a. Storable a => Vector a -> Matrix a
asRow (forall t. Storable t => [Vector t] -> Vector t
vjoin [forall (c :: * -> *) e. Container c e => e -> c e
scalar ℂ
x, Vector ℂ
ev, Vector ℂ
zeros]))
    ev :: Vector ℂ
ev = forall t s (d :: * -> *). Sized t s d => s -> d t
extract C k
v
    zeros :: Vector ℂ
zeros = forall e d (c :: * -> *). Konst e d c => e -> d -> c e
LA.konst ℂ
x (forall a. Ord a => a -> a -> a
max Int
0 ((forall a. Ord a => a -> a -> a
min Int
m' Int
n') forall a. Num a => a -> a -> a
- forall (c :: * -> *) t. Container c t => c t -> IndexOf c
LA.size Vector ℂ
ev))
    (Int
m',Int
n') = forall t s (d :: * -> *). Sized t s d => s -> IndexOf d
size M m n
r

--------------------------------------------------------------------------------

mean :: (KnownNat n, 1<=n) => R n -> ℝ
mean :: forall (n :: Nat). (KnownNat n, 1 <= n) => R n -> ℝ
mean R n
v = R n
v forall (n :: Nat). KnownNat n => R n -> R n -> ℝ
<·> (R n
1forall a. Fractional a => a -> a -> a
/forall (n :: Nat). KnownNat n => R n
dim)

test :: (Bool, IO ())
test :: (Bool, IO ())
test = (Bool
ok,IO ()
info)
  where
    ok :: Bool
ok =   forall t s (d :: * -> *). Sized t s d => s -> d t
extract (forall (n :: Nat). KnownNat n => Sq n
eye :: Sq 5) forall a. Eq a => a -> a -> Bool
== forall a. (Num a, Element a) => Int -> Matrix a
ident Int
5
           Bool -> Bool -> Bool
&& (forall t s (d :: * -> *). Sized t s d => s -> d t
unwrap forall b c a. (b -> c) -> (a -> b) -> a -> c
.forall (n :: Nat). Sym n -> Sq n
unSym) (forall (m :: Nat) (n :: Nat).
(KnownNat m, KnownNat n) =>
L m n -> Sym n
mTm forall (n :: Nat). KnownNat n => Sq n
sm :: Sym 3) forall a. Eq a => a -> a -> Bool
== forall m mt. Transposable m mt => m -> mt
tr ((Int
3forall a. Storable a => Int -> Int -> [a] -> Matrix a
><Int
3)[ℝ
1..]) forall t. Numeric t => Matrix t -> Matrix t -> Matrix t
LA.<> (Int
3forall a. Storable a => Int -> Int -> [a] -> Matrix a
><Int
3)[ℝ
1..]
           Bool -> Bool -> Bool
&& forall t s (d :: * -> *). Sized t s d => s -> d t
unwrap (GL
tm :: L 3 5) forall a. Eq a => a -> a -> Bool
== Int -> [ℝ] -> Matrix ℝ
LA.matrix Int
5 [ℝ
1..ℝ
15]
           Bool -> Bool -> Bool
&& ℝ
thingS forall a. Eq a => a -> a -> Bool
== ℝ
thingD
           Bool -> Bool -> Bool
&& ℝ
precS forall a. Eq a => a -> a -> Bool
== ℝ
precD
           Bool -> Bool -> Bool
&& forall z.
Vector ℝ -> (forall (n :: Nat). KnownNat n => R n -> z) -> z
withVector ([ℝ] -> Vector ℝ
LA.vector [ℝ
1..ℝ
15]) forall {n :: Nat}. KnownNat n => R n -> ℝ
sumV forall a. Eq a => a -> a -> Bool
== forall (c :: * -> *) e. Container c e => c e -> e
sumElements (forall a. Storable a => [a] -> Vector a
LA.fromList [ℝ
1..ℝ
15])

    info :: IO ()
info = do
        forall a. Show a => a -> IO ()
print forall a b. (a -> b) -> a -> b
$ R 2
u
        forall a. Show a => a -> IO ()
print forall a b. (a -> b) -> a -> b
$ R 3
v
        forall a. Show a => a -> IO ()
print (forall (n :: Nat). KnownNat n => Sq n
eye :: Sq 3)
        forall a. Show a => a -> IO ()
print forall a b. (a -> b) -> a -> b
$ ((R 2
u forall (n :: Nat). KnownNat n => R n -> ℝ -> R (n + 1)
& ℝ
5) forall a. Num a => a -> a -> a
+ R 3
1) forall (n :: Nat). KnownNat n => R n -> R n -> ℝ
<·> R 3
v
        forall a. Show a => a -> IO ()
print (GL
tm :: L 2 5)
        forall a. Show a => a -> IO ()
print (GL
tm forall (m :: Nat) (k :: Nat) (n :: Nat).
(KnownNat m, KnownNat k, KnownNat n) =>
L m k -> L k n -> L m n
<> forall (n :: Nat). KnownNat n => Sq n
sm :: L 2 3)
        forall a. Show a => a -> IO ()
print ℝ
thingS
        forall a. Show a => a -> IO ()
print ℝ
thingD
        forall a. Show a => a -> IO ()
print ℝ
precS
        forall a. Show a => a -> IO ()
print ℝ
precD
        forall a. Show a => a -> IO ()
print forall a b. (a -> b) -> a -> b
$ forall z.
Vector ℝ -> (forall (n :: Nat). KnownNat n => R n -> z) -> z
withVector ([ℝ] -> Vector ℝ
LA.vector [ℝ
1..ℝ
15]) forall {n :: Nat}. KnownNat n => R n -> ℝ
sumV
        IO ()
splittest

    sumV :: R n -> ℝ
sumV R n
w = R n
w forall (n :: Nat). KnownNat n => R n -> R n -> ℝ
<·> forall t s (d :: * -> *). Sized t s d => t -> s
konst ℝ
1

    u :: R 2
u = ℝ -> ℝ -> R 2
vec2 ℝ
3 ℝ
5

    𝕧 :: ℝ -> R 1
𝕧 ℝ
x = forall (n :: Nat). KnownNat n => [ℝ] -> R n
vector [ℝ
x] :: R 1

    v :: R (2 + 1)
v = ℝ -> R 1
𝕧 ℝ
2 forall (n :: Nat). KnownNat n => R n -> ℝ -> R (n + 1)
& ℝ
4 forall (n :: Nat). KnownNat n => R n -> ℝ -> R (n + 1)
& ℝ
7

    tm :: GL
    tm :: GL
tm = forall (m :: Nat) (n :: Nat).
(KnownNat m, KnownNat n) =>
ℝ -> [ℝ] -> L m n
lmat ℝ
0 [ℝ
1..]

    lmat :: forall m n . (KnownNat m, KnownNat n) => ℝ -> [ℝ] -> L m n
    lmat :: forall (m :: Nat) (n :: Nat).
(KnownNat m, KnownNat n) =>
ℝ -> [ℝ] -> L m n
lmat ℝ
z [ℝ]
xs = L m n
r
      where
        r :: L m n
r = forall (m :: Nat) (n :: Nat). Matrix ℝ -> L m n
mkL forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall t. Storable t => Int -> Vector t -> Matrix t
reshape Int
n' forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Storable a => [a] -> Vector a
LA.fromList forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Int -> [a] -> [a]
take (Int
m'forall a. Num a => a -> a -> a
*Int
n') forall a b. (a -> b) -> a -> b
$ [ℝ]
xs forall a. [a] -> [a] -> [a]
++ forall a. a -> [a]
repeat ℝ
z
        (Int
m',Int
n') = forall t s (d :: * -> *). Sized t s d => s -> IndexOf d
size L m n
r

    sm :: GSq
    sm :: forall (n :: Nat). KnownNat n => Sq n
sm = forall (m :: Nat) (n :: Nat).
(KnownNat m, KnownNat n) =>
ℝ -> [ℝ] -> L m n
lmat ℝ
0 [ℝ
1..]

    thingS :: ℝ
thingS = (R 2
u forall (n :: Nat). KnownNat n => R n -> ℝ -> R (n + 1)
& ℝ
1) forall (n :: Nat). KnownNat n => R n -> R n -> ℝ
<·> forall m mt. Transposable m mt => m -> mt
tr L 10 3
q forall (m :: Nat) (n :: Nat).
(KnownNat m, KnownNat n) =>
L m n -> R n -> R m
#> L 10 3
q forall (m :: Nat) (n :: Nat).
(KnownNat m, KnownNat n) =>
L m n -> R n -> R m
#> R 3
v
      where
        q :: L 10 3
q = GL
tm :: L 10 3

    thingD :: ℝ
thingD = forall t. Storable t => [Vector t] -> Vector t
vjoin [forall (n :: Nat). R n -> Vector ℝ
ud1 R 2
u, Vector ℝ
1] forall t. Numeric t => Vector t -> Vector t -> t
LA.<.> forall m mt. Transposable m mt => m -> mt
tr Matrix ℝ
m forall t. Numeric t => Matrix t -> Vector t -> Vector t
LA.#> Matrix ℝ
m forall t. Numeric t => Matrix t -> Vector t -> Vector t
LA.#> forall (n :: Nat). R n -> Vector ℝ
ud1 R 3
v
      where
        m :: Matrix ℝ
m = Int -> [ℝ] -> Matrix ℝ
LA.matrix Int
3 [ℝ
1..ℝ
30]

    precS :: ℝ
precS = (ℝ
1::Double) forall a. Num a => a -> a -> a
+ (ℝ
2::Double) forall a. Num a => a -> a -> a
* ((R 3
1 :: R 3) forall a. Num a => a -> a -> a
* (R 2
u forall (n :: Nat). KnownNat n => R n -> ℝ -> R (n + 1)
& ℝ
6)) forall (n :: Nat). KnownNat n => R n -> R n -> ℝ
<·> forall t s (d :: * -> *). Sized t s d => t -> s
konst ℝ
2 forall (m :: Nat) (n :: Nat).
(KnownNat m, KnownNat n) =>
L m n -> R n -> R m
#> R 3
v
    precD :: ℝ
precD = ℝ
1 forall a. Num a => a -> a -> a
+ ℝ
2 forall a. Num a => a -> a -> a
* forall t. Storable t => [Vector t] -> Vector t
vjoin[forall (n :: Nat). R n -> Vector ℝ
ud1 R 2
u, Vector ℝ
6] forall t. Numeric t => Vector t -> Vector t -> t
LA.<.> forall e d (c :: * -> *). Konst e d c => e -> d -> c e
LA.konst ℝ
2 (forall (c :: * -> *) t. Container c t => c t -> IndexOf c
LA.size (forall (n :: Nat). R n -> Vector ℝ
ud1 R 2
u) forall a. Num a => a -> a -> a
+Int
1, forall (c :: * -> *) t. Container c t => c t -> IndexOf c
LA.size (forall (n :: Nat). R n -> Vector ℝ
ud1 R 3
v)) forall t. Numeric t => Matrix t -> Vector t -> Vector t
LA.#> forall (n :: Nat). R n -> Vector ℝ
ud1 R 3
v


splittest :: IO ()
splittest
    = do
    let v :: R 7
v = forall (n :: Nat). KnownNat n => R n
range :: R 7
        a :: R 4
a = forall a b. (a, b) -> b
snd (forall (p :: Nat) (n :: Nat).
(KnownNat p, KnownNat n, p <= n) =>
R n -> (R p, R (n - p))
split R 7
v) :: R 4
    forall a. Show a => a -> IO ()
print forall a b. (a -> b) -> a -> b
$ R 4
a
    forall a. Show a => a -> IO ()
print forall a b. (a -> b) -> a -> b
$ forall a b. (a, b) -> b
snd forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (n :: Nat). (KnownNat n, 1 <= n) => R n -> (ℝ, R (n - 1))
headTail forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a, b) -> b
snd forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (n :: Nat). (KnownNat n, 1 <= n) => R n -> (ℝ, R (n - 1))
headTail forall a b. (a -> b) -> a -> b
$ R 7
v
    forall a. Show a => a -> IO ()
print forall a b. (a -> b) -> a -> b
$ forall {n :: Nat}.
(OrdCond (CmpNat 1 n) 'True 'True 'False ~ 'True, KnownNat n) =>
R n -> ℝ
first (ℝ -> ℝ -> ℝ -> R 3
vec3 ℝ
1 ℝ
2 ℝ
3)
    forall a. Show a => a -> IO ()
print forall a b. (a -> b) -> a -> b
$ forall {n :: Nat}.
(OrdCond (CmpNat 1 n) 'True 'True 'False ~ 'True,
 OrdCond (CmpNat 1 (n - 1)) 'True 'True 'False ~ 'True, KnownNat n,
 KnownNat (n - 1)) =>
R n -> ℝ
second (ℝ -> ℝ -> ℝ -> R 3
vec3 ℝ
1 ℝ
2 ℝ
3)
    forall a. Show a => a -> IO ()
print forall a b. (a -> b) -> a -> b
$ forall {n :: Nat}.
(OrdCond (CmpNat 1 n) 'True 'True 'False ~ 'True,
 OrdCond (CmpNat 1 (n - 1)) 'True 'True 'False ~ 'True,
 OrdCond (CmpNat 1 ((n - 1) - 1)) 'True 'True 'False ~ 'True,
 KnownNat n, KnownNat (n - 1), KnownNat ((n - 1) - 1)) =>
R n -> ℝ
third (ℝ -> ℝ -> ℝ -> R 3
vec3 ℝ
1 ℝ
2 ℝ
3)
    forall a. Show a => a -> IO ()
print forall a b. (a -> b) -> a -> b
$ (forall a b. (a, b) -> b
snd forall a b. (a -> b) -> a -> b
$ forall (p :: Nat) (m :: Nat) (n :: Nat).
(KnownNat p, KnownNat m, KnownNat n, p <= m) =>
L m n -> (L p n, L (m - p) n)
splitRows forall (n :: Nat). KnownNat n => Sq n
eye :: L 4 6)
 where
    first :: R n -> ℝ
first R n
v = forall a b. (a, b) -> a
fst forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (n :: Nat). (KnownNat n, 1 <= n) => R n -> (ℝ, R (n - 1))
headTail forall a b. (a -> b) -> a -> b
$ R n
v
    second :: R n -> ℝ
second R n
v = forall {n :: Nat}.
(OrdCond (CmpNat 1 n) 'True 'True 'False ~ 'True, KnownNat n) =>
R n -> ℝ
first forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a, b) -> b
snd forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (n :: Nat). (KnownNat n, 1 <= n) => R n -> (ℝ, R (n - 1))
headTail forall a b. (a -> b) -> a -> b
$ R n
v
    third :: R n -> ℝ
third R n
v = forall {n :: Nat}.
(OrdCond (CmpNat 1 n) 'True 'True 'False ~ 'True, KnownNat n) =>
R n -> ℝ
first forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a, b) -> b
snd forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (n :: Nat). (KnownNat n, 1 <= n) => R n -> (ℝ, R (n - 1))
headTail forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a, b) -> b
snd forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (n :: Nat). (KnownNat n, 1 <= n) => R n -> (ℝ, R (n - 1))
headTail forall a b. (a -> b) -> a -> b
$ R n
v


instance (KnownNat n', KnownNat m') => Testable (L n' m')
  where
    checkT :: L n' m' -> (Bool, IO ())
checkT L n' m'
_ = (Bool, IO ())
test

--------------------------------------------------------------------------------

instance KnownNat n => Normed (R n)
  where
    norm_0 :: R n -> ℝ
norm_0 R n
v = forall a. Normed a => a -> ℝ
norm_0 (forall t s (d :: * -> *). Sized t s d => s -> d t
extract R n
v)
    norm_1 :: R n -> ℝ
norm_1 R n
v = forall a. Normed a => a -> ℝ
norm_1 (forall t s (d :: * -> *). Sized t s d => s -> d t
extract R n
v)
    norm_2 :: R n -> ℝ
norm_2 R n
v = forall a. Normed a => a -> ℝ
norm_2 (forall t s (d :: * -> *). Sized t s d => s -> d t
extract R n
v)
    norm_Inf :: R n -> ℝ
norm_Inf R n
v = forall a. Normed a => a -> ℝ
norm_Inf (forall t s (d :: * -> *). Sized t s d => s -> d t
extract R n
v)

instance (KnownNat m, KnownNat n) => Normed (L m n)
  where
    norm_0 :: L m n -> ℝ
norm_0 L m n
m = forall a. Normed a => a -> ℝ
norm_0 (forall t s (d :: * -> *). Sized t s d => s -> d t
extract L m n
m)
    norm_1 :: L m n -> ℝ
norm_1 L m n
m = forall a. Normed a => a -> ℝ
norm_1 (forall t s (d :: * -> *). Sized t s d => s -> d t
extract L m n
m)
    norm_2 :: L m n -> ℝ
norm_2 L m n
m = forall a. Normed a => a -> ℝ
norm_2 (forall t s (d :: * -> *). Sized t s d => s -> d t
extract L m n
m)
    norm_Inf :: L m n -> ℝ
norm_Inf L m n
m = forall a. Normed a => a -> ℝ
norm_Inf (forall t s (d :: * -> *). Sized t s d => s -> d t
extract L m n
m)

mkSym :: (Sq n -> Sq n) -> Sym n -> Sym n
mkSym Sq n -> Sq n
f = forall (n :: Nat). Sq n -> Sym n
Sym forall b c a. (b -> c) -> (a -> b) -> a -> c
. Sq n -> Sq n
f forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (n :: Nat). Sym n -> Sq n
unSym
mkSym2 :: (Sq n -> Sq n -> Sq n) -> Sym n -> Sym n -> Sym n
mkSym2 Sq n -> Sq n -> Sq n
f Sym n
x Sym n
y = forall (n :: Nat). Sq n -> Sym n
Sym (Sq n -> Sq n -> Sq n
f (forall (n :: Nat). Sym n -> Sq n
unSym Sym n
x) (forall (n :: Nat). Sym n -> Sq n
unSym Sym n
y))

instance KnownNat n =>  Num (Sym n)
  where
    + :: Sym n -> Sym n -> Sym n
(+) = forall {n :: Nat} {n :: Nat} {n :: Nat}.
(Sq n -> Sq n -> Sq n) -> Sym n -> Sym n -> Sym n
mkSym2 forall a. Num a => a -> a -> a
(+)
    * :: Sym n -> Sym n -> Sym n
(*) = forall {n :: Nat} {n :: Nat} {n :: Nat}.
(Sq n -> Sq n -> Sq n) -> Sym n -> Sym n -> Sym n
mkSym2 forall a. Num a => a -> a -> a
(*)
    (-) = forall {n :: Nat} {n :: Nat} {n :: Nat}.
(Sq n -> Sq n -> Sq n) -> Sym n -> Sym n -> Sym n
mkSym2 (-)
    abs :: Sym n -> Sym n
abs = forall {n :: Nat} {n :: Nat}. (Sq n -> Sq n) -> Sym n -> Sym n
mkSym forall a. Num a => a -> a
abs
    signum :: Sym n -> Sym n
signum = forall {n :: Nat} {n :: Nat}. (Sq n -> Sq n) -> Sym n -> Sym n
mkSym forall a. Num a => a -> a
signum
    negate :: Sym n -> Sym n
negate = forall {n :: Nat} {n :: Nat}. (Sq n -> Sq n) -> Sym n -> Sym n
mkSym forall a. Num a => a -> a
negate
    fromInteger :: Integer -> Sym n
fromInteger = forall (n :: Nat). Sq n -> Sym n
Sym forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Num a => Integer -> a
fromInteger

instance KnownNat n => Fractional (Sym n)
  where
    fromRational :: Rational -> Sym n
fromRational = forall (n :: Nat). Sq n -> Sym n
Sym forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Fractional a => Rational -> a
fromRational
    / :: Sym n -> Sym n -> Sym n
(/) = forall {n :: Nat} {n :: Nat} {n :: Nat}.
(Sq n -> Sq n -> Sq n) -> Sym n -> Sym n -> Sym n
mkSym2 forall a. Fractional a => a -> a -> a
(/)

instance KnownNat n => Floating (Sym n)
  where
    sin :: Sym n -> Sym n
sin   = forall {n :: Nat} {n :: Nat}. (Sq n -> Sq n) -> Sym n -> Sym n
mkSym forall a. Floating a => a -> a
sin
    cos :: Sym n -> Sym n
cos   = forall {n :: Nat} {n :: Nat}. (Sq n -> Sq n) -> Sym n -> Sym n
mkSym forall a. Floating a => a -> a
cos
    tan :: Sym n -> Sym n
tan   = forall {n :: Nat} {n :: Nat}. (Sq n -> Sq n) -> Sym n -> Sym n
mkSym forall a. Floating a => a -> a
tan
    asin :: Sym n -> Sym n
asin  = forall {n :: Nat} {n :: Nat}. (Sq n -> Sq n) -> Sym n -> Sym n
mkSym forall a. Floating a => a -> a
asin
    acos :: Sym n -> Sym n
acos  = forall {n :: Nat} {n :: Nat}. (Sq n -> Sq n) -> Sym n -> Sym n
mkSym forall a. Floating a => a -> a
acos
    atan :: Sym n -> Sym n
atan  = forall {n :: Nat} {n :: Nat}. (Sq n -> Sq n) -> Sym n -> Sym n
mkSym forall a. Floating a => a -> a
atan
    sinh :: Sym n -> Sym n
sinh  = forall {n :: Nat} {n :: Nat}. (Sq n -> Sq n) -> Sym n -> Sym n
mkSym forall a. Floating a => a -> a
sinh
    cosh :: Sym n -> Sym n
cosh  = forall {n :: Nat} {n :: Nat}. (Sq n -> Sq n) -> Sym n -> Sym n
mkSym forall a. Floating a => a -> a
cosh
    tanh :: Sym n -> Sym n
tanh  = forall {n :: Nat} {n :: Nat}. (Sq n -> Sq n) -> Sym n -> Sym n
mkSym forall a. Floating a => a -> a
tanh
    asinh :: Sym n -> Sym n
asinh = forall {n :: Nat} {n :: Nat}. (Sq n -> Sq n) -> Sym n -> Sym n
mkSym forall a. Floating a => a -> a
asinh
    acosh :: Sym n -> Sym n
acosh = forall {n :: Nat} {n :: Nat}. (Sq n -> Sq n) -> Sym n -> Sym n
mkSym forall a. Floating a => a -> a
acosh
    atanh :: Sym n -> Sym n
atanh = forall {n :: Nat} {n :: Nat}. (Sq n -> Sq n) -> Sym n -> Sym n
mkSym forall a. Floating a => a -> a
atanh
    exp :: Sym n -> Sym n
exp   = forall {n :: Nat} {n :: Nat}. (Sq n -> Sq n) -> Sym n -> Sym n
mkSym forall a. Floating a => a -> a
exp
    log :: Sym n -> Sym n
log   = forall {n :: Nat} {n :: Nat}. (Sq n -> Sq n) -> Sym n -> Sym n
mkSym forall a. Floating a => a -> a
log
    sqrt :: Sym n -> Sym n
sqrt  = forall {n :: Nat} {n :: Nat}. (Sq n -> Sq n) -> Sym n -> Sym n
mkSym forall a. Floating a => a -> a
sqrt
    ** :: Sym n -> Sym n -> Sym n
(**)  = forall {n :: Nat} {n :: Nat} {n :: Nat}.
(Sq n -> Sq n -> Sq n) -> Sym n -> Sym n -> Sym n
mkSym2 forall a. Floating a => a -> a -> a
(**)
    pi :: Sym n
pi    = forall (n :: Nat). Sq n -> Sym n
Sym forall a. Floating a => a
pi

instance KnownNat n => Additive (Sym n) where
    add :: Sym n -> Sym n -> Sym n
add = forall a. Num a => a -> a -> a
(+)

instance KnownNat n => Transposable (Sym n) (Sym n) where
    tr :: Sym n -> Sym n
tr  = forall a. a -> a
id
    tr' :: Sym n -> Sym n
tr' = forall a. a -> a
id

instance KnownNat n => Transposable (Her n) (Her n) where
    tr :: Her n -> Her n
tr          = forall a. a -> a
id
    tr' :: Her n -> Her n
tr' (Her M n n
m) = forall (n :: Nat). M n n -> Her n
Her (forall m mt. Transposable m mt => m -> mt
tr' M n n
m)