{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE FunctionalDependencies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE Rank2Types #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE PatternSynonyms #-}
{-# LANGUAGE TupleSections #-}
{-# LANGUAGE UnicodeSyntax #-}
{-# LANGUAGE CPP #-}
{-# LANGUAGE TupleSections #-}
{-# LANGUAGE StandaloneDeriving #-}
module Math.LinearMap.Asserted where
import Data.VectorSpace
import Data.Basis
import Math.Manifold.Core.PseudoAffine
import Prelude ()
import qualified Prelude as Hask
import Control.Category.Constrained.Prelude
import Control.Arrow.Constrained
import Data.Traversable.Constrained
import Data.Coerce
import Data.Type.Coercion
import Data.Tagged
import Data.VectorSpace.Free
import qualified Linear.Matrix as Mat
import qualified Linear.Vector as Mat
import Math.VectorSpace.ZeroDimensional
newtype LinearFunction s v w = LinearFunction { forall s v w. LinearFunction s v w -> v -> w
getLinearFunction :: v -> w }
linearFunction :: VectorSpace w => (v->w) -> LinearFunction (Scalar v) v w
linearFunction :: forall w v.
VectorSpace w =>
(v -> w) -> LinearFunction (Scalar v) v w
linearFunction = forall s v w. (v -> w) -> LinearFunction s v w
LinearFunction
scaleWith :: (VectorSpace v, Scalar v ~ s) => s -> LinearFunction s v v
scaleWith :: forall v s.
(VectorSpace v, Scalar v ~ s) =>
s -> LinearFunction s v v
scaleWith s
μ = forall s v w. (v -> w) -> LinearFunction s v w
LinearFunction (s
μforall v. VectorSpace v => Scalar v -> v -> v
*^)
scaleV :: (VectorSpace v, Scalar v ~ s) => v -> LinearFunction s s v
scaleV :: forall v s.
(VectorSpace v, Scalar v ~ s) =>
v -> LinearFunction s s v
scaleV v
v = forall s v w. (v -> w) -> LinearFunction s v w
LinearFunction (forall v. VectorSpace v => Scalar v -> v -> v
*^v
v)
const0 :: AdditiveGroup w => LinearFunction s v w
const0 :: forall w s v. AdditiveGroup w => LinearFunction s v w
const0 = forall s v w. (v -> w) -> LinearFunction s v w
LinearFunction (forall (a :: * -> * -> *) b x.
(WellPointed a, Object a b, ObjectPoint a x) =>
x -> a b x
const forall v. AdditiveGroup v => v
zeroV)
lNegateV :: AdditiveGroup w => LinearFunction s w w
lNegateV :: forall w s. AdditiveGroup w => LinearFunction s w w
lNegateV = forall s v w. (v -> w) -> LinearFunction s v w
LinearFunction forall v. AdditiveGroup v => v -> v
negateV
addV :: AdditiveGroup w => LinearFunction s (w,w) w
addV :: forall w s. AdditiveGroup w => LinearFunction s (w, w) w
addV = forall s v w. (v -> w) -> LinearFunction s v w
LinearFunction forall (f :: * -> * -> *) a b.
(Function f, Object f a, Object f b) =>
f a b -> a -> b
$ forall (k :: * -> * -> *) a b c.
(Curry k, ObjectPair k a b, ObjectMorphism k b c) =>
k a (k b c) -> k (a, b) c
uncurry forall v. AdditiveGroup v => v -> v -> v
(^+^)
instance AdditiveGroup w => AdditiveGroup (LinearFunction s v w) where
zeroV :: LinearFunction s v w
zeroV = forall w s v. AdditiveGroup w => LinearFunction s v w
const0
LinearFunction v -> w
f ^+^ :: LinearFunction s v w
-> LinearFunction s v w -> LinearFunction s v w
^+^ LinearFunction v -> w
g = forall s v w. (v -> w) -> LinearFunction s v w
LinearFunction forall (f :: * -> * -> *) a b.
(Function f, Object f a, Object f b) =>
f a b -> a -> b
$ \v
x -> v -> w
f v
x forall v. AdditiveGroup v => v -> v -> v
^+^ v -> w
g v
x
LinearFunction v -> w
f ^-^ :: LinearFunction s v w
-> LinearFunction s v w -> LinearFunction s v w
^-^ LinearFunction v -> w
g = forall s v w. (v -> w) -> LinearFunction s v w
LinearFunction forall (f :: * -> * -> *) a b.
(Function f, Object f a, Object f b) =>
f a b -> a -> b
$ \v
x -> v -> w
f v
x forall v. AdditiveGroup v => v -> v -> v
^-^ v -> w
g v
x
negateV :: LinearFunction s v w -> LinearFunction s v w
negateV (LinearFunction v -> w
f) = forall s v w. (v -> w) -> LinearFunction s v w
LinearFunction forall (f :: * -> * -> *) a b.
(Function f, Object f a, Object f b) =>
f a b -> a -> b
$ forall v. AdditiveGroup v => v -> v
negateV 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
. v -> w
f
instance VectorSpace w => VectorSpace (LinearFunction s v w) where
type Scalar (LinearFunction s v w) = Scalar w
Scalar (LinearFunction s v w)
μ *^ :: Scalar (LinearFunction s v w)
-> LinearFunction s v w -> LinearFunction s v w
*^ LinearFunction v -> w
f = forall s v w. (v -> w) -> LinearFunction s v w
LinearFunction forall (f :: * -> * -> *) a b.
(Function f, Object f a, Object f b) =>
f a b -> a -> b
$ (Scalar (LinearFunction s v w)
μforall v. VectorSpace v => Scalar v -> v -> v
*^) forall κ (k :: κ -> κ -> *) (a :: κ) (b :: κ) (c :: κ).
(Category k, Object k a, Object k b, Object k c) =>
k b c -> k a b -> k a c
. v -> w
f
instance VectorSpace w => Semimanifold (LinearFunction s v w) where
type Needle (LinearFunction s v w) = LinearFunction s v w
#if !MIN_VERSION_manifolds_core(0,6,0)
toInterior = pure
fromInterior = id
translateP = Tagged (^+^)
#endif
.+~^ :: LinearFunction s v w
-> Needle (LinearFunction s v w) -> LinearFunction s v w
(.+~^) = forall v. AdditiveGroup v => v -> v -> v
(^+^)
instance VectorSpace w => PseudoAffine (LinearFunction s v w) where
LinearFunction s v w
f.-~. :: LinearFunction s v w
-> LinearFunction s v w -> Maybe (Needle (LinearFunction s v w))
.-~.LinearFunction s v w
g = forall (m :: * -> *) a. Monad m (->) => a -> m a
return forall (f :: * -> * -> *) a b.
(Function f, Object f a, Object f b) =>
f a b -> a -> b
$ LinearFunction s v w
fforall v. AdditiveGroup v => v -> v -> v
^-^LinearFunction s v w
g
LinearFunction s v w
f.-~! :: HasCallStack =>
LinearFunction s v w
-> LinearFunction s v w -> Needle (LinearFunction s v w)
.-~!LinearFunction s v w
g = LinearFunction s v w
fforall v. AdditiveGroup v => v -> v -> v
^-^LinearFunction s v w
g
instance Functor (LinearFunction s v) Coercion Coercion where
fmap :: forall a b.
(Object Coercion a, Object Coercion (LinearFunction s v a),
Object Coercion b, Object Coercion (LinearFunction s v b)) =>
Coercion a b
-> Coercion (LinearFunction s v a) (LinearFunction s v b)
fmap Coercion a b
Coercion = forall {k} (a :: k) (b :: k). Coercible a b => Coercion a b
Coercion
fmapScale :: ( VectorSpace w, Scalar w ~ s, VectorSpace s
, Functor f (LinearFunction s) (LinearFunction s)
, Object (LinearFunction s) s
, Object (LinearFunction s) w
, Object (LinearFunction s) (f s)
, Object (LinearFunction s) (f w)
, EnhancedCat (->) (LinearFunction s)
, VectorSpace (f w), Scalar (f w) ~ s
, VectorSpace (f s), Scalar (f s) ~ s )
=> f s -> LinearFunction s w (f w)
fmapScale :: forall w s (f :: * -> *).
(VectorSpace w, Scalar w ~ s, VectorSpace s,
Functor f (LinearFunction s) (LinearFunction s),
Object (LinearFunction s) s, Object (LinearFunction s) w,
Object (LinearFunction s) (f s), Object (LinearFunction s) (f w),
EnhancedCat (->) (LinearFunction s), VectorSpace (f w),
Scalar (f w) ~ s, VectorSpace (f s), Scalar (f s) ~ s) =>
f s -> LinearFunction s w (f w)
fmapScale f s
v = forall s v w. (v -> w) -> LinearFunction s v w
LinearFunction forall (f :: * -> * -> *) a b.
(Function f, Object f a, Object f b) =>
f a b -> a -> b
$ \w
w -> forall (f :: * -> *) (r :: * -> * -> *) (t :: * -> * -> *) a b.
(Functor f r t, Object r a, Object t (f a), Object r b,
Object t (f b)) =>
r a b -> t (f a) (f b)
fmap (forall v s.
(VectorSpace v, Scalar v ~ s) =>
v -> LinearFunction s s v
scaleV w
w) forall (f :: * -> * -> *) a b.
(Function f, Object f a, Object f b) =>
f a b -> a -> b
$ f s
v
lCoFst :: (AdditiveGroup w) => LinearFunction s v (v,w)
lCoFst :: forall w s v. AdditiveGroup w => LinearFunction s v (v, w)
lCoFst = forall s v w. (v -> w) -> LinearFunction s v w
LinearFunction (,forall v. AdditiveGroup v => v
zeroV)
lCoSnd :: (AdditiveGroup v) => LinearFunction s w (v,w)
lCoSnd :: forall v s w. AdditiveGroup v => LinearFunction s w (v, w)
lCoSnd = forall s v w. (v -> w) -> LinearFunction s v w
LinearFunction (forall v. AdditiveGroup v => v
zeroV,)
type v-+>w = LinearFunction (Scalar w) v w
type Bilinear v w y = LinearFunction (Scalar v) v (LinearFunction (Scalar v) w y)
bilinearFunction :: (v -> w -> y) -> Bilinear v w y
bilinearFunction :: forall v w y. (v -> w -> y) -> Bilinear v w y
bilinearFunction v -> w -> y
f = forall s v w. (v -> w) -> LinearFunction s v w
LinearFunction forall (f :: * -> * -> *) a b.
(Function f, Object f a, Object f b) =>
f a b -> a -> b
$ forall s v w. (v -> w) -> LinearFunction s v w
LinearFunction 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
. v -> w -> y
f
flipBilin :: Bilinear v w y -> Bilinear w v y
flipBilin :: forall v w y. Bilinear v w y -> Bilinear w v y
flipBilin (LinearFunction v -> LinearFunction (Scalar v) w y
f) = forall s v w. (v -> w) -> LinearFunction s v w
LinearFunction
forall (f :: * -> * -> *) a b.
(Function f, Object f a, Object f b) =>
f a b -> a -> b
$ \w
w -> forall s v w. (v -> w) -> LinearFunction s v w
LinearFunction forall (f :: * -> * -> *) a b.
(Function f, Object f a, Object f b) =>
f a b -> a -> b
$ v -> LinearFunction (Scalar v) w y
f forall (k :: * -> * -> *) a b c.
(Category k, Object k a, Object k b, Object k c) =>
k a b -> k b c -> k a c
>>> \(LinearFunction w -> y
g) -> w -> y
g w
w
scale :: VectorSpace v => Bilinear (Scalar v) v v
scale :: forall v. VectorSpace v => Bilinear (Scalar v) v v
scale = forall s v w. (v -> w) -> LinearFunction s v w
LinearFunction forall (f :: * -> * -> *) a b.
(Function f, Object f a, Object f b) =>
f a b -> a -> b
$ \Scalar v
μ -> forall s v w. (v -> w) -> LinearFunction s v w
LinearFunction (Scalar v
μforall v. VectorSpace v => Scalar v -> v -> v
*^)
elacs :: VectorSpace v => Bilinear v (Scalar v) v
elacs :: forall v. VectorSpace v => Bilinear v (Scalar v) v
elacs = forall s v w. (v -> w) -> LinearFunction s v w
LinearFunction forall (f :: * -> * -> *) a b.
(Function f, Object f a, Object f b) =>
f a b -> a -> b
$ \v
v -> forall s v w. (v -> w) -> LinearFunction s v w
LinearFunction (forall v. VectorSpace v => Scalar v -> v -> v
*^v
v)
inner :: InnerSpace v => Bilinear v v (Scalar v)
inner :: forall v. InnerSpace v => Bilinear v v (Scalar v)
inner = forall s v w. (v -> w) -> LinearFunction s v w
LinearFunction forall (f :: * -> * -> *) a b.
(Function f, Object f a, Object f b) =>
f a b -> a -> b
$ \v
v -> forall s v w. (v -> w) -> LinearFunction s v w
LinearFunction (v
vforall v. InnerSpace v => v -> v -> Scalar v
<.>)
biConst0 :: AdditiveGroup v => Bilinear a b v
biConst0 :: forall v a b. AdditiveGroup v => Bilinear a b v
biConst0 = forall s v w. (v -> w) -> LinearFunction s v w
LinearFunction forall (f :: * -> * -> *) a b.
(Function f, Object f a, Object f b) =>
f a b -> a -> b
$ forall (a :: * -> * -> *) b x.
(WellPointed a, Object a b, ObjectPoint a x) =>
x -> a b x
const forall w s v. AdditiveGroup w => LinearFunction s v w
const0
lApply :: Bilinear (v-+>w) v w
lApply :: forall v w. Bilinear (v -+> w) v w
lApply = forall v w y. (v -> w -> y) -> Bilinear v w y
bilinearFunction forall (f :: * -> * -> *) a b.
(Function f, Object f a, Object f b) =>
f a b -> a -> b
$ \(LinearFunction v -> w
f) v
v -> v -> w
f v
v
infixr 0 -+$>
(-+$>) :: LinearFunction s v w -> v -> w
LinearFunction v -> w
f -+$> :: forall s v w. LinearFunction s v w -> v -> w
-+$> v
v = v -> w
f v
v