{-# LANGUAGE DataKinds #-}
{-# LANGUAGE ExistentialQuantification #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE NoStarIsType #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}

-----------------------------------------------------------------------------
{-|
Module      : Math.Tensor.Basic.Delta
Description : Definitions of Kronecker deltas.
Copyright   : (c) Nils Alex, 2020
License     : MIT
Maintainer  : nils.alex@fau.de

Definitions of Kronecker deltas \(\delta^{a}_{\hphantom ab}\)
(identity automorphisms) for arbitrary vector spaces.
-}
-----------------------------------------------------------------------------
module Math.Tensor.Basic.Delta
  ( -- * Kronecker delta
    delta
  , delta'
  , someDelta
  ) where

import Math.Tensor
import Math.Tensor.Safe
import Math.Tensor.Safe.TH
import Math.Tensor.Basic.TH

import Data.Singletons
  ( Sing
  , SingI (sing)
  , Demote
  , withSomeSing
  )
import Data.Singletons.Prelude
import Data.Singletons.Decide
  ( (:~:) (Refl)
  , Decision (Proved)
  , (%~)
  )
import Data.Singletons.TypeLits
  ( Symbol
  , Nat
  , KnownNat
  , withKnownNat
  , natVal
  , withKnownSymbol
  )

import Data.List.NonEmpty (NonEmpty ((:|)))

-- |The Kronecker delta \(\delta^a_{\hphantom ab} \) for a given
-- @'VSpace' id n@ with contravariant
-- index label @a@ and covariant index label @b@. Labels and dimension
-- are passed explicitly as singletons.
delta' :: forall (id :: Symbol) (n :: Nat) (a :: Symbol) (b :: Symbol) (r :: Rank) v.
          (
           KnownNat n,
           Num v,
           '[ '( 'VSpace id n, 'ConCov (a ':| '[]) (b ':| '[])) ] ~ r,
           TailR (TailR r) ~ '[],
           Sane (TailR r) ~ 'True
          ) =>
          Sing id -> Sing n -> Sing a -> Sing b ->
          Tensor r v
delta' :: Sing id -> Sing n -> Sing a -> Sing b -> Tensor r v
delta' Sing id
_ Sing n
_ Sing a
_ Sing b
_ = Tensor r v
forall (id :: Symbol) (n :: Nat) (a :: Symbol) (b :: Symbol)
       (r :: Rank) v.
('[ '( 'VSpace id n, 'ConCov (a ':| '[]) (b ':| '[]))] ~ r,
 TailR (TailR r) ~ '[], Sane (TailR r) ~ 'True, SingI n, Num v) =>
Tensor r v
delta

-- |The Kronecker delta \(\delta^a_{\hphantom ab} \) for a given
-- @'VSpace' id n@ with contravariant
-- index label @a@ and covariant index label @b@.
delta :: forall (id :: Symbol) (n :: Nat) (a :: Symbol) (b :: Symbol) (r :: Rank) v.
         (
          '[ '( 'VSpace id n, 'ConCov (a ':| '[]) (b ':| '[]))] ~ r,
          TailR (TailR r) ~ '[],
          Sane (TailR r) ~ 'True,
          SingI n,
          Num v
         ) => Tensor r v
delta :: Tensor r v
delta = case (Sing n
forall k (a :: k). SingI a => Sing a
sing :: Sing n) of
          Sing n
