    -- Copyright (c) 2010-2015, David Amos. All rights reserved.

    {-# LANGUAGE NoMonomorphismRestriction #-}

    -- |A module defining direct sum and tensor product of vector spaces
    module Math.Algebras.TensorProduct where

    import Prelude hiding ( (*>) )

    import Math.Algebras.VectorSpace

    infix 7 `te`, `tf`
    infix 6 `dsume`, `dsumf`

    -- DIRECT SUM

    -- |A type for constructing a basis for the direct sum of vector spaces.
    -- The direct sum of Vect k a and Vect k b is Vect k (DSum a b)
    type DSum a b = Either a b

    -- |Injection of left summand into direct sum
    i1 :: Vect k a -> Vect k (DSum a b)
    i1 :: Vect k a -> Vect k (DSum a b)
    i1 = (a -> DSum a b) -> Vect k a -> Vect k (DSum a b)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap a -> DSum a b
    forall a b. a -> Either a b
    Left

    -- |Injection of right summand into direct sum
    i2 :: Vect k b -> Vect k (DSum a b)
    i2 :: Vect k b -> Vect k (DSum a b)
    i2 = (b -> DSum a b) -> Vect k b -> Vect k (DSum a b)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap b -> DSum a b
    forall a b. b -> Either a b
    Right

    -- |The coproduct of two linear functions (with the same target).
    -- Satisfies the universal property that f == coprodf f g . i1 and g == coprodf f g . i2
    coprodf :: (Eq k, Num k, Ord t) =>
        (Vect k a -> Vect k t) -> (Vect k b -> Vect k t) -> Vect k (DSum a b) -> Vect k t
    coprodf :: (Vect k a -> Vect k t)
    -> (Vect k b -> Vect k t) -> Vect k (DSum a b) -> Vect k t
    coprodf f :: Vect k a -> Vect k t
    f g :: Vect k b -> Vect k t
    g = (DSum a b -> Vect k t) -> Vect k (DSum a b) -> Vect k t
    forall k b a.
    (Eq k, Num k, Ord b) =>
    (a -> Vect k b) -> Vect k a -> Vect k b
    linear DSum a b -> Vect k t
    fg' where
        fg' :: DSum a b -> Vect k t
    fg' (Left a :: a
    a) = Vect k a -> Vect k t
    f (a -> Vect k a
    forall (m :: * -> *) a. Monad m => a -> m a
    return a
    a)
        fg' (Right b :: b
    b) = Vect k b -> Vect k t
    g (b -> Vect k b
    forall (m :: * -> *) a. Monad m => a -> m a
    return b
    b)

    -- |Projection onto left summand from direct sum
    p1 :: (Eq k, Num k, Ord a) => Vect k (DSum a b) -> Vect k a
    p1 :: Vect k (DSum a b) -> Vect k a
    p1 = (DSum a b -> Vect k a) -> Vect k (DSum a b) -> Vect k a
    forall k b a.
    (Eq k, Num k, Ord b) =>
    (a -> Vect k b) -> Vect k a -> Vect k b
    linear DSum a b -> Vect k a
    forall k a b. Num k => Either a b -> Vect k a
    p1' where
        p1' :: Either a b -> Vect k a
    p1' (Left a :: a
    a) = a -> Vect k a
    forall (m :: * -> *) a. Monad m => a -> m a
    return a
    a
        p1' (Right b :: b
    b) = Vect k a
    forall k b. Vect k b
    zerov

    -- |Projection onto right summand from direct sum
    p2 :: (Eq k, Num k, Ord b) => Vect k (DSum a b) -> Vect k b
    p2 :: Vect k (DSum a b) -> Vect k b
    p2 = (DSum a b -> Vect k b) -> Vect k (DSum a b) -> Vect k b
    forall k b a.
    (Eq k, Num k, Ord b) =>
    (a -> Vect k b) -> Vect k a -> Vect k b
    linear DSum a b -> Vect k b
    forall k a b. Num k => Either a b -> Vect k b
    p2' where
        p2' :: Either a b -> Vect k b
    p2' (Left a :: a
    a) = Vect k b
    forall k b. Vect k b
    zerov
        p2' (Right b :: b
    b) = b -> Vect k b
    forall (m :: * -> *) a. Monad m => a -> m a
    return b
    b

    -- |The product of two linear functions (with the same source).
    -- Satisfies the universal property that f == p1 . prodf f g and g == p2 . prodf f g
    prodf :: (Eq k, Num k, Ord a, Ord b) =>
        (Vect k s -> Vect k a) -> (Vect k s -> Vect k b) -> Vect k s -> Vect k (DSum a b)
    prodf :: (Vect k s -> Vect k a)
    -> (Vect k s -> Vect k b) -> Vect k s -> Vect k (DSum a b)
    prodf f :: Vect k s -> Vect k a
    f g :: Vect k s -> Vect k b
    g = (s -> Vect k (DSum a b)) -> Vect k s -> Vect k (DSum a b)
    forall k b a.
    (Eq k, Num k, Ord b) =>
    (a -> Vect k b) -> Vect k a -> Vect k b
    linear s -> Vect k (DSum a b)
    fg' where
        fg' :: s -> Vect k (DSum a b)
    fg' b :: s
    b = (a -> DSum a b) -> Vect k a -> Vect k (DSum a b)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap a -> DSum a b
    forall a b. a -> Either a b
    Left (Vect k s -> Vect k a
    f (Vect k s -> Vect k a) -> Vect k s -> Vect k a
    forall a b. (a -> b) -> a -> b
    $ s -> Vect k s
    forall (m :: * -> *) a. Monad m => a -> m a
    return s
    b) Vect k (DSum a b) -> Vect k (DSum a b) -> Vect k (DSum a b)
    forall k b.
    (Eq k, Num k, Ord b) =>
    Vect k b -> Vect k b -> Vect k b
    <+> (b -> DSum a b) -> Vect k b -> Vect k (DSum a b)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap b -> DSum a b
    forall a b. b -> Either a b
    Right (Vect k s -> Vect k b
    g (Vect k s -> Vect k b) -> Vect k s -> Vect k b
    forall a b. (a -> b) -> a -> b
    $ s -> Vect k s
    forall (m :: * -> *) a. Monad m => a -> m a
    return s
    b)

    -- |The direct sum of two vector space elements
    dsume :: (Eq k, Num k, Ord a, Ord b) => Vect k a -> Vect k b -> Vect k (DSum a b)
    -- dsume x y = fmap Left x <+> fmap Right y
    dsume :: Vect k a -> Vect k b -> Vect k (DSum a b)
    dsume x :: Vect k a
    x y :: Vect k b
    y = Vect k a -> Vect k (DSum a b)
    forall k a b. Vect k a -> Vect k (DSum a b)
    i1 Vect k a
    x Vect k (DSum a b) -> Vect k (DSum a b) -> Vect k (DSum a b)
    forall k b.
    (Eq k, Num k, Ord b) =>
    Vect k b -> Vect k b -> Vect k b
    <+> Vect k b -> Vect k (DSum a b)
    forall k b a. Vect k b -> Vect k (DSum a b)
    i2 Vect k b
    y

    -- |The direct sum of two linear functions.
    -- Satisfies the universal property that f == p1 . dsumf f g . i1 and g == p2 . dsumf f g . i2
    dsumf :: (Eq k, Num k, Ord a, Ord b, Ord a', Ord b') =>
        (Vect k a -> Vect k a') -> (Vect k b -> Vect k b') -> Vect k (DSum a b) -> Vect k (DSum a' b')
    dsumf :: (Vect k a -> Vect k a')
    -> (Vect k b -> Vect k b')
    -> Vect k (DSum a b)
    -> Vect k (DSum a' b')
    dsumf f :: Vect k a -> Vect k a'
    f g :: Vect k b -> Vect k b'
    g ab :: Vect k (DSum a b)
    ab = (Vect k a' -> Vect k (DSum a' b')
    forall k a b. Vect k a -> Vect k (DSum a b)
    i1 (Vect k a' -> Vect k (DSum a' b'))
    -> (Vect k (DSum a b) -> Vect k a')
    -> Vect k (DSum a b)
    -> Vect k (DSum a' b')
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Vect k a -> Vect k a'
    f (Vect k a -> Vect k a')
    -> (Vect k (DSum a b) -> Vect k a)
    -> Vect k (DSum a b)
    -> Vect k a'
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Vect k (DSum a b) -> Vect k a
    forall k a b. (Eq k, Num k, Ord a) => Vect k (DSum a b) -> Vect k a
    p1) Vect k (DSum a b)
    ab Vect k (DSum a' b') -> Vect k (DSum a' b') -> Vect k (DSum a' b')
    forall k b.
    (Eq k, Num k, Ord b) =>
    Vect k b -> Vect k b -> Vect k b
    <+> (Vect k b' -> Vect k (DSum a' b')
    forall k b a. Vect k b -> Vect k (DSum a b)
    i2 (Vect k b' -> Vect k (DSum a' b'))
    -> (Vect k (DSum a b) -> Vect k b')
    -> Vect k (DSum a b)
    -> Vect k (DSum a' b')
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Vect k b -> Vect k b'
    g (Vect k b -> Vect k b')
    -> (Vect k (DSum a b) -> Vect k b)
    -> Vect k (DSum a b)
    -> Vect k b'
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Vect k (DSum a b) -> Vect k b
    forall k b a. (Eq k, Num k, Ord b) => Vect k (DSum a b) -> Vect k b
    p2) Vect k (DSum a b)
    ab

    -- TENSOR PRODUCT

    -- |A type for constructing a basis for the tensor product of vector spaces.
    -- The tensor product of Vect k a and Vect k b is Vect k (Tensor a b)
    type Tensor a b = (a,b)

    -- |The tensor product of two vector space elements
    te :: Num k => Vect k a -> Vect k b -> Vect k (Tensor a b)
    te :: Vect k a -> Vect k b -> Vect k (Tensor a b)
    te (V us :: [(a, k)]
    us) (V vs :: [(b, k)]
    vs) = [(Tensor a b, k)] -> Vect k (Tensor a b)
    forall k b. [(b, k)] -> Vect k b
    V [((a
    a,b
    b), k
    xk -> k -> k
    forall a. Num a => a -> a -> a
    *k
    y) | (a :: a
    a,x :: k
    x) <- [(a, k)]
    us, (b :: b
    b,y :: k
    y) <- [(b, k)]
    vs]
    -- te (V us) (V vs) = V [((ei,ej), xi*xj) | (ei,xi) <- us, (ej,xj) <- vs]
    -- preserves order - that is, if the inputs are correctly ordered, so is the output

    -- Implicit assumption - f and g are linear
    -- |The tensor product of two linear functions
    tf :: (Eq k, Num k, Ord a', Ord b') => (Vect k a -> Vect k a') -> (Vect k b -> Vect k b')
       -> Vect k (Tensor a b) -> Vect k (Tensor a' b')
    tf :: (Vect k a -> Vect k a')
    -> (Vect k b -> Vect k b')
    -> Vect k (Tensor a b)
    -> Vect k (Tensor a' b')
    tf f :: Vect k a -> Vect k a'
    f g :: Vect k b -> Vect k b'
    g (V ts :: [(Tensor a b, k)]
    ts) = [Vect k (Tensor a' b')] -> Vect k (Tensor a' b')
    forall (t :: * -> *) k b.
    (Foldable t, Num k, Ord b, Eq k) =>
    t (Vect k b) -> Vect k b
    sum [k
    x k -> Vect k (Tensor a' b') -> Vect k (Tensor a' b')
    forall k b. (Eq k, Num k) => k -> Vect k b -> Vect k b
    *> Vect k a' -> Vect k b' -> Vect k (Tensor a' b')
    forall k a b. Num k => Vect k a -> Vect k b -> Vect k (Tensor a b)
    te (Vect k a -> Vect k a'
    f (Vect k a -> Vect k a') -> Vect k a -> Vect k a'
    forall a b. (a -> b) -> a -> b
    $ a -> Vect k a
    forall (m :: * -> *) a. Monad m => a -> m a
    return a
    a) (Vect k b -> Vect k b'
    g (Vect k b -> Vect k b') -> Vect k b -> Vect k b'
    forall a b. (a -> b) -> a -> b
    $ b -> Vect k b
    forall (m :: * -> *) a. Monad m => a -> m a
    return b
    b) | ((a :: a
    a,b :: b
    b), x :: k
    x) <- [(Tensor a b, k)]
    ts]
        where sum :: t (Vect k b) -> Vect k b
    sum = (Vect k b -> Vect k b -> Vect k b)
    -> Vect k b -> t (Vect k b) -> Vect k b
    forall (t :: * -> *) b a.
    Foldable t =>
    (b -> a -> b) -> b -> t a -> b
    foldl Vect k b -> Vect k b -> Vect k b
    forall k b.
    (Eq k, Num k, Ord b) =>
    Vect k b -> Vect k b -> Vect k b
    add Vect k b
    forall k b. Vect k b
    zerov

    -- tensor isomorphisms

    -- in fact, this definition works for any Functor f, not just (Vect k)
    assocL :: Vect k (Tensor a (Tensor b c)) -> Vect k (Tensor (Tensor a b) c)
    assocL :: Vect k (Tensor a (Tensor b c)) -> Vect k (Tensor (Tensor a b) c)
    assocL = (Tensor a (Tensor b c) -> Tensor (Tensor a b) c)
    -> Vect k (Tensor a (Tensor b c)) -> Vect k (Tensor (Tensor a b) c)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap ( \(a :: a
    a,(b :: b
    b,c :: c
    c)) -> ((a
    a,b
    b),c
    c) )

    assocR :: Vect k (Tensor (Tensor a b) c) -> Vect k (Tensor a (Tensor b c))
    assocR :: Vect k (Tensor (Tensor a b) c) -> Vect k (Tensor a (Tensor b c))
    assocR = (Tensor (Tensor a b) c -> Tensor a (Tensor b c))
    -> Vect k (Tensor (Tensor a b) c) -> Vect k (Tensor a (Tensor b c))
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap ( \((a :: a
    a,b :: b
    b),c :: c
    c) -> (a
    a,(b
    b,c
    c)) )

    unitInL :: Vect k a -> Vect k (Tensor () a)
    unitInL :: Vect k a -> Vect k (Tensor () a)
    unitInL = (a -> Tensor () a) -> Vect k a -> Vect k (Tensor () a)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap ( \a :: a
    a -> ((),a
    a) )

    unitOutL :: Vect k (Tensor () a) -> Vect k a
    unitOutL :: Vect k (Tensor () a) -> Vect k a
    unitOutL = (Tensor () a -> a) -> Vect k (Tensor () a) -> Vect k a
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap ( \((),a :: a
    a) -> a
    a )

    unitInR :: Vect k a -> Vect k (Tensor a ())
    unitInR :: Vect k a -> Vect k (Tensor a ())
    unitInR = (a -> Tensor a ()) -> Vect k a -> Vect k (Tensor a ())
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap ( \a :: a
    a -> (a
    a,()) )

    unitOutR :: Vect k (Tensor a ()) -> Vect k a
    unitOutR :: Vect k (Tensor a ()) -> Vect k a
    unitOutR = (Tensor a () -> a) -> Vect k (Tensor a ()) -> Vect k a
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap ( \(a :: a
    a,()) -> a
    a )

    twist :: (Eq k, Num k, Ord a, Ord b) => Vect k (Tensor a b) -> Vect k (Tensor b a)
    twist :: Vect k (Tensor a b) -> Vect k (Tensor b a)
    twist v :: Vect k (Tensor a b)
    v = Vect k (Tensor b a) -> Vect k (Tensor b a)
    forall k b. (Eq k, Num k, Ord b) => Vect k b -> Vect k b
    nf (Vect k (Tensor b a) -> Vect k (Tensor b a))
    -> Vect k (Tensor b a) -> Vect k (Tensor b a)
    forall a b. (a -> b) -> a -> b
    $ (Tensor a b -> Tensor b a)
    -> Vect k (Tensor a b) -> Vect k (Tensor b a)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap ( \(a :: a
    a,b :: b
    b) -> (b
    b,a
    a) ) Vect k (Tensor a b)
    v
    -- note the nf call, as f is not order-preserving

    distrL :: (Eq k, Num k, Ord a, Ord b, Ord c)
        => Vect k (Tensor a (DSum b c)) -> Vect k (DSum (Tensor a b) (Tensor a c))
    distrL :: Vect k (Tensor a (DSum b c))
    -> Vect k (DSum (Tensor a b) (Tensor a c))
    distrL v :: Vect k (Tensor a (DSum b c))
    v = Vect k (DSum (Tensor a b) (Tensor a c))
    -> Vect k (DSum (Tensor a b) (Tensor a c))
    forall k b. (Eq k, Num k, Ord b) => Vect k b -> Vect k b
    nf (Vect k (DSum (Tensor a b) (Tensor a c))
     -> Vect k (DSum (Tensor a b) (Tensor a c)))
    -> Vect k (DSum (Tensor a b) (Tensor a c))
    -> Vect k (DSum (Tensor a b) (Tensor a c))
    forall a b. (a -> b) -> a -> b
    $ (Tensor a (DSum b c) -> DSum (Tensor a b) (Tensor a c))
    -> Vect k (Tensor a (DSum b c))
    -> Vect k (DSum (Tensor a b) (Tensor a c))
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap (\(a :: a
    a,bc :: DSum b c
    bc) -> case DSum b c
    bc of Left b :: b
    b -> Tensor a b -> DSum (Tensor a b) (Tensor a c)
    forall a b. a -> Either a b
    Left (a
    a,b
    b); Right c :: c
    c -> Tensor a c -> DSum (Tensor a b) (Tensor a c)
    forall a b. b -> Either a b
    Right (a
    a,c
    c)) Vect k (Tensor a (DSum b c))
    v

    undistrL :: (Eq k, Num k, Ord a, Ord b, Ord c)
        => Vect k (DSum (Tensor a b) (Tensor a c)) -> Vect k (Tensor a (DSum b c))
    undistrL :: Vect k (DSum (Tensor a b) (Tensor a c))
    -> Vect k (Tensor a (DSum b c))
    undistrL v :: Vect k (DSum (Tensor a b) (Tensor a c))
    v = Vect k (Tensor a (DSum b c)) -> Vect k (Tensor a (DSum b c))
    forall k b. (Eq k, Num k, Ord b) => Vect k b -> Vect k b
    nf (Vect k (Tensor a (DSum b c)) -> Vect k (Tensor a (DSum b c)))
    -> Vect k (Tensor a (DSum b c)) -> Vect k (Tensor a (DSum b c))
    forall a b. (a -> b) -> a -> b
    $ (DSum (Tensor a b) (Tensor a c) -> Tensor a (DSum b c))
    -> Vect k (DSum (Tensor a b) (Tensor a c))
    -> Vect k (Tensor a (DSum b c))
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap ( \abc :: DSum (Tensor a b) (Tensor a c)
    abc -> case DSum (Tensor a b) (Tensor a c)
    abc of Left (a :: a
    a,b :: b
    b) -> (a
    a,b -> DSum b c
    forall a b. a -> Either a b
    Left b
    b); Right (a :: a
    a,c :: c
    c) -> (a
    a,c -> DSum b c
    forall a b. b -> Either a b
    Right c
    c) ) Vect k (DSum (Tensor a b) (Tensor a c))
    v

    distrR :: Vect k (Tensor (DSum a b) c) -> Vect k (DSum (Tensor a c) (Tensor b c))
    distrR :: Vect k (Tensor (DSum a b) c)
    -> Vect k (DSum (Tensor a c) (Tensor b c))
    distrR v :: Vect k (Tensor (DSum a b) c)
    v = (Tensor (DSum a b) c -> DSum (Tensor a c) (Tensor b c))
    -> Vect k (Tensor (DSum a b) c)
    -> Vect k (DSum (Tensor a c) (Tensor b c))
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap ( \(ab :: DSum a b
    ab,c :: c
    c) -> case DSum a b
    ab of Left a :: a
    a -> Tensor a c -> DSum (Tensor a c) (Tensor b c)
    forall a b. a -> Either a b
    Left (a
    a,c
    c); Right b :: b
    b -> Tensor b c -> DSum (Tensor a c) (Tensor b c)
    forall a b. b -> Either a b
    Right (b
    b,c
    c) ) Vect k (Tensor (DSum a b) c)
    v
    -- order-preserving, so no nf call needed

    undistrR :: Vect k (DSum (Tensor a c) (Tensor b c)) -> Vect k (Tensor (DSum a b) c)
    undistrR :: Vect k (DSum (Tensor a c) (Tensor b c))
    -> Vect k (Tensor (DSum a b) c)
    undistrR v :: Vect k (DSum (Tensor a c) (Tensor b c))
    v = (DSum (Tensor a c) (Tensor b c) -> Tensor (DSum a b) c)
    -> Vect k (DSum (Tensor a c) (Tensor b c))
    -> Vect k (Tensor (DSum a b) c)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap ( \abc :: DSum (Tensor a c) (Tensor b c)
    abc -> case DSum (Tensor a c) (Tensor b c)
    abc of Left (a :: a
    a,c :: c
    c) -> (a -> DSum a b
    forall a b. a -> Either a b
    Left a
    a, c
    c); Right (b :: b
    b,c :: c
    c) -> (b -> DSum a b
    forall a b. b -> Either a b
    Right b
    b, c
    c) ) Vect k (DSum (Tensor a c) (Tensor b c))
    v

    -- For example:
    -- > distrL (e1 `te` i1 e2) :: Vect Q (DSum (Tensor EBasis EBasis) (Tensor EBasis EBasis))
    -- Left (e1,e2)

    ev :: (Eq k, Num k, Ord b) => Vect k (Tensor (Dual b) b) -> k
    ev :: Vect k (Tensor (Dual b) b) -> k
    ev = Vect k () -> k
    forall k. Num k => Vect k () -> k
    unwrap (Vect k () -> k)
    -> (Vect k (Tensor (Dual b) b) -> Vect k ())
    -> Vect k (Tensor (Dual b) b)
    -> k
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (Tensor (Dual b) b -> Vect k ())
    -> Vect k (Tensor (Dual b) b) -> Vect k ()
    forall k b a.
    (Eq k, Num k, Ord b) =>
    (a -> Vect k b) -> Vect k a -> Vect k b
    linear (\(Dual bi :: b
    bi, bj :: b
    bj) -> b -> b -> k
    forall a p. (Eq a, Num p) => a -> a -> p
    delta b
    bi b
    bj k -> Vect k () -> Vect k ()
    forall k b. (Eq k, Num k) => k -> Vect k b -> Vect k b
    *> () -> Vect k ()
    forall (m :: * -> *) a. Monad m => a -> m a
    return ())
    -- slightly cheating, as delta i j is meant to compare indices, not the basis elements themselves

    delta :: a -> a -> p
    delta i :: a
    i j :: a
    j = if a
    i a -> a -> Bool
    forall a. Eq a => a -> a -> Bool
    == a
    j then 1 else 0

    reify :: (Eq k, Num k, Ord b) => Vect k (Dual b) -> (Vect k b -> k)
    reify :: Vect k (Dual b) -> Vect k b -> k
    reify f :: Vect k (Dual b)
    f x :: Vect k b
    x = Vect k (Tensor (Dual b) b) -> k
    forall k b. (Eq k, Num k, Ord b) => Vect k (Tensor (Dual b) b) -> k
    ev (Vect k (Dual b)
    f Vect k (Dual b) -> Vect k b -> Vect k (Tensor (Dual b) b)
    forall k a b. Num k => Vect k a -> Vect k b -> Vect k (Tensor a b)
    `te` Vect k b
    x)