linearmap-category 0.4.2.0 → 0.4.3.0
raw patch · 6 files changed
+1660/−578 lines, 6 filesdep +th-abstraction
Dependencies added: th-abstraction
Files
- Math/LinearMap/Category.hs +7/−4
- Math/LinearMap/Category/Class.hs +1/−2
- Math/LinearMap/Category/Instances/Deriving.hs +1606/−541
- Math/VectorSpace/Docile.hs +1/−26
- linearmap-category.cabal +4/−2
- test/tasty/test.hs +41/−3
Math/LinearMap/Category.hs view
@@ -19,6 +19,7 @@ {-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE UnicodeSyntax #-} {-# LANGUAGE TupleSections #-}+{-# LANGUAGE TypeApplications #-} {-# LANGUAGE ConstraintKinds #-} {-# LANGUAGE ExplicitNamespaces #-} @@ -315,11 +316,13 @@ type Seminorm v = Norm v -- | @(m<>n|$|v)^2 ⩵ (m|$|v)^2 + (n|$|v)^2@-instance LSpace v => Semigroup (Norm v) where- Norm m <> Norm n = Norm $ m^+^n+instance ∀ v . LSpace v => Semigroup (Norm v) where+ Norm m <> Norm n = case dualSpaceWitness @v of+ DualSpaceWitness -> Norm $ m^+^n -- | @mempty|$|v ≡ 0@-instance LSpace v => Monoid (Seminorm v) where- mempty = Norm zeroV+instance ∀ v . LSpace v => Monoid (Seminorm v) where+ mempty = case dualSpaceWitness @v of+ DualSpaceWitness -> Norm zeroV mappend = (<>) -- | A multidimensional variance of points @v@ with some distribution can be
Math/LinearMap/Category/Class.hs view
@@ -365,8 +365,7 @@ -- 'LinearSpace', but makes the condition explicit that the scalar and dual vectors -- also form a linear space. 'LinearSpace' only stores that constraint in -- 'dualSpaceWitness' (to avoid UndecidableSuperclasses).-type LSpace v = ( LinearSpace v, LinearSpace (Scalar v), LinearSpace (DualVector v)- , Num' (Scalar v) )+type LSpace v = ( LinearSpace v, Num' (Scalar v) ) instance (LinearSpace v, TensorSpace w, Scalar v~s, Scalar w~s) => AdditiveGroup (LinearMap s v w) where
Math/LinearMap/Category/Instances/Deriving.hs view
@@ -25,545 +25,1610 @@ {-# LANGUAGE TemplateHaskell #-} {-# LANGUAGE CPP #-} {-# LANGUAGE TupleSections #-}--module Math.LinearMap.Category.Instances.Deriving- ( makeLinearSpaceFromBasis, makeFiniteDimensionalFromBasis- -- * The instantiated classes- , AffineSpace(..), Semimanifold(..), PseudoAffine(..)- , TensorSpace(..), LinearSpace(..), FiniteDimensional(..), SemiInner(..)- -- * Internals- , BasisGeneratedSpace(..), LinearSpaceFromBasisDerivationConfig, def ) where--import Math.LinearMap.Category.Class-import Math.VectorSpace.Docile--import Data.VectorSpace-import Data.AffineSpace-import Data.Basis-import qualified Data.Map as Map-import Data.MemoTrie-import Data.Hashable--import Prelude ()-import qualified Prelude as Hask--import Control.Category.Constrained.Prelude-import Control.Arrow.Constrained--import Data.Coerce-import Data.Type.Coercion-import Data.Tagged-import Data.Traversable (traverse)-import Data.Default.Class--import Math.Manifold.Core.PseudoAffine-import Math.LinearMap.Asserted-import Math.VectorSpace.ZeroDimensional-import Data.VectorSpace.Free--import Language.Haskell.TH---- | Given a type @V@ that is already a 'VectorSpace' and 'HasBasis', generate--- the other class instances that are needed to use the type with this--- library.------ Prerequisites: (these can often be derived automatically,--- using either the @newtype@ \/ @via@ strategy or generics \/ anyclass)------ @--- instance 'AdditiveGroup' V------ instance 'VectorSpace' V where--- type Scalar V = -- a simple number type, usually 'Double'------ instance 'HasBasis' V where--- type Basis V = -- a type with an instance of 'HasTrie'--- @------ Note that the 'Basis' does /not/ need to be orthonormal – in fact it--- is not necessary to have a scalar product (i.e. an 'InnerSpace' instance)--- at all.------ This macro, invoked like--- @--- makeLinearSpaceFromBasis [t| V |]--- @------ will then generate @V@-instances for the classes 'Semimanifold',--- 'PseudoAffine', 'AffineSpace', 'TensorSpace' and 'LinearSpace'.-makeLinearSpaceFromBasis :: Q Type -> DecsQ-makeLinearSpaceFromBasis v- = makeLinearSpaceFromBasis' def $ deQuantifyType v--data LinearSpaceFromBasisDerivationConfig = LinearSpaceFromBasisDerivationConfig-instance Default LinearSpaceFromBasisDerivationConfig where- def = LinearSpaceFromBasisDerivationConfig---- | More general version of 'makeLinearSpaceFromBasis', that can be used with--- parameterised types.-makeLinearSpaceFromBasis' :: LinearSpaceFromBasisDerivationConfig- -> Q (Cxt, Type) -> DecsQ-makeLinearSpaceFromBasis' _ cxtv = do- (cxt,v) <- do- (cxt', v') <- cxtv- return (pure cxt', pure v')- - exts <- extsEnabled- if not $ all (`elem`exts) [TypeFamilies, ScopedTypeVariables, TypeApplications]- then reportError "This macro requires -XTypeFamilies, -XScopedTypeVariables and -XTypeApplications."- else pure ()- - sequence- [ InstanceD Nothing <$> cxt <*> [t|Semimanifold $v|] <*> [d|- type instance Needle $v = $v-#if !MIN_VERSION_manifolds_core(0,6,0)- type instance Interior $v = $v- $(varP 'toInterior) = pure- $(varP 'fromInterior) = id- $(varP 'translateP) = Tagged (^+^)- $(varP 'semimanifoldWitness) = SemimanifoldWitness BoundarylessWitness-#endif- $(varP '(.+~^)) = (^+^)- |]- , InstanceD Nothing <$> cxt <*> [t|PseudoAffine $v|] <*> do- [d|- $(varP '(.-~!)) = (^-^)- $(varP '(.-~.)) = \p q -> pure (p^-^q)- |]- , InstanceD Nothing <$> cxt <*> [t|AffineSpace $v|] <*> [d|- type instance Diff $v = $v- $(varP '(.+^)) = (^+^)- $(varP '(.-.)) = (^-^)- |]- , InstanceD Nothing <$> cxt <*> [t|TensorSpace $v|] <*> [d|- type instance TensorProduct $v w = Basis $v :->: w- $(varP 'wellDefinedVector) = \v- -> if v==v then Just v else Nothing- $(varP 'wellDefinedTensor) = \(Tensor v)- -> fmap (const $ Tensor v) . traverse (wellDefinedVector . snd) $ enumerate v- $(varP 'zeroTensor) = Tensor . trie $ const zeroV- $(varP 'toFlatTensor) = LinearFunction $ Tensor . trie . decompose'- $(varP 'fromFlatTensor) = LinearFunction $ \(Tensor t)- -> recompose $ enumerate t- $(varP 'scalarSpaceWitness) = ScalarSpaceWitness- $(varP 'linearManifoldWitness) = LinearManifoldWitness-#if !MIN_VERSION_manifolds_core(0,6,0)- BoundarylessWitness-#endif- $(varP 'addTensors) = \(Tensor v) (Tensor w)- -> Tensor $ (^+^) <$> v <*> w- $(varP 'subtractTensors) = \(Tensor v) (Tensor w)- -> Tensor $ (^-^) <$> v <*> w- $(varP 'tensorProduct) = bilinearFunction- $ \v w -> Tensor . trie $ \bv -> decompose' v bv *^ w- $(varP 'transposeTensor) = LinearFunction $ \(Tensor t)- -> sumV [ (tensorProduct-+$>w)-+$>basisValue b- | (b,w) <- enumerate t ]- $(varP 'fmapTensor) = bilinearFunction- $ \(LinearFunction f) (Tensor t)- -> Tensor $ fmap f t- $(varP 'fzipTensorWith) = bilinearFunction- $ \(LinearFunction f) (Tensor tv, Tensor tw)- -> Tensor $ liftA2 (curry f) tv tw- $(varP 'coerceFmapTensorProduct) = \_ Coercion- -> error "Cannot yet coerce tensors defined from a `HasBasis` instance. This would require `RoleAnnotations` on `:->:`. Cf. https://gitlab.haskell.org/ghc/ghc/-/issues/8177"- |]- , InstanceD Nothing <$> cxt <*> [t|BasisGeneratedSpace $v|] <*> do- [d|- $(varP 'proveTensorProductIsTrie) = \φ -> φ- |]- , InstanceD Nothing <$> cxt <*> [t|LinearSpace $v|] <*> [d|- type instance DualVector $v = DualVectorFromBasis $v- $(varP 'dualSpaceWitness) = case closedScalarWitness @(Scalar $v) of- ClosedScalarWitness -> DualSpaceWitness- $(varP 'linearId) = LinearMap . trie $ basisValue- $(varP 'tensorId) = tid- where tid :: ∀ w . (LinearSpace w, Scalar w ~ Scalar $v)- => ($v⊗w) +> ($v⊗w)- tid = case dualSpaceWitness @w of- DualSpaceWitness -> LinearMap . trie $ Tensor . \i- -> getTensorProduct $- (fmapTensor @(DualVector w)- -+$>(LinearFunction $ \w -> Tensor . trie- $ (\j -> if i==j then w else zeroV)- :: $v⊗w))- -+$> case linearId @w of- LinearMap lw -> Tensor lw :: DualVector w⊗w- $(varP 'applyDualVector) = bilinearFunction- $ \(DualVectorFromBasis f) v- -> sum [decompose' f i * vi | (i,vi) <- decompose v]- $(varP 'applyLinear) = bilinearFunction- $ \(LinearMap f) v- -> sumV [vi *^ untrie f i | (i,vi) <- decompose v]- $(varP 'applyTensorFunctional) = atf- where atf :: ∀ u . (LinearSpace u, Scalar u ~ Scalar $v)- => Bilinear (DualVector ($v ⊗ u))- ($v ⊗ u) (Scalar $v)- atf = case dualSpaceWitness @u of- DualSpaceWitness -> bilinearFunction- $ \(LinearMap f) (Tensor t)- -> sum [ (applyDualVector-+$>fi)-+$>untrie t i- | (i, fi) <- enumerate f ]- $(varP 'applyTensorLinMap) = atlm- where atlm :: ∀ u w . ( LinearSpace u, TensorSpace w- , Scalar u ~ Scalar $v, Scalar w ~ Scalar $v )- => Bilinear (($v ⊗ u) +> w) ($v ⊗ u) w- atlm = case dualSpaceWitness @u of- DualSpaceWitness -> bilinearFunction- $ \(LinearMap f) (Tensor t)- -> sumV [ (applyLinear-+$>(LinearMap fi :: u+>w))- -+$> untrie t i- | (i, Tensor fi) <- enumerate f ]- $(varP 'useTupleLinearSpaceComponents) = \_ -> usingNonTupleTypeAsTupleError- - |]- ]--data FiniteDimensionalFromBasisDerivationConfig- = FiniteDimensionalFromBasisDerivationConfig-instance Default FiniteDimensionalFromBasisDerivationConfig where- def = FiniteDimensionalFromBasisDerivationConfig---- | Like 'makeLinearSpaceFromBasis', but additionally generate instances for--- 'FiniteDimensional' and 'SemiInner'.-makeFiniteDimensionalFromBasis :: Q Type -> DecsQ-makeFiniteDimensionalFromBasis v- = makeFiniteDimensionalFromBasis' def $ deQuantifyType v--makeFiniteDimensionalFromBasis' :: FiniteDimensionalFromBasisDerivationConfig- -> Q (Cxt, Type) -> DecsQ-makeFiniteDimensionalFromBasis' _ cxtv = do- generalInsts <- makeLinearSpaceFromBasis' def cxtv- (cxt,v) <- do- (cxt', v') <- cxtv- return (pure cxt', pure v')- vtnameHash <- abs . hash . show <$> v- - fdInsts <- sequence- [ InstanceD Nothing <$> cxt <*> [t|FiniteDimensional $v|] <*> do- - -- This is a hack. Ideally, @newName@ should generate globally unique names,- -- but it doesn't, so we append a hash of the vector space type.- -- Cf. https://gitlab.haskell.org/ghc/ghc/-/issues/13054- subBasisCstr <- newName $ "CompleteBasis"++show vtnameHash-- tySyns <- sequence [-#if MIN_VERSION_template_haskell(2,15,0)- DataInstD [] Nothing- <$> (AppT (ConT ''SubBasis) <$> v)- <*> pure Nothing- <*> pure [NormalC subBasisCstr []]- <*> pure []-#else- DataInstD [] ''SubBasis- <$> ((:[]) <$> v)- <*> pure Nothing- <*> pure [NormalC subBasisCstr []]- <*> pure []-#endif- ]- methods <- [d|- $(varP 'entireBasis) = $(conE subBasisCstr)- $(varP 'enumerateSubBasis) =- \ $(conP subBasisCstr []) -> basisValue . fst <$> enumerate (trie $ const ())- $(varP 'tensorEquality)- = \(Tensor t) (Tensor t') -> and [ti == untrie t' i | (i,ti) <- enumerate t]- $(varP 'decomposeLinMap) = dlm- where dlm :: ∀ w . ($v+>w)- -> (SubBasis $v, [w]->[w])- dlm (LinearMap f) = - ( $(conE subBasisCstr)- , (map snd (enumerate f) ++) )- $(varP 'decomposeLinMapWithin) = dlm- where dlm :: ∀ w . SubBasis $v- -> ($v+>w)- -> Either (SubBasis $v, [w]->[w])- ([w]->[w])- dlm $(conP subBasisCstr []) (LinearMap f) = - (Right (map snd (enumerate f) ++) )- $(varP 'recomposeSB) = rsb- where rsb :: SubBasis $v- -> [Scalar $v]- -> ($v, [Scalar $v])- rsb $(conP subBasisCstr []) cs = first recompose- $ zipWith' (,) (fst <$> enumerate (trie $ const ())) cs- $(varP 'recomposeSBTensor) = rsbt- where rsbt :: ∀ w . (FiniteDimensional w, Scalar w ~ Scalar $v)- => SubBasis $v -> SubBasis w- -> [Scalar $v]- -> ($v⊗w, [Scalar $v])- rsbt $(conP subBasisCstr []) sbw ws = - (first (\iws -> Tensor $ trie (Map.fromList iws Map.!))- $ zipConsumeWith' (\i cs' -> first (\c->(i,c))- $ recomposeSB sbw cs')- (fst <$> enumerate (trie $ const ())) ws)- $(varP 'recomposeLinMap) = rlm- where rlm :: ∀ w . SubBasis $v- -> [w]- -> ($v+>w, [w])- rlm $(conP subBasisCstr []) ws = - (first (\iws -> LinearMap $ trie (Map.fromList iws Map.!))- $ zipWith' (,) (fst <$> enumerate (trie $ const ())) ws)- $(varP 'recomposeContraLinMap) = rclm- where rclm :: ∀ w f . (LinearSpace w, Scalar w ~ Scalar $v, Hask.Functor f)- => (f (Scalar w) -> w) -> f (DualVectorFromBasis $v)- -> ($v+>w)- rclm f vs = - (LinearMap $ trie (\i -> f $ fmap (`decompose'`i) vs))- $(varP 'recomposeContraLinMapTensor) = rclm- where rclm :: ∀ u w f- . ( FiniteDimensional u, LinearSpace w- , Scalar u ~ Scalar $v, Scalar w ~ Scalar $v, Hask.Functor f- )- => (f (Scalar w) -> w) -> f ($v+>DualVector u)- -> (($v⊗u)+>w)- rclm f vus = case dualSpaceWitness @u of- DualSpaceWitness -> - (- (LinearMap $ trie- (\i -> case recomposeContraLinMap @u @w @f f- $ fmap (\(LinearMap vu) -> untrie vu (i :: Basis $v)) vus of- LinearMap wuff -> Tensor wuff :: DualVector u⊗w )))- $(varP 'uncanonicallyFromDual) = LinearFunction getDualVectorFromBasis- $(varP 'uncanonicallyToDual) = LinearFunction DualVectorFromBasis-- |]- return $ tySyns ++ methods- , InstanceD Nothing <$> cxt <*> [t|SemiInner $v|] <*> do- [d|- $(varP 'dualBasisCandidates)- = cartesianDualBasisCandidates- (enumerateSubBasis CompleteDualVBasis)- (\v -> map (abs . realToFrac . decompose' v . fst)- $ enumerate (trie $ const ()) )- |]- ]- return $ generalInsts ++ fdInsts---deQuantifyType :: Q Type -> Q (Cxt, Type)-deQuantifyType t = do- t' <- t- return $ case t' of- ForallT _ cxt instT -> (cxt, instT)- _ -> ([], t')---newtype DualVectorFromBasis v = DualVectorFromBasis { getDualVectorFromBasis :: v }- deriving newtype (Eq, AdditiveGroup, VectorSpace, HasBasis)--instance AdditiveGroup v => Semimanifold (DualVectorFromBasis v) where- type Needle (DualVectorFromBasis v) = DualVectorFromBasis v-#if !MIN_VERSION_manifolds_core(0,6,0)- type Interior (DualVectorFromBasis v) = DualVectorFromBasis v- toInterior = pure- fromInterior = id- translateP = Tagged (^+^)- semimanifoldWitness = SemimanifoldWitness BoundarylessWitness-#endif- (.+~^) = (^+^)--instance AdditiveGroup v => AffineSpace (DualVectorFromBasis v) where- type Diff (DualVectorFromBasis v) = DualVectorFromBasis v- (.+^) = (^+^)- (.-.) = (^-^)--instance AdditiveGroup v => PseudoAffine (DualVectorFromBasis v) where- (.-~!) = (^-^)- p.-~.q = pure (p^-^q)--instance ∀ v . ( HasBasis v, Num' (Scalar v)- , Scalar (Scalar v) ~ Scalar v- , HasTrie (Basis v)- , Eq v )- => TensorSpace (DualVectorFromBasis v) where- type TensorProduct (DualVectorFromBasis v) w = Basis v :->: w- wellDefinedVector v- | v==v = Just v- | otherwise = Nothing- wellDefinedTensor (Tensor v)- = fmap (const $ Tensor v) . traverse (wellDefinedVector . snd) $ enumerate v- zeroTensor = Tensor . trie $ const zeroV- toFlatTensor = LinearFunction $ Tensor . trie . decompose'- fromFlatTensor = LinearFunction $ \(Tensor t)- -> recompose $ enumerate t- scalarSpaceWitness = ScalarSpaceWitness- linearManifoldWitness = LinearManifoldWitness-#if !MIN_VERSION_manifolds_core(0,6,0)- BoundarylessWitness-#endif- addTensors (Tensor v) (Tensor w) = Tensor $ (^+^) <$> v <*> w- subtractTensors (Tensor v) (Tensor w) = Tensor $ (^-^) <$> v <*> w- tensorProduct = bilinearFunction- $ \v w -> Tensor . trie $ \bv -> decompose' v bv *^ w- transposeTensor = LinearFunction $ \(Tensor t)- -> sumV [ (tensorProduct-+$>w)-+$>basisValue b- | (b,w) <- enumerate t ]- fmapTensor = bilinearFunction- $ \(LinearFunction f) (Tensor t)- -> Tensor $ fmap f t- fzipTensorWith = bilinearFunction- $ \(LinearFunction f) (Tensor tv, Tensor tw)- -> Tensor $ liftA2 (curry f) tv tw- coerceFmapTensorProduct _ Coercion- = error "Cannot yet coerce tensors defined from a `HasBasis` instance. This would require `RoleAnnotations` on `:->:`. Cf. https://gitlab.haskell.org/ghc/ghc/-/issues/8177"----- | Do not manually instantiate this class. It is used internally--- by 'makeLinearSpaceFromBasis'.-class ( HasBasis v, Num' (Scalar v)- , LinearSpace v, DualVector v ~ DualVectorFromBasis v)- => BasisGeneratedSpace v where- proveTensorProductIsTrie- :: ∀ w φ . (TensorProduct v w ~ (Basis v :->: w) => φ) -> φ--instance ∀ v . ( BasisGeneratedSpace v- , Scalar (Scalar v) ~ Scalar v- , HasTrie (Basis v)- , Eq v, Eq (Basis v) )- => LinearSpace (DualVectorFromBasis v) where- type DualVector (DualVectorFromBasis v) = v- dualSpaceWitness = case closedScalarWitness @(Scalar v) of- ClosedScalarWitness -> DualSpaceWitness- linearId = proveTensorProductIsTrie @v @(DualVectorFromBasis v)- (LinearMap . trie $ DualVectorFromBasis . basisValue)- tensorId = tid- where tid :: ∀ w . (LinearSpace w, Scalar w ~ Scalar v)- => (DualVectorFromBasis v⊗w) +> (DualVectorFromBasis v⊗w)- tid = proveTensorProductIsTrie @v @(DualVector w⊗(DualVectorFromBasis v⊗w))- ( case dualSpaceWitness @w of- DualSpaceWitness -> LinearMap . trie $ Tensor . \i- -> getTensorProduct $- (fmapTensor @(DualVector w)- -+$>(LinearFunction $ \w -> Tensor . trie- $ (\j -> if i==j then w else zeroV)- :: DualVectorFromBasis v⊗w))- -+$> case linearId @w of- LinearMap lw -> Tensor lw :: DualVector w⊗w )- applyDualVector = proveTensorProductIsTrie @v @(DualVectorFromBasis v)- ( bilinearFunction $ \f (DualVectorFromBasis v)- -> sum [decompose' f i * vi | (i,vi) <- decompose v] )- applyLinear = ali- where ali :: ∀ w . (TensorSpace w, Scalar w~Scalar v)- => Bilinear (DualVectorFromBasis v +> w) (DualVectorFromBasis v) w- ali = proveTensorProductIsTrie @v @w ( bilinearFunction- $ \(LinearMap f) (DualVectorFromBasis v)- -> sumV [vi *^ untrie f i | (i,vi) <- decompose v] )- applyTensorFunctional = atf- where atf :: ∀ u . (LinearSpace u, Scalar u ~ Scalar v)- => Bilinear (DualVector (DualVectorFromBasis v ⊗ u))- (DualVectorFromBasis v ⊗ u) (Scalar v)- atf = proveTensorProductIsTrie @v @(DualVector u) (case dualSpaceWitness @u of- DualSpaceWitness -> bilinearFunction- $ \(LinearMap f) (Tensor t)- -> sum [ (applyDualVector-+$>fi)-+$>untrie t i- | (i, fi) <- enumerate f ]- )- applyTensorLinMap = atlm- where atlm :: ∀ u w . ( LinearSpace u, TensorSpace w- , Scalar u ~ Scalar v, Scalar w ~ Scalar v )- => Bilinear ((DualVectorFromBasis v ⊗ u) +> w)- (DualVectorFromBasis v ⊗ u) w- atlm = proveTensorProductIsTrie @v @(DualVector u⊗w) (- case dualSpaceWitness @u of- DualSpaceWitness -> bilinearFunction- $ \(LinearMap f) (Tensor t)- -> sumV [ (applyLinear-+$>(LinearMap fi :: u+>w))- -+$> untrie t i- | (i, Tensor fi) <- enumerate f ]- )- useTupleLinearSpaceComponents _ = usingNonTupleTypeAsTupleError---zipWith' :: (a -> b -> c) -> [a] -> [b] -> ([c], [b])-zipWith' _ _ [] = ([], [])-zipWith' _ [] ys = ([], ys)-zipWith' f (x:xs) (y:ys) = first (f x y :) $ zipWith' f xs ys--zipConsumeWith' :: (a -> [b] -> (c,[b])) -> [a] -> [b] -> ([c], [b])-zipConsumeWith' _ _ [] = ([], [])-zipConsumeWith' _ [] ys = ([], ys)-zipConsumeWith' f (x:xs) ys- = case f x ys of- (z, ys') -> first (z :) $ zipConsumeWith' f xs ys'--instance ∀ v . ( BasisGeneratedSpace v, FiniteDimensional v- , Scalar (Scalar v) ~ Scalar v- , HasTrie (Basis v), Ord (Basis v)- , Eq v, Eq (Basis v) )- => FiniteDimensional (DualVectorFromBasis v) where- data SubBasis (DualVectorFromBasis v) = CompleteDualVBasis- entireBasis = CompleteDualVBasis- enumerateSubBasis CompleteDualVBasis- = basisValue . fst <$> enumerate (trie $ const ())- tensorEquality (Tensor t) (Tensor t')- = and [ti == untrie t' i | (i,ti) <- enumerate t]- decomposeLinMap = dlm- where dlm :: ∀ w . (DualVectorFromBasis v+>w)- -> (SubBasis (DualVectorFromBasis v), [w]->[w])- dlm (LinearMap f) = proveTensorProductIsTrie @v @w- ( CompleteDualVBasis- , (map snd (enumerate f) ++) )- decomposeLinMapWithin = dlm- where dlm :: ∀ w . SubBasis (DualVectorFromBasis v)- -> (DualVectorFromBasis v+>w)- -> Either (SubBasis (DualVectorFromBasis v), [w]->[w])- ([w]->[w])- dlm CompleteDualVBasis (LinearMap f) = proveTensorProductIsTrie @v @w- (Right (map snd (enumerate f) ++) )- recomposeSB = rsb- where rsb :: SubBasis (DualVectorFromBasis v)- -> [Scalar v]- -> (DualVectorFromBasis v, [Scalar v])- rsb CompleteDualVBasis cs = first recompose- $ zipWith' (,) (fst <$> enumerate (trie $ const ())) cs- recomposeSBTensor = rsbt- where rsbt :: ∀ w . (FiniteDimensional w, Scalar w ~ Scalar v)- => SubBasis (DualVectorFromBasis v) -> SubBasis w- -> [Scalar v]- -> (DualVectorFromBasis v⊗w, [Scalar v])- rsbt CompleteDualVBasis sbw ws = proveTensorProductIsTrie @v @w- (first (\iws -> Tensor $ trie (Map.fromList iws Map.!))- $ zipConsumeWith' (\i cs' -> first (i,) $ recomposeSB sbw cs')- (fst <$> enumerate (trie $ const ())) ws)- recomposeLinMap = rlm- where rlm :: ∀ w . SubBasis (DualVectorFromBasis v)- -> [w]- -> (DualVectorFromBasis v+>w, [w])- rlm CompleteDualVBasis ws = proveTensorProductIsTrie @v @w- (first (\iws -> LinearMap $ trie (Map.fromList iws Map.!))- $ zipWith' (,) (fst <$> enumerate (trie $ const ())) ws)- recomposeContraLinMap = rclm- where rclm :: ∀ w f . (LinearSpace w, Scalar w ~ Scalar v, Hask.Functor f)- => (f (Scalar w) -> w) -> f v- -> (DualVectorFromBasis v+>w)- rclm f vs = proveTensorProductIsTrie @v @w- (LinearMap $ trie (\i -> f $ fmap (`decompose'`i) vs))- recomposeContraLinMapTensor = rclm- where rclm :: ∀ u w f- . ( FiniteDimensional u, LinearSpace w- , Scalar u ~ Scalar v, Scalar w ~ Scalar v, Hask.Functor f- )- => (f (Scalar w) -> w) -> f (DualVectorFromBasis v+>DualVector u)- -> ((DualVectorFromBasis v⊗u)+>w)- rclm f vus = case dualSpaceWitness @u of- DualSpaceWitness -> proveTensorProductIsTrie @v @(DualVector u)- (proveTensorProductIsTrie @v @(DualVector u⊗w)- (LinearMap $ trie- (\i -> case recomposeContraLinMap @u @w @f f- $ fmap (\(LinearMap vu) -> untrie vu (i :: Basis v)) vus of- LinearMap wuff -> Tensor wuff :: DualVector u⊗w )))- uncanonicallyFromDual = LinearFunction DualVectorFromBasis- uncanonicallyToDual = LinearFunction getDualVectorFromBasis---instance ∀ v . ( BasisGeneratedSpace v, FiniteDimensional v- , Real (Scalar v), Scalar (Scalar v) ~ Scalar v- , HasTrie (Basis v), Ord (Basis v)- , Eq v, Eq (Basis v) )- => SemiInner (DualVectorFromBasis v) where- dualBasisCandidates = cartesianDualBasisCandidates- (enumerateSubBasis entireBasis)- (\v -> map (abs . realToFrac . decompose' v . fst)- $ enumerate (trie $ const ()) )+{-# LANGUAGE LambdaCase #-}+{-# LANGUAGE PatternSynonyms #-}++module Math.LinearMap.Category.Instances.Deriving+ ( makeLinearSpaceFromBasis, makeFiniteDimensionalFromBasis+ , copyNewtypeInstances, pattern AbstractDualVector+ -- * The instantiated classes+ , AffineSpace(..), Semimanifold(..), PseudoAffine(..)+ , TensorSpace(..), LinearSpace(..), FiniteDimensional(..), SemiInner(..)+ -- * Internals+ , BasisGeneratedSpace(..), LinearSpaceFromBasisDerivationConfig, def+ ) where++import Math.LinearMap.Category.Class+import Math.LinearMap.Category.Instances+import Math.VectorSpace.Docile++import Data.VectorSpace+import Data.AffineSpace+import Data.Basis+import qualified Data.Map as Map+import Data.Tree (Forest)+import Data.MemoTrie+import Data.Hashable++import Prelude ()+import qualified Prelude as Hask++import Control.Category.Constrained.Prelude+import Control.Arrow.Constrained++import Data.Coerce+import Data.Type.Coercion+import Data.Tagged+import qualified Data.Kind as Kind+import Data.Traversable (traverse)+import Data.Default.Class++import Math.Manifold.Core.PseudoAffine+import Math.LinearMap.Asserted+import Math.VectorSpace.ZeroDimensional+import Data.VectorSpace.Free++import GHC.Generics (Generic)++import Language.Haskell.TH+import Language.Haskell.TH.Syntax (Name(..), OccName(..)+#if MIN_VERSION_template_haskell(2,17,0)+ , Specificity(..)+#endif+ )+import qualified Language.Haskell.TH.Datatype as D++-- | Given a type @V@ that is already a 'VectorSpace' and 'HasBasis', generate+-- the other class instances that are needed to use the type with this+-- library.+--+-- Prerequisites: (these can often be derived automatically,+-- using either the @newtype@ \/ @via@ strategy or generics \/ anyclass)+--+-- @+-- instance 'AdditiveGroup' V+--+-- instance 'VectorSpace' V where+-- type Scalar V = -- a simple number type, usually 'Double'+--+-- instance 'HasBasis' V where+-- type Basis V = -- a type with an instance of 'HasTrie'+-- @+--+-- Note that the 'Basis' does /not/ need to be orthonormal – in fact it+-- is not necessary to have a scalar product (i.e. an 'InnerSpace' instance)+-- at all.+--+-- The macro, invoked like+-- @+-- makeLinearSpaceFromBasis [t| V |]+-- @+--+-- will then generate @V@-instances for the classes 'Semimanifold',+-- 'PseudoAffine', 'AffineSpace', 'TensorSpace' and 'LinearSpace'.+--+-- It also works on parameterised types, in that case you need to use+-- universal-quantification syntax, e.g.+--+-- @+-- makeLinearSpaceFromBasis [t| ∀ n . (KnownNat n) => V n |]+-- @+makeLinearSpaceFromBasis :: Q Type -> DecsQ+makeLinearSpaceFromBasis v+ = makeLinearSpaceFromBasis' def $ deQuantifyType v++data LinearSpaceFromBasisDerivationConfig = LinearSpaceFromBasisDerivationConfig+instance Default LinearSpaceFromBasisDerivationConfig where+ def = LinearSpaceFromBasisDerivationConfig++-- | More general version of 'makeLinearSpaceFromBasis', that can be used with+-- parameterised types.+makeLinearSpaceFromBasis' :: LinearSpaceFromBasisDerivationConfig+ -> Q ([TyVarBndr+#if MIN_VERSION_template_haskell(2,17,0)+ Specificity+#endif+ ], Cxt, Type) -> DecsQ+makeLinearSpaceFromBasis' _ cxtv = do+ (cxt,v) <- do+ (_, cxt', v') <- cxtv+ return (pure cxt', pure v')+ + exts <- extsEnabled+ if not $ all (`elem`exts) [TypeFamilies, ScopedTypeVariables, TypeApplications]+ then reportError "This macro requires -XTypeFamilies, -XScopedTypeVariables and -XTypeApplications."+ else pure ()+ + sequence+ [ InstanceD Nothing <$> cxt <*> [t|Semimanifold $v|] <*> [d|+ type instance Needle $v = $v+#if !MIN_VERSION_manifolds_core(0,6,0)+ type instance Interior $v = $v+ $(varP 'toInterior) = pure+ $(varP 'fromInterior) = id+ $(varP 'translateP) = Tagged (^+^)+ $(varP 'semimanifoldWitness) = SemimanifoldWitness BoundarylessWitness+#endif+ $(varP '(.+~^)) = (^+^)+ |]+ , InstanceD Nothing <$> cxt <*> [t|PseudoAffine $v|] <*> do+ [d|+ $(varP '(.-~!)) = (^-^)+ $(varP '(.-~.)) = \p q -> pure (p^-^q)+ |]+ , InstanceD Nothing <$> cxt <*> [t|AffineSpace $v|] <*> [d|+ type instance Diff $v = $v+ $(varP '(.+^)) = (^+^)+ $(varP '(.-.)) = (^-^)+ |]+ , InstanceD Nothing <$> cxt <*> [t|TensorSpace $v|] <*> [d|+ type instance TensorProduct $v w = Basis $v :->: w+ $(varP 'wellDefinedVector) = \v+ -> if v==v then Just v else Nothing+ $(varP 'wellDefinedTensor) = \(Tensor v)+ -> fmap (const $ Tensor v) . traverse (wellDefinedVector . snd) $ enumerate v+ $(varP 'zeroTensor) = Tensor . trie $ const zeroV+ $(varP 'toFlatTensor) = LinearFunction $ Tensor . trie . decompose'+ $(varP 'fromFlatTensor) = LinearFunction $ \(Tensor t)+ -> recompose $ enumerate t+ $(varP 'scalarSpaceWitness) = ScalarSpaceWitness+ $(varP 'linearManifoldWitness) = LinearManifoldWitness+#if !MIN_VERSION_manifolds_core(0,6,0)+ BoundarylessWitness+#endif+ $(varP 'addTensors) = \(Tensor v) (Tensor w)+ -> Tensor $ (^+^) <$> v <*> w+ $(varP 'subtractTensors) = \(Tensor v) (Tensor w)+ -> Tensor $ (^-^) <$> v <*> w+ $(varP 'tensorProduct) = bilinearFunction+ $ \v w -> Tensor . trie $ \bv -> decompose' v bv *^ w+ $(varP 'transposeTensor) = LinearFunction $ \(Tensor t)+ -> sumV [ (tensorProduct-+$>w)-+$>basisValue b+ | (b,w) <- enumerate t ]+ $(varP 'fmapTensor) = bilinearFunction+ $ \(LinearFunction f) (Tensor t)+ -> Tensor $ fmap f t+ $(varP 'fzipTensorWith) = bilinearFunction+ $ \(LinearFunction f) (Tensor tv, Tensor tw)+ -> Tensor $ liftA2 (curry f) tv tw+ $(varP 'coerceFmapTensorProduct) = \_ Coercion+ -> error "Cannot yet coerce tensors defined from a `HasBasis` instance. This would require `RoleAnnotations` on `:->:`. Cf. https://gitlab.haskell.org/ghc/ghc/-/issues/8177"+ |]+ , InstanceD Nothing <$> cxt <*> [t|BasisGeneratedSpace $v|] <*> do+ [d|+ $(varP 'proveTensorProductIsTrie) = \φ -> φ+ |]+ , InstanceD Nothing <$> cxt <*> [t|LinearSpace $v|] <*> [d|+ type instance DualVector $v = DualVectorFromBasis $v+ $(varP 'dualSpaceWitness) = case closedScalarWitness @(Scalar $v) of+ ClosedScalarWitness -> DualSpaceWitness+ $(varP 'linearId) = LinearMap . trie $ basisValue+ $(varP 'tensorId) = tid+ where tid :: ∀ w . (LinearSpace w, Scalar w ~ Scalar $v)+ => ($v⊗w) +> ($v⊗w)+ tid = case dualSpaceWitness @w of+ DualSpaceWitness -> LinearMap . trie $ Tensor . \i+ -> getTensorProduct $+ (fmapTensor @(DualVector w)+ -+$>(LinearFunction $ \w -> Tensor . trie+ $ (\j -> if i==j then w else zeroV)+ :: $v⊗w))+ -+$> case linearId @w of+ LinearMap lw -> Tensor lw :: DualVector w⊗w+ $(varP 'applyDualVector) = bilinearFunction+ $ \(DualVectorFromBasis f) v+ -> sum [decompose' f i * vi | (i,vi) <- decompose v]+ $(varP 'applyLinear) = bilinearFunction+ $ \(LinearMap f) v+ -> sumV [vi *^ untrie f i | (i,vi) <- decompose v]+ $(varP 'applyTensorFunctional) = atf+ where atf :: ∀ u . (LinearSpace u, Scalar u ~ Scalar $v)+ => Bilinear (DualVector ($v ⊗ u))+ ($v ⊗ u) (Scalar $v)+ atf = case dualSpaceWitness @u of+ DualSpaceWitness -> bilinearFunction+ $ \(LinearMap f) (Tensor t)+ -> sum [ (applyDualVector-+$>fi)-+$>untrie t i+ | (i, fi) <- enumerate f ]+ $(varP 'applyTensorLinMap) = atlm+ where atlm :: ∀ u w . ( LinearSpace u, TensorSpace w+ , Scalar u ~ Scalar $v, Scalar w ~ Scalar $v )+ => Bilinear (($v ⊗ u) +> w) ($v ⊗ u) w+ atlm = case dualSpaceWitness @u of+ DualSpaceWitness -> bilinearFunction+ $ \(LinearMap f) (Tensor t)+ -> sumV [ (applyLinear-+$>(LinearMap fi :: u+>w))+ -+$> untrie t i+ | (i, Tensor fi) <- enumerate f ]+ $(varP 'useTupleLinearSpaceComponents) = \_ -> usingNonTupleTypeAsTupleError+ + |]+ ]++data FiniteDimensionalFromBasisDerivationConfig+ = FiniteDimensionalFromBasisDerivationConfig+instance Default FiniteDimensionalFromBasisDerivationConfig where+ def = FiniteDimensionalFromBasisDerivationConfig++-- | Like 'makeLinearSpaceFromBasis', but additionally generate instances for+-- 'FiniteDimensional' and 'SemiInner'.+makeFiniteDimensionalFromBasis :: Q Type -> DecsQ+makeFiniteDimensionalFromBasis v+ = makeFiniteDimensionalFromBasis' def $ deQuantifyType v++makeFiniteDimensionalFromBasis' :: FiniteDimensionalFromBasisDerivationConfig+ -> Q ([TyVarBndr+#if MIN_VERSION_template_haskell(2,17,0)+ Specificity+#endif+ ], Cxt, Type) -> DecsQ+makeFiniteDimensionalFromBasis' _ cxtv = do+ generalInsts <- makeLinearSpaceFromBasis' def cxtv+ (cxt,v) <- do+ (_, cxt', v') <- cxtv+ return (pure cxt', pure v')+ vtnameHash <- abs . hash . show <$> v+ + fdInsts <- sequence+ [ InstanceD Nothing <$> cxt <*> [t|FiniteDimensional $v|] <*> do+ + -- This is a hack. Ideally, @newName@ should generate globally unique names,+ -- but it doesn't, so we append a hash of the vector space type.+ -- Cf. https://gitlab.haskell.org/ghc/ghc/-/issues/13054+ subBasisCstr <- newName $ "CompleteBasis"++show vtnameHash++ tySyns <- sequence [+#if MIN_VERSION_template_haskell(2,15,0)+ DataInstD [] Nothing+ <$> (AppT (ConT ''SubBasis) <$> v)+ <*> pure Nothing+ <*> pure [NormalC subBasisCstr []]+ <*> pure []+#else+ DataInstD [] ''SubBasis+ <$> ((:[]) <$> v)+ <*> pure Nothing+ <*> pure [NormalC subBasisCstr []]+ <*> pure []+#endif+ ]+ methods <- [d|+ $(varP 'entireBasis) = $(conE subBasisCstr)+ $(varP 'enumerateSubBasis) =+ \ $(conP subBasisCstr []) -> basisValue . fst <$> enumerate (trie $ const ())+ $(varP 'tensorEquality)+ = \(Tensor t) (Tensor t') -> and [ti == untrie t' i | (i,ti) <- enumerate t]+ $(varP 'decomposeLinMap) = dlm+ where dlm :: ∀ w . ($v+>w)+ -> (SubBasis $v, [w]->[w])+ dlm (LinearMap f) = + ( $(conE subBasisCstr)+ , (map snd (enumerate f) ++) )+ $(varP 'decomposeLinMapWithin) = dlm+ where dlm :: ∀ w . SubBasis $v+ -> ($v+>w)+ -> Either (SubBasis $v, [w]->[w])+ ([w]->[w])+ dlm $(conP subBasisCstr []) (LinearMap f) = + (Right (map snd (enumerate f) ++) )+ $(varP 'recomposeSB) = rsb+ where rsb :: SubBasis $v+ -> [Scalar $v]+ -> ($v, [Scalar $v])+ rsb $(conP subBasisCstr []) cs = first recompose+ $ zipWith' (,) (fst <$> enumerate (trie $ const ())) cs+ $(varP 'recomposeSBTensor) = rsbt+ where rsbt :: ∀ w . (FiniteDimensional w, Scalar w ~ Scalar $v)+ => SubBasis $v -> SubBasis w+ -> [Scalar $v]+ -> ($v⊗w, [Scalar $v])+ rsbt $(conP subBasisCstr []) sbw ws = + (first (\iws -> Tensor $ trie (Map.fromList iws Map.!))+ $ zipConsumeWith' (\i cs' -> first (\c->(i,c))+ $ recomposeSB sbw cs')+ (fst <$> enumerate (trie $ const ())) ws)+ $(varP 'recomposeLinMap) = rlm+ where rlm :: ∀ w . SubBasis $v+ -> [w]+ -> ($v+>w, [w])+ rlm $(conP subBasisCstr []) ws = + (first (\iws -> LinearMap $ trie (Map.fromList iws Map.!))+ $ zipWith' (,) (fst <$> enumerate (trie $ const ())) ws)+ $(varP 'recomposeContraLinMap) = rclm+ where rclm :: ∀ w f . (LinearSpace w, Scalar w ~ Scalar $v, Hask.Functor f)+ => (f (Scalar w) -> w) -> f (DualVectorFromBasis $v)+ -> ($v+>w)+ rclm f vs = + (LinearMap $ trie (\i -> f $ fmap (`decompose'`i) vs))+ $(varP 'recomposeContraLinMapTensor) = rclm+ where rclm :: ∀ u w f+ . ( FiniteDimensional u, LinearSpace w+ , Scalar u ~ Scalar $v, Scalar w ~ Scalar $v, Hask.Functor f+ )+ => (f (Scalar w) -> w) -> f ($v+>DualVector u)+ -> (($v⊗u)+>w)+ rclm f vus = case dualSpaceWitness @u of+ DualSpaceWitness -> + (+ (LinearMap $ trie+ (\i -> case recomposeContraLinMap @u @w @f f+ $ fmap (\(LinearMap vu) -> untrie vu (i :: Basis $v)) vus of+ LinearMap wuff -> Tensor wuff :: DualVector u⊗w )))+ $(varP 'uncanonicallyFromDual) = LinearFunction getDualVectorFromBasis+ $(varP 'uncanonicallyToDual) = LinearFunction DualVectorFromBasis++ |]+ return $ tySyns ++ methods+ , InstanceD Nothing <$> cxt <*> [t|SemiInner $v|] <*> do+ [d|+ $(varP 'dualBasisCandidates)+ = cartesianDualBasisCandidates+ (enumerateSubBasis CompleteDualVBasis)+ (\v -> map (abs . realToFrac . decompose' v . fst)+ $ enumerate (trie $ const ()) )+ |]+ ]+ return $ generalInsts ++ fdInsts+++deQuantifyType :: Q Type -> Q ([TyVarBndr+#if MIN_VERSION_template_haskell(2,17,0)+ Specificity+#endif+ ], Cxt, Type)+deQuantifyType t = do+ t' <- t+ return $ case t' of+ ForallT tvbs cxt instT -> (tvbs, cxt, instT)+ _ -> ([], [], t')+++newtype DualVectorFromBasis v = DualVectorFromBasis { getDualVectorFromBasis :: v }+ deriving newtype (Eq, AdditiveGroup, VectorSpace, HasBasis)++instance AdditiveGroup v => Semimanifold (DualVectorFromBasis v) where+ type Needle (DualVectorFromBasis v) = DualVectorFromBasis v+#if !MIN_VERSION_manifolds_core(0,6,0)+ type Interior (DualVectorFromBasis v) = DualVectorFromBasis v+ toInterior = pure+ fromInterior = id+ translateP = Tagged (^+^)+ semimanifoldWitness = SemimanifoldWitness BoundarylessWitness+#endif+ (.+~^) = (^+^)++instance AdditiveGroup v => AffineSpace (DualVectorFromBasis v) where+ type Diff (DualVectorFromBasis v) = DualVectorFromBasis v+ (.+^) = (^+^)+ (.-.) = (^-^)++instance AdditiveGroup v => PseudoAffine (DualVectorFromBasis v) where+ (.-~!) = (^-^)+ p.-~.q = pure (p^-^q)++instance ∀ v . ( HasBasis v, Num' (Scalar v)+ , Scalar (Scalar v) ~ Scalar v+ , HasTrie (Basis v)+ , Eq v )+ => TensorSpace (DualVectorFromBasis v) where+ type TensorProduct (DualVectorFromBasis v) w = Basis v :->: w+ wellDefinedVector v+ | v==v = Just v+ | otherwise = Nothing+ wellDefinedTensor (Tensor v)+ = fmap (const $ Tensor v) . traverse (wellDefinedVector . snd) $ enumerate v+ zeroTensor = Tensor . trie $ const zeroV+ toFlatTensor = LinearFunction $ Tensor . trie . decompose'+ fromFlatTensor = LinearFunction $ \(Tensor t)+ -> recompose $ enumerate t+ scalarSpaceWitness = ScalarSpaceWitness+ linearManifoldWitness = LinearManifoldWitness+#if !MIN_VERSION_manifolds_core(0,6,0)+ BoundarylessWitness+#endif+ addTensors (Tensor v) (Tensor w) = Tensor $ (^+^) <$> v <*> w+ subtractTensors (Tensor v) (Tensor w) = Tensor $ (^-^) <$> v <*> w+ tensorProduct = bilinearFunction+ $ \v w -> Tensor . trie $ \bv -> decompose' v bv *^ w+ transposeTensor = LinearFunction $ \(Tensor t)+ -> sumV [ (tensorProduct-+$>w)-+$>basisValue b+ | (b,w) <- enumerate t ]+ fmapTensor = bilinearFunction+ $ \(LinearFunction f) (Tensor t)+ -> Tensor $ fmap f t+ fzipTensorWith = bilinearFunction+ $ \(LinearFunction f) (Tensor tv, Tensor tw)+ -> Tensor $ liftA2 (curry f) tv tw+ coerceFmapTensorProduct _ Coercion+ = error "Cannot yet coerce tensors defined from a `HasBasis` instance. This would require `RoleAnnotations` on `:->:`. Cf. https://gitlab.haskell.org/ghc/ghc/-/issues/8177"+++-- | Do not manually instantiate this class. It is used internally+-- by 'makeLinearSpaceFromBasis'.+class ( HasBasis v, Num' (Scalar v)+ , LinearSpace v, DualVector v ~ DualVectorFromBasis v)+ => BasisGeneratedSpace v where+ proveTensorProductIsTrie+ :: ∀ w φ . (TensorProduct v w ~ (Basis v :->: w) => φ) -> φ++instance ∀ v . ( BasisGeneratedSpace v+ , Scalar (Scalar v) ~ Scalar v+ , HasTrie (Basis v)+ , Eq v, Eq (Basis v) )+ => LinearSpace (DualVectorFromBasis v) where+ type DualVector (DualVectorFromBasis v) = v+ dualSpaceWitness = case closedScalarWitness @(Scalar v) of+ ClosedScalarWitness -> DualSpaceWitness+ linearId = proveTensorProductIsTrie @v @(DualVectorFromBasis v)+ (LinearMap . trie $ DualVectorFromBasis . basisValue)+ tensorId = tid+ where tid :: ∀ w . (LinearSpace w, Scalar w ~ Scalar v)+ => (DualVectorFromBasis v⊗w) +> (DualVectorFromBasis v⊗w)+ tid = proveTensorProductIsTrie @v @(DualVector w⊗(DualVectorFromBasis v⊗w))+ ( case dualSpaceWitness @w of+ DualSpaceWitness -> LinearMap . trie $ Tensor . \i+ -> getTensorProduct $+ (fmapTensor @(DualVector w)+ -+$>(LinearFunction $ \w -> Tensor . trie+ $ (\j -> if i==j then w else zeroV)+ :: DualVectorFromBasis v⊗w))+ -+$> case linearId @w of+ LinearMap lw -> Tensor lw :: DualVector w⊗w )+ applyDualVector = proveTensorProductIsTrie @v @(DualVectorFromBasis v)+ ( bilinearFunction $ \f (DualVectorFromBasis v)+ -> sum [decompose' f i * vi | (i,vi) <- decompose v] )+ applyLinear = ali+ where ali :: ∀ w . (TensorSpace w, Scalar w~Scalar v)+ => Bilinear (DualVectorFromBasis v +> w) (DualVectorFromBasis v) w+ ali = proveTensorProductIsTrie @v @w ( bilinearFunction+ $ \(LinearMap f) (DualVectorFromBasis v)+ -> sumV [vi *^ untrie f i | (i,vi) <- decompose v] )+ applyTensorFunctional = atf+ where atf :: ∀ u . (LinearSpace u, Scalar u ~ Scalar v)+ => Bilinear (DualVector (DualVectorFromBasis v ⊗ u))+ (DualVectorFromBasis v ⊗ u) (Scalar v)+ atf = proveTensorProductIsTrie @v @(DualVector u) (case dualSpaceWitness @u of+ DualSpaceWitness -> bilinearFunction+ $ \(LinearMap f) (Tensor t)+ -> sum [ (applyDualVector-+$>fi)-+$>untrie t i+ | (i, fi) <- enumerate f ]+ )+ applyTensorLinMap = atlm+ where atlm :: ∀ u w . ( LinearSpace u, TensorSpace w+ , Scalar u ~ Scalar v, Scalar w ~ Scalar v )+ => Bilinear ((DualVectorFromBasis v ⊗ u) +> w)+ (DualVectorFromBasis v ⊗ u) w+ atlm = proveTensorProductIsTrie @v @(DualVector u⊗w) (+ case dualSpaceWitness @u of+ DualSpaceWitness -> bilinearFunction+ $ \(LinearMap f) (Tensor t)+ -> sumV [ (applyLinear-+$>(LinearMap fi :: u+>w))+ -+$> untrie t i+ | (i, Tensor fi) <- enumerate f ]+ )+ useTupleLinearSpaceComponents _ = usingNonTupleTypeAsTupleError+++zipWith' :: (a -> b -> c) -> [a] -> [b] -> ([c], [b])+zipWith' _ _ [] = ([], [])+zipWith' _ [] ys = ([], ys)+zipWith' f (x:xs) (y:ys) = first (f x y :) $ zipWith' f xs ys++zipConsumeWith' :: (a -> [b] -> (c,[b])) -> [a] -> [b] -> ([c], [b])+zipConsumeWith' _ _ [] = ([], [])+zipConsumeWith' _ [] ys = ([], ys)+zipConsumeWith' f (x:xs) ys+ = case f x ys of+ (z, ys') -> first (z :) $ zipConsumeWith' f xs ys'++instance ∀ v . ( BasisGeneratedSpace v, FiniteDimensional v+ , Scalar (Scalar v) ~ Scalar v+ , HasTrie (Basis v), Ord (Basis v)+ , Eq v, Eq (Basis v) )+ => FiniteDimensional (DualVectorFromBasis v) where+ data SubBasis (DualVectorFromBasis v) = CompleteDualVBasis+ entireBasis = CompleteDualVBasis+ enumerateSubBasis CompleteDualVBasis+ = basisValue . fst <$> enumerate (trie $ const ())+ tensorEquality (Tensor t) (Tensor t')+ = and [ti == untrie t' i | (i,ti) <- enumerate t]+ decomposeLinMap = dlm+ where dlm :: ∀ w . (DualVectorFromBasis v+>w)+ -> (SubBasis (DualVectorFromBasis v), [w]->[w])+ dlm (LinearMap f) = proveTensorProductIsTrie @v @w+ ( CompleteDualVBasis+ , (map snd (enumerate f) ++) )+ decomposeLinMapWithin = dlm+ where dlm :: ∀ w . SubBasis (DualVectorFromBasis v)+ -> (DualVectorFromBasis v+>w)+ -> Either (SubBasis (DualVectorFromBasis v), [w]->[w])+ ([w]->[w])+ dlm CompleteDualVBasis (LinearMap f) = proveTensorProductIsTrie @v @w+ (Right (map snd (enumerate f) ++) )+ recomposeSB = rsb+ where rsb :: SubBasis (DualVectorFromBasis v)+ -> [Scalar v]+ -> (DualVectorFromBasis v, [Scalar v])+ rsb CompleteDualVBasis cs = first recompose+ $ zipWith' (,) (fst <$> enumerate (trie $ const ())) cs+ recomposeSBTensor = rsbt+ where rsbt :: ∀ w . (FiniteDimensional w, Scalar w ~ Scalar v)+ => SubBasis (DualVectorFromBasis v) -> SubBasis w+ -> [Scalar v]+ -> (DualVectorFromBasis v⊗w, [Scalar v])+ rsbt CompleteDualVBasis sbw ws = proveTensorProductIsTrie @v @w+ (first (\iws -> Tensor $ trie (Map.fromList iws Map.!))+ $ zipConsumeWith' (\i cs' -> first (i,) $ recomposeSB sbw cs')+ (fst <$> enumerate (trie $ const ())) ws)+ recomposeLinMap = rlm+ where rlm :: ∀ w . SubBasis (DualVectorFromBasis v)+ -> [w]+ -> (DualVectorFromBasis v+>w, [w])+ rlm CompleteDualVBasis ws = proveTensorProductIsTrie @v @w+ (first (\iws -> LinearMap $ trie (Map.fromList iws Map.!))+ $ zipWith' (,) (fst <$> enumerate (trie $ const ())) ws)+ recomposeContraLinMap = rclm+ where rclm :: ∀ w f . (LinearSpace w, Scalar w ~ Scalar v, Hask.Functor f)+ => (f (Scalar w) -> w) -> f v+ -> (DualVectorFromBasis v+>w)+ rclm f vs = proveTensorProductIsTrie @v @w+ (LinearMap $ trie (\i -> f $ fmap (`decompose'`i) vs))+ recomposeContraLinMapTensor = rclm+ where rclm :: ∀ u w f+ . ( FiniteDimensional u, LinearSpace w+ , Scalar u ~ Scalar v, Scalar w ~ Scalar v, Hask.Functor f+ )+ => (f (Scalar w) -> w) -> f (DualVectorFromBasis v+>DualVector u)+ -> ((DualVectorFromBasis v⊗u)+>w)+ rclm f vus = case dualSpaceWitness @u of+ DualSpaceWitness -> proveTensorProductIsTrie @v @(DualVector u)+ (proveTensorProductIsTrie @v @(DualVector u⊗w)+ (LinearMap $ trie+ (\i -> case recomposeContraLinMap @u @w @f f+ $ fmap (\(LinearMap vu) -> untrie vu (i :: Basis v)) vus of+ LinearMap wuff -> Tensor wuff :: DualVector u⊗w )))+ uncanonicallyFromDual = LinearFunction DualVectorFromBasis+ uncanonicallyToDual = LinearFunction getDualVectorFromBasis+++instance ∀ v . ( BasisGeneratedSpace v, FiniteDimensional v+ , Real (Scalar v), Scalar (Scalar v) ~ Scalar v+ , HasTrie (Basis v), Ord (Basis v)+ , Eq v, Eq (Basis v) )+ => SemiInner (DualVectorFromBasis v) where+ dualBasisCandidates = cartesianDualBasisCandidates+ (enumerateSubBasis entireBasis)+ (\v -> map (abs . realToFrac . decompose' v . fst)+ $ enumerate (trie $ const ()) )+++newtype AbstractDualVector a c+ = AbstractDualVector_ { getConcreteDualVector :: DualVector c }+deriving newtype instance (Eq (DualVector c)) => Eq (AbstractDualVector a c)++class ( Coercible v (VectorSpaceImplementation v)+ , AdditiveGroup (VectorSpaceImplementation v) )+ => AbstractAdditiveGroup v where+ type VectorSpaceImplementation v :: Kind.Type++class (AbstractAdditiveGroup v, VectorSpace (VectorSpaceImplementation v))+ => AbstractVectorSpace v where+ scalarsSameInAbstraction+ :: ( Scalar (VectorSpaceImplementation v) ~ Scalar v+ => ρ ) -> ρ++class ( AbstractVectorSpace v, TensorSpace (VectorSpaceImplementation v)+#if !MIN_VERSION_manifolds_core(0,6,0)+ , Semimanifold v, Interior v ~ v+#endif+ ) => AbstractTensorSpace v where+ abstractTensorProductsCoercion+ :: Coercion (TensorProduct v w)+ (TensorProduct (VectorSpaceImplementation v) w)++class ( AbstractTensorSpace v, LinearSpace (VectorSpaceImplementation v)+ , DualVector v+ ~ AbstractDualVector v (VectorSpaceImplementation v) )+ => AbstractLinearSpace v++scalarsSameInAbstractionAndDuals :: ∀ v ρ . AbstractLinearSpace v+ => ( ( Scalar (VectorSpaceImplementation v) ~ Scalar v+ , Scalar (DualVector v) ~ Scalar v+ , Scalar (DualVector (VectorSpaceImplementation v)) ~ Scalar v )+ => ρ ) -> ρ+scalarsSameInAbstractionAndDuals φ+ = case dualSpaceWitness @(VectorSpaceImplementation v) of+ DualSpaceWitness -> scalarsSameInAbstraction @v φ++abstractDualVectorCoercion :: ∀ a+ . Coercion (AbstractDualVector a (VectorSpaceImplementation a))+ (DualVector (VectorSpaceImplementation a))+abstractDualVectorCoercion = Coercion++abstractTensorsCoercion :: ∀ a c w+ . ( AbstractVectorSpace a, LinearSpace c+ , c ~ VectorSpaceImplementation a, TensorSpace w )+ => Coercion (AbstractDualVector a c⊗w) (DualVector c⊗w)+abstractTensorsCoercion = Coercion++abstractLinmapCoercion :: ∀ a c w+ . ( AbstractLinearSpace a, LinearSpace c+ , c ~ VectorSpaceImplementation a, TensorSpace w )+ => Coercion (AbstractDualVector a c+>w) (DualVector c+>w)+abstractLinmapCoercion = case ( dualSpaceWitness @c+ , abstractTensorProductsCoercion @a @w ) of+ (DualSpaceWitness, Coercion) -> Coercion++coerceLinearMapCodomain :: ∀ v w x . ( LinearSpace v, Coercible w x )+ => (v+>w) -> (v+>x)+coerceLinearMapCodomain = case dualSpaceWitness @v of+ DualSpaceWitness -> \(LinearMap m)+ -> LinearMap $ (coerceFmapTensorProduct ([]::[DualVector v])+ (Coercion :: Coercion w x) $ m)++instance (Show (DualVector c)) => Show (AbstractDualVector a c) where+ showsPrec p (AbstractDualVector_ φ) = showParen (p>10)+ $ ("AbstractDualVector "++) . showsPrec 11 φ++instance ∀ a c . ( AbstractLinearSpace a, VectorSpaceImplementation a ~ c+ , AdditiveGroup (DualVector c) )+ => AdditiveGroup (AbstractDualVector a c) where+ zeroV = AbstractDualVector zeroV+ (^+^) = coerce ((^+^) @(DualVector c))+ negateV = coerce (negateV @(DualVector c))++instance ∀ a c . (AbstractLinearSpace a, VectorSpaceImplementation a ~ c+ , AdditiveGroup (DualVector c))+ => AffineSpace (AbstractDualVector a c) where+ type Diff (AbstractDualVector a c) = AbstractDualVector a c+ (.+^) = coerce ((^+^) @(DualVector c))+ (.-.) = coerce ((^-^) @(DualVector c))++instance ∀ a c . ( AbstractLinearSpace a, VectorSpaceImplementation a ~ c+ , AdditiveGroup (DualVector c) )+ => Semimanifold (AbstractDualVector a c) where+ type Needle (AbstractDualVector a c) = AbstractDualVector a c+ (.+~^) = (^+^)+#if !MIN_VERSION_manifolds_core(0,6,0)+ type instance Interior (AbstractDualVector a c) = AbstractDualVector a c+ toInterior = pure+ fromInterior = id+ translateP = Tagged (^+^)+ semimanifoldWitness = SemimanifoldWitness BoundarylessWitness+#endif++instance ∀ a c . ( AbstractLinearSpace a, VectorSpaceImplementation a ~ c+ , AdditiveGroup (DualVector c) )+ => PseudoAffine (AbstractDualVector a c) where+ v.-~.w = pure (v^-^w)+ (.-~!) = (^-^)++instance ∀ a c . ( AbstractLinearSpace a, VectorSpaceImplementation a ~ c+ , VectorSpace (DualVector c) )+ => VectorSpace (AbstractDualVector a c) where+ type Scalar (AbstractDualVector a c) = Scalar a+ (*^) = scalarsSameInAbstractionAndDuals @a (coerce ((*^) @(DualVector c)))++instance ∀ a c . ( AbstractLinearSpace a, VectorSpaceImplementation a ~ c+ , TensorSpace (DualVector c) )+ => TensorSpace (AbstractDualVector a c) where+ type TensorProduct (AbstractDualVector a c) w+ = TensorProduct (DualVector c) w+ scalarSpaceWitness = scalarsSameInAbstractionAndDuals @a+ (case scalarSpaceWitness @(DualVector c) of ScalarSpaceWitness -> ScalarSpaceWitness)+ linearManifoldWitness = scalarsSameInAbstractionAndDuals @a+ (case linearManifoldWitness @(DualVector c) of+#if MIN_VERSION_manifolds_core(0,6,0)+ LinearManifoldWitness -> LinearManifoldWitness+#else+ LinearManifoldWitness BoundarylessWitness+ -> LinearManifoldWitness BoundarylessWitness+#endif+ )+ zeroTensor = zt+ where zt :: ∀ w . (TensorSpace w, Scalar w ~ Scalar a)+ => (AbstractDualVector a c ⊗ w)+ zt = scalarsSameInAbstractionAndDuals @a+ (coerce (zeroTensor @(DualVector c) @w))+ addTensors = at+ where at :: ∀ w . (TensorSpace w, Scalar w ~ Scalar a)+ => (AbstractDualVector a c ⊗ w) -> (AbstractDualVector a c ⊗ w)+ -> (AbstractDualVector a c ⊗ w)+ at = scalarsSameInAbstractionAndDuals @a+ (coerce (addTensors @(DualVector c) @w))+ subtractTensors = st+ where st :: ∀ w . (TensorSpace w, Scalar w ~ Scalar a)+ => (AbstractDualVector a c ⊗ w) -> (AbstractDualVector a c ⊗ w)+ -> (AbstractDualVector a c ⊗ w)+ st = scalarsSameInAbstractionAndDuals @a+ (coerce (subtractTensors @(DualVector c) @w))+ negateTensor = nt+ where nt :: ∀ w . (TensorSpace w, Scalar w ~ Scalar a)+ => (AbstractDualVector a c ⊗ w) -+> (AbstractDualVector a c ⊗ w)+ nt = scalarsSameInAbstractionAndDuals @a+ (coerce (negateTensor @(DualVector c) @w))+ scaleTensor = st+ where st :: ∀ w . (TensorSpace w, Scalar w ~ Scalar a)+ => Bilinear (Scalar a) (AbstractDualVector a c ⊗ w)+ (AbstractDualVector a c ⊗ w)+ st = scalarsSameInAbstractionAndDuals @a+ (coerce (scaleTensor @(DualVector c) @w))+ toFlatTensor = scalarsSameInAbstractionAndDuals @a+ ( coerce (toFlatTensor @(DualVector c)) )+ fromFlatTensor = scalarsSameInAbstractionAndDuals @a+ ( coerce (fromFlatTensor @(DualVector c)) )+ tensorProduct = tp+ where tp :: ∀ w . (TensorSpace w, Scalar w ~ Scalar a)+ => Bilinear (AbstractDualVector a c) w+ (AbstractDualVector a c ⊗ w)+ tp = scalarsSameInAbstractionAndDuals @a+ (coerce (tensorProduct @(DualVector c) @w))+ wellDefinedVector (AbstractDualVector v) = AbstractDualVector <$> wellDefinedVector v+ wellDefinedTensor = wdt+ where wdt :: ∀ w . (TensorSpace w, Scalar w ~ Scalar a)+ => (AbstractDualVector a c ⊗ w) -> Maybe (AbstractDualVector a c ⊗ w)+ wdt = scalarsSameInAbstractionAndDuals @a+ (coerce (wellDefinedTensor @(DualVector c) @w))+ transposeTensor = scalarsSameInAbstractionAndDuals @a tt+ where tt :: ∀ w . ( TensorSpace w, Scalar w ~ Scalar a+ , Scalar (DualVector c) ~ Scalar a )+ => (AbstractDualVector a c ⊗ w) -+> (w ⊗ AbstractDualVector a c)+ tt = case coerceFmapTensorProduct @w []+ (Coercion @(DualVector c) @(AbstractDualVector a c)) of+ Coercion -> coerce (transposeTensor @(DualVector c) @w)+ fmapTensor = ft+ where ft :: ∀ w x . ( TensorSpace w, Scalar w ~ Scalar a+ , TensorSpace x, Scalar x ~ Scalar a )+ => Bilinear (w-+>x) (AbstractDualVector a c ⊗ w) (AbstractDualVector a c ⊗ x) + ft = scalarsSameInAbstractionAndDuals @a+ (coerce $ fmapTensor @(DualVector c) @w @x)+ fzipTensorWith = ft+ where ft :: ∀ u w x . ( TensorSpace w, Scalar w ~ Scalar a+ , TensorSpace u, Scalar u ~ Scalar a+ , TensorSpace x, Scalar x ~ Scalar a )+ => Bilinear ((w,x)-+>u)+ (AbstractDualVector a c ⊗ w, AbstractDualVector a c ⊗ x)+ (AbstractDualVector a c ⊗ u) + ft = scalarsSameInAbstractionAndDuals @a+ (coerce $ fzipTensorWith @(DualVector c) @u @w @x)+ coerceFmapTensorProduct _ = coerceFmapTensorProduct ([]::[DualVector c])++witnessAbstractDualVectorTensorSpacyness+ :: ∀ a c r . ( AbstractLinearSpace a, VectorSpaceImplementation a ~ c+ , LinearSpace a, LinearSpace c+ , TensorSpace (DualVector c), Num (Scalar a) )+ => (( TensorSpace (AbstractDualVector a c)+ , LinearSpace (DualVector c)+ , Scalar (DualVector c) ~ Scalar a )+ => r) -> r+witnessAbstractDualVectorTensorSpacyness φ = case dualSpaceWitness @c of+ DualSpaceWitness -> scalarsSameInAbstraction @a φ++instance ∀ a c . ( AbstractLinearSpace a, VectorSpaceImplementation a ~ c+ , LinearSpace a, LinearSpace c+ , TensorSpace (DualVector c), Num (Scalar a) )+ => LinearSpace (AbstractDualVector a c) where+ type DualVector (AbstractDualVector a c) = a+ dualSpaceWitness = case (dualSpaceWitness @c, scalarSpaceWitness @c) of+ (DualSpaceWitness, ScalarSpaceWitness)+ -> scalarsSameInAbstraction @a DualSpaceWitness+ linearId = witnessAbstractDualVectorTensorSpacyness @a @c+ (sym (abstractLinmapCoercion @a)+ $ sampleLinearFunction @(DualVector c)+ -+$> linearFunction AbstractDualVector)+ tensorId = tid+ where tid :: ∀ w . (LinearSpace w, Scalar w ~ Scalar a)+ => (AbstractDualVector a c ⊗ w) +> (AbstractDualVector a c ⊗ w) + tid = case ( dualSpaceWitness @w, dualSpaceWitness @c ) of+ (DualSpaceWitness, DualSpaceWitness)+ -> witnessAbstractDualVectorTensorSpacyness @a (+ let LinearMap ida = linearId :: (DualVector c ⊗ w) +> (DualVector c ⊗ w)+ in LinearMap $ + sym (abstractTensorProductsCoercion @a+ @(DualVector w ⊗ (AbstractDualVector a c⊗w)) )+ . coerceFmapTensorProduct ([]::[c ⊗ DualVector w])+ (Coercion @(DualVector c ⊗ w) @(AbstractDualVector a c ⊗ w))+ $ ida )+ applyDualVector = scalarsSameInAbstraction @a ( bilinearFunction+ $ \v (AbstractDualVector d) -> (applyDualVector -+$> d)-+$>(coerce v::c) )+ applyLinear = witnessAbstractDualVectorTensorSpacyness @a ( LinearFunction+ $ \f -> (applyLinear -+$> abstractLinmapCoercion $ f) . LinearFunction coerce+ )+ applyTensorFunctional = atf+ where atf :: ∀ u . ( LinearSpace u, Scalar u ~ Scalar a )+ => Bilinear (DualVector (AbstractDualVector a c⊗u))+ (AbstractDualVector a c⊗u) (Scalar a)+ atf = case (scalarSpaceWitness @a, dualSpaceWitness @u) of+ (ScalarSpaceWitness, DualSpaceWitness)+ -> witnessAbstractDualVectorTensorSpacyness @a (+ LinearFunction $ \f+ -> (applyTensorFunctional @(DualVector c)+ -+$> abstractLinmapCoercion @a $ f)+ . LinearFunction (abstractTensorsCoercion @a $)+ )+ applyTensorLinMap = atlm+ where atlm :: ∀ u w . ( LinearSpace u, Scalar u ~ Scalar a+ , TensorSpace w, Scalar w ~ Scalar a )+ => Bilinear ((AbstractDualVector a c⊗u)+>w)+ (AbstractDualVector a c⊗u) w+ atlm = case (dualSpaceWitness @c, dualSpaceWitness @u) of+ (DualSpaceWitness, DualSpaceWitness)+ -> witnessAbstractDualVectorTensorSpacyness @a (+ LinearFunction $ \(LinearMap f) ->+ let f' = LinearMap (abstractTensorProductsCoercion+ @a @((Tensor (Scalar a) (DualVector u) w))+ $ coerce f) :: (DualVector c⊗u)+>w+ in (applyTensorLinMap @(DualVector c)-+$>f')+ . LinearFunction (abstractTensorsCoercion @a $)+ )+ useTupleLinearSpaceComponents = \_ -> usingNonTupleTypeAsTupleError++instance ∀ a c . ( AbstractLinearSpace a, VectorSpaceImplementation a ~ c+ , FiniteDimensional a, FiniteDimensional c+ , TensorSpace (DualVector c), Eq (DualVector c), Num (Scalar a) )+ => FiniteDimensional (AbstractDualVector a c) where+ newtype SubBasis (AbstractDualVector a c) = AbstractDualVectorSubBasis {+ getAbstractDualVectorSubBasis :: SubBasis (DualVector c) }+ dualFinitenessWitness = scalarsSameInAbstraction @a+ ( case (scalarSpaceWitness @a, dualSpaceWitness @a) of+ (ScalarSpaceWitness, DualSpaceWitness)+ -> DualFinitenessWitness DualSpaceWitness )+ entireBasis = case dualFinitenessWitness @c of+ DualFinitenessWitness _ -> coerce (entireBasis @(DualVector c))+ enumerateSubBasis = case dualFinitenessWitness @c of+ DualFinitenessWitness _ + -> coerce (enumerateSubBasis @(DualVector c))+ decomposeLinMap = scalarsSameInAbstraction @a dclm+ where dclm :: ∀ w . (LSpace w, Scalar w ~ Scalar c)+ => (AbstractDualVector a c +> w)+ -> (SubBasis (AbstractDualVector a c), DList w)+ dclm = case (dualFinitenessWitness @c, abstractTensorProductsCoercion @a @w) of+ (DualFinitenessWitness DualSpaceWitness, Coercion)+ -> coerce (decomposeLinMap @(DualVector c) @w)+ decomposeLinMapWithin = scalarsSameInAbstraction @a dclm+ where dclm :: ∀ w . (LSpace w, Scalar w ~ Scalar c)+ => SubBasis (AbstractDualVector a c) -> (AbstractDualVector a c +> w)+ -> Either (SubBasis (AbstractDualVector a c), DList w) (DList w)+ dclm = case (dualFinitenessWitness @c, abstractTensorProductsCoercion @a @w) of+ (DualFinitenessWitness DualSpaceWitness, Coercion)+ -> coerce (decomposeLinMapWithin @(DualVector c) @w)+ recomposeSB = case dualFinitenessWitness @c of+ DualFinitenessWitness DualSpaceWitness -> scalarsSameInAbstraction @a+ (coerce $ recomposeSB @(DualVector c))+ recomposeSBTensor = scalarsSameInAbstraction @a rst+ where rst :: ∀ w . (FiniteDimensional w, Scalar w ~ Scalar c)+ => SubBasis (AbstractDualVector a c) -> SubBasis w -> [Scalar c]+ -> (AbstractDualVector a c ⊗ w, [Scalar c])+ rst = case dualFinitenessWitness @c of+ DualFinitenessWitness DualSpaceWitness+ -> coerce (recomposeSBTensor @(DualVector c) @w)+ recomposeLinMap = scalarsSameInAbstraction @a rlm+ where rlm :: ∀ w . (LSpace w, Scalar w ~ Scalar c)+ => SubBasis (AbstractDualVector a c)+ -> [w] -> (AbstractDualVector a c +> w, [w])+ rlm = case (dualFinitenessWitness @c, abstractTensorProductsCoercion @a @w) of+ (DualFinitenessWitness DualSpaceWitness, Coercion)+ -> coerce (recomposeLinMap @(DualVector c) @w)+ recomposeContraLinMap = scalarsSameInAbstraction @a rclm+ where rclm :: ∀ f w . (LinearSpace w, Scalar w ~ Scalar c, Hask.Functor f)+ => (f (Scalar w) -> w) -> f a -> AbstractDualVector a c +> w+ rclm = case (dualFinitenessWitness @c, abstractTensorProductsCoercion @a @w) of+ (DualFinitenessWitness DualSpaceWitness, Coercion) -> \f ->+ (coerce $ recomposeContraLinMap @(DualVector c) @w @f) f+ . fmap (coerce :: a -> c)+ recomposeContraLinMapTensor = scalarsSameInAbstraction @a rclmt+ where rclmt :: ∀ f w u . ( LinearSpace w, Scalar w ~ Scalar c+ , FiniteDimensional u, Scalar u ~ Scalar c+ , Hask.Functor f )+ => (f (Scalar w) -> w) -> f (AbstractDualVector a c+>DualVector u)+ -> (AbstractDualVector a c⊗u) +> w+ rclmt = scalarsSameInAbstraction @a (case dualSpaceWitness @u of+ DualSpaceWitness ->+ case ( dualFinitenessWitness @c+ , abstractTensorProductsCoercion @a @(DualVector u)+ , abstractTensorProductsCoercion @a+ @(Tensor (Scalar a) (DualVector u) w) ) of+ (DualFinitenessWitness DualSpaceWitness, Coercion, Coercion) -> \f ->+ (coerce $ recomposeContraLinMapTensor @(DualVector c) @u @w @f) f+ . fmap (coerce :: (AbstractDualVector a c+>DualVector u)+ -> (DualVector c+>DualVector u))+ )+ uncanonicallyFromDual = case dualFinitenessWitness @c of+ DualFinitenessWitness DualSpaceWitness+ -> coerce (uncanonicallyFromDual @(DualVector c))+ uncanonicallyToDual = case dualFinitenessWitness @c of+ DualFinitenessWitness DualSpaceWitness+ -> coerce (uncanonicallyToDual @(DualVector c))+ tensorEquality = te+ where te :: ∀ w . (TensorSpace w, Eq w, Scalar w ~ Scalar a)+ => (AbstractDualVector a c ⊗ w) -> (AbstractDualVector a c ⊗ w) -> Bool+ te = case dualFinitenessWitness @c of+ DualFinitenessWitness _ -> scalarsSameInAbstractionAndDuals @a+ (coerce (tensorEquality @(DualVector c) @w))++instance ∀ a c . ( AbstractLinearSpace a, VectorSpaceImplementation a ~ c+ , SemiInner a, LinearSpace c, SemiInner (DualVector c)+ , TensorSpace (DualVector c), Eq (DualVector c), Num (Scalar a) )+ => SemiInner (AbstractDualVector a c) where+ dualBasisCandidates = case dualSpaceWitness @c of+ DualSpaceWitness -> coerce (dualBasisCandidates @(DualVector c))+ tensorDualBasisCandidates = scalarsSameInAbstraction @a tdbc+ where tdbc :: ∀ w . (SemiInner w, Scalar w ~ Scalar c)+ => [(Int, AbstractDualVector a c ⊗ w)]+ -> Forest (Int, AbstractDualVector a c +> DualVector w)+ tdbc = case (dualSpaceWitness @c, dualSpaceWitness @w) of+ (DualSpaceWitness, DualSpaceWitness)+ -> case abstractTensorProductsCoercion @a @(DualVector w) of+ Coercion -> coerce (tensorDualBasisCandidates @(DualVector c) @w)+ symTensorDualBasisCandidates = scalarsSameInAbstraction @a+ ( case ( coerceFmapTensorProduct @c [] (Coercion @a @c)+ . abstractTensorProductsCoercion @a @a+ , coerceFmapTensorProduct @(DualVector c) []+ (Coercion @(AbstractDualVector a c) @(DualVector c))+ , dualSpaceWitness @c ) of+ (Coercion, Coercion, DualSpaceWitness)+ -> coerce (symTensorDualBasisCandidates @(DualVector c))+ )++ ++pattern AbstractDualVector+ :: AbstractLinearSpace v => DualVector (VectorSpaceImplementation v) -> DualVector v+pattern AbstractDualVector φ = AbstractDualVector_ φ++++abstractVS_zeroV :: ∀ v .+ (AbstractAdditiveGroup v)+ => v+abstractVS_zeroV = coerce (zeroV @(VectorSpaceImplementation v))++abstractVS_addvs :: ∀ v .+ (AbstractAdditiveGroup v)+ => v -> v -> v+abstractVS_addvs = coerce ((^+^) @(VectorSpaceImplementation v))++abstractVS_subvs :: ∀ v .+ (AbstractAdditiveGroup v)+ => v -> v -> v+abstractVS_subvs = coerce ((^-^) @(VectorSpaceImplementation v))++abstractVS_negateV :: ∀ v .+ (AbstractAdditiveGroup v)+ => v -> v+abstractVS_negateV = coerce (negateV @(VectorSpaceImplementation v))++abstractVS_scalev :: ∀ v .+ (AbstractVectorSpace v)+ => Scalar v -> v -> v+abstractVS_scalev = scalarsSameInAbstraction @v+ ( coerce ((*^) @(VectorSpaceImplementation v)) )++abstractVS_innerProd :: ∀ v .+ (AbstractVectorSpace v, InnerSpace (VectorSpaceImplementation v))+ => v -> v -> Scalar v+abstractVS_innerProd = scalarsSameInAbstraction @v+ ( coerce ((<.>) @(VectorSpaceImplementation v)) )++abstractVS_scalarsSameInAbstraction :: ∀ v ρ .+ ( AbstractVectorSpace v+ , Scalar (VectorSpaceImplementation v) ~ Scalar v+ )+ => ( Scalar (VectorSpaceImplementation v) ~ Scalar v+ => ρ ) -> ρ+abstractVS_scalarsSameInAbstraction φ+ = φ++abstractVS_scalarSpaceWitness :: ∀ v .+ (AbstractTensorSpace v)+ => ScalarSpaceWitness v+abstractVS_scalarSpaceWitness+ = case scalarSpaceWitness @(VectorSpaceImplementation v) of+ ScalarSpaceWitness -> scalarsSameInAbstraction @v ScalarSpaceWitness ++abstractVS_linearManifoldWitness :: ∀ v .+ ( AbstractTensorSpace v, AffineSpace v, Needle v ~ v, Diff v ~ v+ )+ => LinearManifoldWitness v+abstractVS_linearManifoldWitness+ = case linearManifoldWitness @(VectorSpaceImplementation v) of+#if MIN_VERSION_manifolds_core(0,6,0)+ LinearManifoldWitness -> LinearManifoldWitness+#else+ LinearManifoldWitness BoundarylessWitness+ -> LinearManifoldWitness BoundarylessWitness+#endif++abstractVS_toFlatTensor :: ∀ v .+ ( AbstractTensorSpace v+ , Coercible (TensorProduct v (Scalar v))+ (TensorProduct (VectorSpaceImplementation v)+ (Scalar (VectorSpaceImplementation v))) )+ => v -+> (v ⊗ Scalar v)+abstractVS_toFlatTensor = coerce (toFlatTensor @(VectorSpaceImplementation v))++abstractVS_fromFlatTensor :: ∀ v .+ ( AbstractTensorSpace v+ , Coercible (TensorProduct v (Scalar v))+ (TensorProduct (VectorSpaceImplementation v)+ (Scalar (VectorSpaceImplementation v))) )+ => (v ⊗ Scalar v) -+> v+abstractVS_fromFlatTensor = coerce (fromFlatTensor @(VectorSpaceImplementation v))++abstractVS_zeroTensor :: ∀ v w+ . ( AbstractTensorSpace v+ , TensorSpace w, Scalar w ~ Scalar v+ , Coercible (TensorProduct v w)+ (TensorProduct (VectorSpaceImplementation v) w) )+ => (v ⊗ w)+abstractVS_zeroTensor = scalarsSameInAbstraction @v+ (coerce (zeroTensor @(VectorSpaceImplementation v) @w))++abstractVS_addTensors :: ∀ v w+ . ( AbstractTensorSpace v+ , TensorSpace w, Scalar w ~ Scalar v+ , Coercible (TensorProduct v w)+ (TensorProduct (VectorSpaceImplementation v) w) )+ => (v ⊗ w) -> (v ⊗ w) -> (v ⊗ w)+abstractVS_addTensors = scalarsSameInAbstraction @v+ (coerce (addTensors @(VectorSpaceImplementation v) @w))++abstractVS_subtractTensors :: ∀ v w+ . ( AbstractTensorSpace v+ , TensorSpace w, Scalar w ~ Scalar v+ , Coercible (TensorProduct v w)+ (TensorProduct (VectorSpaceImplementation v) w) )+ => (v ⊗ w) -> (v ⊗ w) -> (v ⊗ w)+abstractVS_subtractTensors = scalarsSameInAbstraction @v+ (coerce (subtractTensors @(VectorSpaceImplementation v) @w))++abstractVS_scaleTensor :: ∀ v w+ . ( AbstractTensorSpace v+ , TensorSpace w, Scalar w ~ Scalar v+ , Coercible (TensorProduct v w)+ (TensorProduct (VectorSpaceImplementation v) w) )+ => Bilinear (Scalar v) (v ⊗ w) (v ⊗ w)+abstractVS_scaleTensor = scalarsSameInAbstraction @v+ (coerce (scaleTensor @(VectorSpaceImplementation v) @w))++abstractVS_negateTensor :: ∀ v w+ . ( AbstractTensorSpace v+ , TensorSpace w, Scalar w ~ Scalar v+ , Coercible (TensorProduct v w)+ (TensorProduct (VectorSpaceImplementation v) w) )+ => (v ⊗ w) -+> (v ⊗ w)+abstractVS_negateTensor = scalarsSameInAbstraction @v+ (coerce (negateTensor @(VectorSpaceImplementation v) @w))++abstractVS_wellDefinedVector :: ∀ v+ . ( AbstractTensorSpace v+ ) => v -> Maybe v+abstractVS_wellDefinedVector = coerce (wellDefinedVector @(VectorSpaceImplementation v))++abstractVS_wellDefinedTensor :: ∀ v w+ . ( AbstractTensorSpace v+ , TensorSpace w, Scalar w ~ Scalar v+ ) => (v ⊗ w) -> Maybe (v ⊗ w)+abstractVS_wellDefinedTensor+ = scalarsSameInAbstraction @v+ (case abstractTensorProductsCoercion @v @w of+ Coercion -> coerce (wellDefinedTensor @(VectorSpaceImplementation v) @w))++abstractVS_tensorProduct :: ∀ v w . ( AbstractTensorSpace v+ , TensorSpace w, Scalar w ~ Scalar v+ ) => Bilinear v w (v ⊗ w)+abstractVS_tensorProduct = scalarsSameInAbstraction @v+ ( case ( abstractTensorProductsCoercion @v @w ) of+ Coercion -> coerce (tensorProduct @(VectorSpaceImplementation v) @w) )++abstractVS_transposeTensor :: ∀ v w . ( AbstractTensorSpace v+ , TensorSpace w, Scalar w ~ Scalar v+ ) => (v ⊗ w) -+> (w ⊗ v)+abstractVS_transposeTensor+ = scalarsSameInAbstraction @v ( case+ ( abstractTensorProductsCoercion @v @w+ , coerceFmapTensorProduct @w []+ (Coercion @(VectorSpaceImplementation v) @(v)) ) of+ (Coercion, Coercion) -> scalarsSameInAbstraction @v+ (coerce (transposeTensor @(VectorSpaceImplementation v) @w))+ )++abstractVS_fmapTensor :: ∀ v u w . ( AbstractTensorSpace v+ , TensorSpace u, Scalar u ~ Scalar v+ , TensorSpace w, Scalar w ~ Scalar v )+ => Bilinear (u -+> w) (v ⊗ u) (v ⊗ w)+abstractVS_fmapTensor+ = scalarsSameInAbstraction @v+ ( case ( abstractTensorProductsCoercion @v @u+ , abstractTensorProductsCoercion @v @w ) of+ (Coercion, Coercion)+ -> coerce (fmapTensor @(VectorSpaceImplementation v) @u @w) )++abstractVS_fzipTensorsWith :: ∀ v u w x . ( AbstractTensorSpace v+ , TensorSpace u, Scalar u ~ Scalar v+ , TensorSpace w, Scalar w ~ Scalar v+ , TensorSpace x, Scalar x ~ Scalar v )+ => Bilinear ((w, x) -+> u) (v ⊗ w, v ⊗ x) (v ⊗ u)+abstractVS_fzipTensorsWith = scalarsSameInAbstraction @v+ ( case ( abstractTensorProductsCoercion @v @u+ , abstractTensorProductsCoercion @v @w+ , abstractTensorProductsCoercion @v @x ) of+ (Coercion, Coercion, Coercion)+ -> coerce (fzipTensorWith @(VectorSpaceImplementation v) @u @w @x)+ )++abstractVS_coerceFmapTensorProduct :: ∀ v u w p .+ ( AbstractTensorSpace v+ ) => p v -> Coercion u w -> Coercion (TensorProduct v u) (TensorProduct v w)+abstractVS_coerceFmapTensorProduct _ crc+ = case ( abstractTensorProductsCoercion @v @u+ , abstractTensorProductsCoercion @v @w+ , coerceFmapTensorProduct @(VectorSpaceImplementation v) [] crc ) of+ (Coercion, Coercion, Coercion) -> Coercion++abstractVS_dualSpaceWitness :: ∀ v . (AbstractLinearSpace v+ , LinearSpace v+ , LinearSpace (VectorSpaceImplementation v))+ => DualSpaceWitness v+abstractVS_dualSpaceWitness+ = scalarsSameInAbstraction @v+ ( case dualSpaceWitness @(VectorSpaceImplementation v) of+ DualSpaceWitness -> DualSpaceWitness+ )++abstractVS_linearId :: ∀ v . ( AbstractLinearSpace v+ , LinearSpace (VectorSpaceImplementation v) )+ => v +> v+abstractVS_linearId = case dualSpaceWitness @(VectorSpaceImplementation v) of+ DualSpaceWitness -> case coerceFmapTensorProduct+ @(DualVector (VectorSpaceImplementation v)) []+ (Coercion @v @(VectorSpaceImplementation v)) of+ Coercion -> coerce (linearId @(VectorSpaceImplementation v))++abstractVS_tensorId :: ∀ v w . ( AbstractLinearSpace v+ , LinearSpace (VectorSpaceImplementation v)+ , LinearSpace w, Scalar w ~ Scalar v )+ => (v ⊗ w) +> (v ⊗ w) +abstractVS_tensorId = scalarsSameInAbstraction @v+ (case (dualSpaceWitness @w, dualSpaceWitness @(VectorSpaceImplementation v)) of+ (DualSpaceWitness, DualSpaceWitness)+ -> case coerceFmapTensorProduct @(DualVector w) []+ $ Coercion @(TensorProduct (VectorSpaceImplementation v) w)+ @(VectorSpaceImplementation v ⊗ w)+ . abstractTensorProductsCoercion @v @w+ . Coercion @(v ⊗ w) @(TensorProduct v w) of+ Coercion+ -> case ( coerceFmapTensorProduct + @(DualVector (VectorSpaceImplementation v)) []+ (Coercion :: Coercion+ (Tensor (Scalar v) (DualVector w) (Tensor (Scalar v) v w))+ (Tensor (Scalar v)+ (DualVector w)+ (Tensor (Scalar v)+ (VectorSpaceImplementation v) w)))+ ) of+ Coercion+ -> coerce (tensorId @(VectorSpaceImplementation v) @w)+ )++abstractVS_applyDualVector :: ∀ v . ( AbstractLinearSpace v+ , LinearSpace (VectorSpaceImplementation v) )+ => Bilinear (DualVector v) v (Scalar v)+abstractVS_applyDualVector = scalarsSameInAbstraction @v+ ( case dualSpaceWitness @(VectorSpaceImplementation v) of+ DualSpaceWitness -> coerce (applyDualVector @(VectorSpaceImplementation v)) )++abstractVS_applyLinear :: ∀ v w . ( AbstractLinearSpace v+ , LinearSpace (VectorSpaceImplementation v)+ , TensorSpace w, Scalar w ~ Scalar v )+ => Bilinear (v +> w) v w+abstractVS_applyLinear = scalarsSameInAbstraction @v+ ( coerce (applyLinear @(VectorSpaceImplementation v) @w)+ )++abstractVS_applyTensorFunctional :: ∀ v u .+ ( AbstractLinearSpace v+ , LinearSpace (VectorSpaceImplementation v)+ , LinearSpace u, Scalar u ~ Scalar v )+ => Bilinear (DualVector (v⊗u)) (v⊗u) (Scalar v)+abstractVS_applyTensorFunctional = scalarsSameInAbstraction @v+ (case abstractTensorProductsCoercion @v @u of+ Coercion -> coerce (applyTensorFunctional @(VectorSpaceImplementation v) @u))++abstractVS_applyTensorLinMap :: ∀ v u w .+ ( AbstractLinearSpace v+ , LinearSpace (VectorSpaceImplementation v)+ , LinearSpace u, Scalar u ~ Scalar v+ , TensorSpace w, Scalar w ~ Scalar v )+ => Bilinear ((v⊗u)+>w) (v⊗u) w+abstractVS_applyTensorLinMap = scalarsSameInAbstraction @v+ ( case abstractTensorProductsCoercion @v @u of+ Coercion -> coerce (applyTensorLinMap @(VectorSpaceImplementation v) @u @w) )++abstractSubbasisCoercion :: ∀ v .+ Coercible (SubBasis v) (SubBasis (VectorSpaceImplementation v))+ => Coercion (SubBasis v) (SubBasis (VectorSpaceImplementation v))+abstractSubbasisCoercion = Coercion++precomposeCoercion :: Coercion a b -> Coercion (b -> c) (a -> c)+precomposeCoercion Coercion = Coercion++postcomposeCoercion :: Coercion b c -> Coercion (a -> b) (a -> c)+postcomposeCoercion Coercion = Coercion++firstCoercion :: Coercion a b -> Coercion (a,c) (b,c)+firstCoercion Coercion = Coercion++leftCoercion :: Coercion a b -> Coercion (Either a c) (Either b c)+leftCoercion Coercion = Coercion++abstractVS_dualFinitenessWitness :: ∀ v .+ ( AbstractLinearSpace v, FiniteDimensional v+ , FiniteDimensional (VectorSpaceImplementation v) )+ => DualFinitenessWitness v+abstractVS_dualFinitenessWitness = scalarsSameInAbstraction @v+ (case dualFinitenessWitness @(VectorSpaceImplementation v) of+ DualFinitenessWitness DualSpaceWitness+ -> DualFinitenessWitness DualSpaceWitness+ )++abstractVS_entireBasis :: ∀ v .+ ( AbstractLinearSpace v, FiniteDimensional (VectorSpaceImplementation v)+ , Coercible (SubBasis v) (SubBasis (VectorSpaceImplementation v)) )+ => SubBasis v+abstractVS_entireBasis = sym (abstractSubbasisCoercion @v)+ $ entireBasis @(VectorSpaceImplementation v)++abstractVS_enumerateSubBasis :: ∀ v .+ ( AbstractLinearSpace v, FiniteDimensional (VectorSpaceImplementation v)+ , Coercible (SubBasis v) (SubBasis (VectorSpaceImplementation v)) )+ => SubBasis v -> [v]+abstractVS_enumerateSubBasis = precomposeCoercion (abstractSubbasisCoercion @v)+ $ coerce (enumerateSubBasis @(VectorSpaceImplementation v))++abstractVS_decomposeLinMap :: ∀ v w .+ ( AbstractLinearSpace v+ , FiniteDimensional (VectorSpaceImplementation v)+ , Coercible (SubBasis v) (SubBasis (VectorSpaceImplementation v))+ , LSpace w, Scalar w ~ Scalar v )+ => (v +> w) -> (SubBasis v, DList w)+abstractVS_decomposeLinMap = scalarsSameInAbstraction @v+ ( postcomposeCoercion (firstCoercion $ sym (abstractSubbasisCoercion @v))+ $ case abstractTensorProductsCoercion @v @w of+ Coercion -> ( coerce (decomposeLinMap @(VectorSpaceImplementation v) @w)+ :: (v +> w) -> ( SubBasis (VectorSpaceImplementation v)+ , DList w ) )+ )++abstractVS_decomposeLinMapWithin :: ∀ v w . ( AbstractLinearSpace v+ , FiniteDimensional (VectorSpaceImplementation v)+ , Coercible (SubBasis v) (SubBasis (VectorSpaceImplementation v))+ , LSpace w, Scalar w ~ Scalar v )+ => SubBasis v -> (v +> w) -> Either (SubBasis v, DList w) (DList w)+abstractVS_decomposeLinMapWithin = scalarsSameInAbstraction @v+ ( precomposeCoercion (abstractSubbasisCoercion @v)+ . postcomposeCoercion (postcomposeCoercion+ . leftCoercion . firstCoercion $ sym (abstractSubbasisCoercion @v))+ $ coerce (decomposeLinMapWithin @(VectorSpaceImplementation v) @w)+ )++abstractVS_recomposeSB :: ∀ v . ( AbstractLinearSpace v+ , FiniteDimensional (VectorSpaceImplementation v)+ , Coercible (SubBasis v) (SubBasis (VectorSpaceImplementation v)) )+ => SubBasis v -> [Scalar v] -> (v, [Scalar v])+abstractVS_recomposeSB = scalarsSameInAbstraction @v+ ( precomposeCoercion (abstractSubbasisCoercion @v)+ $ coerce (recomposeSB @(VectorSpaceImplementation v))+ )++abstractVS_recomposeSBTensor :: ∀ v w . ( AbstractLinearSpace v+ , FiniteDimensional (VectorSpaceImplementation v)+ , Coercible (SubBasis v) (SubBasis (VectorSpaceImplementation v))+ , FiniteDimensional w, Scalar w ~ Scalar v )+ => SubBasis v -> SubBasis w -> [Scalar v] -> (v ⊗ w, [Scalar v])+abstractVS_recomposeSBTensor = scalarsSameInAbstraction @v+ ( precomposeCoercion (abstractSubbasisCoercion @v)+ $ case abstractTensorProductsCoercion @v @w of+ Coercion -> coerce (recomposeSBTensor @(VectorSpaceImplementation v) @w)+ )++abstractVS_recomposeLinMap :: ∀ v w . ( AbstractLinearSpace v+ , FiniteDimensional (VectorSpaceImplementation v)+ , Coercible (SubBasis v) (SubBasis (VectorSpaceImplementation v))+ , LSpace w, Scalar w ~ Scalar v )+ => SubBasis v -> [w] -> (v +> w, [w])+abstractVS_recomposeLinMap = scalarsSameInAbstraction @v+ ( precomposeCoercion (abstractSubbasisCoercion @v)+ $ coerce (recomposeLinMap @(VectorSpaceImplementation v) @w)+ )++abstractVS_recomposeContraLinMap :: ∀ v f w . ( AbstractLinearSpace v+ , FiniteDimensional (VectorSpaceImplementation v)+ , Coercible (SubBasis v) (SubBasis (VectorSpaceImplementation v))+ , LinearSpace w, Scalar w ~ Scalar v+ , Hask.Functor f )+ => (f (Scalar w) -> w) -> f (DualVector v) -> v +> w+abstractVS_recomposeContraLinMap f = scalarsSameInAbstraction @v+ ( coerce (recomposeContraLinMap @(VectorSpaceImplementation v) @w @f f)+ . fmap getConcreteDualVector+ )++abstractVS_recomposeLinMapTensor :: ∀ v f w u . ( AbstractLinearSpace v+ , FiniteDimensional (VectorSpaceImplementation v)+ , Coercible (SubBasis v) (SubBasis (VectorSpaceImplementation v))+ , LinearSpace w, Scalar w ~ Scalar v+ , FiniteDimensional u, Scalar u ~ Scalar v+ , Hask.Functor f )+ => (f (Scalar w) -> w) -> f (v+>DualVector u) -> (v⊗u) +> w+abstractVS_recomposeLinMapTensor f = scalarsSameInAbstraction @v+ ( coerce (recomposeContraLinMapTensor @(VectorSpaceImplementation v) @u @w @f f)+ . fmap (coerce :: (v+>DualVector u)+ -> (VectorSpaceImplementation v+>DualVector u))+ )++abstractVS_uncanonicallyFromDual :: ∀ v . ( AbstractLinearSpace v+ , FiniteDimensional (VectorSpaceImplementation v) )+ => DualVector v -+> v+abstractVS_uncanonicallyFromDual = scalarsSameInAbstraction @v+ ( case abstractDualVectorCoercion @v of+ Coercion -> coerce (uncanonicallyFromDual @(VectorSpaceImplementation v))+ )++abstractVS_uncanonicallyToDual :: ∀ v . ( AbstractLinearSpace v+ , FiniteDimensional (VectorSpaceImplementation v) )+ => v -+> DualVector v+abstractVS_uncanonicallyToDual = scalarsSameInAbstraction @v+ ( case abstractDualVectorCoercion @v of+ Coercion -> coerce (uncanonicallyToDual @(VectorSpaceImplementation v))+ )++abstractVS_tensorEquality :: ∀ v w . ( AbstractLinearSpace v+ , FiniteDimensional (VectorSpaceImplementation v)+ , TensorSpace w, Eq w, Scalar w ~ Scalar v )+ => (v ⊗ w) -> (v ⊗ w) -> Bool+abstractVS_tensorEquality = scalarsSameInAbstraction @v+ ( case abstractTensorProductsCoercion @v @w of+ Coercion -> coerce (tensorEquality @(VectorSpaceImplementation v) @w)+ )++abstractVS_dualBasisCandidates :: ∀ v . ( AbstractLinearSpace v+ , SemiInner (VectorSpaceImplementation v) )+ => [(Int, v)] -> Forest (Int, DualVector v)+abstractVS_dualBasisCandidates = scalarsSameInAbstraction @v+ ( case abstractDualVectorCoercion @v of+ Coercion -> coerce (dualBasisCandidates @(VectorSpaceImplementation v))+ )++abstractVS_tensorDualBasisCandidates :: ∀ v w . ( AbstractLinearSpace v+ , LinearSpace v+ , SemiInner (VectorSpaceImplementation v)+ , SemiInner w, Scalar w ~ Scalar v)+ => [(Int, v ⊗ w)]+ -> Forest (Int, v +> DualVector w)+abstractVS_tensorDualBasisCandidates = scalarsSameInAbstraction @v+ ( case (dualSpaceWitness @v, dualSpaceWitness @w) of+ (DualSpaceWitness, DualSpaceWitness)+ -> case ( abstractDualVectorCoercion @v+ , abstractTensorProductsCoercion @v @(DualVector w)+ , abstractTensorProductsCoercion @v @w+ ) of+ (Coercion, Coercion, Coercion)+ -> coerce (tensorDualBasisCandidates @(VectorSpaceImplementation v) @w)+ )++abstractVS_symTensorDualBasisCandidates :: ∀ v . ( AbstractLinearSpace v+ , LinearSpace v+ , SemiInner (VectorSpaceImplementation v) )+ => [(Int, SymmetricTensor (Scalar v) v)]+ -> Forest (Int, SymmetricTensor (Scalar v) (DualVector v))+abstractVS_symTensorDualBasisCandidates = scalarsSameInAbstraction @v+ ( case ( dualSpaceWitness @v+ , dualSpaceWitness @(VectorSpaceImplementation v)+ , abstractDualVectorCoercion @v ) of+ (DualSpaceWitness, DualSpaceWitness, crdv)+ -> case ( abstractTensorProductsCoercion @v @v+ , coerceFmapTensorProduct @(DualVector (VectorSpaceImplementation v)) []+ crdv+ , coerceFmapTensorProduct @(VectorSpaceImplementation v) []+ crdv+ , coerceFmapTensorProduct @(VectorSpaceImplementation v) []+ (Coercion @v @(VectorSpaceImplementation v))+ ) of+ (Coercion, Coercion, Coercion, Coercion)+ -> coerce (symTensorDualBasisCandidates @(VectorSpaceImplementation v))+ )++-- | More powerful version of @deriving newtype@, specialised to the classes from+-- this package (and of @manifolds-core@). The 'DualVector' space will be a separate+-- type, even if the type you abstract over is self-dual.+copyNewtypeInstances :: Q Type -> [Name] -> DecsQ+copyNewtypeInstances cxtv classes = do++ (tvbs, cxt, (a,c)) <- do+ (tvbs', cxt', a') <- deQuantifyType cxtv+ let extractImplementationType (AppT tc (VarT tvb)) atvbs+ = extractImplementationType tc $ atvbs++[PlainTV tvb]+ extractImplementationType (ConT aName) atvbs = do+ D.reifyDatatype aName >>= \case+ D.DatatypeInfo{ D.datatypeVariant = D.Newtype+ , D.datatypeVars = dttvbs+ , D.datatypeCons = [+ D.ConstructorInfo+ { D.constructorFields = [c''] } ]+ }+ -> let replaceTVs :: [TyVarBndr] -> [TyVarBndr] -> Type -> Type+ replaceTVs [] [] = id+ replaceTVs (PlainTV infoTV:infoTVs) (PlainTV instTV:instTVs)+ = replaceTVs infoTVs instTVs . replaceTV infoTV instTV+ replaceTVs (KindedTV infoTV _:infoTVs) instTVs+ = replaceTVs (PlainTV infoTV:infoTVs) instTVs+ replaceTVs infoTVs (KindedTV instTV _:instTVs)+ = replaceTVs infoTVs (PlainTV instTV:instTVs)+ replaceTVs infoTVs instTVs+ = error $ "infoTVs = "++show infoTVs++", instTVs = "++show instTVs+ replaceTV :: Name -> Name -> Type -> Type+ replaceTV infoTV instTV (AppT tc (VarT tv))+ | tv==infoTV = AppT (replaceTV infoTV instTV tc) (VarT instTV)+ replaceTV infoTV instTV (AppT tc ta)+ = AppT (replaceTV infoTV instTV tc)+ (replaceTV infoTV instTV ta)+ replaceTV _ _ t@(TupleT _) = t+ replaceTV _ _ t@(ConT _) = t+ replaceTV _ _ t+ = error $ "Don't know how to substitute type variables in "+ ++ show t+ in return $ replaceTVs dttvbs atvbs c''+ _ -> error $ show aName ++ " is not a newtype."+ extractImplementationType a'' _+ = error $ "Don't know how to handle type "++show a''+ ++" (specified: "++show a'++")"+ c' <- extractImplementationType a' []+ return (tvbs', pure cxt', (pure a', pure c'))+ + let allClasses =+ [ ''AbstractAdditiveGroup | _<-[()], ''AdditiveGroup `elem` classes ]+ ++ [ ''AbstractVectorSpace | _<-[()], ''VectorSpace `elem` classes ]+ ++ [ ''AbstractTensorSpace | _<-[()], ''TensorSpace `elem` classes ]+ ++ [ ''AbstractLinearSpace | _<-[()], ''LinearSpace `elem` classes ]+ ++ classes++ vtnameHash <- abs . hash . show <$> a++ sequence [case dClass of+ "AbstractAdditiveGroup" -> InstanceD Nothing <$> cxt <*>+ [t|AbstractAdditiveGroup $a|] <*> [d|+ type instance VectorSpaceImplementation $a = $c+ |]+ "AdditiveGroup" -> InstanceD Nothing <$> cxt <*>+ [t|AdditiveGroup $a|] <*> [d|+ $(varP 'zeroV) = abstractVS_zeroV+ $(varP '(^+^)) = abstractVS_addvs+ $(varP '(^-^)) = abstractVS_subvs+ $(varP 'negateV) = abstractVS_negateV+ |]+ "AffineSpace" -> InstanceD Nothing <$> cxt <*>+ [t|AffineSpace $a|] <*> [d|+ type instance Diff $a = $a+ $(varP '(.-.)) = abstractVS_subvs+ $(varP '(.+^)) = abstractVS_addvs+ |]+ "VectorSpace" -> InstanceD Nothing <$> cxt <*>+ [t|VectorSpace $a|] <*> [d|+ type instance Scalar $a = Scalar ($c)+ $(varP '(*^)) = abstractVS_scalev+ |]+ "AbstractVectorSpace" -> InstanceD Nothing <$> cxt <*>+ [t|AbstractVectorSpace $a|] <*> [d|+ $(varP 'scalarsSameInAbstraction)+ = abstractVS_scalarsSameInAbstraction @($a)+ |]+ "InnerSpace" -> InstanceD Nothing <$> cxt <*>+ [t|InnerSpace $a|] <*> [d|+ $(varP '(<.>)) = abstractVS_innerProd+ |]+ "Semimanifold" -> InstanceD Nothing <$> cxt <*>+ [t|Semimanifold $a|] <*> [d|+ type instance Needle $a = $a+ $(varP '(.+~^)) = abstractVS_addvs+#if !MIN_VERSION_manifolds_core(0,6,0)+ type instance Interior $a = $a+ $(varP 'toInterior) = pure+ $(varP 'fromInterior) = id+ $(varP 'translateP) = Tagged (^+^)+ $(varP 'semimanifoldWitness) = SemimanifoldWitness BoundarylessWitness+#endif+ |]+ "PseudoAffine" -> InstanceD Nothing <$> cxt <*>+ [t|PseudoAffine $a|] <*> [d|+ $(varP '(.-~.)) = \p q -> Just (abstractVS_subvs p q)+ $(varP '(.-~!)) = abstractVS_subvs+ |]+ "TensorSpace" -> InstanceD Nothing <$> cxt <*>+ [t|TensorSpace $a|] <*> [d|+ type instance TensorProduct $a w = TensorProduct $c w+ $(varP 'scalarSpaceWitness) = abstractVS_scalarSpaceWitness+ $(varP 'linearManifoldWitness) = abstractVS_linearManifoldWitness+ $(varP 'toFlatTensor) = abstractVS_toFlatTensor+ $(varP 'fromFlatTensor) = abstractVS_fromFlatTensor+ $(varP 'zeroTensor) = abstractVS_zeroTensor+ $(varP 'addTensors) = abstractVS_addTensors+ $(varP 'subtractTensors) = abstractVS_subtractTensors+ $(varP 'scaleTensor) = abstractVS_scaleTensor+ $(varP 'negateTensor) = abstractVS_negateTensor+ $(varP 'wellDefinedVector) = abstractVS_wellDefinedVector+ $(varP 'wellDefinedTensor) = abstractVS_wellDefinedTensor+ $(varP 'tensorProduct) = abstractVS_tensorProduct+ $(varP 'transposeTensor) = abstractVS_transposeTensor+ $(varP 'fmapTensor) = abstractVS_fmapTensor+ $(varP 'fzipTensorWith) = abstractVS_fzipTensorsWith+ $(varP 'coerceFmapTensorProduct) = abstractVS_coerceFmapTensorProduct+ |]+ "AbstractTensorSpace" -> InstanceD Nothing <$> cxt <*>+ [t|AbstractTensorSpace $a|] <*> [d|+ $(varP 'abstractTensorProductsCoercion)+ = Coercion+ |]+ "LinearSpace" -> InstanceD Nothing <$> cxt <*>+ [t|LinearSpace $a|] <*> [d|+ type instance DualVector $a = AbstractDualVector $a $c+ $(varP 'dualSpaceWitness) = abstractVS_dualSpaceWitness+ $(varP 'linearId) = abstractVS_linearId+ $(varP 'tensorId) = abstractVS_tensorId+ $(varP 'applyDualVector) = abstractVS_applyDualVector+ $(varP 'applyLinear) = abstractVS_applyLinear+ $(varP 'applyTensorFunctional) = abstractVS_applyTensorFunctional+ $(varP 'applyTensorLinMap) = abstractVS_applyTensorLinMap+ $(varP 'useTupleLinearSpaceComponents) = \_ -> usingNonTupleTypeAsTupleError+ |]+ "AbstractLinearSpace" -> InstanceD Nothing <$> cxt <*>+ [t|AbstractLinearSpace $a|] <*> [d|+ |]+ "FiniteDimensional" -> InstanceD Nothing <$> cxt <*>+ [t|FiniteDimensional $a|] <*> do+ subBasisCstr <- newName $ "SubBasis"++show vtnameHash+ + tySyns <- sequence [+#if MIN_VERSION_template_haskell(2,15,0)+ NewtypeInstD [] (Just tvbs)+ <$> (AppT (ConT ''SubBasis) <$> a)+ <*> pure Nothing+ <*> (NormalC subBasisCstr . pure .+ (Bang NoSourceUnpackedness NoSourceStrictness,)+ <$> [t| SubBasis $c |])+ <*> pure []+#else+ NewtypeInstD [] ''SubBasis+ <$> ((:[]) <$> a)+ <*> pure Nothing+ <*> (NormalC subBasisCstr . pure . + (Bang NoSourceUnpackedness NoSourceStrictness,)+ <$> [t| SubBasis $c |])+ <*> pure []+#endif+ ]+ methods <- [d|+ $(varP 'dualFinitenessWitness) = abstractVS_dualFinitenessWitness+ $(varP 'entireBasis) = abstractVS_entireBasis+ $(varP 'enumerateSubBasis) = abstractVS_enumerateSubBasis+ $(varP 'decomposeLinMap) = abstractVS_decomposeLinMap+ $(varP 'decomposeLinMapWithin) = abstractVS_decomposeLinMapWithin+ $(varP 'recomposeSB) = abstractVS_recomposeSB+ $(varP 'recomposeSBTensor) = abstractVS_recomposeSBTensor+ $(varP 'recomposeLinMap) = abstractVS_recomposeLinMap+ $(varP 'recomposeContraLinMap) = abstractVS_recomposeContraLinMap+ $(varP 'recomposeContraLinMapTensor) = abstractVS_recomposeLinMapTensor+ $(varP 'uncanonicallyFromDual) = abstractVS_uncanonicallyFromDual+ $(varP 'uncanonicallyToDual) = abstractVS_uncanonicallyToDual+ $(varP 'tensorEquality) = abstractVS_tensorEquality+ |]+ return $ tySyns ++ methods+ "SemiInner" -> InstanceD Nothing <$> cxt <*>+ [t|SemiInner $a|] <*> [d|+ $(varP 'dualBasisCandidates) = abstractVS_dualBasisCandidates+ $(varP 'tensorDualBasisCandidates) = abstractVS_tensorDualBasisCandidates+ $(varP 'symTensorDualBasisCandidates) = abstractVS_symTensorDualBasisCandidates+ |]+ _ -> error $ "Unsupported class to derive newtype instance for: ‘"++dClass++"’"+ | Name (OccName dClass) _ <- allClasses+ ]
Math/VectorSpace/Docile.hs view
@@ -664,7 +664,7 @@ deriving instance Show (SubBasis ℝ) instance ∀ u v . ( FiniteDimensional u, FiniteDimensional v- , Scalar u ~ Scalar v, Scalar (DualVector u) ~ Scalar (DualVector v) )+ , Scalar u ~ Scalar v ) => FiniteDimensional (u,v) where data SubBasis (u,v) = TupleBasis !(SubBasis u) !(SubBasis v) entireBasis = TupleBasis entireBasis entireBasis@@ -929,31 +929,6 @@ -> LinearMap s (LinearMap s (DualVector v) v) w rcCLM (DualFinitenessWitness DualSpaceWitness) f = recomposeContraLinMap f- recomposeContraLinMapTensor = rcCLMT'- where rcCLMT' :: ∀ f u w . (Hask.Functor f, LinearSpace w, s~Scalar w- , FiniteDimensional u, s~Scalar u)- => (f s->w) -> f (SymmetricTensor s v +> DualVector u)- -> (SymmetricTensor s v ⊗ u) +> w- rcCLMT' f tenss- = LinearMap . arr (fmap rassocTensor . rassocTensor . asTensor)- . rcCLMT (dualFinitenessWitness, dualFinitenessWitness) f- $ fmap getLinearMap tenss- where rcCLMT :: (DualFinitenessWitness v, DualFinitenessWitness u)- -> (f s->w) -> f (Tensor s (DualVector v)- (Tensor s (DualVector v) (DualVector u)))- -- -> LinearMap s (Tensor s (SymmetricTensor s v) u) w- -- ∼ TensorProduct (LinearMap s (SymmetricTensor s v) (DualVector u)) w- -- ⩵ TensorProduct (SymmetricTensor s (DualVector v)) (DualVector u ⊗ w)- -- ⩵ Tensor s (DualVector v) (DualVector v ⊗ (DualVector u ⊗ w))- -> LinearMap s (LinearMap s (DualVector v)- (LinearMap s (DualVector v) u)) w- -- ∼ Tensor s (Tensor s (DualVector v)- -- (DualVector v ⊗ DualVector u)) w- -- ∼ Tensor s (DualVector v)- -- (Tensor s (DualVector v ⊗ DualVector u) w)- rcCLMT ( DualFinitenessWitness DualSpaceWitness- , DualFinitenessWitness DualSpaceWitness ) f- = recomposeContraLinMap f uncanonicallyFromDual = case dualFinitenessWitness :: DualFinitenessWitness v of DualFinitenessWitness DualSpaceWitness -> LinearFunction $ \(SymTensor t) -> SymTensor $ arr fromLinearMap . uncanonicallyFromDual $ t
linearmap-category.cabal view
@@ -2,7 +2,7 @@ -- documentation, see http://haskell.org/cabal/users-guide/ name: linearmap-category-version: 0.4.2.0+version: 0.4.3.0 synopsis: Native, complete, matrix-free linear algebra. description: The term /numerical linear algebra/ is often used almost synonymous with /matrix modifications/. However, what's interesting@@ -61,7 +61,9 @@ semigroups, hashable, data-default-class, ieee754 >= 0.7 && < 0.9,- call-stack, template-haskell >=2.12 && <2.18,+ call-stack,+ template-haskell >=2.12 && <2.18,+ th-abstraction >=0.4 && <0.5, QuickCheck >=2.11 && <2.15 -- hs-source-dirs: default-language: Haskell2010
test/tasty/test.hs view
@@ -36,7 +36,32 @@ import qualified Test.QuickCheck as QC +newtype ℝ⁴ = ℝ⁴ { getℝ⁴ :: V4 ℝ }+ deriving (Eq, Show) +copyNewtypeInstances [t| ℝ⁴ |]+ [ ''AdditiveGroup, ''AffineSpace, ''VectorSpace+ , ''Semimanifold, ''PseudoAffine+ , ''TensorSpace, ''LinearSpace+ , ''FiniteDimensional, ''SemiInner, ''InnerSpace ]++newtype H¹ℝ⁴ a = H¹ℝ⁴ { getH¹ℝ⁴ :: ((a,a),(a,a)) }+ deriving (Eq, Show)++copyNewtypeInstances [t| ∀ a+ . (RealFloat' a, FiniteDimensional a, SemiInner a) => H¹ℝ⁴ a |]+ [ ''AdditiveGroup, ''AffineSpace, ''VectorSpace+ , ''Semimanifold, ''PseudoAffine+ , ''TensorSpace, ''LinearSpace+ , ''FiniteDimensional, ''SemiInner ]++derivative₄ :: H¹ℝ⁴ ℝ -> ℝ⁴+derivative₄ (H¹ℝ⁴ ((w,x),(y,z))) = ℝ⁴ (V4 z w x y) ^-^ ℝ⁴ (V4 x y z w)++instance InnerSpace (H¹ℝ⁴ ℝ) where+ H¹ℝ⁴ v <.> H¹ℝ⁴ w = v<.>w + derivative₄ (H¹ℝ⁴ v)<.>derivative₄ (H¹ℝ⁴ w)++ newtype ℝ⁵ a = ℝ⁵ { getℝ⁵ :: [ℝ] } deriving (Eq, Show) @@ -86,11 +111,11 @@ makeFiniteDimensionalFromBasis [t| H¹ℝ⁵ |] -derivative :: H¹ℝ⁵ -> ℝ⁵ Int-derivative (H¹ℝ⁵ (ℝ⁵ (x₀:xs))) = ℝ⁵ (x₀:xs) ^-^ ℝ⁵ (xs++[x₀])+derivative₅ :: H¹ℝ⁵ -> ℝ⁵ Int+derivative₅ (H¹ℝ⁵ (ℝ⁵ (x₀:xs))) = ℝ⁵ (x₀:xs) ^-^ ℝ⁵ (xs++[x₀]) instance InnerSpace H¹ℝ⁵ where- H¹ℝ⁵ v <.> H¹ℝ⁵ w = v<.>w + derivative (H¹ℝ⁵ v)<.>derivative (H¹ℝ⁵ w)+ H¹ℝ⁵ v <.> H¹ℝ⁵ w = v<.>w + derivative₅ (H¹ℝ⁵ v)<.>derivative₅ (H¹ℝ⁵ w) instance Arbitrary (V4 ℝ) where arbitrary = V4<$>arbitrary<*>arbitrary<*>arbitrary<*>arbitrary@@ -113,6 +138,19 @@ $ \v -> (riesz-+$>coRiesz-+$>v) === (v :: ℝ⁵ Int) , testProperty "Riesz representation, non-orthonormal basis" $ \v -> (riesz-+$>coRiesz-+$>v) ≈≈≈ (v :: H¹ℝ⁵)+ ]+ , testGroup "Newtype-derived space"+ [ testProperty "Addition"+ $ \v w -> ℝ⁴ v^+^ℝ⁴ w === ℝ⁴ (v^+^w)+ , testProperty "Riesz representation, orthonormal basis"+ $ \v -> (riesz-+$>coRiesz-+$>ℝ⁴ v) === ℝ⁴ v+ , testProperty "Riesz is trivial in orthonormal basis"+ $ \v -> (riesz-+$>AbstractDualVector v) ≈≈≈ ℝ⁴ v+ , testProperty "Riesz representation, non-orthonormal basis"+ $ \v -> (riesz-+$>coRiesz-+$>H¹ℝ⁴ v) ≈≈≈ (H¹ℝ⁴ v :: H¹ℝ⁴ Double)+ , testProperty "Riesz nontriviality in general case"+ . QC.expectFailure+ $ \v -> (riesz-+$>AbstractDualVector v) ≈≈≈ (H¹ℝ⁴ v :: H¹ℝ⁴ Double) ] ]