    {-# 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 R n -> R 1 -> R (n + 1)
    forall (n :: Nat) (m :: Nat).
    (KnownNat n, KnownNat m) =>
    R n -> R m -> R (n + m)
    # (ℝ -> R 1
    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) = Dim (n + m) (Vector ℝ) -> R (n + m)
    forall (n :: Nat). Dim n (Vector ℝ) -> R n
    R (Dim n (Vector ℝ) -> Dim m (Vector ℝ) -> Dim (n + m) (Vector ℝ)
    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 = Dim 2 (Vector ℝ) -> R 2
    forall (n :: Nat). Dim n (Vector ℝ) -> R n
    R (ℝ -> ℝ -> Dim 2 (Vector ℝ)
    forall t. Storable t => t -> t -> V 2 t
    gvec2 ℝ
    a ℝ
    b)

    vec3 :: ℝ -> ℝ -> ℝ -> R 3
    vec3 :: ℝ -> ℝ -> ℝ -> R 3
    vec3 ℝ
    a ℝ
    b ℝ
    c = Dim 3 (Vector ℝ) -> R 3
    forall (n :: Nat). Dim n (Vector ℝ) -> R n
    R (ℝ -> ℝ -> ℝ -> Dim 3 (Vector ℝ)
    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 = Dim 4 (Vector ℝ) -> R 4
    forall (n :: Nat). Dim n (Vector ℝ) -> R n
    R (ℝ -> ℝ -> ℝ -> ℝ -> Dim 4 (Vector ℝ)
    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 = [ℝ] -> R n
    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 = [ℝ] -> L m n
    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 = Vector ℝ -> R n
    forall (n :: Nat). Vector ℝ -> R n
    mkR (Int -> (ℝ, ℝ) -> Vector ℝ
    forall e.
    (Fractional e, Container Vector e) =>
    Int -> (e, e) -> Vector e
    LA.linspace (R n -> IndexOf Vector
    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 = Vector ℝ -> R n
    forall (n :: Nat). Vector ℝ -> R n
    mkR (Int -> (ℝ, ℝ) -> Vector ℝ
    forall e.
    (Fractional e, Container Vector e) =>
    Int -> (e, e) -> Vector e
    LA.linspace Int
    d (ℝ
    1,Int -> ℝ
    forall a b. (Integral a, Num b) => a -> b
    fromIntegral Int
    d))
        d :: Int
    d = R n -> IndexOf Vector
    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 = Vector ℝ -> R n
    forall (n :: Nat). Vector ℝ -> R n
    mkR (ℝ -> Vector ℝ
    forall (c :: * -> *) e. Container c e => e -> c e
    scalar (IndexOf Vector -> ℝ
    forall a b. (Integral a, Num b) => a -> b
    fromIntegral (IndexOf Vector -> ℝ) -> IndexOf Vector -> ℝ
    forall a b. (a -> b) -> a -> b
    $ R n -> IndexOf Vector
    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 = ℝ -> R n -> L n n
    forall (m :: Nat) (n :: Nat) (k :: Nat).
    (KnownNat m, KnownNat n, KnownNat k) =>
    ℝ -> R k -> L m n
    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 = R n -> Sq n
    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 = ℝ -> Matrix ℝ
    forall (c :: * -> *) e. Container c e => e -> c e
    scalar ℝ
    x
        z1 :: Matrix ℝ
    z1 = ℝ -> (Int, Int) -> Matrix ℝ
    forall e d (c :: * -> *). Konst e d c => e -> d -> c e
    LA.konst ℝ
    x (Int
    r,Int
    c)
        z2 :: Matrix ℝ
    z2 = ℝ -> (Int, Int) -> Matrix ℝ
    forall e d (c :: * -> *). Konst e d c => e -> d -> c e
    LA.konst ℝ
    x (Int -> Int -> Int
    forall a. Ord a => a -> a -> a
    max Int
    0 (Int
    m'Int -> Int -> Int
    forall a. Num a => a -> a -> a
    -(Int
    raInt -> Int -> Int
    forall a. Num a => a -> a -> a
    +Int
    r)), Int -> Int -> Int
    forall a. Ord a => a -> a -> a
    max Int
    0 (Int
    n'Int -> Int -> Int
    forall a. Num a => a -> a -> a
    -(Int
    caInt -> Int -> Int
    forall a. Num a => a -> a -> a
    +Int
    c)))
        ra :: Int
    ra = Int -> Int -> Int
    forall a. Ord a => a -> a -> a
    min (Matrix ℝ -> Int
    forall t. Matrix t -> Int
    rows Matrix ℝ
    a) (Int -> Int) -> (Int -> Int) -> Int -> Int
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Int -> Int -> Int
    forall a. Ord a => a -> a -> a
    max Int
    0 (Int -> Int) -> Int -> Int
    forall a b. (a -> b) -> a -> b
    $ Int
    m'Int -> Int -> Int
    forall a. Num a => a -> a -> a
    -Int
    r
        ca :: Int
    ca = Int -> Int -> Int
    forall a. Ord a => a -> a -> a
    min (Matrix ℝ -> Int
    forall t. Matrix t -> Int
    cols Matrix ℝ
    a) (Int -> Int) -> (Int -> Int) -> Int -> Int
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Int -> Int -> Int
    forall a. Ord a => a -> a -> a
    max Int
    0 (Int -> Int) -> Int -> Int
    forall a b. (a -> b) -> a -> b
    $ Int
    n'Int -> Int -> Int
    forall a. Num a => a -> a -> a
    -Int
    c
        sa :: Matrix ℝ
    sa = (Int, Int) -> (Int, Int) -> Matrix ℝ -> Matrix ℝ
    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') = L m n -> IndexOf Matrix
    forall t s (d :: * -> *). Sized t s d => s -> IndexOf d
    size L m n
    res
        res :: L m n
    res = Matrix ℝ -> L m n
    forall (m :: Nat) (n :: Nat). Matrix ℝ -> L m n
    mkL (Matrix ℝ -> L m n) -> Matrix ℝ -> L m n
    forall a b. (a -> b) -> a -> b
    $ [[Matrix ℝ]] -> Matrix ℝ
    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 = Matrix ℝ -> L 1 n
    forall (m :: Nat) (n :: Nat). Matrix ℝ -> L m n
    mkL (Matrix ℝ -> L 1 n) -> (R n -> Matrix ℝ) -> R n -> L 1 n
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Vector ℝ -> Matrix ℝ
    forall a. Storable a => Vector a -> Matrix a
    asRow (Vector ℝ -> Matrix ℝ) -> (R n -> Vector ℝ) -> R n -> Matrix ℝ
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . R n -> Vector ℝ
    forall (n :: Nat). R n -> Vector ℝ
    ud1

    --col :: R n -> L n 1
    col :: R n -> L n 1
    col R n
    v = L 1 n -> L n 1
    forall m mt. Transposable m mt => m -> mt
    tr (L 1 n -> L n 1) -> (R n -> L 1 n) -> R n -> L n 1
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . R n -> L 1 n
    forall (n :: Nat). R n -> L 1 n
    row (R n -> L n 1) -> R n -> L n 1
    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 = Vector ℝ -> R n
    forall (n :: Nat). Vector ℝ -> R n
    mkR (Vector ℝ -> R n) -> (L 1 n -> Vector ℝ) -> L 1 n -> R n
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . [Vector ℝ] -> Vector ℝ
    forall a. HasCallStack => [a] -> a
    head ([Vector ℝ] -> Vector ℝ)
    -> (L 1 n -> [Vector ℝ]) -> L 1 n -> Vector ℝ
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Matrix ℝ -> [Vector ℝ]
    forall t. Element t => Matrix t -> [Vector t]
    LA.toRows (Matrix ℝ -> [Vector ℝ])
    -> (L 1 n -> Matrix ℝ) -> L 1 n -> [Vector ℝ]
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . L 1 n -> Matrix ℝ
    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 = L 1 n -> R n
    forall (n :: Nat). L 1 n -> R n
    unrow (L 1 n -> R n) -> (L n 1 -> L 1 n) -> L n 1 -> R n
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . L n 1 -> L 1 n
    forall m mt. Transposable m mt => m -> mt
    tr (L n 1 -> R n) -> L n 1 -> R n
    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 = Matrix ℝ -> L (r1 + r2) c
    forall (m :: Nat) (n :: Nat). Matrix ℝ -> L m n
    mkL (L r1 c -> Matrix ℝ
    forall t s (d :: * -> *). Sized t s d => s -> d t
    extract L r1 c
    a Matrix ℝ -> Matrix ℝ -> Matrix ℝ
    forall t. Element t => Matrix t -> Matrix t -> Matrix t
    LA.=== L r2 c -> Matrix ℝ
    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 = L (r1 + r2) c -> L c (r1 + r2)
    forall m mt. Transposable m mt => m -> mt
    tr (L c r1 -> L r1 c
    forall m mt. Transposable m mt => m -> mt
    tr L c r1
    a L r1 c -> L r2 c -> L (r1 + r2) c
    forall (r1 :: Nat) (r2 :: Nat) (c :: Nat).
    (KnownNat r1, KnownNat r2, KnownNat c) =>
    L r1 c -> L r2 c -> L (r1 + r2) c
    === L c r2 -> L 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@(L m n -> Matrix ℝ
    forall t s (d :: * -> *). Sized t s d => s -> d t
    unwrap -> Matrix ℝ
    x)
        | Matrix ℝ -> Bool
    forall {t}. Matrix t -> Bool
    singleM Matrix ℝ
    x = (ℝ, (Int, Int)) -> Maybe (ℝ, (Int, Int))
    forall a. a -> Maybe a
    Just (Matrix ℝ
    x Matrix ℝ -> IndexOf Matrix -> ℝ
    forall (c :: * -> *) e. Container c e => c e -> IndexOf c -> e
    `atIndex` (Int
    0,Int
    0), (L m n -> IndexOf Matrix
    forall t s (d :: * -> *). Sized t s d => s -> IndexOf d
    size L m n
    s))
        | Bool
    otherwise = Maybe (ℝ, (Int, Int))
    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@(M m n -> Matrix ℂ
    forall t s (d :: * -> *). Sized t s d => s -> d t
    unwrap -> Matrix ℂ
    x)
        | Matrix ℂ -> Bool
    forall {t}. Matrix t -> Bool
    singleM Matrix ℂ
    x = (ℂ, (Int, Int)) -> Maybe (ℂ, (Int, Int))
    forall a. a -> Maybe a
    Just (Matrix ℂ
    x Matrix ℂ -> IndexOf Matrix -> ℂ
    forall (c :: * -> *) e. Container c e => c e -> IndexOf c -> e
    `atIndex` (Int
    0,Int
    0), (M m n -> IndexOf Matrix
    forall t s (d :: * -> *). Sized t s d => s -> IndexOf d
    size M m n
    s))
        | Bool
    otherwise = Maybe (ℂ, (Int, Int))
    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
    (<>) = 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
    (#>) = 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 -> ℝ
    (<·>) = 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 -> ℝ
    (<.>) = 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 = Vector ℝ -> R n
    forall (n :: Nat). Vector ℝ -> R n
    mkR (Matrix ℝ -> Vector ℝ
    forall t. Element t => Matrix t -> Vector t
    LA.takeDiag (L n n -> Matrix ℝ
    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 = Vector ℂ -> C n
    forall (n :: Nat). Vector ℂ -> C n
    mkC (Matrix ℂ -> Vector ℂ
    forall t. Element t => Matrix t -> Vector t
    LA.takeDiag (M n n -> Matrix ℂ
    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) = Vector ℂ -> C n
    forall (n :: Nat). Vector ℂ -> C n
    mkC (Vector ℂ -> C n) -> Vector ℂ -> C n
    forall a b. (a -> b) -> a -> b
    $ (Vector ℝ, Vector ℝ) -> Vector ℂ
    forall t (c :: * -> *).
    (Convert t, Complexable c, RealElement t) =>
    (c t, c t) -> c (Complex t)
    forall (c :: * -> *).
    (Complexable c, RealElement ℝ) =>
    (c ℝ, c ℝ) -> c ℂ
    LA.toComplex (R n -> Vector ℝ
    forall (n :: Nat). R n -> Vector ℝ
    ud1 R n
    r, R n -> Vector ℝ
    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) = Vector ℂ -> (Vector ℝ, Vector ℝ)
    forall t (c :: * -> *).
    (Convert t, Complexable c, RealElement t) =>
    c (Complex t) -> (c t, c t)
    forall (c :: * -> *).
    (Complexable c, RealElement ℝ) =>
    c ℂ -> (c ℝ, c ℝ)
    LA.fromComplex Vector ℂ
    v in (Vector ℝ -> R n
    forall (n :: Nat). Vector ℝ -> R n
    mkR Vector ℝ
    r, Vector ℝ -> R n
    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 = Vector ℂ -> C n
    forall (n :: Nat). Vector ℂ -> C n
    mkC (Vector ℂ -> C n) -> Vector ℂ -> C n
    forall a b. (a -> b) -> a -> b
    $ (Vector ℝ, Vector ℝ) -> Vector ℂ
    forall t (c :: * -> *).
    (Convert t, Complexable c, RealElement t) =>
    (c t, c t) -> c (Complex t)
    forall (c :: * -> *).
    (Complexable c, RealElement ℝ) =>
    (c ℝ, c ℝ) -> c ℂ
    LA.toComplex (R n -> Vector ℝ
    forall (n :: Nat). R n -> Vector ℝ
    ud1 R n
    r, ℝ -> IndexOf Vector -> Vector ℝ
    forall e d (c :: * -> *). Konst e d c => e -> d -> c e
    LA.konst ℝ
    0 (R n -> IndexOf Vector
    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 = (R n, R n) -> R n
    forall a b. (a, b) -> a
    fst ((R n, R n) -> R n) -> (C n -> (R n, R n)) -> C n -> R n
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . C n -> (R n, R n)
    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 = (R n, R n) -> R n
    forall a b. (a, b) -> b
    snd ((R n, R n) -> R n) -> (C n -> (R n, R n)) -> C n -> R n
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . C n -> (R n, R n)
    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) = C n -> (R n, R n)
    forall (n :: Nat). KnownNat n => C n -> (R n, R n)
    fromComplex C n
    c in R n
    rR n -> R n -> R n
    forall a. Floating a => a -> a -> a
    **R n
    2 R n -> R n -> R n
    forall a. Num a => a -> a -> a
    + R n
    iR n -> R n -> R n
    forall 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 = R n -> R n
    forall a. Floating a => a -> a
    sqrt (R n -> R n) -> (C n -> R n) -> C n -> R n
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . C n -> R n
    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 (L m m -> Matrix ℝ
    forall t s (d :: * -> *). Sized t s d => s -> d t
    extract -> Matrix ℝ
    a) (L m n -> Matrix ℝ
    forall t s (d :: * -> *). Sized t s d => s -> d t
    extract -> Matrix ℝ
    b) = (Matrix ℝ -> L m n) -> Maybe (Matrix ℝ) -> Maybe (L m n)
    forall a b. (a -> b) -> Maybe a -> Maybe b
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap Matrix ℝ -> L m n
    forall (m :: Nat) (n :: Nat). Matrix ℝ -> L m n
    mkL (Matrix ℝ -> Matrix ℝ -> Maybe (Matrix ℝ)
    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
    (L m n -> Matrix ℝ
    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
    <\> (L m r -> Matrix ℝ
    forall t s (d :: * -> *). Sized t s d => s -> d t
    extract -> Matrix ℝ
    b) = Matrix ℝ -> L n r
    forall (m :: Nat) (n :: Nat). Matrix ℝ -> L m n
    mkL (Matrix ℝ
    a Matrix ℝ -> Matrix ℝ -> Matrix ℝ
    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 (L m n -> Matrix ℝ
    forall t s (d :: * -> *). Sized t s d => s -> d t
    extract -> Matrix ℝ
    m) = (Matrix ℝ -> L m m
    forall (m :: Nat) (n :: Nat). Matrix ℝ -> L m n
    mkL Matrix ℝ
    u, Vector ℝ -> R n
    forall (n :: Nat). Vector ℝ -> R n
    mkR Vector ℝ
    s', Matrix ℝ -> L n n
    forall (m :: Nat) (n :: Nat). Matrix ℝ -> L m n
    mkL Matrix ℝ
    v)
      where
        (Matrix ℝ
    u,Vector ℝ
    s,Matrix ℝ
    v) = Matrix ℝ -> (Matrix ℝ, Vector ℝ, Matrix ℝ)
    forall t. Field t => Matrix t -> (Matrix t, Vector ℝ, Matrix t)
    LA.svd Matrix ℝ
    m
        s' :: Vector ℝ
    s' = [Vector ℝ] -> Vector ℝ
    forall t. Storable t => [Vector t] -> Vector t
    vjoin [Vector ℝ
    s, Vector ℝ
    z]
        z :: Vector ℝ
    z = ℝ -> Int -> Vector ℝ
    forall e d (c :: * -> *). Konst e d c => e -> d -> c e
    LA.konst ℝ
    0 (Int -> Int -> Int
    forall a. Ord a => a -> a -> a
    max Int
    0 (Matrix ℝ -> Int
    forall t. Matrix t -> Int
    cols Matrix ℝ
    m Int -> Int -> Int
    forall a. Num a => a -> a -> a
    - Vector ℝ -> IndexOf Vector
    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 (L m n -> Matrix ℝ
    forall t s (d :: * -> *). Sized t s d => s -> d t
    extract -> Matrix ℝ
    m) = (Matrix ℝ -> L m n
    forall (m :: Nat) (n :: Nat). Matrix ℝ -> L m n
    mkL Matrix ℝ
    u, Vector ℝ -> R n
    forall (n :: Nat). Vector ℝ -> R n
    mkR Vector ℝ
    s, Matrix ℝ -> L n n
    forall (m :: Nat) (n :: Nat). Matrix ℝ -> L m n
    mkL Matrix ℝ
    v)
      where
        (Matrix ℝ
    u,Vector ℝ
    s,Matrix ℝ
    v) = Matrix ℝ -> (Matrix ℝ, Vector ℝ, Matrix ℝ)
    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 (L m n -> Matrix ℝ
    forall t s (d :: * -> *). Sized t s d => s -> d t
    extract -> Matrix ℝ
    m) = (Matrix ℝ -> L m m
    forall (m :: Nat) (n :: Nat). Matrix ℝ -> L m n
    mkL Matrix ℝ
    u, Vector ℝ -> R m
    forall (n :: Nat). Vector ℝ -> R n
    mkR Vector ℝ
    s, Matrix ℝ -> L n m
    forall (m :: Nat) (n :: Nat). Matrix ℝ -> L m n
    mkL Matrix ℝ
    v)
      where
        (Matrix ℝ
    u,Vector ℝ
    s,Matrix ℝ
    v) = Matrix ℝ -> (Matrix ℝ, Vector ℝ, Matrix ℝ)
    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
    [Sym n] -> ShowS
    Sym n -> String
    (Int -> Sym n -> ShowS)
    -> (Sym n -> String) -> ([Sym n] -> ShowS) -> Show (Sym n)
    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
    $cshowsPrec :: forall (n :: Nat). KnownNat n => Int -> Sym n -> ShowS
    showsPrec :: Int -> Sym n -> ShowS
    $cshow :: forall (n :: Nat). KnownNat n => Sym n -> String
    show :: Sym n -> String
    $cshowList :: forall (n :: Nat). KnownNat n => [Sym n] -> ShowS
    showList :: [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 = Sq n -> Sym n
    forall (n :: Nat). Sq n -> Sym n
    Sym (Sq n -> Sym n) -> Sq n -> Sym n
    forall a b. (a -> b) -> a -> b
    $ (Sq n
    m Sq n -> Sq n -> Sq n
    forall a. Num a => a -> a -> a
    + Sq n -> Sq n
    forall m mt. Transposable m mt => m -> mt
    tr Sq n
    m)Sq n -> Sq n -> Sq n
    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 = Sq n -> Sym n
    forall (n :: Nat). Sq n -> Sym n
    Sym (L m n -> L n m
    forall m mt. Transposable m mt => m -> mt
    tr L m n
    x L n m -> L m n -> Sq n
    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
    𝑖 = ℂ -> 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 = M n n -> Her n
    forall (n :: Nat). M n n -> Her n
    Her (M n n -> Her n) -> M n n -> Her n
    forall a b. (a -> b) -> a -> b
    $ (M n n
    m M n n -> M n n -> M n n
    forall a. Num a => a -> a -> a
    + M n n -> M n n
    forall m mt. Transposable m mt => m -> mt
    LA.tr M n n
    m)M n n -> M n n -> M n n
    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 = Sq n -> Matrix ℝ
    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
            String -> Int -> IO ()
    forall r. PrintfType r => String -> r
    printf String
    "Sym %d" (Matrix ℝ -> Int
    forall t. Matrix t -> Int
    cols Matrix ℝ
    a) IO () -> IO () -> IO ()
    forall a b. IO a -> IO b -> IO b
    forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
    >> String -> IO ()
    putStr ((Char -> Bool) -> ShowS
    forall a. (a -> Bool) -> [a] -> [a]
    dropWhile (Char -> Char -> Bool
    forall a. Eq a => a -> a -> Bool
    /=Char
    '\n') ShowS -> ShowS
    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 = M n n -> Matrix ℂ
    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
            String -> Int -> IO ()
    forall r. PrintfType r => String -> r
    printf String
    "Her %d" (Matrix ℂ -> Int
    forall t. Matrix t -> Int
    cols Matrix ℂ
    a) IO () -> IO () -> IO ()
    forall a b. IO a -> IO b -> IO b
    forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
    >> String -> IO ()
    putStr ((Char -> Bool) -> ShowS
    forall a. (a -> Bool) -> [a] -> [a]
    dropWhile (Char -> Char -> Bool
    forall a. Eq a => a -> a -> Bool
    /=Char
    '\n') ShowS -> ShowS
    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 (L n n -> Matrix ℝ
    forall t s (d :: * -> *). Sized t s d => s -> d t
    extract -> Matrix ℝ
    m)) =  Vector ℝ -> R n
    forall (n :: Nat). Vector ℝ -> R n
    mkR (Vector ℝ -> R n) -> (Matrix ℝ -> Vector ℝ) -> Matrix ℝ -> R n
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Herm ℝ -> Vector ℝ
    forall t. Field t => Herm t -> Vector ℝ
    LA.eigenvaluesSH (Herm ℝ -> Vector ℝ)
    -> (Matrix ℝ -> Herm ℝ) -> Matrix ℝ -> Vector ℝ
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Matrix ℝ -> Herm ℝ
    forall t. Matrix t -> Herm t
    LA.trustSym (Matrix ℝ -> R n) -> Matrix ℝ -> R n
    forall a b. (a -> b) -> a -> b
    $ Matrix ℝ
    m
        eigensystem :: Sym n -> (R n, L n n)
    eigensystem (Sym (L n n -> Matrix ℝ
    forall t s (d :: * -> *). Sized t s d => s -> d t
    extract -> Matrix ℝ
    m)) = (Vector ℝ -> R n
    forall (n :: Nat). Vector ℝ -> R n
    mkR Vector ℝ
    l, Matrix ℝ -> L n n
    forall (m :: Nat) (n :: Nat). Matrix ℝ -> L m n
    mkL Matrix ℝ
    v)
          where
            (Vector ℝ
    l,Matrix ℝ
    v) = Herm ℝ -> (Vector ℝ, Matrix ℝ)
    forall t. Field t => Herm t -> (Vector ℝ, Matrix t)
    LA.eigSH (Herm ℝ -> (Vector ℝ, Matrix ℝ))
    -> (Matrix ℝ -> Herm ℝ) -> Matrix ℝ -> (Vector ℝ, Matrix ℝ)
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Matrix ℝ -> Herm ℝ
    forall t. Matrix t -> Herm t
    LA.trustSym (Matrix ℝ -> (Vector ℝ, Matrix ℝ))
    -> Matrix ℝ -> (Vector ℝ, Matrix ℝ)
    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 (Sq n -> Matrix ℝ
    forall t s (d :: * -> *). Sized t s d => s -> d t
    extract -> Matrix ℝ
    m) = Vector ℂ -> C n
    forall (n :: Nat). Vector ℂ -> C n
    mkC (Vector ℂ -> C n) -> (Matrix ℝ -> Vector ℂ) -> Matrix ℝ -> C n
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Matrix ℝ -> Vector ℂ
    forall t. Field t => Matrix t -> Vector ℂ
    LA.eigenvalues (Matrix ℝ -> C n) -> Matrix ℝ -> C n
    forall a b. (a -> b) -> a -> b
    $ Matrix ℝ
    m
        eigensystem :: Sq n -> (C n, M n n)
    eigensystem (Sq n -> Matrix ℝ
    forall t s (d :: * -> *). Sized t s d => s -> d t
    extract -> Matrix ℝ
    m) = (Vector ℂ -> C n
    forall (n :: Nat). Vector ℂ -> C n
    mkC Vector ℂ
    l, Matrix ℂ -> M n n
    forall (m :: Nat) (n :: Nat). Matrix ℂ -> M m n
    mkM Matrix ℂ
    v)
          where
            (Vector ℂ
    l,Matrix ℂ
    v) = Matrix ℝ -> (Vector ℂ, Matrix ℂ)
    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 (Sq n -> Matrix ℝ
    forall t s (d :: * -> *). Sized t s d => s -> d t
    extract (Sq n -> Matrix ℝ) -> (Sym n -> Sq n) -> Sym n -> Matrix ℝ
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Sym n -> Sq n
    forall (n :: Nat). Sym n -> Sq n
    unSym -> Matrix ℝ
    m) = Matrix ℝ -> Sq n
    forall (m :: Nat) (n :: Nat). Matrix ℝ -> L m n
    mkL (Matrix ℝ -> Sq n) -> Matrix ℝ -> Sq n
    forall a b. (a -> b) -> a -> b
    $ Herm ℝ -> Matrix ℝ
    forall t. Field t => Herm t -> Matrix t
    LA.chol (Herm ℝ -> Matrix ℝ) -> Herm ℝ -> Matrix ℝ
    forall a b. (a -> b) -> a -> b
    $ Matrix ℝ -> Herm ℝ
    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 (Matrix ℝ -> Matrix ℝ
    forall {t}. Field t => Matrix t -> Matrix t
    LA.nullspace (Matrix ℝ -> Matrix ℝ) -> (L m n -> Matrix ℝ) -> L m n -> Matrix ℝ
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . L m n -> Matrix ℝ
    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 (Integer -> Maybe SomeNat) -> Integer -> Maybe SomeNat
    forall a b. (a -> b) -> a -> b
    $ Int -> Integer
    forall a b. (Integral a, Num b) => a -> b
    fromIntegral (Int -> Integer) -> Int -> Integer
    forall a b. (a -> b) -> a -> b
    $ Matrix ℝ -> Int
    forall t. Matrix t -> Int
    cols Matrix ℝ
    a of
           Maybe SomeNat
    Nothing -> String -> z
    forall a. HasCallStack => String -> a
    error String
    "static/dynamic mismatch"
           Just (SomeNat (Proxy n
    _ :: Proxy k)) -> L n n -> z
    forall (k :: Nat). KnownNat k => L n k -> z
    f (Matrix ℝ -> L n n
    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 (Matrix ℝ -> Matrix ℝ
    forall {t}. Field t => Matrix t -> Matrix t
    LA.orth (Matrix ℝ -> Matrix ℝ) -> (L m n -> Matrix ℝ) -> L m n -> Matrix ℝ
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . L m n -> Matrix ℝ
    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 (Integer -> Maybe SomeNat) -> Integer -> Maybe SomeNat
    forall a b. (a -> b) -> a -> b
    $ Int -> Integer
    forall a b. (Integral a, Num b) => a -> b
    fromIntegral (Int -> Integer) -> Int -> Integer
    forall a b. (a -> b) -> a -> b
    $ Matrix ℝ -> Int
    forall t. Matrix t -> Int
    cols Matrix ℝ
    a of
           Maybe SomeNat
    Nothing -> String -> z
    forall a. HasCallStack => String -> a
    error String
    "static/dynamic mismatch"
           Just (SomeNat (Proxy n
    _ :: Proxy k)) -> L n n -> z
    forall (k :: Nat). KnownNat k => L n k -> z
    f (Matrix ℝ -> L n n
    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 (Matrix ℝ -> (Matrix ℝ, Vector ℝ, Matrix ℝ)
    forall t. Field t => Matrix t -> (Matrix t, Vector ℝ, Matrix t)
    LA.compactSVD (Matrix ℝ -> (Matrix ℝ, Vector ℝ, Matrix ℝ))
    -> (L m n -> Matrix ℝ) -> L m n -> (Matrix ℝ, Vector ℝ, Matrix ℝ)
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . L m n -> Matrix ℝ
    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 (Integer -> Maybe SomeNat) -> Integer -> Maybe SomeNat
    forall a b. (a -> b) -> a -> b
    $ Int -> Integer
    forall a b. (Integral a, Num b) => a -> b
    fromIntegral (Int -> Integer) -> Int -> Integer
    forall a b. (a -> b) -> a -> b
    $ Vector ℝ -> IndexOf Vector
    forall (c :: * -> *) t. Container c t => c t -> IndexOf c
    LA.size Vector ℝ
    s of
           Maybe SomeNat
    Nothing -> String -> z
    forall a. HasCallStack => String -> a
    error String
    "static/dynamic mismatch"
           Just (SomeNat (Proxy n
    _ :: Proxy k)) -> (L m n, R n, L n n) -> z
    forall (k :: Nat). KnownNat k => (L m k, R k, L n k) -> z
    f (Matrix ℝ -> L m n
    forall (m :: Nat) (n :: Nat). Matrix ℝ -> L m n
    mkL Matrix ℝ
    u :: L m k, Vector ℝ -> R n
    forall (n :: Nat). Vector ℝ -> R n
    mkR Vector ℝ
    s :: R k, Matrix ℝ -> L n n
    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 (L m n -> Matrix ℝ
    forall t s (d :: * -> *). Sized t s d => s -> d t
    extract -> Matrix ℝ
    x) = (Matrix ℝ -> L m m
    forall (m :: Nat) (n :: Nat). Matrix ℝ -> L m n
    mkL Matrix ℝ
    q, Matrix ℝ -> L m n
    forall (m :: Nat) (n :: Nat). Matrix ℝ -> L m n
    mkL Matrix ℝ
    r)
      where
        (Matrix ℝ
    q,Matrix ℝ
    r) = Matrix ℝ -> (Matrix ℝ, Matrix ℝ)
    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 (R n -> Vector ℝ
    forall t s (d :: * -> *). Sized t s d => s -> d t
    extract -> Vector ℝ
    v) = ( Vector ℝ -> R p
    forall (n :: Nat). Vector ℝ -> R n
    mkR (Int -> Int -> Vector ℝ -> Vector ℝ
    forall t. Storable t => Int -> Int -> Vector t -> Vector t
    subVector Int
    0 Int
    p' Vector ℝ
    v) ,
                             Vector ℝ -> R (n - p)
    forall (n :: Nat). Vector ℝ -> R n
    mkR (Int -> Int -> Vector ℝ -> Vector ℝ
    forall t. Storable t => Int -> Int -> Vector t -> Vector t
    subVector Int
    p' (Vector ℝ -> IndexOf Vector
    forall (c :: * -> *) t. Container c t => c t -> IndexOf c
    LA.size Vector ℝ
    v Int -> Int -> Int
    forall a. Num a => a -> a -> a
    - Int
    p') Vector ℝ
    v) )
      where
        p' :: Int
    p' = Integer -> Int
    forall a b. (Integral a, Num b) => a -> b
    fromIntegral (Integer -> Int) -> (Proxy p -> Integer) -> Proxy p -> Int
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Proxy p -> Integer
    forall (n :: Nat) (proxy :: Nat -> *).
    KnownNat n =>
    proxy n -> Integer
    natVal (Proxy p -> Int) -> Proxy p -> Int
    forall a b. (a -> b) -> a -> b
    $ (Proxy p
    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 = ((Vector ℝ -> Int -> ℝ
    forall c t. Indexable c t => c -> Int -> t
    ! Int
    0) (Vector ℝ -> ℝ) -> (R 1 -> Vector ℝ) -> R 1 -> ℝ
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . R 1 -> Vector ℝ
    forall t s (d :: * -> *). Sized t s d => s -> d t
    extract (R 1 -> ℝ)
    -> (R (n - 1) -> R (n - 1)) -> (R 1, R (n - 1)) -> (ℝ, R (n - 1))
    forall b c b' c'. (b -> c) -> (b' -> c') -> (b, b') -> (c, c')
    forall (a :: * -> * -> *) b c b' c'.
    Arrow a =>
    a b c -> a b' c' -> a (b, b') (c, c')
    *** R (n - 1) -> R (n - 1)
    forall a. a -> a
    id) ((R 1, R (n - 1)) -> (ℝ, R (n - 1)))
    -> (R n -> (R 1, R (n - 1))) -> R n -> (ℝ, R (n - 1))
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . R n -> (R 1, R (n - 1))
    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 (L m n -> Matrix ℝ
    forall t s (d :: * -> *). Sized t s d => s -> d t
    extract -> Matrix ℝ
    x) = ( Matrix ℝ -> L p n
    forall (m :: Nat) (n :: Nat). Matrix ℝ -> L m n
    mkL (Int -> Matrix ℝ -> Matrix ℝ
    forall t. Element t => Int -> Matrix t -> Matrix t
    takeRows Int
    p' Matrix ℝ
    x) ,
                                 Matrix ℝ -> L (m - p) n
    forall (m :: Nat) (n :: Nat). Matrix ℝ -> L m n
    mkL (Int -> Matrix ℝ -> Matrix ℝ
    forall t. Element t => Int -> Matrix t -> Matrix t
    dropRows Int
    p' Matrix ℝ
    x) )
      where
        p' :: Int
    p' = Integer -> Int
    forall a b. (Integral a, Num b) => a -> b
    fromIntegral (Integer -> Int) -> (Proxy p -> Integer) -> Proxy p -> Int
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Proxy p -> Integer
    forall (n :: Nat) (proxy :: Nat -> *).
    KnownNat n =>
    proxy n -> Integer
    natVal (Proxy p -> Int) -> Proxy p -> Int
    forall a b. (a -> b) -> a -> b
    $ (Proxy p
    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 = (L p m -> L m p
    forall m mt. Transposable m mt => m -> mt
    tr (L p m -> L m p)
    -> (L (n - p) m -> L m (n - p))
    -> (L p m, L (n - p) m)
    -> (L m p, L m (n - p))
    forall b c b' c'. (b -> c) -> (b' -> c') -> (b, b') -> (c, c')
    forall (a :: * -> * -> *) b c b' c'.
    Arrow a =>
    a b c -> a b' c' -> a (b, b') (c, c')
    *** L (n - p) m -> L m (n - p)
    forall m mt. Transposable m mt => m -> mt
    tr) ((L p m, L (n - p) m) -> (L m p, L m (n - p)))
    -> (L m n -> (L p m, L (n - p) m)) -> L m n -> (L m p, L m (n - p))
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . L n m -> (L p m, L (n - p) m)
    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 (L n m -> (L p m, L (n - p) m))
    -> (L m n -> L n m) -> L m n -> (L p m, L (n - p) m)
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . L m n -> L n m
    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 (Matrix ℝ -> [Vector ℝ]
    forall t. Element t => Matrix t -> [Vector t]
    LA.toRows (Matrix ℝ -> [Vector ℝ])
    -> (L m n -> Matrix ℝ) -> L m n -> [Vector ℝ]
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . L m n -> Matrix ℝ
    forall t s (d :: * -> *). Sized t s d => s -> d t
    extract -> [Vector ℝ]
    vs) = (Vector ℝ -> R n) -> [Vector ℝ] -> [R n]
    forall a b. (a -> b) -> [a] -> [b]
    map Vector ℝ -> R n
    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 ([Vector ℝ] -> Matrix ℝ
    forall t. Element t => [Vector t] -> Matrix t
    LA.fromRows ([Vector ℝ] -> Matrix ℝ)
    -> ([R n] -> [Vector ℝ]) -> [R n] -> Matrix ℝ
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (R n -> Vector ℝ) -> [R n] -> [Vector ℝ]
    forall a b. (a -> b) -> [a] -> [b]
    map R n -> Vector ℝ
    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 (Integer -> Maybe SomeNat) -> Integer -> Maybe SomeNat
    forall a b. (a -> b) -> a -> b
    $ Int -> Integer
    forall a b. (Integral a, Num b) => a -> b
    fromIntegral (Int -> Integer) -> Int -> Integer
    forall a b. (a -> b) -> a -> b
    $ Matrix ℝ -> Int
    forall t. Matrix t -> Int
    LA.rows Matrix ℝ
    m of
           Maybe SomeNat
    Nothing -> String -> z
    forall a. HasCallStack => String -> a
    error String
    "static/dynamic mismatch"
           Just (SomeNat (Proxy n
    _ :: Proxy m)) -> L n n -> z
    forall (m :: Nat). KnownNat m => L m n -> z
    f (Matrix ℝ -> L n n
    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 (Matrix ℝ -> [Vector ℝ]
    forall t. Element t => Matrix t -> [Vector t]
    LA.toColumns (Matrix ℝ -> [Vector ℝ])
    -> (L m n -> Matrix ℝ) -> L m n -> [Vector ℝ]
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . L m n -> Matrix ℝ
    forall t s (d :: * -> *). Sized t s d => s -> d t
    extract -> [Vector ℝ]
    vs) = (Vector ℝ -> R m) -> [Vector ℝ] -> [R m]
    forall a b. (a -> b) -> [a] -> [b]
    map Vector ℝ -> R m
    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 ([Vector ℝ] -> Matrix ℝ
    forall t. Element t => [Vector t] -> Matrix t
    LA.fromColumns ([Vector ℝ] -> Matrix ℝ)
    -> ([R m] -> [Vector ℝ]) -> [R m] -> Matrix ℝ
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (R m -> Vector ℝ) -> [R m] -> [Vector ℝ]
    forall a b. (a -> b) -> [a] -> [b]
    map R m -> Vector ℝ
    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 (Integer -> Maybe SomeNat) -> Integer -> Maybe SomeNat
    forall a b. (a -> b) -> a -> b
    $ Int -> Integer
    forall a b. (Integral a, Num b) => a -> b
    fromIntegral (Int -> Integer) -> Int -> Integer
    forall a b. (a -> b) -> a -> b
    $ Matrix ℝ -> Int
    forall t. Matrix t -> Int
    LA.cols Matrix ℝ
    m of
           Maybe SomeNat
    Nothing -> String -> z
    forall a. HasCallStack => String -> a
    error String
    "static/dynamic mismatch"
           Just (SomeNat (Proxy n
    _ :: Proxy n)) -> L m n -> z
    forall (n :: Nat). KnownNat n => L m n -> z
    f (Matrix ℝ -> L m n
    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 = Matrix ℝ -> L m n
    forall (m :: Nat) (n :: Nat). Matrix ℝ -> L m n
    mkL (Matrix ℝ -> L m n) -> Matrix ℝ -> L m n
    forall a b. (a -> b) -> a -> b
    $ IndexOf Matrix -> (ℝ -> ℝ -> ℝ) -> Matrix ℝ
    forall d f (c :: * -> *) e. Build d f c e => d -> f -> c e
    LA.build (L m n -> IndexOf Matrix
    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 (Integer -> Maybe SomeNat) -> Integer -> Maybe SomeNat
    forall a b. (a -> b) -> a -> b
    $ Int -> Integer
    forall a b. (Integral a, Num b) => a -> b
    fromIntegral (Int -> Integer) -> Int -> Integer
    forall a b. (a -> b) -> a -> b
    $ Vector ℝ -> IndexOf Vector
    forall (c :: * -> *) t. Container c t => c t -> IndexOf c
    LA.size Vector ℝ
    v of
           Maybe SomeNat
    Nothing -> String -> z
    forall a. HasCallStack => String -> a
    error String
    "static/dynamic mismatch"
           Just (SomeNat (Proxy n
    _ :: Proxy m)) -> R n -> z
    forall (n :: Nat). KnownNat n => R n -> z
    f (Vector ℝ -> R n
    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
        Refl <- Proxy n -> Proxy m -> Maybe (n :~: m)
    forall (a :: Nat) (b :: Nat) (proxy1 :: Nat -> *)
           (proxy2 :: Nat -> *).
    (KnownNat a, KnownNat b) =>
    proxy1 a -> proxy2 b -> Maybe (a :~: b)
    sameNat (Proxy n
    forall {k} (t :: k). Proxy t
    Proxy :: Proxy n) (Proxy m
    forall {k} (t :: k). Proxy t
    Proxy :: Proxy m)
        return $ mkR (unwrap 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 (Integer -> Maybe SomeNat) -> Integer -> Maybe SomeNat
    forall a b. (a -> b) -> a -> b
    $ Int -> Integer
    forall a b. (Integral a, Num b) => a -> b
    fromIntegral (Int -> Integer) -> Int -> Integer
    forall a b. (a -> b) -> a -> b
    $ Matrix ℝ -> Int
    forall t. Matrix t -> Int
    rows Matrix ℝ
    a of
           Maybe SomeNat
    Nothing -> String -> z
    forall a. HasCallStack => String -> a
    error String
    "static/dynamic mismatch"
           Just (SomeNat (Proxy n
    _ :: Proxy m)) ->
               case Integer -> Maybe SomeNat
    someNatVal (Integer -> Maybe SomeNat) -> Integer -> Maybe SomeNat
    forall a b. (a -> b) -> a -> b
    $ Int -> Integer
    forall a b. (Integral a, Num b) => a -> b
    fromIntegral (Int -> Integer) -> Int -> Integer
    forall a b. (a -> b) -> a -> b
    $ Matrix ℝ -> Int
    forall t. Matrix t -> Int
    cols Matrix ℝ
    a of
                   Maybe SomeNat
    Nothing -> String -> z
    forall a. HasCallStack => String -> a
    error String
    "static/dynamic mismatch"
                   Just (SomeNat (Proxy n
    _ :: Proxy n)) ->
                      L n n -> z
    forall (m :: Nat) (n :: Nat).
    (KnownNat m, KnownNat n) =>
    L m n -> z
    f (Matrix ℝ -> L n n
    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
        Refl <- Proxy m -> Proxy j -> Maybe (m :~: j)
    forall (a :: Nat) (b :: Nat) (proxy1 :: Nat -> *)
           (proxy2 :: Nat -> *).
    (KnownNat a, KnownNat b) =>
    proxy1 a -> proxy2 b -> Maybe (a :~: b)
    sameNat (Proxy m
    forall {k} (t :: k). Proxy t
    Proxy :: Proxy m) (Proxy j
    forall {k} (t :: k). Proxy t
    Proxy :: Proxy j)
        Refl <- sameNat (Proxy :: Proxy n) (Proxy :: Proxy k)
        return $ mkL (unwrap 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 = Vector ℝ -> R n
    forall (n :: Nat). Vector ℝ -> R n
    mkR (Int -> RandDist -> Int -> Vector ℝ
    LA.randomVector Int
    s RandDist
    d
                              (Integer -> Int
    forall a. Num a => Integer -> a
    fromInteger (Proxy n -> Integer
    forall (n :: Nat) (proxy :: Nat -> *).
    KnownNat n =>
    proxy n -> Integer
    natVal (Proxy n
    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 = Matrix ℝ -> L m n
    forall (m :: Nat) (n :: Nat). Matrix ℝ -> L m n
    mkL (Matrix ℝ -> L m n) -> IO (Matrix ℝ) -> IO (L m n)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Int -> Int -> IO (Matrix ℝ)
    LA.rand (Integer -> Int
    forall a. Num a => Integer -> a
    fromInteger (Proxy m -> Integer
    forall (n :: Nat) (proxy :: Nat -> *).
    KnownNat n =>
    proxy n -> Integer
    natVal (Proxy m
    forall {k} (t :: k). Proxy t
    Proxy :: Proxy m)))
                           (Integer -> Int
    forall a. Num a => Integer -> a
    fromInteger (Proxy n -> Integer
    forall (n :: Nat) (proxy :: Nat -> *).
    KnownNat n =>
    proxy n -> Integer
    natVal (Proxy n
    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 = Matrix ℝ -> L m n
    forall (m :: Nat) (n :: Nat). Matrix ℝ -> L m n
    mkL (Matrix ℝ -> L m n) -> IO (Matrix ℝ) -> IO (L m n)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Int -> Int -> IO (Matrix ℝ)
    LA.randn (Integer -> Int
    forall a. Num a => Integer -> a
    fromInteger (Proxy m -> Integer
    forall (n :: Nat) (proxy :: Nat -> *).
    KnownNat n =>
    proxy n -> Integer
    natVal (Proxy m
    forall {k} (t :: k). Proxy t
    Proxy :: Proxy m)))
                             (Integer -> Int
    forall a. Num a => Integer -> a
    fromInteger (Proxy n -> Integer
    forall (n :: Nat) (proxy :: Nat -> *).
    KnownNat n =>
    proxy n -> Integer
    natVal (Proxy n
    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 (R n -> Vector ℝ
    forall t s (d :: * -> *). Sized t s d => s -> d t
    extract -> Vector ℝ
    mu) (Sym (Sq n -> Matrix ℝ
    forall t s (d :: * -> *). Sized t s d => s -> d t
    extract -> Matrix ℝ
    sigma)) =
        Matrix ℝ -> L m n
    forall (m :: Nat) (n :: Nat). Matrix ℝ -> L m n
    mkL (Matrix ℝ -> L m n) -> Matrix ℝ -> L m n
    forall a b. (a -> b) -> a -> b
    $ Int -> Int -> Vector ℝ -> Herm ℝ -> Matrix ℝ
    LA.gaussianSample Int
    s (Integer -> Int
    forall a. Num a => Integer -> a
    fromInteger (Proxy m -> Integer
    forall (n :: Nat) (proxy :: Nat -> *).
    KnownNat n =>
    proxy n -> Integer
    natVal (Proxy m
    forall {k} (t :: k). Proxy t
    Proxy :: Proxy m)))
                                Vector ℝ
    mu (Matrix ℝ -> Herm ℝ
    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 (R n -> Vector ℝ
    forall t s (d :: * -> *). Sized t s d => s -> d t
    extract -> Vector ℝ
    mins) (R n -> Vector ℝ
    forall t s (d :: * -> *). Sized t s d => s -> d t
    extract -> Vector ℝ
    maxs) =
        Matrix ℝ -> L m n
    forall (m :: Nat) (n :: Nat). Matrix ℝ -> L m n
    mkL (Matrix ℝ -> L m n) -> Matrix ℝ -> L m n
    forall a b. (a -> b) -> a -> b
    $ Int -> Int -> [(ℝ, ℝ)] -> Matrix ℝ
    LA.uniformSample Int
    s (Integer -> Int
    forall a. Num a => Integer -> a
    fromInteger (Proxy m -> Integer
    forall (n :: Nat) (proxy :: Nat -> *).
    KnownNat n =>
    proxy n -> Integer
    natVal (Proxy m
    forall {k} (t :: k). Proxy t
    Proxy :: Proxy m)))
                               ([ℝ] -> [ℝ] -> [(ℝ, ℝ)]
    forall a b. [a] -> [b] -> [(a, b)]
    zip (Vector ℝ -> [ℝ]
    forall a. Storable a => Vector a -> [a]
    LA.toList Vector ℝ
    mins) (Vector ℝ -> [ℝ]
    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 (L m n -> Matrix ℝ
    forall t s (d :: * -> *). Sized t s d => s -> d t
    extract -> Matrix ℝ
    vs) = Vector ℝ -> R n
    forall (n :: Nat). Vector ℝ -> R n
    mkR (Vector ℝ -> R n)
    -> (Herm ℝ -> Sym n) -> (Vector ℝ, Herm ℝ) -> (R n, Sym n)
    forall b c b' c'. (b -> c) -> (b' -> c') -> (b, b') -> (c, c')
    forall (a :: * -> * -> *) b c b' c'.
    Arrow a =>
    a b c -> a b' c' -> a (b, b') (c, c')
    *** (Sq n -> Sym n
    forall (n :: Nat). Sq n -> Sym n
    Sym (Sq n -> Sym n) -> (Herm ℝ -> Sq n) -> Herm ℝ -> Sym n
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Matrix ℝ -> Sq n
    forall (m :: Nat) (n :: Nat). Matrix ℝ -> L m n
    mkL (Matrix ℝ -> Sq n) -> (Herm ℝ -> Matrix ℝ) -> Herm ℝ -> Sq n
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Herm ℝ -> Matrix ℝ
    forall t. Herm t -> Matrix t
    LA.unSym) ((Vector ℝ, Herm ℝ) -> (R n, Sym n))
    -> (Vector ℝ, Herm ℝ) -> (R n, Sym n)
    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 = 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
        app :: forall (m :: Nat) (n :: Nat).
    (KnownNat m, KnownNat n) =>
    L m n -> R n -> R m
    app = L m n -> R n -> R m
    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 = R n -> R n -> ℝ
    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 = ℝ -> R k -> L m n
    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 = (ℝ -> ℝ) -> R n -> R n
    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 = (ℝ -> ℝ) -> L n m -> L n m
    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 = R n -> R m -> L n m
    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 = (ℝ -> ℝ -> ℝ) -> R n -> R n -> R n
    forall (n :: Nat). KnownNat n => (ℝ -> ℝ -> ℝ) -> R n -> R n -> R n
    zipWithR
        det :: forall (n :: Nat). KnownNat n => L n n -> ℝ
    det = Sq n -> ℝ
    forall (n :: Nat). KnownNat n => L n n -> ℝ
    detL
        invlndet :: forall (n :: Nat). KnownNat n => L n n -> (L n n, (ℝ, ℝ))
    invlndet = Sq n -> (Sq n, (ℝ, ℝ))
    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 = Sq n -> Sq n
    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 = Sq n -> Sq n
    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 = Sq n -> Sq n
    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 = M m k -> M k n -> M m n
    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 = M m n -> C n -> C m
    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 = C n -> C n -> ℂ
    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 = ℂ -> C k -> M m n
    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 = (ℂ -> ℂ) -> C n -> C n
    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 = (ℂ -> ℂ) -> M n m -> M n m
    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 = C n -> C m -> M n m
    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 = (ℂ -> ℂ -> ℂ) -> C n -> C n -> C n
    forall (n :: Nat). KnownNat n => (ℂ -> ℂ -> ℂ) -> C n -> C n -> C n
    zipWithC
        det :: forall (n :: Nat). KnownNat n => M n n -> ℂ
    det = M n n -> ℂ
    forall (n :: Nat). KnownNat n => M n n -> ℂ
    detM
        invlndet :: forall (n :: Nat). KnownNat n => M n n -> (M n n, (ℂ, ℂ))
    invlndet = M n n -> (M n n, (ℂ, ℂ))
    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 = M n n -> M n n
    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 = M n n -> M n n
    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 = M n n -> M n n
    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 (L m k -> Maybe (ℝ, (Int, Int))
    forall (m :: Nat) (n :: Nat).
    (KnownNat m, KnownNat n) =>
    L m n -> Maybe (ℝ, (Int, Int))
    isKonst -> Just (ℝ
    a,(Int
    _,Int
    k))) (L k n -> Maybe (ℝ, (Int, Int))
    forall (m :: Nat) (n :: Nat).
    (KnownNat m, KnownNat n) =>
    L m n -> Maybe (ℝ, (Int, Int))
    isKonst -> Just (ℝ
    b,(Int, Int)
    _)) = ℝ -> L m n
    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
    * Int -> ℝ
    forall a b. (Integral a, Num b) => a -> b
    fromIntegral Int
    k)

    mulR (L m k -> Maybe (ℝ, Vector ℝ, (Int, Int))
    forall (m :: Nat) (n :: Nat).
    (KnownNat m, KnownNat n) =>
    L m n -> Maybe (ℝ, Vector ℝ, (Int, Int))
    isDiag -> Just (ℝ
    0,Vector ℝ
    a,(Int, Int)
    _)) (L k n -> Maybe (ℝ, Vector ℝ, (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)
    _)) = ℝ -> R k -> L m n
    forall (m :: Nat) (n :: Nat) (k :: Nat).
    (KnownNat m, KnownNat n, KnownNat k) =>
    ℝ -> R k -> L m n
    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 (Vector ℝ -> R k
    forall (n :: Nat). Vector ℝ -> R n
    mkR Vector ℝ
    v :: R k)
      where
        v :: Vector ℝ
    v = Vector ℝ
    a' Vector ℝ -> Vector ℝ -> Vector ℝ
    forall a. Num a => a -> a -> a
    * Vector ℝ
    b'
        n :: Int
    n = Int -> Int -> Int
    forall a. Ord a => a -> a -> a
    min (Vector ℝ -> IndexOf Vector
    forall (c :: * -> *) t. Container c t => c t -> IndexOf c
    LA.size Vector ℝ
    a) (Vector ℝ -> IndexOf Vector
    forall (c :: * -> *) t. Container c t => c t -> IndexOf c
    LA.size Vector ℝ
    b)
        a' :: Vector ℝ
    a' = Int -> Int -> Vector ℝ -> Vector ℝ
    forall t. Storable t => Int -> Int -> Vector t -> Vector t
    subVector Int
    0 Int
    n Vector ℝ
    a
        b' :: Vector ℝ
    b' = Int -> Int -> Vector ℝ -> Vector ℝ
    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 = Matrix ℝ -> L m n
    forall (m :: Nat) (n :: Nat). Matrix ℝ -> L m n
    mkL (L m k -> Matrix ℝ
    forall t s (d :: * -> *). Sized t s d => s -> d t
    extract L m k
    a Matrix ℝ -> Matrix ℝ -> Matrix ℝ
    forall t. Numeric t => Matrix t -> Matrix t -> Matrix t
    LA.<> L k n -> Matrix ℝ
    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 (L m n -> Maybe (ℝ, Vector ℝ, (Int, Int))
    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 = Vector ℝ -> R m
    forall (n :: Nat). Vector ℝ -> R n
    mkR (Vector ℝ
    w Vector ℝ -> Vector ℝ -> Vector ℝ
    forall a. Num a => a -> a -> a
    * Int -> Int -> Vector ℝ -> Vector ℝ
    forall t. Storable t => Int -> Int -> Vector t -> Vector t
    subVector Int
    0 (Vector ℝ -> IndexOf Vector
    forall (c :: * -> *) t. Container c t => c t -> IndexOf c
    LA.size Vector ℝ
    w) (R n -> Vector ℝ
    forall t s (d :: * -> *). Sized t s d => s -> d t
    extract R n
    v))
    appR L m n
    m R n
    v = Vector ℝ -> R m
    forall (n :: Nat). Vector ℝ -> R n
    mkR (L m n -> Matrix ℝ
    forall t s (d :: * -> *). Sized t s d => s -> d t
    extract L m n
    m Matrix ℝ -> Vector ℝ -> Vector ℝ
    forall t. Numeric t => Matrix t -> Vector t -> Vector t
    LA.#> R n -> Vector ℝ
    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 (R n -> Vector ℝ
    forall t s (d :: * -> *). Sized t s d => s -> d t
    extract -> Vector ℝ
    u) (R n -> Vector ℝ
    forall t s (d :: * -> *). Sized t s d => s -> d t
    extract -> Vector ℝ
    v) = Vector ℝ -> Vector ℝ -> ℝ
    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 (R 3 -> Vector ℝ
    forall t s (d :: * -> *). Sized t s d => s -> d t
    extract -> Vector ℝ
    x) (R 3 -> Vector ℝ
    forall t s (d :: * -> *). Sized t s d => s -> d t
    extract -> Vector ℝ
    y) = ℝ -> ℝ -> ℝ -> R 3
    vec3 ℝ
    z1 ℝ
    z2 ℝ
    z3
      where
        z1 :: ℝ
    z1 = Vector ℝ
    xVector ℝ -> Int -> ℝ
    forall c t. Indexable c t => c -> Int -> t
    !Int
    1ℝ -> ℝ -> ℝ
    forall a. Num a => a -> a -> a
    *Vector ℝ
    yVector ℝ -> Int -> ℝ
    forall c t. Indexable c t => c -> Int -> t
    !Int
    2ℝ -> ℝ -> ℝ
    forall a. Num a => a -> a -> a
    -Vector ℝ
    xVector ℝ -> Int -> ℝ
    forall c t. Indexable c t => c -> Int -> t
    !Int
    2ℝ -> ℝ -> ℝ
    forall a. Num a => a -> a -> a
    *Vector ℝ
    yVector ℝ -> Int -> ℝ
    forall c t. Indexable c t => c -> Int -> t
    !Int
    1
        z2 :: ℝ
    z2 = Vector ℝ
    xVector ℝ -> Int -> ℝ
    forall c t. Indexable c t => c -> Int -> t
    !Int
    2ℝ -> ℝ -> ℝ
    forall a. Num a => a -> a -> a
    *Vector ℝ
    yVector ℝ -> Int -> ℝ
    forall c t. Indexable c t => c -> Int -> t
    !Int
    0ℝ -> ℝ -> ℝ
    forall a. Num a => a -> a -> a
    -Vector ℝ
    xVector ℝ -> Int -> ℝ
    forall c t. Indexable c t => c -> Int -> t
    !Int
    0ℝ -> ℝ -> ℝ
    forall a. Num a => a -> a -> a
    *Vector ℝ
    yVector ℝ -> Int -> ℝ
    forall c t. Indexable c t => c -> Int -> t
    !Int
    2
        z3 :: ℝ
    z3 = Vector ℝ
    xVector ℝ -> Int -> ℝ
    forall c t. Indexable c t => c -> Int -> t
    !Int
    0ℝ -> ℝ -> ℝ
    forall a. Num a => a -> a -> a
    *Vector ℝ
    yVector ℝ -> Int -> ℝ
    forall c t. Indexable c t => c -> Int -> t
    !Int
    1ℝ -> ℝ -> ℝ
    forall a. Num a => a -> a -> a
    -Vector ℝ
    xVector ℝ -> Int -> ℝ
    forall c t. Indexable c t => c -> Int -> t
    !Int
    1ℝ -> ℝ -> ℝ
    forall a. Num a => a -> a -> a
    *Vector ℝ
    yVector ℝ -> Int -> ℝ
    forall 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 (R n -> Vector ℝ
    forall t s (d :: * -> *). Sized t s d => s -> d t
    extract -> Vector ℝ
    x) (R m -> Vector ℝ
    forall t s (d :: * -> *). Sized t s d => s -> d t
    extract -> Vector ℝ
    y) = Matrix ℝ -> L n m
    forall (m :: Nat) (n :: Nat). Matrix ℝ -> L m n
    mkL (Vector ℝ -> Vector ℝ -> Matrix ℝ
    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 (R n -> Vector ℝ
    forall t s (d :: * -> *). Sized t s d => s -> d t
    unwrap -> Vector ℝ
    v) = Vector ℝ -> R n
    forall (n :: Nat). Vector ℝ -> R n
    mkR ((ℝ -> ℝ) -> Vector ℝ -> Vector ℝ
    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 (R n -> Vector ℝ
    forall t s (d :: * -> *). Sized t s d => s -> d t
    extract -> Vector ℝ
    x) (R n -> Vector ℝ
    forall t s (d :: * -> *). Sized t s d => s -> d t
    extract -> Vector ℝ
    y) = Vector ℝ -> R n
    forall (n :: Nat). Vector ℝ -> R n
    mkR ((ℝ -> ℝ -> ℝ) -> Vector ℝ -> Vector ℝ -> Vector ℝ
    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 = (Matrix ℝ -> Matrix ℝ) -> L n m -> L n m
    forall (m :: Nat) (n :: Nat).
    (KnownNat m, KnownNat n) =>
    (Matrix ℝ -> Matrix ℝ) -> L m n -> L m n
    overMatL' ((ℝ -> ℝ) -> Matrix ℝ -> Matrix ℝ
    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 = Matrix ℝ -> ℝ
    forall t. Field t => Matrix t -> t
    LA.det (Matrix ℝ -> ℝ) -> (Sq n -> Matrix ℝ) -> Sq n -> ℝ
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Sq n -> Matrix ℝ
    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 = (Matrix ℝ -> Sq n) -> (Matrix ℝ, (ℝ, ℝ)) -> (Sq n, (ℝ, ℝ))
    forall a b c. (a -> b) -> (a, c) -> (b, c)
    forall (p :: * -> * -> *) a b c.
    Bifunctor p =>
    (a -> b) -> p a c -> p b c
    BF.first Matrix ℝ -> Sq n
    forall (m :: Nat) (n :: Nat). Matrix ℝ -> L m n
    mkL ((Matrix ℝ, (ℝ, ℝ)) -> (Sq n, (ℝ, ℝ)))
    -> (Sq n -> (Matrix ℝ, (ℝ, ℝ))) -> Sq n -> (Sq n, (ℝ, ℝ))
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Matrix ℝ -> (Matrix ℝ, (ℝ, ℝ))
    forall t. Field t => Matrix t -> (Matrix t, (t, t))
    LA.invlndet (Matrix ℝ -> (Matrix ℝ, (ℝ, ℝ)))
    -> (Sq n -> Matrix ℝ) -> Sq n -> (Matrix ℝ, (ℝ, ℝ))
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Sq n -> Matrix ℝ
    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 = (Matrix ℝ -> Matrix ℝ) -> L n n -> L n n
    forall (m :: Nat) (n :: Nat).
    (KnownNat m, KnownNat n) =>
    (Matrix ℝ -> Matrix ℝ) -> L m n -> L m n
    overMatL' Matrix ℝ -> Matrix ℝ
    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 = (Matrix ℝ -> Matrix ℝ) -> L n n -> L n n
    forall (m :: Nat) (n :: Nat).
    (KnownNat m, KnownNat n) =>
    (Matrix ℝ -> Matrix ℝ) -> L m n -> L m n
    overMatL' Matrix ℝ -> Matrix ℝ
    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 = (Matrix ℝ -> Matrix ℝ) -> L n n -> L n n
    forall (m :: Nat) (n :: Nat).
    (KnownNat m, KnownNat n) =>
    (Matrix ℝ -> Matrix ℝ) -> L m n -> L m n
    overMatL' Matrix ℝ -> Matrix ℝ
    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 (M m k -> Maybe (ℂ, (Int, Int))
    forall (m :: Nat) (n :: Nat).
    (KnownNat m, KnownNat n) =>
    M m n -> Maybe (ℂ, (Int, Int))
    isKonstC -> Just (ℂ
    a,(Int
    _,Int
    k))) (M k n -> Maybe (ℂ, (Int, Int))
    forall (m :: Nat) (n :: Nat).
    (KnownNat m, KnownNat n) =>
    M m n -> Maybe (ℂ, (Int, Int))
    isKonstC -> Just (ℂ
    b,(Int, Int)
    _)) = ℂ -> M m n
    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
    * Int -> ℂ
    forall a b. (Integral a, Num b) => a -> b
    fromIntegral Int
    k)

    mulC (M m k -> Maybe (ℂ, Vector ℂ, (Int, Int))
    forall (m :: Nat) (n :: Nat).
    (KnownNat m, KnownNat n) =>
    M m n -> Maybe (ℂ, Vector ℂ, (Int, Int))
    isDiagC -> Just (ℂ
    0,Vector ℂ
    a,(Int, Int)
    _)) (M k n -> Maybe (ℂ, Vector ℂ, (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)
    _)) = ℂ -> C k -> M m n
    forall (m :: Nat) (n :: Nat) (k :: Nat).
    (KnownNat m, KnownNat n, KnownNat k) =>
    ℂ -> C k -> M m n
    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 (Vector ℂ -> C k
    forall (n :: Nat). Vector ℂ -> C n
    mkC Vector ℂ
    v :: C k)
      where
        v :: Vector ℂ
    v = Vector ℂ
    a' Vector ℂ -> Vector ℂ -> Vector ℂ
    forall a. Num a => a -> a -> a
    * Vector ℂ
    b'
        n :: Int
    n = Int -> Int -> Int
    forall a. Ord a => a -> a -> a
    min (Vector ℂ -> IndexOf Vector
    forall (c :: * -> *) t. Container c t => c t -> IndexOf c
    LA.size Vector ℂ
    a) (Vector ℂ -> IndexOf Vector
    forall (c :: * -> *) t. Container c t => c t -> IndexOf c
    LA.size Vector ℂ
    b)
        a' :: Vector ℂ
    a' = Int -> Int -> Vector ℂ -> Vector ℂ
    forall t. Storable t => Int -> Int -> Vector t -> Vector t
    subVector Int
    0 Int
    n Vector ℂ
    a
        b' :: Vector ℂ
    b' = Int -> Int -> Vector ℂ -> Vector ℂ
    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 = Matrix ℂ -> M m n
    forall (m :: Nat) (n :: Nat). Matrix ℂ -> M m n
    mkM (M m k -> Matrix ℂ
    forall t s (d :: * -> *). Sized t s d => s -> d t
    extract M m k
    a Matrix ℂ -> Matrix ℂ -> Matrix ℂ
    forall t. Numeric t => Matrix t -> Matrix t -> Matrix t
    LA.<> M k n -> Matrix ℂ
    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 (M m n -> Maybe (ℂ, Vector ℂ, (Int, Int))
    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 = Vector ℂ -> C m
    forall (n :: Nat). Vector ℂ -> C n
    mkC (Vector ℂ
    w Vector ℂ -> Vector ℂ -> Vector ℂ
    forall a. Num a => a -> a -> a
    * Int -> Int -> Vector ℂ -> Vector ℂ
    forall t. Storable t => Int -> Int -> Vector t -> Vector t
    subVector Int
    0 (Vector ℂ -> IndexOf Vector
    forall (c :: * -> *) t. Container c t => c t -> IndexOf c
    LA.size Vector ℂ
    w) (C n -> Vector ℂ
    forall t s (d :: * -> *). Sized t s d => s -> d t
    extract C n
    v))
    appC M m n
    m C n
    v = Vector ℂ -> C m
    forall (n :: Nat). Vector ℂ -> C n
    mkC (M m n -> Matrix ℂ
    forall t s (d :: * -> *). Sized t s d => s -> d t
    extract M m n
    m Matrix ℂ -> Vector ℂ -> Vector ℂ
    forall t. Numeric t => Matrix t -> Vector t -> Vector t
    LA.#> C n -> Vector ℂ
    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 (C n -> Vector ℂ
    forall t s (d :: * -> *). Sized t s d => s -> d t
    extract -> Vector ℂ
    u) (C n -> Vector ℂ
    forall t s (d :: * -> *). Sized t s d => s -> d t
    extract -> Vector ℂ
    v) = Vector ℂ -> Vector ℂ -> ℂ
    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 (C 3 -> Vector ℂ
    forall t s (d :: * -> *). Sized t s d => s -> d t
    extract -> Vector ℂ
    x) (C 3 -> Vector ℂ
    forall t s (d :: * -> *). Sized t s d => s -> d t
    extract -> Vector ℂ
    y) = Vector ℂ -> C 3
    forall (n :: Nat). Vector ℂ -> C n
    mkC ([ℂ] -> Vector ℂ
    forall a. Storable a => [a] -> Vector a
    LA.fromList [ℂ
    z1, ℂ
    z2, ℂ
    z3])
      where
        z1 :: ℂ
    z1 = Vector ℂ
    xVector ℂ -> Int -> ℂ
    forall c t. Indexable c t => c -> Int -> t
    !Int
    1ℂ -> ℂ -> ℂ
    forall a. Num a => a -> a -> a
    *Vector ℂ
    yVector ℂ -> Int -> ℂ
    forall c t. Indexable c t => c -> Int -> t
    !Int
    2ℂ -> ℂ -> ℂ
    forall a. Num a => a -> a -> a
    -Vector ℂ
    xVector ℂ -> Int -> ℂ
    forall c t. Indexable c t => c -> Int -> t
    !Int
    2ℂ -> ℂ -> ℂ
    forall a. Num a => a -> a -> a
    *Vector ℂ
    yVector ℂ -> Int -> ℂ
    forall c t. Indexable c t => c -> Int -> t
    !Int
    1
        z2 :: ℂ
    z2 = Vector ℂ
    xVector ℂ -> Int -> ℂ
    forall c t. Indexable c t => c -> Int -> t
    !Int
    2ℂ -> ℂ -> ℂ
    forall a. Num a => a -> a -> a
    *Vector ℂ
    yVector ℂ -> Int -> ℂ
    forall c t. Indexable c t => c -> Int -> t
    !Int
    0ℂ -> ℂ -> ℂ
    forall a. Num a => a -> a -> a
    -Vector ℂ
    xVector ℂ -> Int -> ℂ
    forall c t. Indexable c t => c -> Int -> t
    !Int
    0ℂ -> ℂ -> ℂ
    forall a. Num a => a -> a -> a
    *Vector ℂ
    yVector ℂ -> Int -> ℂ
    forall c t. Indexable c t => c -> Int -> t
    !Int
    2
        z3 :: ℂ
    z3 = Vector ℂ
    xVector ℂ -> Int -> ℂ
    forall c t. Indexable c t => c -> Int -> t
    !Int
    0ℂ -> ℂ -> ℂ
    forall a. Num a => a -> a -> a
    *Vector ℂ
    yVector ℂ -> Int -> ℂ
    forall c t. Indexable c t => c -> Int -> t
    !Int
    1ℂ -> ℂ -> ℂ
    forall a. Num a => a -> a -> a
    -Vector ℂ
    xVector ℂ -> Int -> ℂ
    forall c t. Indexable c t => c -> Int -> t
    !Int
    1ℂ -> ℂ -> ℂ
    forall a. Num a => a -> a -> a
    *Vector ℂ
    yVector ℂ -> Int -> ℂ
    forall 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 (C n -> Vector ℂ
    forall t s (d :: * -> *). Sized t s d => s -> d t
    extract -> Vector ℂ
    x) (C m -> Vector ℂ
    forall t s (d :: * -> *). Sized t s d => s -> d t
    extract -> Vector ℂ
    y) = Matrix ℂ -> M n m
    forall (m :: Nat) (n :: Nat). Matrix ℂ -> M m n
    mkM (Vector ℂ -> Vector ℂ -> Matrix ℂ
    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 (C n -> Vector ℂ
    forall t s (d :: * -> *). Sized t s d => s -> d t
    unwrap -> Vector ℂ
    v) = Vector ℂ -> C n
    forall (n :: Nat). Vector ℂ -> C n
    mkC ((ℂ -> ℂ) -> Vector ℂ -> Vector ℂ
    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 (C n -> Vector ℂ
    forall t s (d :: * -> *). Sized t s d => s -> d t
    extract -> Vector ℂ
    x) (C n -> Vector ℂ
    forall t s (d :: * -> *). Sized t s d => s -> d t
    extract -> Vector ℂ
    y) = Vector ℂ -> C n
    forall (n :: Nat). Vector ℂ -> C n
    mkC ((ℂ -> ℂ -> ℂ) -> Vector ℂ -> Vector ℂ -> Vector ℂ
    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 = (Matrix ℂ -> Matrix ℂ) -> M n m -> M n m
    forall (m :: Nat) (n :: Nat).
    (KnownNat m, KnownNat n) =>
    (Matrix ℂ -> Matrix ℂ) -> M m n -> M m n
    overMatM' ((ℂ -> ℂ) -> Matrix ℂ -> Matrix ℂ
    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 = Matrix ℂ -> ℂ
    forall t. Field t => Matrix t -> t
    LA.det (Matrix ℂ -> ℂ) -> (M n n -> Matrix ℂ) -> M n n -> ℂ
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . M n n -> Matrix ℂ
    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 = (Matrix ℂ -> M n n) -> (Matrix ℂ, (ℂ, ℂ)) -> (M n n, (ℂ, ℂ))
    forall a b c. (a -> b) -> (a, c) -> (b, c)
    forall (p :: * -> * -> *) a b c.
    Bifunctor p =>
    (a -> b) -> p a c -> p b c
    BF.first Matrix ℂ -> M n n
    forall (m :: Nat) (n :: Nat). Matrix ℂ -> M m n
    mkM ((Matrix ℂ, (ℂ, ℂ)) -> (M n n, (ℂ, ℂ)))
    -> (M n n -> (Matrix ℂ, (ℂ, ℂ))) -> M n n -> (M n n, (ℂ, ℂ))
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Matrix ℂ -> (Matrix ℂ, (ℂ, ℂ))
    forall t. Field t => Matrix t -> (Matrix t, (t, t))
    LA.invlndet (Matrix ℂ -> (Matrix ℂ, (ℂ, ℂ)))
    -> (M n n -> Matrix ℂ) -> M n n -> (Matrix ℂ, (ℂ, ℂ))
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . M n n -> Matrix ℂ
    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 = (Matrix ℂ -> Matrix ℂ) -> M n n -> M n n
    forall (m :: Nat) (n :: Nat).
    (KnownNat m, KnownNat n) =>
    (Matrix ℂ -> Matrix ℂ) -> M m n -> M m n
    overMatM' Matrix ℂ -> Matrix ℂ
    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 = (Matrix ℂ -> Matrix ℂ) -> M n n -> M n n
    forall (m :: Nat) (n :: Nat).
    (KnownNat m, KnownNat n) =>
    (Matrix ℂ -> Matrix ℂ) -> M m n -> M m n
    overMatM' Matrix ℂ -> Matrix ℂ
    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 = (Matrix ℂ -> Matrix ℂ) -> M n n -> M n n
    forall (m :: Nat) (n :: Nat).
    (KnownNat m, KnownNat n) =>
    (Matrix ℂ -> Matrix ℂ) -> M m n -> M m n
    overMatM' Matrix ℂ -> Matrix ℂ
    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' Int -> Int -> Bool
    forall a. Eq a => a -> a -> Bool
    == Int
    1 = Matrix ℝ -> L m n
    forall (m :: Nat) (n :: Nat). Matrix ℝ -> L m n
    mkL (ℝ -> Vector ℝ -> Int -> Int -> Matrix ℝ
    forall t. Storable t => t -> Vector t -> Int -> Int -> Matrix t
    LA.diagRect ℝ
    x Vector ℝ
    ev Int
    m' Int
    n')
        | Int
    m'Int -> Int -> Int
    forall a. Num a => a -> a -> a
    *Int
    n' Int -> Int -> Bool
    forall a. Ord a => a -> a -> Bool
    > Int
    0 = L m n
    r
        | Bool
    otherwise = [ℝ] -> L m n
    forall (m :: Nat) (n :: Nat).
    (KnownNat m, KnownNat n) =>
    [ℝ] -> L m n
    matrix []
      where
        r :: L m n
    r = Matrix ℝ -> L m n
    forall (m :: Nat) (n :: Nat). Matrix ℝ -> L m n
    mkL (Vector ℝ -> Matrix ℝ
    forall a. Storable a => Vector a -> Matrix a
    asRow ([Vector ℝ] -> Vector ℝ
    forall t. Storable t => [Vector t] -> Vector t
    vjoin [ℝ -> Vector ℝ
    forall (c :: * -> *) e. Container c e => e -> c e
    scalar ℝ
    x, Vector ℝ
    ev, Vector ℝ
    zeros]))
        ev :: Vector ℝ
    ev = R k -> Vector ℝ
    forall t s (d :: * -> *). Sized t s d => s -> d t
    extract R k
    v
        zeros :: Vector ℝ
    zeros = ℝ -> Int -> Vector ℝ
    forall e d (c :: * -> *). Konst e d c => e -> d -> c e
    LA.konst ℝ
    x (Int -> Int -> Int
    forall a. Ord a => a -> a -> a
    max Int
    0 ((Int -> Int -> Int
    forall a. Ord a => a -> a -> a
    min Int
    m' Int
    n') Int -> Int -> Int
    forall a. Num a => a -> a -> a
    - Vector ℝ -> IndexOf Vector
    forall (c :: * -> *) t. Container c t => c t -> IndexOf c
    LA.size Vector ℝ
    ev))
        (Int
    m',Int
    n') = L m n -> IndexOf Matrix
    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' Int -> Int -> Bool
    forall a. Eq a => a -> a -> Bool
    == Int
    1 = Matrix ℂ -> M m n
    forall (m :: Nat) (n :: Nat). Matrix ℂ -> M m n
    mkM (ℂ -> Vector ℂ -> Int -> Int -> Matrix ℂ
    forall t. Storable t => t -> Vector t -> Int -> Int -> Matrix t
    LA.diagRect ℂ
    x Vector ℂ
    ev Int
    m' Int
    n')
        | Int
    m'Int -> Int -> Int
    forall a. Num a => a -> a -> a
    *Int
    n' Int -> Int -> Bool
    forall a. Ord a => a -> a -> Bool
    > Int
    0 = M m n
    r
        | Bool
    otherwise = [ℂ] -> M m n
    forall t s (d :: * -> *). Sized t s d => [t] -> s
    fromList []
      where
        r :: M m n
    r = Matrix ℂ -> M m n
    forall (m :: Nat) (n :: Nat). Matrix ℂ -> M m n
    mkM (Vector ℂ -> Matrix ℂ
    forall a. Storable a => Vector a -> Matrix a
    asRow ([Vector ℂ] -> Vector ℂ
    forall t. Storable t => [Vector t] -> Vector t
    vjoin [ℂ -> Vector ℂ
    forall (c :: * -> *) e. Container c e => e -> c e
    scalar ℂ
    x, Vector ℂ
    ev, Vector ℂ
    zeros]))
        ev :: Vector ℂ
    ev = C k -> Vector ℂ
    forall t s (d :: * -> *). Sized t s d => s -> d t
    extract C k
    v
        zeros :: Vector ℂ
    zeros = ℂ -> Int -> Vector ℂ
    forall e d (c :: * -> *). Konst e d c => e -> d -> c e
    LA.konst ℂ
    x (Int -> Int -> Int
    forall a. Ord a => a -> a -> a
    max Int
    0 ((Int -> Int -> Int
    forall a. Ord a => a -> a -> a
    min Int
    m' Int
    n') Int -> Int -> Int
    forall a. Num a => a -> a -> a
    - Vector ℂ -> IndexOf Vector
    forall (c :: * -> *) t. Container c t => c t -> IndexOf c
    LA.size Vector ℂ
    ev))
        (Int
    m',Int
    n') = M m n -> IndexOf Matrix
    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 R n -> R n -> ℝ
    forall (n :: Nat). KnownNat n => R n -> R n -> ℝ
    <·> (R n
    1R n -> R n -> R n
    forall a. Fractional a => a -> a -> a
    /R n
    forall (n :: Nat). KnownNat n => R n
    dim)

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

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

        sumV :: R n -> ℝ
    sumV R n
    w = R n
    w R n -> R n -> ℝ
    forall (n :: Nat). KnownNat n => R 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 = [ℝ] -> R 1
    forall (n :: Nat). KnownNat n => [ℝ] -> R n
    vector [ℝ
    x] :: R 1

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

        tm :: GL
        tm :: GL
    tm = ℝ -> [ℝ] -> L m n
    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 = Matrix ℝ -> L m n
    forall (m :: Nat) (n :: Nat). Matrix ℝ -> L m n
    mkL (Matrix ℝ -> L m n) -> ([ℝ] -> Matrix ℝ) -> [ℝ] -> L m n
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Int -> Vector ℝ -> Matrix ℝ
    forall t. Storable t => Int -> Vector t -> Matrix t
    reshape Int
    n' (Vector ℝ -> Matrix ℝ) -> ([ℝ] -> Vector ℝ) -> [ℝ] -> Matrix ℝ
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . [ℝ] -> Vector ℝ
    forall a. Storable a => [a] -> Vector a
    LA.fromList ([ℝ] -> Vector ℝ) -> ([ℝ] -> [ℝ]) -> [ℝ] -> Vector ℝ
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Int -> [ℝ] -> [ℝ]
    forall a. Int -> [a] -> [a]
    take (Int
    m'Int -> Int -> Int
    forall a. Num a => a -> a -> a
    *Int
    n') ([ℝ] -> L m n) -> [ℝ] -> L m n
    forall a b. (a -> b) -> a -> b
    $ [ℝ]
    xs [ℝ] -> [ℝ] -> [ℝ]
    forall a. [a] -> [a] -> [a]
    ++ ℝ -> [ℝ]
    forall a. a -> [a]
    repeat ℝ
    z
            (Int
    m',Int
    n') = L m n -> IndexOf Matrix
    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 = ℝ -> [ℝ] -> L n n
    forall (m :: Nat) (n :: Nat).
    (KnownNat m, KnownNat n) =>
    ℝ -> [ℝ] -> L m n
    lmat ℝ
    0 [ℝ
    1..]

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

        thingD :: ℝ
    thingD = [Vector ℝ] -> Vector ℝ
    forall t. Storable t => [Vector t] -> Vector t
    vjoin [R 2 -> Vector ℝ
    forall (n :: Nat). R n -> Vector ℝ
    ud1 R 2
    u, Vector ℝ
    1] Vector ℝ -> Vector ℝ -> ℝ
    forall t. Numeric t => Vector t -> Vector t -> t
    LA.<.> Matrix ℝ -> Matrix ℝ
    forall m mt. Transposable m mt => m -> mt
    tr Matrix ℝ
    m Matrix ℝ -> Vector ℝ -> Vector ℝ
    forall t. Numeric t => Matrix t -> Vector t -> Vector t
    LA.#> Matrix ℝ
    m Matrix ℝ -> Vector ℝ -> Vector ℝ
    forall t. Numeric t => Matrix t -> Vector t -> Vector t
    LA.#> R 3 -> Vector ℝ
    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) R 3 -> R 3 -> R 3
    forall a. Num a => a -> a -> a
    * (R 2
    u R 2 -> ℝ -> R (2 + 1)
    forall (n :: Nat). KnownNat n => R n -> ℝ -> R (n + 1)
    & ℝ
    6)) R 3 -> R 3 -> ℝ
    forall (n :: Nat). KnownNat n => R n -> R n -> ℝ
    <·> ℝ -> Sq 3
    forall t s (d :: * -> *). Sized t s d => t -> s
    konst ℝ
    2 Sq 3 -> R 3 -> R 3
    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
    * [Vector ℝ] -> Vector ℝ
    forall t. Storable t => [Vector t] -> Vector t
    vjoin[R 2 -> Vector ℝ
    forall (n :: Nat). R n -> Vector ℝ
    ud1 R 2
    u, Vector ℝ
    6] Vector ℝ -> Vector ℝ -> ℝ
    forall t. Numeric t => Vector t -> Vector t -> t
    LA.<.> ℝ -> (Int, Int) -> Matrix ℝ
    forall e d (c :: * -> *). Konst e d c => e -> d -> c e
    LA.konst ℝ
    2 (Vector ℝ -> IndexOf Vector
    forall (c :: * -> *) t. Container c t => c t -> IndexOf c
    LA.size (R 2 -> Vector ℝ
    forall (n :: Nat). R n -> Vector ℝ
    ud1 R 2
    u) Int -> Int -> Int
    forall a. Num a => a -> a -> a
    +Int
    1, Vector ℝ -> IndexOf Vector
    forall (c :: * -> *) t. Container c t => c t -> IndexOf c
    LA.size (R 3 -> Vector ℝ
    forall (n :: Nat). R n -> Vector ℝ
    ud1 R 3
    v)) Matrix ℝ -> Vector ℝ -> Vector ℝ
    forall t. Numeric t => Matrix t -> Vector t -> Vector t
    LA.#> R 3 -> Vector ℝ
    forall (n :: Nat). R n -> Vector ℝ
    ud1 R 3
    v

    splittest :: IO ()
    splittest
        = do
        let v :: R 7
    v = R 7
    forall (n :: Nat). KnownNat n => R n
    range :: R 7
            a :: R 4
    a = (R 3, R 4) -> R 4
    forall a b. (a, b) -> b
    snd (R 7 -> (R 3, R (7 - 3))
    forall (p :: Nat) (n :: Nat).
    (KnownNat p, KnownNat n, p <= n) =>
    R n -> (R p, R (n - p))
    split R 7
    v) :: R 4
        R 4 -> IO ()
    forall a. Show a => a -> IO ()
    print (R 4 -> IO ()) -> R 4 -> IO ()
    forall a b. (a -> b) -> a -> b
    $ R 4
    a
        R (6 - 1) -> IO ()
    forall a. Show a => a -> IO ()
    print (R (6 - 1) -> IO ()) -> R (6 - 1) -> IO ()
    forall a b. (a -> b) -> a -> b
    $ (ℝ, R (6 - 1)) -> R (6 - 1)
    forall a b. (a, b) -> b
    snd ((ℝ, R (6 - 1)) -> R (6 - 1))
    -> (R 7 -> (ℝ, R (6 - 1))) -> R 7 -> R (6 - 1)
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . R 6 -> (ℝ, R (6 - 1))
    forall (n :: Nat). (KnownNat n, 1 <= n) => R n -> (ℝ, R (n - 1))
    headTail (R 6 -> (ℝ, R (6 - 1))) -> (R 7 -> R 6) -> R 7 -> (ℝ, R (6 - 1))
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (ℝ, R 6) -> R 6
    forall a b. (a, b) -> b
    snd ((ℝ, R 6) -> R 6) -> (R 7 -> (ℝ, R 6)) -> R 7 -> R 6
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . R 7 -> (ℝ, R 6)
    R 7 -> (ℝ, R (7 - 1))
    forall (n :: Nat). (KnownNat n, 1 <= n) => R n -> (ℝ, R (n - 1))
    headTail (R 7 -> R (6 - 1)) -> R 7 -> R (6 - 1)
    forall a b. (a -> b) -> a -> b
    $ R 7
    v
        ℝ -> IO ()
    forall a. Show a => a -> IO ()
    print (ℝ -> IO ()) -> ℝ -> IO ()
    forall a b. (a -> b) -> a -> b
    $ R 3 -> ℝ
    forall {n :: Nat}.
    (Assert (OrdCond (CmpNat 1 n) 'True 'True 'False) (TypeError ...),
     KnownNat n) =>
    R n -> ℝ
    first (ℝ -> ℝ -> ℝ -> R 3
    vec3 ℝ
    1 ℝ
    2 ℝ
    3)
        ℝ -> IO ()
    forall a. Show a => a -> IO ()
    print (ℝ -> IO ()) -> ℝ -> IO ()
    forall a b. (a -> b) -> a -> b
    $ R 3 -> ℝ
    forall {n :: Nat}.
    (Assert
       (OrdCond (CmpNat 1 (n - 1)) 'True 'True 'False) (TypeError ...),
     Assert (OrdCond (CmpNat 1 n) 'True 'True 'False) (TypeError ...),
     KnownNat n, KnownNat (n - 1)) =>
    R n -> ℝ
    second (ℝ -> ℝ -> ℝ -> R 3
    vec3 ℝ
    1 ℝ
    2 ℝ
    3)
        ℝ -> IO ()
    forall a. Show a => a -> IO ()
    print (ℝ -> IO ()) -> ℝ -> IO ()
    forall a b. (a -> b) -> a -> b
    $ R 3 -> ℝ
    forall {n :: Nat}.
    (Assert
       (OrdCond (CmpNat 1 ((n - 1) - 1)) 'True 'True 'False)
       (TypeError ...),
     Assert
       (OrdCond (CmpNat 1 (n - 1)) 'True 'True 'False) (TypeError ...),
     Assert (OrdCond (CmpNat 1 n) 'True 'True 'False) (TypeError ...),
     KnownNat n, KnownNat (n - 1), KnownNat ((n - 1) - 1)) =>
    R n -> ℝ
    third (ℝ -> ℝ -> ℝ -> R 3
    vec3 ℝ
    1 ℝ
    2 ℝ
    3)
        L 4 6 -> IO ()
    forall a. Show a => a -> IO ()
    print (L 4 6 -> IO ()) -> L 4 6 -> IO ()
    forall a b. (a -> b) -> a -> b
    $ ((L 2 6, L 4 6) -> L 4 6
    forall a b. (a, b) -> b
    snd ((L 2 6, L 4 6) -> L 4 6) -> (L 2 6, L 4 6) -> L 4 6
    forall a b. (a -> b) -> a -> b
    $ L 6 6 -> (L 2 6, L (6 - 2) 6)
    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 L 6 6
    forall (n :: Nat). KnownNat n => Sq n
    eye :: L 4 6)
     where
        first :: R n -> ℝ
    first R n
    v = (ℝ, R (n - 1)) -> ℝ
    forall a b. (a, b) -> a
    fst ((ℝ, R (n - 1)) -> ℝ) -> (R n -> (ℝ, R (n - 1))) -> R n -> ℝ
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . R n -> (ℝ, R (n - 1))
    forall (n :: Nat). (KnownNat n, 1 <= n) => R n -> (ℝ, R (n - 1))
    headTail (R n -> ℝ) -> R n -> ℝ
    forall a b. (a -> b) -> a -> b
    $ R n
    v
        second :: R n -> ℝ
    second R n
    v = R (n - 1) -> ℝ
    forall {n :: Nat}.
    (Assert (OrdCond (CmpNat 1 n) 'True 'True 'False) (TypeError ...),
     KnownNat n) =>
    R n -> ℝ
    first (R (n - 1) -> ℝ) -> (R n -> R (n - 1)) -> R n -> ℝ
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (ℝ, R (n - 1)) -> R (n - 1)
    forall a b. (a, b) -> b
    snd ((ℝ, R (n - 1)) -> R (n - 1))
    -> (R n -> (ℝ, R (n - 1))) -> R n -> R (n - 1)
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . R n -> (ℝ, R (n - 1))
    forall (n :: Nat). (KnownNat n, 1 <= n) => R n -> (ℝ, R (n - 1))
    headTail (R n -> ℝ) -> R n -> ℝ
    forall a b. (a -> b) -> a -> b
    $ R n
    v
        third :: R n -> ℝ
    third R n
    v = R ((n - 1) - 1) -> ℝ
    forall {n :: Nat}.
    (Assert (OrdCond (CmpNat 1 n) 'True 'True 'False) (TypeError ...),
     KnownNat n) =>
    R n -> ℝ
    first (R ((n - 1) - 1) -> ℝ) -> (R n -> R ((n - 1) - 1)) -> R n -> ℝ
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (ℝ, R ((n - 1) - 1)) -> R ((n - 1) - 1)
    forall a b. (a, b) -> b
    snd ((ℝ, R ((n - 1) - 1)) -> R ((n - 1) - 1))
    -> (R n -> (ℝ, R ((n - 1) - 1))) -> R n -> R ((n - 1) - 1)
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . R (n - 1) -> (ℝ, R ((n - 1) - 1))
    forall (n :: Nat). (KnownNat n, 1 <= n) => R n -> (ℝ, R (n - 1))
    headTail (R (n - 1) -> (ℝ, R ((n - 1) - 1)))
    -> (R n -> R (n - 1)) -> R n -> (ℝ, R ((n - 1) - 1))
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (ℝ, R (n - 1)) -> R (n - 1)
    forall a b. (a, b) -> b
    snd ((ℝ, R (n - 1)) -> R (n - 1))
    -> (R n -> (ℝ, R (n - 1))) -> R n -> R (n - 1)
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . R n -> (ℝ, R (n - 1))
    forall (n :: Nat). (KnownNat n, 1 <= n) => R n -> (ℝ, R (n - 1))
    headTail (R n -> ℝ) -> R n -> ℝ
    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 = Vector ℝ -> ℝ
    forall a. Normed a => a -> ℝ
    norm_0 (R n -> Vector ℝ
    forall t s (d :: * -> *). Sized t s d => s -> d t
    extract R n
    v)
        norm_1 :: R n -> ℝ
    norm_1 R n
    v = Vector ℝ -> ℝ
    forall a. Normed a => a -> ℝ
    norm_1 (R n -> Vector ℝ
    forall t s (d :: * -> *). Sized t s d => s -> d t
    extract R n
    v)
        norm_2 :: R n -> ℝ
    norm_2 R n
    v = Vector ℝ -> ℝ
    forall a. Normed a => a -> ℝ
    norm_2 (R n -> Vector ℝ
    forall t s (d :: * -> *). Sized t s d => s -> d t
    extract R n
    v)
        norm_Inf :: R n -> ℝ
    norm_Inf R n
    v = Vector ℝ -> ℝ
    forall a. Normed a => a -> ℝ
    norm_Inf (R n -> Vector ℝ
    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 = Matrix ℝ -> ℝ
    forall a. Normed a => a -> ℝ
    norm_0 (L m n -> Matrix ℝ
    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 = Matrix ℝ -> ℝ
    forall a. Normed a => a -> ℝ
    norm_1 (L m n -> Matrix ℝ
    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 = Matrix ℝ -> ℝ
    forall a. Normed a => a -> ℝ
    norm_2 (L m n -> Matrix ℝ
    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 = Matrix ℝ -> ℝ
    forall a. Normed a => a -> ℝ
    norm_Inf (L m n -> Matrix ℝ
    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 = Sq n -> Sym n
    forall (n :: Nat). Sq n -> Sym n
    Sym (Sq n -> Sym n) -> (Sym n -> Sq n) -> Sym n -> Sym n
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Sq n -> Sq n
    f (Sq n -> Sq n) -> (Sym n -> Sq n) -> Sym n -> Sq n
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Sym n -> Sq n
    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 = Sq n -> Sym n
    forall (n :: Nat). Sq n -> Sym n
    Sym (Sq n -> Sq n -> Sq n
    f (Sym n -> Sq n
    forall (n :: Nat). Sym n -> Sq n
    unSym Sym n
    x) (Sym n -> Sq n
    forall (n :: Nat). Sym n -> Sq n
    unSym Sym n
    y))

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

    instance KnownNat n => Fractional (Sym n)
      where
        fromRational :: Rational -> Sym n
    fromRational = Sq n -> Sym n
    forall (n :: Nat). Sq n -> Sym n
    Sym (Sq n -> Sym n) -> (Rational -> Sq n) -> Rational -> Sym n
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Rational -> Sq n
    forall a. Fractional a => Rational -> a
    fromRational
        / :: Sym n -> Sym n -> Sym n
    (/) = (Sq n -> Sq n -> Sq n) -> 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 Sq n -> Sq n -> Sq n
    forall a. Fractional a => a -> a -> a
    (/)

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

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

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

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