-- |
-- Module      : Math.LinearMap.Instances.Deriving
-- Copyright   : (c) Justus Sagemüller 2021
-- License     : GPL v3
-- 
-- Maintainer  : (@) jsag $ hvl.no
-- Stability   : experimental
-- Portability : portable
-- 
{-# LANGUAGE FlexibleInstances          #-}
{-# LANGUAGE FlexibleContexts           #-}
{-# LANGUAGE UndecidableInstances       #-}
{-# LANGUAGE TypeOperators              #-}
{-# LANGUAGE TypeFamilies               #-}
{-# LANGUAGE AllowAmbiguousTypes        #-}
{-# LANGUAGE TypeApplications           #-}
{-# LANGUAGE Rank2Types                 #-}
{-# LANGUAGE ScopedTypeVariables        #-}
{-# LANGUAGE UnicodeSyntax              #-}
{-# LANGUAGE StandaloneDeriving         #-}
{-# LANGUAGE DeriveGeneric              #-}
{-# LANGUAGE GADTs                      #-}
{-# LANGUAGE DerivingStrategies         #-}
{-# LANGUAGE GeneralizedNewtypeDeriving #-}
{-# LANGUAGE TemplateHaskell            #-}
{-# LANGUAGE CPP                        #-}
{-# LANGUAGE TupleSections              #-}
{-# 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 :: Q Type -> Q [Dec]
makeLinearSpaceFromBasis Q Type
v
   = LinearSpaceFromBasisDerivationConfig
-> Q ([TyVarBndr Specificity], Cxt, Type) -> Q [Dec]
makeLinearSpaceFromBasis' forall a. Default a => a
def forall (f :: * -> * -> *) a b.
(Function f, Object f a, Object f b) =>
f a b -> a -> b
$ Q Type -> Q ([TyVarBndr Specificity], Cxt, Type)
deQuantifyType Q Type
v

data LinearSpaceFromBasisDerivationConfig = LinearSpaceFromBasisDerivationConfig
instance Default LinearSpaceFromBasisDerivationConfig where
  def :: LinearSpaceFromBasisDerivationConfig
def = LinearSpaceFromBasisDerivationConfig
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' :: LinearSpaceFromBasisDerivationConfig
-> Q ([TyVarBndr Specificity], Cxt, Type) -> Q [Dec]
makeLinearSpaceFromBasis' LinearSpaceFromBasisDerivationConfig
_ Q ([TyVarBndr Specificity], Cxt, Type)
cxtv = do
 (Q Cxt
cxt,Q Type
v) <- do
   ([TyVarBndr Specificity]
_, Cxt
cxt', Type
v') <- Q ([TyVarBndr Specificity], Cxt, Type)
cxtv
   forall (m :: * -> *) a. Monad m (->) => a -> m a
return (forall (f :: * -> *) (r :: * -> * -> *) (t :: * -> * -> *) a.
(Applicative f r t, Object r a, Object t (f a)) =>
t a (f a)
pure Cxt
cxt', forall (f :: * -> *) (r :: * -> * -> *) (t :: * -> * -> *) a.
(Applicative f r t, Object r a, Object t (f a)) =>
t a (f a)
pure Type
v')
 
 [Extension]
exts <- Q [Extension]
extsEnabled
 if Bool -> Bool
not forall (f :: * -> * -> *) a b.
(Function f, Object f a, Object f b) =>
f a b -> a -> b
$ forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem`[Extension]
exts) [Extension
TypeFamilies, Extension
ScopedTypeVariables, Extension
TypeApplications]
   then [Char] -> Q ()
reportError [Char]
"This macro requires -XTypeFamilies, -XScopedTypeVariables and -XTypeApplications."
   else forall (f :: * -> *) (r :: * -> * -> *) (t :: * -> * -> *) a.
(Applicative f r t, Object r a, Object t (f a)) =>
t a (f a)
pure ()
 
 forall (s :: * -> *) (t :: * -> *) (k :: * -> * -> *)
       (l :: * -> * -> *) (f :: * -> *) a.
(Traversable s t k l, k ~ l, s ~ t, Monoidal f k k,
 ObjectPair k a (t a), ObjectPair k (f a) (f (t a)),
 Object k (t (f a)), TraversalObject k t a) =>
k (t (f a)) (f (t a))
sequence
  [ Maybe Overlap -> Cxt -> Type -> [Dec] -> Dec
InstanceD forall a. Maybe a
Nothing forall (f :: * -> *) (r :: * -> * -> *) a b.
(Functor f r (->), Object r a, Object r b) =>
r a b -> f a -> f b
<$> Q Cxt
cxt forall (f :: * -> *) (r :: * -> * -> *) (t :: * -> * -> *) a b.
(Applicative f r t, ObjectMorphism r a b,
 ObjectMorphism t (f a) (f b), Object t (t (f a) (f b)),
 ObjectPair r (r a b) a, ObjectPair t (f (r a b)) (f a), Object r a,
 Object r b) =>
t (f (r a b)) (t (f a) (f b))
<*> [t|Semimanifold $v|] forall (f :: * -> *) (r :: * -> * -> *) (t :: * -> * -> *) a b.
(Applicative f r t, ObjectMorphism r a b,
 ObjectMorphism t (f a) (f b), Object t (t (f a) (f b)),
 ObjectPair r (r a b) a, ObjectPair t (f (r a b)) (f a), Object r a,
 Object r b) =>
t (f (r a b)) (t (f a) (f b))
<*> [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 '(.+~^)) = (^+^)
      |]
  , Maybe Overlap -> Cxt -> Type -> [Dec] -> Dec
InstanceD forall a. Maybe a
Nothing forall (f :: * -> *) (r :: * -> * -> *) a b.
(Functor f r (->), Object r a, Object r b) =>
r a b -> f a -> f b
<$> Q Cxt
cxt forall (f :: * -> *) (r :: * -> * -> *) (t :: * -> * -> *) a b.
(Applicative f r t, ObjectMorphism r a b,
 ObjectMorphism t (f a) (f b), Object t (t (f a) (f b)),
 ObjectPair r (r a b) a, ObjectPair t (f (r a b)) (f a), Object r a,
 Object r b) =>
t (f (r a b)) (t (f a) (f b))
<*> [t|PseudoAffine $v|] forall (f :: * -> *) (r :: * -> * -> *) (t :: * -> * -> *) a b.
(Applicative f r t, ObjectMorphism r a b,
 ObjectMorphism t (f a) (f b), Object t (t (f a) (f b)),
 ObjectPair r (r a b) a, ObjectPair t (f (r a b)) (f a), Object r a,
 Object r b) =>
t (f (r a b)) (t (f a) (f b))
<*> do
      [d|
         $(varP '(.-~!)) = (^-^)
         $(varP '(.-~.)) = \p q -> pure (p^-^q)
       |]
  , Maybe Overlap -> Cxt -> Type -> [Dec] -> Dec
InstanceD forall a. Maybe a
Nothing forall (f :: * -> *) (r :: * -> * -> *) a b.
(Functor f r (->), Object r a, Object r b) =>
r a b -> f a -> f b
<$> Q Cxt
cxt forall (f :: * -> *) (r :: * -> * -> *) (t :: * -> * -> *) a b.
(Applicative f r t, ObjectMorphism r a b,
 ObjectMorphism t (f a) (f b), Object t (t (f a) (f b)),
 ObjectPair r (r a b) a, ObjectPair t (f (r a b)) (f a), Object r a,
 Object r b) =>
t (f (r a b)) (t (f a) (f b))
<*> [t|AffineSpace $v|] forall (f :: * -> *) (r :: * -> * -> *) (t :: * -> * -> *) a b.
(Applicative f r t, ObjectMorphism r a b,
 ObjectMorphism t (f a) (f b), Object t (t (f a) (f b)),
 ObjectPair r (r a b) a, ObjectPair t (f (r a b)) (f a), Object r a,
 Object r b) =>
t (f (r a b)) (t (f a) (f b))
<*> [d|
         type instance Diff $v = $v
         $(varP '(.+^)) = (^+^)
         $(varP '(.-.)) = (^-^)
       |]
  , Maybe Overlap -> Cxt -> Type -> [Dec] -> Dec
InstanceD forall a. Maybe a
Nothing forall (f :: * -> *) (r :: * -> * -> *) a b.
(Functor f r (->), Object r a, Object r b) =>
r a b -> f a -> f b
<$> Q Cxt
cxt forall (f :: * -> *) (r :: * -> * -> *) (t :: * -> * -> *) a b.
(Applicative f r t, ObjectMorphism r a b,
 ObjectMorphism t (f a) (f b), Object t (t (f a) (f b)),
 ObjectPair r (r a b) a, ObjectPair t (f (r a b)) (f a), Object r a,
 Object r b) =>
t (f (r a b)) (t (f a) (f b))
<*> [t|TensorSpace $v|] forall (f :: * -> *) (r :: * -> * -> *) (t :: * -> * -> *) a b.
(Applicative f r t, ObjectMorphism r a b,
 ObjectMorphism t (f a) (f b), Object t (t (f a) (f b)),
 ObjectPair r (r a b) a, ObjectPair t (f (r a b)) (f a), Object r a,
 Object r b) =>
t (f (r a b)) (t (f a) (f b))
<*> [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) = \_ VSCCoercion
           -> error "Cannot yet coerce tensors defined from a `HasBasis` instance. This would require `RoleAnnotations` on `:->:`. Cf. https://gitlab.haskell.org/ghc/ghc/-/issues/8177"
       |]
  , Maybe Overlap -> Cxt -> Type -> [Dec] -> Dec
InstanceD forall a. Maybe a
Nothing forall (f :: * -> *) (r :: * -> * -> *) a b.
(Functor f r (->), Object r a, Object r b) =>
r a b -> f a -> f b
<$> Q Cxt
cxt forall (f :: * -> *) (r :: * -> * -> *) (t :: * -> * -> *) a b.
(Applicative f r t, ObjectMorphism r a b,
 ObjectMorphism t (f a) (f b), Object t (t (f a) (f b)),
 ObjectPair r (r a b) a, ObjectPair t (f (r a b)) (f a), Object r a,
 Object r b) =>
t (f (r a b)) (t (f a) (f b))
<*> [t|BasisGeneratedSpace $v|] forall (f :: * -> *) (r :: * -> * -> *) (t :: * -> * -> *) a b.
(Applicative f r t, ObjectMorphism r a b,
 ObjectMorphism t (f a) (f b), Object t (t (f a) (f b)),
 ObjectPair r (r a b) a, ObjectPair t (f (r a b)) (f a), Object r a,
 Object r b) =>
t (f (r a b)) (t (f a) (f b))
<*> do
      [d|
         $(varP 'proveTensorProductIsTrie) = \φ -> φ
       |]
  , Maybe Overlap -> Cxt -> Type -> [Dec] -> Dec
InstanceD forall a. Maybe a
Nothing forall (f :: * -> *) (r :: * -> * -> *) a b.
(Functor f r (->), Object r a, Object r b) =>
r a b -> f a -> f b
<$> Q Cxt
cxt forall (f :: * -> *) (r :: * -> * -> *) (t :: * -> * -> *) a b.
(Applicative f r t, ObjectMorphism r a b,
 ObjectMorphism t (f a) (f b), Object t (t (f a) (f b)),
 ObjectPair r (r a b) a, ObjectPair t (f (r a b)) (f a), Object r a,
 Object r b) =>
t (f (r a b)) (t (f a) (f b))
<*> [t|LinearSpace $v|] forall (f :: * -> *) (r :: * -> * -> *) (t :: * -> * -> *) a b.
(Applicative f r t, ObjectMorphism r a b,
 ObjectMorphism t (f a) (f b), Object t (t (f a) (f b)),
 ObjectPair r (r a b) a, ObjectPair t (f (r a b)) (f a), Object r a,
 Object r b) =>
t (f (r a b)) (t (f a) (f b))
<*> [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
def = FiniteDimensionalFromBasisDerivationConfig
FiniteDimensionalFromBasisDerivationConfig

-- | Like 'makeLinearSpaceFromBasis', but additionally generate instances for
--   'FiniteDimensional' and 'SemiInner'.
makeFiniteDimensionalFromBasis :: Q Type -> DecsQ
makeFiniteDimensionalFromBasis :: Q Type -> Q [Dec]
makeFiniteDimensionalFromBasis Q Type
v
   = FiniteDimensionalFromBasisDerivationConfig
-> Q ([TyVarBndr Specificity], Cxt, Type) -> Q [Dec]
makeFiniteDimensionalFromBasis' forall a. Default a => a
def forall (f :: * -> * -> *) a b.
(Function f, Object f a, Object f b) =>
f a b -> a -> b
$ Q Type -> Q ([TyVarBndr Specificity], Cxt, Type)
deQuantifyType Q Type
v

makeFiniteDimensionalFromBasis' :: FiniteDimensionalFromBasisDerivationConfig
              -> Q ([TyVarBndr
#if MIN_VERSION_template_haskell(2,17,0)
                        Specificity
#endif
                       ], Cxt, Type) -> DecsQ
makeFiniteDimensionalFromBasis' :: FiniteDimensionalFromBasisDerivationConfig
-> Q ([TyVarBndr Specificity], Cxt, Type) -> Q [Dec]
makeFiniteDimensionalFromBasis' FiniteDimensionalFromBasisDerivationConfig
_ Q ([TyVarBndr Specificity], Cxt, Type)
cxtv = do
 [Dec]
generalInsts <- LinearSpaceFromBasisDerivationConfig
-> Q ([TyVarBndr Specificity], Cxt, Type) -> Q [Dec]
makeLinearSpaceFromBasis' forall a. Default a => a
def Q ([TyVarBndr Specificity], Cxt, Type)
cxtv
 (Q Cxt
cxt,Q Type
v) <- do
   ([TyVarBndr Specificity]
_, Cxt
cxt', Type
v') <- Q ([TyVarBndr Specificity], Cxt, Type)
cxtv
   forall (m :: * -> *) a. Monad m (->) => a -> m a
return (forall (f :: * -> *) (r :: * -> * -> *) (t :: * -> * -> *) a.
(Applicative f r t, Object r a, Object t (f a)) =>
t a (f a)
pure Cxt
cxt', forall (f :: * -> *) (r :: * -> * -> *) (t :: * -> * -> *) a.
(Applicative f r t, Object r a, Object t (f a)) =>
t a (f a)
pure Type
v')
 Int
vtnameHash <- forall a. Num a => a -> a
abs forall κ (k :: κ -> κ -> *) (a :: κ) (b :: κ) (c :: κ).
(Category k, Object k a, Object k b, Object k c) =>
k b c -> k a b -> k a c
. forall a. Hashable a => a -> Int
hash forall κ (k :: κ -> κ -> *) (a :: κ) (b :: κ) (c :: κ).
(Category k, Object k a, Object k b, Object k c) =>
k b c -> k a b -> k a c
. forall a. Show a => a -> [Char]
show forall (f :: * -> *) (r :: * -> * -> *) a b.
(Functor f r (->), Object r a, Object r b) =>
r a b -> f a -> f b
<$> Q Type
v
 
 [Dec]
fdInsts <- forall (s :: * -> *) (t :: * -> *) (k :: * -> * -> *)
       (l :: * -> * -> *) (f :: * -> *) a.
(Traversable s t k l, k ~ l, s ~ t, Monoidal f k k,
 ObjectPair k a (t a), ObjectPair k (f a) (f (t a)),
 Object k (t (f a)), TraversalObject k t a) =>
k (t (f a)) (f (t a))
sequence
  [ Maybe Overlap -> Cxt -> Type -> [Dec] -> Dec
InstanceD forall a. Maybe a
Nothing forall (f :: * -> *) (r :: * -> * -> *) a b.
(Functor f r (->), Object r a, Object r b) =>
r a b -> f a -> f b
<$> Q Cxt
cxt forall (f :: * -> *) (r :: * -> * -> *) (t :: * -> * -> *) a b.
(Applicative f r t, ObjectMorphism r a b,
 ObjectMorphism t (f a) (f b), Object t (t (f a) (f b)),
 ObjectPair r (r a b) a, ObjectPair t (f (r a b)) (f a), Object r a,
 Object r b) =>
t (f (r a b)) (t (f a) (f b))
<*> [t|FiniteDimensional $v|] forall (f :: * -> *) (r :: * -> * -> *) (t :: * -> * -> *) a b.
(Applicative f r t, ObjectMorphism r a b,
 ObjectMorphism t (f a) (f b), Object t (t (f a) (f b)),
 ObjectPair r (r a b) a, ObjectPair t (f (r a b)) (f a), Object r a,
 Object r b) =>
t (f (r a b)) (t (f a) (f b))
<*> 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
    Name
subBasisCstr <- forall (m :: * -> *). Quote m => [Char] -> m Name
newName forall (f :: * -> * -> *) a b.
(Function f, Object f a, Object f b) =>
f a b -> a -> b
$ [Char]
"CompleteBasis"forall a. [a] -> [a] -> [a]
++forall a. Show a => a -> [Char]
show Int
vtnameHash

    [Dec]
tySyns <- forall (s :: * -> *) (t :: * -> *) (k :: * -> * -> *)
       (l :: * -> * -> *) (f :: * -> *) a.
(Traversable s t k l, k ~ l, s ~ t, Monoidal f k k,
 ObjectPair k a (t a), ObjectPair k (f a) (f (t a)),
 Object k (t (f a)), TraversalObject k t a) =>
k (t (f a)) (f (t a))
sequence [
#if MIN_VERSION_template_haskell(2,15,0)
       Cxt
-> Maybe [TyVarBndr ()]
-> Type
-> Maybe Type
-> [Con]
-> [DerivClause]
-> Dec
DataInstD [] forall a. Maybe a
Nothing
          forall (f :: * -> *) (r :: * -> * -> *) a b.
(Functor f r (->), Object r a, Object r b) =>
r a b -> f a -> f b
<$> (Type -> Type -> Type
AppT (Name -> Type
ConT ''SubBasis) forall (f :: * -> *) (r :: * -> * -> *) a b.
(Functor f r (->), Object r a, Object r b) =>
r a b -> f a -> f b
<$> Q Type
v)
          forall (f :: * -> *) (r :: * -> * -> *) (t :: * -> * -> *) a b.
(Applicative f r t, ObjectMorphism r a b,
 ObjectMorphism t (f a) (f b), Object t (t (f a) (f b)),
 ObjectPair r (r a b) a, ObjectPair t (f (r a b)) (f a), Object r a,
 Object r b) =>
t (f (r a b)) (t (f a) (f b))
<*> forall (f :: * -> *) (r :: * -> * -> *) (t :: * -> * -> *) a.
(Applicative f r t, Object r a, Object t (f a)) =>
t a (f a)
pure forall a. Maybe a
Nothing
          forall (f :: * -> *) (r :: * -> * -> *) (t :: * -> * -> *) a b.
(Applicative f r t, ObjectMorphism r a b,
 ObjectMorphism t (f a) (f b), Object t (t (f a) (f b)),
 ObjectPair r (r a b) a, ObjectPair t (f (r a b)) (f a), Object r a,
 Object r b) =>
t (f (r a b)) (t (f a) (f b))
<*> forall (f :: * -> *) (r :: * -> * -> *) (t :: * -> * -> *) a.
(Applicative f r t, Object r a, Object t (f a)) =>
t a (f a)
pure [Name -> [BangType] -> Con
NormalC Name
subBasisCstr []]
          forall (f :: * -> *) (r :: * -> * -> *) (t :: * -> * -> *) a b.
(Applicative f r t, ObjectMorphism r a b,
 ObjectMorphism t (f a) (f b), Object t (t (f a) (f b)),
 ObjectPair r (r a b) a, ObjectPair t (f (r a b)) (f a), Object r a,
 Object r b) =>
t (f (r a b)) (t (f a) (f b))
<*> forall (f :: * -> *) (r :: * -> * -> *) (t :: * -> * -> *) a.
(Applicative f r t, Object r a, Object t (f a)) =>
t a (f a)
pure []
#else
       DataInstD [] ''SubBasis
          <$> ((:[]) <$> v)
          <*> pure Nothing
          <*> pure [NormalC subBasisCstr []]
          <*> pure []
#endif
     ]
    [Dec]
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

      |]
    forall (m :: * -> *) a. Monad m (->) => a -> m a
return forall (f :: * -> * -> *) a b.
(Function f, Object f a, Object f b) =>
f a b -> a -> b
$ [Dec]
tySyns forall a. [a] -> [a] -> [a]
++ [Dec]
methods
  , Maybe Overlap -> Cxt -> Type -> [Dec] -> Dec
InstanceD forall a. Maybe a
Nothing forall (f :: * -> *) (r :: * -> * -> *) a b.
(Functor f r (->), Object r a, Object r b) =>
r a b -> f a -> f b
<$> Q Cxt
cxt forall (f :: * -> *) (r :: * -> * -> *) (t :: * -> * -> *) a b.
(Applicative f r t, ObjectMorphism r a b,
 ObjectMorphism t (f a) (f b), Object t (t (f a) (f b)),
 ObjectPair r (r a b) a, ObjectPair t (f (r a b)) (f a), Object r a,
 Object r b) =>
t (f (r a b)) (t (f a) (f b))
<*> [t|SemiInner $v|] forall (f :: * -> *) (r :: * -> * -> *) (t :: * -> * -> *) a b.
(Applicative f r t, ObjectMorphism r a b,
 ObjectMorphism t (f a) (f b), Object t (t (f a) (f b)),
 ObjectPair r (r a b) a, ObjectPair t (f (r a b)) (f a), Object r a,
 Object r b) =>
t (f (r a b)) (t (f a) (f b))
<*> do
     [d|
        $(varP 'dualBasisCandidates)
           = cartesianDualBasisCandidates
               (enumerateSubBasis CompleteDualVBasis)
               (\v -> map (abs . realToFrac . decompose' v . fst)
                       $ enumerate (trie $ const ()) )
      |]
  ]
 forall (m :: * -> *) a. Monad m (->) => a -> m a
return forall (f :: * -> * -> *) a b.
(Function f, Object f a, Object f b) =>
f a b -> a -> b
$ [Dec]
generalInsts forall a. [a] -> [a] -> [a]
++ [Dec]
fdInsts


deQuantifyType :: Q Type -> Q ([TyVarBndr
#if MIN_VERSION_template_haskell(2,17,0)
                                 Specificity
#endif
                                ], Cxt, Type)
deQuantifyType :: Q Type -> Q ([TyVarBndr Specificity], Cxt, Type)
deQuantifyType Q Type
t = do
   Type
t' <- Q Type
t
   forall (m :: * -> *) a. Monad m (->) => a -> m a
return forall (f :: * -> * -> *) a b.
(Function f, Object f a, Object f b) =>
f a b -> a -> b
$ case Type
t' of
     ForallT [TyVarBndr Specificity]
tvbs Cxt
cxt Type
instT -> ([TyVarBndr Specificity]
tvbs, Cxt
cxt, Type
instT)
     Type
_ -> ([], [], Type
t')


newtype DualVectorFromBasis v = DualVectorFromBasis { forall v. DualVectorFromBasis v -> v
getDualVectorFromBasis :: v }
  deriving newtype (DualVectorFromBasis v -> DualVectorFromBasis v -> Bool
forall v.
Eq v =>
DualVectorFromBasis v -> DualVectorFromBasis v -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: DualVectorFromBasis v -> DualVectorFromBasis v -> Bool
$c/= :: forall v.
Eq v =>
DualVectorFromBasis v -> DualVectorFromBasis v -> Bool
== :: DualVectorFromBasis v -> DualVectorFromBasis v -> Bool
$c== :: forall v.
Eq v =>
DualVectorFromBasis v -> DualVectorFromBasis v -> Bool
Eq, DualVectorFromBasis v
DualVectorFromBasis v -> DualVectorFromBasis v
DualVectorFromBasis v
-> DualVectorFromBasis v -> DualVectorFromBasis v
forall v.
v -> (v -> v -> v) -> (v -> v) -> (v -> v -> v) -> AdditiveGroup v
forall v. AdditiveGroup v => DualVectorFromBasis v
forall v.
AdditiveGroup v =>
DualVectorFromBasis v -> DualVectorFromBasis v
forall v.
AdditiveGroup v =>
DualVectorFromBasis v
-> DualVectorFromBasis v -> DualVectorFromBasis v
^-^ :: DualVectorFromBasis v
-> DualVectorFromBasis v -> DualVectorFromBasis v
$c^-^ :: forall v.
AdditiveGroup v =>
DualVectorFromBasis v
-> DualVectorFromBasis v -> DualVectorFromBasis v
negateV :: DualVectorFromBasis v -> DualVectorFromBasis v
$cnegateV :: forall v.
AdditiveGroup v =>
DualVectorFromBasis v -> DualVectorFromBasis v
^+^ :: DualVectorFromBasis v
-> DualVectorFromBasis v -> DualVectorFromBasis v
$c^+^ :: forall v.
AdditiveGroup v =>
DualVectorFromBasis v
-> DualVectorFromBasis v -> DualVectorFromBasis v
zeroV :: DualVectorFromBasis v
$czeroV :: forall v. AdditiveGroup v => DualVectorFromBasis v
AdditiveGroup, Scalar (DualVectorFromBasis v)
-> DualVectorFromBasis v -> DualVectorFromBasis v
forall v. AdditiveGroup v -> (Scalar v -> v -> v) -> VectorSpace v
forall {v}. VectorSpace v => AdditiveGroup (DualVectorFromBasis v)
forall v.
VectorSpace v =>
Scalar (DualVectorFromBasis v)
-> DualVectorFromBasis v -> DualVectorFromBasis v
*^ :: Scalar (DualVectorFromBasis v)
-> DualVectorFromBasis v -> DualVectorFromBasis v
$c*^ :: forall v.
VectorSpace v =>
Scalar (DualVectorFromBasis v)
-> DualVectorFromBasis v -> DualVectorFromBasis v
VectorSpace, Basis (DualVectorFromBasis v) -> DualVectorFromBasis v
DualVectorFromBasis v
-> [(Basis (DualVectorFromBasis v),
     Scalar (DualVectorFromBasis v))]
DualVectorFromBasis v
-> Basis (DualVectorFromBasis v) -> Scalar (DualVectorFromBasis v)
forall v.
VectorSpace v
-> (Basis v -> v)
-> (v -> [(Basis v, Scalar v)])
-> (v -> Basis v -> Scalar v)
-> HasBasis v
forall {v}. HasBasis v => VectorSpace (DualVectorFromBasis v)
forall v.
HasBasis v =>
Basis (DualVectorFromBasis v) -> DualVectorFromBasis v
forall v.
HasBasis v =>
DualVectorFromBasis v
-> [(Basis (DualVectorFromBasis v),
     Scalar (DualVectorFromBasis v))]
forall v.
HasBasis v =>
DualVectorFromBasis v
-> Basis (DualVectorFromBasis v) -> Scalar (DualVectorFromBasis v)
decompose' :: DualVectorFromBasis v
-> Basis (DualVectorFromBasis v) -> Scalar (DualVectorFromBasis v)
$cdecompose' :: forall v.
HasBasis v =>
DualVectorFromBasis v
-> Basis (DualVectorFromBasis v) -> Scalar (DualVectorFromBasis v)
decompose :: DualVectorFromBasis v
-> [(Basis (DualVectorFromBasis v),
     Scalar (DualVectorFromBasis v))]
$cdecompose :: forall v.
HasBasis v =>
DualVectorFromBasis v
-> [(Basis (DualVectorFromBasis v),
     Scalar (DualVectorFromBasis v))]
basisValue :: Basis (DualVectorFromBasis v) -> DualVectorFromBasis v
$cbasisValue :: forall v.
HasBasis v =>
Basis (DualVectorFromBasis v) -> DualVectorFromBasis v
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
  .+~^ :: DualVectorFromBasis v
-> Needle (DualVectorFromBasis v) -> DualVectorFromBasis v
(.+~^) = forall v. AdditiveGroup v => v -> v -> v
(^+^)

instance AdditiveGroup v => AffineSpace (DualVectorFromBasis v) where
  type Diff (DualVectorFromBasis v) = DualVectorFromBasis v
  .+^ :: DualVectorFromBasis v
-> Diff (DualVectorFromBasis v) -> DualVectorFromBasis v
(.+^) = forall v. AdditiveGroup v => v -> v -> v
(^+^)
  .-. :: DualVectorFromBasis v
-> DualVectorFromBasis v -> Diff (DualVectorFromBasis v)
(.-.) = forall v. AdditiveGroup v => v -> v -> v
(^-^)

instance AdditiveGroup v => PseudoAffine (DualVectorFromBasis v) where
  .-~! :: HasCallStack =>
DualVectorFromBasis v
-> DualVectorFromBasis v -> Needle (DualVectorFromBasis v)
(.-~!) = forall v. AdditiveGroup v => v -> v -> v
(^-^)
  DualVectorFromBasis v
p.-~. :: DualVectorFromBasis v
-> DualVectorFromBasis v -> Maybe (Needle (DualVectorFromBasis v))
.-~.DualVectorFromBasis v
q = forall (f :: * -> *) (r :: * -> * -> *) (t :: * -> * -> *) a.
(Applicative f r t, Object r a, Object t (f a)) =>
t a (f a)
pure (DualVectorFromBasis v
pforall v. AdditiveGroup v => v -> v -> v
^-^DualVectorFromBasis v
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 :: DualVectorFromBasis v -> Maybe (DualVectorFromBasis v)
wellDefinedVector DualVectorFromBasis v
v
   | DualVectorFromBasis v
vforall a. Eq a => a -> a -> Bool
==DualVectorFromBasis v
v       = forall a. a -> Maybe a
Just DualVectorFromBasis v
v
   | Bool
otherwise  = forall a. Maybe a
Nothing
  wellDefinedTensor :: forall w.
(TensorSpace w, Scalar w ~ Scalar (DualVectorFromBasis v)) =>
(DualVectorFromBasis v ⊗ w) -> Maybe (DualVectorFromBasis v ⊗ w)
wellDefinedTensor (Tensor TensorProduct (DualVectorFromBasis v) w
v)
     = forall (f :: * -> *) (r :: * -> * -> *) (t :: * -> * -> *) a b.
(Functor f r t, Object r a, Object t (f a), Object r b,
 Object t (f b)) =>
r a b -> t (f a) (f b)
fmap (forall (a :: * -> * -> *) b x.
(WellPointed a, Object a b, ObjectPoint a x) =>
x -> a b x
const forall (f :: * -> * -> *) a b.
(Function f, Object f a, Object f b) =>
f a b -> a -> b
$ forall s v w. TensorProduct v w -> Tensor s v w
Tensor TensorProduct (DualVectorFromBasis v) w
v) forall κ (k :: κ -> κ -> *) (a :: κ) (b :: κ) (c :: κ).
(Category k, Object k a, Object k b, Object k c) =>
k b c -> k a b -> k a c
. forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse (forall v. TensorSpace v => v -> Maybe v
wellDefinedVector forall κ (k :: κ -> κ -> *) (a :: κ) (b :: κ) (c :: κ).
(Category k, Object k a, Object k b, Object k c) =>
k b c -> k a b -> k a c
. forall (a :: * -> * -> *) x y.
(PreArrow a, ObjectPair a x y) =>
a (x, y) y
snd) forall (f :: * -> * -> *) a b.
(Function f, Object f a, Object f b) =>
f a b -> a -> b
$ forall a b. HasTrie a => (a :->: b) -> [(a, b)]
enumerate TensorProduct (DualVectorFromBasis v) w
v
  zeroTensor :: forall w.
(TensorSpace w, Scalar w ~ Scalar (DualVectorFromBasis v)) =>
DualVectorFromBasis v ⊗ w
zeroTensor = forall s v w. TensorProduct v w -> Tensor s v w
Tensor forall κ (k :: κ -> κ -> *) (a :: κ) (b :: κ) (c :: κ).
(Category k, Object k a, Object k b, Object k c) =>
k b c -> k a b -> k a c
. forall a b. HasTrie a => (a -> b) -> a :->: b
trie forall (f :: * -> * -> *) a b.
(Function f, Object f a, Object f b) =>
f a b -> a -> b
$ forall (a :: * -> * -> *) b x.
(WellPointed a, Object a b, ObjectPoint a x) =>
x -> a b x
const forall v. AdditiveGroup v => v
zeroV
  toFlatTensor :: DualVectorFromBasis v
-+> (DualVectorFromBasis v ⊗ Scalar (DualVectorFromBasis v))
toFlatTensor = forall s v w. (v -> w) -> LinearFunction s v w
LinearFunction forall (f :: * -> * -> *) a b.
(Function f, Object f a, Object f b) =>
f a b -> a -> b
$ forall s v w. TensorProduct v w -> Tensor s v w
Tensor forall κ (k :: κ -> κ -> *) (a :: κ) (b :: κ) (c :: κ).
(Category k, Object k a, Object k b, Object k c) =>
k b c -> k a b -> k a c
. forall a b. HasTrie a => (a -> b) -> a :->: b
trie forall κ (k :: κ -> κ -> *) (a :: κ) (b :: κ) (c :: κ).
(Category k, Object k a, Object k b, Object k c) =>
k b c -> k a b -> k a c
. forall v. HasBasis v => v -> Basis v -> Scalar v
decompose'
  fromFlatTensor :: (DualVectorFromBasis v ⊗ Scalar (DualVectorFromBasis v))
-+> DualVectorFromBasis v
fromFlatTensor = forall s v w. (v -> w) -> LinearFunction s v w
LinearFunction forall (f :: * -> * -> *) a b.
(Function f, Object f a, Object f b) =>
f a b -> a -> b
$ \(Tensor TensorProduct (DualVectorFromBasis v) (Scalar v)
t)
          -> forall v. HasBasis v => [(Basis v, Scalar v)] -> v
recompose forall (f :: * -> * -> *) a b.
(Function f, Object f a, Object f b) =>
f a b -> a -> b
$ forall a b. HasTrie a => (a :->: b) -> [(a, b)]
enumerate TensorProduct (DualVectorFromBasis v) (Scalar v)
t
  scalarSpaceWitness :: ScalarSpaceWitness (DualVectorFromBasis v)
scalarSpaceWitness = forall v.
(Num' (Scalar v), Scalar (Scalar v) ~ Scalar v) =>
ScalarSpaceWitness v
ScalarSpaceWitness
  linearManifoldWitness :: LinearManifoldWitness (DualVectorFromBasis v)
linearManifoldWitness = forall v.
(Needle v ~ v, AffineSpace v, Diff v ~ v) =>
LinearManifoldWitness v
LinearManifoldWitness
#if !MIN_VERSION_manifolds_core(0,6,0)
        BoundarylessWitness
#endif
  addTensors :: forall w.
(TensorSpace w, Scalar w ~ Scalar (DualVectorFromBasis v)) =>
(DualVectorFromBasis v ⊗ w)
-> (DualVectorFromBasis v ⊗ w) -> DualVectorFromBasis v ⊗ w
addTensors (Tensor TensorProduct (DualVectorFromBasis v) w
v) (Tensor TensorProduct (DualVectorFromBasis v) w
w) = forall s v w. TensorProduct v w -> Tensor s v w
Tensor forall (f :: * -> * -> *) a b.
(Function f, Object f a, Object f b) =>
f a b -> a -> b
$ forall v. AdditiveGroup v => v -> v -> v
(^+^) forall (f :: * -> *) (r :: * -> * -> *) a b.
(Functor f r (->), Object r a, Object r b) =>
r a b -> f a -> f b
<$> TensorProduct (DualVectorFromBasis v) w
v forall (f :: * -> *) (r :: * -> * -> *) (t :: * -> * -> *) a b.
(Applicative f r t, ObjectMorphism r a b,
 ObjectMorphism t (f a) (f b), Object t (t (f a) (f b)),
 ObjectPair r (r a b) a, ObjectPair t (f (r a b)) (f a), Object r a,
 Object r b) =>
t (f (r a b)) (t (f a) (f b))
<*> TensorProduct (DualVectorFromBasis v) w
w
  subtractTensors :: forall w.
(TensorSpace (DualVectorFromBasis v), TensorSpace w,
 Scalar w ~ Scalar (DualVectorFromBasis v)) =>
(DualVectorFromBasis v ⊗ w)
-> (DualVectorFromBasis v ⊗ w) -> DualVectorFromBasis v ⊗ w
subtractTensors (Tensor TensorProduct (DualVectorFromBasis v) w
v) (Tensor TensorProduct (DualVectorFromBasis v) w
w) = forall s v w. TensorProduct v w -> Tensor s v w
Tensor forall (f :: * -> * -> *) a b.
(Function f, Object f a, Object f b) =>
f a b -> a -> b
$ forall v. AdditiveGroup v => v -> v -> v
(^-^) forall (f :: * -> *) (r :: * -> * -> *) a b.
(Functor f r (->), Object r a, Object r b) =>
r a b -> f a -> f b
<$> TensorProduct (DualVectorFromBasis v) w
v forall (f :: * -> *) (r :: * -> * -> *) (t :: * -> * -> *) a b.
(Applicative f r t, ObjectMorphism r a b,
 ObjectMorphism t (f a) (f b), Object t (t (f a) (f b)),
 ObjectPair r (r a b) a, ObjectPair t (f (r a b)) (f a), Object r a,
 Object r b) =>
t (f (r a b)) (t (f a) (f b))
<*> TensorProduct (DualVectorFromBasis v) w
w
  tensorProduct :: forall w.
(TensorSpace w, Scalar w ~ Scalar (DualVectorFromBasis v)) =>
Bilinear (DualVectorFromBasis v) w (DualVectorFromBasis v ⊗ w)
tensorProduct = forall v w y. (v -> w -> y) -> Bilinear v w y
bilinearFunction
    forall (f :: * -> * -> *) a b.
(Function f, Object f a, Object f b) =>
f a b -> a -> b
$ \DualVectorFromBasis v
v w
w -> forall s v w. TensorProduct v w -> Tensor s v w
Tensor forall κ (k :: κ -> κ -> *) (a :: κ) (b :: κ) (c :: κ).
(Category k, Object k a, Object k b, Object k c) =>
k b c -> k a b -> k a c
. forall a b. HasTrie a => (a -> b) -> a :->: b
trie forall (f :: * -> * -> *) a b.
(Function f, Object f a, Object f b) =>
f a b -> a -> b
$ \Basis v
bv -> forall v. HasBasis v => v -> Basis v -> Scalar v
decompose' DualVectorFromBasis v
v Basis v
bv forall v. VectorSpace v => Scalar v -> v -> v
*^ w
w
  transposeTensor :: forall w.
(TensorSpace w, Scalar w ~ Scalar (DualVectorFromBasis v)) =>
(DualVectorFromBasis v ⊗ w) -+> (w ⊗ DualVectorFromBasis v)
transposeTensor = forall s v w. (v -> w) -> LinearFunction s v w
LinearFunction forall (f :: * -> * -> *) a b.
(Function f, Object f a, Object f b) =>
f a b -> a -> b
$ \(Tensor TensorProduct (DualVectorFromBasis v) w
t)
       -> forall (f :: * -> *) v. (Foldable f, AdditiveGroup v) => f v -> v
sumV [ (forall v w.
(TensorSpace v, TensorSpace w, Scalar w ~ Scalar v) =>
Bilinear v w (v ⊗ w)
tensorProductforall s v w. LinearFunction s v w -> v -> w
-+$>w
w)forall s v w. LinearFunction s v w -> v -> w
-+$>forall v. HasBasis v => Basis v -> v
basisValue Basis v
b
               | (Basis v
b,w
w) <- forall a b. HasTrie a => (a :->: b) -> [(a, b)]
enumerate TensorProduct (DualVectorFromBasis v) w
t ]
  fmapTensor :: forall w x.
(TensorSpace w, TensorSpace x,
 Scalar w ~ Scalar (DualVectorFromBasis v),
 Scalar x ~ Scalar (DualVectorFromBasis v)) =>
Bilinear
  (w -+> x) (DualVectorFromBasis v ⊗ w) (DualVectorFromBasis v ⊗ x)
fmapTensor = forall v w y. (v -> w -> y) -> Bilinear v w y
bilinearFunction
    forall (f :: * -> * -> *) a b.
(Function f, Object f a, Object f b) =>
f a b -> a -> b
$ \(LinearFunction w -> x
f) (Tensor TensorProduct (DualVectorFromBasis v) w
t)
         -> forall s v w. TensorProduct v w -> Tensor s v w
Tensor forall (f :: * -> * -> *) a b.
(Function f, Object f a, Object f b) =>
f a b -> a -> b
$ forall (f :: * -> *) (r :: * -> * -> *) (t :: * -> * -> *) a b.
(Functor f r t, Object r a, Object t (f a), Object r b,
 Object t (f b)) =>
r a b -> t (f a) (f b)
fmap w -> x
f TensorProduct (DualVectorFromBasis v) w
t
  fzipTensorWith :: forall u w x.
(TensorSpace u, TensorSpace w, TensorSpace x,
 Scalar u ~ Scalar (DualVectorFromBasis v),
 Scalar w ~ Scalar (DualVectorFromBasis v),
 Scalar x ~ Scalar (DualVectorFromBasis v)) =>
Bilinear
  ((w, x) -+> u)
  (DualVectorFromBasis v ⊗ w, DualVectorFromBasis v ⊗ x)
  (DualVectorFromBasis v ⊗ u)
fzipTensorWith = forall v w y. (v -> w -> y) -> Bilinear v w y
bilinearFunction
    forall (f :: * -> * -> *) a b.
(Function f, Object f a, Object f b) =>
f a b -> a -> b
$ \(LinearFunction (w, x) -> u
f) (Tensor TensorProduct (DualVectorFromBasis v) w
tv, Tensor TensorProduct (DualVectorFromBasis v) x
tw)
         -> forall s v w. TensorProduct v w -> Tensor s v w
Tensor forall (f :: * -> * -> *) a b.
(Function f, Object f a, Object f b) =>
f a b -> a -> b
$ forall (f :: * -> *) (r :: * -> * -> *) (t :: * -> * -> *) c b a.
(Applicative f r t, Object r c, ObjectMorphism r b c,
 Object t (f c), ObjectMorphism t (f b) (f c), ObjectPair r a b,
 ObjectPair t (f a) (f b)) =>
r a (r b c) -> t (f a) (t (f b) (f c))
liftA2 (forall (k :: * -> * -> *) a b c.
(Curry k, ObjectPair k a b, ObjectMorphism k b c) =>
k (a, b) c -> k a (k b c)
curry (w, x) -> u
f) TensorProduct (DualVectorFromBasis v) w
tv TensorProduct (DualVectorFromBasis v) x
tw
  coerceFmapTensorProduct :: forall (p :: * -> *) a b.
Functor p =>
p (DualVectorFromBasis v)
-> VSCCoercion a b
-> VSCCoercion
     (TensorProduct (DualVectorFromBasis v) a)
     (TensorProduct (DualVectorFromBasis v) b)
coerceFmapTensorProduct p (DualVectorFromBasis v)
_ VSCCoercion a b
VSCCoercion
    = forall a. HasCallStack => [Char] -> a
error [Char]
"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 :: DualSpaceWitness (DualVectorFromBasis v)
dualSpaceWitness = case forall s. Num' s => ClosedScalarWitness s
closedScalarWitness @(Scalar v) of
    ClosedScalarWitness (Scalar v)
ClosedScalarWitness -> forall v.
(LinearSpace (Scalar v), DualVector (Scalar v) ~ Scalar v,
 LinearSpace (DualVector v), Scalar (DualVector v) ~ Scalar v,
 DualVector (DualVector v) ~ v) =>
DualSpaceWitness v
DualSpaceWitness
  linearId :: DualVectorFromBasis v +> DualVectorFromBasis v
linearId = forall v w φ.
BasisGeneratedSpace v =>
((TensorProduct v w ~ (Basis v :->: w)) => φ) -> φ
proveTensorProductIsTrie @v @(DualVectorFromBasis v)
     (forall s v w. TensorProduct (DualVector v) w -> LinearMap s v w
LinearMap forall κ (k :: κ -> κ -> *) (a :: κ) (b :: κ) (c :: κ).
(Category k, Object k a, Object k b, Object k c) =>
k b c -> k a b -> k a c
. forall a b. HasTrie a => (a -> b) -> a :->: b
trie forall (f :: * -> * -> *) a b.
(Function f, Object f a, Object f b) =>
f a b -> a -> b
$ forall v. v -> DualVectorFromBasis v
DualVectorFromBasis forall κ (k :: κ -> κ -> *) (a :: κ) (b :: κ) (c :: κ).
(Category k, Object k a, Object k b, Object k c) =>
k b c -> k a b -> k a c
. forall v. HasBasis v => Basis v -> v
basisValue)
  tensorId :: forall w.
(LinearSpace w, Scalar w ~ Scalar (DualVectorFromBasis v)) =>
(DualVectorFromBasis v ⊗ w) +> (DualVectorFromBasis v ⊗ w)
tensorId = forall w.
(LinearSpace w, Scalar w ~ Scalar v) =>
(DualVectorFromBasis v ⊗ w) +> (DualVectorFromBasis v ⊗ w)
tid
   where tid :: ∀ w . (LinearSpace w, Scalar w ~ Scalar v)
           => (DualVectorFromBasis v⊗w) +> (DualVectorFromBasis v⊗w)
         tid :: forall w.
(LinearSpace w, Scalar w ~ Scalar v) =>
(DualVectorFromBasis v ⊗ w) +> (DualVectorFromBasis v ⊗ w)
tid = forall v w φ.
BasisGeneratedSpace v =>
((TensorProduct v w ~ (Basis v :->: w)) => φ) -> φ
proveTensorProductIsTrie @v @(DualVector w⊗(DualVectorFromBasis v⊗w))
                    ( case forall v. LinearSpace v => DualSpaceWitness v
dualSpaceWitness @w of
          DualSpaceWitness w
DualSpaceWitness -> forall s v w. TensorProduct (DualVector v) w -> LinearMap s v w
LinearMap forall κ (k :: κ -> κ -> *) (a :: κ) (b :: κ) (c :: κ).
(Category k, Object k a, Object k b, Object k c) =>
k b c -> k a b -> k a c
. forall a b. HasTrie a => (a -> b) -> a :->: b
trie forall (f :: * -> * -> *) a b.
(Function f, Object f a, Object f b) =>
f a b -> a -> b
$ forall s v w. TensorProduct v w -> Tensor s v w
Tensor forall κ (k :: κ -> κ -> *) (a :: κ) (b :: κ) (c :: κ).
(Category k, Object k a, Object k b, Object k c) =>
k b c -> k a b -> k a c
. \Basis v
i
           -> forall s v w. Tensor s v w -> TensorProduct v w
getTensorProduct forall (f :: * -> * -> *) a b.
(Function f, Object f a, Object f b) =>
f a b -> a -> b
$
             (forall v w x.
(TensorSpace v, TensorSpace w, TensorSpace x, Scalar w ~ Scalar v,
 Scalar x ~ Scalar v) =>
Bilinear (w -+> x) (v ⊗ w) (v ⊗ x)
fmapTensor @(DualVector w)
                 forall s v w. LinearFunction s v w -> v -> w
-+$>(forall s v w. (v -> w) -> LinearFunction s v w
LinearFunction forall (f :: * -> * -> *) a b.
(Function f, Object f a, Object f b) =>
f a b -> a -> b
$ \w
w -> forall s v w. TensorProduct v w -> Tensor s v w
Tensor forall κ (k :: κ -> κ -> *) (a :: κ) (b :: κ) (c :: κ).
(Category k, Object k a, Object k b, Object k c) =>
k b c -> k a b -> k a c
. forall a b. HasTrie a => (a -> b) -> a :->: b
trie
                              forall (f :: * -> * -> *) a b.
(Function f, Object f a, Object f b) =>
f a b -> a -> b
$ (\Basis v
j -> if Basis v
iforall a. Eq a => a -> a -> Bool
==Basis v
j then w
w else forall v. AdditiveGroup v => v
zeroV)
                               :: DualVectorFromBasis v⊗w))
              forall s v w. LinearFunction s v w -> v -> w
-+$> case forall v. LinearSpace v => v +> v
linearId @w of
                    LinearMap TensorProduct (DualVector w) w
lw -> forall s v w. TensorProduct v w -> Tensor s v w
Tensor TensorProduct (DualVector w) w
lw :: DualVector w⊗w )
  applyDualVector :: LinearSpace (DualVectorFromBasis v) =>
Bilinear
  (DualVector (DualVectorFromBasis v))
  (DualVectorFromBasis v)
  (Scalar (DualVectorFromBasis v))
applyDualVector = forall v w φ.
BasisGeneratedSpace v =>
((TensorProduct v w ~ (Basis v :->: w)) => φ) -> φ
proveTensorProductIsTrie @v @(DualVectorFromBasis v)
     ( forall v w y. (v -> w -> y) -> Bilinear v w y
bilinearFunction forall (f :: * -> * -> *) a b.
(Function f, Object f a, Object f b) =>
f a b -> a -> b
$ \v
f (DualVectorFromBasis v
v)
          -> forall (t :: * -> *) a. (Foldable t, Num a) => t a -> a
sum [forall v. HasBasis v => v -> Basis v -> Scalar v
decompose' v
f Basis v
i forall a. Num a => a -> a -> a
* Scalar v
vi | (Basis v
i,Scalar v
vi) <- forall v. HasBasis v => v -> [(Basis v, Scalar v)]
decompose v
v] )
  applyLinear :: forall w.
(TensorSpace w, Scalar w ~ Scalar (DualVectorFromBasis v)) =>
Bilinear (DualVectorFromBasis v +> w) (DualVectorFromBasis v) w
applyLinear = forall w.
(TensorSpace w, Scalar w ~ Scalar v) =>
Bilinear (DualVectorFromBasis v +> w) (DualVectorFromBasis v) w
ali
   where ali :: ∀ w . (TensorSpace w, Scalar w~Scalar v)
           => Bilinear (DualVectorFromBasis v +> w) (DualVectorFromBasis v) w
         ali :: forall w.
(TensorSpace w, Scalar w ~ Scalar v) =>
Bilinear (DualVectorFromBasis v +> w) (DualVectorFromBasis v) w
ali = forall v w φ.
BasisGeneratedSpace v =>
((TensorProduct v w ~ (Basis v :->: w)) => φ) -> φ
proveTensorProductIsTrie @v @w ( forall v w y. (v -> w -> y) -> Bilinear v w y
bilinearFunction
            forall (f :: * -> * -> *) a b.
(Function f, Object f a, Object f b) =>
f a b -> a -> b
$ \(LinearMap TensorProduct (DualVector (DualVectorFromBasis v)) w
f) (DualVectorFromBasis v
v)
                -> forall (f :: * -> *) v. (Foldable f, AdditiveGroup v) => f v -> v
sumV [Scalar v
vi forall v. VectorSpace v => Scalar v -> v -> v
*^ forall a b. HasTrie a => (a :->: b) -> a -> b
untrie TensorProduct (DualVector (DualVectorFromBasis v)) w
f Basis v
i | (Basis v
i,Scalar v
vi) <- forall v. HasBasis v => v -> [(Basis v, Scalar v)]
decompose v
v] )
  applyTensorFunctional :: forall u.
(LinearSpace u, Scalar u ~ Scalar (DualVectorFromBasis v)) =>
Bilinear
  (DualVector (DualVectorFromBasis v ⊗ u))
  (DualVectorFromBasis v ⊗ u)
  (Scalar (DualVectorFromBasis v))
applyTensorFunctional = forall u.
(LinearSpace u, Scalar u ~ Scalar v) =>
Bilinear
  (DualVector (DualVectorFromBasis v ⊗ u))
  (DualVectorFromBasis v ⊗ u)
  (Scalar v)
atf
   where atf :: ∀ u . (LinearSpace u, Scalar u ~ Scalar v)
          => Bilinear (DualVector (DualVectorFromBasis v ⊗ u))
                         (DualVectorFromBasis v ⊗ u) (Scalar v)
         atf :: forall u.
(LinearSpace u, Scalar u ~ Scalar v) =>
Bilinear
  (DualVector (DualVectorFromBasis v ⊗ u))
  (DualVectorFromBasis v ⊗ u)
  (Scalar v)
atf = forall v w φ.
BasisGeneratedSpace v =>
((TensorProduct v w ~ (Basis v :->: w)) => φ) -> φ
proveTensorProductIsTrie @v @(DualVector u) (case forall v. LinearSpace v => DualSpaceWitness v
dualSpaceWitness @u of
          DualSpaceWitness u
DualSpaceWitness -> forall v w y. (v -> w -> y) -> Bilinear v w y
bilinearFunction
           forall (f :: * -> * -> *) a b.
(Function f, Object f a, Object f b) =>
f a b -> a -> b
$ \(LinearMap TensorProduct (DualVector (DualVectorFromBasis v)) (DualVector u)
f) (Tensor TensorProduct (DualVectorFromBasis v) u
t)
             -> forall (t :: * -> *) a. (Foldable t, Num a) => t a -> a
sum [ (forall v.
(LinearSpace v, LinearSpace v) =>
Bilinear (DualVector v) v (Scalar v)
applyDualVectorforall s v w. LinearFunction s v w -> v -> w
-+$>DualVector u
fi)forall s v w. LinearFunction s v w -> v -> w
-+$>forall a b. HasTrie a => (a :->: b) -> a -> b
untrie TensorProduct (DualVectorFromBasis v) u
t Basis v
i
                    | (Basis v
i, DualVector u
fi) <- forall a b. HasTrie a => (a :->: b) -> [(a, b)]
enumerate TensorProduct (DualVector (DualVectorFromBasis v)) (DualVector u)
f ]
               )
  applyTensorLinMap :: forall u w.
(LinearSpace u, TensorSpace w,
 Scalar u ~ Scalar (DualVectorFromBasis v),
 Scalar w ~ Scalar (DualVectorFromBasis v)) =>
Bilinear
  ((DualVectorFromBasis v ⊗ u) +> w) (DualVectorFromBasis v ⊗ u) w
applyTensorLinMap = forall u w.
(LinearSpace u, TensorSpace w, Scalar u ~ Scalar v,
 Scalar w ~ Scalar v) =>
Bilinear
  ((DualVectorFromBasis v ⊗ u) +> w) (DualVectorFromBasis v ⊗ u) w
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 :: forall u w.
(LinearSpace u, TensorSpace w, Scalar u ~ Scalar v,
 Scalar w ~ Scalar v) =>
Bilinear
  ((DualVectorFromBasis v ⊗ u) +> w) (DualVectorFromBasis v ⊗ u) w
atlm = forall v w φ.
BasisGeneratedSpace v =>
((TensorProduct v w ~ (Basis v :->: w)) => φ) -> φ
proveTensorProductIsTrie @v @(DualVector u⊗w) (
          case forall v. LinearSpace v => DualSpaceWitness v
dualSpaceWitness @u of
           DualSpaceWitness u
DualSpaceWitness -> forall v w y. (v -> w -> y) -> Bilinear v w y
bilinearFunction
             forall (f :: * -> * -> *) a b.
(Function f, Object f a, Object f b) =>
f a b -> a -> b
$ \(LinearMap TensorProduct
  (DualVector (Tensor (Scalar v) (DualVectorFromBasis v) u)) w
f) (Tensor TensorProduct (DualVectorFromBasis v) u
t)
              -> forall (f :: * -> *) v. (Foldable f, AdditiveGroup v) => f v -> v
sumV [ (forall v w.
(LinearSpace v, TensorSpace w, Scalar w ~ Scalar v) =>
Bilinear (v +> w) v w
applyLinearforall s v w. LinearFunction s v w -> v -> w
-+$>(forall s v w. TensorProduct (DualVector v) w -> LinearMap s v w
LinearMap TensorProduct (DualVector u) w
fi :: u+>w))
                         forall s v w. LinearFunction s v w -> v -> w
-+$> forall a b. HasTrie a => (a :->: b) -> a -> b
untrie TensorProduct (DualVectorFromBasis v) u
t Basis v
i
                      | (Basis v
i, Tensor TensorProduct (DualVector u) w
fi) <- forall a b. HasTrie a => (a :->: b) -> [(a, b)]
enumerate TensorProduct
  (DualVector (Tensor (Scalar v) (DualVectorFromBasis v) u)) w
f ]
          )
  useTupleLinearSpaceComponents :: forall x y φ.
(DualVectorFromBasis v ~ (x, y)) =>
((LinearSpace x, LinearSpace y, Scalar x ~ Scalar y) => φ) -> φ
useTupleLinearSpaceComponents (LinearSpace x, LinearSpace y, Scalar x ~ Scalar y) => φ
_ = forall a. a
usingNonTupleTypeAsTupleError


zipWith' :: (a -> b -> c) -> [a] -> [b] -> ([c], [b])
zipWith' :: forall a b c. (a -> b -> c) -> [a] -> [b] -> ([c], [b])
zipWith' a -> b -> c
_ [a]
_ [] = ([], [])
zipWith' a -> b -> c
_ [] [b]
ys = ([], [b]
ys)
zipWith' a -> b -> c
f (a
x:[a]
xs) (b
y:[b]
ys) = forall (a :: * -> * -> *) b d c.
(Morphism a, ObjectPair a b d, ObjectPair a c d) =>
a b c -> a (b, d) (c, d)
first (a -> b -> c
f a
x b
y forall a. a -> [a] -> [a]
:) forall (f :: * -> * -> *) a b.
(Function f, Object f a, Object f b) =>
f a b -> a -> b
$ forall a b c. (a -> b -> c) -> [a] -> [b] -> ([c], [b])
zipWith' a -> b -> c
f [a]
xs [b]
ys

zipConsumeWith' :: (a -> [b] -> (c,[b])) -> [a] -> [b] -> ([c], [b])
zipConsumeWith' :: forall a b c. (a -> [b] -> (c, [b])) -> [a] -> [b] -> ([c], [b])
zipConsumeWith' a -> [b] -> (c, [b])
_ [a]
_ [] = ([], [])
zipConsumeWith' a -> [b] -> (c, [b])
_ [] [b]
ys = ([], [b]
ys)
zipConsumeWith' a -> [b] -> (c, [b])
f (a
x:[a]
xs) [b]
ys
    = case a -> [b] -> (c, [b])
f a
x [b]
ys of
       (c
z, [b]
ys') -> forall (a :: * -> * -> *) b d c.
(Morphism a, ObjectPair a b d, ObjectPair a c d) =>
a b c -> a (b, d) (c, d)
first (c
z forall a. a -> [a] -> [a]
:) forall (f :: * -> * -> *) a b.
(Function f, Object f a, Object f b) =>
f a b -> a -> b
$ forall a b c. (a -> [b] -> (c, [b])) -> [a] -> [b] -> ([c], [b])
zipConsumeWith' a -> [b] -> (c, [b])
f [a]
xs [b]
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 :: SubBasis (DualVectorFromBasis v)
entireBasis = forall v. SubBasis (DualVectorFromBasis v)
CompleteDualVBasis
  enumerateSubBasis :: SubBasis (DualVectorFromBasis v) -> [DualVectorFromBasis v]
enumerateSubBasis SubBasis (DualVectorFromBasis v)
R:SubBasisDualVectorFromBasis v
CompleteDualVBasis
      = forall v. HasBasis v => Basis v -> v
basisValue forall κ (k :: κ -> κ -> *) (a :: κ) (b :: κ) (c :: κ).
(Category k, Object k a, Object k b, Object k c) =>
k b c -> k a b -> k a c
. forall (a :: * -> * -> *) x y.
(PreArrow a, ObjectPair a x y) =>
a (x, y) x
fst forall (f :: * -> *) (r :: * -> * -> *) a b.
(Functor f r (->), Object r a, Object r b) =>
r a b -> f a -> f b
<$> forall a b. HasTrie a => (a :->: b) -> [(a, b)]
enumerate (forall a b. HasTrie a => (a -> b) -> a :->: b
trie forall (f :: * -> * -> *) a b.
(Function f, Object f a, Object f b) =>
f a b -> a -> b
$ forall (a :: * -> * -> *) b x.
(WellPointed a, Object a b, ObjectPoint a x) =>
x -> a b x
const ())
  tensorEquality :: forall w.
(TensorSpace w, Eq w, Scalar w ~ Scalar (DualVectorFromBasis v)) =>
(DualVectorFromBasis v ⊗ w) -> (DualVectorFromBasis v ⊗ w) -> Bool
tensorEquality (Tensor TensorProduct (DualVectorFromBasis v) w
t) (Tensor TensorProduct (DualVectorFromBasis v) w
t')
      = forall (t :: * -> *). Foldable t => t Bool -> Bool
and [w
ti forall a. Eq a => a -> a -> Bool
== forall a b. HasTrie a => (a :->: b) -> a -> b
untrie TensorProduct (DualVectorFromBasis v) w
t' Basis v
i | (Basis v
i,w
ti) <- forall a b. HasTrie a => (a :->: b) -> [(a, b)]
enumerate TensorProduct (DualVectorFromBasis v) w
t]
  decomposeLinMap :: forall w.
(LSpace w, Scalar w ~ Scalar (DualVectorFromBasis v)) =>
(DualVectorFromBasis v +> w)
-> (SubBasis (DualVectorFromBasis v), DList w)
decomposeLinMap = forall w.
(DualVectorFromBasis v +> w)
-> (SubBasis (DualVectorFromBasis v), [w] -> [w])
dlm
   where dlm :: ∀ w . (DualVectorFromBasis v+>w)
               -> (SubBasis (DualVectorFromBasis v), [w]->[w])
         dlm :: forall w.
(DualVectorFromBasis v +> w)
-> (SubBasis (DualVectorFromBasis v), [w] -> [w])
dlm (LinearMap TensorProduct (DualVector (DualVectorFromBasis v)) w
f) = forall v w φ.
BasisGeneratedSpace v =>
((TensorProduct v w ~ (Basis v :->: w)) => φ) -> φ
proveTensorProductIsTrie @v @w
                 ( forall v. SubBasis (DualVectorFromBasis v)
CompleteDualVBasis
                 , (forall a b. (a -> b) -> [a] -> [b]
map forall (a :: * -> * -> *) x y.
(PreArrow a, ObjectPair a x y) =>
a (x, y) y
snd (forall a b. HasTrie a => (a :->: b) -> [(a, b)]
enumerate TensorProduct (DualVector (DualVectorFromBasis v)) w
f) forall a. [a] -> [a] -> [a]
++) )
  decomposeLinMapWithin :: forall w.
(LSpace w, Scalar w ~ Scalar (DualVectorFromBasis v)) =>
SubBasis (DualVectorFromBasis v)
-> (DualVectorFromBasis v +> w)
-> Either (SubBasis (DualVectorFromBasis v), DList w) (DList w)
decomposeLinMapWithin = forall w.
SubBasis (DualVectorFromBasis v)
-> (DualVectorFromBasis v +> w)
-> Either
     (SubBasis (DualVectorFromBasis v), [w] -> [w]) ([w] -> [w])
dlm
   where dlm :: ∀ w . SubBasis (DualVectorFromBasis v)
                -> (DualVectorFromBasis v+>w)
                -> Either (SubBasis (DualVectorFromBasis v), [w]->[w])
                          ([w]->[w])
         dlm :: forall w.
SubBasis (DualVectorFromBasis v)
-> (DualVectorFromBasis v +> w)
-> Either
     (SubBasis (DualVectorFromBasis v), [w] -> [w]) ([w] -> [w])
dlm SubBasis (DualVectorFromBasis v)
R:SubBasisDualVectorFromBasis v
CompleteDualVBasis (LinearMap TensorProduct (DualVector (DualVectorFromBasis v)) w
f) = forall v w φ.
BasisGeneratedSpace v =>
((TensorProduct v w ~ (Basis v :->: w)) => φ) -> φ
proveTensorProductIsTrie @v @w
                 (forall a b. b -> Either a b
Right (forall a b. (a -> b) -> [a] -> [b]
map forall (a :: * -> * -> *) x y.
(PreArrow a, ObjectPair a x y) =>
a (x, y) y
snd (forall a b. HasTrie a => (a :->: b) -> [(a, b)]
enumerate TensorProduct (DualVector (DualVectorFromBasis v)) w
f) forall a. [a] -> [a] -> [a]
++) )
  recomposeSB :: SubBasis (DualVectorFromBasis v)
-> [Scalar (DualVectorFromBasis v)]
-> (DualVectorFromBasis v, [Scalar (DualVectorFromBasis v)])
recomposeSB = SubBasis (DualVectorFromBasis v)
-> [Scalar v] -> (DualVectorFromBasis v, [Scalar v])
rsb
   where rsb :: SubBasis (DualVectorFromBasis v)
                -> [Scalar v]
                -> (DualVectorFromBasis v, [Scalar v])
         rsb :: SubBasis (DualVectorFromBasis v)
-> [Scalar v] -> (DualVectorFromBasis v, [Scalar v])
rsb SubBasis (DualVectorFromBasis v)
R:SubBasisDualVectorFromBasis v
CompleteDualVBasis [Scalar v]
cs = forall (a :: * -> * -> *) b d c.
(Morphism a, ObjectPair a b d, ObjectPair a c d) =>
a b c -> a (b, d) (c, d)
first forall v. HasBasis v => [(Basis v, Scalar v)] -> v
recompose
                   forall (f :: * -> * -> *) a b.
(Function f, Object f a, Object f b) =>
f a b -> a -> b
$ forall a b c. (a -> b -> c) -> [a] -> [b] -> ([c], [b])
zipWith' (,) (forall (a :: * -> * -> *) x y.
(PreArrow a, ObjectPair a x y) =>
a (x, y) x
fst forall (f :: * -> *) (r :: * -> * -> *) a b.
(Functor f r (->), Object r a, Object r b) =>
r a b -> f a -> f b
<$> forall a b. HasTrie a => (a :->: b) -> [(a, b)]
enumerate (forall a b. HasTrie a => (a -> b) -> a :->: b
trie forall (f :: * -> * -> *) a b.
(Function f, Object f a, Object f b) =>
f a b -> a -> b
$ forall (a :: * -> * -> *) b x.
(WellPointed a, Object a b, ObjectPoint a x) =>
x -> a b x
const ())) [Scalar v]
cs
  recomposeSBTensor :: forall w.
(FiniteDimensional w, Scalar w ~ Scalar (DualVectorFromBasis v)) =>
SubBasis (DualVectorFromBasis v)
-> SubBasis w
-> [Scalar (DualVectorFromBasis v)]
-> (DualVectorFromBasis v ⊗ w, [Scalar (DualVectorFromBasis v)])
recomposeSBTensor = forall w.
(FiniteDimensional w, Scalar w ~ Scalar v) =>
SubBasis (DualVectorFromBasis v)
-> SubBasis w
-> [Scalar v]
-> (DualVectorFromBasis v ⊗ w, [Scalar v])
rsbt
   where rsbt :: ∀ w . (FiniteDimensional w, Scalar w ~ Scalar v)
             => SubBasis (DualVectorFromBasis v) -> SubBasis w
                -> [Scalar v]
                -> (DualVectorFromBasis v⊗w, [Scalar v])
         rsbt :: forall w.
(FiniteDimensional w, Scalar w ~ Scalar v) =>
SubBasis (DualVectorFromBasis v)
-> SubBasis w
-> [Scalar v]
-> (DualVectorFromBasis v ⊗ w, [Scalar v])
rsbt SubBasis (DualVectorFromBasis v)
R:SubBasisDualVectorFromBasis v
CompleteDualVBasis SubBasis w
sbw [Scalar v]
ws = forall v w φ.
BasisGeneratedSpace v =>
((TensorProduct v w ~ (Basis v :->: w)) => φ) -> φ
proveTensorProductIsTrie @v @w
                 (forall (a :: * -> * -> *) b d c.
(Morphism a, ObjectPair a b d, ObjectPair a c d) =>
a b c -> a (b, d) (c, d)
first (\[(Basis v, w)]
iws -> forall s v w. TensorProduct v w -> Tensor s v w
Tensor forall (f :: * -> * -> *) a b.
(Function f, Object f a, Object f b) =>
f a b -> a -> b
$ forall a b. HasTrie a => (a -> b) -> a :->: b
trie (forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList [(Basis v, w)]
iws forall k a. Ord k => Map k a -> k -> a
Map.!))
                   forall (f :: * -> * -> *) a b.
(Function f, Object f a, Object f b) =>
f a b -> a -> b
$ forall a b c. (a -> [b] -> (c, [b])) -> [a] -> [b] -> ([c], [b])
zipConsumeWith' (\Basis v
i [Scalar v]
cs' -> forall (a :: * -> * -> *) b d c.
(Morphism a, ObjectPair a b d, ObjectPair a c d) =>
a b c -> a (b, d) (c, d)
first (Basis v
i,) forall (f :: * -> * -> *) a b.
(Function f, Object f a, Object f b) =>
f a b -> a -> b
$ forall v.
FiniteDimensional v =>
SubBasis v -> [Scalar v] -> (v, [Scalar v])
recomposeSB SubBasis w
sbw [Scalar v]
cs')
                         (forall (a :: * -> * -> *) x y.
(PreArrow a, ObjectPair a x y) =>
a (x, y) x
fst forall (f :: * -> *) (r :: * -> * -> *) a b.
(Functor f r (->), Object r a, Object r b) =>
r a b -> f a -> f b
<$> forall a b. HasTrie a => (a :->: b) -> [(a, b)]
enumerate (forall a b. HasTrie a => (a -> b) -> a :->: b
trie forall (f :: * -> * -> *) a b.
(Function f, Object f a, Object f b) =>
f a b -> a -> b
$ forall (a :: * -> * -> *) b x.
(WellPointed a, Object a b, ObjectPoint a x) =>
x -> a b x
const ())) [Scalar v]
ws)
  recomposeLinMap :: forall w.
(LSpace w, Scalar w ~ Scalar (DualVectorFromBasis v)) =>
SubBasis (DualVectorFromBasis v)
-> [w] -> (DualVectorFromBasis v +> w, [w])
recomposeLinMap = forall w.
SubBasis (DualVectorFromBasis v)
-> [w] -> (DualVectorFromBasis v +> w, [w])
rlm
   where rlm :: ∀ w . SubBasis (DualVectorFromBasis v)
                -> [w]
                -> (DualVectorFromBasis v+>w, [w])
         rlm :: forall w.
SubBasis (DualVectorFromBasis v)
-> [w] -> (DualVectorFromBasis v +> w, [w])
rlm SubBasis (DualVectorFromBasis v)
R:SubBasisDualVectorFromBasis v
CompleteDualVBasis [w]
ws = forall v w φ.
BasisGeneratedSpace v =>
((TensorProduct v w ~ (Basis v :->: w)) => φ) -> φ
proveTensorProductIsTrie @v @w
                 (forall (a :: * -> * -> *) b d c.
(Morphism a, ObjectPair a b d, ObjectPair a c d) =>
a b c -> a (b, d) (c, d)
first (\[(Basis v, w)]
iws -> forall s v w. TensorProduct (DualVector v) w -> LinearMap s v w
LinearMap forall (f :: * -> * -> *) a b.
(Function f, Object f a, Object f b) =>
f a b -> a -> b
$ forall a b. HasTrie a => (a -> b) -> a :->: b
trie (forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList [(Basis v, w)]
iws forall k a. Ord k => Map k a -> k -> a
Map.!))
                   forall (f :: * -> * -> *) a b.
(Function f, Object f a, Object f b) =>
f a b -> a -> b
$ forall a b c. (a -> b -> c) -> [a] -> [b] -> ([c], [b])
zipWith' (,) (forall (a :: * -> * -> *) x y.
(PreArrow a, ObjectPair a x y) =>
a (x, y) x
fst forall (f :: * -> *) (r :: * -> * -> *) a b.
(Functor f r (->), Object r a, Object r b) =>
r a b -> f a -> f b
<$> forall a b. HasTrie a => (a :->: b) -> [(a, b)]
enumerate (forall a b. HasTrie a => (a -> b) -> a :->: b
trie forall (f :: * -> * -> *) a b.
(Function f, Object f a, Object f b) =>
f a b -> a -> b
$ forall (a :: * -> * -> *) b x.
(WellPointed a, Object a b, ObjectPoint a x) =>
x -> a b x
const ())) [w]
ws)
  recomposeContraLinMap :: forall w (f :: * -> *).
(LinearSpace w, Scalar w ~ Scalar (DualVectorFromBasis v),
 Functor f) =>
(f (Scalar w) -> w)
-> f (DualVector (DualVectorFromBasis v))
-> DualVectorFromBasis v +> w
recomposeContraLinMap = forall w (f :: * -> *).
(LinearSpace w, Scalar w ~ Scalar v, Functor f) =>
(f (Scalar w) -> w) -> f v -> DualVectorFromBasis v +> w
rclm
   where rclm :: ∀ w f . (LinearSpace w, Scalar w ~ Scalar v, Hask.Functor f)
              => (f (Scalar w) -> w) -> f v
                -> (DualVectorFromBasis v+>w)
         rclm :: forall w (f :: * -> *).
(LinearSpace w, Scalar w ~ Scalar v, Functor f) =>
(f (Scalar w) -> w) -> f v -> DualVectorFromBasis v +> w
rclm f (Scalar w) -> w
f f v
vs = forall v w φ.
BasisGeneratedSpace v =>
((TensorProduct v w ~ (Basis v :->: w)) => φ) -> φ
proveTensorProductIsTrie @v @w
               (forall s v w. TensorProduct (DualVector v) w -> LinearMap s v w
LinearMap forall (f :: * -> * -> *) a b.
(Function f, Object f a, Object f b) =>
f a b -> a -> b
$ forall a b. HasTrie a => (a -> b) -> a :->: b
trie (\Basis v
i -> f (Scalar w) -> w
f forall (f :: * -> * -> *) a b.
(Function f, Object f a, Object f b) =>
f a b -> a -> b
$ forall (f :: * -> *) (r :: * -> * -> *) (t :: * -> * -> *) a b.
(Functor f r t, Object r a, Object t (f a), Object r b,
 Object t (f b)) =>
r a b -> t (f a) (f b)
fmap (forall v. HasBasis v => v -> Basis v -> Scalar v
`decompose'`Basis v
i) f v
vs))
  recomposeContraLinMapTensor :: forall u w (f :: * -> *).
(FiniteDimensional u, LinearSpace w,
 Scalar u ~ Scalar (DualVectorFromBasis v),
 Scalar w ~ Scalar (DualVectorFromBasis v), Functor f) =>
(f (Scalar w) -> w)
-> f (DualVectorFromBasis v +> DualVector u)
-> (DualVectorFromBasis v ⊗ u) +> w
recomposeContraLinMapTensor = forall u w (f :: * -> *).
(FiniteDimensional u, LinearSpace w, Scalar u ~ Scalar v,
 Scalar w ~ Scalar v, Functor f) =>
(f (Scalar w) -> w)
-> f (DualVectorFromBasis v +> DualVector u)
-> (DualVectorFromBasis v ⊗ u) +> w
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 :: forall u w (f :: * -> *).
(FiniteDimensional u, LinearSpace w, Scalar u ~ Scalar v,
 Scalar w ~ Scalar v, Functor f) =>
(f (Scalar w) -> w)
-> f (DualVectorFromBasis v +> DualVector u)
-> (DualVectorFromBasis v ⊗ u) +> w
rclm f (Scalar w) -> w
f f (DualVectorFromBasis v +> DualVector u)
vus = case forall v. LinearSpace v => DualSpaceWitness v
dualSpaceWitness @u of
           DualSpaceWitness u
DualSpaceWitness -> forall v w φ.
BasisGeneratedSpace v =>
((TensorProduct v w ~ (Basis v :->: w)) => φ) -> φ
proveTensorProductIsTrie @v @(DualVector u)
                      (forall v w φ.
BasisGeneratedSpace v =>
((TensorProduct v w ~ (Basis v :->: w)) => φ) -> φ
proveTensorProductIsTrie @v @(DualVector u⊗w)
               (forall s v w. TensorProduct (DualVector v) w -> LinearMap s v w
LinearMap forall (f :: * -> * -> *) a b.
(Function f, Object f a, Object f b) =>
f a b -> a -> b
$ forall a b. HasTrie a => (a -> b) -> a :->: b
trie
                   (\Basis v
i -> case forall v w (f :: * -> *).
(FiniteDimensional v, LinearSpace w, Scalar w ~ Scalar v,
 Functor f) =>
(f (Scalar w) -> w) -> f (DualVector v) -> v +> w
recomposeContraLinMap @u @w @f f (Scalar w) -> w
f
                              forall (f :: * -> * -> *) a b.
(Function f, Object f a, Object f b) =>
f a b -> a -> b
$ forall (f :: * -> *) (r :: * -> * -> *) (t :: * -> * -> *) a b.
(Functor f r t, Object r a, Object t (f a), Object r b,
 Object t (f b)) =>
r a b -> t (f a) (f b)
fmap (\(LinearMap TensorProduct (DualVector (DualVectorFromBasis v)) (DualVector u)
vu) -> forall a b. HasTrie a => (a :->: b) -> a -> b
untrie TensorProduct (DualVector (DualVectorFromBasis v)) (DualVector u)
vu (Basis v
i :: Basis v)) f (DualVectorFromBasis v +> DualVector u)
vus of
                      LinearMap TensorProduct (DualVector u) w
wuff -> forall s v w. TensorProduct v w -> Tensor s v w
Tensor TensorProduct (DualVector u) w
wuff :: DualVector u⊗w )))
  uncanonicallyFromDual :: DualVector (DualVectorFromBasis v) -+> DualVectorFromBasis v
uncanonicallyFromDual = forall s v w. (v -> w) -> LinearFunction s v w
LinearFunction forall v. v -> DualVectorFromBasis v
DualVectorFromBasis
  uncanonicallyToDual :: DualVectorFromBasis v -+> DualVector (DualVectorFromBasis v)
uncanonicallyToDual = forall s v w. (v -> w) -> LinearFunction s v w
LinearFunction forall v. DualVectorFromBasis v -> v
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 :: [(Int, DualVectorFromBasis v)]
-> Forest (Int, DualVector (DualVectorFromBasis v))
dualBasisCandidates = forall v.
[DualVector v]
-> (v -> [ℝ]) -> [(Int, v)] -> Forest (Int, DualVector v)
cartesianDualBasisCandidates
          (forall v. FiniteDimensional v => SubBasis v -> [v]
enumerateSubBasis forall v. FiniteDimensional v => SubBasis v
entireBasis)
          (\DualVectorFromBasis v
v -> forall a b. (a -> b) -> [a] -> [b]
map (forall a. Num a => a -> a
abs forall κ (k :: κ -> κ -> *) (a :: κ) (b :: κ) (c :: κ).
(Category k, Object k a, Object k b, Object k c) =>
k b c -> k a b -> k a c
. forall a b. (Real a, Fractional b) => a -> b
realToFrac forall κ (k :: κ -> κ -> *) (a :: κ) (b :: κ) (c :: κ).
(Category k, Object k a, Object k b, Object k c) =>
k b c -> k a b -> k a c
. forall v. HasBasis v => v -> Basis v -> Scalar v
decompose' DualVectorFromBasis v
v forall κ (k :: κ -> κ -> *) (a :: κ) (b :: κ) (c :: κ).
(Category k, Object k a, Object k b, Object k c) =>
k b c -> k a b -> k a c
. forall (a :: * -> * -> *) x y.
(PreArrow a, ObjectPair a x y) =>
a (x, y) x
fst)
                  forall (f :: * -> * -> *) a b.
(Function f, Object f a, Object f b) =>
f a b -> a -> b
$ forall a b. HasTrie a => (a :->: b) -> [(a, b)]
enumerate (forall a b. HasTrie a => (a -> b) -> a :->: b
trie forall (f :: * -> * -> *) a b.
(Function f, Object f a, Object f b) =>
f a b -> a -> b
$ forall (a :: * -> * -> *) b x.
(WellPointed a, Object a b, ObjectPoint a x) =>
x -> a b x
const ()) )


newtype AbstractDualVector a c
           = AbstractDualVector_ { forall a c. AbstractDualVector a c -> DualVector c
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
    :: VSCCoercion (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 :: forall v ρ.
AbstractLinearSpace v =>
((Scalar (VectorSpaceImplementation v) ~ Scalar v,
  Scalar (DualVector v) ~ Scalar v,
  Scalar (DualVector (VectorSpaceImplementation v)) ~ Scalar v) =>
 ρ)
-> ρ
scalarsSameInAbstractionAndDuals (Scalar (VectorSpaceImplementation v) ~ Scalar v,
 Scalar (DualVector v) ~ Scalar v,
 Scalar (DualVector (VectorSpaceImplementation v)) ~ Scalar v) =>
ρ
φ
     = case forall v. LinearSpace v => DualSpaceWitness v
dualSpaceWitness @(VectorSpaceImplementation v) of
        DualSpaceWitness (VectorSpaceImplementation v)
DualSpaceWitness -> forall v ρ.
AbstractVectorSpace v =>
((Scalar (VectorSpaceImplementation v) ~ Scalar v) => ρ) -> ρ
scalarsSameInAbstraction @v (Scalar (VectorSpaceImplementation v) ~ Scalar v,
 Scalar (DualVector v) ~ Scalar v,
 Scalar (DualVector (VectorSpaceImplementation v)) ~ Scalar v) =>
ρ
φ

abstractDualVectorCoercion :: ∀ a
   . VSCCoercion (AbstractDualVector a (VectorSpaceImplementation a))
              (DualVector (VectorSpaceImplementation a))
abstractDualVectorCoercion :: forall a.
VSCCoercion
  (AbstractDualVector a (VectorSpaceImplementation a))
  (DualVector (VectorSpaceImplementation a))
abstractDualVectorCoercion = forall a b. Coercible a b => VSCCoercion a b
VSCCoercion

abstractTensorsCoercion :: ∀ a c w
  . ( AbstractVectorSpace a, LinearSpace c
    , c ~ VectorSpaceImplementation a, TensorSpace w )
      => VSCCoercion (AbstractDualVector a c⊗w) (DualVector c⊗w)
abstractTensorsCoercion :: forall a c w.
(AbstractVectorSpace a, LinearSpace c,
 c ~ VectorSpaceImplementation a, TensorSpace w) =>
VSCCoercion (AbstractDualVector a c ⊗ w) (DualVector c ⊗ w)
abstractTensorsCoercion = forall a b. Coercible a b => VSCCoercion a b
VSCCoercion

abstractLinmapCoercion :: ∀ a c w
  . ( AbstractLinearSpace a, LinearSpace c
    , c ~ VectorSpaceImplementation a, TensorSpace w )
      => VSCCoercion (AbstractDualVector a c+>w) (DualVector c+>w)
abstractLinmapCoercion :: forall a c w.
(AbstractLinearSpace a, LinearSpace c,
 c ~ VectorSpaceImplementation a, TensorSpace w) =>
VSCCoercion (AbstractDualVector a c +> w) (DualVector c +> w)
abstractLinmapCoercion = case ( forall v. LinearSpace v => DualSpaceWitness v
dualSpaceWitness @c
                              , forall v w.
AbstractTensorSpace v =>
VSCCoercion
  (TensorProduct v w) (TensorProduct (VectorSpaceImplementation v) w)
abstractTensorProductsCoercion @a @w ) of
   (DualSpaceWitness c
DualSpaceWitness, VSCCoercion (TensorProduct a w) (TensorProduct c w)
VSCCoercion) -> forall a b. Coercible a b => VSCCoercion a b
VSCCoercion

coerceLinearMapCodomain :: ∀ v w x . ( LinearSpace v, Coercible w x )
         => (v+>w) -> (v+>x)
coerceLinearMapCodomain :: forall v w x. (LinearSpace v, Coercible w x) => (v +> w) -> v +> x
coerceLinearMapCodomain = case forall v. LinearSpace v => DualSpaceWitness v
dualSpaceWitness @v of
 DualSpaceWitness v
DualSpaceWitness -> \(LinearMap TensorProduct (DualVector v) w
m)
     -> forall s v w. TensorProduct (DualVector v) w -> LinearMap s v w
LinearMap forall (f :: * -> * -> *) a b.
(Function f, Object f a, Object f b) =>
f a b -> a -> b
$ (forall v (p :: * -> *) a b.
(TensorSpace v, Functor p) =>
p v
-> VSCCoercion a b
-> VSCCoercion (TensorProduct v a) (TensorProduct v b)
coerceFmapTensorProduct ([]::[DualVector v])
                            (forall a b. Coercible a b => VSCCoercion a b
VSCCoercion :: VSCCoercion w x) forall (f :: * -> * -> *) a b.
(Function f, Object f a, Object f b) =>
f a b -> a -> b
$ TensorProduct (DualVector v) w
m)

instance (Show (DualVector c)) => Show (AbstractDualVector a c) where
  showsPrec :: Int -> AbstractDualVector a c -> ShowS
showsPrec Int
p (AbstractDualVector_ DualVector c
φ) = Bool -> ShowS -> ShowS
showParen (Int
pforall a. Ord a => a -> a -> Bool
>Int
10)
       forall (f :: * -> * -> *) a b.
(Function f, Object f a, Object f b) =>
f a b -> a -> b
$ ([Char]
"AbstractDualVector "forall a. [a] -> [a] -> [a]
++) forall κ (k :: κ -> κ -> *) (a :: κ) (b :: κ) (c :: κ).
(Category k, Object k a, Object k b, Object k c) =>
k b c -> k a b -> k a c
. forall a. Show a => Int -> a -> ShowS
showsPrec Int
11 DualVector c
φ

instance ∀ a c . ( AbstractLinearSpace a, VectorSpaceImplementation a ~ c
                 , AdditiveGroup (DualVector c) )
     => AdditiveGroup (AbstractDualVector a c) where
  zeroV :: AbstractDualVector a c
zeroV = forall v.
AbstractLinearSpace v =>
DualVector (VectorSpaceImplementation v) -> DualVector v
AbstractDualVector forall v. AdditiveGroup v => v
zeroV
  ^+^ :: AbstractDualVector a c
-> AbstractDualVector a c -> AbstractDualVector a c
(^+^) = coerce :: forall a b. Coercible a b => a -> b
coerce (forall v. AdditiveGroup v => v -> v -> v
(^+^) @(DualVector c))
  negateV :: AbstractDualVector a c -> AbstractDualVector a c
negateV = coerce :: forall a b. Coercible a b => a -> b
coerce (forall v. AdditiveGroup v => v -> v
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
  .+^ :: AbstractDualVector a c
-> Diff (AbstractDualVector a c) -> AbstractDualVector a c
(.+^) = coerce :: forall a b. Coercible a b => a -> b
coerce (forall v. AdditiveGroup v => v -> v -> v
(^+^) @(DualVector c))
  .-. :: AbstractDualVector a c
-> AbstractDualVector a c -> Diff (AbstractDualVector a c)
(.-.) = coerce :: forall a b. Coercible a b => a -> b
coerce (forall v. AdditiveGroup v => v -> v -> v
(^-^) @(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
  .+~^ :: AbstractDualVector a c
-> Needle (AbstractDualVector a c) -> AbstractDualVector a c
(.+~^) = forall v. AdditiveGroup v => v -> v -> v
(^+^)
#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
  AbstractDualVector a c
v.-~. :: AbstractDualVector a c
-> AbstractDualVector a c
-> Maybe (Needle (AbstractDualVector a c))
.-~.AbstractDualVector a c
w = forall (f :: * -> *) (r :: * -> * -> *) (t :: * -> * -> *) a.
(Applicative f r t, Object r a, Object t (f a)) =>
t a (f a)
pure (AbstractDualVector a c
vforall v. AdditiveGroup v => v -> v -> v
^-^AbstractDualVector a c
w)
  .-~! :: HasCallStack =>
AbstractDualVector a c
-> AbstractDualVector a c -> Needle (AbstractDualVector a c)
(.-~!) = forall v. AdditiveGroup v => v -> v -> v
(^-^)

instance ∀ a c . ( AbstractLinearSpace a, VectorSpaceImplementation a ~ c
                 , VectorSpace (DualVector c) )
     => VectorSpace (AbstractDualVector a c) where
  type Scalar (AbstractDualVector a c) = Scalar a
  *^ :: Scalar (AbstractDualVector a c)
-> AbstractDualVector a c -> AbstractDualVector a c
(*^) = forall v ρ.
AbstractLinearSpace v =>
((Scalar (VectorSpaceImplementation v) ~ Scalar v,
  Scalar (DualVector v) ~ Scalar v,
  Scalar (DualVector (VectorSpaceImplementation v)) ~ Scalar v) =>
 ρ)
-> ρ
scalarsSameInAbstractionAndDuals @a (coerce :: forall a b. Coercible a b => a -> b
coerce (forall v. VectorSpace v => Scalar v -> v -> v
(*^) @(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 :: ScalarSpaceWitness (AbstractDualVector a c)
scalarSpaceWitness = forall v ρ.
AbstractLinearSpace v =>
((Scalar (VectorSpaceImplementation v) ~ Scalar v,
  Scalar (DualVector v) ~ Scalar v,
  Scalar (DualVector (VectorSpaceImplementation v)) ~ Scalar v) =>
 ρ)
-> ρ
scalarsSameInAbstractionAndDuals @a
     (case forall v. TensorSpace v => ScalarSpaceWitness v
scalarSpaceWitness @(DualVector c) of ScalarSpaceWitness (DualVector c)
ScalarSpaceWitness -> forall v.
(Num' (Scalar v), Scalar (Scalar v) ~ Scalar v) =>
ScalarSpaceWitness v
ScalarSpaceWitness)
  linearManifoldWitness :: LinearManifoldWitness (AbstractDualVector a c)
linearManifoldWitness = forall v ρ.
AbstractLinearSpace v =>
((Scalar (VectorSpaceImplementation v) ~ Scalar v,
  Scalar (DualVector v) ~ Scalar v,
  Scalar (DualVector (VectorSpaceImplementation v)) ~ Scalar v) =>
 ρ)
-> ρ
scalarsSameInAbstractionAndDuals @a
     (case forall v. TensorSpace v => LinearManifoldWitness v
linearManifoldWitness @(DualVector c) of
#if MIN_VERSION_manifolds_core(0,6,0)
       LinearManifoldWitness (DualVector c)
LinearManifoldWitness -> forall v.
(Needle v ~ v, AffineSpace v, Diff v ~ v) =>
LinearManifoldWitness v
LinearManifoldWitness
#else
       LinearManifoldWitness BoundarylessWitness
          -> LinearManifoldWitness BoundarylessWitness
#endif
         )
  zeroTensor :: forall w.
(TensorSpace w, Scalar w ~ Scalar (AbstractDualVector a c)) =>
AbstractDualVector a c ⊗ w
zeroTensor = forall w.
(TensorSpace w, Scalar w ~ Scalar a) =>
AbstractDualVector a c ⊗ w
zt
   where zt :: ∀ w . (TensorSpace w, Scalar w ~ Scalar a)
            => (AbstractDualVector a c ⊗ w)
         zt :: forall w.
(TensorSpace w, Scalar w ~ Scalar a) =>
AbstractDualVector a c ⊗ w
zt = forall v ρ.
AbstractLinearSpace v =>
((Scalar (VectorSpaceImplementation v) ~ Scalar v,
  Scalar (DualVector v) ~ Scalar v,
  Scalar (DualVector (VectorSpaceImplementation v)) ~ Scalar v) =>
 ρ)
-> ρ
scalarsSameInAbstractionAndDuals @a
                (coerce :: forall a b. Coercible a b => a -> b
coerce (forall v w.
(TensorSpace v, TensorSpace w, Scalar w ~ Scalar v) =>
v ⊗ w
zeroTensor @(DualVector c) @w))
  addTensors :: forall w.
(TensorSpace w, Scalar w ~ Scalar (AbstractDualVector a c)) =>
(AbstractDualVector a c ⊗ w)
-> (AbstractDualVector a c ⊗ w) -> AbstractDualVector a c ⊗ w
addTensors = forall w.
(TensorSpace w, Scalar w ~ Scalar a) =>
(AbstractDualVector a c ⊗ w)
-> (AbstractDualVector a c ⊗ w) -> AbstractDualVector a c ⊗ w
at
   where at :: ∀ w . (TensorSpace w, Scalar w ~ Scalar a)
            => (AbstractDualVector a c ⊗ w) -> (AbstractDualVector a c ⊗ w)
                                            -> (AbstractDualVector a c ⊗ w)
         at :: forall w.
(TensorSpace w, Scalar w ~ Scalar a) =>
(AbstractDualVector a c ⊗ w)
-> (AbstractDualVector a c ⊗ w) -> AbstractDualVector a c ⊗ w
at = forall v ρ.
AbstractLinearSpace v =>
((Scalar (VectorSpaceImplementation v) ~ Scalar v,
  Scalar (DualVector v) ~ Scalar v,
  Scalar (DualVector (VectorSpaceImplementation v)) ~ Scalar v) =>
 ρ)
-> ρ
scalarsSameInAbstractionAndDuals @a
                (coerce :: forall a b. Coercible a b => a -> b
coerce (forall v w.
(TensorSpace v, TensorSpace w, Scalar w ~ Scalar v) =>
(v ⊗ w) -> (v ⊗ w) -> v ⊗ w
addTensors @(DualVector c) @w))
  subtractTensors :: forall w.
(TensorSpace (AbstractDualVector a c), TensorSpace w,
 Scalar w ~ Scalar (AbstractDualVector a c)) =>
(AbstractDualVector a c ⊗ w)
-> (AbstractDualVector a c ⊗ w) -> AbstractDualVector a c ⊗ w
subtractTensors = forall w.
(TensorSpace w, Scalar w ~ Scalar a) =>
(AbstractDualVector a c ⊗ w)
-> (AbstractDualVector a c ⊗ w) -> AbstractDualVector a c ⊗ w
st
   where st :: ∀ w . (TensorSpace w, Scalar w ~ Scalar a)
            => (AbstractDualVector a c ⊗ w) -> (AbstractDualVector a c ⊗ w)
                                            -> (AbstractDualVector a c ⊗ w)
         st :: forall w.
(TensorSpace w, Scalar w ~ Scalar a) =>
(AbstractDualVector a c ⊗ w)
-> (AbstractDualVector a c ⊗ w) -> AbstractDualVector a c ⊗ w
st = forall v ρ.
AbstractLinearSpace v =>
((Scalar (VectorSpaceImplementation v) ~ Scalar v,
  Scalar (DualVector v) ~ Scalar v,
  Scalar (DualVector (VectorSpaceImplementation v)) ~ Scalar v) =>
 ρ)
-> ρ
scalarsSameInAbstractionAndDuals @a
                (coerce :: forall a b. Coercible a b => a -> b
coerce (forall v w.
(TensorSpace v, TensorSpace v, TensorSpace w,
 Scalar w ~ Scalar v) =>
(v ⊗ w) -> (v ⊗ w) -> v ⊗ w
subtractTensors @(DualVector c) @w))
  negateTensor :: forall w.
(TensorSpace w, Scalar w ~ Scalar (AbstractDualVector a c)) =>
(AbstractDualVector a c ⊗ w) -+> (AbstractDualVector a c ⊗ w)
negateTensor = forall w.
(TensorSpace w, Scalar w ~ Scalar a) =>
(AbstractDualVector a c ⊗ w) -+> (AbstractDualVector a c ⊗ w)
nt
   where nt :: ∀ w . (TensorSpace w, Scalar w ~ Scalar a)
            => (AbstractDualVector a c ⊗ w) -+> (AbstractDualVector a c ⊗ w)
         nt :: forall w.
(TensorSpace w, Scalar w ~ Scalar a) =>
(AbstractDualVector a c ⊗ w) -+> (AbstractDualVector a c ⊗ w)
nt = forall v ρ.
AbstractLinearSpace v =>
((Scalar (VectorSpaceImplementation v) ~ Scalar v,
  Scalar (DualVector v) ~ Scalar v,
  Scalar (DualVector (VectorSpaceImplementation v)) ~ Scalar v) =>
 ρ)
-> ρ
scalarsSameInAbstractionAndDuals @a
                (coerce :: forall a b. Coercible a b => a -> b
coerce (forall v w.
(TensorSpace v, TensorSpace w, Scalar w ~ Scalar v) =>
(v ⊗ w) -+> (v ⊗ w)
negateTensor @(DualVector c) @w))
  scaleTensor :: forall w.
(TensorSpace w, Scalar w ~ Scalar (AbstractDualVector a c)) =>
Bilinear
  (Scalar (AbstractDualVector a c))
  (AbstractDualVector a c ⊗ w)
  (AbstractDualVector a c ⊗ w)
scaleTensor = forall w.
(TensorSpace w, Scalar w ~ Scalar a) =>
Bilinear
  (Scalar a)
  (AbstractDualVector a c ⊗ w)
  (AbstractDualVector a c ⊗ w)
st
   where st :: ∀ w . (TensorSpace w, Scalar w ~ Scalar a)
            => Bilinear (Scalar a) (AbstractDualVector a c ⊗ w)
                                   (AbstractDualVector a c ⊗ w)
         st :: forall w.
(TensorSpace w, Scalar w ~ Scalar a) =>
Bilinear
  (Scalar a)
  (AbstractDualVector a c ⊗ w)
  (AbstractDualVector a c ⊗ w)
st = forall v ρ.
AbstractLinearSpace v =>
((Scalar (VectorSpaceImplementation v) ~ Scalar v,
  Scalar (DualVector v) ~ Scalar v,
  Scalar (DualVector (VectorSpaceImplementation v)) ~ Scalar v) =>
 ρ)
-> ρ
scalarsSameInAbstractionAndDuals @a
                (coerce :: forall a b. Coercible a b => a -> b
coerce (forall v w.
(TensorSpace v, TensorSpace w, Scalar w ~ Scalar v) =>
Bilinear (Scalar v) (v ⊗ w) (v ⊗ w)
scaleTensor @(DualVector c) @w))
  toFlatTensor :: AbstractDualVector a c
-+> (AbstractDualVector a c ⊗ Scalar (AbstractDualVector a c))
toFlatTensor = forall v ρ.
AbstractLinearSpace v =>
((Scalar (VectorSpaceImplementation v) ~ Scalar v,
  Scalar (DualVector v) ~ Scalar v,
  Scalar (DualVector (VectorSpaceImplementation v)) ~ Scalar v) =>
 ρ)
-> ρ
scalarsSameInAbstractionAndDuals @a
                    ( coerce :: forall a b. Coercible a b => a -> b
coerce (forall v. TensorSpace v => v -+> (v ⊗ Scalar v)
toFlatTensor @(DualVector c)) )
  fromFlatTensor :: (AbstractDualVector a c ⊗ Scalar (AbstractDualVector a c))
-+> AbstractDualVector a c
fromFlatTensor = forall v ρ.
AbstractLinearSpace v =>
((Scalar (VectorSpaceImplementation v) ~ Scalar v,
  Scalar (DualVector v) ~ Scalar v,
  Scalar (DualVector (VectorSpaceImplementation v)) ~ Scalar v) =>
 ρ)
-> ρ
scalarsSameInAbstractionAndDuals @a
                    ( coerce :: forall a b. Coercible a b => a -> b
coerce (forall v. TensorSpace v => (v ⊗ Scalar v) -+> v
fromFlatTensor @(DualVector c)) )
  tensorProduct :: forall w.
(TensorSpace w, Scalar w ~ Scalar (AbstractDualVector a c)) =>
Bilinear (AbstractDualVector a c) w (AbstractDualVector a c ⊗ w)
tensorProduct = forall w.
(TensorSpace w, Scalar w ~ Scalar a) =>
Bilinear (AbstractDualVector a c) w (AbstractDualVector a c ⊗ w)
tp
   where tp :: ∀ w . (TensorSpace w, Scalar w ~ Scalar a)
            => Bilinear (AbstractDualVector a c) w
                                   (AbstractDualVector a c ⊗ w)
         tp :: forall w.
(TensorSpace w, Scalar w ~ Scalar a) =>
Bilinear (AbstractDualVector a c) w (AbstractDualVector a c ⊗ w)
tp = forall v ρ.
AbstractLinearSpace v =>
((Scalar (VectorSpaceImplementation v) ~ Scalar v,
  Scalar (DualVector v) ~ Scalar v,
  Scalar (DualVector (VectorSpaceImplementation v)) ~ Scalar v) =>
 ρ)
-> ρ
scalarsSameInAbstractionAndDuals @a
                (coerce :: forall a b. Coercible a b => a -> b
coerce (forall v w.
(TensorSpace v, TensorSpace w, Scalar w ~ Scalar v) =>
Bilinear v w (v ⊗ w)
tensorProduct @(DualVector c) @w))
  wellDefinedVector :: AbstractDualVector a c -> Maybe (AbstractDualVector a c)
wellDefinedVector (AbstractDualVector DualVector (VectorSpaceImplementation a)
v) = forall v.
AbstractLinearSpace v =>
DualVector (VectorSpaceImplementation v) -> DualVector v
AbstractDualVector forall (f :: * -> *) (r :: * -> * -> *) a b.
(Functor f r (->), Object r a, Object r b) =>
r a b -> f a -> f b
<$> forall v. TensorSpace v => v -> Maybe v
wellDefinedVector DualVector (VectorSpaceImplementation a)
v
  wellDefinedTensor :: forall w.
(TensorSpace w, Scalar w ~ Scalar (AbstractDualVector a c)) =>
(AbstractDualVector a c ⊗ w) -> Maybe (AbstractDualVector a c ⊗ w)
wellDefinedTensor = forall w.
(TensorSpace w, Scalar w ~ Scalar a) =>
(AbstractDualVector a c ⊗ w) -> Maybe (AbstractDualVector a c ⊗ w)
wdt
   where wdt :: ∀ w . (TensorSpace w, Scalar w ~ Scalar a)
            => (AbstractDualVector a c ⊗ w) -> Maybe (AbstractDualVector a c ⊗ w)
         wdt :: forall w.
(TensorSpace w, Scalar w ~ Scalar a) =>
(AbstractDualVector a c ⊗ w) -> Maybe (AbstractDualVector a c ⊗ w)
wdt = forall v ρ.
AbstractLinearSpace v =>
((Scalar (VectorSpaceImplementation v) ~ Scalar v,
  Scalar (DualVector v) ~ Scalar v,
  Scalar (DualVector (VectorSpaceImplementation v)) ~ Scalar v) =>
 ρ)
-> ρ
scalarsSameInAbstractionAndDuals @a
                (coerce :: forall a b. Coercible a b => a -> b
coerce (forall v w.
(TensorSpace v, TensorSpace w, Scalar w ~ Scalar v) =>
(v ⊗ w) -> Maybe (v ⊗ w)
wellDefinedTensor @(DualVector c) @w))
  transposeTensor :: forall w.
(TensorSpace w, Scalar w ~ Scalar (AbstractDualVector a c)) =>
(AbstractDualVector a c ⊗ w) -+> (w ⊗ AbstractDualVector a c)
transposeTensor = forall v ρ.
AbstractLinearSpace v =>
((Scalar (VectorSpaceImplementation v) ~ Scalar v,
  Scalar (DualVector v) ~ Scalar v,
  Scalar (DualVector (VectorSpaceImplementation v)) ~ Scalar v) =>
 ρ)
-> ρ
scalarsSameInAbstractionAndDuals @a forall w.
(TensorSpace w, Scalar w ~ Scalar a,
 Scalar (DualVector c) ~ Scalar a) =>
(AbstractDualVector a c ⊗ w) -+> (w ⊗ AbstractDualVector a c)
tt
   where tt :: ∀ w . ( TensorSpace w, Scalar w ~ Scalar a
                     , Scalar (DualVector c) ~ Scalar a )
            => (AbstractDualVector a c ⊗ w) -+> (w ⊗ AbstractDualVector a c)
         tt :: forall w.
(TensorSpace w, Scalar w ~ Scalar a,
 Scalar (DualVector c) ~ Scalar a) =>
(AbstractDualVector a c ⊗ w) -+> (w ⊗ AbstractDualVector a c)
tt = case forall v (p :: * -> *) a b.
(TensorSpace v, Functor p) =>
p v
-> VSCCoercion a b
-> VSCCoercion (TensorProduct v a) (TensorProduct v b)
coerceFmapTensorProduct @w []
                       (forall a b. Coercible a b => VSCCoercion a b
VSCCoercion @(DualVector c) @(AbstractDualVector a c)) of
             VSCCoercion
  (TensorProduct w (DualVector c))
  (TensorProduct w (AbstractDualVector a c))
VSCCoercion -> coerce :: forall a b. Coercible a b => a -> b
coerce (forall v w.
(TensorSpace v, TensorSpace w, Scalar w ~ Scalar v) =>
(v ⊗ w) -+> (w ⊗ v)
transposeTensor @(DualVector c) @w)
  fmapTensor :: forall w x.
(TensorSpace w, TensorSpace x,
 Scalar w ~ Scalar (AbstractDualVector a c),
 Scalar x ~ Scalar (AbstractDualVector a c)) =>
Bilinear
  (w -+> x) (AbstractDualVector a c ⊗ w) (AbstractDualVector a c ⊗ x)
fmapTensor = forall 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
   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 :: forall 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 = forall v ρ.
AbstractLinearSpace v =>
((Scalar (VectorSpaceImplementation v) ~ Scalar v,
  Scalar (DualVector v) ~ Scalar v,
  Scalar (DualVector (VectorSpaceImplementation v)) ~ Scalar v) =>
 ρ)
-> ρ
scalarsSameInAbstractionAndDuals @a
                 (coerce :: forall a b. Coercible a b => a -> b
coerce forall (f :: * -> * -> *) a b.
(Function f, Object f a, Object f b) =>
f a b -> a -> b
$ forall v w x.
(TensorSpace v, TensorSpace w, TensorSpace x, Scalar w ~ Scalar v,
 Scalar x ~ Scalar v) =>
Bilinear (w -+> x) (v ⊗ w) (v ⊗ x)
fmapTensor @(DualVector c) @w @x)
  fzipTensorWith :: forall u w x.
(TensorSpace u, TensorSpace w, TensorSpace x,
 Scalar u ~ Scalar (AbstractDualVector a c),
 Scalar w ~ Scalar (AbstractDualVector a c),
 Scalar x ~ Scalar (AbstractDualVector a c)) =>
Bilinear
  ((w, x) -+> u)
  (AbstractDualVector a c ⊗ w, AbstractDualVector a c ⊗ x)
  (AbstractDualVector a c ⊗ u)
fzipTensorWith = forall 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
   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 :: forall 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 = forall v ρ.
AbstractLinearSpace v =>
((Scalar (VectorSpaceImplementation v) ~ Scalar v,
  Scalar (DualVector v) ~ Scalar v,
  Scalar (DualVector (VectorSpaceImplementation v)) ~ Scalar v) =>
 ρ)
-> ρ
scalarsSameInAbstractionAndDuals @a
                 (coerce :: forall a b. Coercible a b => a -> b
coerce forall (f :: * -> * -> *) a b.
(Function f, Object f a, Object f b) =>
f a b -> a -> b
$ forall v u w x.
(TensorSpace v, TensorSpace u, TensorSpace w, TensorSpace x,
 Scalar u ~ Scalar v, Scalar w ~ Scalar v, Scalar x ~ Scalar v) =>
Bilinear ((w, x) -+> u) (v ⊗ w, v ⊗ x) (v ⊗ u)
fzipTensorWith @(DualVector c) @u @w @x)
  coerceFmapTensorProduct :: forall (p :: * -> *) a b.
Functor p =>
p (AbstractDualVector a c)
-> VSCCoercion a b
-> VSCCoercion
     (TensorProduct (AbstractDualVector a c) a)
     (TensorProduct (AbstractDualVector a c) b)
coerceFmapTensorProduct p (AbstractDualVector a c)
_ = forall v (p :: * -> *) a b.
(TensorSpace v, Functor p) =>
p v
-> VSCCoercion a b
-> VSCCoercion (TensorProduct v a) (TensorProduct v b)
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 :: forall 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 (TensorSpace (AbstractDualVector a c), LinearSpace (DualVector c),
 Scalar (DualVector c) ~ Scalar a) =>
r
φ = case forall v. LinearSpace v => DualSpaceWitness v
dualSpaceWitness @c of
   DualSpaceWitness c
DualSpaceWitness -> forall v ρ.
AbstractVectorSpace v =>
((Scalar (VectorSpaceImplementation v) ~ Scalar v) => ρ) -> ρ
scalarsSameInAbstraction @a (TensorSpace (AbstractDualVector a c), LinearSpace (DualVector c),
 Scalar (DualVector c) ~ Scalar a) =>
r
φ

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 :: DualSpaceWitness (AbstractDualVector a c)
dualSpaceWitness = case (forall v. LinearSpace v => DualSpaceWitness v
dualSpaceWitness @c, forall v. TensorSpace v => ScalarSpaceWitness v
scalarSpaceWitness @c) of
    (DualSpaceWitness c
DualSpaceWitness, ScalarSpaceWitness c
ScalarSpaceWitness)
        -> forall v ρ.
AbstractVectorSpace v =>
((Scalar (VectorSpaceImplementation v) ~ Scalar v) => ρ) -> ρ
scalarsSameInAbstraction @a forall v.
(LinearSpace (Scalar v), DualVector (Scalar v) ~ Scalar v,
 LinearSpace (DualVector v), Scalar (DualVector v) ~ Scalar v,
 DualVector (DualVector v) ~ v) =>
DualSpaceWitness v
DualSpaceWitness
  linearId :: AbstractDualVector a c +> AbstractDualVector a c
linearId = forall 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 @a @c
       (forall a b. VSCCoercion a b -> VSCCoercion b a
symVSC (forall a c w.
(AbstractLinearSpace a, LinearSpace c,
 c ~ VectorSpaceImplementation a, TensorSpace w) =>
VSCCoercion (AbstractDualVector a c +> w) (DualVector c +> w)
abstractLinmapCoercion @a)
           forall (f :: * -> * -> *) a b.
(Function f, Object f a, Object f b) =>
f a b -> a -> b
$ forall v w.
(LinearSpace v, TensorSpace w, Scalar v ~ Scalar w) =>
(v -+> w) -+> (v +> w)
sampleLinearFunction @(DualVector c)
           forall s v w. LinearFunction s v w -> v -> w
-+$> forall w v.
VectorSpace w =>
(v -> w) -> LinearFunction (Scalar v) v w
linearFunction forall v.
AbstractLinearSpace v =>
DualVector (VectorSpaceImplementation v) -> DualVector v
AbstractDualVector)
  tensorId :: forall w.
(LinearSpace w, Scalar w ~ Scalar (AbstractDualVector a c)) =>
(AbstractDualVector a c ⊗ w) +> (AbstractDualVector a c ⊗ w)
tensorId = forall w.
(LinearSpace w, Scalar w ~ Scalar a) =>
(AbstractDualVector a c ⊗ w) +> (AbstractDualVector a c ⊗ w)
tid
   where tid :: ∀ w . (LinearSpace w, Scalar w ~ Scalar a)
            => (AbstractDualVector a c ⊗ w) +> (AbstractDualVector a c ⊗ w) 
         tid :: forall w.
(LinearSpace w, Scalar w ~ Scalar a) =>
(AbstractDualVector a c ⊗ w) +> (AbstractDualVector a c ⊗ w)
tid = case ( forall v. LinearSpace v => DualSpaceWitness v
dualSpaceWitness @w, forall v. LinearSpace v => DualSpaceWitness v
dualSpaceWitness @c ) of
          (DualSpaceWitness w
DualSpaceWitness, DualSpaceWitness c
DualSpaceWitness)
            -> forall 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 @a (
                let LinearMap TensorProduct (DualVector (DualVector c ⊗ w)) (DualVector c ⊗ w)
ida = forall v. LinearSpace v => v +> v
linearId :: (DualVector c ⊗ w) +> (DualVector c ⊗ w)
                in forall s v w. TensorProduct (DualVector v) w -> LinearMap s v w
LinearMap forall (f :: * -> * -> *) a b.
(Function f, Object f a, Object f b) =>
f a b -> a -> b
$ 
                    forall a b. VSCCoercion a b -> VSCCoercion b a
symVSC (forall v w.
AbstractTensorSpace v =>
VSCCoercion
  (TensorProduct v w) (TensorProduct (VectorSpaceImplementation v) w)
abstractTensorProductsCoercion @a
                          @(DualVector w ⊗ (AbstractDualVector a c⊗w)) )
                    forall κ (k :: κ -> κ -> *) (a :: κ) (b :: κ) (c :: κ).
(Category k, Object k a, Object k b, Object k c) =>
k b c -> k a b -> k a c
. forall v (p :: * -> *) a b.
(TensorSpace v, Functor p) =>
p v
-> VSCCoercion a b
-> VSCCoercion (TensorProduct v a) (TensorProduct v b)
coerceFmapTensorProduct ([]::[c ⊗ DualVector w])
                       (forall a b. Coercible a b => VSCCoercion a b
VSCCoercion @(DualVector c ⊗ w) @(AbstractDualVector a c ⊗ w))
                    forall (f :: * -> * -> *) a b.
(Function f, Object f a, Object f b) =>
f a b -> a -> b
$ TensorProduct (DualVector (DualVector c ⊗ w)) (DualVector c ⊗ w)
ida )
  applyDualVector :: LinearSpace (AbstractDualVector a c) =>
Bilinear
  (DualVector (AbstractDualVector a c))
  (AbstractDualVector a c)
  (Scalar (AbstractDualVector a c))
applyDualVector = forall v ρ.
AbstractVectorSpace v =>
((Scalar (VectorSpaceImplementation v) ~ Scalar v) => ρ) -> ρ
scalarsSameInAbstraction @a ( forall v w y. (v -> w -> y) -> Bilinear v w y
bilinearFunction
     forall (f :: * -> * -> *) a b.
(Function f, Object f a, Object f b) =>
f a b -> a -> b
$ \a
v (AbstractDualVector DualVector (VectorSpaceImplementation a)
d) -> (forall v.
(LinearSpace v, LinearSpace v) =>
Bilinear (DualVector v) v (Scalar v)
applyDualVector forall s v w. LinearFunction s v w -> v -> w
-+$> DualVector (VectorSpaceImplementation a)
d)forall s v w. LinearFunction s v w -> v -> w
-+$>(coerce :: forall a b. Coercible a b => a -> b
coerce a
v::c) )
  applyLinear :: forall w.
(TensorSpace w, Scalar w ~ Scalar (AbstractDualVector a c)) =>
Bilinear (AbstractDualVector a c +> w) (AbstractDualVector a c) w
applyLinear = forall 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 @a ( forall s v w. (v -> w) -> LinearFunction s v w
LinearFunction
     forall (f :: * -> * -> *) a b.
(Function f, Object f a, Object f b) =>
f a b -> a -> b
$ \LinearMap (Scalar a) (AbstractDualVector a c) w
f -> (forall v w.
(LinearSpace v, TensorSpace w, Scalar w ~ Scalar v) =>
Bilinear (v +> w) v w
applyLinear forall s v w. LinearFunction s v w -> v -> w
-+$> forall a c w.
(AbstractLinearSpace a, LinearSpace c,
 c ~ VectorSpaceImplementation a, TensorSpace w) =>
VSCCoercion (AbstractDualVector a c +> w) (DualVector c +> w)
abstractLinmapCoercion forall (f :: * -> * -> *) a b.
(Function f, Object f a, Object f b) =>
f a b -> a -> b
$ LinearMap (Scalar a) (AbstractDualVector a c) w
f) forall κ (k :: κ -> κ -> *) (a :: κ) (b :: κ) (c :: κ).
(Category k, Object k a, Object k b, Object k c) =>
k b c -> k a b -> k a c
. forall s v w. (v -> w) -> LinearFunction s v w
LinearFunction coerce :: forall a b. Coercible a b => a -> b
coerce
      )
  applyTensorFunctional :: forall u.
(LinearSpace u, Scalar u ~ Scalar (AbstractDualVector a c)) =>
Bilinear
  (DualVector (AbstractDualVector a c ⊗ u))
  (AbstractDualVector a c ⊗ u)
  (Scalar (AbstractDualVector a c))
applyTensorFunctional = forall u.
(LinearSpace u, Scalar u ~ Scalar a) =>
Bilinear
  (DualVector (AbstractDualVector a c ⊗ u))
  (AbstractDualVector a c ⊗ u)
  (Scalar a)
atf
   where atf :: ∀ u . ( LinearSpace u, Scalar u ~ Scalar a )
                  => Bilinear (DualVector (AbstractDualVector a c⊗u))
                                       (AbstractDualVector a c⊗u) (Scalar a)
         atf :: forall u.
(LinearSpace u, Scalar u ~ Scalar a) =>
Bilinear
  (DualVector (AbstractDualVector a c ⊗ u))
  (AbstractDualVector a c ⊗ u)
  (Scalar a)
atf = case (forall v. TensorSpace v => ScalarSpaceWitness v
scalarSpaceWitness @a, forall v. LinearSpace v => DualSpaceWitness v
dualSpaceWitness @u) of
          (ScalarSpaceWitness a
ScalarSpaceWitness, DualSpaceWitness u
DualSpaceWitness)
            -> forall 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 @a (
                forall s v w. (v -> w) -> LinearFunction s v w
LinearFunction forall (f :: * -> * -> *) a b.
(Function f, Object f a, Object f b) =>
f a b -> a -> b
$ \LinearMap (Scalar a) (AbstractDualVector a c) (DualVector u)
f
                 -> (forall v u.
(LinearSpace v, LinearSpace u, Scalar u ~ Scalar v) =>
Bilinear (DualVector (v ⊗ u)) (v ⊗ u) (Scalar v)
applyTensorFunctional @(DualVector c)
                         forall s v w. LinearFunction s v w -> v -> w
-+$> forall a c w.
(AbstractLinearSpace a, LinearSpace c,
 c ~ VectorSpaceImplementation a, TensorSpace w) =>
VSCCoercion (AbstractDualVector a c +> w) (DualVector c +> w)
abstractLinmapCoercion @a forall (f :: * -> * -> *) a b.
(Function f, Object f a, Object f b) =>
f a b -> a -> b
$ LinearMap (Scalar a) (AbstractDualVector a c) (DualVector u)
f)
                      forall κ (k :: κ -> κ -> *) (a :: κ) (b :: κ) (c :: κ).
(Category k, Object k a, Object k b, Object k c) =>
k b c -> k a b -> k a c
. forall s v w. (v -> w) -> LinearFunction s v w
LinearFunction (forall a c w.
(AbstractVectorSpace a, LinearSpace c,
 c ~ VectorSpaceImplementation a, TensorSpace w) =>
VSCCoercion (AbstractDualVector a c ⊗ w) (DualVector c ⊗ w)
abstractTensorsCoercion @a forall (f :: * -> * -> *) a b.
(Function f, Object f a, Object f b) =>
f a b -> a -> b
$)
              )
  applyTensorLinMap :: forall u w.
(LinearSpace u, TensorSpace w,
 Scalar u ~ Scalar (AbstractDualVector a c),
 Scalar w ~ Scalar (AbstractDualVector a c)) =>
Bilinear
  ((AbstractDualVector a c ⊗ u) +> w) (AbstractDualVector a c ⊗ u) w
applyTensorLinMap = forall 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
   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 :: forall 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 (forall v. LinearSpace v => DualSpaceWitness v
dualSpaceWitness @c, forall v. LinearSpace v => DualSpaceWitness v
dualSpaceWitness @u) of
          (DualSpaceWitness c
DualSpaceWitness, DualSpaceWitness u
DualSpaceWitness)
                      -> forall 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 @a (
             forall s v w. (v -> w) -> LinearFunction s v w
LinearFunction forall (f :: * -> * -> *) a b.
(Function f, Object f a, Object f b) =>
f a b -> a -> b
$ \(LinearMap TensorProduct
  (DualVector (Tensor (Scalar a) (AbstractDualVector a c) u)) w
f) ->
                     let f' :: (DualVector c ⊗ u) +> w
f' = forall s v w. TensorProduct (DualVector v) w -> LinearMap s v w
LinearMap (forall v w.
AbstractTensorSpace v =>
VSCCoercion
  (TensorProduct v w) (TensorProduct (VectorSpaceImplementation v) w)
abstractTensorProductsCoercion
                                           @a @((Tensor (Scalar a) (DualVector u) w))
                                          forall (f :: * -> * -> *) a b.
(Function f, Object f a, Object f b) =>
f a b -> a -> b
$ coerce :: forall a b. Coercible a b => a -> b
coerce TensorProduct
  (DualVector (Tensor (Scalar a) (AbstractDualVector a c) u)) w
f) :: (DualVector c⊗u)+>w
                     in (forall v u w.
(LinearSpace v, LinearSpace u, TensorSpace w, Scalar u ~ Scalar v,
 Scalar w ~ Scalar v) =>
Bilinear ((v ⊗ u) +> w) (v ⊗ u) w
applyTensorLinMap @(DualVector c)forall s v w. LinearFunction s v w -> v -> w
-+$>(DualVector c ⊗ u) +> w
f')
                              forall κ (k :: κ -> κ -> *) (a :: κ) (b :: κ) (c :: κ).
(Category k, Object k a, Object k b, Object k c) =>
k b c -> k a b -> k a c
. forall s v w. (v -> w) -> LinearFunction s v w
LinearFunction (forall a c w.
(AbstractVectorSpace a, LinearSpace c,
 c ~ VectorSpaceImplementation a, TensorSpace w) =>
VSCCoercion (AbstractDualVector a c ⊗ w) (DualVector c ⊗ w)
abstractTensorsCoercion @a forall (f :: * -> * -> *) a b.
(Function f, Object f a, Object f b) =>
f a b -> a -> b
$)
           )
  useTupleLinearSpaceComponents :: forall x y φ.
(AbstractDualVector a c ~ (x, y)) =>
((LinearSpace x, LinearSpace y, Scalar x ~ Scalar y) => φ) -> φ
useTupleLinearSpaceComponents = \(LinearSpace x, LinearSpace y, Scalar x ~ Scalar y) => φ
_ -> forall a. a
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 {
                        forall a c.
SubBasis (AbstractDualVector a c) -> SubBasis (DualVector c)
getAbstractDualVectorSubBasis :: SubBasis (DualVector c) }
  dualFinitenessWitness :: DualFinitenessWitness (AbstractDualVector a c)
dualFinitenessWitness = forall v ρ.
AbstractVectorSpace v =>
((Scalar (VectorSpaceImplementation v) ~ Scalar v) => ρ) -> ρ
scalarsSameInAbstraction @a
       ( case (forall v. TensorSpace v => ScalarSpaceWitness v
scalarSpaceWitness @a, forall v. LinearSpace v => DualSpaceWitness v
dualSpaceWitness @a) of
        (ScalarSpaceWitness a
ScalarSpaceWitness, DualSpaceWitness a
DualSpaceWitness)
            -> forall v.
FiniteDimensional (DualVector v) =>
DualSpaceWitness v -> DualFinitenessWitness v
DualFinitenessWitness forall v.
(LinearSpace (Scalar v), DualVector (Scalar v) ~ Scalar v,
 LinearSpace (DualVector v), Scalar (DualVector v) ~ Scalar v,
 DualVector (DualVector v) ~ v) =>
DualSpaceWitness v
DualSpaceWitness )
  entireBasis :: SubBasis (AbstractDualVector a c)
entireBasis = case forall v. FiniteDimensional v => DualFinitenessWitness v
dualFinitenessWitness @c of
    DualFinitenessWitness DualSpaceWitness c
_ -> coerce :: forall a b. Coercible a b => a -> b
coerce (forall v. FiniteDimensional v => SubBasis v
entireBasis @(DualVector c))
  enumerateSubBasis :: SubBasis (AbstractDualVector a c) -> [AbstractDualVector a c]
enumerateSubBasis = case forall v. FiniteDimensional v => DualFinitenessWitness v
dualFinitenessWitness @c of
    DualFinitenessWitness DualSpaceWitness c
_ 
          -> coerce :: forall a b. Coercible a b => a -> b
coerce (forall v. FiniteDimensional v => SubBasis v -> [v]
enumerateSubBasis @(DualVector c))
  decomposeLinMap :: forall w.
(LSpace w, Scalar w ~ Scalar (AbstractDualVector a c)) =>
(AbstractDualVector a c +> w)
-> (SubBasis (AbstractDualVector a c), DList w)
decomposeLinMap = forall v ρ.
AbstractVectorSpace v =>
((Scalar (VectorSpaceImplementation v) ~ Scalar v) => ρ) -> ρ
scalarsSameInAbstraction @a forall w.
(LSpace w, Scalar w ~ Scalar c) =>
(AbstractDualVector a c +> w)
-> (SubBasis (AbstractDualVector a c), DList w)
dclm
   where dclm :: ∀ w . (LSpace w, Scalar w ~ Scalar c)
            => (AbstractDualVector a c +> w)
                  -> (SubBasis (AbstractDualVector a c), DList w)
         dclm :: forall w.
(LSpace w, Scalar w ~ Scalar c) =>
(AbstractDualVector a c +> w)
-> (SubBasis (AbstractDualVector a c), DList w)
dclm = case (forall v. FiniteDimensional v => DualFinitenessWitness v
dualFinitenessWitness @c, forall v w.
AbstractTensorSpace v =>
VSCCoercion
  (TensorProduct v w) (TensorProduct (VectorSpaceImplementation v) w)
abstractTensorProductsCoercion @a @w) of
          (DualFinitenessWitness DualSpaceWitness c
DualSpaceWitness, VSCCoercion (TensorProduct a w) (TensorProduct c w)
VSCCoercion)
              -> coerce :: forall a b. Coercible a b => a -> b
coerce (forall v w.
(FiniteDimensional v, LSpace w, Scalar w ~ Scalar v) =>
(v +> w) -> (SubBasis v, DList w)
decomposeLinMap @(DualVector c) @w)
  decomposeLinMapWithin :: forall w.
(LSpace w, Scalar w ~ Scalar (AbstractDualVector a c)) =>
SubBasis (AbstractDualVector a c)
-> (AbstractDualVector a c +> w)
-> Either (SubBasis (AbstractDualVector a c), DList w) (DList w)
decomposeLinMapWithin = forall v ρ.
AbstractVectorSpace v =>
((Scalar (VectorSpaceImplementation v) ~ Scalar v) => ρ) -> ρ
scalarsSameInAbstraction @a forall 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
   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 :: forall 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 (forall v. FiniteDimensional v => DualFinitenessWitness v
dualFinitenessWitness @c, forall v w.
AbstractTensorSpace v =>
VSCCoercion
  (TensorProduct v w) (TensorProduct (VectorSpaceImplementation v) w)
abstractTensorProductsCoercion @a @w) of
          (DualFinitenessWitness DualSpaceWitness c
DualSpaceWitness, VSCCoercion (TensorProduct a w) (TensorProduct c w)
VSCCoercion)
              -> coerce :: forall a b. Coercible a b => a -> b
coerce (forall v w.
(FiniteDimensional v, LSpace w, Scalar w ~ Scalar v) =>
SubBasis v -> (v +> w) -> Either (SubBasis v, DList w) (DList w)
decomposeLinMapWithin @(DualVector c) @w)
  recomposeSB :: SubBasis (AbstractDualVector a c)
-> [Scalar (AbstractDualVector a c)]
-> (AbstractDualVector a c, [Scalar (AbstractDualVector a c)])
recomposeSB = case forall v. FiniteDimensional v => DualFinitenessWitness v
dualFinitenessWitness @c of
          DualFinitenessWitness DualSpaceWitness c
DualSpaceWitness -> forall v ρ.
AbstractVectorSpace v =>
((Scalar (VectorSpaceImplementation v) ~ Scalar v) => ρ) -> ρ
scalarsSameInAbstraction @a
                                (coerce :: forall a b. Coercible a b => a -> b
coerce forall (f :: * -> * -> *) a b.
(Function f, Object f a, Object f b) =>
f a b -> a -> b
$ forall v.
FiniteDimensional v =>
SubBasis v -> [Scalar v] -> (v, [Scalar v])
recomposeSB @(DualVector c))
  recomposeSBTensor :: forall w.
(FiniteDimensional w,
 Scalar w ~ Scalar (AbstractDualVector a c)) =>
SubBasis (AbstractDualVector a c)
-> SubBasis w
-> [Scalar (AbstractDualVector a c)]
-> (AbstractDualVector a c ⊗ w, [Scalar (AbstractDualVector a c)])
recomposeSBTensor = forall v ρ.
AbstractVectorSpace v =>
((Scalar (VectorSpaceImplementation v) ~ Scalar v) => ρ) -> ρ
scalarsSameInAbstraction @a forall w.
(FiniteDimensional w, Scalar w ~ Scalar c) =>
SubBasis (AbstractDualVector a c)
-> SubBasis w
-> [Scalar c]
-> (AbstractDualVector a c ⊗ w, [Scalar c])
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 :: forall w.
(FiniteDimensional w, Scalar w ~ Scalar c) =>
SubBasis (AbstractDualVector a c)
-> SubBasis w
-> [Scalar c]
-> (AbstractDualVector a c ⊗ w, [Scalar c])
rst = case forall v. FiniteDimensional v => DualFinitenessWitness v
dualFinitenessWitness @c of
          DualFinitenessWitness DualSpaceWitness c
DualSpaceWitness
                  -> coerce :: forall a b. Coercible a b => a -> b
coerce (forall v w.
(FiniteDimensional v, FiniteDimensional w, Scalar w ~ Scalar v) =>
SubBasis v -> SubBasis w -> [Scalar v] -> (v ⊗ w, [Scalar v])
recomposeSBTensor @(DualVector c) @w)
  recomposeLinMap :: forall w.
(LSpace w, Scalar w ~ Scalar (AbstractDualVector a c)) =>
SubBasis (AbstractDualVector a c)
-> [w] -> (AbstractDualVector a c +> w, [w])
recomposeLinMap = forall v ρ.
AbstractVectorSpace v =>
((Scalar (VectorSpaceImplementation v) ~ Scalar v) => ρ) -> ρ
scalarsSameInAbstraction @a forall w.
(LSpace w, Scalar w ~ Scalar c) =>
SubBasis (AbstractDualVector a c)
-> [w] -> (AbstractDualVector a c +> w, [w])
rlm
   where rlm :: ∀ w . (LSpace w, Scalar w ~ Scalar c)
           => SubBasis (AbstractDualVector a c)
                 -> [w] -> (AbstractDualVector a c +> w, [w])
         rlm :: forall w.
(LSpace w, Scalar w ~ Scalar c) =>
SubBasis (AbstractDualVector a c)
-> [w] -> (AbstractDualVector a c +> w, [w])
rlm = case (forall v. FiniteDimensional v => DualFinitenessWitness v
dualFinitenessWitness @c, forall v w.
AbstractTensorSpace v =>
VSCCoercion
  (TensorProduct v w) (TensorProduct (VectorSpaceImplementation v) w)
abstractTensorProductsCoercion @a @w) of
          (DualFinitenessWitness DualSpaceWitness c
DualSpaceWitness, VSCCoercion (TensorProduct a w) (TensorProduct c w)
VSCCoercion)
              -> coerce :: forall a b. Coercible a b => a -> b
coerce (forall v w.
(FiniteDimensional v, LSpace w, Scalar w ~ Scalar v) =>
SubBasis v -> [w] -> (v +> w, [w])
recomposeLinMap @(DualVector c) @w)
  recomposeContraLinMap :: forall w (f :: * -> *).
(LinearSpace w, Scalar w ~ Scalar (AbstractDualVector a c),
 Functor f) =>
(f (Scalar w) -> w)
-> f (DualVector (AbstractDualVector a c))
-> AbstractDualVector a c +> w
recomposeContraLinMap = forall v ρ.
AbstractVectorSpace v =>
((Scalar (VectorSpaceImplementation v) ~ Scalar v) => ρ) -> ρ
scalarsSameInAbstraction @a forall (f :: * -> *) w.
(LinearSpace w, Scalar w ~ Scalar c, Functor f) =>
(f (Scalar w) -> w) -> f a -> AbstractDualVector a c +> w
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 :: forall (f :: * -> *) w.
(LinearSpace w, Scalar w ~ Scalar c, Functor f) =>
(f (Scalar w) -> w) -> f a -> AbstractDualVector a c +> w
rclm = case (forall v. FiniteDimensional v => DualFinitenessWitness v
dualFinitenessWitness @c, forall v w.
AbstractTensorSpace v =>
VSCCoercion
  (TensorProduct v w) (TensorProduct (VectorSpaceImplementation v) w)
abstractTensorProductsCoercion @a @w) of
          (DualFinitenessWitness DualSpaceWitness c
DualSpaceWitness, VSCCoercion (TensorProduct a w) (TensorProduct c w)
VSCCoercion) -> \f (Scalar w) -> w
f ->
             (coerce :: forall a b. Coercible a b => a -> b
coerce forall (f :: * -> * -> *) a b.
(Function f, Object f a, Object f b) =>
f a b -> a -> b
$ forall v w (f :: * -> *).
(FiniteDimensional v, LinearSpace w, Scalar w ~ Scalar v,
 Functor f) =>
(f (Scalar w) -> w) -> f (DualVector v) -> v +> w
recomposeContraLinMap @(DualVector c) @w @f) f (Scalar w) -> w
f
               forall κ (k :: κ -> κ -> *) (a :: κ) (b :: κ) (c :: κ).
(Category k, Object k a, Object k b, Object k c) =>
k b c -> k a b -> k a c
. forall (f :: * -> *) (r :: * -> * -> *) (t :: * -> * -> *) a b.
(Functor f r t, Object r a, Object t (f a), Object r b,
 Object t (f b)) =>
r a b -> t (f a) (f b)
fmap (coerce :: forall a b. Coercible a b => a -> b
coerce :: a -> c)
  recomposeContraLinMapTensor :: forall u w (f :: * -> *).
(FiniteDimensional u, LinearSpace w,
 Scalar u ~ Scalar (AbstractDualVector a c),
 Scalar w ~ Scalar (AbstractDualVector a c), Functor f) =>
(f (Scalar w) -> w)
-> f (AbstractDualVector a c +> DualVector u)
-> (AbstractDualVector a c ⊗ u) +> w
recomposeContraLinMapTensor = forall v ρ.
AbstractVectorSpace v =>
((Scalar (VectorSpaceImplementation v) ~ Scalar v) => ρ) -> ρ
scalarsSameInAbstraction @a forall (f :: * -> *) w u.
(LinearSpace w, Scalar w ~ Scalar c, FiniteDimensional u,
 Scalar u ~ Scalar c, Functor f) =>
(f (Scalar w) -> w)
-> f (AbstractDualVector a c +> DualVector u)
-> (AbstractDualVector a c ⊗ u) +> w
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 :: forall (f :: * -> *) w u.
(LinearSpace w, Scalar w ~ Scalar c, FiniteDimensional u,
 Scalar u ~ Scalar c, Functor f) =>
(f (Scalar w) -> w)
-> f (AbstractDualVector a c +> DualVector u)
-> (AbstractDualVector a c ⊗ u) +> w
rclmt = forall v ρ.
AbstractVectorSpace v =>
((Scalar (VectorSpaceImplementation v) ~ Scalar v) => ρ) -> ρ
scalarsSameInAbstraction @a (case forall v. LinearSpace v => DualSpaceWitness v
dualSpaceWitness @u of
           DualSpaceWitness u
DualSpaceWitness ->
                 case ( forall v. FiniteDimensional v => DualFinitenessWitness v
dualFinitenessWitness @c
                      , forall v w.
AbstractTensorSpace v =>
VSCCoercion
  (TensorProduct v w) (TensorProduct (VectorSpaceImplementation v) w)
abstractTensorProductsCoercion @a @(DualVector u)
                      , forall v w.
AbstractTensorSpace v =>
VSCCoercion
  (TensorProduct v w) (TensorProduct (VectorSpaceImplementation v) w)
abstractTensorProductsCoercion @a
                          @(Tensor (Scalar a) (DualVector u) w) ) of
            (DualFinitenessWitness DualSpaceWitness c
DualSpaceWitness, VSCCoercion
  (TensorProduct a (DualVector u)) (TensorProduct c (DualVector u))
VSCCoercion, VSCCoercion
  (TensorProduct a (Tensor (Scalar a) (DualVector u) w))
  (TensorProduct c (Tensor (Scalar a) (DualVector u) w))
VSCCoercion) -> \f (Scalar a) -> w
f ->
              (coerce :: forall a b. Coercible a b => a -> b
coerce forall (f :: * -> * -> *) a b.
(Function f, Object f a, Object f b) =>
f a b -> a -> b
$ forall v u w (f :: * -> *).
(FiniteDimensional v, FiniteDimensional u, LinearSpace w,
 Scalar u ~ Scalar v, Scalar w ~ Scalar v, Functor f) =>
(f (Scalar w) -> w) -> f (v +> DualVector u) -> (v ⊗ u) +> w
recomposeContraLinMapTensor @(DualVector c) @u @w @f) f (Scalar a) -> w
f
                forall κ (k :: κ -> κ -> *) (a :: κ) (b :: κ) (c :: κ).
(Category k, Object k a, Object k b, Object k c) =>
k b c -> k a b -> k a c
. forall (f :: * -> *) (r :: * -> * -> *) (t :: * -> * -> *) a b.
(Functor f r t, Object r a, Object t (f a), Object r b,
 Object t (f b)) =>
r a b -> t (f a) (f b)
fmap (coerce :: forall a b. Coercible a b => a -> b
coerce :: (AbstractDualVector a c+>DualVector u)
                                    -> (DualVector c+>DualVector u))
          )
  uncanonicallyFromDual :: DualVector (AbstractDualVector a c) -+> AbstractDualVector a c
uncanonicallyFromDual = case forall v. FiniteDimensional v => DualFinitenessWitness v
dualFinitenessWitness @c of
    DualFinitenessWitness DualSpaceWitness c
DualSpaceWitness
        -> coerce :: forall a b. Coercible a b => a -> b
coerce (forall v. FiniteDimensional v => DualVector v -+> v
uncanonicallyFromDual @(DualVector c))
  uncanonicallyToDual :: AbstractDualVector a c -+> DualVector (AbstractDualVector a c)
uncanonicallyToDual = case forall v. FiniteDimensional v => DualFinitenessWitness v
dualFinitenessWitness @c of
    DualFinitenessWitness DualSpaceWitness c
DualSpaceWitness
        -> coerce :: forall a b. Coercible a b => a -> b
coerce (forall v. FiniteDimensional v => v -+> DualVector v
uncanonicallyToDual @(DualVector c))
  tensorEquality :: forall w.
(TensorSpace w, Eq w,
 Scalar w ~ Scalar (AbstractDualVector a c)) =>
(AbstractDualVector a c ⊗ w)
-> (AbstractDualVector a c ⊗ w) -> Bool
tensorEquality = forall w.
(TensorSpace w, Eq w, Scalar w ~ Scalar a) =>
(AbstractDualVector a c ⊗ w)
-> (AbstractDualVector a c ⊗ w) -> Bool
te
   where te :: ∀ w . (TensorSpace w, Eq w, Scalar w ~ Scalar a)
                => (AbstractDualVector a c ⊗ w) -> (AbstractDualVector a c ⊗ w) -> Bool
         te :: forall w.
(TensorSpace w, Eq w, Scalar w ~ Scalar a) =>
(AbstractDualVector a c ⊗ w)
-> (AbstractDualVector a c ⊗ w) -> Bool
te = case forall v. FiniteDimensional v => DualFinitenessWitness v
dualFinitenessWitness @c of
           DualFinitenessWitness DualSpaceWitness c
_ -> forall v ρ.
AbstractLinearSpace v =>
((Scalar (VectorSpaceImplementation v) ~ Scalar v,
  Scalar (DualVector v) ~ Scalar v,
  Scalar (DualVector (VectorSpaceImplementation v)) ~ Scalar v) =>
 ρ)
-> ρ
scalarsSameInAbstractionAndDuals @a
                (coerce :: forall a b. Coercible a b => a -> b
coerce (forall v w.
(FiniteDimensional v, TensorSpace w, Eq w, Scalar w ~ Scalar v) =>
(v ⊗ w) -> (v ⊗ w) -> Bool
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 :: [(Int, AbstractDualVector a c)]
-> Forest (Int, DualVector (AbstractDualVector a c))
dualBasisCandidates = case forall v. LinearSpace v => DualSpaceWitness v
dualSpaceWitness @c of
    DualSpaceWitness c
DualSpaceWitness -> coerce :: forall a b. Coercible a b => a -> b
coerce (forall v. SemiInner v => [(Int, v)] -> Forest (Int, DualVector v)
dualBasisCandidates @(DualVector c))
  tensorDualBasisCandidates :: forall w.
(SemiInner w, Scalar w ~ Scalar (AbstractDualVector a c)) =>
[(Int, AbstractDualVector a c ⊗ w)]
-> Forest (Int, DualVector (AbstractDualVector a c ⊗ w))
tensorDualBasisCandidates = forall v ρ.
AbstractVectorSpace v =>
((Scalar (VectorSpaceImplementation v) ~ Scalar v) => ρ) -> ρ
scalarsSameInAbstraction @a forall w.
(SemiInner w, Scalar w ~ Scalar c) =>
[(Int, AbstractDualVector a c ⊗ w)]
-> Forest (Int, AbstractDualVector a c +> DualVector w)
tdbc
   where tdbc :: ∀ w . (SemiInner w, Scalar w ~ Scalar c)
            => [(Int, AbstractDualVector a c ⊗ w)]
             -> Forest (Int, AbstractDualVector a c +> DualVector w)
         tdbc :: forall w.
(SemiInner w, Scalar w ~ Scalar c) =>
[(Int, AbstractDualVector a c ⊗ w)]
-> Forest (Int, AbstractDualVector a c +> DualVector w)
tdbc = case (forall v. LinearSpace v => DualSpaceWitness v
dualSpaceWitness @c, forall v. LinearSpace v => DualSpaceWitness v
dualSpaceWitness @w) of
           (DualSpaceWitness c
DualSpaceWitness, DualSpaceWitness w
DualSpaceWitness)
               -> case forall v w.
AbstractTensorSpace v =>
VSCCoercion
  (TensorProduct v w) (TensorProduct (VectorSpaceImplementation v) w)
abstractTensorProductsCoercion @a @(DualVector w) of
             VSCCoercion
  (TensorProduct a (DualVector w))
  (TensorProduct (VectorSpaceImplementation a) (DualVector w))
VSCCoercion -> coerce :: forall a b. Coercible a b => a -> b
coerce (forall v w.
(SemiInner v, SemiInner w, Scalar w ~ Scalar v) =>
[(Int, v ⊗ w)] -> Forest (Int, DualVector (v ⊗ w))
tensorDualBasisCandidates @(DualVector c) @w)
  symTensorDualBasisCandidates :: [(Int,
  SymmetricTensor
    (Scalar (AbstractDualVector a c)) (AbstractDualVector a c))]
-> Forest
     (Int,
      SymmetricTensor
        (Scalar (AbstractDualVector a c))
        (DualVector (AbstractDualVector a c)))
symTensorDualBasisCandidates = forall v ρ.
AbstractVectorSpace v =>
((Scalar (VectorSpaceImplementation v) ~ Scalar v) => ρ) -> ρ
scalarsSameInAbstraction @a
          ( case ( forall v (p :: * -> *) a b.
(TensorSpace v, Functor p) =>
p v
-> VSCCoercion a b
-> VSCCoercion (TensorProduct v a) (TensorProduct v b)
coerceFmapTensorProduct @c [] (forall a b. Coercible a b => VSCCoercion a b
VSCCoercion @a @c)
                          forall κ (k :: κ -> κ -> *) (a :: κ) (b :: κ) (c :: κ).
(Category k, Object k a, Object k b, Object k c) =>
k b c -> k a b -> k a c
. forall v w.
AbstractTensorSpace v =>
VSCCoercion
  (TensorProduct v w) (TensorProduct (VectorSpaceImplementation v) w)
abstractTensorProductsCoercion @a @a
                 , forall v (p :: * -> *) a b.
(TensorSpace v, Functor p) =>
p v
-> VSCCoercion a b
-> VSCCoercion (TensorProduct v a) (TensorProduct v b)
coerceFmapTensorProduct @(DualVector c) []
                      (forall a b. Coercible a b => VSCCoercion a b
VSCCoercion @(AbstractDualVector a c) @(DualVector c))
                 , forall v. LinearSpace v => DualSpaceWitness v
dualSpaceWitness @c ) of
             (VSCCoercion (TensorProduct a a) (TensorProduct c c)
VSCCoercion, VSCCoercion
  (TensorProduct (DualVector c) (AbstractDualVector a c))
  (TensorProduct (DualVector c) (DualVector c))
VSCCoercion, DualSpaceWitness c
DualSpaceWitness)
               -> coerce :: forall a b. Coercible a b => a -> b
coerce (forall v.
SemiInner v =>
[(Int, SymmetricTensor (Scalar v) v)]
-> Forest (Int, SymmetricTensor (Scalar v) (DualVector v))
symTensorDualBasisCandidates @(DualVector c))
          )

 

pattern AbstractDualVector
    :: AbstractLinearSpace v => DualVector (VectorSpaceImplementation v) -> DualVector v
pattern $bAbstractDualVector :: forall v.
AbstractLinearSpace v =>
DualVector (VectorSpaceImplementation v) -> DualVector v
$mAbstractDualVector :: forall {r} {v}.
AbstractLinearSpace v =>
DualVector v
-> (DualVector (VectorSpaceImplementation v) -> r)
-> ((# #) -> r)
-> r
AbstractDualVector φ = AbstractDualVector_ φ



abstractVS_zeroV :: ∀ v .
    (AbstractAdditiveGroup v)
       => v
abstractVS_zeroV :: forall v. AbstractAdditiveGroup v => v
abstractVS_zeroV = coerce :: forall a b. Coercible a b => a -> b
coerce (forall v. AdditiveGroup v => v
zeroV @(VectorSpaceImplementation v))

abstractVS_addvs :: ∀ v .
    (AbstractAdditiveGroup v)
       => v -> v -> v
abstractVS_addvs :: forall v. AbstractAdditiveGroup v => v -> v -> v
abstractVS_addvs = coerce :: forall a b. Coercible a b => a -> b
coerce (forall v. AdditiveGroup v => v -> v -> v
(^+^) @(VectorSpaceImplementation v))

abstractVS_subvs :: ∀ v .
    (AbstractAdditiveGroup v)
       => v -> v -> v
abstractVS_subvs :: forall v. AbstractAdditiveGroup v => v -> v -> v
abstractVS_subvs = coerce :: forall a b. Coercible a b => a -> b
coerce (forall v. AdditiveGroup v => v -> v -> v
(^-^) @(VectorSpaceImplementation v))

abstractVS_negateV :: ∀ v .
    (AbstractAdditiveGroup v)
       => v -> v
abstractVS_negateV :: forall v. AbstractAdditiveGroup v => v -> v
abstractVS_negateV = coerce :: forall a b. Coercible a b => a -> b
coerce (forall v. AdditiveGroup v => v -> v
negateV @(VectorSpaceImplementation v))

abstractVS_scalev :: ∀ v .
    (AbstractVectorSpace v)
       => Scalar v -> v -> v
abstractVS_scalev :: forall v. AbstractVectorSpace v => Scalar v -> v -> v
abstractVS_scalev = forall v ρ.
AbstractVectorSpace v =>
((Scalar (VectorSpaceImplementation v) ~ Scalar v) => ρ) -> ρ
scalarsSameInAbstraction @v
  ( coerce :: forall a b. Coercible a b => a -> b
coerce (forall v. VectorSpace v => Scalar v -> v -> v
(*^) @(VectorSpaceImplementation v)) )

abstractVS_innerProd :: ∀ v .
    (AbstractVectorSpace v, InnerSpace (VectorSpaceImplementation v))
       => v -> v -> Scalar v
abstractVS_innerProd :: forall v.
(AbstractVectorSpace v,
 InnerSpace (VectorSpaceImplementation v)) =>
v -> v -> Scalar v
abstractVS_innerProd = forall v ρ.
AbstractVectorSpace v =>
((Scalar (VectorSpaceImplementation v) ~ Scalar v) => ρ) -> ρ
scalarsSameInAbstraction @v
  ( coerce :: forall a b. Coercible a b => a -> b
coerce (forall v. InnerSpace v => v -> v -> Scalar v
(<.>) @(VectorSpaceImplementation v)) )

abstractVS_scalarsSameInAbstraction :: ∀ v ρ .
    ( AbstractVectorSpace v
    , Scalar (VectorSpaceImplementation v) ~ Scalar v
    )
   => ( Scalar (VectorSpaceImplementation v) ~ Scalar v
         => ρ ) -> ρ
abstractVS_scalarsSameInAbstraction :: forall v ρ.
(AbstractVectorSpace v,
 Scalar (VectorSpaceImplementation v) ~ Scalar v) =>
((Scalar (VectorSpaceImplementation v) ~ Scalar v) => ρ) -> ρ
abstractVS_scalarsSameInAbstraction (Scalar (VectorSpaceImplementation v) ~ Scalar v) => ρ
φ
   = (Scalar (VectorSpaceImplementation v) ~ Scalar v) => ρ
φ

abstractVS_scalarSpaceWitness :: ∀ v .
    (AbstractTensorSpace v)
       => ScalarSpaceWitness v
abstractVS_scalarSpaceWitness :: forall v. AbstractTensorSpace v => ScalarSpaceWitness v
abstractVS_scalarSpaceWitness
   = case forall v. TensorSpace v => ScalarSpaceWitness v
scalarSpaceWitness @(VectorSpaceImplementation v) of
      ScalarSpaceWitness (VectorSpaceImplementation v)
ScalarSpaceWitness -> forall v ρ.
AbstractVectorSpace v =>
((Scalar (VectorSpaceImplementation v) ~ Scalar v) => ρ) -> ρ
scalarsSameInAbstraction @v forall v.
(Num' (Scalar v), Scalar (Scalar v) ~ Scalar v) =>
ScalarSpaceWitness v
ScalarSpaceWitness 

abstractVS_linearManifoldWitness :: ∀ v .
    ( AbstractTensorSpace v, AffineSpace v, Needle v ~ v, Diff v ~ v
    )
       => LinearManifoldWitness v
abstractVS_linearManifoldWitness :: forall v.
(AbstractTensorSpace v, AffineSpace v, Needle v ~ v, Diff v ~ v) =>
LinearManifoldWitness v
abstractVS_linearManifoldWitness
   = case forall v. TensorSpace v => LinearManifoldWitness v
linearManifoldWitness @(VectorSpaceImplementation v) of
#if MIN_VERSION_manifolds_core(0,6,0)
           LinearManifoldWitness (VectorSpaceImplementation v)
LinearManifoldWitness -> forall v.
(Needle v ~ v, AffineSpace v, Diff v ~ v) =>
LinearManifoldWitness v
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 :: forall v.
(AbstractTensorSpace v,
 Coercible
   (TensorProduct v (Scalar v))
   (TensorProduct
      (VectorSpaceImplementation v)
      (Scalar (VectorSpaceImplementation v)))) =>
v -+> (v ⊗ Scalar v)
abstractVS_toFlatTensor = coerce :: forall a b. Coercible a b => a -> b
coerce (forall v. TensorSpace v => v -+> (v ⊗ Scalar v)
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 :: forall v.
(AbstractTensorSpace v,
 Coercible
   (TensorProduct v (Scalar v))
   (TensorProduct
      (VectorSpaceImplementation v)
      (Scalar (VectorSpaceImplementation v)))) =>
(v ⊗ Scalar v) -+> v
abstractVS_fromFlatTensor = coerce :: forall a b. Coercible a b => a -> b
coerce (forall v. TensorSpace v => (v ⊗ Scalar v) -+> v
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 :: forall v w.
(AbstractTensorSpace v, TensorSpace w, Scalar w ~ Scalar v,
 Coercible
   (TensorProduct v w)
   (TensorProduct (VectorSpaceImplementation v) w)) =>
v ⊗ w
abstractVS_zeroTensor = forall v ρ.
AbstractVectorSpace v =>
((Scalar (VectorSpaceImplementation v) ~ Scalar v) => ρ) -> ρ
scalarsSameInAbstraction @v
  (coerce :: forall a b. Coercible a b => a -> b
coerce (forall v w.
(TensorSpace v, TensorSpace w, Scalar w ~ Scalar v) =>
v ⊗ w
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 :: forall 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 = forall v ρ.
AbstractVectorSpace v =>
((Scalar (VectorSpaceImplementation v) ~ Scalar v) => ρ) -> ρ
scalarsSameInAbstraction @v
  (coerce :: forall a b. Coercible a b => a -> b
coerce (forall v w.
(TensorSpace v, TensorSpace w, Scalar w ~ Scalar v) =>
(v ⊗ w) -> (v ⊗ w) -> v ⊗ w
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 :: forall 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 = forall v ρ.
AbstractVectorSpace v =>
((Scalar (VectorSpaceImplementation v) ~ Scalar v) => ρ) -> ρ
scalarsSameInAbstraction @v
  (coerce :: forall a b. Coercible a b => a -> b
coerce (forall v w.
(TensorSpace v, TensorSpace v, TensorSpace w,
 Scalar w ~ Scalar v) =>
(v ⊗ w) -> (v ⊗ w) -> v ⊗ w
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 :: forall 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 = forall v ρ.
AbstractVectorSpace v =>
((Scalar (VectorSpaceImplementation v) ~ Scalar v) => ρ) -> ρ
scalarsSameInAbstraction @v
  (coerce :: forall a b. Coercible a b => a -> b
coerce (forall v w.
(TensorSpace v, TensorSpace w, Scalar w ~ Scalar v) =>
Bilinear (Scalar v) (v ⊗ w) (v ⊗ w)
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 :: forall v w.
(AbstractTensorSpace v, TensorSpace w, Scalar w ~ Scalar v,
 Coercible
   (TensorProduct v w)
   (TensorProduct (VectorSpaceImplementation v) w)) =>
(v ⊗ w) -+> (v ⊗ w)
abstractVS_negateTensor = forall v ρ.
AbstractVectorSpace v =>
((Scalar (VectorSpaceImplementation v) ~ Scalar v) => ρ) -> ρ
scalarsSameInAbstraction @v
  (coerce :: forall a b. Coercible a b => a -> b
coerce (forall v w.
(TensorSpace v, TensorSpace w, Scalar w ~ Scalar v) =>
(v ⊗ w) -+> (v ⊗ w)
negateTensor @(VectorSpaceImplementation v) @w))

abstractVS_wellDefinedVector :: ∀ v
         . ( AbstractTensorSpace v
           ) => v -> Maybe v
abstractVS_wellDefinedVector :: forall v. AbstractTensorSpace v => v -> Maybe v
abstractVS_wellDefinedVector = coerce :: forall a b. Coercible a b => a -> b
coerce (forall v. TensorSpace v => v -> Maybe v
wellDefinedVector @(VectorSpaceImplementation v))

abstractVS_wellDefinedTensor :: ∀ v w
         . ( AbstractTensorSpace v
           , TensorSpace w, Scalar w ~ Scalar v
           ) => (v ⊗ w) -> Maybe (v ⊗ w)
abstractVS_wellDefinedTensor :: forall v w.
(AbstractTensorSpace v, TensorSpace w, Scalar w ~ Scalar v) =>
(v ⊗ w) -> Maybe (v ⊗ w)
abstractVS_wellDefinedTensor
    = forall v ρ.
AbstractVectorSpace v =>
((Scalar (VectorSpaceImplementation v) ~ Scalar v) => ρ) -> ρ
scalarsSameInAbstraction @v
        (case forall v w.
AbstractTensorSpace v =>
VSCCoercion
  (TensorProduct v w) (TensorProduct (VectorSpaceImplementation v) w)
abstractTensorProductsCoercion @v @w of
           VSCCoercion
  (TensorProduct v w) (TensorProduct (VectorSpaceImplementation v) w)
VSCCoercion -> coerce :: forall a b. Coercible a b => a -> b
coerce (forall v w.
(TensorSpace v, TensorSpace w, Scalar w ~ Scalar v) =>
(v ⊗ w) -> Maybe (v ⊗ w)
wellDefinedTensor @(VectorSpaceImplementation v) @w))

abstractVS_tensorProduct :: ∀ v w . ( AbstractTensorSpace v
           , TensorSpace w, Scalar w ~ Scalar v
           ) => Bilinear v w (v ⊗ w)
abstractVS_tensorProduct :: forall v w.
(AbstractTensorSpace v, TensorSpace w, Scalar w ~ Scalar v) =>
Bilinear v w (v ⊗ w)
abstractVS_tensorProduct = forall v ρ.
AbstractVectorSpace v =>
((Scalar (VectorSpaceImplementation v) ~ Scalar v) => ρ) -> ρ
scalarsSameInAbstraction @v
    ( case ( forall v w.
AbstractTensorSpace v =>
VSCCoercion
  (TensorProduct v w) (TensorProduct (VectorSpaceImplementation v) w)
abstractTensorProductsCoercion @v @w ) of
       VSCCoercion
  (TensorProduct v w) (TensorProduct (VectorSpaceImplementation v) w)
VSCCoercion -> coerce :: forall a b. Coercible a b => a -> b
coerce (forall v w.
(TensorSpace v, TensorSpace w, Scalar w ~ Scalar v) =>
Bilinear v w (v ⊗ w)
tensorProduct @(VectorSpaceImplementation v) @w) )

abstractVS_transposeTensor :: ∀ v w . ( AbstractTensorSpace v
           , TensorSpace w, Scalar w ~ Scalar v
           ) => (v ⊗ w) -+> (w ⊗ v)
abstractVS_transposeTensor :: forall v w.
(AbstractTensorSpace v, TensorSpace w, Scalar w ~ Scalar v) =>
(v ⊗ w) -+> (w ⊗ v)
abstractVS_transposeTensor
    = forall v ρ.
AbstractVectorSpace v =>
((Scalar (VectorSpaceImplementation v) ~ Scalar v) => ρ) -> ρ
scalarsSameInAbstraction @v ( case
           ( forall v w.
AbstractTensorSpace v =>
VSCCoercion
  (TensorProduct v w) (TensorProduct (VectorSpaceImplementation v) w)
abstractTensorProductsCoercion @v @w
           , forall v (p :: * -> *) a b.
(TensorSpace v, Functor p) =>
p v
-> VSCCoercion a b
-> VSCCoercion (TensorProduct v a) (TensorProduct v b)
coerceFmapTensorProduct @w []
                (forall a b. Coercible a b => VSCCoercion a b
VSCCoercion @(VectorSpaceImplementation v) @(v)) ) of
   (VSCCoercion
  (TensorProduct v w) (TensorProduct (VectorSpaceImplementation v) w)
VSCCoercion, VSCCoercion
  (TensorProduct w (VectorSpaceImplementation v)) (TensorProduct w v)
VSCCoercion) -> forall v ρ.
AbstractVectorSpace v =>
((Scalar (VectorSpaceImplementation v) ~ Scalar v) => ρ) -> ρ
scalarsSameInAbstraction @v
      (coerce :: forall a b. Coercible a b => a -> b
coerce (forall v w.
(TensorSpace v, TensorSpace w, Scalar w ~ Scalar v) =>
(v ⊗ w) -+> (w ⊗ v)
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 :: forall 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
   = forall v ρ.
AbstractVectorSpace v =>
((Scalar (VectorSpaceImplementation v) ~ Scalar v) => ρ) -> ρ
scalarsSameInAbstraction @v
       ( case ( forall v w.
AbstractTensorSpace v =>
VSCCoercion
  (TensorProduct v w) (TensorProduct (VectorSpaceImplementation v) w)
abstractTensorProductsCoercion @v @u
              , forall v w.
AbstractTensorSpace v =>
VSCCoercion
  (TensorProduct v w) (TensorProduct (VectorSpaceImplementation v) w)
abstractTensorProductsCoercion @v @w ) of
           (VSCCoercion
  (TensorProduct v u) (TensorProduct (VectorSpaceImplementation v) u)
VSCCoercion, VSCCoercion
  (TensorProduct v w) (TensorProduct (VectorSpaceImplementation v) w)
VSCCoercion)
              -> coerce :: forall a b. Coercible a b => a -> b
coerce (forall v w x.
(TensorSpace v, TensorSpace w, TensorSpace x, Scalar w ~ Scalar v,
 Scalar x ~ Scalar v) =>
Bilinear (w -+> x) (v ⊗ w) (v ⊗ x)
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 :: forall 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 = forall v ρ.
AbstractVectorSpace v =>
((Scalar (VectorSpaceImplementation v) ~ Scalar v) => ρ) -> ρ
scalarsSameInAbstraction @v
       ( case ( forall v w.
AbstractTensorSpace v =>
VSCCoercion
  (TensorProduct v w) (TensorProduct (VectorSpaceImplementation v) w)
abstractTensorProductsCoercion @v @u
              , forall v w.
AbstractTensorSpace v =>
VSCCoercion
  (TensorProduct v w) (TensorProduct (VectorSpaceImplementation v) w)
abstractTensorProductsCoercion @v @w
              , forall v w.
AbstractTensorSpace v =>
VSCCoercion
  (TensorProduct v w) (TensorProduct (VectorSpaceImplementation v) w)
abstractTensorProductsCoercion @v @x ) of
           (VSCCoercion
  (TensorProduct v u) (TensorProduct (VectorSpaceImplementation v) u)
VSCCoercion, VSCCoercion
  (TensorProduct v w) (TensorProduct (VectorSpaceImplementation v) w)
VSCCoercion, VSCCoercion
  (TensorProduct v x) (TensorProduct (VectorSpaceImplementation v) x)
VSCCoercion)
              -> coerce :: forall a b. Coercible a b => a -> b
coerce (forall v u w x.
(TensorSpace v, TensorSpace u, TensorSpace w, TensorSpace x,
 Scalar u ~ Scalar v, Scalar w ~ Scalar v, Scalar x ~ Scalar v) =>
Bilinear ((w, x) -+> u) (v ⊗ w, v ⊗ x) (v ⊗ u)
fzipTensorWith @(VectorSpaceImplementation v) @u @w @x)
        )

abstractVS_coerceFmapTensorProduct :: ∀ v u w p .
         ( AbstractTensorSpace v
         ) => p v -> VSCCoercion u w -> VSCCoercion (TensorProduct v u) (TensorProduct v w)
abstractVS_coerceFmapTensorProduct :: forall v u w (p :: * -> *).
AbstractTensorSpace v =>
p v
-> VSCCoercion u w
-> VSCCoercion (TensorProduct v u) (TensorProduct v w)
abstractVS_coerceFmapTensorProduct p v
_ VSCCoercion u w
crc
      = case ( forall v w.
AbstractTensorSpace v =>
VSCCoercion
  (TensorProduct v w) (TensorProduct (VectorSpaceImplementation v) w)
abstractTensorProductsCoercion @v @u
             , forall v w.
AbstractTensorSpace v =>
VSCCoercion
  (TensorProduct v w) (TensorProduct (VectorSpaceImplementation v) w)
abstractTensorProductsCoercion @v @w
             , forall v (p :: * -> *) a b.
(TensorSpace v, Functor p) =>
p v
-> VSCCoercion a b
-> VSCCoercion (TensorProduct v a) (TensorProduct v b)
coerceFmapTensorProduct @(VectorSpaceImplementation v) [] VSCCoercion u w
crc ) of
          (VSCCoercion
  (TensorProduct v u) (TensorProduct (VectorSpaceImplementation v) u)
VSCCoercion, VSCCoercion
  (TensorProduct v w) (TensorProduct (VectorSpaceImplementation v) w)
VSCCoercion, VSCCoercion
  (TensorProduct (VectorSpaceImplementation v) u)
  (TensorProduct (VectorSpaceImplementation v) w)
VSCCoercion) -> forall a b. Coercible a b => VSCCoercion a b
VSCCoercion

abstractVS_dualSpaceWitness :: ∀ v . (AbstractLinearSpace v
        , LinearSpace v
        , LinearSpace (VectorSpaceImplementation v))
     => DualSpaceWitness v
abstractVS_dualSpaceWitness :: forall v.
(AbstractLinearSpace v, LinearSpace v,
 LinearSpace (VectorSpaceImplementation v)) =>
DualSpaceWitness v
abstractVS_dualSpaceWitness
      = forall v ρ.
AbstractVectorSpace v =>
((Scalar (VectorSpaceImplementation v) ~ Scalar v) => ρ) -> ρ
scalarsSameInAbstraction @v
  ( case forall v. LinearSpace v => DualSpaceWitness v
dualSpaceWitness @(VectorSpaceImplementation v) of
      DualSpaceWitness (VectorSpaceImplementation v)
DualSpaceWitness -> forall v.
(LinearSpace (Scalar v), DualVector (Scalar v) ~ Scalar v,
 LinearSpace (DualVector v), Scalar (DualVector v) ~ Scalar v,
 DualVector (DualVector v) ~ v) =>
DualSpaceWitness v
DualSpaceWitness
   )

abstractVS_linearId :: ∀ v . ( AbstractLinearSpace v
           , LinearSpace (VectorSpaceImplementation v) )
                   => v +> v
abstractVS_linearId :: forall v.
(AbstractLinearSpace v,
 LinearSpace (VectorSpaceImplementation v)) =>
v +> v
abstractVS_linearId = case forall v. LinearSpace v => DualSpaceWitness v
dualSpaceWitness @(VectorSpaceImplementation v) of
 DualSpaceWitness (VectorSpaceImplementation v)
DualSpaceWitness -> case forall v (p :: * -> *) a b.
(TensorSpace v, Functor p) =>
p v
-> VSCCoercion a b
-> VSCCoercion (TensorProduct v a) (TensorProduct v b)
coerceFmapTensorProduct
                             @(DualVector (VectorSpaceImplementation v)) []
                             (forall a b. Coercible a b => VSCCoercion a b
VSCCoercion @v @(VectorSpaceImplementation v)) of
   VSCCoercion
  (TensorProduct (DualVector (VectorSpaceImplementation v)) v)
  (TensorProduct
     (DualVector (VectorSpaceImplementation v))
     (VectorSpaceImplementation v))
VSCCoercion -> coerce :: forall a b. Coercible a b => a -> b
coerce (forall v. LinearSpace v => v +> v
linearId @(VectorSpaceImplementation v))

abstractVS_tensorId :: ∀ v w . ( AbstractLinearSpace v
           , LinearSpace (VectorSpaceImplementation v)
           , LinearSpace w, Scalar w ~ Scalar v )
                   => (v ⊗ w) +> (v ⊗ w) 
abstractVS_tensorId :: forall v w.
(AbstractLinearSpace v, LinearSpace (VectorSpaceImplementation v),
 LinearSpace w, Scalar w ~ Scalar v) =>
(v ⊗ w) +> (v ⊗ w)
abstractVS_tensorId = forall v ρ.
AbstractVectorSpace v =>
((Scalar (VectorSpaceImplementation v) ~ Scalar v) => ρ) -> ρ
scalarsSameInAbstraction @v
  (case (forall v. LinearSpace v => DualSpaceWitness v
dualSpaceWitness @w, forall v. LinearSpace v => DualSpaceWitness v
dualSpaceWitness @(VectorSpaceImplementation v)) of
     (DualSpaceWitness w
DualSpaceWitness, DualSpaceWitness (VectorSpaceImplementation v)
DualSpaceWitness)
       -> case forall v (p :: * -> *) a b.
(TensorSpace v, Functor p) =>
p v
-> VSCCoercion a b
-> VSCCoercion (TensorProduct v a) (TensorProduct v b)
coerceFmapTensorProduct @(DualVector w) []
                 forall (f :: * -> * -> *) a b.
(Function f, Object f a, Object f b) =>
f a b -> a -> b
$ forall a b. Coercible a b => VSCCoercion a b
VSCCoercion @(TensorProduct (VectorSpaceImplementation v) w)
                            @(VectorSpaceImplementation v ⊗ w)
                  forall κ (k :: κ -> κ -> *) (a :: κ) (b :: κ) (c :: κ).
(Category k, Object k a, Object k b, Object k c) =>
k b c -> k a b -> k a c
. forall v w.
AbstractTensorSpace v =>
VSCCoercion
  (TensorProduct v w) (TensorProduct (VectorSpaceImplementation v) w)
abstractTensorProductsCoercion @v @w
                  forall κ (k :: κ -> κ -> *) (a :: κ) (b :: κ) (c :: κ).
(Category k, Object k a, Object k b, Object k c) =>
k b c -> k a b -> k a c
. forall a b. Coercible a b => VSCCoercion a b
VSCCoercion @(v ⊗ w) @(TensorProduct v w) of
         VSCCoercion
  (TensorProduct (DualVector w) (Tensor (Scalar v) v w))
  (TensorProduct
     (DualVector w) (Tensor (Scalar v) (VectorSpaceImplementation v) w))
VSCCoercion
           -> case ( forall v (p :: * -> *) a b.
(TensorSpace v, Functor p) =>
p v
-> VSCCoercion a b
-> VSCCoercion (TensorProduct v a) (TensorProduct v b)
coerceFmapTensorProduct 
                      @(DualVector (VectorSpaceImplementation v)) []
                      (forall a b. Coercible a b => VSCCoercion a b
VSCCoercion :: VSCCoercion
                          (Tensor (Scalar v) (DualVector w) (Tensor (Scalar v) v w))
                          (Tensor (Scalar v)
                                  (DualVector w)
                                  (Tensor (Scalar v)
                                          (VectorSpaceImplementation v) w)))
                   ) of
            VSCCoercion
  (TensorProduct
     (DualVector (VectorSpaceImplementation v))
     (Tensor (Scalar v) (DualVector w) (Tensor (Scalar v) v w)))
  (TensorProduct
     (DualVector (VectorSpaceImplementation v))
     (Tensor
        (Scalar v)
        (DualVector w)
        (Tensor (Scalar v) (VectorSpaceImplementation v) w)))
VSCCoercion
               -> coerce :: forall a b. Coercible a b => a -> b
coerce (forall v w.
(LinearSpace v, LinearSpace w, Scalar w ~ Scalar v) =>
(v ⊗ w) +> (v ⊗ w)
tensorId @(VectorSpaceImplementation v) @w)
       )

abstractVS_applyDualVector :: ∀ v . ( AbstractLinearSpace v
           , LinearSpace (VectorSpaceImplementation v) )
                   => Bilinear (DualVector v) v (Scalar v)
abstractVS_applyDualVector :: forall v.
(AbstractLinearSpace v,
 LinearSpace (VectorSpaceImplementation v)) =>
Bilinear (DualVector v) v (Scalar v)
abstractVS_applyDualVector = forall v ρ.
AbstractVectorSpace v =>
((Scalar (VectorSpaceImplementation v) ~ Scalar v) => ρ) -> ρ
scalarsSameInAbstraction @v
 ( case forall v. LinearSpace v => DualSpaceWitness v
dualSpaceWitness @(VectorSpaceImplementation v) of
    DualSpaceWitness (VectorSpaceImplementation v)
DualSpaceWitness -> coerce :: forall a b. Coercible a b => a -> b
coerce (forall v.
(LinearSpace v, LinearSpace v) =>
Bilinear (DualVector v) v (Scalar v)
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 :: forall v w.
(AbstractLinearSpace v, LinearSpace (VectorSpaceImplementation v),
 TensorSpace w, Scalar w ~ Scalar v) =>
Bilinear (v +> w) v w
abstractVS_applyLinear = forall v ρ.
AbstractVectorSpace v =>
((Scalar (VectorSpaceImplementation v) ~ Scalar v) => ρ) -> ρ
scalarsSameInAbstraction @v
 ( coerce :: forall a b. Coercible a b => a -> b
coerce (forall v w.
(LinearSpace v, TensorSpace w, Scalar w ~ Scalar v) =>
Bilinear (v +> w) v w
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 :: forall v u.
(AbstractLinearSpace v, LinearSpace (VectorSpaceImplementation v),
 LinearSpace u, Scalar u ~ Scalar v) =>
Bilinear (DualVector (v ⊗ u)) (v ⊗ u) (Scalar v)
abstractVS_applyTensorFunctional = forall v ρ.
AbstractVectorSpace v =>
((Scalar (VectorSpaceImplementation v) ~ Scalar v) => ρ) -> ρ
scalarsSameInAbstraction @v
 (case forall v w.
AbstractTensorSpace v =>
VSCCoercion
  (TensorProduct v w) (TensorProduct (VectorSpaceImplementation v) w)
abstractTensorProductsCoercion @v @u of
   VSCCoercion
  (TensorProduct v u) (TensorProduct (VectorSpaceImplementation v) u)
VSCCoercion -> coerce :: forall a b. Coercible a b => a -> b
coerce (forall v u.
(LinearSpace v, LinearSpace u, Scalar u ~ Scalar v) =>
Bilinear (DualVector (v ⊗ u)) (v ⊗ u) (Scalar v)
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 :: forall 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 = forall v ρ.
AbstractVectorSpace v =>
((Scalar (VectorSpaceImplementation v) ~ Scalar v) => ρ) -> ρ
scalarsSameInAbstraction @v
 ( case forall v w.
AbstractTensorSpace v =>
VSCCoercion
  (TensorProduct v w) (TensorProduct (VectorSpaceImplementation v) w)
abstractTensorProductsCoercion @v @u of
   VSCCoercion
  (TensorProduct v u) (TensorProduct (VectorSpaceImplementation v) u)
VSCCoercion -> coerce :: forall a b. Coercible a b => a -> b
coerce (forall v u w.
(LinearSpace v, LinearSpace u, TensorSpace w, Scalar u ~ Scalar v,
 Scalar w ~ Scalar v) =>
Bilinear ((v ⊗ u) +> w) (v ⊗ u) w
applyTensorLinMap @(VectorSpaceImplementation v) @u @w) )

abstractSubbasisCoercion :: ∀ v .
       Coercible (SubBasis v) (SubBasis (VectorSpaceImplementation v))
     => VSCCoercion (SubBasis v) (SubBasis (VectorSpaceImplementation v))
abstractSubbasisCoercion :: forall v.
Coercible (SubBasis v) (SubBasis (VectorSpaceImplementation v)) =>
VSCCoercion (SubBasis v) (SubBasis (VectorSpaceImplementation v))
abstractSubbasisCoercion = forall a b. Coercible a b => VSCCoercion a b
VSCCoercion

precomposeCoercion :: Coercion a b -> Coercion (b -> c) (a -> c)
precomposeCoercion :: forall a b c. Coercion a b -> Coercion (b -> c) (a -> c)
precomposeCoercion Coercion a b
Coercion = forall {k} (a :: k) (b :: k). Coercible a b => Coercion a b
Coercion

postcomposeCoercion :: Coercion b c -> Coercion (a -> b) (a -> c)
postcomposeCoercion :: forall b c a. Coercion b c -> Coercion (a -> b) (a -> c)
postcomposeCoercion Coercion b c
Coercion = forall {k} (a :: k) (b :: k). Coercible a b => Coercion a b
Coercion

firstCoercion :: Coercion a b -> Coercion (a,c) (b,c)
firstCoercion :: forall a b c. Coercion a b -> Coercion (a, c) (b, c)
firstCoercion Coercion a b
Coercion = forall {k} (a :: k) (b :: k). Coercible a b => Coercion a b
Coercion

leftCoercion :: Coercion a b -> Coercion (Either a c) (Either b c)
leftCoercion :: forall a b c. Coercion a b -> Coercion (Either a c) (Either b c)
leftCoercion Coercion a b
Coercion = forall {k} (a :: k) (b :: k). Coercible a b => Coercion a b
Coercion

abstractVS_dualFinitenessWitness :: ∀ v .
       ( AbstractLinearSpace v, FiniteDimensional v
       , FiniteDimensional (VectorSpaceImplementation v) )
     => DualFinitenessWitness v
abstractVS_dualFinitenessWitness :: forall v.
(AbstractLinearSpace v, FiniteDimensional v,
 FiniteDimensional (VectorSpaceImplementation v)) =>
DualFinitenessWitness v
abstractVS_dualFinitenessWitness = forall v ρ.
AbstractVectorSpace v =>
((Scalar (VectorSpaceImplementation v) ~ Scalar v) => ρ) -> ρ
scalarsSameInAbstraction @v
  (case forall v. FiniteDimensional v => DualFinitenessWitness v
dualFinitenessWitness @(VectorSpaceImplementation v) of
     DualFinitenessWitness DualSpaceWitness (VectorSpaceImplementation v)
DualSpaceWitness
        -> forall v.
FiniteDimensional (DualVector v) =>
DualSpaceWitness v -> DualFinitenessWitness v
DualFinitenessWitness forall v.
(LinearSpace (Scalar v), DualVector (Scalar v) ~ Scalar v,
 LinearSpace (DualVector v), Scalar (DualVector v) ~ Scalar v,
 DualVector (DualVector v) ~ v) =>
DualSpaceWitness v
DualSpaceWitness
    )

abstractVS_entireBasis :: ∀ v .
       ( AbstractLinearSpace v, FiniteDimensional (VectorSpaceImplementation v)
       , Coercible (SubBasis v) (SubBasis (VectorSpaceImplementation v)) )
          => SubBasis v
abstractVS_entireBasis :: forall v.
(AbstractLinearSpace v,
 FiniteDimensional (VectorSpaceImplementation v),
 Coercible (SubBasis v) (SubBasis (VectorSpaceImplementation v))) =>
SubBasis v
abstractVS_entireBasis = forall a b. VSCCoercion a b -> VSCCoercion b a
symVSC (forall v.
Coercible (SubBasis v) (SubBasis (VectorSpaceImplementation v)) =>
VSCCoercion (SubBasis v) (SubBasis (VectorSpaceImplementation v))
abstractSubbasisCoercion @v)
            forall (f :: * -> * -> *) a b.
(Function f, Object f a, Object f b) =>
f a b -> a -> b
$ forall v. FiniteDimensional v => SubBasis v
entireBasis @(VectorSpaceImplementation v)

abstractVS_enumerateSubBasis :: ∀ v .
       ( AbstractLinearSpace v, FiniteDimensional (VectorSpaceImplementation v)
       , Coercible (SubBasis v) (SubBasis (VectorSpaceImplementation v)) )
          => SubBasis v -> [v]
abstractVS_enumerateSubBasis :: forall v.
(AbstractLinearSpace v,
 FiniteDimensional (VectorSpaceImplementation v),
 Coercible (SubBasis v) (SubBasis (VectorSpaceImplementation v))) =>
SubBasis v -> [v]
abstractVS_enumerateSubBasis = forall a b c. Coercion a b -> Coercion (b -> c) (a -> c)
precomposeCoercion
               (forall a b. VSCCoercion a b -> Coercion a b
getVSCCoercion forall (f :: * -> * -> *) a b.
(Function f, Object f a, Object f b) =>
f a b -> a -> b
$ forall v.
Coercible (SubBasis v) (SubBasis (VectorSpaceImplementation v)) =>
VSCCoercion (SubBasis v) (SubBasis (VectorSpaceImplementation v))
abstractSubbasisCoercion @v)
    forall (f :: * -> * -> *) a b.
(Function f, Object f a, Object f b) =>
f a b -> a -> b
$ coerce :: forall a b. Coercible a b => a -> b
coerce (forall v. FiniteDimensional v => SubBasis v -> [v]
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 :: forall 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 = forall v ρ.
AbstractVectorSpace v =>
((Scalar (VectorSpaceImplementation v) ~ Scalar v) => ρ) -> ρ
scalarsSameInAbstraction @v
   ( forall b c a. Coercion b c -> Coercion (a -> b) (a -> c)
postcomposeCoercion (forall a b c. Coercion a b -> Coercion (a, c) (b, c)
firstCoercion forall (f :: * -> * -> *) a b.
(Function f, Object f a, Object f b) =>
f a b -> a -> b
$ forall {k} (a :: k) (b :: k). Coercion a b -> Coercion b a
sym
            (forall a b. VSCCoercion a b -> Coercion a b
getVSCCoercion forall (f :: * -> * -> *) a b.
(Function f, Object f a, Object f b) =>
f a b -> a -> b
$ forall v.
Coercible (SubBasis v) (SubBasis (VectorSpaceImplementation v)) =>
VSCCoercion (SubBasis v) (SubBasis (VectorSpaceImplementation v))
abstractSubbasisCoercion @v))
      forall (f :: * -> * -> *) a b.
(Function f, Object f a, Object f b) =>
f a b -> a -> b
$ case forall v w.
AbstractTensorSpace v =>
VSCCoercion
  (TensorProduct v w) (TensorProduct (VectorSpaceImplementation v) w)
abstractTensorProductsCoercion @v @w of
         VSCCoercion
  (TensorProduct v w) (TensorProduct (VectorSpaceImplementation v) w)
VSCCoercion -> ( coerce :: forall a b. Coercible a b => a -> b
coerce (forall v w.
(FiniteDimensional v, LSpace w, Scalar w ~ Scalar v) =>
(v +> w) -> (SubBasis v, DList w)
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 :: forall 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 = forall v ρ.
AbstractVectorSpace v =>
((Scalar (VectorSpaceImplementation v) ~ Scalar v) => ρ) -> ρ
scalarsSameInAbstraction @v
 ( forall a b c. Coercion a b -> Coercion (b -> c) (a -> c)
precomposeCoercion (forall a b. VSCCoercion a b -> Coercion a b
getVSCCoercion forall (f :: * -> * -> *) a b.
(Function f, Object f a, Object f b) =>
f a b -> a -> b
$ forall v.
Coercible (SubBasis v) (SubBasis (VectorSpaceImplementation v)) =>
VSCCoercion (SubBasis v) (SubBasis (VectorSpaceImplementation v))
abstractSubbasisCoercion @v)
    forall κ (k :: κ -> κ -> *) (a :: κ) (b :: κ) (c :: κ).
(Category k, Object k a, Object k b, Object k c) =>
k b c -> k a b -> k a c
. forall b c a. Coercion b c -> Coercion (a -> b) (a -> c)
postcomposeCoercion (forall b c a. Coercion b c -> Coercion (a -> b) (a -> c)
postcomposeCoercion
        forall κ (k :: κ -> κ -> *) (a :: κ) (b :: κ) (c :: κ).
(Category k, Object k a, Object k b, Object k c) =>
k b c -> k a b -> k a c
. forall a b c. Coercion a b -> Coercion (Either a c) (Either b c)
leftCoercion forall κ (k :: κ -> κ -> *) (a :: κ) (b :: κ) (c :: κ).
(Category k, Object k a, Object k b, Object k c) =>
k b c -> k a b -> k a c
. forall a b c. Coercion a b -> Coercion (a, c) (b, c)
firstCoercion forall (f :: * -> * -> *) a b.
(Function f, Object f a, Object f b) =>
f a b -> a -> b
$ forall {k} (a :: k) (b :: k). Coercion a b -> Coercion b a
sym
              (forall a b. VSCCoercion a b -> Coercion a b
getVSCCoercion forall (f :: * -> * -> *) a b.
(Function f, Object f a, Object f b) =>
f a b -> a -> b
$ forall v.
Coercible (SubBasis v) (SubBasis (VectorSpaceImplementation v)) =>
VSCCoercion (SubBasis v) (SubBasis (VectorSpaceImplementation v))
abstractSubbasisCoercion @v))
      forall (f :: * -> * -> *) a b.
(Function f, Object f a, Object f b) =>
f a b -> a -> b
$ coerce :: forall a b. Coercible a b => a -> b
coerce (forall v w.
(FiniteDimensional v, LSpace w, Scalar w ~ Scalar v) =>
SubBasis v -> (v +> w) -> Either (SubBasis v, DList w) (DList w)
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 :: forall v.
(AbstractLinearSpace v,
 FiniteDimensional (VectorSpaceImplementation v),
 Coercible (SubBasis v) (SubBasis (VectorSpaceImplementation v))) =>
SubBasis v -> [Scalar v] -> (v, [Scalar v])
abstractVS_recomposeSB = forall v ρ.
AbstractVectorSpace v =>
((Scalar (VectorSpaceImplementation v) ~ Scalar v) => ρ) -> ρ
scalarsSameInAbstraction @v
 ( forall a b c. Coercion a b -> Coercion (b -> c) (a -> c)
precomposeCoercion (forall a b. VSCCoercion a b -> Coercion a b
getVSCCoercion forall (f :: * -> * -> *) a b.
(Function f, Object f a, Object f b) =>
f a b -> a -> b
$ forall v.
Coercible (SubBasis v) (SubBasis (VectorSpaceImplementation v)) =>
VSCCoercion (SubBasis v) (SubBasis (VectorSpaceImplementation v))
abstractSubbasisCoercion @v)
  forall (f :: * -> * -> *) a b.
(Function f, Object f a, Object f b) =>
f a b -> a -> b
$ coerce :: forall a b. Coercible a b => a -> b
coerce (forall v.
FiniteDimensional v =>
SubBasis v -> [Scalar v] -> (v, [Scalar v])
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 :: forall 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 = forall v ρ.
AbstractVectorSpace v =>
((Scalar (VectorSpaceImplementation v) ~ Scalar v) => ρ) -> ρ
scalarsSameInAbstraction @v
 ( forall a b c. Coercion a b -> Coercion (b -> c) (a -> c)
precomposeCoercion (forall a b. VSCCoercion a b -> Coercion a b
getVSCCoercion forall (f :: * -> * -> *) a b.
(Function f, Object f a, Object f b) =>
f a b -> a -> b
$ forall v.
Coercible (SubBasis v) (SubBasis (VectorSpaceImplementation v)) =>
VSCCoercion (SubBasis v) (SubBasis (VectorSpaceImplementation v))
abstractSubbasisCoercion @v)
  forall (f :: * -> * -> *) a b.
(Function f, Object f a, Object f b) =>
f a b -> a -> b
$ case forall v w.
AbstractTensorSpace v =>
VSCCoercion
  (TensorProduct v w) (TensorProduct (VectorSpaceImplementation v) w)
abstractTensorProductsCoercion @v @w of
     VSCCoercion
  (TensorProduct v w) (TensorProduct (VectorSpaceImplementation v) w)
VSCCoercion -> coerce :: forall a b. Coercible a b => a -> b
coerce (forall v w.
(FiniteDimensional v, FiniteDimensional w, Scalar w ~ Scalar v) =>
SubBasis v -> SubBasis w -> [Scalar v] -> (v ⊗ w, [Scalar v])
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 :: forall 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 = forall v ρ.
AbstractVectorSpace v =>
((Scalar (VectorSpaceImplementation v) ~ Scalar v) => ρ) -> ρ
scalarsSameInAbstraction @v
 ( forall a b c. Coercion a b -> Coercion (b -> c) (a -> c)
precomposeCoercion (forall a b. VSCCoercion a b -> Coercion a b
getVSCCoercion forall (f :: * -> * -> *) a b.
(Function f, Object f a, Object f b) =>
f a b -> a -> b
$ forall v.
Coercible (SubBasis v) (SubBasis (VectorSpaceImplementation v)) =>
VSCCoercion (SubBasis v) (SubBasis (VectorSpaceImplementation v))
abstractSubbasisCoercion @v)
  forall (f :: * -> * -> *) a b.
(Function f, Object f a, Object f b) =>
f a b -> a -> b
$ coerce :: forall a b. Coercible a b => a -> b
coerce (forall v w.
(FiniteDimensional v, LSpace w, Scalar w ~ Scalar v) =>
SubBasis v -> [w] -> (v +> w, [w])
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 :: forall v (f :: * -> *) w.
(AbstractLinearSpace v,
 FiniteDimensional (VectorSpaceImplementation v),
 Coercible (SubBasis v) (SubBasis (VectorSpaceImplementation v)),
 LinearSpace w, Scalar w ~ Scalar v, Functor f) =>
(f (Scalar w) -> w) -> f (DualVector v) -> v +> w
abstractVS_recomposeContraLinMap f (Scalar w) -> w
f = forall v ρ.
AbstractVectorSpace v =>
((Scalar (VectorSpaceImplementation v) ~ Scalar v) => ρ) -> ρ
scalarsSameInAbstraction @v
 ( coerce :: forall a b. Coercible a b => a -> b
coerce (forall v w (f :: * -> *).
(FiniteDimensional v, LinearSpace w, Scalar w ~ Scalar v,
 Functor f) =>
(f (Scalar w) -> w) -> f (DualVector v) -> v +> w
recomposeContraLinMap @(VectorSpaceImplementation v) @w @f f (Scalar w) -> w
f)
                forall κ (k :: κ -> κ -> *) (a :: κ) (b :: κ) (c :: κ).
(Category k, Object k a, Object k b, Object k c) =>
k b c -> k a b -> k a c
. forall (f :: * -> *) (r :: * -> * -> *) (t :: * -> * -> *) a b.
(Functor f r t, Object r a, Object t (f a), Object r b,
 Object t (f b)) =>
r a b -> t (f a) (f b)
fmap forall a c. AbstractDualVector a c -> DualVector c
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 :: forall 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, Functor f) =>
(f (Scalar w) -> w) -> f (v +> DualVector u) -> (v ⊗ u) +> w
abstractVS_recomposeLinMapTensor f (Scalar w) -> w
f = forall v ρ.
AbstractVectorSpace v =>
((Scalar (VectorSpaceImplementation v) ~ Scalar v) => ρ) -> ρ
scalarsSameInAbstraction @v
 ( coerce :: forall a b. Coercible a b => a -> b
coerce (forall v u w (f :: * -> *).
(FiniteDimensional v, FiniteDimensional u, LinearSpace w,
 Scalar u ~ Scalar v, Scalar w ~ Scalar v, Functor f) =>
(f (Scalar w) -> w) -> f (v +> DualVector u) -> (v ⊗ u) +> w
recomposeContraLinMapTensor @(VectorSpaceImplementation v) @u @w @f f (Scalar w) -> w
f)
              forall κ (k :: κ -> κ -> *) (a :: κ) (b :: κ) (c :: κ).
(Category k, Object k a, Object k b, Object k c) =>
k b c -> k a b -> k a c
. forall (f :: * -> *) (r :: * -> * -> *) (t :: * -> * -> *) a b.
(Functor f r t, Object r a, Object t (f a), Object r b,
 Object t (f b)) =>
r a b -> t (f a) (f b)
fmap (coerce :: forall a b. Coercible a b => a -> b
coerce :: (v+>DualVector u)
                          -> (VectorSpaceImplementation v+>DualVector u))
  )

abstractVS_uncanonicallyFromDual :: ∀ v . ( AbstractLinearSpace v
        , FiniteDimensional (VectorSpaceImplementation v) )
   => DualVector v -+> v
abstractVS_uncanonicallyFromDual :: forall v.
(AbstractLinearSpace v,
 FiniteDimensional (VectorSpaceImplementation v)) =>
DualVector v -+> v
abstractVS_uncanonicallyFromDual = forall v ρ.
AbstractVectorSpace v =>
((Scalar (VectorSpaceImplementation v) ~ Scalar v) => ρ) -> ρ
scalarsSameInAbstraction @v
 ( case forall a.
VSCCoercion
  (AbstractDualVector a (VectorSpaceImplementation a))
  (DualVector (VectorSpaceImplementation a))
abstractDualVectorCoercion @v of
            VSCCoercion
  (AbstractDualVector v (VectorSpaceImplementation v))
  (DualVector (VectorSpaceImplementation v))
VSCCoercion -> coerce :: forall a b. Coercible a b => a -> b
coerce (forall v. FiniteDimensional v => DualVector v -+> v
uncanonicallyFromDual @(VectorSpaceImplementation v))
  )

abstractVS_uncanonicallyToDual :: ∀ v . ( AbstractLinearSpace v
        , FiniteDimensional (VectorSpaceImplementation v) )
   => v -+> DualVector v
abstractVS_uncanonicallyToDual :: forall v.
(AbstractLinearSpace v,
 FiniteDimensional (VectorSpaceImplementation v)) =>
v -+> DualVector v
abstractVS_uncanonicallyToDual = forall v ρ.
AbstractVectorSpace v =>
((Scalar (VectorSpaceImplementation v) ~ Scalar v) => ρ) -> ρ
scalarsSameInAbstraction @v
 ( case forall a.
VSCCoercion
  (AbstractDualVector a (VectorSpaceImplementation a))
  (DualVector (VectorSpaceImplementation a))
abstractDualVectorCoercion @v of
            VSCCoercion
  (AbstractDualVector v (VectorSpaceImplementation v))
  (DualVector (VectorSpaceImplementation v))
VSCCoercion -> coerce :: forall a b. Coercible a b => a -> b
coerce (forall v. FiniteDimensional v => v -+> DualVector v
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 :: forall v w.
(AbstractLinearSpace v,
 FiniteDimensional (VectorSpaceImplementation v), TensorSpace w,
 Eq w, Scalar w ~ Scalar v) =>
(v ⊗ w) -> (v ⊗ w) -> Bool
abstractVS_tensorEquality = forall v ρ.
AbstractVectorSpace v =>
((Scalar (VectorSpaceImplementation v) ~ Scalar v) => ρ) -> ρ
scalarsSameInAbstraction @v
 ( case forall v w.
AbstractTensorSpace v =>
VSCCoercion
  (TensorProduct v w) (TensorProduct (VectorSpaceImplementation v) w)
abstractTensorProductsCoercion @v @w of
    VSCCoercion
  (TensorProduct v w) (TensorProduct (VectorSpaceImplementation v) w)
VSCCoercion -> coerce :: forall a b. Coercible a b => a -> b
coerce (forall v w.
(FiniteDimensional v, TensorSpace w, Eq w, Scalar w ~ Scalar v) =>
(v ⊗ w) -> (v ⊗ w) -> Bool
tensorEquality @(VectorSpaceImplementation v) @w)
  )

abstractVS_dualBasisCandidates :: ∀ v . ( AbstractLinearSpace v
        , SemiInner (VectorSpaceImplementation v) )
      => [(Int, v)] -> Forest (Int, DualVector v)
abstractVS_dualBasisCandidates :: forall v.
(AbstractLinearSpace v, SemiInner (VectorSpaceImplementation v)) =>
[(Int, v)] -> Forest (Int, DualVector v)
abstractVS_dualBasisCandidates = forall v ρ.
AbstractVectorSpace v =>
((Scalar (VectorSpaceImplementation v) ~ Scalar v) => ρ) -> ρ
scalarsSameInAbstraction @v
 ( case forall a.
VSCCoercion
  (AbstractDualVector a (VectorSpaceImplementation a))
  (DualVector (VectorSpaceImplementation a))
abstractDualVectorCoercion @v of
            VSCCoercion
  (AbstractDualVector v (VectorSpaceImplementation v))
  (DualVector (VectorSpaceImplementation v))
VSCCoercion -> coerce :: forall a b. Coercible a b => a -> b
coerce (forall v. SemiInner v => [(Int, v)] -> Forest (Int, DualVector v)
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 :: forall 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 = forall v ρ.
AbstractVectorSpace v =>
((Scalar (VectorSpaceImplementation v) ~ Scalar v) => ρ) -> ρ
scalarsSameInAbstraction @v
 ( case (forall v. LinearSpace v => DualSpaceWitness v
dualSpaceWitness @v, forall v. LinearSpace v => DualSpaceWitness v
dualSpaceWitness @w) of
    (DualSpaceWitness v
DualSpaceWitness, DualSpaceWitness w
DualSpaceWitness)
         -> case ( forall a.
VSCCoercion
  (AbstractDualVector a (VectorSpaceImplementation a))
  (DualVector (VectorSpaceImplementation a))
abstractDualVectorCoercion @v
                 , forall v w.
AbstractTensorSpace v =>
VSCCoercion
  (TensorProduct v w) (TensorProduct (VectorSpaceImplementation v) w)
abstractTensorProductsCoercion @v @(DualVector w)
                 , forall v w.
AbstractTensorSpace v =>
VSCCoercion
  (TensorProduct v w) (TensorProduct (VectorSpaceImplementation v) w)
abstractTensorProductsCoercion @v @w
                 ) of
       (VSCCoercion
  (AbstractDualVector v (VectorSpaceImplementation v))
  (DualVector (VectorSpaceImplementation v))
VSCCoercion, VSCCoercion
  (TensorProduct v (DualVector w))
  (TensorProduct (VectorSpaceImplementation v) (DualVector w))
VSCCoercion, VSCCoercion
  (TensorProduct v w) (TensorProduct (VectorSpaceImplementation v) w)
VSCCoercion)
          -> coerce :: forall a b. Coercible a b => a -> b
coerce (forall v w.
(SemiInner v, SemiInner w, Scalar w ~ Scalar v) =>
[(Int, v ⊗ w)] -> Forest (Int, DualVector (v ⊗ w))
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 :: forall v.
(AbstractLinearSpace v, LinearSpace v,
 SemiInner (VectorSpaceImplementation v)) =>
[(Int, SymmetricTensor (Scalar v) v)]
-> Forest (Int, SymmetricTensor (Scalar v) (DualVector v))
abstractVS_symTensorDualBasisCandidates = forall v ρ.
AbstractVectorSpace v =>
((Scalar (VectorSpaceImplementation v) ~ Scalar v) => ρ) -> ρ
scalarsSameInAbstraction @v
 ( case ( forall v. LinearSpace v => DualSpaceWitness v
dualSpaceWitness @v
        , forall v. LinearSpace v => DualSpaceWitness v
dualSpaceWitness @(VectorSpaceImplementation v)
        , forall a.
VSCCoercion
  (AbstractDualVector a (VectorSpaceImplementation a))
  (DualVector (VectorSpaceImplementation a))
abstractDualVectorCoercion @v ) of
    (DualSpaceWitness v
DualSpaceWitness, DualSpaceWitness (VectorSpaceImplementation v)
DualSpaceWitness, VSCCoercion
  (AbstractDualVector v (VectorSpaceImplementation v))
  (DualVector (VectorSpaceImplementation v))
crdv)
       -> case ( forall v w.
AbstractTensorSpace v =>
VSCCoercion
  (TensorProduct v w) (TensorProduct (VectorSpaceImplementation v) w)
abstractTensorProductsCoercion @v @v
               , forall v (p :: * -> *) a b.
(TensorSpace v, Functor p) =>
p v
-> VSCCoercion a b
-> VSCCoercion (TensorProduct v a) (TensorProduct v b)
coerceFmapTensorProduct @(DualVector (VectorSpaceImplementation v)) []
                   VSCCoercion
  (AbstractDualVector v (VectorSpaceImplementation v))
  (DualVector (VectorSpaceImplementation v))
crdv
               , forall v (p :: * -> *) a b.
(TensorSpace v, Functor p) =>
p v
-> VSCCoercion a b
-> VSCCoercion (TensorProduct v a) (TensorProduct v b)
coerceFmapTensorProduct @(VectorSpaceImplementation v) []
                   VSCCoercion
  (AbstractDualVector v (VectorSpaceImplementation v))
  (DualVector (VectorSpaceImplementation v))
crdv
               , forall v (p :: * -> *) a b.
(TensorSpace v, Functor p) =>
p v
-> VSCCoercion a b
-> VSCCoercion (TensorProduct v a) (TensorProduct v b)
coerceFmapTensorProduct @(VectorSpaceImplementation v) []
                   (forall a b. Coercible a b => VSCCoercion a b
VSCCoercion @v @(VectorSpaceImplementation v))
               ) of
     (VSCCoercion
  (TensorProduct v v) (TensorProduct (VectorSpaceImplementation v) v)
VSCCoercion, VSCCoercion
  (TensorProduct
     (DualVector (VectorSpaceImplementation v))
     (AbstractDualVector v (VectorSpaceImplementation v)))
  (TensorProduct
     (DualVector (VectorSpaceImplementation v))
     (DualVector (VectorSpaceImplementation v)))
VSCCoercion, VSCCoercion
  (TensorProduct
     (VectorSpaceImplementation v)
     (AbstractDualVector v (VectorSpaceImplementation v)))
  (TensorProduct
     (VectorSpaceImplementation v)
     (DualVector (VectorSpaceImplementation v)))
VSCCoercion, VSCCoercion
  (TensorProduct (VectorSpaceImplementation v) v)
  (TensorProduct
     (VectorSpaceImplementation v) (VectorSpaceImplementation v))
VSCCoercion)
        -> coerce :: forall a b. Coercible a b => a -> b
coerce (forall v.
SemiInner v =>
[(Int, SymmetricTensor (Scalar v) v)]
-> Forest (Int, SymmetricTensor (Scalar v) (DualVector v))
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 :: Q Type -> [Name] -> Q [Dec]
copyNewtypeInstances Q Type
cxtv [Name]
classes = do

 ([TyVarBndr Specificity]
tvbs, Q Cxt
cxt, (Q Type
a,Q Type
c)) <- do
   ([TyVarBndr Specificity]
tvbs', Cxt
cxt', Type
a') <- Q Type -> Q ([TyVarBndr Specificity], Cxt, Type)
deQuantifyType Q Type
cxtv
   let extractImplementationType :: Type -> [TyVarBndr Specificity] -> Q Type
extractImplementationType (AppT Type
tc (VarT Name
tvb)) [TyVarBndr Specificity]
atvbs
#if MIN_VERSION_template_haskell(2,17,0)
              = Type -> [TyVarBndr Specificity] -> Q Type
extractImplementationType Type
tc forall (f :: * -> * -> *) a b.
(Function f, Object f a, Object f b) =>
f a b -> a -> b
$ [TyVarBndr Specificity]
atvbsforall a. [a] -> [a] -> [a]
++[forall flag. Name -> flag -> TyVarBndr flag
PlainTV Name
tvb Specificity
SpecifiedSpec]
#else
              = extractImplementationType tc $ atvbs++[PlainTV tvb]
#endif
       extractImplementationType (ConT Name
aName) [TyVarBndr Specificity]
atvbs = do
         Name -> Q DatatypeInfo
D.reifyDatatype Name
aName forall (f :: * -> * -> *) (m :: * -> *) a b.
(Function f, Monad m f, Object f a, Object f b, Object f (m a),
 Object f (m b), Object f (m (m b))) =>
m a -> f a (m b) -> m b
>>= \case
          D.DatatypeInfo{ datatypeVariant :: DatatypeInfo -> DatatypeVariant
D.datatypeVariant = DatatypeVariant
D.Newtype
                        , datatypeVars :: DatatypeInfo -> [TyVarBndr ()]
D.datatypeVars = [TyVarBndr ()]
dttvbs
                        , datatypeCons :: DatatypeInfo -> [ConstructorInfo]
D.datatypeCons = [
                           D.ConstructorInfo
                              { constructorFields :: ConstructorInfo -> Cxt
D.constructorFields = [Type
c''] } ]
                        }
#if MIN_VERSION_template_haskell(2,17,0)
             -> let replaceTVs :: [TyVarBndr ()] -> [TyVarBndr Specificity] -> Type -> Type
                    replaceTVs :: [TyVarBndr ()] -> [TyVarBndr Specificity] -> Type -> Type
replaceTVs (PlainTV Name
infoTV ()
_:[TyVarBndr ()]
infoTVs)
                               (PlainTV Name
instTV Specificity
_:[TyVarBndr Specificity]
instTVs)
                        = [TyVarBndr ()] -> [TyVarBndr Specificity] -> Type -> Type
replaceTVs [TyVarBndr ()]
infoTVs [TyVarBndr Specificity]
instTVs forall κ (k :: κ -> κ -> *) (a :: κ) (b :: κ) (c :: κ).
(Category k, Object k a, Object k b, Object k c) =>
k b c -> k a b -> k a c
. Name -> Name -> Type -> Type
replaceTV Name
infoTV Name
instTV
                    replaceTVs (KindedTV Name
infoTV ()
flag Type
_:[TyVarBndr ()]
infoTVs) [TyVarBndr Specificity]
instTVs
                        = [TyVarBndr ()] -> [TyVarBndr Specificity] -> Type -> Type
replaceTVs (forall flag. Name -> flag -> TyVarBndr flag
PlainTV Name
infoTV ()
flagforall a. a -> [a] -> [a]
:[TyVarBndr ()]
infoTVs) [TyVarBndr Specificity]
instTVs
                    replaceTVs [TyVarBndr ()]
infoTVs (KindedTV Name
instTV Specificity
flag Type
_:[TyVarBndr Specificity]
instTVs)
                        = [TyVarBndr ()] -> [TyVarBndr Specificity] -> Type -> Type
replaceTVs [TyVarBndr ()]
infoTVs (forall flag. Name -> flag -> TyVarBndr flag
PlainTV Name
instTV Specificity
flagforall a. a -> [a] -> [a]
:[TyVarBndr Specificity]
instTVs)
#else
             -> let replaceTVs :: [TyVarBndr] -> [TyVarBndr] -> Type -> Type
                    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)
#endif
                    replaceTVs [] [] = forall κ (k :: κ -> κ -> *) (a :: κ).
(Category k, Object k a) =>
k a a
id
                    replaceTVs [TyVarBndr ()]
infoTVs [TyVarBndr Specificity]
instTVs
                        = forall a. HasCallStack => [Char] -> a
error forall (f :: * -> * -> *) a b.
(Function f, Object f a, Object f b) =>
f a b -> a -> b
$ [Char]
"infoTVs = "forall a. [a] -> [a] -> [a]
++forall a. Show a => a -> [Char]
show [TyVarBndr ()]
infoTVsforall a. [a] -> [a] -> [a]
++[Char]
", instTVs = "forall a. [a] -> [a] -> [a]
++forall a. Show a => a -> [Char]
show [TyVarBndr Specificity]
instTVs
                    replaceTV :: Name -> Name -> Type -> Type
                    replaceTV :: Name -> Name -> Type -> Type
replaceTV Name
infoTV Name
instTV (AppT Type
tc (VarT Name
tv))
                     | Name
tvforall a. Eq a => a -> a -> Bool
==Name
infoTV  = Type -> Type -> Type
AppT (Name -> Name -> Type -> Type
replaceTV Name
infoTV Name
instTV Type
tc) (Name -> Type
VarT Name
instTV)
                    replaceTV Name
infoTV Name
instTV (AppT Type
tc Type
ta)
                           = Type -> Type -> Type
AppT (Name -> Name -> Type -> Type
replaceTV Name
infoTV Name
instTV Type
tc)
                                  (Name -> Name -> Type -> Type
replaceTV Name
infoTV Name
instTV Type
ta)
                    replaceTV Name
_ Name
_ t :: Type
t@(TupleT Int
_) = Type
t
                    replaceTV Name
_ Name
_ t :: Type
t@(ConT Name
_) = Type
t
                    replaceTV Name
_ Name
_ Type
t
                        = forall a. HasCallStack => [Char] -> a
error forall (f :: * -> * -> *) a b.
(Function f, Object f a, Object f b) =>
f a b -> a -> b
$ [Char]
"Don't know how to substitute type variables in "
                                    forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> [Char]
show Type
t
                in forall (m :: * -> *) a. Monad m (->) => a -> m a
return forall (f :: * -> * -> *) a b.
(Function f, Object f a, Object f b) =>
f a b -> a -> b
$ [TyVarBndr ()] -> [TyVarBndr Specificity] -> Type -> Type
replaceTVs [TyVarBndr ()]
dttvbs [TyVarBndr Specificity]
atvbs Type
c''
          DatatypeInfo
_ -> forall a. HasCallStack => [Char] -> a
error forall (f :: * -> * -> *) a b.
(Function f, Object f a, Object f b) =>
f a b -> a -> b
$ forall a. Show a => a -> [Char]
show Name
aName forall a. [a] -> [a] -> [a]
++ [Char]
" is not a newtype."
       extractImplementationType Type
a'' [TyVarBndr Specificity]
_
           = forall a. HasCallStack => [Char] -> a
error forall (f :: * -> * -> *) a b.
(Function f, Object f a, Object f b) =>
f a b -> a -> b
$ [Char]
"Don't know how to handle type "forall a. [a] -> [a] -> [a]
++forall a. Show a => a -> [Char]
show Type
a''
                            forall a. [a] -> [a] -> [a]
++[Char]
" (specified: "forall a. [a] -> [a] -> [a]
++forall a. Show a => a -> [Char]
show Type
a'forall a. [a] -> [a] -> [a]
++[Char]
")"
   Type
c' <- Type -> [TyVarBndr Specificity] -> Q Type
extractImplementationType Type
a' []
   forall (m :: * -> *) a. Monad m (->) => a -> m a
return ([TyVarBndr Specificity]
tvbs', forall (f :: * -> *) (r :: * -> * -> *) (t :: * -> * -> *) a.
(Applicative f r t, Object r a, Object t (f a)) =>
t a (f a)
pure Cxt
cxt', (forall (f :: * -> *) (r :: * -> * -> *) (t :: * -> * -> *) a.
(Applicative f r t, Object r a, Object t (f a)) =>
t a (f a)
pure Type
a', forall (f :: * -> *) (r :: * -> * -> *) (t :: * -> * -> *) a.
(Applicative f r t, Object r a, Object t (f a)) =>
t a (f a)
pure Type
c'))
 
 let allClasses :: [Name]
allClasses =
       [ ''AbstractAdditiveGroup | ()
_<-[()], ''AdditiveGroup forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [Name]
classes ]
      forall a. [a] -> [a] -> [a]
++ [ ''AbstractVectorSpace | ()
_<-[()], ''VectorSpace forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [Name]
classes ]
      forall a. [a] -> [a] -> [a]
++ [ ''AbstractTensorSpace | ()
_<-[()], ''TensorSpace forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [Name]
classes ]
      forall a. [a] -> [a] -> [a]
++ [ ''AbstractLinearSpace | ()
_<-[()], ''LinearSpace forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [Name]
classes ]
      forall a. [a] -> [a] -> [a]
++ [Name]
classes

 Int
vtnameHash <- forall a. Num a => a -> a
abs forall κ (k :: κ -> κ -> *) (a :: κ) (b :: κ) (c :: κ).
(Category k, Object k a, Object k b, Object k c) =>
k b c -> k a b -> k a c
. forall a. Hashable a => a -> Int
hash forall κ (k :: κ -> κ -> *) (a :: κ) (b :: κ) (c :: κ).
(Category k, Object k a, Object k b, Object k c) =>
k b c -> k a b -> k a c
. forall a. Show a => a -> [Char]
show forall (f :: * -> *) (r :: * -> * -> *) a b.
(Functor f r (->), Object r a, Object r b) =>
r a b -> f a -> f b
<$> Q Type
a

 forall (s :: * -> *) (t :: * -> *) (k :: * -> * -> *)
       (l :: * -> * -> *) (f :: * -> *) a.
(Traversable s t k l, k ~ l, s ~ t, Monoidal f k k,
 ObjectPair k a (t a), ObjectPair k (f a) (f (t a)),
 Object k (t (f a)), TraversalObject k t a) =>
k (t (f a)) (f (t a))
sequence [case [Char]
dClass of
     [Char]
"AbstractAdditiveGroup" -> Maybe Overlap -> Cxt -> Type -> [Dec] -> Dec
InstanceD forall a. Maybe a
Nothing forall (f :: * -> *) (r :: * -> * -> *) a b.
(Functor f r (->), Object r a, Object r b) =>
r a b -> f a -> f b
<$> Q Cxt
cxt forall (f :: * -> *) (r :: * -> * -> *) (t :: * -> * -> *) a b.
(Applicative f r t, ObjectMorphism r a b,
 ObjectMorphism t (f a) (f b), Object t (t (f a) (f b)),
 ObjectPair r (r a b) a, ObjectPair t (f (r a b)) (f a), Object r a,
 Object r b) =>
t (f (r a b)) (t (f a) (f b))
<*>
                          [t|AbstractAdditiveGroup $a|] forall (f :: * -> *) (r :: * -> * -> *) (t :: * -> * -> *) a b.
(Applicative f r t, ObjectMorphism r a b,
 ObjectMorphism t (f a) (f b), Object t (t (f a) (f b)),
 ObjectPair r (r a b) a, ObjectPair t (f (r a b)) (f a), Object r a,
 Object r b) =>
t (f (r a b)) (t (f a) (f b))
<*> [d|
         type instance VectorSpaceImplementation $a = $c
      |]
     [Char]
"AdditiveGroup" -> Maybe Overlap -> Cxt -> Type -> [Dec] -> Dec
InstanceD forall a. Maybe a
Nothing forall (f :: * -> *) (r :: * -> * -> *) a b.
(Functor f r (->), Object r a, Object r b) =>
r a b -> f a -> f b
<$> Q Cxt
cxt forall (f :: * -> *) (r :: * -> * -> *) (t :: * -> * -> *) a b.
(Applicative f r t, ObjectMorphism r a b,
 ObjectMorphism t (f a) (f b), Object t (t (f a) (f b)),
 ObjectPair r (r a b) a, ObjectPair t (f (r a b)) (f a), Object r a,
 Object r b) =>
t (f (r a b)) (t (f a) (f b))
<*>
                          [t|AdditiveGroup $a|] forall (f :: * -> *) (r :: * -> * -> *) (t :: * -> * -> *) a b.
(Applicative f r t, ObjectMorphism r a b,
 ObjectMorphism t (f a) (f b), Object t (t (f a) (f b)),
 ObjectPair r (r a b) a, ObjectPair t (f (r a b)) (f a), Object r a,
 Object r b) =>
t (f (r a b)) (t (f a) (f b))
<*> [d|
         $(varP 'zeroV) = abstractVS_zeroV
         $(varP '(^+^)) = abstractVS_addvs
         $(varP '(^-^)) = abstractVS_subvs
         $(varP 'negateV) = abstractVS_negateV
      |]
     [Char]
"AffineSpace" -> Maybe Overlap -> Cxt -> Type -> [Dec] -> Dec
InstanceD forall a. Maybe a
Nothing forall (f :: * -> *) (r :: * -> * -> *) a b.
(Functor f r (->), Object r a, Object r b) =>
r a b -> f a -> f b
<$> Q Cxt
cxt forall (f :: * -> *) (r :: * -> * -> *) (t :: * -> * -> *) a b.
(Applicative f r t, ObjectMorphism r a b,
 ObjectMorphism t (f a) (f b), Object t (t (f a) (f b)),
 ObjectPair r (r a b) a, ObjectPair t (f (r a b)) (f a), Object r a,
 Object r b) =>
t (f (r a b)) (t (f a) (f b))
<*>
                          [t|AffineSpace $a|] forall (f :: * -> *) (r :: * -> * -> *) (t :: * -> * -> *) a b.
(Applicative f r t, ObjectMorphism r a b,
 ObjectMorphism t (f a) (f b), Object t (t (f a) (f b)),
 ObjectPair r (r a b) a, ObjectPair t (f (r a b)) (f a), Object r a,
 Object r b) =>
t (f (r a b)) (t (f a) (f b))
<*> [d|
         type instance Diff $a = $a
         $(varP '(.-.)) = abstractVS_subvs
         $(varP '(.+^)) = abstractVS_addvs
      |]
     [Char]
"VectorSpace" -> Maybe Overlap -> Cxt -> Type -> [Dec] -> Dec
InstanceD forall a. Maybe a
Nothing forall (f :: * -> *) (r :: * -> * -> *) a b.
(Functor f r (->), Object r a, Object r b) =>
r a b -> f a -> f b
<$> Q Cxt
cxt forall (f :: * -> *) (r :: * -> * -> *) (t :: * -> * -> *) a b.
(Applicative f r t, ObjectMorphism r a b,
 ObjectMorphism t (f a) (f b), Object t (t (f a) (f b)),
 ObjectPair r (r a b) a, ObjectPair t (f (r a b)) (f a), Object r a,
 Object r b) =>
t (f (r a b)) (t (f a) (f b))
<*>
                          [t|VectorSpace $a|] forall (f :: * -> *) (r :: * -> * -> *) (t :: * -> * -> *) a b.
(Applicative f r t, ObjectMorphism r a b,
 ObjectMorphism t (f a) (f b), Object t (t (f a) (f b)),
 ObjectPair r (r a b) a, ObjectPair t (f (r a b)) (f a), Object r a,
 Object r b) =>
t (f (r a b)) (t (f a) (f b))
<*> [d|
         type instance Scalar $a = Scalar ($c)
         $(varP '(*^)) = abstractVS_scalev
      |]
     [Char]
"AbstractVectorSpace" -> Maybe Overlap -> Cxt -> Type -> [Dec] -> Dec
InstanceD forall a. Maybe a
Nothing forall (f :: * -> *) (r :: * -> * -> *) a b.
(Functor f r (->), Object r a, Object r b) =>
r a b -> f a -> f b
<$> Q Cxt
cxt forall (f :: * -> *) (r :: * -> * -> *) (t :: * -> * -> *) a b.
(Applicative f r t, ObjectMorphism r a b,
 ObjectMorphism t (f a) (f b), Object t (t (f a) (f b)),
 ObjectPair r (r a b) a, ObjectPair t (f (r a b)) (f a), Object r a,
 Object r b) =>
t (f (r a b)) (t (f a) (f b))
<*>
                          [t|AbstractVectorSpace $a|] forall (f :: * -> *) (r :: * -> * -> *) (t :: * -> * -> *) a b.
(Applicative f r t, ObjectMorphism r a b,
 ObjectMorphism t (f a) (f b), Object t (t (f a) (f b)),
 ObjectPair r (r a b) a, ObjectPair t (f (r a b)) (f a), Object r a,
 Object r b) =>
t (f (r a b)) (t (f a) (f b))
<*> [d|
         $(varP 'scalarsSameInAbstraction)
            = abstractVS_scalarsSameInAbstraction @($a)
      |]
     [Char]
"InnerSpace" -> Maybe Overlap -> Cxt -> Type -> [Dec] -> Dec
InstanceD forall a. Maybe a
Nothing forall (f :: * -> *) (r :: * -> * -> *) a b.
(Functor f r (->), Object r a, Object r b) =>
r a b -> f a -> f b
<$> Q Cxt
cxt forall (f :: * -> *) (r :: * -> * -> *) (t :: * -> * -> *) a b.
(Applicative f r t, ObjectMorphism r a b,
 ObjectMorphism t (f a) (f b), Object t (t (f a) (f b)),
 ObjectPair r (r a b) a, ObjectPair t (f (r a b)) (f a), Object r a,
 Object r b) =>
t (f (r a b)) (t (f a) (f b))
<*>
                          [t|InnerSpace $a|] forall (f :: * -> *) (r :: * -> * -> *) (t :: * -> * -> *) a b.
(Applicative f r t, ObjectMorphism r a b,
 ObjectMorphism t (f a) (f b), Object t (t (f a) (f b)),
 ObjectPair r (r a b) a, ObjectPair t (f (r a b)) (f a), Object r a,
 Object r b) =>
t (f (r a b)) (t (f a) (f b))
<*> [d|
         $(varP '(<.>)) = abstractVS_innerProd
      |]
     [Char]
"Semimanifold" -> Maybe Overlap -> Cxt -> Type -> [Dec] -> Dec
InstanceD forall a. Maybe a
Nothing forall (f :: * -> *) (r :: * -> * -> *) a b.
(Functor f r (->), Object r a, Object r b) =>
r a b -> f a -> f b
<$> Q Cxt
cxt forall (f :: * -> *) (r :: * -> * -> *) (t :: * -> * -> *) a b.
(Applicative f r t, ObjectMorphism r a b,
 ObjectMorphism t (f a) (f b), Object t (t (f a) (f b)),
 ObjectPair r (r a b) a, ObjectPair t (f (r a b)) (f a), Object r a,
 Object r b) =>
t (f (r a b)) (t (f a) (f b))
<*>
                          [t|Semimanifold $a|] forall (f :: * -> *) (r :: * -> * -> *) (t :: * -> * -> *) a b.
(Applicative f r t, ObjectMorphism r a b,
 ObjectMorphism t (f a) (f b), Object t (t (f a) (f b)),
 ObjectPair r (r a b) a, ObjectPair t (f (r a b)) (f a), Object r a,
 Object r b) =>
t (f (r a b)) (t (f a) (f b))
<*> [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
      |]
     [Char]
"PseudoAffine" -> Maybe Overlap -> Cxt -> Type -> [Dec] -> Dec
InstanceD forall a. Maybe a
Nothing forall (f :: * -> *) (r :: * -> * -> *) a b.
(Functor f r (->), Object r a, Object r b) =>
r a b -> f a -> f b
<$> Q Cxt
cxt forall (f :: * -> *) (r :: * -> * -> *) (t :: * -> * -> *) a b.
(Applicative f r t, ObjectMorphism r a b,
 ObjectMorphism t (f a) (f b), Object t (t (f a) (f b)),
 ObjectPair r (r a b) a, ObjectPair t (f (r a b)) (f a), Object r a,
 Object r b) =>
t (f (r a b)) (t (f a) (f b))
<*>
                          [t|PseudoAffine $a|] forall (f :: * -> *) (r :: * -> * -> *) (t :: * -> * -> *) a b.
(Applicative f r t, ObjectMorphism r a b,
 ObjectMorphism t (f a) (f b), Object t (t (f a) (f b)),
 ObjectPair r (r a b) a, ObjectPair t (f (r a b)) (f a), Object r a,
 Object r b) =>
t (f (r a b)) (t (f a) (f b))
<*> [d|
         $(varP '(.-~.)) = \p q -> Just (abstractVS_subvs p q)
         $(varP '(.-~!)) = abstractVS_subvs
      |]
     [Char]
"TensorSpace" -> Maybe Overlap -> Cxt -> Type -> [Dec] -> Dec
InstanceD forall a. Maybe a
Nothing forall (f :: * -> *) (r :: * -> * -> *) a b.
(Functor f r (->), Object r a, Object r b) =>
r a b -> f a -> f b
<$> Q Cxt
cxt forall (f :: * -> *) (r :: * -> * -> *) (t :: * -> * -> *) a b.
(Applicative f r t, ObjectMorphism r a b,
 ObjectMorphism t (f a) (f b), Object t (t (f a) (f b)),
 ObjectPair r (r a b) a, ObjectPair t (f (r a b)) (f a), Object r a,
 Object r b) =>
t (f (r a b)) (t (f a) (f b))
<*>
                          [t|TensorSpace $a|] forall (f :: * -> *) (r :: * -> * -> *) (t :: * -> * -> *) a b.
(Applicative f r t, ObjectMorphism r a b,
 ObjectMorphism t (f a) (f b), Object t (t (f a) (f b)),
 ObjectPair r (r a b) a, ObjectPair t (f (r a b)) (f a), Object r a,
 Object r b) =>
t (f (r a b)) (t (f a) (f b))
<*> [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
      |]
     [Char]
"AbstractTensorSpace" -> Maybe Overlap -> Cxt -> Type -> [Dec] -> Dec
InstanceD forall a. Maybe a
Nothing forall (f :: * -> *) (r :: * -> * -> *) a b.
(Functor f r (->), Object r a, Object r b) =>
r a b -> f a -> f b
<$> Q Cxt
cxt forall (f :: * -> *) (r :: * -> * -> *) (t :: * -> * -> *) a b.
(Applicative f r t, ObjectMorphism r a b,
 ObjectMorphism t (f a) (f b), Object t (t (f a) (f b)),
 ObjectPair r (r a b) a, ObjectPair t (f (r a b)) (f a), Object r a,
 Object r b) =>
t (f (r a b)) (t (f a) (f b))
<*>
                          [t|AbstractTensorSpace $a|] forall (f :: * -> *) (r :: * -> * -> *) (t :: * -> * -> *) a b.
(Applicative f r t, ObjectMorphism r a b,
 ObjectMorphism t (f a) (f b), Object t (t (f a) (f b)),
 ObjectPair r (r a b) a, ObjectPair t (f (r a b)) (f a), Object r a,
 Object r b) =>
t (f (r a b)) (t (f a) (f b))
<*> [d|
         $(varP 'abstractTensorProductsCoercion)
                  = VSCCoercion
      |]
     [Char]
"LinearSpace" -> Maybe Overlap -> Cxt -> Type -> [Dec] -> Dec
InstanceD forall a. Maybe a
Nothing forall (f :: * -> *) (r :: * -> * -> *) a b.
(Functor f r (->), Object r a, Object r b) =>
r a b -> f a -> f b
<$> Q Cxt
cxt forall (f :: * -> *) (r :: * -> * -> *) (t :: * -> * -> *) a b.
(Applicative f r t, ObjectMorphism r a b,
 ObjectMorphism t (f a) (f b), Object t (t (f a) (f b)),
 ObjectPair r (r a b) a, ObjectPair t (f (r a b)) (f a), Object r a,
 Object r b) =>
t (f (r a b)) (t (f a) (f b))
<*>
                          [t|LinearSpace $a|] forall (f :: * -> *) (r :: * -> * -> *) (t :: * -> * -> *) a b.
(Applicative f r t, ObjectMorphism r a b,
 ObjectMorphism t (f a) (f b), Object t (t (f a) (f b)),
 ObjectPair r (r a b) a, ObjectPair t (f (r a b)) (f a), Object r a,
 Object r b) =>
t (f (r a b)) (t (f a) (f b))
<*> [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
      |]
     [Char]
"AbstractLinearSpace" -> Maybe Overlap -> Cxt -> Type -> [Dec] -> Dec
InstanceD forall a. Maybe a
Nothing forall (f :: * -> *) (r :: * -> * -> *) a b.
(Functor f r (->), Object r a, Object r b) =>
r a b -> f a -> f b
<$> Q Cxt
cxt forall (f :: * -> *) (r :: * -> * -> *) (t :: * -> * -> *) a b.
(Applicative f r t, ObjectMorphism r a b,
 ObjectMorphism t (f a) (f b), Object t (t (f a) (f b)),
 ObjectPair r (r a b) a, ObjectPair t (f (r a b)) (f a), Object r a,
 Object r b) =>
t (f (r a b)) (t (f a) (f b))
<*>
                          [t|AbstractLinearSpace $a|] forall (f :: * -> *) (r :: * -> * -> *) (t :: * -> * -> *) a b.
(Applicative f r t, ObjectMorphism r a b,
 ObjectMorphism t (f a) (f b), Object t (t (f a) (f b)),
 ObjectPair r (r a b) a, ObjectPair t (f (r a b)) (f a), Object r a,
 Object r b) =>
t (f (r a b)) (t (f a) (f b))
<*> [d|
      |]
     [Char]
"FiniteDimensional" -> Maybe Overlap -> Cxt -> Type -> [Dec] -> Dec
InstanceD forall a. Maybe a
Nothing forall (f :: * -> *) (r :: * -> * -> *) a b.
(Functor f r (->), Object r a, Object r b) =>
r a b -> f a -> f b
<$> Q Cxt
cxt forall (f :: * -> *) (r :: * -> * -> *) (t :: * -> * -> *) a b.
(Applicative f r t, ObjectMorphism r a b,
 ObjectMorphism t (f a) (f b), Object t (t (f a) (f b)),
 ObjectPair r (r a b) a, ObjectPair t (f (r a b)) (f a), Object r a,
 Object r b) =>
t (f (r a b)) (t (f a) (f b))
<*>
                          [t|FiniteDimensional $a|] forall (f :: * -> *) (r :: * -> * -> *) (t :: * -> * -> *) a b.
(Applicative f r t, ObjectMorphism r a b,
 ObjectMorphism t (f a) (f b), Object t (t (f a) (f b)),
 ObjectPair r (r a b) a, ObjectPair t (f (r a b)) (f a), Object r a,
 Object r b) =>
t (f (r a b)) (t (f a) (f b))
<*> do
        Name
subBasisCstr <- forall (m :: * -> *). Quote m => [Char] -> m Name
newName forall (f :: * -> * -> *) a b.
(Function f, Object f a, Object f b) =>
f a b -> a -> b
$ [Char]
"SubBasis"forall a. [a] -> [a] -> [a]
++forall a. Show a => a -> [Char]
show Int
vtnameHash
        
        [Dec]
tySyns <- forall (s :: * -> *) (t :: * -> *) (k :: * -> * -> *)
       (l :: * -> * -> *) (f :: * -> *) a.
(Traversable s t k l, k ~ l, s ~ t, Monoidal f k k,
 ObjectPair k a (t a), ObjectPair k (f a) (f (t a)),
 Object k (t (f a)), TraversalObject k t a) =>
k (t (f a)) (f (t a))
sequence [
#if MIN_VERSION_template_haskell(2,15,0)
           Cxt
-> Maybe [TyVarBndr ()]
-> Type
-> Maybe Type
-> Con
-> [DerivClause]
-> Dec
NewtypeInstD [] (forall a. a -> Maybe a
Just (
#if MIN_VERSION_template_haskell(2,17,0)
                                  forall a b. (a -> b) -> [a] -> [b]
map (forall (f :: * -> *) (r :: * -> * -> *) (t :: * -> * -> *) a b.
(Functor f r t, Object r a, Object t (f a), Object r b,
 Object t (f b)) =>
r a b -> t (f a) (f b)
fmap forall (f :: * -> * -> *) a b.
(Function f, Object f a, Object f b) =>
f a b -> a -> b
$ forall (a :: * -> * -> *) b x.
(WellPointed a, Object a b, ObjectPoint a x) =>
x -> a b x
const ()) [TyVarBndr Specificity]
tvbs
#else
                                  tvbs
#endif
                                      ))
              forall (f :: * -> *) (r :: * -> * -> *) a b.
(Functor f r (->), Object r a, Object r b) =>
r a b -> f a -> f b
<$> (Type -> Type -> Type
AppT (Name -> Type
ConT ''SubBasis) forall (f :: * -> *) (r :: * -> * -> *) a b.
(Functor f r (->), Object r a, Object r b) =>
r a b -> f a -> f b
<$> Q Type
a)
              forall (f :: * -> *) (r :: * -> * -> *) (t :: * -> * -> *) a b.
(Applicative f r t, ObjectMorphism r a b,
 ObjectMorphism t (f a) (f b), Object t (t (f a) (f b)),
 ObjectPair r (r a b) a, ObjectPair t (f (r a b)) (f a), Object r a,
 Object r b) =>
t (f (r a b)) (t (f a) (f b))
<*> forall (f :: * -> *) (r :: * -> * -> *) (t :: * -> * -> *) a.
(Applicative f r t, Object r a, Object t (f a)) =>
t a (f a)
pure forall a. Maybe a
Nothing
              forall (f :: * -> *) (r :: * -> * -> *) (t :: * -> * -> *) a b.
(Applicative f r t, ObjectMorphism r a b,
 ObjectMorphism t (f a) (f b), Object t (t (f a) (f b)),
 ObjectPair r (r a b) a, ObjectPair t (f (r a b)) (f a), Object r a,
 Object r b) =>
t (f (r a b)) (t (f a) (f b))
<*> (Name -> [BangType] -> Con
NormalC Name
subBasisCstr forall κ (k :: κ -> κ -> *) (a :: κ) (b :: κ) (c :: κ).
(Category k, Object k a, Object k b, Object k c) =>
k b c -> k a b -> k a c
. forall (f :: * -> *) (r :: * -> * -> *) (t :: * -> * -> *) a.
(Applicative f r t, Object r a, Object t (f a)) =>
t a (f a)
pure forall κ (k :: κ -> κ -> *) (a :: κ) (b :: κ) (c :: κ).
(Category k, Object k a, Object k b, Object k c) =>
k b c -> k a b -> k a c
.
                          (SourceUnpackedness -> SourceStrictness -> Bang
Bang SourceUnpackedness
NoSourceUnpackedness SourceStrictness
NoSourceStrictness,)
                     forall (f :: * -> *) (r :: * -> * -> *) a b.
(Functor f r (->), Object r a, Object r b) =>
r a b -> f a -> f b
<$> [t| SubBasis $c |])
              forall (f :: * -> *) (r :: * -> * -> *) (t :: * -> * -> *) a b.
(Applicative f r t, ObjectMorphism r a b,
 ObjectMorphism t (f a) (f b), Object t (t (f a) (f b)),
 ObjectPair r (r a b) a, ObjectPair t (f (r a b)) (f a), Object r a,
 Object r b) =>
t (f (r a b)) (t (f a) (f b))
<*> forall (f :: * -> *) (r :: * -> * -> *) (t :: * -> * -> *) a.
(Applicative f r t, Object r a, Object t (f a)) =>
t a (f a)
pure []
#else
           NewtypeInstD [] ''SubBasis
              <$> ((:[]) <$> a)
              <*> pure Nothing
              <*> (NormalC subBasisCstr . pure . 
                          (Bang NoSourceUnpackedness NoSourceStrictness,)
                     <$> [t| SubBasis $c |])
              <*> pure []
#endif
         ]
        [Dec]
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
          |]
        forall (m :: * -> *) a. Monad m (->) => a -> m a
return forall (f :: * -> * -> *) a b.
(Function f, Object f a, Object f b) =>
f a b -> a -> b
$ [Dec]
tySyns forall a. [a] -> [a] -> [a]
++ [Dec]
methods
     [Char]
"SemiInner" -> Maybe Overlap -> Cxt -> Type -> [Dec] -> Dec
InstanceD forall a. Maybe a
Nothing forall (f :: * -> *) (r :: * -> * -> *) a b.
(Functor f r (->), Object r a, Object r b) =>
r a b -> f a -> f b
<$> Q Cxt
cxt forall (f :: * -> *) (r :: * -> * -> *) (t :: * -> * -> *) a b.
(Applicative f r t, ObjectMorphism r a b,
 ObjectMorphism t (f a) (f b), Object t (t (f a) (f b)),
 ObjectPair r (r a b) a, ObjectPair t (f (r a b)) (f a), Object r a,
 Object r b) =>
t (f (r a b)) (t (f a) (f b))
<*>
                          [t|SemiInner $a|] forall (f :: * -> *) (r :: * -> * -> *) (t :: * -> * -> *) a b.
(Applicative f r t, ObjectMorphism r a b,
 ObjectMorphism t (f a) (f b), Object t (t (f a) (f b)),
 ObjectPair r (r a b) a, ObjectPair t (f (r a b)) (f a), Object r a,
 Object r b) =>
t (f (r a b)) (t (f a) (f b))
<*> [d|
          $(varP 'dualBasisCandidates) = abstractVS_dualBasisCandidates
          $(varP 'tensorDualBasisCandidates) = abstractVS_tensorDualBasisCandidates
          $(varP 'symTensorDualBasisCandidates) = abstractVS_symTensorDualBasisCandidates
       |]
     [Char]
_ -> forall a. HasCallStack => [Char] -> a
error forall (f :: * -> * -> *) a b.
(Function f, Object f a, Object f b) =>
f a b -> a -> b
$ [Char]
"Unsupported class to derive newtype instance for: ‘"forall a. [a] -> [a] -> [a]
++[Char]
dClassforall a. [a] -> [a] -> [a]
++[Char]
"’"
   | Name (OccName [Char]
dClass) NameFlavour
_ <- [Name]
allClasses
   ]