-- |
-- 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              #-}

module Math.LinearMap.Category.Instances.Deriving
   ( makeLinearSpaceFromBasis, makeFiniteDimensionalFromBasis
   -- * The instantiated classes
   , AffineSpace(..), Semimanifold(..), PseudoAffine(..)
   , TensorSpace(..), LinearSpace(..), FiniteDimensional(..), SemiInner(..)
   -- * Internals
   , BasisGeneratedSpace(..), LinearSpaceFromBasisDerivationConfig, def ) where

import Math.LinearMap.Category.Class
import Math.VectorSpace.Docile

import Data.VectorSpace
import Data.AffineSpace
import Data.Basis
import qualified Data.Map as Map
import Data.MemoTrie
import Data.Hashable

import Prelude ()
import qualified Prelude as Hask

import Control.Category.Constrained.Prelude
import Control.Arrow.Constrained

import Data.Coerce
import Data.Type.Coercion
import Data.Tagged
import Data.Traversable (traverse)
import Data.Default.Class

import Math.Manifold.Core.PseudoAffine
import Math.LinearMap.Asserted
import Math.VectorSpace.ZeroDimensional
import Data.VectorSpace.Free

import Language.Haskell.TH

-- | Given a type @V@ that is already a 'VectorSpace' and 'HasBasis', generate
--   the other class instances that are needed to use the type with this
--   library.
--
--   Prerequisites: (these can often be derived automatically,
--   using either the @newtype@ \/ @via@ strategy or generics \/ anyclass)
--
-- @
-- instance 'AdditiveGroup' V
--
-- instance 'VectorSpace' V where
--   type Scalar V = -- a simple number type, usually 'Double'
--
-- instance 'HasBasis' V where
--   type Basis V = -- a type with an instance of 'HasTrie'
-- @
--
--   Note that the 'Basis' does /not/ need to be orthonormal – in fact it
--   is not necessary to have a scalar product (i.e. an 'InnerSpace' instance)
--   at all.
--
--   This macro, invoked like
-- @
-- makeLinearSpaceFromBasis [t| V |]
-- @
--
--   will then generate @V@-instances for the classes 'Semimanifold',
--   'PseudoAffine', 'AffineSpace', 'TensorSpace' and 'LinearSpace'.
makeLinearSpaceFromBasis :: Q Type -> DecsQ
makeLinearSpaceFromBasis :: Q Type -> DecsQ
makeLinearSpaceFromBasis Q Type
v
   = LinearSpaceFromBasisDerivationConfig -> Q (Cxt, Type) -> DecsQ
