-- |
-- Module      : Math.LinearMap.Asserted
-- Copyright   : (c) Justus Sagemüller 2016
-- License     : GPL v3
-- 
-- Maintainer  : (@) jsag $ hvl.no
-- Stability   : experimental
-- Portability : portable
-- 
{-# 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




-- | A linear map, represented simply as a Haskell function tagged with
--   the type of scalar with respect to which it is linear. Many (sparse)
--   linear mappings can actually be calculated much more efficiently
--   if you don't represent them with any kind of matrix, but
--   just as a function (which is after all, mathematically speaking,
--   what a linear map foremostly is).
-- 
--   However, if you sum up many 'LinearFunction's – which you can
--   simply do with the 'VectorSpace' instance – they will become ever
--   slower to calculate, because the summand-functions are actually computed
--   individually and only the results summed. That's where
--   'Math.LinearMap.Category.LinearMap' is generally preferrable.
--   You can always convert between these equivalent categories using 'arr'.
newtype LinearFunction s v w = LinearFunction { LinearFunction s v w -> v -> w
getLinearFunction :: v -> w }




linearFunction :: VectorSpace w => (v->w) -> LinearFunction (Scalar v) v w
linearFunction :: (v -> w) -> LinearFunction (Scalar v) v w
linearFunction = (v -> w) -> LinearFunction (Scalar v) v w
forall s v w. (v -> w) -> LinearFunction s v w
LinearFunction

scaleWith :: (VectorSpace v, Scalar v ~ s) => s -> LinearFunction s v v
scaleWith :: s -> LinearFunction s v v
scaleWith s
μ = (v -> v) -> LinearFunction s v v
forall s v w. (v -> w) -> LinearFunction s v w
LinearFunction (s
Scalar v
μScalar v -> v -> v
forall v. VectorSpace v => Scalar v -> v -> v
*^)

scaleV :: (VectorSpace v, Scalar v ~ s) => v -> LinearFunction s s v
scaleV :: v -> LinearFunction s s v
scaleV v
v = (s -> v) -> LinearFunction s s v
forall s v w. (v -> w) -> LinearFunction s v w
LinearFunction (Scalar v -> v -> v
forall v. VectorSpace v => Scalar v -> v -> v
*^v
v)

const0 :: AdditiveGroup w => LinearFunction s v w
const0 :: LinearFunction s v w
const0 = (v -> w) -> LinearFunction s v w
forall s v w. (v -> w) -> LinearFunction s v w
LinearFunction (w -> 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)

lNegateV :: AdditiveGroup w => LinearFunction s w w
lNegateV :: LinearFunction s w w
lNegateV = (w -> w) -> LinearFunction s w w
forall s v w. (v -> w) -> LinearFunction s v w
LinearFunction w -> w
forall v. AdditiveGroup v => v -> v
negateV

addV :: AdditiveGroup w => LinearFunction s (w,w) w
addV :: LinearFunction s (w, w) w
addV = ((w, w) -> w) -> LinearFunction s (w, w) w
forall s v w. (v -> w) -> LinearFunction s v w
LinearFunction (((w, w) -> w) -> LinearFunction s (w, w) w)
-> ((w, w) -> w) -> LinearFunction s (w, w) w
forall (f :: * -> * -> *) a b.
(Function f, Object f a, Object f b) =>
f a b -> a -> b
$ (w -> w -> w) -> (w, w) -> w
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 w -> w -> w
forall v. AdditiveGroup v => v -> v -> v
(^+^)

instance AdditiveGroup w => AdditiveGroup (LinearFunction s v w) where
  zeroV :: LinearFunction s v w
zeroV = LinearFunction s v w
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 = (v -> w) -> LinearFunction s v w
forall s v w. (v -> w) -> LinearFunction s v w
LinearFunction ((v -> w) -> LinearFunction s v w)
-> (v -> w) -> LinearFunction s v w
forall (f :: * -> * -> *) a b.
(Function f, Object f a, Object f b) =>
f a b -> a -> b
$ \v
x -> v -> w
f v
x w -> w -> w
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 = (v -> w) -> LinearFunction s v w
forall s v w. (v -> w) -> LinearFunction s v w
LinearFunction ((v -> w) -> LinearFunction s v w)
-> (v -> w) -> LinearFunction s v w
forall (f :: * -> * -> *) a b.
(Function f, Object f a, Object f b) =>
f a b -> a -> b
$ \v
x -> v -> w
f v
x w -> w -> w
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) = (v -> w) -> LinearFunction s v w
forall s v w. (v -> w) -> LinearFunction s v w
LinearFunction ((v -> w) -> LinearFunction s v w)
-> (v -> w) -> LinearFunction s v w
forall (f :: * -> * -> *) a b.
(Function f, Object f a, Object f b) =>
f a b -> a -> b
$ w -> w
forall v. AdditiveGroup v => v -> v
negateV (w -> w) -> (v -> w) -> 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
. 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 = (v -> w) -> LinearFunction s v w
forall s v w. (v -> w) -> LinearFunction s v w
LinearFunction ((v -> w) -> LinearFunction s v w)
-> (v -> w) -> LinearFunction s v w
forall (f :: * -> * -> *) a b.
(Function f, Object f a, Object f b) =>
f a b -> a -> b
$ (Scalar w
Scalar (LinearFunction s v w)
μScalar w -> w -> w
forall v. VectorSpace v => Scalar v -> v -> v
*^) (w -> w) -> (v -> w) -> 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
. 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
(.+~^) = 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 = LinearFunction s v w -> Maybe (LinearFunction s v w)
forall (m :: * -> *) a. Monad m (->) => a -> m a
return (LinearFunction s v w -> Maybe (LinearFunction s v w))
-> LinearFunction s v w -> Maybe (LinearFunction s v w)
forall (f :: * -> * -> *) a b.
(Function f, Object f a, Object f b) =>
f a b -> a -> b
$ LinearFunction s v w
fLinearFunction s v w
-> LinearFunction s v w -> LinearFunction s v w
forall v. AdditiveGroup v => v -> v -> v
^-^LinearFunction s v w
g
  LinearFunction s v w
