{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE DerivingVia #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE PatternSynonyms #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE ViewPatterns #-}

module Downhill.BVar
  ( BVar (..),
    var,
    constant,
    backprop,

    -- * Pattern synonyms
    pattern T2,
    pattern T3,
  )
where

import Data.AdditiveGroup (AdditiveGroup)
import Data.AffineSpace (AffineSpace ((.+^), (.-.)))
import qualified Data.AffineSpace as AffineSpace
import Data.VectorSpace
  ( AdditiveGroup (..),
    InnerSpace ((<.>)),
    VectorSpace (Scalar, (*^)),
  )
import Downhill.Grad
  ( Dual (evalGrad),
    HasGrad,
    HasGradAffine,
    HilbertSpace (coriesz, riesz),
    MScalar,
    Manifold (Grad, Tang),
  )
import Downhill.Linear.BackGrad
  ( BackGrad (..),
    realNode,
  )
import qualified Downhill.Linear.Backprop as BP
import Downhill.Linear.Expr (BasicVector (..), Expr (ExprVar))
import Downhill.Linear.Lift (lift1_dense, lift2_dense)
import qualified Downhill.Linear.Prelude as Linear
import Prelude hiding (id, (.))

-- | Variable is a value paired with derivative.
data BVar r a = BVar
  { forall r a. BVar r a -> a
bvarValue :: a,
    forall r a. BVar r a -> BackGrad r (Grad a)
bvarGrad :: BackGrad r (Grad a)
  }

instance (AdditiveGroup b, HasGrad b) => AdditiveGroup (BVar r b) where
  zeroV :: BVar r b
zeroV = forall r a. a -> BackGrad r (Grad a) -> BVar r a
BVar forall v. AdditiveGroup v => v
zeroV forall v. AdditiveGroup v => v
zeroV
  negateV :: BVar r b -> BVar r b
negateV (BVar b
y0 BackGrad r (Grad b)
dy) = forall r a. a -> BackGrad r (Grad a) -> BVar r a
BVar (forall v. AdditiveGroup v => v -> v
negateV b
y0) (forall v. AdditiveGroup v => v -> v
negateV BackGrad r (Grad b)
dy)
  BVar b
y0 BackGrad r (Grad b)
dy ^-^ :: BVar r b -> BVar r b -> BVar r b
^-^ BVar b
z0 BackGrad r (Grad b)
dz = forall r a. a -> BackGrad r (Grad a) -> BVar r a
BVar (b
y0 forall v. AdditiveGroup v => v -> v -> v
^-^ b
z0) (BackGrad r (Grad b)
dy forall v. AdditiveGroup v => v -> v -> v
^-^ BackGrad r (Grad b)
dz)
  BVar b
y0 BackGrad r (Grad b)
dy ^+^ :: BVar r b -> BVar r b -> BVar r b
^+^ BVar b
z0 BackGrad r (Grad b)
dz = forall r a. a -> BackGrad r (Grad a) -> BVar r a
BVar (b
y0 forall v. AdditiveGroup v => v -> v -> v
^+^ b
z0) (BackGrad r (Grad b)
dy forall v. AdditiveGroup v => v -> v -> v
^+^ BackGrad r (Grad b)
dz)

instance (Num b, HasGrad b, MScalar b ~ b) => Num (BVar r b) where
  (BVar b
f0 BackGrad r (Grad b)
df) + :: BVar r b -> BVar r b -> BVar r b
+ (BVar b
g0 BackGrad r (Grad b)
dg) = forall r a. a -> BackGrad r (Grad a) -> BVar r a
BVar (b
f0 forall a. Num a => a -> a -> a
+ b
g0) (BackGrad r (Grad b)
df forall v. AdditiveGroup v => v -> v -> v
^+^ BackGrad r (Grad b)
dg)
  (BVar b
f0 BackGrad r (Grad b)
df) - :: BVar r b -> BVar r b -> BVar r b
- (BVar b
g0 BackGrad r (Grad b)
dg) = forall r a. a -> BackGrad r (Grad a) -> BVar r a
BVar (b
f0 forall a. Num a => a -> a -> a
- b
g0) (BackGrad r (Grad b)
df forall v. AdditiveGroup v => v -> v -> v
^-^ BackGrad r (Grad b)
dg)
  (BVar b
f0 BackGrad r (Grad b)
df) * :: BVar r b -> BVar r b -> BVar r b
* (BVar b
g0 BackGrad r (Grad b)
dg) = forall r a. a -> BackGrad r (Grad a) -> BVar r a
BVar (b
f0 forall a. Num a => a -> a -> a
* b
g0) (b
f0 forall v. VectorSpace v => Scalar v -> v -> v
*^ BackGrad r (Grad b)
dg forall v. AdditiveGroup v => v -> v -> v
^+^ b
g0 forall v. VectorSpace v => Scalar v -> v -> v
*^ BackGrad r (Grad b)
df)
  negate :: BVar r b -> BVar r b
negate (BVar b
f0 BackGrad r (Grad b)
df) = forall r a. a -> BackGrad r (Grad a) -> BVar r a
BVar (forall a. Num a => a -> a
negate b
f0) (forall v. AdditiveGroup v => v -> v
negateV BackGrad r (Grad b)
df)
  abs :: BVar r b -> BVar r b
abs (BVar b
f0 BackGrad r (Grad b)
df) = forall r a. a -> BackGrad r (Grad a) -> BVar r a
BVar (forall a. Num a => a -> a
abs b
f0) (forall a. Num a => a -> a
signum b
f0 forall v. VectorSpace v => Scalar v -> v -> v
*^ BackGrad r (Grad b)
df) -- TODO: ineffiency: multiplication by 1
  signum :: BVar r b -> BVar r b
signum (BVar b
f0 BackGrad r (Grad b)
_) = forall r a. a -> BackGrad r (Grad a) -> BVar r a
BVar (forall a. Num a => a -> a
signum b
f0) forall v. AdditiveGroup v => v
zeroV
  fromInteger :: Integer -> BVar r b
fromInteger Integer
x = forall r a. a -> BackGrad r (Grad a) -> BVar r a
BVar (forall a. Num a => Integer -> a
fromInteger Integer
x) forall v. AdditiveGroup v => v
zeroV

sqr :: Num a => a -> a
sqr :: forall a. Num a => a -> a
sqr a
x = a
x forall a. Num a => a -> a -> a
* a
x

rsqrt :: Floating a => a -> a
rsqrt :: forall a. Floating a => a -> a
rsqrt a
x = forall a. Fractional a => a -> a
recip (forall a. Floating a => a -> a
sqrt a
x)

instance (Fractional b, HasGrad b, MScalar b ~ b) => Fractional (BVar r b) where
  fromRational :: Rational -> BVar r b
fromRational Rational
x = forall r a. a -> BackGrad r (Grad a) -> BVar r a
BVar (forall a. Fractional a => Rational -> a
fromRational Rational
x) forall v. AdditiveGroup v => v
zeroV
  recip :: BVar r b -> BVar r b
recip (BVar b
x BackGrad r (Grad b)
dx) = forall r a. a -> BackGrad r (Grad a) -> BVar r a
BVar (forall a. Fractional a => a -> a
recip b
x) (b
df forall v. VectorSpace v => Scalar v -> v -> v
*^ BackGrad r (Grad b)
dx)
    where
      df :: b
df = forall a. Num a => a -> a
negate (forall a. Fractional a => a -> a
recip (forall a. Num a => a -> a
sqr b
x))
  BVar b
x BackGrad r (Grad b)
dx / :: BVar r b -> BVar r b -> BVar r b
/ BVar b
y BackGrad r (Grad b)
dy = forall r a. a -> BackGrad r (Grad a) -> BVar r a
BVar (b
x forall a. Fractional a => a -> a -> a
/ b
y) ((forall a. Fractional a => a -> a
recip b
y forall v. VectorSpace v => Scalar v -> v -> v
*^ BackGrad r (Grad b)
dx) forall v. AdditiveGroup v => v -> v -> v
^-^ ((b
x forall a. Fractional a => a -> a -> a
/ forall a. Num a => a -> a
sqr b
y) forall v. VectorSpace v => Scalar v -> v -> v
*^ BackGrad r (Grad b)
dy))

instance (Floating b, HasGrad b, MScalar b ~ b) => Floating (BVar r b) where
  pi :: BVar r b
pi = forall r a. a -> BackGrad r (Grad a) -> BVar r a
BVar forall a. Floating a => a
pi forall v. AdditiveGroup v => v
zeroV
  exp :: BVar r b -> BVar r b
exp (BVar b
x BackGrad r (Grad b)
dx) = forall r a. a -> BackGrad r (Grad a) -> BVar r a
BVar (forall a. Floating a => a -> a
exp b
x) (forall a. Floating a => a -> a
exp b
x forall v. VectorSpace v => Scalar v -> v -> v
*^ BackGrad r (Grad b)
dx)
  log :: BVar r b -> BVar r b
log (BVar b
x BackGrad r (Grad b)
dx) = forall r a. a -> BackGrad r (Grad a) -> BVar r a
BVar (forall a. Floating a => a -> a
log b
x) (forall a. Fractional a => a -> a
recip b
x forall v. VectorSpace v => Scalar v -> v -> v
*^ BackGrad r (Grad b)
dx)
  sin :: BVar r b -> BVar r b
sin (BVar b
x BackGrad r (Grad b)
dx) = forall r a. a -> BackGrad r (Grad a) -> BVar r a
BVar (forall a. Floating a => a -> a
sin b
x) (forall a. Floating a => a -> a
cos b
x forall v. VectorSpace v => Scalar v -> v -> v
*^ BackGrad r (Grad b)
dx)
  cos :: BVar r b -> BVar r b
cos (BVar b
x BackGrad r (Grad b)
dx) = forall r a. a -> BackGrad r (Grad a) -> BVar r a
BVar (forall a. Floating a => a -> a
cos b
x) (forall a. Num a => a -> a
negate (forall a. Floating a => a -> a
sin b
x) forall v. VectorSpace v => Scalar v -> v -> v
*^ BackGrad r (Grad b)
dx)
  asin :: BVar r b -> BVar r b
asin (BVar b
x BackGrad r (Grad b)
dx) = forall r a. a -> BackGrad r (Grad a) -> BVar r a
BVar (forall a. Floating a => a -> a
asin b
x) (forall a. Floating a => a -> a
rsqrt (b
1 forall a. Num a => a -> a -> a
- forall a. Num a => a -> a
sqr b
x) forall v. VectorSpace v => Scalar v -> v -> v
*^ BackGrad r (Grad b)
dx)
  acos :: BVar r b -> BVar r b
acos (BVar b
x BackGrad r (Grad b)
dx) = forall r a. a -> BackGrad r (Grad a) -> BVar r a
BVar (forall a. Floating a => a -> a
acos b
x) (forall a. Num a => a -> a
negate (forall a. Floating a => a -> a
rsqrt (b
1 forall a. Num a => a -> a -> a
- forall a. Num a => a -> a
sqr b
x)) forall v. VectorSpace v => Scalar v -> v -> v
*^ BackGrad r (Grad b)
dx)
  atan :: BVar r b -> BVar r b
atan (BVar b
x BackGrad r (Grad b)
dx) = forall r a. a -> BackGrad r (Grad a) -> BVar r a
BVar (forall a. Floating a => a -> a
atan b
x) (forall a. Fractional a => a -> a
recip (b
1 forall a. Num a => a -> a -> a
+ forall a. Num a => a -> a
sqr b
x) forall v. VectorSpace v => Scalar v -> v -> v
*^ BackGrad r (Grad b)
dx)
  sinh :: BVar r b -> BVar r b
sinh (BVar b
x BackGrad r (Grad b)
dx) = forall r a. a -> BackGrad r (Grad a) -> BVar r a
BVar (forall a. Floating a => a -> a
sinh b
x) (forall a. Floating a => a -> a
cosh b
x forall v. VectorSpace v => Scalar v -> v -> v
*^ BackGrad r (Grad b)
dx)
  cosh :: BVar r b -> BVar r b
cosh (BVar b
x BackGrad r (Grad b)
dx) = forall r a. a -> BackGrad r (Grad a) -> BVar r a
BVar (forall a. Floating a => a -> a
cosh b
x) (forall a. Floating a => a -> a
sinh b
x forall v. VectorSpace v => Scalar v -> v -> v
*^ BackGrad r (Grad b)
dx)
  asinh :: BVar r b -> BVar r b
asinh (BVar b
x BackGrad r (Grad b)
dx) = forall r a. a -> BackGrad r (Grad a) -> BVar r a
BVar (forall a. Floating a => a -> a
asinh b
x) (forall a. Floating a => a -> a
rsqrt (b
1 forall a. Num a => a -> a -> a
+ forall a. Num a => a -> a
sqr b
x) forall v. VectorSpace v => Scalar v -> v -> v
*^ BackGrad r (Grad b)
dx)
  acosh :: BVar r b -> BVar r b
acosh (BVar b
x BackGrad r (Grad b)
dx) = forall r a. a -> BackGrad r (Grad a) -> BVar r a
BVar (forall a. Floating a => a -> a
acosh b
x) (forall a. Floating a => a -> a
rsqrt (forall a. Num a => a -> a
sqr b
x forall a. Num a => a -> a -> a
- b
1) forall v. VectorSpace v => Scalar v -> v -> v
*^ BackGrad r (Grad b)
dx)
  atanh :: BVar r b -> BVar r b
atanh (BVar b
x BackGrad r (Grad b)
dx) = forall r a. a -> BackGrad r (Grad a) -> BVar r a
BVar (forall a. Floating a => a -> a
atanh b
x) (forall a. Fractional a => a -> a
recip (b
1 forall a. Num a => a -> a -> a
- forall a. Num a => a -> a
sqr b
x) forall v. VectorSpace v => Scalar v -> v -> v
*^ BackGrad r (Grad b)
dx)

instance
  ( VectorSpace v,
    HasGrad v,
    Tang v ~ v,
    HasGrad (MScalar v),
    Grad (Scalar v) ~ Scalar v
  ) =>
  VectorSpace (BVar r v)
  where
  type Scalar (BVar r v) = BVar r (MScalar v)
  BVar Scalar (Grad v)
a BackGrad r (Grad (Scalar (Grad v)))
da *^ :: Scalar (BVar r v) -> BVar r v -> BVar r v
*^ BVar v
v BackGrad r (Grad v)
dv = forall r a. a -> BackGrad r (Grad a) -> BVar r a
BVar (Scalar (Grad v)
a forall v. VectorSpace v => Scalar v -> v -> v
*^ v
v) (forall v a b r.
(BasicVector v, BasicVector a, BasicVector b) =>
(v -> a)
-> (v -> b) -> BackGrad r a -> BackGrad r b -> BackGrad r v
lift2_dense Grad v -> MScalar v
bpA Grad v -> Grad v
bpV BackGrad r (Grad (Scalar (Grad v)))
da BackGrad r (Grad v)
dv)
    where
      bpA :: Grad v -> MScalar v
      bpA :: Grad v -> MScalar v
bpA Grad v
dz = forall v dv. Dual v dv => dv -> v -> Scalar v
evalGrad Grad v
dz v
v
      bpV :: Grad v -> Grad v
      bpV :: Grad v -> Grad v
bpV Grad v
dz = Scalar (Grad v)
a forall v. VectorSpace v => Scalar v -> v -> v
*^ Grad v
dz

instance (HasGrad p, HasGradAffine p) => AffineSpace (BVar r p) where
  type Diff (BVar r p) = BVar r (Tang p)
  BVar p
y0 BackGrad r (Grad p)
dy .+^ :: BVar r p -> Diff (BVar r p) -> BVar r p
.+^ BVar Diff p
z0 BackGrad r (Grad (Diff p))
dz = forall r a. a -> BackGrad r (Grad a) -> BVar r a
BVar (p
y0 forall p. AffineSpace p => p -> Diff p -> p
.+^ Diff p
z0) (BackGrad r (Grad p)
dy forall v. AdditiveGroup v => v -> v -> v
^+^ BackGrad r (Grad (Diff p))
dz)
  BVar p
y0 BackGrad r (Grad p)
dy .-. :: BVar r p -> BVar r p -> Diff (BVar r p)
.-. BVar p
z0 BackGrad r (Grad p)
dz = forall r a. a -> BackGrad r (Grad a) -> BVar r a
BVar (p
y0 forall p. AffineSpace p => p -> p -> Diff p
.-. p
z0) (BackGrad r (Grad p)
dy forall v. AdditiveGroup v => v -> v -> v
^-^ BackGrad r (Grad p)
dz)

-- maybe move all those equality constraints to Dual class?
instance
  ( HasGrad (Scalar v),
    HasGrad v,
    HasGrad dv,
    Dual v dv,
    Grad dv ~ v,
    Grad v ~ dv,
    Tang v ~ v,
    Tang dv ~ dv,
    Grad (Scalar dv) ~ Scalar dv
  ) =>
  Dual (BVar r v) (BVar r dv)
  where
  evalGrad :: BVar r dv -> BVar r v -> Scalar (BVar r v)
evalGrad (BVar dv
dv BackGrad r (Grad dv)
d_dv) (BVar v
v BackGrad r (Grad v)
d_v) = forall r a. a -> BackGrad r (Grad a) -> BVar r a
BVar (forall v dv. Dual v dv => dv -> v -> Scalar v
evalGrad dv
dv v
v) (forall v a b r.
(BasicVector v, BasicVector a, BasicVector b) =>
(v -> a)
-> (v -> b) -> BackGrad r a -> BackGrad r b -> BackGrad r v
lift2_dense (forall v. VectorSpace v => Scalar v -> v -> v
*^ v
v) (forall v. VectorSpace v => Scalar v -> v -> v
*^ dv
dv) BackGrad r (Grad dv)
d_dv BackGrad r (Grad v)
d_v)

instance
  ( HasGrad (MScalar p),
    HasGrad (Tang p),
    HasGrad (Grad p),
    Grad (Grad p) ~ Tang p,
    Tang (Grad p) ~ Grad p,
    Tang (Tang p) ~ Tang p,
    Grad (Tang p) ~ Grad p,
    Grad (MScalar p) ~ MScalar p,
    Scalar (Grad p) ~ Scalar (Tang p),
    Manifold p
  ) =>
  Manifold (BVar r p)
  where
  type Tang (BVar r p) = BVar r (Tang p)
  type Grad (BVar r p) = BVar r (Grad p)

instance
  ( HilbertSpace v dv,
    HasGrad (Scalar v),
    HasGrad v,
    HasGrad dv,
    Grad dv ~ v,
    Grad v ~ dv,
    Tang v ~ v,
    Tang dv ~ dv,
    Grad (Scalar dv) ~ Scalar dv
  ) =>
  HilbertSpace (BVar r v) (BVar r dv)
  where
  riesz :: BVar r v -> BVar r dv
riesz (BVar v
v BackGrad r (Grad v)
dv) = forall r a. a -> BackGrad r (Grad a) -> BVar r a
BVar (forall v dv. HilbertSpace v dv => v -> dv
riesz v
v) (forall v a r.
(BasicVector v, BasicVector a) =>
(v -> a) -> BackGrad r a -> BackGrad r v
lift1_dense forall v dv. HilbertSpace v dv => v -> dv
riesz BackGrad r (Grad v)
dv)
  coriesz :: BVar r dv -> BVar r v
coriesz (BVar dv
v BackGrad r (Grad dv)
dv) = forall r a. a -> BackGrad r (Grad a) -> BVar r a
BVar (forall v dv. HilbertSpace v dv => dv -> v
coriesz dv
v) (forall v a r.
(BasicVector v, BasicVector a) =>
(v -> a) -> BackGrad r a -> BackGrad r v
lift1_dense forall v dv. HilbertSpace v dv => dv -> v
coriesz BackGrad r (Grad dv)
dv)

instance
  ( VectorSpace v,
    HasGrad v,
    Tang v ~ v,
    HilbertSpace (Tang v) (Grad v),
    BasicVector (MScalar v),
    Grad (MScalar v) ~ MScalar v,
    InnerSpace v,
    HasGrad (MScalar v)
  ) =>
  InnerSpace (BVar r v)
  where
  BVar v
u BackGrad r (Grad v)
du <.> :: BVar r v -> BVar r v -> Scalar (BVar r v)
<.> BVar v
v BackGrad r (Grad v)
dv = forall r a. a -> BackGrad r (Grad a) -> BVar r a
BVar (v
u forall v. InnerSpace v => v -> v -> Scalar v
<.> v
v) (forall v a b r.
(BasicVector v, BasicVector a, BasicVector b) =>
(v -> a)
-> (v -> b) -> BackGrad r a -> BackGrad r b -> BackGrad r v
lift2_dense MScalar v -> Grad v
bpU MScalar v -> Grad v
bpV BackGrad r (Grad v)
du BackGrad r (Grad v)
dv)
    where
      bpU :: MScalar v -> Grad v
      bpU :: MScalar v -> Grad v
bpU MScalar v
dz = MScalar v
dz forall v. VectorSpace v => Scalar v -> v -> v
*^ forall v dv. HilbertSpace v dv => v -> dv
riesz v
v
      bpV :: MScalar v -> Grad v
      bpV :: MScalar v -> Grad v
bpV MScalar v
dz = MScalar v
dz forall v. VectorSpace v => Scalar v -> v -> v
*^ forall v dv. HilbertSpace v dv => v -> dv
riesz v
u

-- | A variable with derivative of zero.
constant :: forall r a. (BasicVector (Grad a), AdditiveGroup (Grad a)) => a -> BVar r a
constant :: forall r a.
(BasicVector (Grad a), AdditiveGroup (Grad a)) =>
a -> BVar r a
constant a
x = forall r a. a -> BackGrad r (Grad a) -> BVar r a
BVar a
x forall v. AdditiveGroup v => v
zeroV

-- | A variable with identity derivative.
var :: a -> BVar (Grad a) a
var :: forall a. a -> BVar (Grad a) a
var a
x = forall r a. a -> BackGrad r (Grad a) -> BVar r a
BVar a
x (forall a v. Expr a v -> BackGrad a v
realNode forall a. Expr a a
ExprVar)

-- | Reverse mode differentiation.
backprop :: forall r a. (HasGrad a, BasicVector r) => BVar r a -> Grad a -> r
backprop :: forall r a. (HasGrad a, BasicVector r) => BVar r a -> Grad a -> r
backprop (BVar a
_y0 BackGrad r (Grad a)
x) = forall a v.
(BasicVector a, BasicVector v) =>
BackGrad a v -> v -> a
BP.backprop BackGrad r (Grad a)
x

splitPair :: (BasicVector (Grad a), BasicVector (Grad b)) => BVar r (a, b) -> (BVar r a, BVar r b)
splitPair :: forall a b r.
(BasicVector (Grad a), BasicVector (Grad b)) =>
BVar r (a, b) -> (BVar r a, BVar r b)
splitPair (BVar (a
a, b
b) (Linear.T2 BackGrad r (Grad a)
da BackGrad r (Grad b)
db)) = (forall r a. a -> BackGrad r (Grad a) -> BVar r a
BVar a
a BackGrad r (Grad a)
da, forall r a. a -> BackGrad r (Grad a) -> BVar r a
BVar b
b BackGrad r (Grad b)
db)

pattern T2 :: forall r a b. (BasicVector (Grad a), BasicVector (Grad b)) => BVar r a -> BVar r b -> BVar r (a, b)
pattern $bT2 :: forall r a b.
(BasicVector (Grad a), BasicVector (Grad b)) =>
BVar r a -> BVar r b -> BVar r (a, b)
$mT2 :: forall {r} {r} {a} {b}.
(BasicVector (Grad a), BasicVector (Grad b)) =>
BVar r (a, b) -> (BVar r a -> BVar r b -> r) -> ((# #) -> r) -> r
T2 a b <-
  (splitPair -> (a, b))
  where
    T2 (BVar a
a BackGrad r (Grad a)
da) (BVar b
b BackGrad r (Grad b)
db) = forall r a. a -> BackGrad r (Grad a) -> BVar r a
BVar (a
a, b
b) (forall r a b.
(BasicVector a, BasicVector b) =>
BackGrad r a -> BackGrad r b -> BackGrad r (a, b)
Linear.T2 BackGrad r (Grad a)
da BackGrad r (Grad b)
db)

splitTriple :: (BasicVector (Grad a), BasicVector (Grad b), BasicVector (Grad c)) => BVar r (a, b, c) -> (BVar r a, BVar r b, BVar r c)
splitTriple :: forall a b c r.
(BasicVector (Grad a), BasicVector (Grad b),
 BasicVector (Grad c)) =>
BVar r (a, b, c) -> (BVar r a, BVar r b, BVar r c)
splitTriple (BVar (a
a, b
b, c
c) (Linear.T3 BackGrad r (Grad a)
da BackGrad r (Grad b)
db BackGrad r (Grad c)
dc)) = (forall r a. a -> BackGrad r (Grad a) -> BVar r a
BVar a
a BackGrad r (Grad a)
da, forall r a. a -> BackGrad r (Grad a) -> BVar r a
BVar b
b BackGrad r (Grad b)
db, forall r a. a -> BackGrad r (Grad a) -> BVar r a
BVar c
c BackGrad r (Grad c)
dc)

pattern T3 ::
  forall r a b c.
  (BasicVector (Grad a), BasicVector (Grad b), BasicVector (Grad c)) =>
  BVar r a ->
  BVar r b ->
  BVar r c ->
  BVar r (a, b, c)
pattern $bT3 :: forall r a b c.
(BasicVector (Grad a), BasicVector (Grad b),
 BasicVector (Grad c)) =>
BVar r a -> BVar r b -> BVar r c -> BVar r (a, b, c)
$mT3 :: forall {r} {r} {a} {b} {c}.
(BasicVector (Grad a), BasicVector (Grad b),
 BasicVector (Grad c)) =>
BVar r (a, b, c)
-> (BVar r a -> BVar r b -> BVar r c -> r) -> ((# #) -> r) -> r
T3 a b c <-
  (splitTriple -> (a, b, c))
  where
    T3 (BVar a
a BackGrad r (Grad a)
da) (BVar b
b BackGrad r (Grad b)
db) (BVar c
c BackGrad r (Grad c)
dc) = forall r a. a -> BackGrad r (Grad a) -> BVar r a
BVar (a
a, b
b, c
c) (forall r a b c.
(BasicVector a, BasicVector b, BasicVector c) =>
BackGrad r a
-> BackGrad r b -> BackGrad r c -> BackGrad r (a, b, c)
Linear.T3 BackGrad r (Grad a)
da BackGrad r (Grad b)
db BackGrad r (Grad c)
dc)