{-# LANGUAGE NoImplicitPrelude #-}

{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE StandaloneDeriving, GeneralizedNewtypeDeriving #-}
{-# LANGUAGE DefaultSignatures #-}

-- |

-- Module      : OAlg.Hom.Vectorial

-- Description : homomorphisms between vectorial structures

-- Copyright   : (c) Erich Gut

-- License     : BSD3

-- Maintainer  : zerich.gut@gmail.com

--

-- homomorphisms between 'Vectorial' structures having the same associated 'Scalar'.

module OAlg.Hom.Vectorial
  (
    -- * Vectorial

    HomVectorial, DualisableVectorial

    -- * Proposition

  , prpHomVectorial, prpDualisableVectorial
  , prpHomDisjOpVecZ
  )
  where

import Data.Kind

import OAlg.Prelude

import OAlg.Category.Path
import OAlg.Category.Dualisable
import OAlg.Category.SDuality
import OAlg.Category.Unify

import OAlg.Structure.Oriented hiding (Path(..))
import OAlg.Structure.Fibred
import OAlg.Structure.FibredOriented
import OAlg.Structure.Additive
import OAlg.Structure.Vectorial

import OAlg.Hom.Definition
import OAlg.Hom.Fibred
import OAlg.Hom.Additive

--------------------------------------------------------------------------------

-- HomVectorial -


-- | type family of homomorphisms between 'Vectorial' structures having the same associated 'Scalar.

--

-- __Property__ Let @__h__@ be a type instance of the class @'HomVectorial' __k__@, then

-- for all @__a__@, @__b__@, @v@ in @__h__ __a__ __b__@ and @x@ in @__k__@ holds:

-- @'amap' h (x '!' v) '==' x '!' 'amap' h v@.

class (HomAdditive h, Transformable (ObjectClass h) (Vec k)) => HomVectorial k h


instance HomVectorial k h => HomVectorial k (Path h)


--------------------------------------------------------------------------------

-- prpHomVectorial -


relHomVectorial :: HomVectorial k h
  => Homomorphous (Vec k) x y -> h x y -> k -> x -> Statement
relHomVectorial :: forall k (h :: * -> * -> *) x y.
HomVectorial k h =>
Homomorphous (Vec k) x y -> h x y -> k -> x -> Statement
relHomVectorial (Struct (Vec k) x
Struct :>: Struct (Vec k) y
Struct) h x y
h k
k x
x
  = (h x y -> x -> y
forall (h :: * -> * -> *) x y. Applicative h => h x y -> x -> y
amap h x y
h (k
Scalar x
k Scalar x -> x -> x
forall v. Vectorial v => Scalar v -> v -> v
! x
x) y -> y -> Bool
forall a. Eq a => a -> a -> Bool
== k
Scalar y
k Scalar y -> y -> y
forall v. Vectorial v => Scalar v -> v -> v
! h x y -> x -> y
forall (h :: * -> * -> *) x y. Applicative h => h x y -> x -> y
amap h x y
h x
x) Bool -> Message -> Statement
:?> [Parameter] -> Message
Params [String
"k"String -> String -> Parameter
:=k -> String
forall a. Show a => a -> String
show k
k, String
"x"String -> String -> Parameter
:=x -> String
forall a. Show a => a -> String
show x
x]

-- | validity according to 'HomVectorial'.

prpHomVectorial :: HomVectorial k h
  => h x y -> k -> x -> Statement
prpHomVectorial :: forall k (h :: * -> * -> *) x y.
HomVectorial k h =>
h x y -> k -> x -> Statement
prpHomVectorial h x y
h k
k x
x = String -> Label
Prp String
"HomVectorial"
  Label -> Statement -> Statement
:<=>: Homomorphous (Vec k) x y -> h x y -> k -> x -> Statement
forall k (h :: * -> * -> *) x y.
HomVectorial k h =>
Homomorphous (Vec k) x y -> h x y -> k -> x -> Statement
relHomVectorial (Homomorphous (ObjectClass h) x y -> Homomorphous (Vec k) x y
forall s t x y.
Transformable s t =>
Homomorphous s x y -> Homomorphous t x y
tauHom (h x y -> Homomorphous (ObjectClass h) x y
forall x y. h x y -> Homomorphous (ObjectClass h) x y
forall (m :: * -> * -> *) x y.
Morphism m =>
m x y -> Homomorphous (ObjectClass m) x y
homomorphous h x y
h)) h x y
h k
k x
x
  
--------------------------------------------------------------------------------

-- DualisableVectorial -


-- | duality according to @__o__@ on @__k__@-'Vectorial' structures.

--

-- __Propoerty__ Let @'DualisableVectorial' __k s o__@ then for all @__x__@, @s@ in @'Struct' __s x__@

-- and @k@ in @__k__@ holds:

--

-- (1) @'toDualStk' q s (k '!' x) '==' k '!' toDualStk q s x@.

--

-- where @q@ is any proxy for @__o__@.

class (DualisableAdditive s o, Transformable s (Vec k)) => DualisableVectorial k s o

instance (HomVectorial k h, DualisableVectorial k s o) => HomVectorial k (HomDisj s o h)

--------------------------------------------------------------------------------

-- relDualisableVectorial -


relDualisableVectorial :: DualisableVectorial k s o
  => q o -> Struct s x -> Struct (Vec k) x -> Struct (Vec k) (o x) -> k -> x -> Statement
relDualisableVectorial :: forall k s (o :: * -> *) (q :: (* -> *) -> *) x.
DualisableVectorial k s o =>
q o
-> Struct s x
-> Struct (Vec k) x
-> Struct (Vec k) (o x)
-> k
-> x
-> Statement
relDualisableVectorial q o
q Struct s x
s Struct (Vec k) x
Struct Struct (Vec k) (o x)
Struct k
k x
x
  = (q o -> Struct s x -> x -> o x
forall s (o :: * -> *) (q :: (* -> *) -> *) x.
DualisableFibred s o =>
q o -> Struct s x -> x -> o x
toDualStk q o
q Struct s x
s (k
Scalar x
k Scalar x -> x -> x
forall v. Vectorial v => Scalar v -> v -> v
! x
x) o x -> o x -> Bool
forall a. Eq a => a -> a -> Bool
== k
Scalar (o x)
k Scalar (o x) -> o x -> o x
forall v. Vectorial v => Scalar v -> v -> v
! q o -> Struct s x -> x -> o x
forall s (o :: * -> *) (q :: (* -> *) -> *) x.
DualisableFibred s o =>
q o -> Struct s x -> x -> o x
toDualStk q o
q Struct s x
s x
x) Bool -> Message -> Statement
:?> [Parameter] -> Message
Params [String
"k"String -> String -> Parameter
:=k -> String
forall a. Show a => a -> String
show k
k, String
"x"String -> String -> Parameter
:=x -> String
forall a. Show a => a -> String
show x
x]

-- | validity according to 'DualisableVectorial'.

prpDualisableVectorial :: DualisableVectorial k s o
  => q o -> Struct s x -> k -> x -> Statement
prpDualisableVectorial :: forall k s (o :: * -> *) (q :: (* -> *) -> *) x.
DualisableVectorial k s o =>
q o -> Struct s x -> k -> x -> Statement
prpDualisableVectorial q o
q Struct s x
s k
k x
x = String -> Label
Prp String
"DualisableVectorial"
  Label -> Statement -> Statement
:<=>: q o
-> Struct s x
-> Struct (Vec k) x
-> Struct (Vec k) (o x)
-> k
-> x
-> Statement
forall k s (o :: * -> *) (q :: (* -> *) -> *) x.
DualisableVectorial k s o =>
q o
-> Struct s x
-> Struct (Vec k) x
-> Struct (Vec k) (o x)
-> k
-> x
-> Statement
relDualisableVectorial q o
q Struct s x
s (Struct s x -> Struct (Vec k) x
forall x. Struct s x -> Struct (Vec k) x
forall s t x. Transformable s t => Struct s x -> Struct t x
tau Struct s x
s) (Struct s (o x) -> Struct (Vec k) (o x)
forall x. Struct s x -> Struct (Vec k) x
forall s t x. Transformable s t => Struct s x -> Struct t x
tau (Struct s x -> Struct s (o x)
forall (o :: * -> *) s x.
Transformable1 o s =>
Struct s x -> Struct s (o x)
tauO Struct s x
s)) k
k x
x

--------------------------------------------------------------------------------

-- VecX -


-- | type index for @__k__@-'Vectorial' structures @__x__@ having also standard random variables for

-- @__k__@ and @__x__@.

data VecX k

type instance Structure (VecX k) x
  = (Vectorial x, Scalar x ~ k, FibredOriented x, XStandard k, XStandard x)

instance HomVectorial k (HomEmpty (VecX k))

instance Transformable (VecX k) Fbr where tau :: forall x. Struct (VecX k) x -> Struct Fbr x
tau Struct (VecX k) x
Struct = Struct Fbr x
forall s x. Structure s x => Struct s x
Struct
instance TransformableFbr (VecX k)

instance Transformable (VecX k) Add where tau :: forall x. Struct (VecX k) x -> Struct Add x
tau Struct (VecX k) x
Struct = Struct Add x
forall s x. Structure s x => Struct s x
Struct
instance TransformableAdd (VecX k)

instance Transformable (VecX k) (Vec k) where tau :: forall x. Struct (VecX k) x -> Struct (Vec k) x
tau Struct (VecX k) x
Struct = Struct (Vec k) x
forall s x. Structure s x => Struct s x
Struct

instance Transformable (VecX k) Ort where tau :: forall x. Struct (VecX k) x -> Struct Ort x
tau Struct (VecX k) x
Struct = Struct Ort x
forall s x. Structure s x => Struct s x
Struct
instance TransformableOrt (VecX k)

instance Transformable (VecX k) FbrOrt where tau :: forall x. Struct (VecX k) x -> Struct FbrOrt x
tau Struct (VecX k) x
Struct = Struct FbrOrt x
forall s x. Structure s x => Struct s x
Struct
instance TransformableFbrOrt (VecX k)

instance TransformableG Op (VecX k) (VecX k) where tauG :: forall x. Struct (VecX k) x -> Struct (VecX k) (Op x)
tauG Struct (VecX k) x
Struct = Struct (VecX k) (Op x)
forall s x. Structure s x => Struct s x
Struct 
instance TransformableOp (VecX k)
instance DualisableVectorial k (VecX k) Op

instance Transformable (VecX k) Type where tau :: forall x. Struct (VecX k) x -> Struct (*) x
tau Struct (VecX k) x
_ = Struct (*) x
forall s x. Structure s x => Struct s x
Struct
instance TransformableType (VecX k)

instance Transformable (VecX k) Typ where tau :: forall x. Struct (VecX k) x -> Struct Typ x
tau Struct (VecX k) x
Struct = Struct Typ x
forall s x. Structure s x => Struct s x
Struct

relHomDisjOpVecZStruct :: HomVectorial Z h
  => Homomorphous (VecX Z) x y -> h x y -> Statement
relHomDisjOpVecZStruct :: forall (h :: * -> * -> *) x y.
HomVectorial Z h =>
Homomorphous (VecX Z) x y -> h x y -> Statement
relHomDisjOpVecZStruct (sx :: Struct (VecX Z) x
sx@Struct (VecX Z) x
Struct :>: Struct (VecX Z) y
Struct) h x y
h= X (Z, x) -> ((Z, x) -> Statement) -> Statement
forall x. X x -> (x -> Statement) -> Statement
Forall (Struct (VecX Z) x -> X (Z, x)
forall k x. Struct (VecX k) x -> X (k, x)
xkx Struct (VecX Z) x
sx) (\(Z
k,x
x) -> h x y -> Z -> x -> Statement
forall k (h :: * -> * -> *) x y.
HomVectorial k h =>
h x y -> k -> x -> Statement
prpHomVectorial h x y
h Z
k x
x)
  where
    xkx :: Struct (VecX k) x -> X (k,x)
    xkx :: forall k x. Struct (VecX k) x -> X (k, x)
xkx Struct (VecX k) x
Struct = X k -> X x -> X (k, x)
forall a b. X a -> X b -> X (a, b)
xTupple2 X k
forall x. XStandard x => X x
xStandard X x
forall x. XStandard x => X x
xStandard 
                                                 

relHomDisjOpVecZ :: X (SomeMorphism (HomDisjEmpty (VecX Z) Op)) -> Statement
relHomDisjOpVecZ :: X (SomeMorphism (HomDisjEmpty (VecX Z) Op)) -> Statement
relHomDisjOpVecZ X (SomeMorphism (HomDisjEmpty (VecX Z) Op))
xsh = X (SomeMorphism (HomDisjEmpty (VecX Z) Op))
-> (SomeMorphism (HomDisjEmpty (VecX Z) Op) -> Statement)
-> Statement
forall x. X x -> (x -> Statement) -> Statement
Forall X (SomeMorphism (HomDisjEmpty (VecX Z) Op))
xsh
  (\(SomeMorphism HomDisjEmpty (VecX Z) Op x y
h) -> Homomorphous (VecX Z) x y
-> HomDisjEmpty (VecX Z) Op x y -> Statement
forall (h :: * -> * -> *) x y.
HomVectorial Z h =>
Homomorphous (VecX Z) x y -> h x y -> Statement
relHomDisjOpVecZStruct (Homomorphous (VecX Z) x y -> Homomorphous (VecX Z) x y
forall s t x y.
Transformable s t =>
Homomorphous s x y -> Homomorphous t x y
tauHom (HomDisjEmpty (VecX Z) Op x y
-> Homomorphous (ObjectClass (HomDisjEmpty (VecX Z) Op)) x y
forall x y.
HomDisj (VecX Z) Op (HomEmpty (VecX Z)) x y
-> Homomorphous (ObjectClass (HomDisjEmpty (VecX Z) Op)) x y
forall (m :: * -> * -> *) x y.
Morphism m =>
m x y -> Homomorphous (ObjectClass m) x y
homomorphous HomDisjEmpty (VecX Z) Op x y
h)) HomDisjEmpty (VecX Z) Op x y
h)

-- | validity of 'HomDisjEmpty' __('Vec' 'Z') 'Op'@ according to 'HomVectorial'. 

prpHomDisjOpVecZ :: Statement
prpHomDisjOpVecZ :: Statement
prpHomDisjOpVecZ = String -> Label
Prp String
"HomDisjOpVecZ" Label -> Statement -> Statement
:<=>: X (SomeMorphism (HomDisjEmpty (VecX Z) Op)) -> Statement
relHomDisjOpVecZ X (SomeMorphism (HomDisjEmpty (VecX Z) Op))
xsh where
  xsh :: X (SomeMorphism (HomDisjEmpty (VecX Z) Op))
  xsh :: X (SomeMorphism (HomDisjEmpty (VecX Z) Op))
xsh = (SomeCmpb2 (HomDisjEmpty (VecX Z) Op)
 -> SomeMorphism (HomDisjEmpty (VecX Z) Op))
-> X (SomeCmpb2 (HomDisjEmpty (VecX Z) Op))
-> X (SomeMorphism (HomDisjEmpty (VecX Z) Op))
forall (h :: * -> * -> *) (f :: * -> *) x y.
Applicative1 h f =>
h x y -> f x -> f y
amap1 SomeCmpb2 (HomDisjEmpty (VecX Z) Op)
-> SomeMorphism (HomDisjEmpty (VecX Z) Op)
forall (h :: * -> * -> *).
Category h =>
SomeCmpb2 h -> SomeMorphism h
smCmpb2 (X (SomeCmpb2 (HomDisjEmpty (VecX Z) Op))
 -> X (SomeMorphism (HomDisjEmpty (VecX Z) Op)))
-> X (SomeCmpb2 (HomDisjEmpty (VecX Z) Op))
-> X (SomeMorphism (HomDisjEmpty (VecX Z) Op))
forall (h :: * -> * -> *) x y. Applicative h => h x y -> x -> y
$ X (SomeObjectClass (SHom (VecX Z) (VecX Z) Op (HomEmpty (VecX Z))))
-> X (SomeMorphism (HomEmpty (VecX Z)))
-> X (SomeCmpb2 (HomDisjEmpty (VecX Z) Op))
forall (o :: * -> *) s (h :: * -> * -> *).
(TransformableG o s s, Morphism h,
 Transformable (ObjectClass h) s) =>
X (SomeObjectClass (SHom s s o h))
-> X (SomeMorphism h) -> X (SomeCmpb2 (HomDisj s o h))
xscmHomDisj X (SomeObjectClass (SHom (VecX Z) (VecX Z) Op (HomEmpty (VecX Z))))
forall s.
(s ~ VecX Z) =>
X (SomeObjectClass (SHom s s Op (HomEmpty s)))
xsoVecXZ X (SomeMorphism (HomEmpty (VecX Z)))
forall x. X x
XEmpty

--------------------------------------------------------------------------------

-- xsoVecXZ -


xsoVecXZ :: s ~ VecX Z => X (SomeObjectClass (SHom s s Op (HomEmpty s)))
xsoVecXZ :: forall s.
(s ~ VecX Z) =>
X (SomeObjectClass (SHom s s Op (HomEmpty s)))
xsoVecXZ = [SomeObjectClass (SHom s s Op (HomEmpty s))]
-> X (SomeObjectClass (SHom s s Op (HomEmpty s)))
forall a. [a] -> X a
xOneOf [ Struct (ObjectClass (SHom s s Op (HomEmpty s))) (ZVec Z)
-> SomeObjectClass (SHom s s Op (HomEmpty s))
forall (m :: * -> * -> *) x.
Transformable (ObjectClass m) Typ =>
Struct (ObjectClass m) x -> SomeObjectClass m
SomeObjectClass (Struct (VecX Z) (ZVec Z)
forall s x. Structure s x => Struct s x
Struct :: Struct (VecX Z) (ZVec Z))
                  , Struct (ObjectClass (SHom s s Op (HomEmpty s))) (ZVec Q)
-> SomeObjectClass (SHom s s Op (HomEmpty s))
forall (m :: * -> * -> *) x.
Transformable (ObjectClass m) Typ =>
Struct (ObjectClass m) x -> SomeObjectClass m
SomeObjectClass (Struct (VecX Z) (ZVec Q)
forall s x. Structure s x => Struct s x
Struct :: Struct (VecX Z) (ZVec Q))
                  , Struct (ObjectClass (SHom s s Op (HomEmpty s))) (ZVec OS)
-> SomeObjectClass (SHom s s Op (HomEmpty s))
forall (m :: * -> * -> *) x.
Transformable (ObjectClass m) Typ =>
Struct (ObjectClass m) x -> SomeObjectClass m
SomeObjectClass (Struct (VecX Z) (ZVec OS)
forall s x. Structure s x => Struct s x
Struct :: Struct (VecX Z) (ZVec OS))
                  ]

--------------------------------------------------------------------------------

-- ZVec -


newtype ZVec x = ZVec x deriving (ZVec x -> ZVec x -> Bool
(ZVec x -> ZVec x -> Bool)
-> (ZVec x -> ZVec x -> Bool) -> Eq (ZVec x)
forall x. Eq x => ZVec x -> ZVec x -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: forall x. Eq x => ZVec x -> ZVec x -> Bool
== :: ZVec x -> ZVec x -> Bool
$c/= :: forall x. Eq x => ZVec x -> ZVec x -> Bool
/= :: ZVec x -> ZVec x -> Bool
Eq,Int -> ZVec x -> ShowS
[ZVec x] -> ShowS
ZVec x -> String
(Int -> ZVec x -> ShowS)
-> (ZVec x -> String) -> ([ZVec x] -> ShowS) -> Show (ZVec x)
forall x. Show x => Int -> ZVec x -> ShowS
forall x. Show x => [ZVec x] -> ShowS
forall x. Show x => ZVec x -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: forall x. Show x => Int -> ZVec x -> ShowS
showsPrec :: Int -> ZVec x -> ShowS
$cshow :: forall x. Show x => ZVec x -> String
show :: ZVec x -> String
$cshowList :: forall x. Show x => [ZVec x] -> ShowS
showList :: [ZVec x] -> ShowS
Show,ZVec x -> Statement
(ZVec x -> Statement) -> Validable (ZVec x)
forall x. Validable x => ZVec x -> Statement
forall a. (a -> Statement) -> Validable a
$cvalid :: forall x. Validable x => ZVec x -> Statement
valid :: ZVec x -> Statement
Validable)

instance XStandard x => XStandard (ZVec x) where xStandard :: X (ZVec x)
xStandard = (x -> ZVec x) -> X x -> X (ZVec x)
forall (h :: * -> * -> *) (f :: * -> *) x y.
Applicative1 h f =>
h x y -> f x -> f y
amap1 x -> ZVec x
forall x. x -> ZVec x
ZVec X x
forall x. XStandard x => X x
xStandard

type instance Point (ZVec x) = Point x
instance ShowPoint x => ShowPoint (ZVec x)
instance EqPoint x => EqPoint (ZVec x)
instance ValidablePoint x => ValidablePoint (ZVec x)
instance TypeablePoint x => TypeablePoint (ZVec x)

instance Oriented x => Oriented (ZVec x) where
  orientation :: ZVec x -> Orientation (Point (ZVec x))
orientation (ZVec x
x) = x -> Orientation (Point x)
forall q. Oriented q => q -> Orientation (Point q)
orientation x
x

type instance Root (ZVec x) = Root x
instance ShowRoot x => ShowRoot (ZVec x)
instance EqRoot x => EqRoot (ZVec x)
instance ValidableRoot x => ValidableRoot (ZVec x)
instance TypeableRoot x => TypeableRoot (ZVec x)

instance FibredOriented x => Fibred (ZVec x)
instance FibredOriented x => FibredOriented (ZVec x)

instance (Additive x, FibredOriented x) => Additive (ZVec x) where
  zero :: Root (ZVec x) -> ZVec x
zero Root (ZVec x)
r = x -> ZVec x
forall x. x -> ZVec x
ZVec (Root x -> x
forall a. Additive a => Root a -> a
zero Root x
Root (ZVec x)
r)
  ZVec x
a + :: ZVec x -> ZVec x -> ZVec x
+ ZVec x
b = x -> ZVec x
forall x. x -> ZVec x
ZVec (x
ax -> x -> x
forall a. Additive a => a -> a -> a
+x
b)
  ntimes :: N -> ZVec x -> ZVec x
ntimes N
n (ZVec x
a) = x -> ZVec x
forall x. x -> ZVec x
ZVec (N -> x -> x
forall a. Additive a => N -> a -> a
ntimes N
n x
a)

instance (Abelian x, FibredOriented x) => Abelian (ZVec x) where
  negate :: ZVec x -> ZVec x
negate (ZVec x
x) = x -> ZVec x
forall x. x -> ZVec x
ZVec (x -> x
forall a. Abelian a => a -> a
negate x
x)
  ZVec x
a - :: ZVec x -> ZVec x -> ZVec x
- ZVec x
b = x -> ZVec x
forall x. x -> ZVec x
ZVec (x
ax -> x -> x
forall a. Abelian a => a -> a -> a
-x
b)
  ztimes :: Z -> ZVec x -> ZVec x
ztimes Z
z (ZVec x
a) = x -> ZVec x
forall x. x -> ZVec x
ZVec (Z -> x -> x
forall a. Abelian a => Z -> a -> a
ztimes Z
z x
a)

instance (Abelian x, FibredOriented x) => Vectorial (ZVec x) where
  type Scalar (ZVec x) = Z
  ! :: Scalar (ZVec x) -> ZVec x -> ZVec x
(!) = Z -> ZVec x -> ZVec x
Scalar (ZVec x) -> ZVec x -> ZVec x
forall a. Abelian a => Z -> a -> a
ztimes