safe-tensor 0.1.0.0 → 0.2.0.0
raw patch · 18 files changed
+442/−289 lines, 18 files
Files
- CHANGELOG.md +5/−0
- README.md +4/−1
- safe-tensor.cabal +3/−3
- src/Math/Tensor.hs +79/−56
- src/Math/Tensor/Basic.hs +0/−1
- src/Math/Tensor/Basic/Area.hs +0/−6
- src/Math/Tensor/Basic/Delta.hs +7/−11
- src/Math/Tensor/Basic/Epsilon.hs +0/−4
- src/Math/Tensor/Basic/Sym2.hs +4/−11
- src/Math/Tensor/Basic/TH.hs +0/−1
- src/Math/Tensor/LinearAlgebra.hs +0/−1
- src/Math/Tensor/LinearAlgebra/Equations.hs +0/−1
- src/Math/Tensor/LinearAlgebra/Matrix.hs +0/−1
- src/Math/Tensor/LinearAlgebra/Scalar.hs +0/−1
- src/Math/Tensor/Safe.hs +239/−91
- src/Math/Tensor/Safe/Proofs.hs +80/−77
- src/Math/Tensor/Safe/TH.hs +21/−22
- src/Math/Tensor/Safe/Vector.hs +0/−1
CHANGELOG.md view
@@ -1,4 +1,9 @@ # Changelog +## [0.2.0.0] - 2020-07-08+ * Minor API adjustments+ * major documentation improvements+ * backwards compatibility with GHC 8.6.5+ ## [0.1.0.0] - 2020-07-07 Initial release.
README.md view
@@ -1,8 +1,9 @@+ [](https://hackage.haskell.org/package/safe-tensor) [](https://travis-ci.org/nilsalex/safe-tensor) # safe-tensor Dependently typed tensor algebra in Haskell. Useful for applications in field theory, e.g., carrying out calculations for https://doi.org/10.1103/PhysRevD.101.084025 ## Rationale-Tensor calculus is reflected in the type system. Let us view a tensor as a multilinear map from a product of vector spaces and duals thereof to the common field. The type of each tensor is its *generalized rank*, describing the vector spaces it acts on and assigning a label to each vector space. There are a few rules for tensor operations:+Tensor calculus is reflected in the type system. We regard a tensor as a multilinear map from a product of vector spaces and duals thereof to the common field. The type of each tensor is its *generalized rank*, describing the vector spaces it acts on and assigning a label to each vector space. There are a few rules for tensor operations: - Only tensors of the same type may be added. The result is a tensor of this type. - Tensors may be multiplied if the resulting generalized rank does not contain repeated labels for the same (dual) vector space.@@ -11,3 +12,5 @@ It is thus impossible to perform inconsistent tensor operations. There is also an existentially typed variant of the tensor type useful for runtime computations. These computations take place in the Error monad, throwing errors if operand types are not consistent.++The approach is described in detail in the [Hackage documentation](https://hackage.haskell.org/package/safe-tensor/docs/Math-Tensor-Safe.html).
safe-tensor.cabal view
@@ -4,12 +4,12 @@ -- -- see: https://github.com/sol/hpack ----- hash: d8db1e3bc409f22390d910f02253e624ef929b8fb88ef85dd8dce87340fc3b65+-- hash: 01b45dfa508544cf3d4c145d847b74cfe33a819cd020b449016b3c1d38cf3afc name: safe-tensor-version: 0.1.0.0+version: 0.2.0.0 synopsis: Dependently typed tensor algebra-description: Please see the README on GitHub at <https://github.com/nilsalex/safe-tensor#readme>+description: For an introduction to the library, see "Math.Tensor.Safe". For more information, see the README on GitHub at <https://github.com/nilsalex/safe-tensor#readme> category: Math homepage: https://github.com/nilsalex/safe-tensor#readme bug-reports: https://github.com/nilsalex/safe-tensor/issues
src/Math/Tensor.hs view
@@ -18,37 +18,53 @@ Copyright : (c) Nils Alex, 2020 License : MIT Maintainer : nils.alex@fau.de-Stability : experimental -Existentially quantified wrapper around the safe interface from 'Math.Tensor.Safe'.+Existentially quantified wrapper around the safe interface from "Math.Tensor.Safe". In contrast to the safe interface, all tensor operations are fair game, but potentially-unsafe operations take place in the Error monad 'Control.Monad.Except' and may fail+illegal operations take place in the Error monad "Control.Monad.Except" and may fail with an error message.++For usage examples, see <https://github.com/nilsalex/safe-tensor/#readme>.++For the documentation on generalized tensor ranks, see "Math.Tensor.Safe". -} ----------------------------------------------------------------------------- module Math.Tensor- ( -- * Existentially quantified around 'Tensor'+ ( -- * Existentially quantified tensor+ -- |Wrapping a @'Tensor' r v@ in a @'T' v@ allows to define tensor operations like+ -- additions or multiplications without any constraints on the generalized ranks+ -- of the operands. T(..)- , Label- -- * Fundamental operations+ , -- * Unrefined rank types+ -- |These unrefined versions of the types used to parameterise generalized tensor+ -- ranks are used in functions producing or manipulating existentially quantified+ -- tensors.+ Label+ , Dimension+ , RankT+ -- * Tensor operations+ -- |The existentially quantified versions of tensor operations from "Math.Tensor.Safe".+ -- Some operations are always safe and therefore pure. The unsafe operations take place+ -- in the Error monad "Control.Monad.Except". , rankT- , scalar- , zero- -- * Conversion from and to lists+ -- ** Special tensors+ , scalarT+ , zeroT+ -- ** Conversion from and to lists , toListT , fromListT , removeZerosT- -- * Tensor algebra+ -- ** Tensor algebra , (.*) , (.+) , (.-)- , (#.)- -- * Tensor operations+ , (.°)+ -- ** Other operations , contractT , transposeT , transposeMultT , relabelT- , -- * Constructing ranks+ , -- * Rank construction conRank , covRank , conCovRank@@ -65,9 +81,6 @@ , fromSing ) import Data.Singletons.Prelude- ( SBool (STrue, SFalse)- , SMaybe (SNothing, SJust)- ) import Data.Singletons.Prelude.Maybe ( sIsJust )@@ -86,7 +99,7 @@ import Control.Monad.Except (MonadError, throwError) --- |'T' wraps around 'Tensor' and exposes only the value type @v@.+-- |@'T'@ wraps around @'Tensor'@ and exposes only the value type @v@. data T :: Type -> Type where T :: forall (r :: Rank) v. SingI r => Tensor r v -> T v @@ -95,15 +108,30 @@ instance Functor T where fmap f (T t) = T $ fmap f t --- |Produces a 'Scalar' of given value. Result is pure+-- |The unrefined type of labels.+--+-- @ Demote Symbol ~ 'Data.Text.Text' @+type Label = Demote Symbol++-- |The unrefined type of dimensions.+--+-- @ Demote Nat ~ 'GHC.Natural.Natural' @+type Dimension = Demote Nat++-- |The unrefined type of generalized tensor ranks.+--+-- @ 'Demote' 'Rank' ~ 'GRank' 'Label' 'Dimension' ~ [('VSpace' 'Label' 'Dimension', 'IList' 'Dimension')] @+type RankT = Demote Rank++-- |@'Scalar'@ of given value. Result is pure -- because there is only one possible rank: @'[]@-scalar :: v -> T v-scalar v = T $ Scalar v+scalarT :: v -> T v+scalarT v = T $ Scalar v --- |Produces a 'ZeroTensor' of given rank @r@. Throws an+-- |@'ZeroTensor'@ of given rank @r@. Throws an -- error if @'Sane' r ~ ''False'@.-zero :: MonadError String m => Demote Rank -> m (T v)-zero dr =+zeroT :: MonadError String m => RankT -> m (T v)+zeroT dr = withSomeSing dr $ \sr -> case sSane sr %~ STrue of Proved Refl ->@@ -124,14 +152,14 @@ xs' <- vecFromList sn xs return $ x `VCons` xs' --- |Pure function removing all zeros from a tensor. Wraps around 'removeZeros'.+-- |Pure function removing all zeros from a tensor. Wraps around @'removeZeros'@. removeZerosT :: (Eq v, Num v) => T v -> T v removeZerosT o = case o of T t -> T $ removeZeros t --- |Tensor product. Returns an error if ranks overlap, i.e.--- @MergeR r1 r2 ~ 'Nothing@. Wraps around '(&*)'.+-- |Tensor product. Throws an error if ranks overlap, i.e.+-- @'MergeR' r1 r2 ~ ''Nothing'@. Wraps around @'(&*)'@. (.*) :: (Num v, MonadError String m) => T v -> T v -> m (T v) (.*) o1 o2 = case o1 of@@ -146,12 +174,12 @@ infixl 7 .* -- |Scalar multiplication of a tensor.-(#.) :: Num v => v -> T v -> T v-(#.) s = fmap (*s)+(.°) :: Num v => v -> T v -> T v+(.°) s = fmap (*s) -infixl 7 #.+infixl 7 .° --- |Tensor addition. Returns an error if summand ranks do not coincide. Wraps around '(&+)'.+-- |Tensor addition. Throws an error if summand ranks do not coincide. Wraps around @'(&+)'@. (.+) :: (Eq v, Num v, MonadError String m) => T v -> T v -> m (T v) (.+) o1 o2 = case o1 of@@ -167,7 +195,7 @@ Disproved _ -> throwError "Generalized tensor ranks do not match. Cannot add." infixl 6 .+ --- |Tensor subtraction. Returns an error if summand ranks do not coincide. Wraps around '(&-)'.+-- |Tensor subtraction. Throws an error if summand ranks do not coincide. Wraps around @'(&-)'@. (.-) :: (Eq v, Num v, MonadError String m) => T v -> T v -> m (T v) (.-) o1 o2 = case o1 of@@ -183,7 +211,7 @@ Disproved _ -> throwError "Generalized tensor ranks do not match. Cannot add." -- |Tensor contraction. Pure function, because a tensor of any rank can be contracted.--- Wraps around 'contract'.+-- Wraps around @'contract'@. contractT :: (Num v, Eq v) => T v -> T v contractT o = case o of@@ -192,10 +220,10 @@ sr' = sContractR sr in withSingI sr' $ T $ contract t --- |Tensor transposition. Returns an error if given indices cannot be transposed.--- Wraps around 'transpose'.+-- |Tensor transposition. Throws an error if given indices cannot be transposed.+-- Wraps around @'transpose'@. transposeT :: MonadError String m =>- Demote (VSpace Symbol Nat) -> Demote (Ix Symbol) -> Demote (Ix Symbol) ->+ VSpace Label Dimension -> Ix Label -> Ix Label -> T v -> m (T v) transposeT v ia ib o = case o of@@ -209,10 +237,10 @@ STrue -> return $ T $ transpose sv sia sib t SFalse -> throwError $ "Cannot transpose indices " ++ show v ++ " " ++ show ia ++ " " ++ show ib ++ "!" --- |Transposition of multiple indices. Returns an error if given indices cannot be transposed.--- Wraps around 'transposeMult'.+-- |Transposition of multiple indices. Throws an error if given indices cannot be transposed.+-- Wraps around @'transposeMult'@. transposeMultT :: MonadError String m =>- Demote (VSpace Symbol Nat) -> Demote [(Symbol,Symbol)] -> Demote [(Symbol,Symbol)] -> T v -> m (T v)+ VSpace Label Dimension -> [(Label,Label)] -> [(Label,Label)] -> T v -> m (T v) transposeMultT _ [] [] _ = throwError "Empty lists for transpositions!" transposeMultT v (con:cons) [] o = case o of@@ -240,10 +268,10 @@ Disproved _ -> throwError $ "Cannot transpose indices " ++ show v ++ " " ++ show tr ++ "!" transposeMultT _ _ _ _ = throwError "Simultaneous transposition of contravariant and covariant indices not yet supported!" --- |Relabelling of tensor indices. Returns an error if given relabellings are not allowed.--- Wraps around 'relabel'.+-- |Relabelling of tensor indices. Throws an error if given relabellings are not allowed.+-- Wraps around @'relabel'@. relabelT :: MonadError String m =>- Demote (VSpace Symbol Nat) -> Demote [(Symbol,Symbol)] -> T v -> m (T v)+ VSpace Label Dimension -> [(Label,Label)] -> T v -> m (T v) relabelT _ [] _ = throwError "Empty list for relabelling!" relabelT v (r:rs) o = case o of@@ -261,8 +289,8 @@ Disproved _ -> throwError $ "Cannot relabel indices " ++ show v ++ " " ++ show rr ++ "!" _ -> throwError $ "Cannot relabel indices " ++ show v ++ " " ++ show rr ++ "!" --- |Exposes the hidden rank over which 'T' quantifies. Possible because of the @'SingI' r@ constraint.-rankT :: T v -> Demote Rank+-- |Hidden rank over which @'T'@ quantifies. Possible because of the @'SingI' r@ constraint.+rankT :: T v -> RankT rankT o = case o of T (_ :: Tensor r v) ->@@ -278,9 +306,9 @@ in withSingI sn $ first vecToList <$> toList t --- |Constructs a tensor from a rank and an assocs list. Returns an error for illegal ranks+-- |Constructs a tensor from a rank and an assocs list. Throws an error for illegal ranks -- or incompatible assocs lists.-fromListT :: MonadError String m => Demote Rank -> [([Int], v)] -> m (T v)+fromListT :: MonadError String m => RankT -> [([Int], v)] -> m (T v) fromListT r xs = withSomeSing r $ \sr -> withSingI sr $@@ -292,33 +320,28 @@ return (vec', val)) xs Disproved _ -> throwError $ "Insane tensor rank : " <> show r --- |The unrefined type of labels.------ @ Demote Symbol ~ Text @-type Label = Demote Symbol- -- |Lifts sanity check of ranks into the error monad. saneRank :: (Ord s, Ord n, MonadError String m) => GRank s n -> m (GRank s n) saneRank r | sane r = pure r | otherwise = throwError "Index lists must be strictly ascending." --- |Creates contravariant rank from vector space labe, vector space dimension,--- and list of index labels. Returns an error for illegal ranks.+-- |Contravariant rank from vector space label, vector space dimension,+-- and list of index labels. Throws an error for illegal ranks. conRank :: (MonadError String m, Integral a, Ord s, Ord n, Num n) => s -> a -> [s] -> m (GRank s n) conRank _ _ [] = throwError "Generalized rank must have non-vanishing index list!" conRank v d (i:is) = saneRank [(VSpace v (fromIntegral d), Con (i :| is))] --- |Creates covariant rank from vector space labe, vector space dimension,--- and list of index labels. Returns an error for illegal ranks.+-- |Covariant rank from vector space label, vector space dimension,+-- and list of index labels. Throws an error for illegal ranks. covRank :: (MonadError String m, Integral a, Ord s, Ord n, Num n) => s -> a -> [s] -> m (GRank s n) covRank _ _ [] = throwError "Generalized rank must have non-vanishing index list!" covRank v d (i:is) = saneRank [(VSpace v (fromIntegral d), Cov (i :| is))] --- |Creates mixed rank from vector space label, vector space dimension,--- and lists of index labels. Returns an error for illegal ranks.+-- |Mixed rank from vector space label, vector space dimension,+-- and lists of index labels. Throws an error for illegal ranks. conCovRank :: (MonadError String m, Integral a, Ord s, Ord n, Num n) => s -> a -> [s] -> [s] -> m (GRank s n) conCovRank _ _ _ [] = throwError "Generalized rank must have non-vanishing index list!"
src/Math/Tensor/Basic.hs view
@@ -5,7 +5,6 @@ Copyright : (c) Nils Alex, 2020 License : MIT Maintainer : nils.alex@fau.de-Stability : experimental Definitions of basic tensors, re-exported for convenience. -}
src/Math/Tensor/Basic/Area.hs view
@@ -20,7 +20,6 @@ Copyright : (c) Nils Alex, 2020 License : MIT Maintainer : nils.alex@fau.de-Stability : experimental Definitions of area-symmetric tensors. -}@@ -65,11 +64,6 @@ , withSingI ) import Data.Singletons.Prelude- ( SBool (STrue)- , PSemigroup ((<>))- , SMaybe (SJust)- , (%<>)- ) import Data.Singletons.Decide ( (:~:) (Refl) , Decision (Proved)
src/Math/Tensor/Basic/Delta.hs view
@@ -18,7 +18,6 @@ Copyright : (c) Nils Alex, 2020 License : MIT Maintainer : nils.alex@fau.de-Stability : experimental Definitions of Kronecker deltas \(\delta^{a}_{\hphantom ab}\) (identity automorphisms) for arbitrary vector spaces.@@ -43,9 +42,6 @@ , withSomeSing ) import Data.Singletons.Prelude- ( SList (SNil)- , SBool (STrue)- ) import Data.Singletons.Decide ( (:~:) (Refl) , Decision (Proved)@@ -71,8 +67,8 @@ KnownNat n, Num v, '[ '( 'VSpace id n, 'ConCov (a ':| '[]) (b ':| '[])) ] ~ r,- Tail' (Tail' r) ~ '[],- Sane (Tail' r) ~ 'True+ TailR (TailR r) ~ '[],+ Sane (TailR r) ~ 'True ) => Sing id -> Sing n -> Sing a -> Sing b -> Tensor r v@@ -84,8 +80,8 @@ delta :: forall (id :: Symbol) (n :: Nat) (a :: Symbol) (b :: Symbol) (r :: Rank) v. ( '[ '( 'VSpace id n, 'ConCov (a ':| '[]) (b ':| '[]))] ~ r,- Tail' (Tail' r) ~ '[],- Sane (Tail' r) ~ 'True,+ TailR (TailR r) ~ '[],+ Sane (TailR r) ~ 'True, SingI n, Num v ) => Tensor r v@@ -93,7 +89,7 @@ sn -> let x = fromIntegral $ withKnownNat sn $ natVal sn in Tensor (f x) where- f :: Int -> [(Int, Tensor (Tail' r) v)]+ f :: Int -> [(Int, Tensor (TailR r) v)] f x = map (\i -> (i, Tensor [(i, Scalar 1)])) [0..x - 1] -- |The Kronecker delta \(\delta^a_{\hphantom ab} \) for a given@@ -113,6 +109,6 @@ withKnownSymbol sa $ withKnownSymbol sb $ let sl = sDeltaRank svid svdim sa sb- in case sTail' (sTail' sl) of- SNil -> case sSane (sTail' sl) %~ STrue of+ in case sTailR (sTailR sl) of+ SNil -> case sSane (sTailR sl) %~ STrue of Proved Refl -> T $ delta' svid svdim sa sb
src/Math/Tensor/Basic/Epsilon.hs view
@@ -19,7 +19,6 @@ Copyright : (c) Nils Alex, 2020 License : MIT Maintainer : nils.alex@fau.de-Stability : experimental Definitions of covariant and contravariant epsilon tensor densities like \(\epsilon_{abc}\).@@ -49,9 +48,6 @@ , fromSing ) import Data.Singletons.Prelude- ( SBool (STrue)- , SMaybe (SNothing, SJust)- ) import Data.Singletons.Decide ( (:~:) (Refl) , Decision (Proved)
src/Math/Tensor/Basic/Sym2.hs view
@@ -19,7 +19,6 @@ Copyright : (c) Nils Alex, 2020 License : MIT Maintainer : nils.alex@fau.de-Stability : experimental Definitions of symmetric tensors. -}@@ -75,12 +74,6 @@ , withSingI ) import Data.Singletons.Prelude- ( SBool (STrue)- , POrd ((<))- , SOrdering (SLT)- , SMaybe (SJust)- , sCompare- ) import Data.Singletons.Decide ( (:~:) (Refl) , Decision (Proved)@@ -185,7 +178,7 @@ sn -> let x = fromIntegral $ withKnownNat sn $ natVal sn in Tensor (f x) where- f :: Int -> [(Int, Tensor (Tail' r) v)]+ f :: Int -> [(Int, Tensor (TailR r) v)] f x = map (\i -> (i, Tensor [(i, Scalar 1)])) [0..x - 1] eta' :: forall (id :: Symbol) (n :: Nat) (a :: Symbol) (b :: Symbol) (r :: Rank) v.@@ -210,7 +203,7 @@ sn -> let x = fromIntegral $ withKnownNat sn $ natVal sn in Tensor (f x) where- f :: Int -> [(Int, Tensor (Tail' r) v)]+ f :: Int -> [(Int, Tensor (TailR r) v)] f x = map (\i -> (i, Tensor [(i, Scalar (if i == 0 then 1 else -1))])) [0..x - 1] gammaInv' :: forall (id :: Symbol) (n :: Nat) (a :: Symbol) (b :: Symbol) (r :: Rank) v.@@ -235,7 +228,7 @@ sn -> let x = fromIntegral $ withKnownNat sn $ natVal sn in Tensor (f x) where- f :: Int -> [(Int, Tensor (Tail' r) v)]+ f :: Int -> [(Int, Tensor (TailR r) v)] f x = map (\i -> (i, Tensor [(i, Scalar 1)])) [0..x - 1] etaInv' :: forall (id :: Symbol) (n :: Nat) (a :: Symbol) (b :: Symbol) (r :: Rank) v.@@ -260,7 +253,7 @@ sn -> let x = fromIntegral $ withKnownNat sn $ natVal sn in Tensor (f x) where- f :: Int -> [(Int, Tensor (Tail' r) v)]+ f :: Int -> [(Int, Tensor (TailR r) v)] f x = map (\i -> (i, Tensor [(i, Scalar (if i == 0 then 1 else -1))])) [0..x - 1] injSym2Con' :: forall (id :: Symbol) (n :: Nat) (a :: Symbol) (b :: Symbol)
src/Math/Tensor/Basic/TH.hs view
@@ -30,7 +30,6 @@ Copyright : (c) Nils Alex, 2020 License : MIT Maintainer : nils.alex@fau.de-Stability : experimental Template Haskell for 'Math.Tensor.Basic'. -}
src/Math/Tensor/LinearAlgebra.hs view
@@ -5,7 +5,6 @@ Copyright : (c) Nils Alex, 2020 License : MIT Maintainer : nils.alex@fau.de-Stability : experimental Linear algebra for tensor equations. -}
src/Math/Tensor/LinearAlgebra/Equations.hs view
@@ -10,7 +10,6 @@ Copyright : (c) Nils Alex, 2020 License : MIT Maintainer : nils.alex@fau.de-Stability : experimental Linear tensor equations. -}
src/Math/Tensor/LinearAlgebra/Matrix.hs view
@@ -8,7 +8,6 @@ Copyright : (c) Nils Alex, 2020 License : MIT Maintainer : nils.alex@fau.de-Stability : experimental Gaussian elimination subroutines. -}
src/Math/Tensor/LinearAlgebra/Scalar.hs view
@@ -8,7 +8,6 @@ Copyright : (c) Nils Alex, 2020 License : MIT Maintainer : nils.alex@fau.de-Stability : experimental Scalar types for usage as Tensor values. -}
src/Math/Tensor/Safe.hs view
@@ -19,41 +19,198 @@ Copyright : (c) Nils Alex, 2020 License : MIT Maintainer : nils.alex@fau.de-Stability : experimental -Dependently typed tensor algebra.+Dependently typed implementation of the Einstein tensor calculus, primarily used+in mathematical physics. For usage examples, see+<https://github.com/nilsalex/safe-tensor/#readme>. -} ----------------------------------------------------------------------------- module Math.Tensor.Safe- ( -- * The Tensor GADT+ ( + -- * Tensor calculus+ -- |Given a field \(K\) and a \(K\)-vector space \(V\) of dimension \(n\),+ -- a /tensor/ \(T\) of rank \((r,s)\) is a multilinear map from \(r\)+ -- copies of the dual vector space \(V^\ast\) and \(s\) copies of \(V\)+ -- to \(K\),+ --+ -- \[+ -- T \colon \underbrace{V^\ast \times \dots \times V^\ast}_{r\text{ times}} \times \underbrace{V \times \dots \times V}_{s\text{ times}} \rightarrow K.+ -- \]+ --+ -- The /components/ \(T^{a_1\dots a_r}_{\hphantom{a_1\dots a_r}b_1\dots b_s} \in K\)+ -- with respect to a basis \((e_i)_{i=1\dots n}\) of \(V\) and a corresponding+ -- dual basis \((\epsilon^i)_{i=1\dots n}\) of \(V^\ast\) are the \(n^{r+s}\)+ -- numbers+ --+ -- \[+ -- T^{a_1\dots a_r}_{\hphantom{a_1\dots a_r}b_1\dots b_s} = T(\epsilon^{a_1},\dots,\epsilon^{a_r},e_{b_1},\dots,e_{b_s}).+ -- \]+ --+ -- The upper indices \(a_i\) are called /contravariant/ and the lower indices \(b_i\) are+ -- called /covariant/, reflecting their behaviour under a+ -- [change of basis](https://en.wikipedia.org/wiki/Change_of_basis). From the components+ -- and the basis, the tensor can be reconstructed as+ --+ -- \[+ -- T = T^{a_1\dots a_r}_{\hphantom{a_1\dots a_3}b_1\dots b_s} \cdot e_{a_1} \otimes \dots \otimes e_{a_r} \otimes \epsilon^{b_1} \otimes \dots \otimes \epsilon^{b_s}+ -- \]+ --+ -- using the [Einstein summation convention](https://ncatlab.org/nlab/show/Einstein+summation+convention)+ -- and the [tensor product](https://en.wikipedia.org/wiki/Tensor_product).+ --+ -- The representation of tensors using their components with respect to a fixed but arbitrary+ -- basis forms the foundation of this tensor calculus. An example is the sum of a \((2,0)\) tensor+ -- \(T\) and the transposition of a \((2,0)\) tensor \(S\), which using the calculus can be+ -- written as+ --+ -- \[+ -- \lbrack T + \operatorname{transpose}(S)\rbrack^{a b} = T^{a b} + S^{b a}.+ -- \]+ --+ -- The /generalized rank/ of the tensor \(T^{a b}\) in the above example is the set of+ -- contravariant indices \(\{a, b\}\). The indices must be distinct. The generalized+ -- rank of a tensor with both contravariant and covariant indices+ -- (e.g. \(T^{ac}_{\hphantom{ac}rbl}\)) is the set of contravariant and the+ -- set of covariant indices (e.g. \((\{a,c\}, \{b,l,r\})\)). Note that+ -- both sets need not be distinct, as they label completely different entities+ -- (basis vectors vs. dual basis vectors). Overlapping indices can be removed+ -- by performing a [contraction](https://ncatlab.org/nlab/show/contraction#contraction_of_tensors),+ -- see also @'contract'@.+ --+ -- Tensors with generalized rank can be understood as a+ -- [graded algebra](https://ncatlab.org/nlab/show/graded+algebra) where only+ -- tensors of the same generalized rank can be added together and the tensor product+ -- of two tensors yields a tensor with new generalized rank. Importantly, this product+ -- is only possible if both the contravariant indices and the covariant indices of the+ -- factors do not overlap. As an example, the generalized rank of the tensor product+ -- \(T^{ap}_{\hphantom{ap}fc} S^{eg}_{\hphantom{eg}p}\) would be+ -- \((\{a,e,g,p\},\{c,f,p\})\).+ --+ -- We take this abstraction one step further and consider tensors that are multilinear+ -- maps over potentially different vector spaces and duals thereof. The generalized rank+ -- now consists of the contra- and covariant index sets for each distinct vector space.+ -- Upon multiplication of tensors, only the indices for each vector space must be distinct+ -- and contraction only removes overlapping indices among the same vector space.+ --+ -- Practical examples of configurations with multiple vector spaces are situations where+ -- both the tangent space to spacetime, \(V = T_pM\), and symmetric tensors+ -- \(S^2(V) \subset V\otimes V\), which form a proper subset of \(V\otimes V\),+ -- are considered simultaneously. See also "Math.Tensor.Basic.Sym2".++ -- * Generalized rank+ -- |The tensor calculus described above is now implemented in Haskell. Using @Template Haskell@+ -- provided by the @singletons@ library, this code is lifted to the type level and+ -- singletons are generated.+ --+ -- A vector space is parameterised by a label @a@ and a dimension @b@.+ VSpace(..)+ , -- |Each vector space must have a list of indices. This can be a contravariant index list,+ -- a covariant index list, or both. For @'sane'@ generalized ranks, the individual+ -- lists must be ascending. As already noted, both lists in the mixed case need not+ -- be disjoint.+ IList(..)+ , -- |The generalized tensor rank is a list of vector spaces and associated index lists.+ -- Sane generalized ranks have their vector spaces in ascending order.+ GRank+ , -- |The specialisation used for the parameterisation of the tensor type.+ Rank+ , -- |As explained above, the contravariant or covariant indices for each vector space must+ -- be unique. They must also be /sorted/ for more efficiency. The same applies for the+ -- vector spaces: Each distinct vector space must have a unique representation,+ -- generalized ranks are sorted by the vector spaces. This is checked by the function+ -- @'sane'@.+ sane+ , -- |The function @'headR'@ extracts the first index within a generalized rank.+ -- The first index is always referring to the+ -- first vector space within the rank. If the rank is purely covariant or purley contravariant,+ -- the first index ist the first element of the respective index list. For mixed+ -- ranks, the first index is the one which compares less. If they compare equal, it is always+ -- the contravariant index. This defines an order where contractible indices always appear+ -- next to each other, which greatly facilitates contraction.+ headR+ , -- |The remaining rank after popping the @'headR'@ is obtained by the function @'tailR'@.+ tailR+ , -- |The total number of indices. + lengthR+ , -- |A generalized rank is contracted by considering each vector space separately.+ -- Indices appearing in both upper and lower position are removed from the rank.+ -- If that leaves a vector space without indices, it is also discarded.+ contractR+ , -- |Merging two generalized ranks in order to obtain the generalized rank of the+ -- tensor product. Returns @'Nothing'@ for incompatible ranks.+ mergeR+ , -- |To perform transpositions of two indices, single contravariant or covariant indices+ -- have to be specified. A representation for single indices is provided by the sum type @'Ix'@.+ Ix(..)+ , -- |To perform transpositions of multiple indices at once, a list of source+ -- and a list of target indices has to be provided. Both lists must be permutations+ -- of each other. A suitable representation is provided by the sum type @'TransRule'@.+ --+ -- Note that transposing indices in a tensor does not change its generalized rank.+ TransRule (..)+ , -- |To relabel a tensor, a list of source-target pairs has to be provided. Relabelling+ -- affects each index regardless of upper or lower position, so it suffices to have+ -- the type synonym @'RelabelRule'@.+ RelabelRule+ , -- |Relabelling a tensor changes its generalized rank. If tensor indices corresponding+ -- to a given vector space can be relabelled using a given @'RelabelRule'@,+ -- @'relabelR'@ returns the new generalized rank. Otherwise, it returns @'Nothing'@.+ relabelR++ , -- * The Tensor GADT+ -- |The @'Tensor'@ type parameterised by a generalized rank @r@ and a value type @v@+ -- is a recursive container for tensor components of value @v@.+ --+ -- - The base case is a @'Scalar'@, which represents a tensor with empty rank.+ -- A scalar holds a single value of type @v@.+ --+ -- - For non-empty ranks, a tensor is represented of as a mapping from all possible+ -- index values for the first index @'headR' r@ to tensors of lower rank @'tailR' r@,+ -- implemented as sparse ascending assocs list (omitting zero values).+ --+ -- - There is a shortcut for zero tensors, which are represented as @'ZeroTensor'@+ -- regardless of the generalized rank.+ --+ -- Generalized ranks must be @'Sane'@. The empty rank @'[]@ is always sane. Tensor(..)- -- * Generic Rank of a Tensor- -- |A vector space is the product of a label and a dimension.- , VSpace(..)- -- |The generic tensor rank is a list of vector spaces with label, dimension and- -- associated index list.- , GRank- -- |The rank of a tensor is a generic rank specialized to 'Symbol' and 'Nat'- , Rank- -- * Length-typed assocs lists- -- |Type-level naturals used internally.- , N(..)- , -- |Length-typed vector used internally.- Vec(..)- , vecFromListUnsafe- , -- * Conversion from and to lists+ , -- ** Conversion from and to lists+ -- |A @'Tensor' r v@ can be constructed from a list of key-value pairs,+ -- where keys are length-typed vectors @'Vec'@ of @n = 'lengthR' r@ indices+ -- and values are the corresponding components.+ --+ -- The index values must be given in the order defined by repeatedly applying+ -- @'headR'@ to the rank.+ --+ -- Given a value, such an assocs list is obtained by @'toList'@. fromList , fromList' , toList- , -- * Tensor algebra++ , -- * Basic operations+ -- |We have now everything at our disposal to define basic tensor operations+ -- using the rank-parameterised @'Tensor'@ type. These operations (algebra,+ -- contraction, transposition, relabelling) are /safe/ in the sense that+ -- they can only be performed between tensors of matching type and the+ -- type of the resulting tensor is predetermined. There is also an+ -- existentially quantified variant of these operations available from+ -- "Math.Tensor".++ -- ** Tensor algebra (&+), (&-), (&*), removeZeros- , -- * Contraction+ , -- ** Contraction contract- , -- * Transpositions+ , -- ** Transpositions transpose , transposeMult- , -- * Relabelling+ , -- ** Relabelling relabel++ , -- * Length-typed vectors+ -- |Type-level naturals used for tensor construction and also internally.+ N(..)+ , -- |Length-typed vector used for tensor construction and also internally.+ Vec(..)+ , vecFromListUnsafe ) where import Math.Tensor.Safe.TH@@ -70,15 +227,6 @@ , withSingI, fromSing ) import Data.Singletons.Prelude- ( SBool (STrue, SFalse)- , SList (SNil)- , SMaybe (SJust)- , SOrdering (SLT, SEQ, SGT)- , STuple2 (STuple2)- , Tail- , sFst, sSnd, sHead, sTail- , sCompare, (%==)- ) import Data.Singletons.Prelude.Maybe ( IsJust , sIsJust@@ -94,19 +242,14 @@ import Data.Bifunctor (first,second) import Data.List (foldl',groupBy,sortBy) --- |The 'Tensor' type is parameterized by its generalized 'Rank' @r@ and holds--- arbitrary values @v@.+-- |The @'Tensor'@ type parameterized by its generalized rank @r@ and+-- arbitrary value type @v@. data Tensor :: Rank -> Type -> Type where- ZeroTensor :: forall (r :: Rank) v . Sane r ~ 'True => Tensor r v -- ^- -- A tensor of any sane rank type can be zero.- Scalar :: forall v. !v -> Tensor '[] v -- ^- -- A tensor of empty rank is a scalar holding some value.+ ZeroTensor :: forall (r :: Rank) v . Sane r ~ 'True => Tensor r v+ Scalar :: forall v. !v -> Tensor '[] v Tensor :: forall (r :: Rank) (r' :: Rank) v.- (Sane r ~ 'True, Tail' r ~ r') =>- [(Int, Tensor r' v)] -> Tensor r v -- ^- -- A non-zero tensor of sane non-empty rank is represented as an assocs list of- -- component-value pairs. The keys must be unique and in ascending order.- -- The values are tensors of the next-lower rank.+ (Sane r ~ 'True, TailR r ~ r') =>+ [(Int, Tensor r' v)] -> Tensor r v deriving instance Eq v => Eq (Tensor r v) deriving instance Show v => Show (Tensor r v)@@ -127,7 +270,7 @@ EQ -> (ix, f vx vy) : unionWith f g h xs' ys' GT -> (iy, h vy) : unionWith f g h xs ys' --- |Given a 'Num' and 'Eq' instance, remove all zero values from the tensor,+-- |Given a @'Num'@ and @'Eq'@ instance, remove all zero values from the tensor, -- eventually replacing a zero @Scalar@ or an empty @Tensor@ with @ZeroTensor@. removeZeros :: (Num v, Eq v) => Tensor r v -> Tensor r v removeZeros ZeroTensor = ZeroTensor@@ -144,7 +287,7 @@ _ -> True) $ fmap (fmap removeZeros) ms --- |Tensor addition. Ranks of summands and sum coincide.+-- |Tensor addition. Generalized ranks of summands and sum coincide. -- Zero values are removed from the result. (&+) :: forall (r :: Rank) (r' :: Rank) v. ((r ~ r'), Num v, Eq v) =>@@ -162,7 +305,7 @@ infixl 6 &+ --- |Tensor subtraction. Ranks of operands and difference coincide.+-- |Tensor subtraction. Generalized ranks of operands and difference coincide. -- Zero values are removed from the result. (&-) :: forall (r :: Rank) (r' :: Rank) v. ((r ~ r'), Num v, Eq v) =>@@ -171,22 +314,23 @@ infixl 6 &- --- |Tensor multiplication, ranks of factors passed explicitly as singletons.+-- |Tensor multiplication, ranks @r@, @r'@ of factors passed explicitly as singletons.+-- Rank of result is @'MergeR' r r'@. mult :: forall (r :: Rank) (r' :: Rank) (r'' :: Rank) v. (Num v, 'Just r'' ~ MergeR r r') => Sing r -> Sing r' -> Tensor r v -> Tensor r' v -> Tensor r'' v mult _ _ (Scalar s) (Scalar t) = Scalar (s*t) mult sr sr' (Scalar s) (Tensor ms) =- case saneTail'Proof sr' of- Sub Dict -> Tensor $ fmap (fmap (mult sr (sTail' sr') (Scalar s))) ms+ case saneTailRProof sr' of+ Sub Dict -> Tensor $ fmap (fmap (mult sr (sTailR sr') (Scalar s))) ms mult sr sr' (Tensor ms) (Scalar s) =- case saneTail'Proof sr of- Sub Dict -> Tensor $ fmap (fmap (\t -> mult (sTail' sr) sr' t (Scalar s))) ms+ case saneTailRProof sr of+ Sub Dict -> Tensor $ fmap (fmap (\t -> mult (sTailR sr) sr' t (Scalar s))) ms mult sr sr' (Tensor ms) (Tensor ms') =- let sh = sHead' sr- sh' = sHead' sr'- st = sTail' sr- st' = sTail' sr'+ let sh = sHeadR sr+ sh' = sHeadR sr'+ st = sTailR sr+ st' = sTailR sr' in case saneMergeRProof sr sr' of Sub Dict -> case sh of@@ -196,22 +340,22 @@ case sCompare sv sv' of SLT -> case proofMergeLT sr sr' of Sub Dict ->- case saneTail'Proof sr of+ case saneTailRProof sr of Sub Dict -> Tensor $ fmap (fmap (\t -> mult st sr' t (Tensor ms'))) ms SGT -> case proofMergeGT sr sr' of Sub Dict ->- case saneTail'Proof sr' of+ case saneTailRProof sr' of Sub Dict -> Tensor $ fmap (fmap (mult sr st' (Tensor ms))) ms' SEQ -> case proofMergeIxNotEQ sr sr' of Sub Dict -> case sIxCompare si si' of SLT -> case proofMergeIxLT sr sr' of Sub Dict ->- case saneTail'Proof sr of+ case saneTailRProof sr of Sub Dict -> Tensor $ fmap (fmap (\t -> mult st sr' t (Tensor ms'))) ms SGT -> case proofMergeIxGT sr sr' of Sub Dict ->- case saneTail'Proof sr' of+ case saneTailRProof sr' of Sub Dict -> Tensor $ fmap (fmap (mult sr st' (Tensor ms))) ms' mult sr sr' ZeroTensor ZeroTensor = case saneMergeRProof sr sr' of@@ -229,8 +373,8 @@ case saneMergeRProof sr sr' of Sub Dict -> ZeroTensor --- |Tensor multiplication. Ranks of factors must not overlap. The Product--- rank is the merged rank of the factors.+-- |Tensor multiplication. Generalized anks @r@, @r'@ of factors must not overlap. The product+-- rank is the merged rank @'MergeR' r r'@ of the factor ranks. (&*) :: forall (r :: Rank) (r' :: Rank) (r'' :: Rank) v. (Num v, 'Just r'' ~ MergeR r r', SingI r, SingI r') => Tensor r v -> Tensor r' v -> Tensor r'' v@@ -253,18 +397,18 @@ Sub Dict -> ZeroTensor contract'' _ (Scalar v) = Scalar v contract'' sr (Tensor ms) =- case sTail' sr of+ case sTailR sr of SNil -> case singletonContractProof sr of Sub Dict -> Tensor ms st -> case saneContractProof sr of Sub Dict ->- let st' = sTail' st- sh = sHead' sr+ let st' = sTailR st+ sh = sHeadR sr sv = sFst sh si = sSnd sh- sh' = sHead' st+ sh' = sHeadR st sv' = sFst sh' si' = sSnd sh' in case sv %== sv' of@@ -281,10 +425,10 @@ [] -> Nothing [(_, v')] -> Just v' _ -> error "duplicate key in tensor assoc list") ms- ms'' = catMaybes ms' :: [Tensor (Tail' (Tail' r)) v]- in case saneTail'Proof sr of+ ms'' = catMaybes ms' :: [Tensor (TailR (TailR r)) v]+ in case saneTailRProof sr of Sub Dict ->- case saneTail'Proof st of+ case saneTailRProof st of Sub Dict -> case contractTailSameVSameIProof sr of Sub Dict -> contract' st' $ foldl' (&+) ZeroTensor ms''@@ -299,7 +443,8 @@ Sub Dict -> removeZeros $ Tensor $ fmap (fmap (contract'' st)) ms -- |Tensor contraction. Contracting a tensor is the identity function on non-contractible tensors.--- Otherwise, the result is the contracted tensor with the contracted labels removed from the rank.+-- Otherwise, the result is the contracted tensor with the contracted labels removed from the+-- generalized rank. contract :: forall (r :: Rank) (r' :: Rank) v. (r' ~ ContractR r, SingI r, Num v, Eq v) => Tensor r v -> Tensor r' v@@ -307,7 +452,7 @@ -- |Tensor transposition. Given a vector space and two index labels, the result is a tensor with -- the corresponding entries swapped. Only possible if the indices are part of the rank. The--- rank remains untouched.+-- generalized rank remains untouched. transpose :: forall (vs :: VSpace Symbol Nat) (a :: Ix Symbol) (b :: Ix Symbol) (r :: Rank) v. (CanTranspose vs a b r ~ 'True, SingI r) => Sing vs -> Sing a -> Sing b -> Tensor r v -> Tensor r v@@ -320,10 +465,10 @@ Proved Refl -> transpose v b a t SLT -> let sr = sing :: Sing r- sh = sHead' sr+ sh = sHeadR sr sv = sFst sh si = sSnd sh- st = sTail' sr+ st = sTailR sr in withSingI st $ case sv %~ v of Proved Refl -> case si %~ a of@@ -340,17 +485,17 @@ Disproved _ -> case sCanTranspose v a b st of STrue -> Tensor $ fmap (fmap (transpose v a b)) ms --- |Transposition of multiple labels. Given a vector space and a list of transpositions, the+-- |Transposition of multiple labels. Given a vector space and a transposition rule, the -- result is a tensor with the corresponding entries swapped. Only possible if the indices are--- part of the rank. The rank remains untouched.-transposeMult :: forall (vs :: VSpace Symbol Nat) (tl :: TransList Symbol) (r :: Rank) v.+-- part of the generalized rank. The generalized rank remains untouched.+transposeMult :: forall (vs :: VSpace Symbol Nat) (tl :: TransRule Symbol) (r :: Rank) v. (IsJust (Transpositions vs tl r) ~ 'True, SingI r) => Sing vs -> Sing tl -> Tensor r v -> Tensor r v transposeMult _ _ ZeroTensor = ZeroTensor transposeMult sv stl tens@(Tensor ms) = let sr = sing :: Sing r- sh = sHead' sr- st = sTail' sr+ sh = sHeadR sr+ st = sTailR sr sr' = sTail sr sts = sTranspositions sv stl sr in case sv %~ sFst sh of@@ -395,19 +540,20 @@ t' = toInt t go _ [] = error "cannot transpose elements of empty list" --- |Tensor relabelling. Given a vector space and a list of relabellings, the result is a tensor--- with the resulting rank after relabelling. Only possible if labels to be renamed are part of--- the rank and if uniqueness of labels after relabelling is preserved.-relabel :: forall (vs :: VSpace Symbol Nat) (rl :: RelabelList Symbol) (r1 :: Rank) (r2 :: Rank) v.+-- |Tensor relabelling. Given a vector space and a relabelling rule, the result is a tensor+-- with the resulting generalized rank after relabelling. Only possible if labels to be+-- renamed are part of the generalized rank and if uniqueness of labels after+-- relabelling is preserved.+relabel :: forall (vs :: VSpace Symbol Nat) (rl :: RelabelRule Symbol) (r1 :: Rank) (r2 :: Rank) v. (RelabelR vs rl r1 ~ 'Just r2, Sane r2 ~ 'True, SingI r1, SingI r2) => Sing vs -> Sing rl -> Tensor r1 v -> Tensor r2 v relabel _ _ ZeroTensor = ZeroTensor relabel sv srl tens@(Tensor ms) = let sr1 = sing :: Sing r1 sr2 = sing :: Sing r2- sh = sHead' sr1- sr1' = sTail' sr1- sr2' = sTail' sr2+ sh = sHeadR sr1+ sr1' = sTailR sr1+ sr2' = sTailR sr2 sr1'' = sTail sr1 sts = sRelabelTranspositions srl (sSnd (sHead sr1)) in case sv %~ sFst sh of@@ -453,14 +599,14 @@ t' = toInt t go _ [] = error "cannot transpose elements of empty list" --- |Get assocs list from tensor. Keys are length-indexed vectors of indices.+-- |Get assocs list from @'Tensor'@. Keys are length-typed vectors of indices. toList :: forall r v n. (SingI r, SingI n, LengthR r ~ n) => Tensor r v -> [(Vec n Int, v)] toList ZeroTensor = [] toList (Scalar s) = [(VNil, s)] toList (Tensor ms) =- let st = sTail' (sing :: Sing r)+ let st = sTailR (sing :: Sing r) sn = sing :: Sing n sm = sLengthR st in case st of@@ -475,13 +621,15 @@ Proved Refl -> concatMap (\(i, v) -> case v of Tensor _ -> fmap (first (VCons i)) (withSingI st $ toList v)) ms +-- |Construct @'Tensor'@ from assocs list. Keys are length-typed vectors of indices. Generalized+-- rank is passed explicitly as singleton. fromList' :: forall r v n. (Sane r ~ 'True, LengthR r ~ n) => Sing r -> [(Vec n Int, v)] -> Tensor r v fromList' _ [] = ZeroTensor fromList' sr xs = let sn = sLengthR sr- st = sTail' sr+ st = sTailR sr sm = sLengthR st in case sn of SZ ->@@ -502,7 +650,7 @@ let ys' = groupBy (\(i,_) (i',_) -> i == i') ys in fmap (\x -> (fst $ head x, fmap snd x)) ys' --- |Construct 'Tensor' from assocs list. Keys are length-indexed vectors of indices.+-- |Construct @'Tensor'@ from assocs list. Keys are length-typed vectors of indices. fromList :: forall r v n. (SingI r, Sane r ~ 'True, LengthR r ~ n) => [(Vec n Int, v)] -> Tensor r v@@ -517,7 +665,7 @@ Tensor r v -> [([Int], Tensor (Tail r) v)] toTListWhile (Tensor ms) = let sr = sing :: Sing r- st = sTail' sr+ st = sTailR sr in case st %~ sTail sr of Proved Refl -> fmap (first pure) ms Disproved _ ->@@ -537,8 +685,8 @@ Sing a -> Tensor r v -> [([Int], Tensor r' v)] toTListUntil sa (Tensor ms) = let sr = sing :: Sing r- st = sTail' sr- sh = sHead' sr+ st = sTailR sr+ sh = sHeadR sr in case sSnd sh %~ sa of Proved Refl -> withSingI st $ case st %~ (sing :: Sing r') of@@ -564,7 +712,7 @@ else error $ "illegal assocs in fromTList : " ++ show (fmap fst xs) | otherwise = let sr' = sing :: Sing r'- st' = sTail' sr'+ st' = sTailR sr' in withSingI st' $ case sSane st' of STrue -> Tensor $ fmap (fmap fromTList) xs'''
src/Math/Tensor/Safe/Proofs.hs view
@@ -14,19 +14,22 @@ ----------------------------------------------------------------------------- {-| Module : Math.Tensor.Safe.Proofs-Description : Identities for functions on generalized tensor ranks.+Description : Type level equalities for generalized ranks. Copyright : (c) Nils Alex, 2020 License : MIT Maintainer : nils.alex@fau.de-Stability : experimental -Identities for functions on generalized tensor ranks.+Type level equalities for generalized ranks. Used in "Math.Tensor.Safe" to prove+impossible cases in pattern matching on singletons. Note that at the moment+not every pattern match has a proof, which is reflected in the number of+@-Wincomplete-patterns@ warnings.+ -} ----------------------------------------------------------------------------- module Math.Tensor.Safe.Proofs ( -- * Tails of sane ranks are sane- saneTail'Proof- , singITail'Proof+ saneTailRProof+ , singITailRProof , -- * Properties of merged ranks saneMergeRProof , proofMergeLT@@ -59,20 +62,20 @@ , Fst, Snd, Compare ) --- |The 'Tail'' of a sane rank type is sane.-{-# INLINE saneTail'Proof #-}-saneTail'Proof :: forall (r :: Rank).Sing r -> (Sane r ~ 'True) :- (Sane (Tail' r) ~ 'True)-saneTail'Proof _ = Sub axiom+-- |The 'TailR' of a sane rank type is sane.+{-# INLINE saneTailRProof #-}+saneTailRProof :: forall (r :: Rank).Sing r -> (Sane r ~ 'True) :- (Sane (TailR r) ~ 'True)+saneTailRProof _ = Sub axiom where- axiom :: Sane r ~ 'True => Dict (Sane (Tail' r) ~ 'True)+ axiom :: Sane r ~ 'True => Dict (Sane (TailR r) ~ 'True) axiom = unsafeCoerce (Dict :: Dict (a ~ a)) -- |If a rank type has a 'SingI' instance, the tail has a 'SingI' instance.-{-# INLINE singITail'Proof #-}-singITail'Proof :: forall (r :: Rank).Sing r -> SingI r :- SingI (Tail' r)-singITail'Proof _ = Sub axiom+{-# INLINE singITailRProof #-}+singITailRProof :: forall (r :: Rank).Sing r -> SingI r :- SingI (TailR r)+singITailRProof _ = Sub axiom where- axiom :: SingI r => Dict (SingI (Tail' r))+ axiom :: SingI r => Dict (SingI (TailR r)) axiom = unsafeCoerce (Dict :: Dict (a ~ a)) -- |Successfully merging two sane rank types (result is not @Nothing@) yields a sane rank type.@@ -87,19 +90,19 @@ axiom = unsafeCoerce (Dict :: Dict (a ~ a)) -- |If two rank types can be merged and the first 'VSpace' of the first rank type is less than--- the first 'VSpace' of the second rank type, the 'Tail'' of the merged rank type is equal to+-- the first 'VSpace' of the second rank type, the 'TailR' of the merged rank type is equal to -- the tail of the first rank type merged with the second rank type. {-# INLINE proofMergeLT #-} proofMergeLT :: forall (r :: Rank) (r' :: Rank) (r'' :: Rank). Sing r -> Sing r' -> (Sane r ~ 'True, Sane r' ~ 'True, MergeR r r' ~ 'Just r'',- Compare (Fst (Head' r)) (Fst (Head' r')) ~ 'LT)- :- (MergeR (Tail' r) r' ~ 'Just (Tail' r''))+ Compare (Fst (HeadR r)) (Fst (HeadR r')) ~ 'LT)+ :- (MergeR (TailR r) r' ~ 'Just (TailR r'')) proofMergeLT _ _ = Sub axiom where axiom :: (Sane r ~ 'True, Sane r' ~ 'True, MergeR r r' ~ 'Just r'',- Compare (Fst (Head' r)) (Fst (Head' r')) ~ 'LT)- => Dict (MergeR (Tail' r) r' ~ 'Just (Tail' r''))+ Compare (Fst (HeadR r)) (Fst (HeadR r')) ~ 'LT)+ => Dict (MergeR (TailR r) r' ~ 'Just (TailR r'')) axiom = unsafeCoerce (Dict :: Dict (a ~ a)) -- |If two rank types can be merged and the first 'VSpace' of the first rank type coincides with@@ -109,67 +112,67 @@ proofMergeIxNotEQ :: forall (r :: Rank) (r' :: Rank) (r'' :: Rank). Sing r -> Sing r' -> (Sane r ~ 'True, Sane r' ~ 'True, MergeR r r' ~ 'Just r'',- Compare (Fst (Head' r)) (Fst (Head' r')) ~ 'EQ)- :- ((IxCompare (Snd (Head' r)) (Snd (Head' r')) == 'EQ) ~ 'False)+ Compare (Fst (HeadR r)) (Fst (HeadR r')) ~ 'EQ)+ :- ((IxCompare (Snd (HeadR r)) (Snd (HeadR r')) == 'EQ) ~ 'False) proofMergeIxNotEQ _ _ = Sub axiom where axiom :: (Sane r ~ 'True, Sane r' ~ 'True, MergeR r r' ~ 'Just r'',- Compare (Fst (Head' r)) (Fst (Head' r')) ~ 'EQ)- => Dict ((IxCompare (Snd (Head' r)) (Snd (Head' r')) == 'EQ) ~ 'False)+ Compare (Fst (HeadR r)) (Fst (HeadR r')) ~ 'EQ)+ => Dict ((IxCompare (Snd (HeadR r)) (Snd (HeadR r')) == 'EQ) ~ 'False) axiom = unsafeCoerce (Dict :: Dict (a ~ a)) -- |If two rank types can be merged and the first 'VSpace' of the first rank type coincides with -- the first 'VSpace' of the second rank type and the first index of the first rank type compares--- less than the first index of the second rank type, the 'Tail'' of the merged rank type is equal+-- less than the first index of the second rank type, the 'TailR' of the merged rank type is equal -- to the tail of the first rank type merged with the second rank type. {-# INLINE proofMergeIxLT #-} proofMergeIxLT :: forall (r :: Rank) (r' :: Rank) (r'' :: Rank). Sing r -> Sing r' -> (Sane r ~ 'True, Sane r' ~ 'True, MergeR r r' ~ 'Just r'',- Compare (Fst (Head' r)) (Fst (Head' r')) ~ 'EQ,- IxCompare (Snd (Head' r)) (Snd (Head' r')) ~ 'LT)- :- (MergeR (Tail' r) r' ~ 'Just (Tail' r''))+ Compare (Fst (HeadR r)) (Fst (HeadR r')) ~ 'EQ,+ IxCompare (Snd (HeadR r)) (Snd (HeadR r')) ~ 'LT)+ :- (MergeR (TailR r) r' ~ 'Just (TailR r'')) proofMergeIxLT _ _ = Sub axiom where axiom :: (Sane r ~ 'True, Sane r' ~ 'True, MergeR r r' ~ 'Just r'',- Compare (Fst (Head' r)) (Fst (Head' r')) ~ 'EQ,- IxCompare (Snd (Head' r)) (Snd (Head' r')) ~ 'LT)- => Dict (MergeR (Tail' r) r' ~ 'Just (Tail' r''))+ Compare (Fst (HeadR r)) (Fst (HeadR r')) ~ 'EQ,+ IxCompare (Snd (HeadR r)) (Snd (HeadR r')) ~ 'LT)+ => Dict (MergeR (TailR r) r' ~ 'Just (TailR r'')) axiom = unsafeCoerce (Dict :: Dict (a ~ a)) -- |If two rank types can be merged and the first 'VSpace' of the first rank type is greater than--- the first 'VSpace' of the second rank type, the 'Tail'' of the merged rank type is equal to+-- the first 'VSpace' of the second rank type, the 'TailR' of the merged rank type is equal to -- the first rank type merged with the tail of the second rank type. {-# INLINE proofMergeGT #-} proofMergeGT :: forall (r :: Rank) (r' :: Rank) (r'' :: Rank). Sing r -> Sing r' -> (Sane r ~ 'True, Sane r' ~ 'True, MergeR r r' ~ 'Just r'',- Compare (Fst (Head' r)) (Fst (Head' r')) ~ 'GT)- :- (MergeR r (Tail' r') ~ 'Just (Tail' r''))+ Compare (Fst (HeadR r)) (Fst (HeadR r')) ~ 'GT)+ :- (MergeR r (TailR r') ~ 'Just (TailR r'')) proofMergeGT _ _ = Sub axiom where axiom :: (Sane r ~ 'True, Sane r' ~ 'True, MergeR r r' ~ 'Just r'',- Compare (Fst (Head' r)) (Fst (Head' r')) ~ 'GT)- => Dict (MergeR r (Tail' r') ~ 'Just (Tail' r''))+ Compare (Fst (HeadR r)) (Fst (HeadR r')) ~ 'GT)+ => Dict (MergeR r (TailR r') ~ 'Just (TailR r'')) axiom = unsafeCoerce (Dict :: Dict (a ~ a)) -- |If two rank types can be merged and the first 'VSpace' of the first rank type coincides with -- the first 'VSpace' of the second rank type and the first index of the first rank type compares--- greater than the first index of the second rank type, the 'Tail'' of the merged rank type is equal+-- greater than the first index of the second rank type, the 'TailR' of the merged rank type is equal -- to the first rank type merged with the tail of the second rank type. {-# INLINE proofMergeIxGT #-} proofMergeIxGT :: forall (r :: Rank) (r' :: Rank) (r'' :: Rank). Sing r -> Sing r' -> (Sane r ~ 'True, Sane r' ~ 'True, MergeR r r' ~ 'Just r'',- Compare (Fst (Head' r)) (Fst (Head' r')) ~ 'EQ,- IxCompare (Snd (Head' r)) (Snd (Head' r')) ~ 'GT)- :- (MergeR r (Tail' r') ~ 'Just (Tail' r''))+ Compare (Fst (HeadR r)) (Fst (HeadR r')) ~ 'EQ,+ IxCompare (Snd (HeadR r)) (Snd (HeadR r')) ~ 'GT)+ :- (MergeR r (TailR r') ~ 'Just (TailR r'')) proofMergeIxGT _ _ = Sub axiom where axiom :: (Sane r ~ 'True, Sane r' ~ 'True, MergeR r r' ~ 'Just r'',- Compare (Fst (Head' r)) (Fst (Head' r')) ~ 'EQ,- IxCompare (Snd (Head' r)) (Snd (Head' r')) ~ 'GT)- => Dict (MergeR r (Tail' r') ~ 'Just (Tail' r''))+ Compare (Fst (HeadR r)) (Fst (HeadR r')) ~ 'EQ,+ IxCompare (Snd (HeadR r)) (Snd (HeadR r')) ~ 'GT)+ => Dict (MergeR r (TailR r') ~ 'Just (TailR r'')) axiom = unsafeCoerce (Dict :: Dict (a ~ a)) -- |If a rank type is sane, its contraction is also sane.@@ -183,72 +186,72 @@ -- |The contraction of the empty rank type is the empty rank type. {-# INLINE singletonContractProof #-} singletonContractProof :: forall (r :: Rank).- Sing r -> (Tail' r ~ '[]) :- (ContractR r ~ r)+ Sing r -> (TailR r ~ '[]) :- (ContractR r ~ r) singletonContractProof _ = Sub axiom where- axiom :: Tail' r ~ '[] => Dict (ContractR r ~ r)+ axiom :: TailR r ~ '[] => Dict (ContractR r ~ r) axiom = unsafeCoerce (Dict :: Dict (a ~ a)) -- |If the first two labels of a rank type cannot be contracted because they belong to--- different 'VSpace's, the 'Tail'' of the contracted rank type is equal to the contraction--- of the 'Tail'' of the rank type.+-- different 'VSpace's, the 'TailR' of the contracted rank type is equal to the contraction+-- of the 'TailR' of the rank type. {-# INLINE contractTailDiffVProof #-} contractTailDiffVProof :: forall (r :: Rank) (t :: Rank) (t' :: Rank). Sing r ->- (t ~ Tail' r, t' ~ Tail' t, (Fst (Head' r) == Fst (Head' t)) ~ 'False)- :- (Tail' (ContractR r) ~ ContractR t)+ (t ~ TailR r, t' ~ TailR t, (Fst (HeadR r) == Fst (HeadR t)) ~ 'False)+ :- (TailR (ContractR r) ~ ContractR t) contractTailDiffVProof _ = Sub axiom where- axiom :: (t ~ Tail' r, t' ~ Tail' t, (Fst (Head' r) == Fst (Head' t)) ~ 'False)- => Dict (Tail' (ContractR r) ~ ContractR t)+ axiom :: (t ~ TailR r, t' ~ TailR t, (Fst (HeadR r) == Fst (HeadR t)) ~ 'False)+ => Dict (TailR (ContractR r) ~ ContractR t) axiom = unsafeCoerce (Dict :: Dict (a ~ a)) -- |If the first two labels of a rank type cannot be contracted because the first label is--- covariant, the 'Tail'' of the contracted rank type is equal to the contraction--- of the 'Tail'' of the rank type.+-- covariant, the 'TailR' of the contracted rank type is equal to the contraction+-- of the 'TailR' of the rank type. {-# INLINE contractTailSameVNoConProof #-} contractTailSameVNoConProof :: forall (r :: Rank) (t :: Rank) (t' :: Rank) (i :: Symbol). Sing r ->- (t ~ Tail' r, t' ~ Tail' t, (Fst (Head' r) == Fst (Head' t)) ~ 'True,- Snd (Head' r) ~ 'ICov i)- :- (Tail' (ContractR r) ~ ContractR t)+ (t ~ TailR r, t' ~ TailR t, (Fst (HeadR r) == Fst (HeadR t)) ~ 'True,+ Snd (HeadR r) ~ 'ICov i)+ :- (TailR (ContractR r) ~ ContractR t) contractTailSameVNoConProof _ = Sub axiom where- axiom :: (t ~ Tail' r, t' ~ Tail' t, (Fst (Head' r) == Fst (Head' t)) ~ 'True,- Snd (Head' r) ~ 'ICov i)- => Dict (Tail' (ContractR r) ~ ContractR t)+ axiom :: (t ~ TailR r, t' ~ TailR t, (Fst (HeadR r) == Fst (HeadR t)) ~ 'True,+ Snd (HeadR r) ~ 'ICov i)+ => Dict (TailR (ContractR r) ~ ContractR t) axiom = unsafeCoerce (Dict :: Dict (a ~ a)) -- |If the first two labels of a rank type cannot be contracted because the second label is--- covariant, the 'Tail'' of the contracted rank type is equal to the contraction--- of the 'Tail'' of the rank type.+-- covariant, the 'TailR' of the contracted rank type is equal to the contraction+-- of the 'TailR' of the rank type. {-# INLINE contractTailSameVNoCovProof #-} contractTailSameVNoCovProof :: forall (r :: Rank) (t :: Rank) (t' :: Rank) (i :: Symbol). Sing r ->- (t ~ Tail' r, t' ~ Tail' t, (Fst (Head' r) == Fst (Head' t)) ~ 'True,- Snd (Head' t) ~ 'ICon i)- :- (Tail' (ContractR r) ~ ContractR t)+ (t ~ TailR r, t' ~ TailR t, (Fst (HeadR r) == Fst (HeadR t)) ~ 'True,+ Snd (HeadR t) ~ 'ICon i)+ :- (TailR (ContractR r) ~ ContractR t) contractTailSameVNoCovProof _ = Sub axiom where- axiom :: (t ~ Tail' r, t' ~ Tail' t, (Fst (Head' r) == Fst (Head' t)) ~ 'True,- Snd (Head' t) ~ 'ICon i)- => Dict (Tail' (ContractR r) ~ ContractR t)+ axiom :: (t ~ TailR r, t' ~ TailR t, (Fst (HeadR r) == Fst (HeadR t)) ~ 'True,+ Snd (HeadR t) ~ 'ICon i)+ => Dict (TailR (ContractR r) ~ ContractR t) axiom = unsafeCoerce (Dict :: Dict (a ~ a)) -- |If the first two labels of a rank type cannot be contracted because they differ,--- the 'Tail'' of the contracted rank type is equal to the contraction of the 'Tail'' of the rank type.+-- the 'TailR' of the contracted rank type is equal to the contraction of the 'TailR' of the rank type. {-# INLINE contractTailSameVDiffIProof #-} contractTailSameVDiffIProof :: forall (r :: Rank) (t :: Rank) (t' :: Rank) (i :: Symbol) (j :: Symbol). Sing r ->- (t ~ Tail' r, t' ~ Tail' t, (Fst (Head' r) == Fst (Head' t)) ~ 'True,- Snd (Head' r) ~ 'ICon i, Snd (Head' t) ~ 'ICov j, (i == j) ~ 'False)- :- (Tail' (ContractR r) ~ ContractR t)+ (t ~ TailR r, t' ~ TailR t, (Fst (HeadR r) == Fst (HeadR t)) ~ 'True,+ Snd (HeadR r) ~ 'ICon i, Snd (HeadR t) ~ 'ICov j, (i == j) ~ 'False)+ :- (TailR (ContractR r) ~ ContractR t) contractTailSameVDiffIProof _ = Sub axiom where- axiom :: (t ~ Tail' r, t' ~ Tail' t, (Fst (Head' r) == Fst (Head' t)) ~ 'True,- Snd (Head' r) ~ 'ICon i, Snd (Head' t) ~ 'ICov j, (i == j) ~ 'False)- => Dict (Tail' (ContractR r) ~ ContractR t)+ axiom :: (t ~ TailR r, t' ~ TailR t, (Fst (HeadR r) == Fst (HeadR t)) ~ 'True,+ Snd (HeadR r) ~ 'ICon i, Snd (HeadR t) ~ 'ICov j, (i == j) ~ 'False)+ => Dict (TailR (ContractR r) ~ ContractR t) axiom = unsafeCoerce (Dict :: Dict (a ~ a)) -- |If the first two labels of a rank type can be contracted, the contracted rank type is equal@@ -256,12 +259,12 @@ {-# INLINE contractTailSameVSameIProof #-} contractTailSameVSameIProof :: forall (r :: Rank) (t :: Rank) (t' :: Rank) (i :: Symbol) (j :: Symbol). Sing r ->- (t ~ Tail' r, t' ~ Tail' t, (Fst (Head' r) == Fst (Head' t)) ~ 'True,- Snd (Head' r) ~ 'ICon i, Snd (Head' t) ~ 'ICov j, (i == j) ~ 'True)+ (t ~ TailR r, t' ~ TailR t, (Fst (HeadR r) == Fst (HeadR t)) ~ 'True,+ Snd (HeadR r) ~ 'ICon i, Snd (HeadR t) ~ 'ICov j, (i == j) ~ 'True) :- (ContractR t' ~ ContractR r) contractTailSameVSameIProof _ = Sub axiom where- axiom :: (t ~ Tail' r, t' ~ Tail' t, (Fst (Head' r) == Fst (Head' t)) ~ 'True,- Snd (Head' r) ~ 'ICon i, Snd (Head' t) ~ 'ICov j, (i == j) ~ 'True)+ axiom :: (t ~ TailR r, t' ~ TailR t, (Fst (HeadR r) == Fst (HeadR t)) ~ 'True,+ Snd (HeadR r) ~ 'ICon i, Snd (HeadR t) ~ 'ICov j, (i == j) ~ 'True) => Dict (ContractR t' ~ ContractR r) axiom = unsafeCoerce (Dict :: Dict (a ~ a))
src/Math/Tensor/Safe/TH.hs view
@@ -26,14 +26,13 @@ ----------------------------------------------------------------------------- {-| Module : Math.Tensor.Safe.TH-Description : Generalized rank lifted to the type level.+Description : Type families and singletons for generalized types. Copyright : (c) Nils Alex, 2020 License : MIT Maintainer : nils.alex@fau.de-Stability : experimental -Generalized rank lifted to the type level. For documentation see re-exports-in "Math.Tensor.Safe".+Type families and singletons for generalized types.+For documentation see re-exports in "Math.Tensor.Safe". -} ----------------------------------------------------------------------------- module Math.Tensor.Safe.TH where@@ -147,8 +146,8 @@ sane ((v, is):(v', is'):xs) = v < v' && isAscendingI is && sane ((v',is'):xs) - head' :: Ord s => GRank s n -> (VSpace s n, Ix s)- head' ((v, l):_) = (v, case l of+ headR :: Ord s => GRank s n -> (VSpace s n, Ix s)+ headR ((v, l):_) = (v, case l of ConCov (a :| _) (b :| _) -> case compare a b of LT -> ICon a@@ -156,10 +155,10 @@ GT -> ICov b Con (a :| _) -> ICon a Cov (a :| _) -> ICov a)- head' [] = error "head' of empty list"+ headR [] = error "headR of empty list" - tail' :: Ord s => GRank s n -> GRank s n- tail' ((v, l):ls) =+ tailR :: Ord s => GRank s n -> GRank s n+ tailR ((v, l):ls) = let l' = case l of ConCov (a :| []) (b :| []) -> case compare a b of@@ -193,7 +192,7 @@ in case l' of Just l'' -> (v, l''):ls Nothing -> ls- tail' [] = error "tail' of empty list"+ tailR [] = error "tailR of empty list" mergeR :: (Ord s, Ord n) => GRank s n -> GRank s n -> Maybe (GRank s n) mergeR [] ys = Just ys@@ -357,30 +356,30 @@ removeUntil i r = go i r where go i' r'- | snd (head' r') == i' = tail' r'- | otherwise = go i $ tail' r'+ | snd (headR r') == i' = tailR r'+ | otherwise = go i $ tailR r' - data TransList a = TransCon (NonEmpty a) (NonEmpty a) |+ data TransRule a = TransCon (NonEmpty a) (NonEmpty a) | TransCov (NonEmpty a) (NonEmpty a) deriving (Show, Eq) - saneTransList :: Ord a => TransList a -> Bool- saneTransList tl =+ saneTransRule :: Ord a => TransRule a -> Bool+ saneTransRule tl = case tl of TransCon sources targets -> isAscendingNE sources && sort targets == sources TransCov sources targets -> isAscendingNE sources && sort targets == sources - canTransposeMult :: (Ord s, Ord n) => VSpace s n -> TransList s -> GRank s n -> Bool+ canTransposeMult :: (Ord s, Ord n) => VSpace s n -> TransRule s -> GRank s n -> Bool canTransposeMult vs tl r = case transpositions vs tl r of Just _ -> True Nothing -> False - transpositions :: (Ord s, Ord n) => VSpace s n -> TransList s -> GRank s n -> Maybe [(N,N)]+ transpositions :: (Ord s, Ord n) => VSpace s n -> TransRule s -> GRank s n -> Maybe [(N,N)] transpositions _ _ [] = Nothing transpositions vs tl ((vs',il):r) =- case saneTransList tl of+ case saneTransRule tl of False -> Nothing True -> case compare vs vs' of@@ -451,10 +450,10 @@ zip' (_ :| []) (_ :| (_:_)) = Nothing zip' (y:|(y':ys')) (z:|(z':zs')) = ((y,z):) <$> zip' (y':|ys') (z':|zs') - type RelabelList s = NonEmpty (s,s)+ type RelabelRule s = NonEmpty (s,s) - saneRelabelList :: Ord a => NonEmpty (a,a) -> Bool- saneRelabelList xs = isAscendingNE xs &&+ saneRelabelRule :: Ord a => NonEmpty (a,a) -> Bool+ saneRelabelRule xs = isAscendingNE xs && isAscendingNE xs' where xs' = sort $ fmap (\(a,b) -> (b,a)) xs@@ -481,7 +480,7 @@ [] -> Just $ (x,x) :| [] x':xs' -> ((x,x) <|) <$> go ((source,target) :| ms) (x' :| xs') - relabelR :: (Ord s, Ord n) => VSpace s n -> RelabelList s -> GRank s n -> Maybe (GRank s n)+ relabelR :: (Ord s, Ord n) => VSpace s n -> RelabelRule s -> GRank s n -> Maybe (GRank s n) relabelR _ _ [] = Nothing relabelR vs rls ((vs',il):r) = case vs `compare` vs' of
src/Math/Tensor/Safe/Vector.hs view
@@ -11,7 +11,6 @@ Copyright : (c) Nils Alex, 2020 License : MIT Maintainer : nils.alex@fau.de-Stability : experimental Length-typed vector. -}