makeLinearSpaceFromBasis' LinearSpaceFromBasisDerivationConfig
forall a. Default a => a
def (Q (Cxt, Type) -> DecsQ) -> Q (Cxt, Type) -> DecsQ
forall (f :: * -> * -> *) a b.
(Function f, Object f a, Object f b) =>
f a b -> a -> b
$ Q Type -> Q (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 (Cxt, Type) -> DecsQ
makeLinearSpaceFromBasis' :: LinearSpaceFromBasisDerivationConfig -> Q (Cxt, Type) -> DecsQ
makeLinearSpaceFromBasis' LinearSpaceFromBasisDerivationConfig
_ Q (Cxt, Type)
cxtv = do
 (Q Cxt
cxt,Q Type
v) <- do
   (Cxt
cxt', Type
v') <- Q (Cxt, Type)
cxtv
   (Q Cxt, Q Type) -> Q (Q Cxt, Q Type)
forall (m :: * -> *) a. Monad m (->) => a -> m a
return (Cxt -> Q Cxt
forall (f :: * -> *) (r :: * -> * -> *) (t :: * -> * -> *) a.
(Applicative f r t, Object r a, Object t (f a)) =>
t a (f a)
pure Cxt
cxt', Type -> Q Type
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 (Bool -> Bool) -> Bool -> Bool
forall (f :: * -> * -> *) a b.
(Function f, Object f a, Object f b) =>
f a b -> a -> b
$ (Extension -> Bool) -> [Extension] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (Extension -> [Extension] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem`[Extension]
exts) [Extension
TypeFamilies, Extension
ScopedTypeVariables, Extension
TypeApplications]
   then String -> Q ()
reportError String
"This macro requires -XTypeFamilies, -XScopedTypeVariables and -XTypeApplications."
   else () -> Q ()
forall (f :: * -> *) (r :: * -> * -> *) (t :: * -> * -> *) a.
(Applicative f r t, Object r a, Object t (f a)) =>
t a (f a)
pure ()
 
 [Q Dec] -> DecsQ
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 Maybe Overlap
forall a. Maybe a
Nothing (Cxt -> Type -> [Dec] -> Dec) -> Q Cxt -> Q (Type -> [Dec] -> Dec)
forall (f :: * -> *) (r :: * -> * -> *) a b.
(Functor f r (->), Object r a, Object r b) =>
r a b -> f a -> f b
<$> Q Cxt
cxt Q (Type -> [Dec] -> Dec) -> Q Type -> Q ([Dec] -> Dec)
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|] Q ([Dec] -> Dec) -> DecsQ -> Q Dec
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 Maybe Overlap
forall a. Maybe a
Nothing (Cxt -> Type -> [Dec] -> Dec) -> Q Cxt -> Q (Type -> [Dec] -> Dec)
forall (f :: * -> *) (r :: * -> * -> *) a b.
(Functor f r (->), Object r a, Object r b) =>
r a b -> f a -> f b
<$> Q Cxt
cxt Q (Type -> [Dec] -> Dec) -> Q Type -> Q ([Dec] -> Dec)
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|] Q ([Dec] -> Dec) -> DecsQ -> Q Dec
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 Maybe Overlap
forall a. Maybe a
Nothing (Cxt -> Type -> [Dec] -> Dec) -> Q Cxt -> Q (Type -> [Dec] -> Dec)
forall (f :: * -> *) (r :: * -> * -> *) a b.
(Functor f r (->), Object r a, Object r b) =>
r a b -> f a -> f b
<$> Q Cxt
cxt Q (Type -> [Dec] -> Dec) -> Q Type -> Q ([Dec] -> Dec)
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|] Q ([Dec] -> Dec) -> DecsQ -> Q Dec
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 Maybe Overlap
forall a. Maybe a
Nothing (Cxt -> Type -> [Dec] -> Dec) -> Q Cxt -> Q (Type -> [Dec] -> Dec)
forall (f :: * -> *) (r :: * -> * -> *) a b.
(Functor f r (->), Object r a, Object r b) =>
r a b -> f a -> f b
<$> Q Cxt
cxt Q (Type -> [Dec] -> Dec) -> Q Type -> Q ([Dec] -> Dec)
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|] Q ([Dec] -> Dec) -> DecsQ -> Q Dec
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) = \_ Coercion
           -> error "Cannot yet coerce tensors defined from a `HasBasis` instance. This would require `RoleAnnotations` on `:->:`. Cf. https://gitlab.haskell.org/ghc/ghc/-/issues/8177"
       |]
  , Maybe Overlap -> Cxt -> Type -> [Dec] -> Dec
InstanceD Maybe Overlap
forall a. Maybe a
Nothing (Cxt -> Type -> [Dec] -> Dec) -> Q Cxt -> Q (Type -> [Dec] -> Dec)
forall (f :: * -> *) (r :: * -> * -> *) a b.
(Functor f r (->), Object r a, Object r b) =>
r a b -> f a -> f b
<$> Q Cxt
cxt Q (Type -> [Dec] -> Dec) -> Q Type -> Q ([Dec] -> Dec)
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|] Q ([Dec] -> Dec) -> DecsQ -> Q Dec
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 Maybe Overlap
forall a. Maybe a
Nothing (Cxt -> Type -> [Dec] -> Dec) -> Q Cxt -> Q (Type -> [Dec] -> Dec)
forall (f :: * -> *) (r :: * -> * -> *) a b.
(Functor f r (->), Object r a, Object r b) =>
r a b -> f a -> f b
<$> Q Cxt
cxt Q (Type -> [Dec] -> Dec) -> Q Type -> Q ([Dec] -> Dec)
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|] Q ([Dec] -> Dec) -> DecsQ -> Q Dec
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 -> DecsQ
makeFiniteDimensionalFromBasis Q Type
v
   = FiniteDimensionalFromBasisDerivationConfig
-> Q (Cxt, Type) -> DecsQ
makeFiniteDimensionalFromBasis' FiniteDimensionalFromBasisDerivationConfig
forall a. Default a => a
def (Q (Cxt, Type) -> DecsQ) -> Q (Cxt, Type) -> DecsQ
forall (f :: * -> * -> *) a b.
(Function f, Object f a, Object f b) =>
f a b -> a -> b
$ Q Type -> Q (Cxt, Type)
deQuantifyType Q Type
v

makeFiniteDimensionalFromBasis' :: FiniteDimensionalFromBasisDerivationConfig
              -> Q (Cxt, Type) -> DecsQ
makeFiniteDimensionalFromBasis' :: FiniteDimensionalFromBasisDerivationConfig
-> Q (Cxt, Type) -> DecsQ
makeFiniteDimensionalFromBasis' FiniteDimensionalFromBasisDerivationConfig
_ Q (Cxt, Type)
cxtv = do
 [Dec]
generalInsts <- LinearSpaceFromBasisDerivationConfig -> Q (Cxt, Type) -> DecsQ
makeLinearSpaceFromBasis' LinearSpaceFromBasisDerivationConfig
forall a. Default a => a
def Q (Cxt, Type)
cxtv
 (Q Cxt
cxt,Q Type
v) <- do
   (Cxt
cxt', Type
v') <- Q (Cxt, Type)
cxtv
   (Q Cxt, Q Type) -> Q (Q Cxt, Q Type)
forall (m :: * -> *) a. Monad m (->) => a -> m a
return (Cxt -> Q Cxt
forall (f :: * -> *) (r :: * -> * -> *) (t :: * -> * -> *) a.
(Applicative f r t, Object r a, Object t (f a)) =>
t a (f a)
pure Cxt
cxt', Type -> Q Type
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 <- Int -> Int
forall a. Num a => a -> a
abs (Int -> Int) -> (Type -> Int) -> Type -> Int
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
. String -> Int
forall a. Hashable a => a -> Int
hash (String -> Int) -> (Type -> String) -> Type -> Int
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
. Type -> String
forall a. Show a => a -> String
show (Type -> Int) -> Q Type -> Q Int
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 <- [Q Dec] -> DecsQ
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 Maybe Overlap
forall a. Maybe a
Nothing (Cxt -> Type -> [Dec] -> Dec) -> Q Cxt -> Q (Type -> [Dec] -> Dec)
forall (f :: * -> *) (r :: * -> * -> *) a b.
(Functor f r (->), Object r a, Object r b) =>
r a b -> f a -> f b
<$> Q Cxt
cxt Q (Type -> [Dec] -> Dec) -> Q Type -> Q ([Dec] -> Dec)
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|] Q ([Dec] -> Dec) -> DecsQ -> Q Dec
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 <- String -> Q Name
newName (String -> Q Name) -> String -> Q Name
forall (f :: * -> * -> *) a b.
(Function f, Object f a, Object f b) =>
f a b -> a -> b
$ String
"CompleteBasis"String -> String -> String
forall a. [a] -> [a] -> [a]
++Int -> String
forall a. Show a => a -> String
show Int
vtnameHash

    [Dec]
tySyns <- [Q Dec] -> DecsQ
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 [] Maybe [TyVarBndr]
forall a. Maybe a
Nothing
          (Type -> Maybe Type -> [Con] -> [DerivClause] -> Dec)
-> Q Type -> Q (Maybe Type -> [Con] -> [DerivClause] -> Dec)
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) (Type -> Type) -> Q Type -> Q Type
forall (f :: * -> *) (r :: * -> * -> *) a b.
(Functor f r (->), Object r a, Object r b) =>
r a b -> f a -> f b
<$> Q Type
v)
          Q (Maybe Type -> [Con] -> [DerivClause] -> Dec)
-> Q (Maybe Type) -> Q ([Con] -> [DerivClause] -> Dec)
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))
<*> Maybe Type -> Q (Maybe Type)
forall (f :: * -> *) (r :: * -> * -> *) (t :: * -> * -> *) a.
(Applicative f r t, Object r a, Object t (f a)) =>
t a (f a)
pure Maybe Type
forall a. Maybe a
Nothing
          Q ([Con] -> [DerivClause] -> Dec)
-> Q [Con] -> Q ([DerivClause] -> Dec)
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))
<*> [Con] -> Q [Con]
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 []]
          Q ([DerivClause] -> Dec) -> Q [DerivClause] -> Q Dec
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))
<*> [DerivClause] -> Q [DerivClause]
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

      |]
    [Dec] -> DecsQ
forall (m :: * -> *) a. Monad m (->) => a -> m a
return ([Dec] -> DecsQ) -> [Dec] -> DecsQ
forall (f :: * -> * -> *) a b.
(Function f, Object f a, Object f b) =>
f a b -> a -> b
$ [Dec]
tySyns [Dec] -> [Dec] -> [Dec]
forall a. [a] -> [a] -> [a]
++ [Dec]
methods
  , Maybe Overlap -> Cxt -> Type -> [Dec] -> Dec
InstanceD Maybe Overlap
forall a. Maybe a
Nothing (Cxt -> Type -> [Dec] -> Dec) -> Q Cxt -> Q (Type -> [Dec] -> Dec)
forall (f :: * -> *) (r :: * -> * -> *) a b.
(Functor f r (->), Object r a, Object r b) =>
r a b -> f a -> f b
<$> Q Cxt
cxt Q (Type -> [Dec] -> Dec) -> Q Type -> Q ([Dec] -> Dec)
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|] Q ([Dec] -> Dec) -> DecsQ -> Q Dec
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 ()) )
      |]
  ]
 [Dec] -> DecsQ
forall (m :: * -> *) a. Monad m (->) => a -> m a
return ([Dec] -> DecsQ) -> [Dec] -> DecsQ
forall (f :: * -> * -> *) a b.
(Function f, Object f a, Object f b) =>
f a b -> a -> b
$ [Dec]
generalInsts [Dec] -> [Dec] -> [Dec]
forall a. [a] -> [a] -> [a]
++ [Dec]
fdInsts


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


newtype DualVectorFromBasis v = DualVectorFromBasis { DualVectorFromBasis v -> v
getDualVectorFromBasis :: v }
  deriving newtype (DualVectorFromBasis v -> DualVectorFromBasis v -> Bool
(DualVectorFromBasis v -> DualVectorFromBasis v -> Bool)
-> (DualVectorFromBasis v -> DualVectorFromBasis v -> Bool)
-> Eq (DualVectorFromBasis v)
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
DualVectorFromBasis v
-> (DualVectorFromBasis v
    -> DualVectorFromBasis v -> DualVectorFromBasis v)
-> (DualVectorFromBasis v -> DualVectorFromBasis v)
-> (DualVectorFromBasis v
    -> DualVectorFromBasis v -> DualVectorFromBasis v)
-> AdditiveGroup (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, AdditiveGroup (DualVectorFromBasis v)
AdditiveGroup (DualVectorFromBasis v)
-> (Scalar (DualVectorFromBasis v)
    -> DualVectorFromBasis v -> DualVectorFromBasis v)
-> VectorSpace (DualVectorFromBasis v)
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
$cp1VectorSpace :: forall v. VectorSpace v => AdditiveGroup (DualVectorFromBasis v)
VectorSpace, VectorSpace (DualVectorFromBasis v)
VectorSpace (DualVectorFromBasis v)
-> (Basis (DualVectorFromBasis v) -> DualVectorFromBasis v)
-> (DualVectorFromBasis v
    -> [(Basis (DualVectorFromBasis v),
         Scalar (DualVectorFromBasis v))])
-> (DualVectorFromBasis v
    -> Basis (DualVectorFromBasis v) -> Scalar (DualVectorFromBasis v))
-> HasBasis (DualVectorFromBasis v)
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
$cp1HasBasis :: forall v. HasBasis v => VectorSpace (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
(.+~^) = 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
(.+^) = DualVectorFromBasis v
-> Diff (DualVectorFromBasis v) -> DualVectorFromBasis v
forall v. AdditiveGroup v => v -> v -> v
(^+^)
  .-. :: DualVectorFromBasis v
-> DualVectorFromBasis v -> Diff (DualVectorFromBasis v)
(.-.) = DualVectorFromBasis v
-> DualVectorFromBasis v -> Diff (DualVectorFromBasis v)
forall v. AdditiveGroup v => v -> v -> v
(^-^)

instance AdditiveGroup v => PseudoAffine (DualVectorFromBasis v) where
  .-~! :: DualVectorFromBasis v
-> DualVectorFromBasis v -> Needle (DualVectorFromBasis v)
(.-~!) = 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 = DualVectorFromBasis v -> Maybe (DualVectorFromBasis v)
forall (f :: * -> *) (r :: * -> * -> *) (t :: * -> * -> *) a.
(Applicative f r t, Object r a, Object t (f a)) =>
t a (f a)
pure (DualVectorFromBasis v
pDualVectorFromBasis v
-> DualVectorFromBasis v -> DualVectorFromBasis v
forall 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
vDualVectorFromBasis v -> DualVectorFromBasis v -> Bool
forall a. Eq a => a -> a -> Bool
==DualVectorFromBasis v
v       = DualVectorFromBasis v -> Maybe (DualVectorFromBasis v)
forall a. a -> Maybe a
Just DualVectorFromBasis v
v
   | Bool
otherwise  = Maybe (DualVectorFromBasis v)
forall a. Maybe a
Nothing
  wellDefinedTensor :: (DualVectorFromBasis v ⊗ w) -> Maybe (DualVectorFromBasis v ⊗ w)
wellDefinedTensor (Tensor TensorProduct (DualVectorFromBasis v) w
v)
     = ([w] -> Tensor (Scalar v) (DualVectorFromBasis v) w)
-> Maybe [w] -> Maybe (Tensor (Scalar v) (DualVectorFromBasis v) w)
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 (Tensor (Scalar v) (DualVectorFromBasis v) w
-> [w] -> Tensor (Scalar v) (DualVectorFromBasis v) w
forall (a :: * -> * -> *) b x.
(WellPointed a, Object a b, ObjectPoint a x) =>
x -> a b x
const (Tensor (Scalar v) (DualVectorFromBasis v) w
 -> [w] -> Tensor (Scalar v) (DualVectorFromBasis v) w)
-> Tensor (Scalar v) (DualVectorFromBasis v) w
-> [w]
-> Tensor (Scalar v) (DualVectorFromBasis v) w
forall (f :: * -> * -> *) a b.
(Function f, Object f a, Object f b) =>
f a b -> a -> b
$ TensorProduct (DualVectorFromBasis v) w
-> Tensor (Scalar v) (DualVectorFromBasis v) w
forall s v w. TensorProduct v w -> Tensor s v w
Tensor TensorProduct (DualVectorFromBasis v) w
v) (Maybe [w] -> Maybe (Tensor (Scalar v) (DualVectorFromBasis v) w))
-> ([(Basis v, w)] -> Maybe [w])
-> [(Basis v, w)]
-> Maybe (Tensor (Scalar v) (DualVectorFromBasis 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
. ((Basis v, w) -> Maybe w) -> [(Basis v, w)] -> Maybe [w]
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse (w -> Maybe w
forall v. TensorSpace v => v -> Maybe v
wellDefinedVector (w -> Maybe w) -> ((Basis v, w) -> w) -> (Basis v, w) -> Maybe 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
. (Basis v, w) -> w
forall (a :: * -> * -> *) x y.
(PreArrow a, ObjectPair a x y) =>
a (x, y) y
snd) ([(Basis v, w)]
 -> Maybe (Tensor (Scalar v) (DualVectorFromBasis v) w))
-> [(Basis v, w)]
-> Maybe (Tensor (Scalar v) (DualVectorFromBasis v) w)
forall (f :: * -> * -> *) a b.
(Function f, Object f a, Object f b) =>
f a b -> a -> b
$ (Basis v :->: w) -> [(Basis v, w)]
forall a b. HasTrie a => (a :->: b) -> [(a, b)]
enumerate Basis v :->: w
TensorProduct (DualVectorFromBasis v) w
v
  zeroTensor :: DualVectorFromBasis v ⊗ w
zeroTensor = (Basis v :->: w) -> Tensor (Scalar v) (DualVectorFromBasis v) w
forall s v w. TensorProduct v w -> Tensor s v w
Tensor ((Basis v :->: w) -> Tensor (Scalar v) (DualVectorFromBasis v) w)
-> ((Basis v -> w) -> Basis v :->: w)
-> (Basis v -> w)
-> Tensor (Scalar v) (DualVectorFromBasis 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
. (Basis v -> w) -> Basis v :->: w
forall a b. HasTrie a => (a -> b) -> a :->: b
trie ((Basis v -> w) -> Tensor (Scalar v) (DualVectorFromBasis v) w)
-> (Basis v -> w) -> Tensor (Scalar v) (DualVectorFromBasis v) w
forall (f :: * -> * -> *) a b.
(Function f, Object f a, Object f b) =>
f a b -> a -> b
$ w -> Basis v -> w
forall (a :: * -> * -> *) b x.
(WellPointed a, Object a b, ObjectPoint a x) =>
x -> a b x
const w
forall v. AdditiveGroup v => v
zeroV
  toFlatTensor :: DualVectorFromBasis v
-+> (DualVectorFromBasis v ⊗ Scalar (DualVectorFromBasis v))
toFlatTensor = (DualVectorFromBasis v
 -> Tensor (Scalar v) (DualVectorFromBasis v) (Scalar v))
-> LinearFunction
     (Scalar v)
     (DualVectorFromBasis v)
     (Tensor (Scalar v) (DualVectorFromBasis v) (Scalar v))
forall s v w. (v -> w) -> LinearFunction s v w
LinearFunction ((DualVectorFromBasis v
  -> Tensor (Scalar v) (DualVectorFromBasis v) (Scalar v))
 -> LinearFunction
      (Scalar v)
      (DualVectorFromBasis v)
      (Tensor (Scalar v) (DualVectorFromBasis v) (Scalar v)))
-> (DualVectorFromBasis v
    -> Tensor (Scalar v) (DualVectorFromBasis v) (Scalar v))
-> LinearFunction
     (Scalar v)
     (DualVectorFromBasis v)
     (Tensor (Scalar v) (DualVectorFromBasis v) (Scalar v))
forall (f :: * -> * -> *) a b.
(Function f, Object f a, Object f b) =>
f a b -> a -> b
$ (Basis v :->: Scalar v)
-> Tensor (Scalar v) (DualVectorFromBasis v) (Scalar v)
forall s v w. TensorProduct v w -> Tensor s v w
Tensor ((Basis v :->: Scalar v)
 -> Tensor (Scalar v) (DualVectorFromBasis v) (Scalar v))
-> (DualVectorFromBasis v -> Basis v :->: Scalar v)
-> DualVectorFromBasis v
-> Tensor (Scalar v) (DualVectorFromBasis v) (Scalar 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
. (Basis v -> Scalar v) -> Basis v :->: Scalar v
forall a b. HasTrie a => (a -> b) -> a :->: b
trie ((Basis v -> Scalar v) -> Basis v :->: Scalar v)
-> (DualVectorFromBasis v -> Basis v -> Scalar v)
-> DualVectorFromBasis v
-> Basis v :->: Scalar 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
. DualVectorFromBasis v -> Basis v -> Scalar v
forall v. HasBasis v => v -> Basis v -> Scalar v
decompose'
  fromFlatTensor :: (DualVectorFromBasis v ⊗ Scalar (DualVectorFromBasis v))
-+> DualVectorFromBasis v
fromFlatTensor = (Tensor (Scalar v) (DualVectorFromBasis v) (Scalar v)
 -> DualVectorFromBasis v)
-> LinearFunction
     (Scalar v)
     (Tensor (Scalar v) (DualVectorFromBasis v) (Scalar v))
     (DualVectorFromBasis v)
forall s v w. (v -> w) -> LinearFunction s v w
LinearFunction ((Tensor (Scalar v) (DualVectorFromBasis v) (Scalar v)
  -> DualVectorFromBasis v)
 -> LinearFunction
      (Scalar v)
      (Tensor (Scalar v) (DualVectorFromBasis v) (Scalar v))
      (DualVectorFromBasis v))
-> (Tensor (Scalar v) (DualVectorFromBasis v) (Scalar v)
    -> DualVectorFromBasis v)
-> LinearFunction
     (Scalar v)
     (Tensor (Scalar v) (DualVectorFromBasis v) (Scalar v))
     (DualVectorFromBasis v)
forall (f :: * -> * -> *) a b.
(Function f, Object f a, Object f b) =>
f a b -> a -> b
$ \(Tensor TensorProduct (DualVectorFromBasis v) (Scalar v)
t)
          -> [(Basis v, Scalar v)] -> DualVectorFromBasis v
forall v. HasBasis v => [(Basis v, Scalar v)] -> v
recompose ([(Basis v, Scalar v)] -> DualVectorFromBasis v)
-> [(Basis v, Scalar v)] -> DualVectorFromBasis v
forall (f :: * -> * -> *) a b.
(Function f, Object f a, Object f b) =>
f a b -> a -> b
$ (Basis v :->: Scalar v) -> [(Basis v, Scalar v)]
forall a b. HasTrie a => (a :->: b) -> [(a, b)]
enumerate Basis v :->: Scalar v
TensorProduct (DualVectorFromBasis v) (Scalar v)
t
  scalarSpaceWitness :: ScalarSpaceWitness (DualVectorFromBasis v)
scalarSpaceWitness = ScalarSpaceWitness (DualVectorFromBasis v)
forall v.
(Num' (Scalar v), Scalar (Scalar v) ~ Scalar v) =>
ScalarSpaceWitness v
ScalarSpaceWitness
  linearManifoldWitness :: LinearManifoldWitness (DualVectorFromBasis v)
linearManifoldWitness = LinearManifoldWitness (DualVectorFromBasis v)
forall v.
(Needle v ~ v, AffineSpace v, Diff v ~ v) =>
LinearManifoldWitness v
LinearManifoldWitness
#if !MIN_VERSION_manifolds_core(0,6,0)
        BoundarylessWitness
#endif
  addTensors :: (DualVectorFromBasis v ⊗ w)
-> (DualVectorFromBasis v ⊗ w) -> DualVectorFromBasis v ⊗ w
addTensors (Tensor TensorProduct (DualVectorFromBasis v) w
v) (Tensor TensorProduct (DualVectorFromBasis v) w
w) = (Basis v :->: w) -> Tensor (Scalar v) (DualVectorFromBasis v) w
forall s v w. TensorProduct v w -> Tensor s v w
Tensor ((Basis v :->: w) -> Tensor (Scalar v) (DualVectorFromBasis v) w)
-> (Basis v :->: w) -> Tensor (Scalar v) (DualVectorFromBasis v) w
forall (f :: * -> * -> *) a b.
(Function f, Object f a, Object f b) =>
f a b -> a -> b
$ w -> w -> w
forall v. AdditiveGroup v => v -> v -> v
(^+^) (w -> w -> w) -> (Basis v :->: w) -> Basis v :->: (w -> w)
forall (f :: * -> *) (r :: * -> * -> *) a b.
(Functor f r (->), Object r a, Object r b) =>
r a b -> f a -> f b
<$> Basis v :->: w
TensorProduct (DualVectorFromBasis v) w
v (Basis v :->: (w -> w)) -> (Basis v :->: w) -> Basis v :->: w
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))
<*> Basis v :->: w
TensorProduct (DualVectorFromBasis v) w
w
  subtractTensors :: (DualVectorFromBasis v ⊗ w)
-> (DualVectorFromBasis v ⊗ w) -> DualVectorFromBasis v ⊗ w
subtractTensors (Tensor TensorProduct (DualVectorFromBasis v) w
v) (Tensor TensorProduct (DualVectorFromBasis v) w
w) = (Basis v :->: w) -> Tensor (Scalar v) (DualVectorFromBasis v) w
forall s v w. TensorProduct v w -> Tensor s v w
Tensor ((Basis v :->: w) -> Tensor (Scalar v) (DualVectorFromBasis v) w)
-> (Basis v :->: w) -> Tensor (Scalar v) (DualVectorFromBasis v) w
forall (f :: * -> * -> *) a b.
(Function f, Object f a, Object f b) =>
f a b -> a -> b
$ w -> w -> w
forall v. AdditiveGroup v => v -> v -> v
(^-^) (w -> w -> w) -> (Basis v :->: w) -> Basis v :->: (w -> w)
forall (f :: * -> *) (r :: * -> * -> *) a b.
(Functor f r (->), Object r a, Object r b) =>
r a b -> f a -> f b
<$> Basis v :->: w
TensorProduct (DualVectorFromBasis v) w
v (Basis v :->: (w -> w)) -> (Basis v :->: w) -> Basis v :->: w
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))
<*> Basis v :->: w
TensorProduct (DualVectorFromBasis v) w
w
  tensorProduct :: Bilinear (DualVectorFromBasis v) w (DualVectorFromBasis v ⊗ w)
tensorProduct = (DualVectorFromBasis v
 -> w -> Tensor (Scalar v) (DualVectorFromBasis v) w)
-> LinearFunction
     (Scalar v)
     (DualVectorFromBasis v)
     (LinearFunction
        (Scalar v) w (Tensor (Scalar v) (DualVectorFromBasis v) w))
forall v w y. (v -> w -> y) -> Bilinear v w y
bilinearFunction
    ((DualVectorFromBasis v
  -> w -> Tensor (Scalar v) (DualVectorFromBasis v) w)
 -> LinearFunction
      (Scalar v)
      (DualVectorFromBasis v)
      (LinearFunction
         (Scalar v) w (Tensor (Scalar v) (DualVectorFromBasis v) w)))
-> (DualVectorFromBasis v
    -> w -> Tensor (Scalar v) (DualVectorFromBasis v) w)
-> LinearFunction
     (Scalar v)
     (DualVectorFromBasis v)
     (LinearFunction
        (Scalar v) w (Tensor (Scalar v) (DualVectorFromBasis v) w))
forall (f :: * -> * -> *) a b.
(Function f, Object f a, Object f b) =>
f a b -> a -> b
$ \DualVectorFromBasis v
v w
w -> (Basis v :->: w) -> Tensor (Scalar v) (DualVectorFromBasis v) w
forall s v w. TensorProduct v w -> Tensor s v w
Tensor ((Basis v :->: w) -> Tensor (Scalar v) (DualVectorFromBasis v) w)
-> ((Basis v -> w) -> Basis v :->: w)
-> (Basis v -> w)
-> Tensor (Scalar v) (DualVectorFromBasis 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
. (Basis v -> w) -> Basis v :->: w
forall a b. HasTrie a => (a -> b) -> a :->: b
trie ((Basis v -> w) -> Tensor (Scalar v) (DualVectorFromBasis v) w)
-> (Basis v -> w) -> Tensor (Scalar v) (DualVectorFromBasis v) w
forall (f :: * -> * -> *) a b.
(Function f, Object f a, Object f b) =>
f a b -> a -> b
$ \Basis v
bv -> DualVectorFromBasis v
-> Basis (DualVectorFromBasis v) -> Scalar (DualVectorFromBasis v)
forall v. HasBasis v => v -> Basis v -> Scalar v
decompose' DualVectorFromBasis v
v Basis v
Basis (DualVectorFromBasis v)
bv Scalar w -> w -> w
forall v. VectorSpace v => Scalar v -> v -> v
*^ w
w
  transposeTensor :: (DualVectorFromBasis v ⊗ w) -+> (w ⊗ DualVectorFromBasis v)
transposeTensor = (Tensor (Scalar v) (DualVectorFromBasis v) w
 -> w ⊗ DualVectorFromBasis v)
-> LinearFunction
     (Scalar v)
     (Tensor (Scalar v) (DualVectorFromBasis v) w)
     (w ⊗ DualVectorFromBasis v)
forall s v w. (v -> w) -> LinearFunction s v w
LinearFunction ((Tensor (Scalar v) (DualVectorFromBasis v) w
  -> w ⊗ DualVectorFromBasis v)
 -> LinearFunction
      (Scalar v)
      (Tensor (Scalar v) (DualVectorFromBasis v) w)
      (w ⊗ DualVectorFromBasis v))
-> (Tensor (Scalar v) (DualVectorFromBasis v) w
    -> w ⊗ DualVectorFromBasis v)
-> LinearFunction
     (Scalar v)
     (Tensor (Scalar v) (DualVectorFromBasis v) w)
     (w ⊗ DualVectorFromBasis v)
forall (f :: * -> * -> *) a b.
(Function f, Object f a, Object f b) =>
f a b -> a -> b
$ \(Tensor TensorProduct (DualVectorFromBasis v) w
t)
       -> [w ⊗ DualVectorFromBasis v] -> w ⊗ DualVectorFromBasis v
forall (f :: * -> *) v. (Foldable f, AdditiveGroup v) => f v -> v
sumV [ (LinearFunction
  (Scalar v)
  w
  (LinearFunction
     (Scalar v) (DualVectorFromBasis v) (w ⊗ DualVectorFromBasis v))
forall v w.
(TensorSpace v, TensorSpace w, Scalar w ~ Scalar v) =>
Bilinear v w (v ⊗ w)
tensorProductLinearFunction
  (Scalar v)
  w
  (LinearFunction
     (Scalar v) (DualVectorFromBasis v) (w ⊗ DualVectorFromBasis v))
-> w
-> LinearFunction
     (Scalar v) (DualVectorFromBasis v) (w ⊗ DualVectorFromBasis v)
forall s v w. LinearFunction s v w -> v -> w
-+$>w
w)LinearFunction
  (Scalar v) (DualVectorFromBasis v) (w ⊗ DualVectorFromBasis v)
-> DualVectorFromBasis v -> w ⊗ DualVectorFromBasis v
forall s v w. LinearFunction s v w -> v -> w
-+$>Basis (DualVectorFromBasis v) -> DualVectorFromBasis v
forall v. HasBasis v => Basis v -> v
basisValue Basis v
Basis (DualVectorFromBasis v)
b
               | (Basis v
b,w
w) <- (Basis v :->: w) -> [(Basis v, w)]
forall a b. HasTrie a => (a :->: b) -> [(a, b)]
enumerate Basis v :->: w
TensorProduct (DualVectorFromBasis v) w
t ]
  fmapTensor :: Bilinear
  (w -+> x) (DualVectorFromBasis v ⊗ w) (DualVectorFromBasis v ⊗ x)
fmapTensor = (LinearFunction (Scalar v) w x
 -> Tensor (Scalar v) (DualVectorFromBasis v) w
 -> Tensor (Scalar v) (DualVectorFromBasis v) x)
-> LinearFunction
     (Scalar x)
     (LinearFunction (Scalar v) w x)
     (LinearFunction
        (Scalar x)
        (Tensor (Scalar v) (DualVectorFromBasis v) w)
        (Tensor (Scalar v) (DualVectorFromBasis v) x))
forall v w y. (v -> w -> y) -> Bilinear v w y
bilinearFunction
    ((LinearFunction (Scalar v) w x
  -> Tensor (Scalar v) (DualVectorFromBasis v) w
  -> Tensor (Scalar v) (DualVectorFromBasis v) x)
 -> LinearFunction
      (Scalar x)
      (LinearFunction (Scalar v) w x)
      (LinearFunction
         (Scalar x)
         (Tensor (Scalar v) (DualVectorFromBasis v) w)
         (Tensor (Scalar v) (DualVectorFromBasis v) x)))
-> (LinearFunction (Scalar v) w x
    -> Tensor (Scalar v) (DualVectorFromBasis v) w
    -> Tensor (Scalar v) (DualVectorFromBasis v) x)
-> LinearFunction
     (Scalar x)
     (LinearFunction (Scalar v) w x)
     (LinearFunction
        (Scalar x)
        (Tensor (Scalar v) (DualVectorFromBasis v) w)
        (Tensor (Scalar v) (DualVectorFromBasis v) x))
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)
         -> (Basis v :->: x) -> Tensor (Scalar v) (DualVectorFromBasis v) x
forall s v w. TensorProduct v w -> Tensor s v w
Tensor ((Basis v :->: x) -> Tensor (Scalar v) (DualVectorFromBasis v) x)
-> (Basis v :->: x) -> Tensor (Scalar v) (DualVectorFromBasis v) x
forall (f :: * -> * -> *) a b.
(Function f, Object f a, Object f b) =>
f a b -> a -> b
$ (w -> x) -> (Basis v :->: w) -> Basis v :->: x
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 Basis v :->: w
TensorProduct (DualVectorFromBasis v) w
t
  fzipTensorWith :: Bilinear
  ((w, x) -+> u)
  (DualVectorFromBasis v ⊗ w, DualVectorFromBasis v ⊗ x)
  (DualVectorFromBasis v ⊗ u)
fzipTensorWith = (LinearFunction (Scalar v) (w, x) u
 -> (Tensor (Scalar v) (DualVectorFromBasis v) w,
     Tensor (Scalar v) (DualVectorFromBasis v) x)
 -> Tensor (Scalar v) (DualVectorFromBasis v) u)
-> LinearFunction
     (Scalar u)
     (LinearFunction (Scalar v) (w, x) u)
     (LinearFunction
        (Scalar u)
        (Tensor (Scalar v) (DualVectorFromBasis v) w,
         Tensor (Scalar v) (DualVectorFromBasis v) x)
        (Tensor (Scalar v) (DualVectorFromBasis v) u))
forall v w y. (v -> w -> y) -> Bilinear v w y
bilinearFunction
    ((LinearFunction (Scalar v) (w, x) u
  -> (Tensor (Scalar v) (DualVectorFromBasis v) w,
      Tensor (Scalar v) (DualVectorFromBasis v) x)
  -> Tensor (Scalar v) (DualVectorFromBasis v) u)
 -> LinearFunction
      (Scalar u)
      (LinearFunction (Scalar v) (w, x) u)
      (LinearFunction
         (Scalar u)
         (Tensor (Scalar v) (DualVectorFromBasis v) w,
          Tensor (Scalar v) (DualVectorFromBasis v) x)
         (Tensor (Scalar v) (DualVectorFromBasis v) u)))
-> (LinearFunction (Scalar v) (w, x) u
    -> (Tensor (Scalar v) (DualVectorFromBasis v) w,
        Tensor (Scalar v) (DualVectorFromBasis v) x)
    -> Tensor (Scalar v) (DualVectorFromBasis v) u)
-> LinearFunction
     (Scalar u)
     (LinearFunction (Scalar v) (w, x) u)
     (LinearFunction
        (Scalar u)
        (Tensor (Scalar v) (DualVectorFromBasis v) w,
         Tensor (Scalar v) (DualVectorFromBasis v) x)
        (Tensor (Scalar v) (DualVectorFromBasis v) u))
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)
         -> (Basis v :->: u) -> Tensor (Scalar v) (DualVectorFromBasis v) u
forall s v w. TensorProduct v w -> Tensor s v w
Tensor ((Basis v :->: u) -> Tensor (Scalar v) (DualVectorFromBasis v) u)
-> (Basis v :->: u) -> Tensor (Scalar v) (DualVectorFromBasis v) u
forall (f :: * -> * -> *) a b.
(Function f, Object f a, Object f b) =>
f a b -> a -> b
$ (w -> x -> u)
-> (Basis v :->: w) -> (Basis v :->: x) -> Basis v :->: u
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 (((w, x) -> u) -> w -> x -> u
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) Basis v :->: w
TensorProduct (DualVectorFromBasis v) w
tv Basis v :->: x
TensorProduct (DualVectorFromBasis v) x
tw
  coerceFmapTensorProduct :: p (DualVectorFromBasis v)
-> Coercion a b
-> Coercion
     (TensorProduct (DualVectorFromBasis v) a)
     (TensorProduct (DualVectorFromBasis v) b)
coerceFmapTensorProduct p (DualVectorFromBasis v)
_ Coercion a b
Coercion
    = String -> Coercion (Basis v :->: a) (Basis v :->: b)
forall a. HasCallStack => String -> a
error String
"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 Num' (Scalar v) => ClosedScalarWitness (Scalar v)
forall s. Num' s => ClosedScalarWitness s
closedScalarWitness @(Scalar v) of
    ClosedScalarWitness (Scalar v)
ClosedScalarWitness -> DualSpaceWitness (DualVectorFromBasis v)
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 = ((TensorProduct v (DualVectorFromBasis v)
  ~ (Basis v :->: DualVectorFromBasis v)) =>
 LinearMap
   (Scalar v) (DualVectorFromBasis v) (DualVectorFromBasis v))
-> LinearMap
     (Scalar v) (DualVectorFromBasis v) (DualVectorFromBasis v)
forall v w φ.
BasisGeneratedSpace v =>
((TensorProduct v w ~ (Basis v :->: w)) => φ) -> φ
proveTensorProductIsTrie @v @(DualVectorFromBasis v)
     ((Basis v :->: DualVectorFromBasis v)
-> LinearMap
     (Scalar v) (DualVectorFromBasis v) (DualVectorFromBasis v)
forall s v w. TensorProduct (DualVector v) w -> LinearMap s v w
LinearMap ((Basis v :->: DualVectorFromBasis v)
 -> LinearMap
      (Scalar v) (DualVectorFromBasis v) (DualVectorFromBasis v))
-> ((Basis v -> DualVectorFromBasis v)
    -> Basis v :->: DualVectorFromBasis v)
-> (Basis v -> DualVectorFromBasis v)
-> LinearMap
     (Scalar v) (DualVectorFromBasis v) (DualVectorFromBasis 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
. (Basis v -> DualVectorFromBasis v)
-> Basis v :->: DualVectorFromBasis v
forall a b. HasTrie a => (a -> b) -> a :->: b
trie ((Basis v -> DualVectorFromBasis v)
 -> LinearMap
      (Scalar v) (DualVectorFromBasis v) (DualVectorFromBasis v))
-> (Basis v -> DualVectorFromBasis v)
-> LinearMap
     (Scalar v) (DualVectorFromBasis v) (DualVectorFromBasis v)
forall (f :: * -> * -> *) a b.
(Function f, Object f a, Object f b) =>
f a b -> a -> b
$ v -> DualVectorFromBasis v
forall v. v -> DualVectorFromBasis v
DualVectorFromBasis (v -> DualVectorFromBasis v)
-> (Basis v -> v) -> Basis v -> DualVectorFromBasis 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
. Basis v -> v
forall v. HasBasis v => Basis v -> v
basisValue)
  tensorId :: (DualVectorFromBasis v ⊗ w) +> (DualVectorFromBasis v ⊗ w)
tensorId = (DualVectorFromBasis v ⊗ w) +> (DualVectorFromBasis v ⊗ w)
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 :: (DualVectorFromBasis v ⊗ w) +> (DualVectorFromBasis v ⊗ w)
tid = ((TensorProduct v (DualVector w ⊗ (DualVectorFromBasis v ⊗ w))
  ~ (Basis v :->: (DualVector w ⊗ (DualVectorFromBasis v ⊗ w)))) =>
 LinearMap
   (Scalar v)
   (Tensor (Scalar v) (DualVectorFromBasis v) w)
   (Tensor (Scalar v) (DualVectorFromBasis v) w))
-> LinearMap
     (Scalar v)
     (Tensor (Scalar v) (DualVectorFromBasis v) w)
     (Tensor (Scalar v) (DualVectorFromBasis v) w)
forall v w φ.
BasisGeneratedSpace v =>
((TensorProduct v w ~ (Basis v :->: w)) => φ) -> φ
proveTensorProductIsTrie @v @(DualVector w⊗(DualVectorFromBasis v⊗w))
                    ( case LinearSpace w => DualSpaceWitness w
forall v. LinearSpace v => DualSpaceWitness v
dualSpaceWitness @w of
          DualSpaceWitness w
DualSpaceWitness -> (Basis v
 :->: Tensor
        (Scalar v)
        (DualVector w)
        (Tensor (Scalar v) (DualVectorFromBasis v) w))
-> LinearMap
     (Scalar v)
     (Tensor (Scalar v) (DualVectorFromBasis v) w)
     (Tensor (Scalar v) (DualVectorFromBasis v) w)
forall s v w. TensorProduct (DualVector v) w -> LinearMap s v w
LinearMap ((Basis v
  :->: Tensor
         (Scalar v)
         (DualVector w)
         (Tensor (Scalar v) (DualVectorFromBasis v) w))
 -> LinearMap
      (Scalar v)
      (Tensor (Scalar v) (DualVectorFromBasis v) w)
      (Tensor (Scalar v) (DualVectorFromBasis v) w))
-> ((Basis v
     -> Tensor
          (Scalar v)
          (DualVector w)
          (Tensor (Scalar v) (DualVectorFromBasis v) w))
    -> Basis v
       :->: Tensor
              (Scalar v)
              (DualVector w)
              (Tensor (Scalar v) (DualVectorFromBasis v) w))
-> (Basis v
    -> Tensor
         (Scalar v)
         (DualVector w)
         (Tensor (Scalar v) (DualVectorFromBasis v) w))
-> LinearMap
     (Scalar v)
     (Tensor (Scalar v) (DualVectorFromBasis v) w)
     (Tensor (Scalar v) (DualVectorFromBasis 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
. (Basis v
 -> Tensor
      (Scalar v)
      (DualVector w)
      (Tensor (Scalar v) (DualVectorFromBasis v) w))
-> Basis v
   :->: Tensor
          (Scalar v)
          (DualVector w)
          (Tensor (Scalar v) (DualVectorFromBasis v) w)
forall a b. HasTrie a => (a -> b) -> a :->: b
trie ((Basis v
  -> Tensor
       (Scalar v)
       (DualVector w)
       (Tensor (Scalar v) (DualVectorFromBasis v) w))
 -> LinearMap
      (Scalar v)
      (Tensor (Scalar v) (DualVectorFromBasis v) w)
      (Tensor (Scalar v) (DualVectorFromBasis v) w))
-> (Basis v
    -> Tensor
         (Scalar v)
         (DualVector w)
         (Tensor (Scalar v) (DualVectorFromBasis v) w))
-> LinearMap
     (Scalar v)
     (Tensor (Scalar v) (DualVectorFromBasis v) w)
     (Tensor (Scalar v) (DualVectorFromBasis v) w)
forall (f :: * -> * -> *) a b.
(Function f, Object f a, Object f b) =>
f a b -> a -> b
$ TensorProduct
  (DualVector w) (Tensor (Scalar v) (DualVectorFromBasis v) w)
-> Tensor
     (Scalar v)
     (DualVector w)
     (Tensor (Scalar v) (DualVectorFromBasis v) w)
forall s v w. TensorProduct v w -> Tensor s v w
Tensor (TensorProduct
   (DualVector w) (Tensor (Scalar v) (DualVectorFromBasis v) w)
 -> Tensor
      (Scalar v)
      (DualVector w)
      (Tensor (Scalar v) (DualVectorFromBasis v) w))
-> (Basis v
    -> TensorProduct
         (DualVector w) (Tensor (Scalar v) (DualVectorFromBasis v) w))
-> Basis v
-> Tensor
     (Scalar v)
     (DualVector w)
     (Tensor (Scalar v) (DualVectorFromBasis 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
. \Basis v
i
           -> Tensor
  (Scalar v)
  (DualVector w)
  (Tensor (Scalar v) (DualVectorFromBasis v) w)
-> TensorProduct
     (DualVector w) (Tensor (Scalar v) (DualVectorFromBasis v) w)
forall s v w. Tensor s v w -> TensorProduct v w
getTensorProduct (Tensor
   (Scalar v)
   (DualVector w)
   (Tensor (Scalar v) (DualVectorFromBasis v) w)
 -> TensorProduct
      (DualVector w) (Tensor (Scalar v) (DualVectorFromBasis v) w))
-> Tensor
     (Scalar v)
     (DualVector w)
     (Tensor (Scalar v) (DualVectorFromBasis v) w)
-> TensorProduct
     (DualVector w) (Tensor (Scalar v) (DualVectorFromBasis v) w)
forall (f :: * -> * -> *) a b.
(Function f, Object f a, Object f b) =>
f a b -> a -> b
$
             (forall w x.
(TensorSpace (DualVector w), TensorSpace w, TensorSpace x,
 Scalar w ~ Scalar (DualVector w),
 Scalar x ~ Scalar (DualVector w)) =>
Bilinear (w -+> x) (DualVector w ⊗ w) (DualVector w ⊗ x)
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)
                 LinearFunction
  (Scalar v)
  (LinearFunction
     (Scalar v) w (Tensor (Scalar v) (DualVectorFromBasis v) w))
  (LinearFunction
     (Scalar v)
     (Tensor (Scalar v) (DualVector w) w)
     (Tensor
        (Scalar v)
        (DualVector w)
        (Tensor (Scalar v) (DualVectorFromBasis v) w)))
-> LinearFunction
     (Scalar v) w (Tensor (Scalar v) (DualVectorFromBasis v) w)
-> LinearFunction
     (Scalar v)
     (Tensor (Scalar v) (DualVector w) w)
     (Tensor
        (Scalar v)
        (DualVector w)
        (Tensor (Scalar v) (DualVectorFromBasis v) w))
forall s v w. LinearFunction s v w -> v -> w
-+$>((w -> Tensor (Scalar v) (DualVectorFromBasis v) w)
-> LinearFunction
     (Scalar v) w (Tensor (Scalar v) (DualVectorFromBasis v) w)
forall s v w. (v -> w) -> LinearFunction s v w
LinearFunction ((w -> Tensor (Scalar v) (DualVectorFromBasis v) w)
 -> LinearFunction
      (Scalar v) w (Tensor (Scalar v) (DualVectorFromBasis v) w))
-> (w -> Tensor (Scalar v) (DualVectorFromBasis v) w)
-> LinearFunction
     (Scalar v) w (Tensor (Scalar v) (DualVectorFromBasis v) w)
forall (f :: * -> * -> *) a b.
(Function f, Object f a, Object f b) =>
f a b -> a -> b
$ \w
w -> (Basis v :->: w) -> Tensor (Scalar v) (DualVectorFromBasis v) w
forall s v w. TensorProduct v w -> Tensor s v w
Tensor ((Basis v :->: w) -> Tensor (Scalar v) (DualVectorFromBasis v) w)
-> ((Basis v -> w) -> Basis v :->: w)
-> (Basis v -> w)
-> Tensor (Scalar v) (DualVectorFromBasis 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
. (Basis v -> w) -> Basis v :->: w
forall a b. HasTrie a => (a -> b) -> a :->: b
trie
                              ((Basis v -> w) -> Tensor (Scalar v) (DualVectorFromBasis v) w)
-> (Basis v -> w) -> Tensor (Scalar v) (DualVectorFromBasis v) w
forall (f :: * -> * -> *) a b.
(Function f, Object f a, Object f b) =>
f a b -> a -> b
$ (\Basis v
j -> if Basis v
iBasis v -> Basis v -> Bool
forall a. Eq a => a -> a -> Bool
==Basis v
j then w
w else w
forall v. AdditiveGroup v => v
zeroV)
                               :: DualVectorFromBasis v⊗w))
              LinearFunction
  (Scalar v)
  (Tensor (Scalar v) (DualVector w) w)
  (Tensor
     (Scalar v)
     (DualVector w)
     (Tensor (Scalar v) (DualVectorFromBasis v) w))
-> Tensor (Scalar v) (DualVector w) w
-> Tensor
     (Scalar v)
     (DualVector w)
     (Tensor (Scalar v) (DualVectorFromBasis v) w)
forall s v w. LinearFunction s v w -> v -> w
-+$> case LinearSpace w => w +> w
forall v. LinearSpace v => v +> v
linearId @w of
                    LinearMap TensorProduct (DualVector w) w
lw -> TensorProduct (DualVector w) w
-> Tensor (Scalar v) (DualVector w) w
forall s v w. TensorProduct v w -> Tensor s v w
Tensor TensorProduct (DualVector w) w
lw :: DualVector w⊗w )
  applyDualVector :: Bilinear
  (DualVector (DualVectorFromBasis v))
  (DualVectorFromBasis v)
  (Scalar (DualVectorFromBasis v))
applyDualVector = ((TensorProduct v (DualVectorFromBasis v)
  ~ (Basis v :->: DualVectorFromBasis v)) =>
 LinearFunction
   (Scalar v)
   v
   (LinearFunction (Scalar v) (DualVectorFromBasis v) (Scalar v)))
-> LinearFunction
     (Scalar v)
     v
     (LinearFunction (Scalar v) (DualVectorFromBasis v) (Scalar v))
forall v w φ.
BasisGeneratedSpace v =>
((TensorProduct v w ~ (Basis v :->: w)) => φ) -> φ
proveTensorProductIsTrie @v @(DualVectorFromBasis v)
     ( (v -> DualVectorFromBasis v -> Scalar v)
-> LinearFunction
     (Scalar v)
     v
     (LinearFunction (Scalar v) (DualVectorFromBasis v) (Scalar v))
forall v w y. (v -> w -> y) -> Bilinear v w y
bilinearFunction ((v -> DualVectorFromBasis v -> Scalar v)
 -> LinearFunction
      (Scalar v)
      v
      (LinearFunction (Scalar v) (DualVectorFromBasis v) (Scalar v)))
-> (v -> DualVectorFromBasis v -> Scalar v)
-> LinearFunction
     (Scalar v)
     v
     (LinearFunction (Scalar v) (DualVectorFromBasis v) (Scalar v))
forall (f :: * -> * -> *) a b.
(Function f, Object f a, Object f b) =>
f a b -> a -> b
$ \v
f (DualVectorFromBasis v
v)
          -> [Scalar v] -> Scalar v
forall (t :: * -> *) a. (Foldable t, Num a) => t a -> a
sum [v -> Basis v -> Scalar v
forall v. HasBasis v => v -> Basis v -> Scalar v
decompose' v
f Basis v
i Scalar v -> Scalar v -> Scalar v
forall a. Num a => a -> a -> a
* Scalar v
vi | (Basis v
i,Scalar v
vi) <- v -> [(Basis v, Scalar v)]
forall v. HasBasis v => v -> [(Basis v, Scalar v)]
decompose v
v] )
  applyLinear :: Bilinear (DualVectorFromBasis v +> w) (DualVectorFromBasis v) w
applyLinear = Bilinear (DualVectorFromBasis v +> w) (DualVectorFromBasis v) w
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 :: Bilinear (DualVectorFromBasis v +> w) (DualVectorFromBasis v) w
ali = ((TensorProduct v w ~ (Basis v :->: w)) =>
 LinearFunction
   (Scalar v)
   (LinearMap (Scalar v) (DualVectorFromBasis v) w)
   (LinearFunction (Scalar v) (DualVectorFromBasis v) w))
-> LinearFunction
     (Scalar v)
     (LinearMap (Scalar v) (DualVectorFromBasis v) w)
     (LinearFunction (Scalar v) (DualVectorFromBasis v) w)
forall v w φ.
BasisGeneratedSpace v =>
((TensorProduct v w ~ (Basis v :->: w)) => φ) -> φ
proveTensorProductIsTrie @v @w ( (LinearMap (Scalar v) (DualVectorFromBasis v) w
 -> DualVectorFromBasis v -> w)
-> LinearFunction
     (Scalar v)
     (LinearMap (Scalar v) (DualVectorFromBasis v) w)
     (LinearFunction (Scalar v) (DualVectorFromBasis v) w)
forall v w y. (v -> w -> y) -> Bilinear v w y
bilinearFunction
            ((LinearMap (Scalar v) (DualVectorFromBasis v) w
  -> DualVectorFromBasis v -> w)
 -> LinearFunction
      (Scalar v)
      (LinearMap (Scalar v) (DualVectorFromBasis v) w)
      (LinearFunction (Scalar v) (DualVectorFromBasis v) w))
-> (LinearMap (Scalar v) (DualVectorFromBasis v) w
    -> DualVectorFromBasis v -> w)
-> LinearFunction
     (Scalar v)
     (LinearMap (Scalar v) (DualVectorFromBasis v) w)
     (LinearFunction (Scalar v) (DualVectorFromBasis v) w)
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)
                -> [w] -> w
forall (f :: * -> *) v. (Foldable f, AdditiveGroup v) => f v -> v
sumV [Scalar v
Scalar w
vi Scalar w -> w -> w
forall v. VectorSpace v => Scalar v -> v -> v
*^ (Basis v :->: w) -> Basis v -> w
forall a b. HasTrie a => (a :->: b) -> a -> b
untrie Basis v :->: w
TensorProduct (DualVector (DualVectorFromBasis v)) w
f Basis v
i | (Basis v
i,Scalar v
vi) <- v -> [(Basis v, Scalar v)]
forall v. HasBasis v => v -> [(Basis v, Scalar v)]
decompose v
v] )
  applyTensorFunctional :: Bilinear
  (DualVector (DualVectorFromBasis v ⊗ u))
  (DualVectorFromBasis v ⊗ u)
  (Scalar (DualVectorFromBasis v))
applyTensorFunctional = Bilinear
  (DualVector (DualVectorFromBasis v ⊗ u))
  (DualVectorFromBasis v ⊗ u)
  (Scalar (DualVectorFromBasis v))
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 :: Bilinear
  (DualVector (DualVectorFromBasis v ⊗ u))
  (DualVectorFromBasis v ⊗ u)
  (Scalar v)
atf = ((TensorProduct v (DualVector u) ~ (Basis v :->: DualVector u)) =>
 LinearFunction
   (Scalar v)
   (LinearMap (Scalar v) (DualVectorFromBasis v) (DualVector u))
   (LinearFunction
      (Scalar v)
      (Tensor (Scalar v) (DualVectorFromBasis v) u)
      (Scalar v)))
-> LinearFunction
     (Scalar v)
     (LinearMap (Scalar v) (DualVectorFromBasis v) (DualVector u))
     (LinearFunction
        (Scalar v)
        (Tensor (Scalar v) (DualVectorFromBasis v) u)
        (Scalar v))
forall v w φ.
BasisGeneratedSpace v =>
((TensorProduct v w ~ (Basis v :->: w)) => φ) -> φ
proveTensorProductIsTrie @v @(DualVector u) (case LinearSpace u => DualSpaceWitness u
forall v. LinearSpace v => DualSpaceWitness v
dualSpaceWitness @u of
          DualSpaceWitness u
DualSpaceWitness -> (LinearMap (Scalar v) (DualVectorFromBasis v) (DualVector u)
 -> Tensor (Scalar v) (DualVectorFromBasis v) u -> Scalar v)
-> LinearFunction
     (Scalar v)
     (LinearMap (Scalar v) (DualVectorFromBasis v) (DualVector u))
     (LinearFunction
        (Scalar v)
        (Tensor (Scalar v) (DualVectorFromBasis v) u)
        (Scalar v))
forall v w y. (v -> w -> y) -> Bilinear v w y
bilinearFunction
           ((LinearMap (Scalar v) (DualVectorFromBasis v) (DualVector u)
  -> Tensor (Scalar v) (DualVectorFromBasis v) u -> Scalar v)
 -> LinearFunction
      (Scalar v)
      (LinearMap (Scalar v) (DualVectorFromBasis v) (DualVector u))
      (LinearFunction
         (Scalar v)
         (Tensor (Scalar v) (DualVectorFromBasis v) u)
         (Scalar v)))
-> (LinearMap (Scalar v) (DualVectorFromBasis v) (DualVector u)
    -> Tensor (Scalar v) (DualVectorFromBasis v) u -> Scalar v)
-> LinearFunction
     (Scalar v)
     (LinearMap (Scalar v) (DualVectorFromBasis v) (DualVector u))
     (LinearFunction
        (Scalar v)
        (Tensor (Scalar v) (DualVectorFromBasis v) u)
        (Scalar v))
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)
             -> [Scalar v] -> Scalar v
forall (t :: * -> *) a. (Foldable t, Num a) => t a -> a
sum [ (LinearFunction
  (Scalar v) (DualVector u) (LinearFunction (Scalar v) u (Scalar v))
forall v.
(LinearSpace v, LinearSpace v) =>
Bilinear (DualVector v) v (Scalar v)
applyDualVectorLinearFunction
  (Scalar v) (DualVector u) (LinearFunction (Scalar v) u (Scalar v))
-> DualVector u -> LinearFunction (Scalar v) u (Scalar v)
forall s v w. LinearFunction s v w -> v -> w
-+$>DualVector u
fi)LinearFunction (Scalar v) u (Scalar v) -> u -> Scalar v
forall s v w. LinearFunction s v w -> v -> w
-+$>(Basis v :->: u) -> Basis v -> u
forall a b. HasTrie a => (a :->: b) -> a -> b
untrie Basis v :->: u
TensorProduct (DualVectorFromBasis v) u
t Basis v
i
                    | (Basis v
i, DualVector u
fi) <- (Basis v :->: DualVector u) -> [(Basis v, DualVector u)]
forall a b. HasTrie a => (a :->: b) -> [(a, b)]
enumerate Basis v :->: DualVector u
TensorProduct (DualVector (DualVectorFromBasis v)) (DualVector u)
f ]
               )
  applyTensorLinMap :: Bilinear
  ((DualVectorFromBasis v ⊗ u) +> w) (DualVectorFromBasis v ⊗ u) w
applyTensorLinMap = Bilinear
  ((DualVectorFromBasis v ⊗ u) +> w) (DualVectorFromBasis v ⊗ u) w
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 :: Bilinear
  ((DualVectorFromBasis v ⊗ u) +> w) (DualVectorFromBasis v ⊗ u) w
atlm = ((TensorProduct v (DualVector u ⊗ w)
  ~ (Basis v :->: (DualVector u ⊗ w))) =>
 LinearFunction
   (Scalar v)
   (LinearMap
      (Scalar v) (Tensor (Scalar v) (DualVectorFromBasis v) u) w)
   (LinearFunction
      (Scalar v) (Tensor (Scalar v) (DualVectorFromBasis v) u) w))
-> LinearFunction
     (Scalar v)
     (LinearMap
        (Scalar v) (Tensor (Scalar v) (DualVectorFromBasis v) u) w)
     (LinearFunction
        (Scalar v) (Tensor (Scalar v) (DualVectorFromBasis v) u) w)
forall v w φ.
BasisGeneratedSpace v =>
((TensorProduct v w ~ (Basis v :->: w)) => φ) -> φ
proveTensorProductIsTrie @v @(DualVector u⊗w) (
          case LinearSpace u => DualSpaceWitness u
forall v. LinearSpace v => DualSpaceWitness v
dualSpaceWitness @u of
           DualSpaceWitness u
DualSpaceWitness -> (LinearMap
   (Scalar v) (Tensor (Scalar v) (DualVectorFromBasis v) u) w
 -> Tensor (Scalar v) (DualVectorFromBasis v) u -> w)
-> LinearFunction
     (Scalar v)
     (LinearMap
        (Scalar v) (Tensor (Scalar v) (DualVectorFromBasis v) u) w)
     (LinearFunction
        (Scalar v) (Tensor (Scalar v) (DualVectorFromBasis v) u) w)
forall v w y. (v -> w -> y) -> Bilinear v w y
bilinearFunction
             ((LinearMap
    (Scalar v) (Tensor (Scalar v) (DualVectorFromBasis v) u) w
  -> Tensor (Scalar v) (DualVectorFromBasis v) u -> w)
 -> LinearFunction
      (Scalar v)
      (LinearMap
         (Scalar v) (Tensor (Scalar v) (DualVectorFromBasis v) u) w)
      (LinearFunction
         (Scalar v) (Tensor (Scalar v) (DualVectorFromBasis v) u) w))
-> (LinearMap
      (Scalar v) (Tensor (Scalar v) (DualVectorFromBasis v) u) w
    -> Tensor (Scalar v) (DualVectorFromBasis v) u -> w)
-> LinearFunction
     (Scalar v)
     (LinearMap
        (Scalar v) (Tensor (Scalar v) (DualVectorFromBasis v) u) w)
     (LinearFunction
        (Scalar v) (Tensor (Scalar v) (DualVectorFromBasis v) u) w)
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)
              -> [w] -> w
forall (f :: * -> *) v. (Foldable f, AdditiveGroup v) => f v -> v
sumV [ (LinearFunction
  (Scalar v)
  (LinearMap (Scalar u) u w)
  (LinearFunction (Scalar v) u w)
forall v w.
(LinearSpace v, TensorSpace w, Scalar w ~ Scalar v) =>
Bilinear (v +> w) v w
applyLinearLinearFunction
  (Scalar v)
  (LinearMap (Scalar u) u w)
  (LinearFunction (Scalar v) u w)
-> LinearMap (Scalar u) u w -> LinearFunction (Scalar v) u w
forall s v w. LinearFunction s v w -> v -> w
-+$>(TensorProduct (DualVector u) w -> LinearMap (Scalar v) u w
forall s v w. TensorProduct (DualVector v) w -> LinearMap s v w
LinearMap TensorProduct (DualVector u) w
fi :: u+>w))
                         LinearFunction (Scalar v) u w -> u -> w
forall s v w. LinearFunction s v w -> v -> w
-+$> (Basis v :->: u) -> Basis v -> u
forall a b. HasTrie a => (a :->: b) -> a -> b
untrie Basis v :->: u
TensorProduct (DualVectorFromBasis v) u
t Basis v
i
                      | (Basis v
i, Tensor TensorProduct (DualVector u) w
fi) <- (Basis v :->: Tensor (Scalar v) (DualVector u) w)
-> [(Basis v, Tensor (Scalar v) (DualVector u) w)]
forall a b. HasTrie a => (a :->: b) -> [(a, b)]
enumerate Basis v :->: Tensor (Scalar v) (DualVector u) w
TensorProduct
  (DualVector (Tensor (Scalar v) (DualVectorFromBasis v) u)) w
f ]
          )
  useTupleLinearSpaceComponents :: ((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' :: (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) = ([c] -> [c]) -> ([c], [b]) -> ([c], [b])
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 c -> [c] -> [c]
forall a. a -> [a] -> [a]
:) (([c], [b]) -> ([c], [b])) -> ([c], [b]) -> ([c], [b])
forall (f :: * -> * -> *) a b.
(Function f, Object f a, Object f b) =>
f a b -> a -> b
$ (a -> b -> c) -> [a] -> [b] -> ([c], [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' :: (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') -> ([c] -> [c]) -> ([c], [b]) -> ([c], [b])
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 c -> [c] -> [c]
forall a. a -> [a] -> [a]
:) (([c], [b]) -> ([c], [b])) -> ([c], [b]) -> ([c], [b])
forall (f :: * -> * -> *) a b.
(Function f, Object f a, Object f b) =>
f a b -> a -> b
$ (a -> [b] -> (c, [b])) -> [a] -> [b] -> ([c], [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 = SubBasis (DualVectorFromBasis v)
forall v. SubBasis (DualVectorFromBasis v)
CompleteDualVBasis
  enumerateSubBasis :: SubBasis (DualVectorFromBasis v) -> [DualVectorFromBasis v]
enumerateSubBasis SubBasis (DualVectorFromBasis v)
CompleteDualVBasis
      = Basis v -> DualVectorFromBasis v
forall v. HasBasis v => Basis v -> v
basisValue (Basis v -> DualVectorFromBasis v)
-> ((Basis v, ()) -> Basis v)
-> (Basis v, ())
-> DualVectorFromBasis 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
. (Basis v, ()) -> Basis v
forall (a :: * -> * -> *) x y.
(PreArrow a, ObjectPair a x y) =>
a (x, y) x
fst ((Basis v, ()) -> DualVectorFromBasis v)
-> [(Basis v, ())] -> [DualVectorFromBasis v]
forall (f :: * -> *) (r :: * -> * -> *) a b.
(Functor f r (->), Object r a, Object r b) =>
r a b -> f a -> f b
<$> (Basis v :->: ()) -> [(Basis v, ())]
forall a b. HasTrie a => (a :->: b) -> [(a, b)]
enumerate ((Basis v -> ()) -> Basis v :->: ()
forall a b. HasTrie a => (a -> b) -> a :->: b
trie ((Basis v -> ()) -> Basis v :->: ())
-> (Basis v -> ()) -> Basis v :->: ()
forall (f :: * -> * -> *) a b.
(Function f, Object f a, Object f b) =>
f a b -> a -> b
$ () -> Basis v -> ()
forall (a :: * -> * -> *) b x.
(WellPointed a, Object a b, ObjectPoint a x) =>
x -> a b x
const ())
  tensorEquality :: (DualVectorFromBasis v ⊗ w) -> (DualVectorFromBasis v ⊗ w) -> Bool
tensorEquality (Tensor TensorProduct (DualVectorFromBasis v) w
t) (Tensor TensorProduct (DualVectorFromBasis v) w
t')
      = [Bool] -> Bool
forall (t :: * -> *). Foldable t => t Bool -> Bool
and [w
ti w -> w -> Bool
forall a. Eq a => a -> a -> Bool
== (Basis v :->: w) -> Basis v -> w
forall a b. HasTrie a => (a :->: b) -> a -> b
untrie Basis v :->: w
TensorProduct (DualVectorFromBasis v) w
t' Basis v
i | (Basis v
i,w
ti) <- (Basis v :->: w) -> [(Basis v, w)]
forall a b. HasTrie a => (a :->: b) -> [(a, b)]
enumerate Basis v :->: w
TensorProduct (DualVectorFromBasis v) w
t]
  decomposeLinMap :: (DualVectorFromBasis v +> w)
-> (SubBasis (DualVectorFromBasis v), DList w)
decomposeLinMap = (DualVectorFromBasis v +> w)
-> (SubBasis (DualVectorFromBasis v), DList w)
forall w.
(DualVectorFromBasis v +> w)
-> (SubBasis (DualVectorFromBasis v), [w] -> [w])
dlm
   where dlm :: ∀ w . (DualVectorFromBasis v+>w)
               -> (SubBasis (DualVectorFromBasis v), [w]->[w])
         dlm :: (DualVectorFromBasis v +> w)
-> (SubBasis (DualVectorFromBasis v), [w] -> [w])
dlm (LinearMap TensorProduct (DualVector (DualVectorFromBasis v)) w
f) = ((TensorProduct v w ~ (Basis v :->: w)) =>
 (SubBasis (DualVectorFromBasis v), [w] -> [w]))
-> (SubBasis (DualVectorFromBasis v), [w] -> [w])
forall v w φ.
BasisGeneratedSpace v =>
((TensorProduct v w ~ (Basis v :->: w)) => φ) -> φ
proveTensorProductIsTrie @v @w
                 ( SubBasis (DualVectorFromBasis v)
forall v. SubBasis (DualVectorFromBasis v)
CompleteDualVBasis
                 , (((Basis v, w) -> w) -> [(Basis v, w)] -> [w]
forall a b. (a -> b) -> [a] -> [b]
map (Basis v, w) -> w
forall (a :: * -> * -> *) x y.
(PreArrow a, ObjectPair a x y) =>
a (x, y) y
snd ((Basis v :->: w) -> [(Basis v, w)]
forall a b. HasTrie a => (a :->: b) -> [(a, b)]
enumerate Basis v :->: w
TensorProduct (DualVector (DualVectorFromBasis v)) w
f) [w] -> [w] -> [w]
forall a. [a] -> [a] -> [a]
++) )
  decomposeLinMapWithin :: SubBasis (DualVectorFromBasis v)
-> (DualVectorFromBasis v +> w)
-> Either (SubBasis (DualVectorFromBasis v), DList w) (DList w)
decomposeLinMapWithin = SubBasis (DualVectorFromBasis v)
-> (DualVectorFromBasis v +> w)
-> Either (SubBasis (DualVectorFromBasis v), DList w) (DList w)
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 :: SubBasis (DualVectorFromBasis v)
-> (DualVectorFromBasis v +> w)
-> Either
     (SubBasis (DualVectorFromBasis v), [w] -> [w]) ([w] -> [w])
dlm SubBasis (DualVectorFromBasis v)
CompleteDualVBasis (LinearMap TensorProduct (DualVector (DualVectorFromBasis v)) w
f) = ((TensorProduct v w ~ (Basis v :->: w)) =>
 Either (SubBasis (DualVectorFromBasis v), [w] -> [w]) ([w] -> [w]))
-> Either
     (SubBasis (DualVectorFromBasis v), [w] -> [w]) ([w] -> [w])
forall v w φ.
BasisGeneratedSpace v =>
((TensorProduct v w ~ (Basis v :->: w)) => φ) -> φ
proveTensorProductIsTrie @v @w
                 (([w] -> [w])
-> Either
     (SubBasis (DualVectorFromBasis v), [w] -> [w]) ([w] -> [w])
forall a b. b -> Either a b
Right (((Basis v, w) -> w) -> [(Basis v, w)] -> [w]
forall a b. (a -> b) -> [a] -> [b]
map (Basis v, w) -> w
forall (a :: * -> * -> *) x y.
(PreArrow a, ObjectPair a x y) =>
a (x, y) y
snd ((Basis v :->: w) -> [(Basis v, w)]
forall a b. HasTrie a => (a :->: b) -> [(a, b)]
enumerate Basis v :->: w
TensorProduct (DualVector (DualVectorFromBasis v)) w
f) [w] -> [w] -> [w]
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])
SubBasis (DualVectorFromBasis v)
-> [Scalar (DualVectorFromBasis v)]
-> (DualVectorFromBasis v, [Scalar (DualVectorFromBasis 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)
CompleteDualVBasis [Scalar v]
cs = ([(Basis v, Scalar v)] -> DualVectorFromBasis v)
-> ([(Basis v, Scalar v)], [Scalar v])
-> (DualVectorFromBasis v, [Scalar v])
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, Scalar v)] -> DualVectorFromBasis v
forall v. HasBasis v => [(Basis v, Scalar v)] -> v
recompose
                   (([(Basis v, Scalar v)], [Scalar v])
 -> (DualVectorFromBasis v, [Scalar v]))
-> ([(Basis v, Scalar v)], [Scalar v])
-> (DualVectorFromBasis v, [Scalar v])
forall (f :: * -> * -> *) a b.
(Function f, Object f a, Object f b) =>
f a b -> a -> b
$ (Basis v -> Scalar v -> (Basis v, Scalar v))
-> [Basis v] -> [Scalar v] -> ([(Basis v, Scalar v)], [Scalar v])
forall a b c. (a -> b -> c) -> [a] -> [b] -> ([c], [b])
zipWith' (,) ((Basis v, ()) -> Basis v
forall (a :: * -> * -> *) x y.
(PreArrow a, ObjectPair a x y) =>
a (x, y) x
fst ((Basis v, ()) -> Basis v) -> [(Basis v, ())] -> [Basis v]
forall (f :: * -> *) (r :: * -> * -> *) a b.
(Functor f r (->), Object r a, Object r b) =>
r a b -> f a -> f b
<$> (Basis v :->: ()) -> [(Basis v, ())]
forall a b. HasTrie a => (a :->: b) -> [(a, b)]
enumerate ((Basis v -> ()) -> Basis v :->: ()
forall a b. HasTrie a => (a -> b) -> a :->: b
trie ((Basis v -> ()) -> Basis v :->: ())
-> (Basis v -> ()) -> Basis v :->: ()
forall (f :: * -> * -> *) a b.
(Function f, Object f a, Object f b) =>
f a b -> a -> b
$ () -> Basis v -> ()
forall (a :: * -> * -> *) b x.
(WellPointed a, Object a b, ObjectPoint a x) =>
x -> a b x
const ())) [Scalar v]
cs
  recomposeSBTensor :: SubBasis (DualVectorFromBasis v)
-> SubBasis w
-> [Scalar (DualVectorFromBasis v)]
-> (DualVectorFromBasis v ⊗ w, [Scalar (DualVectorFromBasis v)])
recomposeSBTensor = SubBasis (DualVectorFromBasis v)
-> SubBasis w
-> [Scalar (DualVectorFromBasis v)]
-> (DualVectorFromBasis v ⊗ w, [Scalar (DualVectorFromBasis v)])
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 :: SubBasis (DualVectorFromBasis v)
-> SubBasis w
-> [Scalar v]
-> (DualVectorFromBasis v ⊗ w, [Scalar v])
rsbt SubBasis (DualVectorFromBasis v)
CompleteDualVBasis SubBasis w
sbw [Scalar v]
ws = ((TensorProduct v w ~ (Basis v :->: w)) =>
 (Tensor (Scalar v) (DualVectorFromBasis v) w, [Scalar v]))
-> (Tensor (Scalar v) (DualVectorFromBasis v) w, [Scalar v])
forall v w φ.
BasisGeneratedSpace v =>
((TensorProduct v w ~ (Basis v :->: w)) => φ) -> φ
proveTensorProductIsTrie @v @w
                 (([(Basis v, w)] -> Tensor (Scalar v) (DualVectorFromBasis v) w)
-> ([(Basis v, w)], [Scalar v])
-> (Tensor (Scalar v) (DualVectorFromBasis v) w, [Scalar v])
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 -> (Basis v :->: w) -> Tensor (Scalar v) (DualVectorFromBasis v) w
forall s v w. TensorProduct v w -> Tensor s v w
Tensor ((Basis v :->: w) -> Tensor (Scalar v) (DualVectorFromBasis v) w)
-> (Basis v :->: w) -> Tensor (Scalar v) (DualVectorFromBasis v) w
forall (f :: * -> * -> *) a b.
(Function f, Object f a, Object f b) =>
f a b -> a -> b
$ (Basis v -> w) -> Basis v :->: w
forall a b. HasTrie a => (a -> b) -> a :->: b
trie ([(Basis v, w)] -> Map (Basis v) w
forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList [(Basis v, w)]
iws Map (Basis v) w -> Basis v -> w
forall k a. Ord k => Map k a -> k -> a
Map.!))
                   (([(Basis v, w)], [Scalar v])
 -> (Tensor (Scalar v) (DualVectorFromBasis v) w, [Scalar v]))
-> ([(Basis v, w)], [Scalar v])
-> (Tensor (Scalar v) (DualVectorFromBasis v) w, [Scalar v])
forall (f :: * -> * -> *) a b.
(Function f, Object f a, Object f b) =>
f a b -> a -> b
$ (Basis v -> [Scalar v] -> ((Basis v, w), [Scalar v]))
-> [Basis v] -> [Scalar v] -> ([(Basis v, w)], [Scalar v])
forall a b c. (a -> [b] -> (c, [b])) -> [a] -> [b] -> ([c], [b])
zipConsumeWith' (\Basis v
i [Scalar v]
cs' -> (w -> (Basis v, w))
-> (w, [Scalar v]) -> ((Basis v, w), [Scalar v])
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,) ((w, [Scalar v]) -> ((Basis v, w), [Scalar v]))
-> (w, [Scalar v]) -> ((Basis v, w), [Scalar v])
forall (f :: * -> * -> *) a b.
(Function f, Object f a, Object f b) =>
f a b -> a -> b
$ SubBasis w -> [Scalar w] -> (w, [Scalar w])
forall v.
FiniteDimensional v =>
SubBasis v -> [Scalar v] -> (v, [Scalar v])
recomposeSB SubBasis w
sbw [Scalar v]
[Scalar w]
cs')
                         ((Basis v, ()) -> Basis v
forall (a :: * -> * -> *) x y.
(PreArrow a, ObjectPair a x y) =>
a (x, y) x
fst ((Basis v, ()) -> Basis v) -> [(Basis v, ())] -> [Basis v]
forall (f :: * -> *) (r :: * -> * -> *) a b.
(Functor f r (->), Object r a, Object r b) =>
r a b -> f a -> f b
<$> (Basis v :->: ()) -> [(Basis v, ())]
forall a b. HasTrie a => (a :->: b) -> [(a, b)]
enumerate ((Basis v -> ()) -> Basis v :->: ()
forall a b. HasTrie a => (a -> b) -> a :->: b
trie ((Basis v -> ()) -> Basis v :->: ())
-> (Basis v -> ()) -> Basis v :->: ()
forall (f :: * -> * -> *) a b.
(Function f, Object f a, Object f b) =>
f a b -> a -> b
$ () -> Basis v -> ()
forall (a :: * -> * -> *) b x.
(WellPointed a, Object a b, ObjectPoint a x) =>
x -> a b x
const ())) [Scalar v]
ws)
  recomposeLinMap :: SubBasis (DualVectorFromBasis v)
-> [w] -> (DualVectorFromBasis v +> w, [w])
recomposeLinMap = SubBasis (DualVectorFromBasis v)
-> [w] -> (DualVectorFromBasis v +> w, [w])
forall w.
SubBasis (DualVectorFromBasis v)
-> [w] -> (DualVectorFromBasis v +> w, [w])
rlm
   where rlm :: ∀ w . SubBasis (DualVectorFromBasis v)
                -> [w]
                -> (DualVectorFromBasis v+>w, [w])
         rlm :: SubBasis (DualVectorFromBasis v)
-> [w] -> (DualVectorFromBasis v +> w, [w])
rlm SubBasis (DualVectorFromBasis v)
CompleteDualVBasis [w]
ws = ((TensorProduct v w ~ (Basis v :->: w)) =>
 (LinearMap (Scalar v) (DualVectorFromBasis v) w, [w]))
-> (LinearMap (Scalar v) (DualVectorFromBasis v) w, [w])
forall v w φ.
BasisGeneratedSpace v =>
((TensorProduct v w ~ (Basis v :->: w)) => φ) -> φ
proveTensorProductIsTrie @v @w
                 (([(Basis v, w)] -> LinearMap (Scalar v) (DualVectorFromBasis v) w)
-> ([(Basis v, w)], [w])
-> (LinearMap (Scalar v) (DualVectorFromBasis v) w, [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 -> (Basis v :->: w) -> LinearMap (Scalar v) (DualVectorFromBasis v) w
forall s v w. TensorProduct (DualVector v) w -> LinearMap s v w
LinearMap ((Basis v :->: w)
 -> LinearMap (Scalar v) (DualVectorFromBasis v) w)
-> (Basis v :->: w)
-> LinearMap (Scalar v) (DualVectorFromBasis v) w
forall (f :: * -> * -> *) a b.
(Function f, Object f a, Object f b) =>
f a b -> a -> b
$ (Basis v -> w) -> Basis v :->: w
forall a b. HasTrie a => (a -> b) -> a :->: b
trie ([(Basis v, w)] -> Map (Basis v) w
forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList [(Basis v, w)]
iws Map (Basis v) w -> Basis v -> w
forall k a. Ord k => Map k a -> k -> a
Map.!))
                   (([(Basis v, w)], [w])
 -> (LinearMap (Scalar v) (DualVectorFromBasis v) w, [w]))
-> ([(Basis v, w)], [w])
-> (LinearMap (Scalar v) (DualVectorFromBasis v) w, [w])
forall (f :: * -> * -> *) a b.
(Function f, Object f a, Object f b) =>
f a b -> a -> b
$ (Basis v -> w -> (Basis v, w))
-> [Basis v] -> [w] -> ([(Basis v, w)], [w])
forall a b c. (a -> b -> c) -> [a] -> [b] -> ([c], [b])
zipWith' (,) ((Basis v, ()) -> Basis v
forall (a :: * -> * -> *) x y.
(PreArrow a, ObjectPair a x y) =>
a (x, y) x
fst ((Basis v, ()) -> Basis v) -> [(Basis v, ())] -> [Basis v]
forall (f :: * -> *) (r :: * -> * -> *) a b.
(Functor f r (->), Object r a, Object r b) =>
r a b -> f a -> f b
<$> (Basis v :->: ()) -> [(Basis v, ())]
forall a b. HasTrie a => (a :->: b) -> [(a, b)]
enumerate ((Basis v -> ()) -> Basis v :->: ()
forall a b. HasTrie a => (a -> b) -> a :->: b
trie ((Basis v -> ()) -> Basis v :->: ())
-> (Basis v -> ()) -> Basis v :->: ()
forall (f :: * -> * -> *) a b.
(Function f, Object f a, Object f b) =>
f a b -> a -> b
$ () -> Basis v -> ()
forall (a :: * -> * -> *) b x.
(WellPointed a, Object a b, ObjectPoint a x) =>
x -> a b x
const ())) [w]
ws)
  recomposeContraLinMap :: (f (Scalar w) -> w)
-> f (DualVector (DualVectorFromBasis v))
-> DualVectorFromBasis v +> w
recomposeContraLinMap = (f (Scalar w) -> w)
-> f (DualVector (DualVectorFromBasis v))
-> DualVectorFromBasis v +> w
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 :: (f (Scalar w) -> w) -> f v -> DualVectorFromBasis v +> w
rclm f (Scalar w) -> w
f f v
vs = ((TensorProduct v w ~ (Basis v :->: w)) =>
 LinearMap (Scalar v) (DualVectorFromBasis v) w)
-> LinearMap (Scalar v) (DualVectorFromBasis v) w
forall v w φ.
BasisGeneratedSpace v =>
((TensorProduct v w ~ (Basis v :->: w)) => φ) -> φ
proveTensorProductIsTrie @v @w
               ((Basis v :->: w) -> LinearMap (Scalar v) (DualVectorFromBasis v) w
forall s v w. TensorProduct (DualVector v) w -> LinearMap s v w
LinearMap ((Basis v :->: w)
 -> LinearMap (Scalar v) (DualVectorFromBasis v) w)
-> (Basis v :->: w)
-> LinearMap (Scalar v) (DualVectorFromBasis v) w
forall (f :: * -> * -> *) a b.
(Function f, Object f a, Object f b) =>
f a b -> a -> b
$ (Basis v -> w) -> Basis v :->: w
forall a b. HasTrie a => (a -> b) -> a :->: b
trie (\Basis v
i -> f (Scalar v) -> w
f (Scalar w) -> w
f (f (Scalar v) -> w) -> f (Scalar v) -> w
forall (f :: * -> * -> *) a b.
(Function f, Object f a, Object f b) =>
f a b -> a -> b
$ (v -> Scalar v) -> f v -> f (Scalar 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 (v -> Basis v -> Scalar v
forall v. HasBasis v => v -> Basis v -> Scalar v
`decompose'`Basis v
i) f v
vs))
  recomposeContraLinMapTensor :: (f (Scalar w) -> w)
-> f (DualVectorFromBasis v +> DualVector u)
-> (DualVectorFromBasis v ⊗ u) +> w
recomposeContraLinMapTensor = (f (Scalar w) -> w)
-> f (DualVectorFromBasis v +> DualVector u)
-> (DualVectorFromBasis v ⊗ u) +> w
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 :: (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 LinearSpace u => DualSpaceWitness u
forall v. LinearSpace v => DualSpaceWitness v
dualSpaceWitness @u of
           DualSpaceWitness u
DualSpaceWitness -> ((TensorProduct v (DualVector u) ~ (Basis v :->: DualVector u)) =>
 LinearMap
   (Scalar v) (Tensor (Scalar v) (DualVectorFromBasis v) u) w)
-> LinearMap
     (Scalar v) (Tensor (Scalar v) (DualVectorFromBasis v) u) w
forall v w φ.
BasisGeneratedSpace v =>
((TensorProduct v w ~ (Basis v :->: w)) => φ) -> φ
proveTensorProductIsTrie @v @(DualVector u)
                      (((TensorProduct v (DualVector u ⊗ w)
  ~ (Basis v :->: (DualVector u ⊗ w))) =>
 LinearMap
   (Scalar v) (Tensor (Scalar v) (DualVectorFromBasis v) u) w)
-> LinearMap
     (Scalar v) (Tensor (Scalar v) (DualVectorFromBasis v) u) w
forall v w φ.
BasisGeneratedSpace v =>
((TensorProduct v w ~ (Basis v :->: w)) => φ) -> φ
proveTensorProductIsTrie @v @(DualVector u⊗w)
               ((Basis v :->: Tensor (Scalar v) (DualVector u) w)
-> LinearMap
     (Scalar v) (Tensor (Scalar v) (DualVectorFromBasis v) u) w
forall s v w. TensorProduct (DualVector v) w -> LinearMap s v w
LinearMap ((Basis v :->: Tensor (Scalar v) (DualVector u) w)
 -> LinearMap
      (Scalar v) (Tensor (Scalar v) (DualVectorFromBasis v) u) w)
-> (Basis v :->: Tensor (Scalar v) (DualVector u) w)
-> LinearMap
     (Scalar v) (Tensor (Scalar v) (DualVectorFromBasis v) u) w
forall (f :: * -> * -> *) a b.
(Function f, Object f a, Object f b) =>
f a b -> a -> b
$ (Basis v -> Tensor (Scalar v) (DualVector u) w)
-> Basis v :->: Tensor (Scalar v) (DualVector u) w
forall a b. HasTrie a => (a -> b) -> a :->: b
trie
                   (\Basis v
i -> case (f (Scalar w) -> w) -> f (DualVector u) -> u +> w
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
                              (f (DualVector u) -> LinearMap (Scalar v) u w)
-> f (DualVector u) -> LinearMap (Scalar v) u w
forall (f :: * -> * -> *) a b.
(Function f, Object f a, Object f b) =>
f a b -> a -> b
$ (LinearMap (Scalar v) (DualVectorFromBasis v) (DualVector u)
 -> DualVector u)
-> f (LinearMap (Scalar v) (DualVectorFromBasis v) (DualVector u))
-> f (DualVector u)
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) -> (Basis v :->: DualVector u) -> Basis v -> DualVector u
forall a b. HasTrie a => (a :->: b) -> a -> b
untrie Basis v :->: DualVector u
TensorProduct (DualVector (DualVectorFromBasis v)) (DualVector u)
vu (Basis v
i :: Basis v)) f (LinearMap (Scalar v) (DualVectorFromBasis v) (DualVector u))
f (DualVectorFromBasis v +> DualVector u)
vus of
                      LinearMap TensorProduct (DualVector u) w
wuff -> TensorProduct (DualVector u) w
-> Tensor (Scalar v) (DualVector u) w
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 = (v -> DualVectorFromBasis v)
-> LinearFunction (Scalar v) v (DualVectorFromBasis v)
forall s v w. (v -> w) -> LinearFunction s v w
LinearFunction v -> DualVectorFromBasis v
forall v. v -> DualVectorFromBasis v
DualVectorFromBasis
  uncanonicallyToDual :: DualVectorFromBasis v -+> DualVector (DualVectorFromBasis v)
uncanonicallyToDual = (DualVectorFromBasis v -> v)
-> LinearFunction (Scalar v) (DualVectorFromBasis v) v
forall s v w. (v -> w) -> LinearFunction s v w
LinearFunction DualVectorFromBasis v -> v
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 = [DualVector (DualVectorFromBasis v)]
-> (DualVectorFromBasis v -> [ℝ])
-> [(Int, DualVectorFromBasis v)]
-> Forest (Int, DualVector (DualVectorFromBasis v))
forall v.
[DualVector v]
-> (v -> [ℝ]) -> [(Int, v)] -> Forest (Int, DualVector v)
cartesianDualBasisCandidates
          (SubBasis v -> [v]
forall v. FiniteDimensional v => SubBasis v -> [v]
enumerateSubBasis SubBasis v
forall v. FiniteDimensional v => SubBasis v
entireBasis)
          (\DualVectorFromBasis v
v -> ((Basis v, ()) -> ℝ) -> [(Basis v, ())] -> [ℝ]
forall a b. (a -> b) -> [a] -> [b]
map (ℝ -> ℝ
forall a. Num a => a -> a
abs (ℝ -> ℝ) -> ((Basis v, ()) -> ℝ) -> (Basis 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
. Scalar v -> ℝ
forall a b. (Real a, Fractional b) => a -> b
realToFrac (Scalar v -> ℝ)
-> ((Basis v, ()) -> Scalar v) -> (Basis 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
. DualVectorFromBasis v
-> Basis (DualVectorFromBasis v) -> Scalar (DualVectorFromBasis v)
forall v. HasBasis v => v -> Basis v -> Scalar v
decompose' DualVectorFromBasis v
v (Basis v -> Scalar v)
-> ((Basis v, ()) -> Basis v) -> (Basis v, ()) -> Scalar 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
. (Basis v, ()) -> Basis v
forall (a :: * -> * -> *) x y.
(PreArrow a, ObjectPair a x y) =>
a (x, y) x
fst)
                  ([(Basis v, ())] -> [ℝ]) -> [(Basis v, ())] -> [ℝ]
forall (f :: * -> * -> *) a b.
(Function f, Object f a, Object f b) =>
f a b -> a -> b
$ (Basis v :->: ()) -> [(Basis v, ())]
forall a b. HasTrie a => (a :->: b) -> [(a, b)]
enumerate ((Basis v -> ()) -> Basis v :->: ()
forall a b. HasTrie a => (a -> b) -> a :->: b
trie ((Basis v -> ()) -> Basis v :->: ())
-> (Basis v -> ()) -> Basis v :->: ()
forall (f :: * -> * -> *) a b.
(Function f, Object f a, Object f b) =>
f a b -> a -> b
$ () -> Basis v -> ()
forall (a :: * -> * -> *) b x.
(WellPointed a, Object a b, ObjectPoint a x) =>
x -> a b x
const ()) )