{-# LANGUAGE DataKinds #-}
{-# LANGUAGE DeriveFoldable #-}
{-# LANGUAGE DeriveFunctor #-}
{-# LANGUAGE DeriveTraversable #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE PatternSynonyms #-}
{-# LANGUAGE RoleAnnotations #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE ViewPatterns #-}

-- SPDX-License-Identifier: MPL-2.0

{- | Runtime-checked shapes and nominal type-indexed matrices/tensors. Shape
witnesses never coerce arbitrary dimensions. Conversion checks occur at the
dynamic/static boundary; multiplication then requires matching types.
-}
module HMath.API.Shape (
    Shape,
    shapeDimensions,
    shapeElements,
    makeShape,
    pattern ScalarShape,
    pattern VectorShape,
    pattern MatrixShape,
    StaticMatrix,
    staticMatrix,
    dynamicMatrix,
    staticMultiply,
    staticTranspose,
    KnownShape (..),
    StaticTensor,
    staticTensor,
    dynamicTensor,
    Coordinates,
    coordinates,
    coordinateValues,
    coordinatesToVector,
) where

import Data.Proxy (Proxy (..))
import GHC.TypeLits (KnownNat, Nat, natVal)
import HMath.Error
import qualified HMath.Matrix as M
import qualified HMath.Tensor as T
import qualified HMath.Vector as V

-- | Scalars have shape [] and one element. Zero axes are allowed.
data Shape = Shape ![Int] !Int deriving (Shape -> Shape -> Bool
(Shape -> Shape -> Bool) -> (Shape -> Shape -> Bool) -> Eq Shape
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: Shape -> Shape -> Bool
== :: Shape -> Shape -> Bool
$c/= :: Shape -> Shape -> Bool
/= :: Shape -> Shape -> Bool
Eq, Eq Shape
Eq Shape =>
(Shape -> Shape -> Ordering)
-> (Shape -> Shape -> Bool)
-> (Shape -> Shape -> Bool)
-> (Shape -> Shape -> Bool)
-> (Shape -> Shape -> Bool)
-> (Shape -> Shape -> Shape)
-> (Shape -> Shape -> Shape)
-> Ord Shape
Shape -> Shape -> Bool
Shape -> Shape -> Ordering
Shape -> Shape -> Shape
forall a.
Eq a =>
(a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
$ccompare :: Shape -> Shape -> Ordering
compare :: Shape -> Shape -> Ordering
$c< :: Shape -> Shape -> Bool
< :: Shape -> Shape -> Bool
$c<= :: Shape -> Shape -> Bool
<= :: Shape -> Shape -> Bool
$c> :: Shape -> Shape -> Bool
> :: Shape -> Shape -> Bool
$c>= :: Shape -> Shape -> Bool
>= :: Shape -> Shape -> Bool
$cmax :: Shape -> Shape -> Shape
max :: Shape -> Shape -> Shape
$cmin :: Shape -> Shape -> Shape
min :: Shape -> Shape -> Shape
Ord, Int -> Shape -> ShowS
[Shape] -> ShowS
Shape -> String
(Int -> Shape -> ShowS)
-> (Shape -> String) -> ([Shape] -> ShowS) -> Show Shape
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> Shape -> ShowS
showsPrec :: Int -> Shape -> ShowS
$cshow :: Shape -> String
show :: Shape -> String
$cshowList :: [Shape] -> ShowS
showList :: [Shape] -> ShowS
Show)

{- | Return runtime dimensions in axis order. Scalars have []; zero-length axes are
retained.
-}
shapeDimensions :: Shape -> [Int]
shapeDimensions :: Shape -> [Int]
shapeDimensions (Shape [Int]
ds Int
_) = [Int]
ds

{- | Return the validated shape product, including one for scalar [] and zero when an axis
is zero.
-}
shapeElements :: Shape -> Int
shapeElements :: Shape -> Int
shapeElements (Shape [Int]
_ Int
n) = Int
n

{- | Validate nonnegative dimensions and an Int-representable element product, returning an
immutable shape witness. Invalid dimensions/overflow return Left MathError. Example:
shapeElements \<$> makeShape [2,3] == Right 6.
-}
makeShape :: [Int] -> Either MathError Shape
makeShape :: [Int] -> Either MathError Shape
makeShape [Int]
ds = [Int] -> Int -> Shape
Shape [Int]
ds (Int -> Shape) -> Either MathError Int -> Either MathError Shape
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Int] -> Either MathError Int
T.shapeSize [Int]
ds

-- | Read-only views: construction always uses makeShape.
pattern ScalarShape :: Shape
pattern $mScalarShape :: forall {r}. Shape -> ((# #) -> r) -> ((# #) -> r) -> r
ScalarShape <- (shapeDimensions -> [])

pattern VectorShape :: Int -> Shape
pattern $mVectorShape :: forall {r}. Shape -> (Int -> r) -> ((# #) -> r) -> r
VectorShape n <- (shapeDimensions -> [n])
pattern MatrixShape :: Int -> Int -> Shape
pattern $mMatrixShape :: forall {r}. Shape -> (Int -> Int -> r) -> ((# #) -> r) -> r
MatrixShape m n <- (shapeDimensions -> [m, n])

{- | Nominal type-indexed matrix dimensions,validated by staticMatrix. Compatible
multiplication is expressed by shared type indices.
-}
newtype StaticMatrix (m :: Nat) (n :: Nat) a = StaticMatrix (M.Matrix a) deriving (StaticMatrix m n a -> StaticMatrix m n a -> Bool
(StaticMatrix m n a -> StaticMatrix m n a -> Bool)
-> (StaticMatrix m n a -> StaticMatrix m n a -> Bool)
-> Eq (StaticMatrix m n a)
forall (m :: Nat) (n :: Nat) a.
Eq a =>
StaticMatrix m n a -> StaticMatrix m n a -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: forall (m :: Nat) (n :: Nat) a.
Eq a =>
StaticMatrix m n a -> StaticMatrix m n a -> Bool
== :: StaticMatrix m n a -> StaticMatrix m n a -> Bool
$c/= :: forall (m :: Nat) (n :: Nat) a.
Eq a =>
StaticMatrix m n a -> StaticMatrix m n a -> Bool
/= :: StaticMatrix m n a -> StaticMatrix m n a -> Bool
Eq, Int -> StaticMatrix m n a -> ShowS
[StaticMatrix m n a] -> ShowS
StaticMatrix m n a -> String
(Int -> StaticMatrix m n a -> ShowS)
-> (StaticMatrix m n a -> String)
-> ([StaticMatrix m n a] -> ShowS)
-> Show (StaticMatrix m n a)
forall (m :: Nat) (n :: Nat) a.
Show a =>
Int -> StaticMatrix m n a -> ShowS
forall (m :: Nat) (n :: Nat) a.
Show a =>
[StaticMatrix m n a] -> ShowS
forall (m :: Nat) (n :: Nat) a.
Show a =>
StaticMatrix m n a -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: forall (m :: Nat) (n :: Nat) a.
Show a =>
Int -> StaticMatrix m n a -> ShowS
showsPrec :: Int -> StaticMatrix m n a -> ShowS
$cshow :: forall (m :: Nat) (n :: Nat) a.
Show a =>
StaticMatrix m n a -> String
show :: StaticMatrix m n a -> String
$cshowList :: forall (m :: Nat) (n :: Nat) a.
Show a =>
[StaticMatrix m n a] -> ShowS
showList :: [StaticMatrix m n a] -> ShowS
Show)

type role StaticMatrix nominal nominal representational

{- | Given a dynamic matrix, compare its dimensions against type-level m and n, returning a
nominally indexed witness. Reject type-level Int overflow or runtime mismatch.
-}
staticMatrix ::
    forall m n a. (KnownNat m, KnownNat n) => M.Matrix a -> Either MathError (StaticMatrix m n a)
staticMatrix :: forall (m :: Nat) (n :: Nat) a.
(KnownNat m, KnownNat n) =>
Matrix a -> Either MathError (StaticMatrix m n a)
staticMatrix Matrix a
a = do
    r <- Proxy m -> Either MathError Int
forall (n :: Nat). KnownNat n => Proxy n -> Either MathError Int
natInt (Proxy m
forall {k} (t :: k). Proxy t
Proxy :: Proxy m)
    c <- natInt (Proxy :: Proxy n)
    if M.shape a == (r, c) then Right (StaticMatrix a) else Left (ShapeMismatch (r, c) (M.shape a))

{- | Forget the nominal type-level dimensions of a StaticMatrix, returning the same
immutable dynamic matrix without changing its values.
-}
dynamicMatrix :: StaticMatrix m n a -> M.Matrix a
dynamicMatrix :: forall (m :: Nat) (n :: Nat) a. StaticMatrix m n a -> Matrix a
dynamicMatrix (StaticMatrix Matrix a
a) = Matrix a
a

{- | Multiply statically compatible m-by-k and k-by-n matrices. Return an m-by-n witness;
checked dynamic size errors can still return Left MathError. Num arithmetic follows the
element instance.
-}
staticMultiply ::
    (Num a) => StaticMatrix m k a -> StaticMatrix k n a -> Either MathError (StaticMatrix m n a)
staticMultiply :: forall a (m :: Nat) (k :: Nat) (n :: Nat).
Num a =>
StaticMatrix m k a
-> StaticMatrix k n a -> Either MathError (StaticMatrix m n a)
staticMultiply (StaticMatrix Matrix a
a) (StaticMatrix Matrix a
b) = Matrix a -> StaticMatrix m n a
forall (m :: Nat) (n :: Nat) a. Matrix a -> StaticMatrix m n a
StaticMatrix (Matrix a -> StaticMatrix m n a)
-> Either MathError (Matrix a)
-> Either MathError (StaticMatrix m n a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Matrix a -> Matrix a -> Either MathError (Matrix a)
forall a.
Num a =>
Matrix a -> Matrix a -> Either MathError (Matrix a)
M.multiplyChecked Matrix a
a Matrix a
b

{- | Transpose a StaticMatrix m n to StaticMatrix n m, preserving values with axes
exchanged.
-}
staticTranspose :: StaticMatrix m n a -> StaticMatrix n m a
staticTranspose :: forall (m :: Nat) (n :: Nat) a.
StaticMatrix m n a -> StaticMatrix n m a
staticTranspose (StaticMatrix Matrix a
a) = Matrix a -> StaticMatrix n m a
forall (m :: Nat) (n :: Nat) a. Matrix a -> StaticMatrix m n a
StaticMatrix (Matrix a -> Matrix a
forall a. Matrix a -> Matrix a
M.transposeMatrix Matrix a
a)

instance Functor (StaticMatrix m n) where
    fmap :: forall a b. (a -> b) -> StaticMatrix m n a -> StaticMatrix m n b
fmap a -> b
f (StaticMatrix Matrix a
a) =
        Matrix b -> StaticMatrix m n b
forall (m :: Nat) (n :: Nat) a. Matrix a -> StaticMatrix m n a
StaticMatrix ((MathError -> Matrix b)
-> (Matrix b -> Matrix b)
-> Either MathError (Matrix b)
-> Matrix b
forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either (String -> Matrix b
forall a. HasCallStack => String -> a
error (String -> Matrix b)
-> (MathError -> String) -> MathError -> Matrix b
forall b c a. (b -> c) -> (a -> b) -> a -> c
. MathError -> String
forall a. Show a => a -> String
show) Matrix b -> Matrix b
forall a. a -> a
id ((Int -> Int -> [b] -> Either MathError (Matrix b))
-> (Int, Int) -> [b] -> Either MathError (Matrix b)
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry Int -> Int -> [b] -> Either MathError (Matrix b)
forall a. Int -> Int -> [a] -> Either MathError (Matrix a)
M.fromListChecked (Matrix a -> (Int, Int)
forall a. Matrix a -> (Int, Int)
M.shape Matrix a
a) ((a -> b) -> [a] -> [b]
forall a b. (a -> b) -> [a] -> [b]
map a -> b
f (Matrix a -> [a]
forall a. Matrix a -> [a]
M.toList Matrix a
a))))
instance Foldable (StaticMatrix m n) where foldMap :: forall m a. Monoid m => (a -> m) -> StaticMatrix m n a -> m
foldMap a -> m
f = (a -> m) -> [a] -> m
forall m a. Monoid m => (a -> m) -> [a] -> m
forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap a -> m
f ([a] -> m)
-> (StaticMatrix m n a -> [a]) -> StaticMatrix m n a -> m
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Matrix a -> [a]
forall a. Matrix a -> [a]
M.toList (Matrix a -> [a])
-> (StaticMatrix m n a -> Matrix a) -> StaticMatrix m n a -> [a]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. StaticMatrix m n a -> Matrix a
forall (m :: Nat) (n :: Nat) a. StaticMatrix m n a -> Matrix a
dynamicMatrix
instance Traversable (StaticMatrix m n) where
    traverse :: forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> StaticMatrix m n a -> f (StaticMatrix m n b)
traverse a -> f b
f (StaticMatrix Matrix a
a) =
        (\[b]
xs -> Matrix b -> StaticMatrix m n b
forall (m :: Nat) (n :: Nat) a. Matrix a -> StaticMatrix m n a
StaticMatrix ((MathError -> Matrix b)
-> (Matrix b -> Matrix b)
-> Either MathError (Matrix b)
-> Matrix b
forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either (String -> Matrix b
forall a. HasCallStack => String -> a
error (String -> Matrix b)
-> (MathError -> String) -> MathError -> Matrix b
forall b c a. (b -> c) -> (a -> b) -> a -> c
. MathError -> String
forall a. Show a => a -> String
show) Matrix b -> Matrix b
forall a. a -> a
id ((Int -> Int -> [b] -> Either MathError (Matrix b))
-> (Int, Int) -> [b] -> Either MathError (Matrix b)
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry Int -> Int -> [b] -> Either MathError (Matrix b)
forall a. Int -> Int -> [a] -> Either MathError (Matrix a)
M.fromListChecked (Matrix a -> (Int, Int)
forall a. Matrix a -> (Int, Int)
M.shape Matrix a
a) [b]
xs)))
            ([b] -> StaticMatrix m n b) -> f [b] -> f (StaticMatrix m n b)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (a -> f b) -> [a] -> f [b]
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> [a] -> f [b]
traverse a -> f b
f (Matrix a -> [a]
forall a. Matrix a -> [a]
M.toList Matrix a
a)

-- | Type-level list of natural dimensions, reflected without Int truncation.
class KnownShape (ds :: [Nat]) where
    {- | Given a type-level shape proxy, reflect exact Integer dimensions
    without truncation to Int.
    -}
    reflectedShape :: proxy ds -> [Integer]

instance KnownShape '[] where reflectedShape :: forall (proxy :: [Nat] -> *). proxy '[] -> [Integer]
reflectedShape proxy '[]
_ = []
instance (KnownNat n, KnownShape ns) => KnownShape (n ': ns) where
    reflectedShape :: forall (proxy :: [Nat] -> *). proxy (n : ns) -> [Integer]
reflectedShape proxy (n : ns)
_ = Integer -> Integer
forall a. Integral a => a -> Integer
toInteger (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)) Integer -> [Integer] -> [Integer]
forall a. a -> [a] -> [a]
: Proxy ns -> [Integer]
forall (ds :: [Nat]) (proxy :: [Nat] -> *).
KnownShape ds =>
proxy ds -> [Integer]
forall (proxy :: [Nat] -> *). proxy ns -> [Integer]
reflectedShape (Proxy ns
forall {k} (t :: k). Proxy t
Proxy :: Proxy ns)

{- | Nominal type-indexed tensor shape,validated against reflected runtime dimensions by
staticTensor.
-}
newtype StaticTensor (ds :: [Nat]) a = StaticTensor (T.Tensor a) deriving (StaticTensor ds a -> StaticTensor ds a -> Bool
(StaticTensor ds a -> StaticTensor ds a -> Bool)
-> (StaticTensor ds a -> StaticTensor ds a -> Bool)
-> Eq (StaticTensor ds a)
forall (ds :: [Nat]) a.
Eq a =>
StaticTensor ds a -> StaticTensor ds a -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: forall (ds :: [Nat]) a.
Eq a =>
StaticTensor ds a -> StaticTensor ds a -> Bool
== :: StaticTensor ds a -> StaticTensor ds a -> Bool
$c/= :: forall (ds :: [Nat]) a.
Eq a =>
StaticTensor ds a -> StaticTensor ds a -> Bool
/= :: StaticTensor ds a -> StaticTensor ds a -> Bool
Eq, Int -> StaticTensor ds a -> ShowS
[StaticTensor ds a] -> ShowS
StaticTensor ds a -> String
(Int -> StaticTensor ds a -> ShowS)
-> (StaticTensor ds a -> String)
-> ([StaticTensor ds a] -> ShowS)
-> Show (StaticTensor ds a)
forall (ds :: [Nat]) a. Show a => Int -> StaticTensor ds a -> ShowS
forall (ds :: [Nat]) a. Show a => [StaticTensor ds a] -> ShowS
forall (ds :: [Nat]) a. Show a => StaticTensor ds a -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: forall (ds :: [Nat]) a. Show a => Int -> StaticTensor ds a -> ShowS
showsPrec :: Int -> StaticTensor ds a -> ShowS
$cshow :: forall (ds :: [Nat]) a. Show a => StaticTensor ds a -> String
show :: StaticTensor ds a -> String
$cshowList :: forall (ds :: [Nat]) a. Show a => [StaticTensor ds a] -> ShowS
showList :: [StaticTensor ds a] -> ShowS
Show)

type role StaticTensor nominal representational

{- | Given dynamic tensor and type-level shape ds, return a nominal witness only if runtime
dimensions match reflectedShape exactly. A mismatch returns Left InvalidArgument.
-}
staticTensor :: forall ds a. (KnownShape ds) => T.Tensor a -> Either MathError (StaticTensor ds a)
staticTensor :: forall (ds :: [Nat]) a.
KnownShape ds =>
Tensor a -> Either MathError (StaticTensor ds a)
staticTensor Tensor a
t
    | (Int -> Integer) -> [Int] -> [Integer]
forall a b. (a -> b) -> [a] -> [b]
map Int -> Integer
forall a. Integral a => a -> Integer
toInteger (Tensor a -> [Int]
forall a. Tensor a -> [Int]
T.tensorShape Tensor a
t) [Integer] -> [Integer] -> Bool
forall a. Eq a => a -> a -> Bool
== Proxy ds -> [Integer]
forall (ds :: [Nat]) (proxy :: [Nat] -> *).
KnownShape ds =>
proxy ds -> [Integer]
forall (proxy :: [Nat] -> *). proxy ds -> [Integer]
reflectedShape (Proxy ds
forall {k} (t :: k). Proxy t
Proxy :: Proxy ds) = StaticTensor ds a -> Either MathError (StaticTensor ds a)
forall a b. b -> Either a b
Right (Tensor a -> StaticTensor ds a
forall (ds :: [Nat]) a. Tensor a -> StaticTensor ds a
StaticTensor Tensor a
t)
    | Bool
otherwise = MathError -> Either MathError (StaticTensor ds a)
forall a b. a -> Either a b
Left (String -> MathError
InvalidArgument String
"staticTensor: type-level shape differs from runtime shape")

{- | Forget a StaticTensor shape witness, returning its underlying immutable dynamic tensor
without numerical conversion.
-}
dynamicTensor :: StaticTensor ds a -> T.Tensor a
dynamicTensor :: forall (ds :: [Nat]) a. StaticTensor ds a -> Tensor a
dynamicTensor (StaticTensor Tensor a
t) = Tensor a
t

{- | Fixed-length coordinates with lawful zip Applicative. Elements are lazy;
pure/fmap/traverse preserve length. Type-level lengths can exceed Int; the
conversion to ordinary vectors rejects such lengths before traversing data.
-}
newtype Coordinates (n :: Nat) a = Coordinates [a]
    deriving (Coordinates n a -> Coordinates n a -> Bool
(Coordinates n a -> Coordinates n a -> Bool)
-> (Coordinates n a -> Coordinates n a -> Bool)
-> Eq (Coordinates n a)
forall (n :: Nat) a.
Eq a =>
Coordinates n a -> Coordinates n a -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: forall (n :: Nat) a.
Eq a =>
Coordinates n a -> Coordinates n a -> Bool
== :: Coordinates n a -> Coordinates n a -> Bool
$c/= :: forall (n :: Nat) a.
Eq a =>
Coordinates n a -> Coordinates n a -> Bool
/= :: Coordinates n a -> Coordinates n a -> Bool
Eq, Int -> Coordinates n a -> ShowS
[Coordinates n a] -> ShowS
Coordinates n a -> String
(Int -> Coordinates n a -> ShowS)
-> (Coordinates n a -> String)
-> ([Coordinates n a] -> ShowS)
-> Show (Coordinates n a)
forall (n :: Nat) a. Show a => Int -> Coordinates n a -> ShowS
forall (n :: Nat) a. Show a => [Coordinates n a] -> ShowS
forall (n :: Nat) a. Show a => Coordinates n a -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: forall (n :: Nat) a. Show a => Int -> Coordinates n a -> ShowS
showsPrec :: Int -> Coordinates n a -> ShowS
$cshow :: forall (n :: Nat) a. Show a => Coordinates n a -> String
show :: Coordinates n a -> String
$cshowList :: forall (n :: Nat) a. Show a => [Coordinates n a] -> ShowS
showList :: [Coordinates n a] -> ShowS
Show, (forall a b. (a -> b) -> Coordinates n a -> Coordinates n b)
-> (forall a b. a -> Coordinates n b -> Coordinates n a)
-> Functor (Coordinates n)
forall (n :: Nat) a b. a -> Coordinates n b -> Coordinates n a
forall (n :: Nat) a b.
(a -> b) -> Coordinates n a -> Coordinates n b
forall a b. a -> Coordinates n b -> Coordinates n a
forall a b. (a -> b) -> Coordinates n a -> Coordinates n b
forall (f :: * -> *).
(forall a b. (a -> b) -> f a -> f b)
-> (forall a b. a -> f b -> f a) -> Functor f
$cfmap :: forall (n :: Nat) a b.
(a -> b) -> Coordinates n a -> Coordinates n b
fmap :: forall a b. (a -> b) -> Coordinates n a -> Coordinates n b
$c<$ :: forall (n :: Nat) a b. a -> Coordinates n b -> Coordinates n a
<$ :: forall a b. a -> Coordinates n b -> Coordinates n a
Functor, (forall m. Monoid m => Coordinates n m -> m)
-> (forall m a. Monoid m => (a -> m) -> Coordinates n a -> m)
-> (forall m a. Monoid m => (a -> m) -> Coordinates n a -> m)
-> (forall a b. (a -> b -> b) -> b -> Coordinates n a -> b)
-> (forall a b. (a -> b -> b) -> b -> Coordinates n a -> b)
-> (forall b a. (b -> a -> b) -> b -> Coordinates n a -> b)
-> (forall b a. (b -> a -> b) -> b -> Coordinates n a -> b)
-> (forall a. (a -> a -> a) -> Coordinates n a -> a)
-> (forall a. (a -> a -> a) -> Coordinates n a -> a)
-> (forall a. Coordinates n a -> [a])
-> (forall a. Coordinates n a -> Bool)
-> (forall a. Coordinates n a -> Int)
-> (forall a. Eq a => a -> Coordinates n a -> Bool)
-> (forall a. Ord a => Coordinates n a -> a)
-> (forall a. Ord a => Coordinates n a -> a)
-> (forall a. Num a => Coordinates n a -> a)
-> (forall a. Num a => Coordinates n a -> a)
-> Foldable (Coordinates n)
forall (n :: Nat) a. Eq a => a -> Coordinates n a -> Bool
forall (n :: Nat) a. Num a => Coordinates n a -> a
forall (n :: Nat) a. Ord a => Coordinates n a -> a
forall (n :: Nat) m. Monoid m => Coordinates n m -> m
forall (n :: Nat) a. Coordinates n a -> Bool
forall (n :: Nat) a. Coordinates n a -> Int
forall (n :: Nat) a. Coordinates n a -> [a]
forall (n :: Nat) a. (a -> a -> a) -> Coordinates n a -> a
forall (n :: Nat) m a. Monoid m => (a -> m) -> Coordinates n a -> m
forall (n :: Nat) b a. (b -> a -> b) -> b -> Coordinates n a -> b
forall (n :: Nat) a b. (a -> b -> b) -> b -> Coordinates n a -> b
forall a. Eq a => a -> Coordinates n a -> Bool
forall a. Num a => Coordinates n a -> a
forall a. Ord a => Coordinates n a -> a
forall m. Monoid m => Coordinates n m -> m
forall a. Coordinates n a -> Bool
forall a. Coordinates n a -> Int
forall a. Coordinates n a -> [a]
forall a. (a -> a -> a) -> Coordinates n a -> a
forall m a. Monoid m => (a -> m) -> Coordinates n a -> m
forall b a. (b -> a -> b) -> b -> Coordinates n a -> b
forall a b. (a -> b -> b) -> b -> Coordinates n a -> b
forall (t :: * -> *).
(forall m. Monoid m => t m -> m)
-> (forall m a. Monoid m => (a -> m) -> t a -> m)
-> (forall m a. Monoid m => (a -> m) -> t a -> m)
-> (forall a b. (a -> b -> b) -> b -> t a -> b)
-> (forall a b. (a -> b -> b) -> b -> t a -> b)
-> (forall b a. (b -> a -> b) -> b -> t a -> b)
-> (forall b a. (b -> a -> b) -> b -> t a -> b)
-> (forall a. (a -> a -> a) -> t a -> a)
-> (forall a. (a -> a -> a) -> t a -> a)
-> (forall a. t a -> [a])
-> (forall a. t a -> Bool)
-> (forall a. t a -> Int)
-> (forall a. Eq a => a -> t a -> Bool)
-> (forall a. Ord a => t a -> a)
-> (forall a. Ord a => t a -> a)
-> (forall a. Num a => t a -> a)
-> (forall a. Num a => t a -> a)
-> Foldable t
$cfold :: forall (n :: Nat) m. Monoid m => Coordinates n m -> m
fold :: forall m. Monoid m => Coordinates n m -> m
$cfoldMap :: forall (n :: Nat) m a. Monoid m => (a -> m) -> Coordinates n a -> m
foldMap :: forall m a. Monoid m => (a -> m) -> Coordinates n a -> m
$cfoldMap' :: forall (n :: Nat) m a. Monoid m => (a -> m) -> Coordinates n a -> m
foldMap' :: forall m a. Monoid m => (a -> m) -> Coordinates n a -> m
$cfoldr :: forall (n :: Nat) a b. (a -> b -> b) -> b -> Coordinates n a -> b
foldr :: forall a b. (a -> b -> b) -> b -> Coordinates n a -> b
$cfoldr' :: forall (n :: Nat) a b. (a -> b -> b) -> b -> Coordinates n a -> b
foldr' :: forall a b. (a -> b -> b) -> b -> Coordinates n a -> b
$cfoldl :: forall (n :: Nat) b a. (b -> a -> b) -> b -> Coordinates n a -> b
foldl :: forall b a. (b -> a -> b) -> b -> Coordinates n a -> b
$cfoldl' :: forall (n :: Nat) b a. (b -> a -> b) -> b -> Coordinates n a -> b
foldl' :: forall b a. (b -> a -> b) -> b -> Coordinates n a -> b
$cfoldr1 :: forall (n :: Nat) a. (a -> a -> a) -> Coordinates n a -> a
foldr1 :: forall a. (a -> a -> a) -> Coordinates n a -> a
$cfoldl1 :: forall (n :: Nat) a. (a -> a -> a) -> Coordinates n a -> a
foldl1 :: forall a. (a -> a -> a) -> Coordinates n a -> a
$ctoList :: forall (n :: Nat) a. Coordinates n a -> [a]
toList :: forall a. Coordinates n a -> [a]
$cnull :: forall (n :: Nat) a. Coordinates n a -> Bool
null :: forall a. Coordinates n a -> Bool
$clength :: forall (n :: Nat) a. Coordinates n a -> Int
length :: forall a. Coordinates n a -> Int
$celem :: forall (n :: Nat) a. Eq a => a -> Coordinates n a -> Bool
elem :: forall a. Eq a => a -> Coordinates n a -> Bool
$cmaximum :: forall (n :: Nat) a. Ord a => Coordinates n a -> a
maximum :: forall a. Ord a => Coordinates n a -> a
$cminimum :: forall (n :: Nat) a. Ord a => Coordinates n a -> a
minimum :: forall a. Ord a => Coordinates n a -> a
$csum :: forall (n :: Nat) a. Num a => Coordinates n a -> a
sum :: forall a. Num a => Coordinates n a -> a
$cproduct :: forall (n :: Nat) a. Num a => Coordinates n a -> a
product :: forall a. Num a => Coordinates n a -> a
Foldable, Functor (Coordinates n)
Foldable (Coordinates n)
(Functor (Coordinates n), Foldable (Coordinates n)) =>
(forall (f :: * -> *) a b.
 Applicative f =>
 (a -> f b) -> Coordinates n a -> f (Coordinates n b))
-> (forall (f :: * -> *) a.
    Applicative f =>
    Coordinates n (f a) -> f (Coordinates n a))
-> (forall (m :: * -> *) a b.
    Monad m =>
    (a -> m b) -> Coordinates n a -> m (Coordinates n b))
-> (forall (m :: * -> *) a.
    Monad m =>
    Coordinates n (m a) -> m (Coordinates n a))
-> Traversable (Coordinates n)
forall (n :: Nat). Functor (Coordinates n)
forall (n :: Nat). Foldable (Coordinates n)
forall (n :: Nat) (m :: * -> *) a.
Monad m =>
Coordinates n (m a) -> m (Coordinates n a)
forall (n :: Nat) (f :: * -> *) a.
Applicative f =>
Coordinates n (f a) -> f (Coordinates n a)
forall (n :: Nat) (m :: * -> *) a b.
Monad m =>
(a -> m b) -> Coordinates n a -> m (Coordinates n b)
forall (n :: Nat) (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> Coordinates n a -> f (Coordinates n b)
forall (t :: * -> *).
(Functor t, Foldable t) =>
(forall (f :: * -> *) a b.
 Applicative f =>
 (a -> f b) -> t a -> f (t b))
-> (forall (f :: * -> *) a. Applicative f => t (f a) -> f (t a))
-> (forall (m :: * -> *) a b.
    Monad m =>
    (a -> m b) -> t a -> m (t b))
-> (forall (m :: * -> *) a. Monad m => t (m a) -> m (t a))
-> Traversable t
forall (m :: * -> *) a.
Monad m =>
Coordinates n (m a) -> m (Coordinates n a)
forall (f :: * -> *) a.
Applicative f =>
Coordinates n (f a) -> f (Coordinates n a)
forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> Coordinates n a -> m (Coordinates n b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> Coordinates n a -> f (Coordinates n b)
$ctraverse :: forall (n :: Nat) (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> Coordinates n a -> f (Coordinates n b)
traverse :: forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> Coordinates n a -> f (Coordinates n b)
$csequenceA :: forall (n :: Nat) (f :: * -> *) a.
Applicative f =>
Coordinates n (f a) -> f (Coordinates n a)
sequenceA :: forall (f :: * -> *) a.
Applicative f =>
Coordinates n (f a) -> f (Coordinates n a)
$cmapM :: forall (n :: Nat) (m :: * -> *) a b.
Monad m =>
(a -> m b) -> Coordinates n a -> m (Coordinates n b)
mapM :: forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> Coordinates n a -> m (Coordinates n b)
$csequence :: forall (n :: Nat) (m :: * -> *) a.
Monad m =>
Coordinates n (m a) -> m (Coordinates n a)
sequence :: forall (m :: * -> *) a.
Monad m =>
Coordinates n (m a) -> m (Coordinates n a)
Traversable)

type role Coordinates nominal representational

{- | Construct a type-indexed coordinate list only when list length equals the KnownNat
index. A mismatch returns Left InvalidArgument; values remain lazy.
-}
coordinates :: forall n a. (KnownNat n) => [a] -> Either MathError (Coordinates n a)
coordinates :: forall (n :: Nat) a.
KnownNat n =>
[a] -> Either MathError (Coordinates n a)
coordinates [a]
xs
    | Int -> Integer
forall a. Integral a => a -> Integer
toInteger ([a] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [a]
xs) Integer -> Integer -> Bool
forall a. Eq a => a -> a -> Bool
== Integer -> Integer
forall a. Integral a => a -> Integer
toInteger (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)) = Coordinates n a -> Either MathError (Coordinates n a)
forall a b. b -> Either a b
Right ([a] -> Coordinates n a
forall (n :: Nat) a. [a] -> Coordinates n a
Coordinates [a]
xs)
    | Bool
otherwise = MathError -> Either MathError (Coordinates n a)
forall a b. a -> Either a b
Left (String -> MathError
InvalidArgument String
"coordinates: type-level length mismatch")

{- | Extract the ordered list of a Coordinates n value. The nominal length invariant is
preserved by its public constructors.
-}
coordinateValues :: Coordinates n a -> [a]
coordinateValues :: forall (n :: Nat) a. Coordinates n a -> [a]
coordinateValues (Coordinates [a]
xs) = [a]
xs

instance (KnownNat n) => Applicative (Coordinates n) where
    pure :: forall a. a -> Coordinates n a
pure a
x = [a] -> Coordinates n a
forall (n :: Nat) a. [a] -> Coordinates n a
Coordinates [a
x | Integer
_ <- [Integer
1 .. Integer -> Integer
forall a. Integral a => a -> Integer
toInteger (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))]]
    Coordinates [a -> b]
fs <*> :: forall a b.
Coordinates n (a -> b) -> Coordinates n a -> Coordinates n b
<*> Coordinates [a]
xs = [b] -> Coordinates n b
forall (n :: Nat) a. [a] -> Coordinates n a
Coordinates (((a -> b) -> a -> b) -> [a -> b] -> [a] -> [b]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith (a -> b) -> a -> b
forall a b. (a -> b) -> a -> b
($) [a -> b]
fs [a]
xs)

{- | Convert Coordinates n to a dynamic Vector. Reject a type-level length exceeding Int
before traversing the coordinate list; otherwise preserve all values.
-}
coordinatesToVector :: forall n a. (KnownNat n) => Coordinates n a -> Either MathError (V.Vector a)
coordinatesToVector :: forall (n :: Nat) a.
KnownNat n =>
Coordinates n a -> Either MathError (Vector a)
coordinatesToVector Coordinates n a
xs = Proxy n -> Either MathError Int
forall (n :: Nat). KnownNat n => Proxy n -> Either MathError Int
natInt (Proxy n
forall {k} (t :: k). Proxy t
Proxy :: Proxy n) Either MathError Int
-> Either MathError (Vector a) -> Either MathError (Vector a)
forall a b.
Either MathError a -> Either MathError b -> Either MathError b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Vector a -> Either MathError (Vector a)
forall a b. b -> Either a b
Right ([a] -> Vector a
forall a. [a] -> Vector a
V.vector (Coordinates n a -> [a]
forall (n :: Nat) a. Coordinates n a -> [a]
coordinateValues Coordinates n a
xs))

natInt :: (KnownNat n) => Proxy n -> Either MathError Int
natInt :: forall (n :: Nat). KnownNat n => Proxy n -> Either MathError Int
natInt Proxy n
p
    | Integer
value Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
> Int -> Integer
forall a. Integral a => a -> Integer
toInteger (Int
forall a. Bounded a => a
maxBound :: Int) = MathError -> Either MathError Int
forall a b. a -> Either a b
Left (String -> MathError
InvalidArgument String
"static dimension exceeds Int")
    | Bool
otherwise = Int -> Either MathError Int
forall a b. b -> Either a b
Right (Integer -> Int
forall a. Num a => Integer -> a
fromInteger Integer
value)
  where
    value :: Integer
value = Integer -> Integer
forall a. Integral a => a -> Integer
toInteger (Proxy n -> Integer
forall (n :: Nat) (proxy :: Nat -> *).
KnownNat n =>
proxy n -> Integer
natVal Proxy n
p)