Differentiable.hs

{-# LANGUAGE PolyKinds            #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE UnliftedDatatypes    #-}

module Math.Differentiable
  ( IVness(..), SingIVness(..)
  , I, Differentiable, DiffInterp
  )
  where

-- base
import Data.Kind
  ( Type, Constraint )
import GHC.Exts
  ( UnliftedType )
import GHC.TypeNats
  ( Nat )

-- brush-strokes
import Math.Algebra.Dual
  ( D, HasChainRule )
import Math.Interval
  ( 𝕀, 𝕀ℝ )
import Math.Linear
import Math.Module
import Math.Ring
  ( Transcendental )

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

data IVness
  = NonIV
  | IsIV

type SingIVness :: IVness -> UnliftedType
data SingIVness iv where
  SNonIV :: SingIVness NonIV
  SIsIV  :: SingIVness IsIV

-- | Type family to parametrise over both pointwise and interval computations.
type I :: forall l. IVness -> l -> Type
type family I i t
type instance I @Type NonIV Double = Double
type instance I @Type IsIV  Double = 𝕀
type instance I @Nat  NonIV n      = ℝ n
type instance I @Nat  IsIV  n      = 𝕀ℝ n

type Differentiable :: Nat -> IVness -> Nat -> Constraint
class
  ( Module ( I i Double ) ( T ( I i u ) )
  , HasChainRule ( I i Double ) k ( I i u )
  , Traversable ( D k u )
  , Representable ( I i Double ) ( I i u )
  ) => Differentiable k i u
instance
  ( Module ( I i Double ) ( T ( I i u ) )
  , HasChainRule ( I i Double ) k ( I i u )
  , Traversable ( D k u )
  , Representable ( I i Double ) ( I i u )
  ) => Differentiable k i u

type DiffInterp :: Nat -> IVness -> Nat -> Constraint
class
  ( Differentiable k i u
  , Interpolatable ( I i Double ) ( I i u )
  , Module ( I i Double ) ( T ( I i Double ) )
  , Module ( D k u ( I i Double ) )
           ( D k u ( I i 2 ) )
  , Transcendental ( D k u ( I i Double ) )
  , Applicative ( D k u )
  , Representable ( I i Double ) ( I i u )
  ) => DiffInterp k i u
instance
  ( Differentiable k i u
  , Interpolatable ( I i Double ) ( I i u )
  , Module ( I i Double ) ( T ( I i Double ) )
  , Module ( D k u ( I i Double ) )
           ( D k u ( I i 2 ) )
  , Transcendental ( D k u ( I i Double ) )
  , Applicative ( D k u )
  , Representable ( I i Double ) ( I i u )
  ) => DiffInterp k i u