f.-~! :: LinearFunction s v w
-> LinearFunction s v w -> Needle (LinearFunction s v w)
.-~!LinearFunction s v w
g = LinearFunction s v w
fLinearFunction s v w
-> LinearFunction s v w -> LinearFunction s v w
forall v. AdditiveGroup v => v -> v -> v
^-^LinearFunction s v w
g

instance Functor (LinearFunction s v) Coercion Coercion where
  fmap :: Coercion a b
-> Coercion (LinearFunction s v a) (LinearFunction s v b)
fmap Coercion a b
Coercion = Coercion (LinearFunction s v a) (LinearFunction s v b)
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 :: f s -> LinearFunction s w (f w)
fmapScale f s
v = (w -> f w) -> LinearFunction s w (f w)
forall s v w. (v -> w) -> LinearFunction s v w
LinearFunction ((w -> f w) -> LinearFunction s w (f w))
-> (w -> f w) -> LinearFunction s w (f w)
forall (f :: * -> * -> *) a b.
(Function f, Object f a, Object f b) =>
f a b -> a -> b
$ \w
w -> LinearFunction s s w -> LinearFunction s (f s) (f 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 (w -> LinearFunction s s w
forall v s.
(VectorSpace v, Scalar v ~ s) =>
v -> LinearFunction s s v
scaleV w
w) LinearFunction s (f s) (f w) -> f s -> f 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 :: LinearFunction s v (v, w)
lCoFst = (v -> (v, w)) -> LinearFunction s v (v, w)
forall s v w. (v -> w) -> LinearFunction s v w
LinearFunction (,w
forall v. AdditiveGroup v => v
zeroV)
lCoSnd :: (AdditiveGroup v) => LinearFunction s w (v,w)
lCoSnd :: LinearFunction s w (v, w)
lCoSnd = (w -> (v, w)) -> LinearFunction s w (v, w)
forall s v w. (v -> w) -> LinearFunction s v w
LinearFunction (v
forall v. AdditiveGroup v => v
zeroV,)



-- | Infix synonym of 'LinearFunction', without explicit mention of the scalar type.
type v-+>w = LinearFunction (Scalar w) v w

-- | A bilinear function is a linear function mapping to a linear function,
--   or equivalently a 2-argument function that's linear in each argument
--   independently.
--   Note that this can /not/ be uncurried to a linear function with a tuple
--   argument (this would not be linear but quadratic).
type Bilinear v w y = LinearFunction (Scalar v) v (LinearFunction (Scalar v) w y)

bilinearFunction :: (v -> w -> y) -> Bilinear v w y
bilinearFunction :: (v -> w -> y) -> Bilinear v w y
bilinearFunction v -> w -> y
f = (v -> LinearFunction (Scalar v) w y) -> Bilinear v w y
forall s v w. (v -> w) -> LinearFunction s v w
LinearFunction ((v -> LinearFunction (Scalar v) w y) -> Bilinear v w y)
-> (v -> LinearFunction (Scalar v) w y) -> Bilinear v w y
forall (f :: * -> * -> *) a b.
(Function f, Object f a, Object f b) =>
f a b -> a -> b
$ (w -> y) -> LinearFunction (Scalar v) w y
forall s v w. (v -> w) -> LinearFunction s v w
LinearFunction ((w -> y) -> LinearFunction (Scalar v) w y)
-> (v -> w -> y) -> v -> LinearFunction (Scalar v) w y
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 :: Bilinear v w y -> Bilinear w v y
flipBilin (LinearFunction v -> LinearFunction (Scalar v) w y
f) = (w -> LinearFunction (Scalar w) v y) -> Bilinear w v y
forall s v w. (v -> w) -> LinearFunction s v w
LinearFunction
     ((w -> LinearFunction (Scalar w) v y) -> Bilinear w v y)
-> (w -> LinearFunction (Scalar w) v y) -> Bilinear w v y
forall (f :: * -> * -> *) a b.
(Function f, Object f a, Object f b) =>
f a b -> a -> b
$ \w
w -> (v -> y) -> LinearFunction (Scalar w) v y
forall s v w. (v -> w) -> LinearFunction s v w
LinearFunction ((v -> y) -> LinearFunction (Scalar w) v y)
-> (v -> y) -> LinearFunction (Scalar w) v y
forall (f :: * -> * -> *) a b.
(Function f, Object f a, Object f b) =>
f a b -> a -> b
$ v -> LinearFunction (Scalar v) w y
f (v -> LinearFunction (Scalar v) w y)
-> (LinearFunction (Scalar v) w y -> y) -> v -> y
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 :: Bilinear (Scalar v) v v
scale = (Scalar v -> LinearFunction (Scalar (Scalar v)) v v)
-> Bilinear (Scalar v) v v
forall s v w. (v -> w) -> LinearFunction s v w
LinearFunction ((Scalar v -> LinearFunction (Scalar (Scalar v)) v v)
 -> Bilinear (Scalar v) v v)
-> (Scalar v -> LinearFunction (Scalar (Scalar v)) v v)
-> Bilinear (Scalar v) v v
forall (f :: * -> * -> *) a b.
(Function f, Object f a, Object f b) =>
f a b -> a -> b
$ \Scalar v
μ -> (v -> v) -> LinearFunction (Scalar (Scalar v)) v v
forall s v w. (v -> w) -> LinearFunction s v w
LinearFunction (Scalar v
μScalar v -> v -> v
forall v. VectorSpace v => Scalar v -> v -> v
*^)

-- | @elacs ≡ 'flipBilin' 'scale'@.
elacs :: VectorSpace v => Bilinear v (Scalar v) v
elacs :: Bilinear v (Scalar v) v
elacs = (v -> LinearFunction (Scalar v) (Scalar v) v)
-> Bilinear v (Scalar v) v
forall s v w. (v -> w) -> LinearFunction s v w
LinearFunction ((v -> LinearFunction (Scalar v) (Scalar v) v)
 -> Bilinear v (Scalar v) v)
-> (v -> LinearFunction (Scalar v) (Scalar v) v)
-> Bilinear v (Scalar v) v
forall (f :: * -> * -> *) a b.
(Function f, Object f a, Object f b) =>
f a b -> a -> b
$ \v
v -> (Scalar v -> v) -> LinearFunction (Scalar v) (Scalar v) v
forall s v w. (v -> w) -> LinearFunction s v w
LinearFunction (Scalar v -> v -> v
forall v. VectorSpace v => Scalar v -> v -> v
*^v
v)

inner :: InnerSpace v => Bilinear v v (Scalar v)
inner :: Bilinear v v (Scalar v)
inner = (v -> LinearFunction (Scalar v) v (Scalar v))
-> Bilinear v v (Scalar v)
forall s v w. (v -> w) -> LinearFunction s v w
LinearFunction ((v -> LinearFunction (Scalar v) v (Scalar v))
 -> Bilinear v v (Scalar v))
-> (v -> LinearFunction (Scalar v) v (Scalar v))
-> Bilinear v v (Scalar v)
forall (f :: * -> * -> *) a b.
(Function f, Object f a, Object f b) =>
f a b -> a -> b
$ \v
v -> (v -> Scalar v) -> LinearFunction (Scalar v) v (Scalar v)
forall s v w. (v -> w) -> LinearFunction s v w
LinearFunction (v
vv -> v -> Scalar v
forall v. InnerSpace v => v -> v -> Scalar v
<.>)

biConst0 :: AdditiveGroup v => Bilinear a b v
biConst0 :: Bilinear a b v
biConst0 = (a -> LinearFunction (Scalar a) b v) -> Bilinear a b v
forall s v w. (v -> w) -> LinearFunction s v w
LinearFunction ((a -> LinearFunction (Scalar a) b v) -> Bilinear a b v)
-> (a -> LinearFunction (Scalar a) b v) -> Bilinear a b v
forall (f :: * -> * -> *) a b.
(Function f, Object f a, Object f b) =>
f a b -> a -> b
$ LinearFunction (Scalar a) b v -> a -> LinearFunction (Scalar a) b v
forall (a :: * -> * -> *) b x.
(WellPointed a, Object a b, ObjectPoint a x) =>
x -> a b x
const LinearFunction (Scalar a) b v
forall w s v. AdditiveGroup w => LinearFunction s v w
const0

lApply :: Bilinear (v-+>w) v w
lApply :: Bilinear (v -+> w) v w
lApply = ((v -+> w) -> v -> w)
-> LinearFunction (Scalar w) (v -+> w) (v -+> w)
forall v w y. (v -> w -> y) -> Bilinear v w y
bilinearFunction (((v -+> w) -> v -> w)
 -> LinearFunction (Scalar w) (v -+> w) (v -+> w))
-> ((v -+> w) -> v -> w)
-> LinearFunction (Scalar w) (v -+> w) (v -+> w)
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 -+$> :: LinearFunction s v w -> v -> w
-+$> v
v = v -> w
f v
v