sn -> let x :: Int
x = Natural -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Natural -> Int) -> Natural -> Int
forall a b. (a -> b) -> a -> b
$ Sing n -> (KnownNat n => Natural) -> Natural
forall (n :: Nat) r. Sing n -> (KnownNat n => r) -> r
withKnownNat Sing n
sn ((KnownNat n => Natural) -> Natural)
-> (KnownNat n => Natural) -> Natural
forall a b. (a -> b) -> a -> b
$ SNat n -> Natural
forall (n :: Nat) (proxy :: Nat -> Type).
KnownNat n =>
proxy n -> Natural
natVal SNat n
Sing n
sn
                in [(Int,
  Tensor
    (Case_6989586621679113865
       ('VSpace id n)
       ('ConCov (a ':| '[]) (b ':| '[]))
       '[]
       (Case_6989586621679113828
          a
          b
          ('VSpace id n)
          ('ConCov (a ':| '[]) (b ':| '[]))
          '[]
          (CmpSymbol a b)))
    v)]
-> Tensor r v
forall (r :: Rank) (r' :: Rank) v.
(Sane r ~ 'True, TailR r ~ r') =>
[(Int, Tensor r' v)] -> Tensor r v
Tensor (Int -> [(Int, Tensor (TailR r) v)]
f Int
x)
  where
    f :: Int -> [(Int, Tensor (TailR r) v)]
    f :: Int -> [(Int, Tensor (TailR r) v)]
f Int
x = (Int
 -> (Int,
     Tensor
       (Case_6989586621679113865
          ('VSpace id n)
          ('ConCov (a ':| '[]) (b ':| '[]))
          '[]
          (Case_6989586621679113828
             a
             b
             ('VSpace id n)
             ('ConCov (a ':| '[]) (b ':| '[]))
             '[]
             (CmpSymbol a b)))
       v))
-> [Int]
-> [(Int,
     Tensor
       (Case_6989586621679113865
          ('VSpace id n)
          ('ConCov (a ':| '[]) (b ':| '[]))
          '[]
          (Case_6989586621679113828
             a
             b
             ('VSpace id n)
             ('ConCov (a ':| '[]) (b ':| '[]))
             '[]
             (CmpSymbol a b)))
       v)]
forall a b. (a -> b) -> [a] -> [b]
map (\Int
i -> (Int
i, [(Int, Tensor '[] v)]
-> Tensor
     (Case_6989586621679113865
        ('VSpace id n)
        ('ConCov (a ':| '[]) (b ':| '[]))
        '[]
        (Case_6989586621679113828
           a
           b
           ('VSpace id n)
           ('ConCov (a ':| '[]) (b ':| '[]))
           '[]
           (CmpSymbol a b)))
     v
forall (r :: Rank) (r' :: Rank) v.
(Sane r ~ 'True, TailR r ~ r') =>
[(Int, Tensor r' v)] -> Tensor r v
Tensor [(Int
i, v -> Tensor '[] v
forall v. v -> Tensor '[] v
Scalar v
1)])) [Int
0..Int
x Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1]

-- |The Kronecker delta \(\delta^a_{\hphantom ab} \) for a given
-- @'VSpace' id n@ with contravariant
-- index label @a@ and covariant index label @b@. Labels and dimension
-- are passed as values. Result is existentially quantified.
someDelta :: Num v =>
             Demote Symbol -> Demote Nat -> Demote Symbol -> Demote Symbol ->
             T v
someDelta :: Demote Symbol
-> Demote Nat -> Demote Symbol -> Demote Symbol -> T v
someDelta Demote Symbol
vid Demote Nat
vdim Demote Symbol
a Demote Symbol
b =
  Demote Symbol -> (forall (a :: Symbol). Sing a -> T v) -> T v
forall k r.
SingKind k =>
Demote k -> (forall (a :: k). Sing a -> r) -> r
withSomeSing Demote Symbol
vid ((forall (a :: Symbol). Sing a -> T v) -> T v)
-> (forall (a :: Symbol). Sing a -> T v) -> T v
forall a b. (a -> b) -> a -> b
$ \Sing a
svid ->
  Demote Nat -> (forall (a :: Nat). Sing a -> T v) -> T v
forall k r.
SingKind k =>
Demote k -> (forall (a :: k). Sing a -> r) -> r
withSomeSing Demote Nat
vdim ((forall (a :: Nat). Sing a -> T v) -> T v)
-> (forall (a :: Nat). Sing a -> T v) -> T v
forall a b. (a -> b) -> a -> b
$ \Sing a
svdim ->
  Demote Symbol -> (forall (a :: Symbol). Sing a -> T v) -> T v
forall k r.
SingKind k =>
Demote k -> (forall (a :: k). Sing a -> r) -> r
withSomeSing Demote Symbol
a ((forall (a :: Symbol). Sing a -> T v) -> T v)
-> (forall (a :: Symbol). Sing a -> T v) -> T v
forall a b. (a -> b) -> a -> b
$ \Sing a
sa ->
  Demote Symbol -> (forall (a :: Symbol). Sing a -> T v) -> T v
forall k r.
SingKind k =>
Demote k -> (forall (a :: k). Sing a -> r) -> r
withSomeSing Demote Symbol
b ((forall (a :: Symbol). Sing a -> T v) -> T v)
-> (forall (a :: Symbol). Sing a -> T v) -> T v
forall a b. (a -> b) -> a -> b
$ \Sing a
sb ->
  Sing a -> (KnownNat a => T v) -> T v
forall (n :: Nat) r. Sing n -> (KnownNat n => r) -> r
withKnownNat Sing a
svdim ((KnownNat a => T v) -> T v) -> (KnownNat a => T v) -> T v
forall a b. (a -> b) -> a -> b
$
  Sing a -> (KnownSymbol a => T v) -> T v
forall (n :: Symbol) r. Sing n -> (KnownSymbol n => r) -> r
withKnownSymbol Sing a
svid ((KnownSymbol a => T v) -> T v) -> (KnownSymbol a => T v) -> T v
forall a b. (a -> b) -> a -> b
$
  Sing a -> (KnownSymbol a => T v) -> T v
forall (n :: Symbol) r. Sing n -> (KnownSymbol n => r) -> r
withKnownSymbol Sing a
sa ((KnownSymbol a => T v) -> T v) -> (KnownSymbol a => T v) -> T v
forall a b. (a -> b) -> a -> b
$
  Sing a -> (KnownSymbol a => T v) -> T v
forall (n :: Symbol) r. Sing n -> (KnownSymbol n => r) -> r
withKnownSymbol Sing a
sb ((KnownSymbol a => T v) -> T v) -> (KnownSymbol a => T v) -> T v
forall a b. (a -> b) -> a -> b
$
  let sl :: Sing (Apply (Apply (Apply (Apply DeltaRankSym0 a) a) a) a)
sl = Sing a
-> Sing a
-> Sing a
-> Sing a
-> Sing (Apply (Apply (Apply (Apply DeltaRankSym0 a) a) a) a)
forall (t1 :: Symbol) (t2 :: Nat) (t3 :: Symbol) (t4 :: Symbol).
Sing t1
-> Sing t2
-> Sing t3
-> Sing t4
-> Sing (Apply (Apply (Apply (Apply DeltaRankSym0 t1) t2) t3) t4)
sDeltaRank Sing a
svid Sing a
svdim Sing a
sa Sing a
sb
  in  case Sing
  (Case_6989586621679113865
     ('VSpace a a)
     ('ConCov (a ':| '[]) (a ':| '[]))
     '[]
     (Case_6989586621679113828
        a
        a
        ('VSpace a a)
        ('ConCov (a ':| '[]) (a ':| '[]))
        '[]
        (CmpSymbol a a)))
-> Sing
     (Apply
        TailRSym0
        (Case_6989586621679113865
           ('VSpace a a)
           ('ConCov (a ':| '[]) (a ':| '[]))
           '[]
           (Case_6989586621679113828
              a
              a
              ('VSpace a a)
              ('ConCov (a ':| '[]) (a ':| '[]))
              '[]
              (CmpSymbol a a))))
forall s n (t :: [(VSpace s n, IList s)]).
SOrd s =>
Sing t -> Sing (Apply TailRSym0 t)
sTailR (Sing '[ '( 'VSpace a a, 'ConCov (a ':| '[]) (a ':| '[]))]
-> Sing
     (Apply
        TailRSym0 '[ '( 'VSpace a a, 'ConCov (a ':| '[]) (a ':| '[]))])
forall s n (t :: [(VSpace s n, IList s)]).
SOrd s =>
Sing t -> Sing (Apply TailRSym0 t)
sTailR Sing '[ '( 'VSpace a a, 'ConCov (a ':| '[]) (a ':| '[]))]
Sing (Apply (Apply (Apply (Apply DeltaRankSym0 a) a) a) a)
sl) of
        Sing
  (Apply
     TailRSym0
     (Case_6989586621679113865
        ('VSpace a a)
        ('ConCov (a ':| '[]) (a ':| '[]))
        '[]
        (Case_6989586621679113828
           a
           a
           ('VSpace a a)
           ('ConCov (a ':| '[]) (a ':| '[]))
           '[]
           (CmpSymbol a a))))
SNil -> case Sing
  (Case_6989586621679113865
     ('VSpace a a)
     ('ConCov (a ':| '[]) (a ':| '[]))
     '[]
     (Case_6989586621679113828
        a
        a
        ('VSpace a a)
        ('ConCov (a ':| '[]) (a ':| '[]))
        '[]
        (CmpSymbol a a)))
-> Sing
     (Apply
        SaneSym0
        (Case_6989586621679113865
           ('VSpace a a)
           ('ConCov (a ':| '[]) (a ':| '[]))
           '[]
           (Case_6989586621679113828
              a
              a
              ('VSpace a a)
              ('ConCov (a ':| '[]) (a ':| '[]))
              '[]
              (CmpSymbol a a))))
forall a b (t :: [(VSpace a b, IList a)]).
(SOrd a, SOrd b) =>
Sing t -> Sing (Apply SaneSym0 t)
sSane (Sing '[ '( 'VSpace a a, 'ConCov (a ':| '[]) (a ':| '[]))]
-> Sing
     (Apply
        TailRSym0 '[ '( 'VSpace a a, 'ConCov (a ':| '[]) (a ':| '[]))])
forall s n (t :: [(VSpace s n, IList s)]).
SOrd s =>
Sing t -> Sing (Apply TailRSym0 t)
sTailR Sing '[ '( 'VSpace a a, 'ConCov (a ':| '[]) (a ':| '[]))]
Sing (Apply (Apply (Apply (Apply DeltaRankSym0 a) a) a) a)
sl) Sing
  (Sane
     (Case_6989586621679113865
        ('VSpace a a)
        ('ConCov (a ':| '[]) (a ':| '[]))
        '[]
        (Case_6989586621679113828
           a
           a
           ('VSpace a a)
           ('ConCov (a ':| '[]) (a ':| '[]))
           '[]
           (CmpSymbol a a))))
-> Sing 'True
-> Decision
     (Sane
        (Case_6989586621679113865
           ('VSpace a a)
           ('ConCov (a ':| '[]) (a ':| '[]))
           '[]
           (Case_6989586621679113828
              a
              a
              ('VSpace a a)
              ('ConCov (a ':| '[]) (a ':| '[]))
              '[]
              (CmpSymbol a a)))
      :~: 'True)
forall k (a :: k) (b :: k).
SDecide k =>
Sing a -> Sing b -> Decision (a :~: b)
%~ SBool 'True
Sing 'True
STrue of
                  Proved Sane
  (Case_6989586621679113865
     ('VSpace a a)
     ('ConCov (a ':| '[]) (a ':| '[]))
     '[]
     (Case_6989586621679113828
        a
        a
        ('VSpace a a)
        ('ConCov (a ':| '[]) (a ':| '[]))
        '[]
        (CmpSymbol a a)))
:~: 'True
Refl -> Tensor '[ '( 'VSpace a a, 'ConCov (a ':| '[]) (a ':| '[]))] v
-> T v
forall (r :: Rank) v. SingI r => Tensor r v -> T v
T (Tensor '[ '( 'VSpace a a, 'ConCov (a ':| '[]) (a ':| '[]))] v
 -> T v)
-> Tensor '[ '( 'VSpace a a, 'ConCov (a ':| '[]) (a ':| '[]))] v
-> T v
forall a b. (a -> b) -> a -> b
$ Sing a
-> Sing a
-> Sing a
-> Sing a
-> Tensor '[ '( 'VSpace a a, 'ConCov (a ':| '[]) (a ':| '[]))] v
forall (id :: Symbol) (n :: Nat) (a :: Symbol) (b :: Symbol)
       (r :: Rank) v.
(KnownNat n, Num v,
 '[ '( 'VSpace id n, 'ConCov (a ':| '[]) (b ':| '[]))] ~ r,
 TailR (TailR r) ~ '[], Sane (TailR r) ~ 'True) =>
Sing id -> Sing n -> Sing a -> Sing b -> Tensor r v
delta' Sing a
svid Sing a
svdim Sing a
sa Sing a
sb