{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE InstanceSigs #-}
{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE IncoherentInstances #-}
{-# LANGUAGE TupleSections #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE CPP #-}
{-# LANGUAGE ViewPatterns #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE DefaultSignatures #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE ScopedTypeVariables #-}


{-# OPTIONS_GHC -Wall #-}
{-# OPTIONS_GHC -Wno-unused-imports #-} -- TEMP

#include "ConCat/AbsTy.inc"
AbsTyPragmas

-- | Incremental evaluation via generalized automatic differentiation

module ConCat.Incremental where

import Prelude hiding (id,(.),const,curry,uncurry)
-- import qualified Prelude as P
import Data.Maybe (fromMaybe,isNothing)
import Control.Applicative (liftA2)
import Control.Monad ((>=>))
import GHC.Exts (Coercible,coerce)

import Data.Void (Void,absurd)
import Control.Newtype.Generics
import Data.Constraint ((:-)(..),Dict(..))

import ConCat.Misc ((:*),(:+),Unop,Binop, inNew2,Parity,R,Yes1,result, C4)
import ConCat.Rep
import ConCat.Category
import qualified ConCat.AltCat as A
import ConCat.GAD
import ConCat.AdditiveFun

-- For DelRep:

import ConCat.Complex
import Data.Monoid
import Control.Applicative (WrappedMonad(..))
import GHC.Generics (Par1(..),U1(..),K1(..),M1(..),(:+:)(..),(:*:)(..),(:.:)(..))
import Data.Functor.Identity (Identity(..))
import Control.Monad.Trans.Reader (ReaderT(..))
import Control.Monad.Trans.Writer (WriterT(..))
import Control.Monad.Trans.State (StateT(..))

AbsTyImports

import ConCat.Free.LinearRow (L)
-- Tests:
import ConCat.Free.VectorSpace (V)
import GHC.Generics ((:*:))

{--------------------------------------------------------------------
    Changes
--------------------------------------------------------------------}

-- Delta for "Atomic" (all-or-nothing) values.
-- Nothing for no change, and Just a for new value a.
type AtomDel a = Maybe a

type Atomic a = (HasDelta a, Delta a ~ AtomDel a)

infixl 6 .-., .+^, @+

type RepDel a = (HasRep a, HasDelta (Rep a), Delta a ~ Delta (Rep a))

class HasDelta a where
  type Delta a
  (@+) :: HasDelta a => Binop (Delta a)
  (.+^) :: a -> Delta a -> a
  (.-.) :: a -> a -> Delta a

  type Delta a = Delta (Rep a)
  default (@+) :: RepDel a => Binop (Delta a)
  (@+) = forall a. (HasDelta a, HasDelta a) => Binop (Delta a)
(@+) @(Rep a)
  default (.+^) :: RepDel a => a -> Delta a -> a
  a
a .+^ Delta a
da = Rep a -> a
forall a. HasRep a => Rep a -> a
abst (a -> Rep a
forall a. HasRep a => a -> Rep a
repr a
a Rep a -> Delta (Rep a) -> Rep a
forall a. HasDelta a => a -> Delta a -> a
.+^ Delta a
Delta (Rep a)
da)
  default (.-.) :: ({-Eq a,-} RepDel a) => a -> a -> Delta a
  a
a' .-. a
a = a -> Rep a
forall a. HasRep a => a -> Rep a
repr a
a' Rep a -> Rep a -> Delta (Rep a)
forall a. HasDelta a => a -> a -> Delta a
.-. a -> Rep a
forall a. HasRep a => a -> Rep a
repr a
a
  default zeroD :: RepDel a => Delta a
  zeroD :: Delta a              -- needs an explicit type application
  zeroD = forall a. HasDelta a => Delta a
zeroD @(Rep a)  

#define DelAtom(ty) \
  instance HasDelta (ty) where { \
  ; type Delta (ty) = Maybe (ty) \
  ; da @+ Nothing = da \
  ; _  @+ Just a  = Just a \
  ; (.+^) = fromMaybe \
  ; new .-. old = if new == old then Nothing else Just new \
  ; zeroD = Nothing \
  }


-- TODO: Use HasRep instead of Atomic for default, since there are
-- more of them.

-- Semantic function
appD :: HasDelta a => Delta a -> Unop a
appD :: forall a. HasDelta a => Delta a -> Unop a
appD = (a -> Delta a -> a) -> Delta a -> a -> a
forall a b c. (a -> b -> c) -> b -> a -> c
flip a -> Delta a -> a
forall a. HasDelta a => a -> Delta a -> a
(.+^)

-- Unit can't change.
instance HasDelta () where
  type Delta () = () -- no change
  () @+ :: HasDelta () => Binop (Delta ())
@+ () = ()
  () .+^ :: () -> Delta () -> ()
.+^ () = ()
  () .-. :: () -> () -> Delta ()
.-. () = ()
  zeroD :: Delta ()
zeroD = ()

-- instance HasDelta ()
-- instance HasDelta Bool
-- instance HasDelta Int
-- instance HasDelta Float
-- instance HasDelta Double

DelAtom(Bool)
DelAtom(Int)
DelAtom(Float)
DelAtom(Double)

instance (HasDelta a, HasDelta b) => HasDelta (a :* b) where
  type Delta (a :* b) = Delta a :* Delta b
  (Delta a
da,Delta b
db) @+ :: HasDelta (a :* b) => Binop (Delta (a :* b))
@+ (Delta a
da',Delta b
db') = (forall a. (HasDelta a, HasDelta a) => Binop (Delta a)
(@+) @a Delta a
da Delta a
da', forall a. (HasDelta a, HasDelta a) => Binop (Delta a)
(@+) @b Delta b
db Delta b
db')
  (a
a,b
b) .+^ :: (a :* b) -> Delta (a :* b) -> a :* b
.+^ (Delta a
da,Delta b
db) = (a
a a -> Delta a -> a
forall a. HasDelta a => a -> Delta a -> a
.+^ Delta a
da, b
b b -> Delta b -> b
forall a. HasDelta a => a -> Delta a -> a
.+^ Delta b
db)
  (a
a',b
b') .-. :: (a :* b) -> (a :* b) -> Delta (a :* b)
.-. (a
a,b
b) = (a
a' a -> a -> Delta a
forall a. HasDelta a => a -> a -> Delta a
.-. a
a, b
b' b -> b -> Delta b
forall a. HasDelta a => a -> a -> Delta a
.-. b
b)
  zeroD :: Delta (a :* b)
zeroD = (forall a. HasDelta a => Delta a
zeroD @a, forall a. HasDelta a => Delta a
zeroD @b)

instance (HasDelta a, HasDelta b) => HasDelta (a :+ b) where
  -- No change, left, right
  type Delta (a :+ b) = Maybe (Delta a :+ Delta b)
  Delta (a :+ b)
dab @+ :: HasDelta (a :+ b) => Binop (Delta (a :+ b))
@+ Maybe (Delta a :+ Delta b)
Delta (a :+ b)
Nothing = Delta (a :+ b)
dab
  Maybe (Delta a :+ Delta b)
Delta (a :+ b)
Nothing @+ Delta (a :+ b)
dab' = Delta (a :+ b)
dab'
  Just (Left  Delta a
da) @+ Just (Left  Delta a
da') = (Delta a :+ Delta b) -> Maybe (Delta a :+ Delta b)
forall a. a -> Maybe a
Just (Delta a -> Delta a :+ Delta b
forall a b. a -> Either a b
Left  (forall a. (HasDelta a, HasDelta a) => Binop (Delta a)
(@+) @a Delta a
da Delta a
da'))
  Just (Right Delta b
db) @+ Just (Right Delta b
db') = (Delta a :+ Delta b) -> Maybe (Delta a :+ Delta b)
forall a. a -> Maybe a
Just (Delta b -> Delta a :+ Delta b
forall a b. b -> Either a b
Right (forall a. (HasDelta a, HasDelta a) => Binop (Delta a)
(@+) @b Delta b
db Delta b
db'))
  Delta (a :+ b)
_ @+ Delta (a :+ b)
_ = [Char] -> Maybe (Delta a :+ Delta b)
forall a. HasCallStack => [Char] -> a
error [Char]
"(@+): left/right mismatch"
  (.+^) :: (a :+ b) -> Maybe (Delta a :+ Delta b) -> (a :+ b)
  a :+ b
e .+^ :: (a :+ b) -> Maybe (Delta a :+ Delta b) -> a :+ b
.+^ Maybe (Delta a :+ Delta b)
Nothing         = a :+ b
e
  Left  a
a .+^ Just (Left  Delta a
da) = a -> a :+ b
forall a b. a -> Either a b
Left  (Delta a -> Unop a
forall a. HasDelta a => Delta a -> Unop a
appD Delta a
da a
a)
  Right b
a .+^ Just (Right Delta b
da) = b -> a :+ b
forall a b. b -> Either a b
Right (Delta b -> Unop b
forall a. HasDelta a => Delta a -> Unop a
appD Delta b
da b
a)
  a :+ b
_ .+^ Maybe (Delta a :+ Delta b)
_                     = [Char] -> a :+ b
forall a. HasCallStack => [Char] -> a
error [Char]
"(.+^): left/right mismatch"
  Left  a
a' .-. :: (a :+ b) -> (a :+ b) -> Delta (a :+ b)
.-. Left  a
a = (Delta a :+ Delta b) -> Maybe (Delta a :+ Delta b)
forall a. a -> Maybe a
Just (Delta a -> Delta a :+ Delta b
forall a b. a -> Either a b
Left  (a
a' a -> a -> Delta a
forall a. HasDelta a => a -> a -> Delta a
.-. a
a))
  Right b
b' .-. Right b
b = (Delta a :+ Delta b) -> Maybe (Delta a :+ Delta b)
forall a. a -> Maybe a
Just (Delta b -> Delta a :+ Delta b
forall a b. b -> Either a b
Right (b
b' b -> b -> Delta b
forall a. HasDelta a => a -> a -> Delta a
.-. b
b))
  a :+ b
_        .-. a :+ b
_       = Maybe (Delta a :+ Delta b)
Delta (a :+ b)
forall a. Maybe a
Nothing
  zeroD :: Delta (a :+ b)
zeroD = Maybe (Delta a :+ Delta b)
Delta (a :+ b)
forall a. Maybe a
Nothing

instance HasDelta b => HasDelta (a -> b) where
  type Delta (a -> b) = a -> Delta b
  (Delta (a -> b)
df @+ :: HasDelta (a -> b) => Binop (Delta (a -> b))
@+ Delta (a -> b)
df') a
a = forall a. (HasDelta a, HasDelta a) => Binop (Delta a)
(@+) @b (Delta (a -> b)
a -> Delta b
df a
a) (Delta (a -> b)
a -> Delta b
df' a
a)
  .+^ :: (a -> b) -> Delta (a -> b) -> a -> b
(.+^) = (b -> Delta b -> b) -> (a -> b) -> (a -> Delta b) -> a -> b
forall a b c. (a -> b -> c) -> (a -> a) -> (a -> b) -> a -> c
forall (f :: * -> *) a b c.
Applicative f =>
(a -> b -> c) -> f a -> f b -> f c
liftA2 b -> Delta b -> b
forall a. HasDelta a => a -> Delta a -> a
(.+^)
  .-. :: (a -> b) -> (a -> b) -> Delta (a -> b)
(.-.) = (b -> b -> Delta b) -> (a -> b) -> (a -> b) -> a -> Delta b
forall a b c. (a -> b -> c) -> (a -> a) -> (a -> b) -> a -> c
forall (f :: * -> *) a b c.
Applicative f =>
(a -> b -> c) -> f a -> f b -> f c
liftA2 b -> b -> Delta b
forall a. HasDelta a => a -> a -> Delta a
(.-.)
  zeroD :: Delta (a -> b)
zeroD = \ a
_ -> forall a. HasDelta a => Delta a
zeroD @b

  -- (f .+^ df) a = f a .+^ df a
  -- (f' .-. f) a = f' a .-. f a

-- instance HasDelta a => Additive (Delta a) where
--   (^+^) = (@+) @a
--   zero = zeroD @a
--
-- Nope:
-- 
--    Illegal type synonym family application in instance: Delta a
--    In the instance declaration for ‘Additive (Delta a)’

instance OpCon (:*) (Sat HasDelta) where inOp :: forall a b.
(Sat HasDelta a && Sat HasDelta b) |- Sat HasDelta (a :* b)
inOp = (Con (Sat HasDelta a && Sat HasDelta b)
 :- Con (Sat HasDelta (a :* b)))
-> (Sat HasDelta a && Sat HasDelta b) |- Sat HasDelta (a :* b)
forall a b. (Con a :- Con b) -> a |- b
Entail (((HasDelta a, HasDelta b) => Dict (HasDelta (a :* b)))
-> (HasDelta a, HasDelta b) :- HasDelta (a :* b)
forall (a :: Constraint) (b :: Constraint). (a => Dict b) -> a :- b
Sub Dict (HasDelta (a :* b))
(HasDelta a, HasDelta b) => Dict (HasDelta (a :* b))
forall (a :: Constraint). a => Dict a
Dict)
instance OpCon (:+) (Sat HasDelta) where inOp :: forall a b.
(Sat HasDelta a && Sat HasDelta b) |- Sat HasDelta (a :+ b)
inOp = (Con (Sat HasDelta a && Sat HasDelta b)
 :- Con (Sat HasDelta (a :+ b)))
-> (Sat HasDelta a && Sat HasDelta b) |- Sat HasDelta (a :+ b)
forall a b. (Con a :- Con b) -> a |- b
Entail (((HasDelta a, HasDelta b) => Dict (HasDelta (a :+ b)))
-> (HasDelta a, HasDelta b) :- HasDelta (a :+ b)
forall (a :: Constraint) (b :: Constraint). (a => Dict b) -> a :- b
Sub Dict (HasDelta (a :+ b))
(HasDelta a, HasDelta b) => Dict (HasDelta (a :+ b))
forall (a :: Constraint). a => Dict a
Dict)
instance OpCon (->) (Sat HasDelta) where inOp :: forall a b.
(Sat HasDelta a && Sat HasDelta b) |- Sat HasDelta (a -> b)
inOp = (Con (Sat HasDelta a && Sat HasDelta b)
 :- Con (Sat HasDelta (a -> b)))
-> (Sat HasDelta a && Sat HasDelta b) |- Sat HasDelta (a -> b)
forall a b. (Con a :- Con b) -> a |- b
Entail (((HasDelta a, HasDelta b) => Dict (HasDelta (a -> b)))
-> (HasDelta a, HasDelta b) :- HasDelta (a -> b)
forall (a :: Constraint) (b :: Constraint). (a => Dict b) -> a :- b
Sub Dict (HasDelta (a -> b))
(HasDelta a, HasDelta b) => Dict (HasDelta (a -> b))
forall (a :: Constraint). a => Dict a
Dict)

-- Instead, wrap Delta a:

newtype Del a = Del (Delta a)

instance HasRep (Del a) where
  type Rep (Del a) = Delta a
  abst :: Rep (Del a) -> Del a
abst Rep (Del a)
d = Delta a -> Del a
forall a. Delta a -> Del a
Del Rep (Del a)
Delta a
d
  repr :: Del a -> Rep (Del a)
repr (Del Delta a
d) = Rep (Del a)
Delta a
d

AbsTy(Del a)

instance HasDelta a => Additive (Del a) where
  ^+^ :: Del a -> Del a -> Del a
(^+^) = (Rep (Del a) -> Rep (Del a) -> Rep (Del a))
-> Del a -> Del a -> Del a
forall p q r.
(HasRep p, HasRep q, HasRep r) =>
(Rep p -> Rep q -> Rep r) -> p -> q -> r
inAbst2 (forall a. (HasDelta a, HasDelta a) => Binop (Delta a)
(@+) @a)
  zero :: Del a
zero = Rep (Del a) -> Del a
forall a. HasRep a => Rep a -> a
abst (forall a. HasDelta a => Delta a
zeroD @a)

{--------------------------------------------------------------------
    Change transformations
--------------------------------------------------------------------}

infixr 1 -#>
newtype a -#> b = DelX { forall a b. (a -#> b) -> Del a -+> Del b
unDelX :: Del a -+> Del b }

type Inc = GD (-#>)

instance HasRep (a -#> b) where
  type Rep (a -#> b) = Del a -+> Del b
  abst :: Rep (a -#> b) -> a -#> b
abst Rep (a -#> b)
f = (Del a -+> Del b) -> a -#> b
forall a b. (Del a -+> Del b) -> a -#> b
DelX Rep (a -#> b)
Del a -+> Del b
f
  repr :: (a -#> b) -> Rep (a -#> b)
repr (DelX Del a -+> Del b
f) = Rep (a -#> b)
Del a -+> Del b
f

AbsTy(a -#> b)

pairD :: Del u :* Del v -+> Del (u :* v)
pairD :: forall u v. (Del u :* Del v) -+> Del (u :* v)
pairD = Rep ((Del u :* Del v) -+> Del (u :* v))
-> (Del u :* Del v) -+> Del (u :* v)
forall a. HasRep a => Rep a -> a
abst ((Del u -> Exp (->) (Del v) (Del (u :* v)))
-> (Del u :* Del v) -> Del (u :* v)
forall a b c.
Ok3 (->) a b c =>
(a -> Exp (->) b c) -> Prod (->) a b -> c
forall (k :: * -> * -> *) a b c.
(ClosedCat k, Ok3 k a b c) =>
k a (Exp (->) b c) -> k (Prod (->) a b) c
uncurry ((Rep (Del u) -> Rep (Del v) -> Rep (Del (u :* v)))
-> Del u -> Exp (->) (Del v) (Del (u :* v))
forall p q r.
(HasRep p, HasRep q, HasRep r) =>
(Rep p -> Rep q -> Rep r) -> p -> q -> r
inAbst2 (,)))
{-# INLINE pairD #-}

unPairD :: Del (u :* v) -+> Del u :* Del v
unPairD :: forall u v. Del (u :* v) -+> (Del u :* Del v)
unPairD = Rep (Del (u :* v) -+> (Del u :* Del v))
-> Del (u :* v) -+> (Del u :* Del v)
forall a. HasRep a => Rep a -> a
abst (\ (Del (Delta u
du,Delta v
dv)) -> (Delta u -> Del u
forall a. Delta a -> Del a
Del Delta u
du, Delta v -> Del v
forall a. Delta a -> Del a
Del Delta v
dv))
{-# INLINE unPairD #-}

inPairD :: (C4 HasDelta u v u' v')
        => (Del u :* Del v -+> Del u' :* Del v')
        -> (Del (u :* v)   -+> Del (u' :* v'))
-- inPairD = pairD <~ unPairD  -- when (<~) etc are moved from Category to AltCat
inPairD :: forall u v u' v'.
C4 HasDelta u v u' v' =>
((Del u :* Del v) -+> (Del u' :* Del v'))
-> Del (u :* v) -+> Del (u' :* v')
inPairD (Del u :* Del v) -+> (Del u' :* Del v')
h = (Del u' :* Del v') -+> Del (u' :* v')
forall u v. (Del u :* Del v) -+> Del (u :* v)
pairD ((Del u' :* Del v') -+> Del (u' :* v'))
-> (Del (u :* v) -+> (Del u' :* Del v'))
-> Del (u :* v) -+> Del (u' :* v')
forall b c a. Ok3 (-+>) a b c => (b -+> c) -> (a -+> b) -> a -+> c
forall (k :: * -> * -> *) b c a.
(Category k, Ok3 k a b c) =>
k b c -> k a b -> k a c
. (Del u :* Del v) -+> (Del u' :* Del v')
h ((Del u :* Del v) -+> (Del u' :* Del v'))
-> (Del (u :* v) -+> (Del u :* Del v))
-> Del (u :* v) -+> (Del u' :* Del v')
forall b c a. Ok3 (-+>) a b c => (b -+> c) -> (a -+> b) -> a -+> c
forall (k :: * -> * -> *) b c a.
(Category k, Ok3 k a b c) =>
k b c -> k a b -> k a c
. Del (u :* v) -+> (Del u :* Del v)
forall u v. Del (u :* v) -+> (Del u :* Del v)
unPairD

instance Category (-#>) where
  type Ok (-#>) = HasDelta
  id :: forall a. Ok (-#>) a => a -#> a
id  = Rep (a -#> a) -> a -#> a
forall a. HasRep a => Rep a -> a
abst Rep (a -#> a)
Del a -+> Del a
forall a. Ok (-+>) a => a -+> a
forall (k :: * -> * -> *) a. (Category k, Ok k a) => k a a
id
  . :: forall b c a. Ok3 (-#>) a b c => (b -#> c) -> (a -#> b) -> a -#> c
(.) = (Rep (b -#> c) -> Rep (a -#> b) -> Rep (a -#> c))
-> (b -#> c) -> (a -#> b) -> a -#> c
forall p q r.
(HasRep p, HasRep q, HasRep r) =>
(Rep p -> Rep q -> Rep r) -> p -> q -> r
inAbst2 Rep (b -#> c) -> Rep (a -#> b) -> Rep (a -#> c)
(Del b -+> Del c) -> (Del a -+> Del b) -> Del a -+> Del c
forall b c a. Ok3 (-+>) a b c => (b -+> c) -> (a -+> b) -> a -+> c
forall (k :: * -> * -> *) b c a.
(Category k, Ok3 k a b c) =>
k b c -> k a b -> k a c
(.)
  {-# INLINE id #-}
  {-# INLINE (.) #-}

instance MonoidalPCat (-#>) where
  *** :: forall a b c d.
Ok4 (-#>) a b c d =>
(a -#> c) -> (b -#> d) -> Prod (-#>) a b -#> Prod (-#>) c d
(***) = (Rep (a -#> c) -> Rep (b -#> d) -> Rep ((a :* b) -#> (c :* d)))
-> (a -#> c) -> (b -#> d) -> (a :* b) -#> (c :* d)
forall p q r.
(HasRep p, HasRep q, HasRep r) =>
(Rep p -> Rep q -> Rep r) -> p -> q -> r
inAbst2 (((((Del b -+> Del d) -> (Del a :* Del b) -+> (Del c :* Del d))
 -> (Del b -+> Del d) -> Del (a :* b) -+> Del (c :* d))
-> ((Del a -+> Del c)
    -> (Del b -+> Del d) -> (Del a :* Del b) -+> (Del c :* Del d))
-> (Del a -+> Del c)
-> (Del b -+> Del d)
-> Del (a :* b) -+> Del (c :* d)
forall b c a. (b -> c) -> (a -> b) -> a -> c
result((((Del b -+> Del d) -> (Del a :* Del b) -+> (Del c :* Del d))
  -> (Del b -+> Del d) -> Del (a :* b) -+> Del (c :* d))
 -> ((Del a -+> Del c)
     -> (Del b -+> Del d) -> (Del a :* Del b) -+> (Del c :* Del d))
 -> (Del a -+> Del c)
 -> (Del b -+> Del d)
 -> Del (a :* b) -+> Del (c :* d))
-> ((((Del a :* Del b) -+> (Del c :* Del d))
     -> Del (a :* b) -+> Del (c :* d))
    -> ((Del b -+> Del d) -> (Del a :* Del b) -+> (Del c :* Del d))
    -> (Del b -+> Del d)
    -> Del (a :* b) -+> Del (c :* d))
-> (((Del a :* Del b) -+> (Del c :* Del d))
    -> Del (a :* b) -+> Del (c :* d))
-> ((Del a -+> Del c)
    -> (Del b -+> Del d) -> (Del a :* Del b) -+> (Del c :* Del d))
-> (Del a -+> Del c)
-> (Del b -+> Del d)
-> Del (a :* b) -+> Del (c :* d)
forall b c a. Ok3 (->) a b c => (b -> c) -> (a -> b) -> a -> c
forall (k :: * -> * -> *) b c a.
(Category k, Ok3 k a b c) =>
k b c -> k a b -> k a c
.(((Del a :* Del b) -+> (Del c :* Del d))
 -> Del (a :* b) -+> Del (c :* d))
-> ((Del b -+> Del d) -> (Del a :* Del b) -+> (Del c :* Del d))
-> (Del b -+> Del d)
-> Del (a :* b) -+> Del (c :* d)
forall b c a. (b -> c) -> (a -> b) -> a -> c
result) ((Del a :* Del b) -+> (Del c :* Del d))
-> Del (a :* b) -+> Del (c :* d)
forall u v u' v'.
C4 HasDelta u v u' v' =>
((Del u :* Del v) -+> (Del u' :* Del v'))
-> Del (u :* v) -+> Del (u' :* v')
inPairD (Del a -+> Del c)
-> (Del b -+> Del d) -> (Del a :* Del b) -+> (Del c :* Del d)
forall a b c d.
Ok4 (-+>) a b c d =>
(a -+> c) -> (b -+> d) -> Prod (-#>) a b -+> Prod (-#>) c d
forall (k :: * -> * -> *) a b c d.
(MonoidalPCat k, Ok4 k a b c d) =>
k a c -> k b d -> k (Prod (-#>) a b) (Prod (-#>) c d)
(***))
  {-# INLINE (***) #-}

instance BraidedPCat (-#>) where
  swapP :: forall a b. Ok2 (-#>) a b => Prod (-#>) a b -#> Prod (-#>) b a
swapP = Rep ((a :* b) -#> (b :* a)) -> (a :* b) -#> (b :* a)
forall a. HasRep a => Rep a -> a
abst ((Del b :* Del a) -+> Del (b :* a)
forall u v. (Del u :* Del v) -+> Del (u :* v)
pairD ((Del b :* Del a) -+> Del (b :* a))
-> (Del (a :* b) -+> (Del b :* Del a))
-> Del (a :* b) -+> Del (b :* a)
forall b c a. Ok3 (-+>) a b c => (b -+> c) -> (a -+> b) -> a -+> c
forall (k :: * -> * -> *) b c a.
(Category k, Ok3 k a b c) =>
k b c -> k a b -> k a c
. Prod (-+>) (Del a) (Del b) -+> (Del b :* Del a)
forall a b. Ok2 (-+>) a b => Prod (-#>) a b -+> Prod (-#>) b a
forall (k :: * -> * -> *) a b.
(BraidedPCat k, Ok2 k a b) =>
k (Prod (-#>) a b) (Prod (-#>) b a)
swapP (Prod (-+>) (Del a) (Del b) -+> (Del b :* Del a))
-> (Del (a :* b) -+> Prod (-+>) (Del a) (Del b))
-> Del (a :* b) -+> (Del b :* Del a)
forall b c a. Ok3 (-+>) a b c => (b -+> c) -> (a -+> b) -> a -+> c
forall (k :: * -> * -> *) b c a.
(Category k, Ok3 k a b c) =>
k b c -> k a b -> k a c
. Del (a :* b) -+> Prod (-+>) (Del a) (Del b)
forall u v. Del (u :* v) -+> (Del u :* Del v)
unPairD)

instance ProductCat (-#>) where
  exl :: forall a b. Ok2 (-#>) a b => Prod (-#>) a b -#> a
exl = Rep ((a :* b) -#> a) -> (a :* b) -#> a
forall a. HasRep a => Rep a -> a
abst (Prod (-+>) (Del a) (Del b) -+> Del a
forall a b. Ok2 (-+>) a b => Prod (-#>) a b -+> a
forall (k :: * -> * -> *) a b.
(ProductCat k, Ok2 k a b) =>
k (Prod (-#>) a b) a
exl (Prod (-+>) (Del a) (Del b) -+> Del a)
-> (Del (a :* b) -+> Prod (-+>) (Del a) (Del b))
-> Del (a :* b) -+> Del a
forall b c a. Ok3 (-+>) a b c => (b -+> c) -> (a -+> b) -> a -+> c
forall (k :: * -> * -> *) b c a.
(Category k, Ok3 k a b c) =>
k b c -> k a b -> k a c
. Del (a :* b) -+> Prod (-+>) (Del a) (Del b)
forall u v. Del (u :* v) -+> (Del u :* Del v)
unPairD)
  exr :: forall a b. Ok2 (-#>) a b => Prod (-#>) a b -#> b
exr = Rep ((a :* b) -#> b) -> (a :* b) -#> b
forall a. HasRep a => Rep a -> a
abst (Prod (-+>) (Del a) (Del b) -+> Del b
forall a b. Ok2 (-+>) a b => Prod (-#>) a b -+> b
forall (k :: * -> * -> *) a b.
(ProductCat k, Ok2 k a b) =>
k (Prod (-#>) a b) b
exr (Prod (-+>) (Del a) (Del b) -+> Del b)
-> (Del (a :* b) -+> Prod (-+>) (Del a) (Del b))
-> Del (a :* b) -+> Del b
forall b c a. Ok3 (-+>) a b c => (b -+> c) -> (a -+> b) -> a -+> c
forall (k :: * -> * -> *) b c a.
(Category k, Ok3 k a b c) =>
k b c -> k a b -> k a c
. Del (a :* b) -+> Prod (-+>) (Del a) (Del b)
forall u v. Del (u :* v) -+> (Del u :* Del v)
unPairD)
  dup :: forall a. Ok (-#>) a => a -#> Prod (-#>) a a
dup = Rep (a -#> (a :* a)) -> a -#> (a :* a)
forall a. HasRep a => Rep a -> a
abst ((Del a :* Del a) -+> Del (a :* a)
forall u v. (Del u :* Del v) -+> Del (u :* v)
pairD ((Del a :* Del a) -+> Del (a :* a))
-> (Del a -+> (Del a :* Del a)) -> Del a -+> Del (a :* a)
forall b c a. Ok3 (-+>) a b c => (b -+> c) -> (a -+> b) -> a -+> c
forall (k :: * -> * -> *) b c a.
(Category k, Ok3 k a b c) =>
k b c -> k a b -> k a c
. Del a -+> (Del a :* Del a)
forall a. Ok (-+>) a => a -+> Prod (-#>) a a
forall (k :: * -> * -> *) a.
(ProductCat k, Ok k a) =>
k a (Prod (-#>) a a)
dup)
  {-# INLINE exl #-}
  {-# INLINE exr #-}
  {-# INLINE dup #-}

#if 0
-- Types for exl:
      exl            :: Del a :* Del b -+> Del a
      exl . unPairD  :: Del (a :* b) -+> Del a
abst (exl . unPairD) :: a :* b -#> a

-- Types for (&&&):
               f         :: Del a -+> Del c
                     g   :: Del a -+> Del d
               f &&& g   :: Del a -+> Del c :* Del d
      pairD . (f &&& g)  :: Del a -+> Del (c :* d)
abst (pairD . (f &&& g)) :: a -#> c :* d
#endif

-- instance UnitCat (-#>)

instance CoproductPCat (-#>) where
  inlP :: forall a b. Ok2 (-#>) a b => a -#> CoprodP (-#>) a b
inlP = Rep (a -#> CoprodP (-#>) a b) -> a -#> CoprodP (-#>) a b
forall a. HasRep a => Rep a -> a
abst ((Del a :* Del b) -+> Del (CoprodP (-#>) a b)
forall u v. (Del u :* Del v) -+> Del (u :* v)
pairD ((Del a :* Del b) -+> Del (CoprodP (-#>) a b))
-> (Del a -+> (Del a :* Del b))
-> Del a -+> Del (CoprodP (-#>) a b)
forall b c a. Ok3 (-+>) a b c => (b -+> c) -> (a -+> b) -> a -+> c
forall (k :: * -> * -> *) b c a.
(Category k, Ok3 k a b c) =>
k b c -> k a b -> k a c
. Del a -+> (Del a :* Del b)
forall a b. Ok2 (-+>) a b => a -+> CoprodP (-#>) a b
forall (k :: * -> * -> *) a b.
(CoproductPCat k, Ok2 k a b) =>
k a (CoprodP (-#>) a b)
inlP)
  inrP :: forall a b. Ok2 (-#>) a b => b -#> CoprodP (-#>) a b
inrP = Rep (b -#> CoprodP (-#>) a b) -> b -#> CoprodP (-#>) a b
forall a. HasRep a => Rep a -> a
abst ((Del a :* Del b) -+> Del (CoprodP (-#>) a b)
forall u v. (Del u :* Del v) -+> Del (u :* v)
pairD ((Del a :* Del b) -+> Del (CoprodP (-#>) a b))
-> (Del b -+> (Del a :* Del b))
-> Del b -+> Del (CoprodP (-#>) a b)
forall b c a. Ok3 (-+>) a b c => (b -+> c) -> (a -+> b) -> a -+> c
forall (k :: * -> * -> *) b c a.
(Category k, Ok3 k a b c) =>
k b c -> k a b -> k a c
. Del b -+> (Del a :* Del b)
forall a b. Ok2 (-+>) a b => b -+> CoprodP (-#>) a b
forall (k :: * -> * -> *) a b.
(CoproductPCat k, Ok2 k a b) =>
k b (CoprodP (-#>) a b)
inrP)
  jamP :: forall a. Ok (-#>) a => CoprodP (-#>) a a -#> a
jamP = Rep (CoprodP (-#>) a a -#> a) -> CoprodP (-#>) a a -#> a
forall a. HasRep a => Rep a -> a
abst (CoprodP (-+>) (Del a) (Del a) -+> Del a
forall a. Ok (-+>) a => CoprodP (-#>) a a -+> a
forall (k :: * -> * -> *) a.
(CoproductPCat k, Ok k a) =>
k (CoprodP (-#>) a a) a
jamP (CoprodP (-+>) (Del a) (Del a) -+> Del a)
-> (Del (CoprodP (-#>) a a) -+> CoprodP (-+>) (Del a) (Del a))
-> Del (CoprodP (-#>) a a) -+> Del a
forall b c a. Ok3 (-+>) a b c => (b -+> c) -> (a -+> b) -> a -+> c
forall (k :: * -> * -> *) b c a.
(Category k, Ok3 k a b c) =>
k b c -> k a b -> k a c
. Del (CoprodP (-#>) a a) -+> CoprodP (-+>) (Del a) (Del a)
forall u v. Del (u :* v) -+> (Del u :* Del v)
unPairD)
  {-# INLINE inlP #-}
  {-# INLINE inrP #-}
  {-# INLINE jamP #-}

#if 0
-- Types for inlP:
              inlP  :: Del a -+> Del a :* Del b
      pairD . inlP  :: Del a -+> Del (a :* b)
abst (pairD . inlP) :: a -#> a :* b

-- Types for (||||):
               f            :: Del a -+> Del c
                     g      :: Del b -+> Del c
               f |||| g     :: Del a :* Del b -+> Del c
      (f |||| g) . unPairD  :: Del (a :* b) -+> Del c
abst ((f |||| g) . unPairD) :: a :* b -#> c
#endif

atomicD1 :: (Atomic a, Atomic b) => (a -> b) -> (a -#> b)
atomicD1 :: forall a b. (Atomic a, Atomic b) => (a -> b) -> a -#> b
atomicD1 = Rep (a -#> b) -> a -#> b
(Del a -+> Del b) -> a -#> b
forall a. HasRep a => Rep a -> a
abst ((Del a -+> Del b) -> a -#> b)
-> ((a -> b) -> Del a -+> Del b) -> (a -> b) -> a -#> b
forall b c a. Ok3 (->) a b c => (b -> c) -> (a -> b) -> a -> c
forall (k :: * -> * -> *) b c a.
(Category k, Ok3 k a b c) =>
k b c -> k a b -> k a c
. Rep (Del a -+> Del b) -> Del a -+> Del b
(Del a -> Del b) -> Del a -+> Del b
forall a. HasRep a => Rep a -> a
abst ((Del a -> Del b) -> Del a -+> Del b)
-> ((a -> b) -> Del a -> Del b) -> (a -> b) -> Del a -+> Del b
forall b c a. Ok3 (->) a b c => (b -> c) -> (a -> b) -> a -> c
forall (k :: * -> * -> *) b c a.
(Category k, Ok3 k a b c) =>
k b c -> k a b -> k a c
. (AtomDel a -> AtomDel b) -> Del a -> Del b
(Rep (Del a) -> Rep (Del b)) -> Del a -> Del b
forall p q. (HasRep p, HasRep q) => (Rep p -> Rep q) -> p -> q
inAbst ((AtomDel a -> AtomDel b) -> Del a -> Del b)
-> ((a -> b) -> AtomDel a -> AtomDel b)
-> (a -> b)
-> Del a
-> Del b
forall b c a. Ok3 (->) a b c => (b -> c) -> (a -> b) -> a -> c
forall (k :: * -> * -> *) b c a.
(Category k, Ok3 k a b c) =>
k b c -> k a b -> k a c
. (a -> b) -> AtomDel a -> AtomDel b
forall a b. (a -> b) -> Maybe a -> Maybe b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap
-- atomicD1 f = abst $ abst $ inAbst $ fmap f

#if 0
                         f    :: a -> b
                    fmap f    :: Maybe a -> Maybe b
            inAbst (fmap f)   :: Del a -> Del b
      abst (inAbst (fmap f))  :: Del a -+> Del b
abst (abst (inAbst (fmap f))) :: a -#> b
#endif

-- Similar to liftA2 on Maybe, but yields a Just when either argument does.
orMaybe :: (a :* b -> c) -> a :* b -> (Maybe a :* Maybe b -> Maybe c)
orMaybe :: forall a b c.
((a :* b) -> c) -> (a :* b) -> (Maybe a :* Maybe b) -> Maybe c
orMaybe (a :* b) -> c
_ (a
_,b
_) (Maybe a
Nothing,Maybe b
Nothing) = Maybe c
forall a. Maybe a
Nothing
orMaybe (a :* b) -> c
f (a
_,b
b) (Just a
a',Maybe b
Nothing) = c -> Maybe c
forall a. a -> Maybe a
Just ((a :* b) -> c
f (a
a',b
b ))
orMaybe (a :* b) -> c
f (a
a,b
_) (Maybe a
Nothing,Just b
b') = c -> Maybe c
forall a. a -> Maybe a
Just ((a :* b) -> c
f (a
a ,b
b'))
orMaybe (a :* b) -> c
f (a
_,b
_) (Just a
a',Just b
b') = c -> Maybe c
forall a. a -> Maybe a
Just ((a :* b) -> c
f (a
a',b
b'))

atomicD2 :: (Atomic a, Atomic b, Atomic c) => (a :* b -> c) -> (a :* b) -> (a :* b -#> c)
atomicD2 :: forall a b c.
(Atomic a, Atomic b, Atomic c) =>
((a :* b) -> c) -> (a :* b) -> (a :* b) -#> c
atomicD2 (a :* b) -> c
f a :* b
dab = Rep ((a :* b) -#> c) -> (a :* b) -#> c
forall a. HasRep a => Rep a -> a
abst (Rep ((a :* b) -#> c) -> (a :* b) -#> c)
-> Rep ((a :* b) -#> c) -> (a :* b) -#> c
forall a b. (a -> b) -> a -> b
$ Rep (Rep ((a :* b) -#> c)) -> Rep ((a :* b) -#> c)
forall a. HasRep a => Rep a -> a
abst (Rep (Rep ((a :* b) -#> c)) -> Rep ((a :* b) -#> c))
-> Rep (Rep ((a :* b) -#> c)) -> Rep ((a :* b) -#> c)
forall a b. (a -> b) -> a -> b
$ (Rep (Del (a :* b)) -> Rep (Del c)) -> Del (a :* b) -> Del c
forall p q. (HasRep p, HasRep q) => (Rep p -> Rep q) -> p -> q
inAbst ((Rep (Del (a :* b)) -> Rep (Del c)) -> Del (a :* b) -> Del c)
-> (Rep (Del (a :* b)) -> Rep (Del c)) -> Del (a :* b) -> Del c
forall a b. (a -> b) -> a -> b
$ ((a :* b) -> c)
-> (a :* b) -> (AtomDel a :* AtomDel b) -> AtomDel c
forall a b c.
((a :* b) -> c) -> (a :* b) -> (Maybe a :* Maybe b) -> Maybe c
orMaybe (a :* b) -> c
f a :* b
dab

#if 0

                    orMaybe f dab    :: Maybe a :* Maybe b -> Maybe c
                                     :: Delta (a :* b) -> Delta c
            inAbst (orMaybe f dab)   :: Del (a :* b) -> Del c
      abst (inAbst (orMaybe f dab))  :: Del (a :* b) -+> Del c
abst (abst (inAbst (orMaybe f dab))) :: (a :* b) -#> c
#endif

-- instance Atomic a => ScalarCat (-#>) a where
--   scale s = atomicD1 (* s)

atomic1 :: (Atomic a, Atomic b) => (a -> b) -> GD (-#>) a b
atomic1 :: forall a b. (Atomic a, Atomic b) => (a -> b) -> GD (-#>) a b
atomic1 a -> b
f = (a -> b :* ConstObj (->) (a -#> b)) -> GD (-#>) a b
forall (k :: * -> * -> *) a b. (a -> b :* k a b) -> GD k a b
D (a -> b
f (a -> b)
-> (a -> ConstObj (->) (a -#> b))
-> a
-> b :* ConstObj (->) (a -#> b)
forall (k :: * -> * -> *) a c d.
(MProductCat k, Ok3 k a c d) =>
k a c -> k a d -> k a (Prod k c d)
&&& ConstObj (->) (a -#> b) -> a -> ConstObj (->) (a -#> b)
forall a.
Ok (->) a =>
ConstObj (->) (a -#> b) -> a -> ConstObj (->) (a -#> b)
forall (k :: * -> * -> *) b a. (ConstCat k b, Ok k a) => b -> k a b
const ((a -> b) -> ConstObj (->) (a -#> b)
forall a b. (Atomic a, Atomic b) => (a -> b) -> a -#> b
atomicD1 a -> b
f))

atomic2 :: (Atomic a, Atomic b, Atomic c) => (a :* b -> c) -> GD (-#>) (a :* b) c
atomic2 :: forall a b c.
(Atomic a, Atomic b, Atomic c) =>
((a :* b) -> c) -> GD (-#>) (a :* b) c
atomic2 (a :* b) -> c
f = ((a :* b) -> c :* ((a :* b) -#> c)) -> GD (-#>) (a :* b) c
forall (k :: * -> * -> *) a b. (a -> b :* k a b) -> GD k a b
D ((a :* b) -> c
f ((a :* b) -> c)
-> ((a :* b) -> (a :* b) -#> c)
-> (a :* b)
-> c :* ((a :* b) -#> c)
forall (k :: * -> * -> *) a c d.
(MProductCat k, Ok3 k a c d) =>
k a c -> k a d -> k a (Prod k c d)
&&& ((a :* b) -> c) -> (a :* b) -> (a :* b) -#> c
forall a b c.
(Atomic a, Atomic b, Atomic c) =>
((a :* b) -> c) -> (a :* b) -> (a :* b) -#> c
atomicD2 (a :* b) -> c
f)

instance {-# overlapping #-} (Num s, Additive s, Atomic s) => NumCat Inc s where
  negateC :: Inc s s
negateC = (s -> s) -> Inc s s
forall a b. (Atomic a, Atomic b) => (a -> b) -> GD (-#>) a b
atomic1 s -> s
forall (k :: * -> * -> *) a. NumCat k a => k a a
negateC
  addC :: Inc (Prod Inc s s) s
addC    = (Prod Inc s s -> s) -> Inc (Prod Inc s s) s
forall a b c.
(Atomic a, Atomic b, Atomic c) =>
((a :* b) -> c) -> GD (-#>) (a :* b) c
atomic2 Prod Inc s s -> s
forall (k :: * -> * -> *) a. NumCat k a => k (Prod k a a) a
addC
  subC :: Inc (Prod Inc s s) s
subC    = (Prod Inc s s -> s) -> Inc (Prod Inc s s) s
forall a b c.
(Atomic a, Atomic b, Atomic c) =>
((a :* b) -> c) -> GD (-#>) (a :* b) c
atomic2 Prod Inc s s -> s
forall (k :: * -> * -> *) a. NumCat k a => k (Prod k a a) a
subC
  mulC :: Inc (Prod Inc s s) s
mulC    = (Prod Inc s s -> s) -> Inc (Prod Inc s s) s
forall a b c.
(Atomic a, Atomic b, Atomic c) =>
((a :* b) -> c) -> GD (-#>) (a :* b) c
atomic2 Prod Inc s s -> s
forall (k :: * -> * -> *) a. NumCat k a => k (Prod k a a) a
mulC
  powIC :: Ok Inc Int => Inc (Prod Inc s Int) s
powIC   = [Char] -> Inc (Prod Inc s Int) s
forall a. HasCallStack => [Char] -> a
error [Char]
"powIC: not yet defined on IF"
  {-# INLINE negateC #-}
  {-# INLINE addC #-}
  {-# INLINE subC #-}
  {-# INLINE mulC #-}
  {-# INLINE powIC #-}


{--------------------------------------------------------------------
    "Differentiation" interface
--------------------------------------------------------------------}

andInc :: forall a b . (a -> b) -> (a -> b :* (Delta a -> Delta b))
andInc :: forall a b. (a -> b) -> a -> b :* (Delta a -> Delta b)
andInc a -> b
f = (((b :* (a -#> b)) -> b :* (Delta a -> Delta b))
-> (a -> b :* (a -#> b)) -> a -> b :* (Delta a -> Delta b)
forall b c a. (b -> c) -> (a -> b) -> a -> c
result(((b :* (a -#> b)) -> b :* (Delta a -> Delta b))
 -> (a -> b :* (a -#> b)) -> a -> b :* (Delta a -> Delta b))
-> (((a -#> b) -> Delta a -> Delta b)
    -> (b :* (a -#> b)) -> b :* (Delta a -> Delta b))
-> ((a -#> b) -> Delta a -> Delta b)
-> (a -> b :* (a -#> b))
-> a
-> b :* (Delta a -> Delta b)
forall b c a. Ok3 (->) a b c => (b -> c) -> (a -> b) -> a -> c
forall (k :: * -> * -> *) b c a.
(Category k, Ok3 k a b c) =>
k b c -> k a b -> k a c
.((a -#> b) -> Delta a -> Delta b)
-> (b :* (a -#> b)) -> b :* (Delta a -> Delta b)
forall a b b'.
Ok3 (->) a b b' =>
(b -> b') -> Prod (-#>) a b -> Prod (-#>) a b'
forall (k :: * -> * -> *) a b b'.
(MonoidalPCat k, Ok3 k a b b') =>
k b b' -> k (Prod (-#>) a b) (Prod (-#>) a b')
second) ((Del a -> Del b) -> Rep (Del a) -> Rep (Del b)
(Del a -> Del b) -> Delta a -> Delta b
forall p q. (HasRep p, HasRep q) => (p -> q) -> Rep p -> Rep q
inRepr((Del a -> Del b) -> Delta a -> Delta b)
-> ((a -#> b) -> Del a -> Del b) -> (a -#> b) -> Delta a -> Delta b
forall b c a. Ok3 (->) a b c => (b -> c) -> (a -> b) -> a -> c
forall (k :: * -> * -> *) b c a.
(Category k, Ok3 k a b c) =>
k b c -> k a b -> k a c
.Rep (a -#> b) -> Rep (Rep (a -#> b))
Rep (a -#> b) -> Del a -> Del b
forall a. HasRep a => a -> Rep a
repr(Rep (a -#> b) -> Del a -> Del b)
-> ((a -#> b) -> Rep (a -#> b)) -> (a -#> b) -> Del a -> Del b
forall b c a. Ok3 (->) a b c => (b -> c) -> (a -> b) -> a -> c
forall (k :: * -> * -> *) b c a.
(Category k, Ok3 k a b c) =>
k b c -> k a b -> k a c
.(a -#> b) -> Rep (a -#> b)
forall a. HasRep a => a -> Rep a
repr) (Inc a b -> Rep (Inc a b)
forall a. HasRep a => a -> Rep a
repr (forall (k :: * -> * -> *) a b. (a -> b) -> k a b
A.toCcc @Inc a -> b
f))
{-# INLINE andInc #-}

--                                     toCcc @Inc f         :: GD (-#>) a b
--                              repr  (toCcc @Inc f)        :: a -> b :* (a -#> b)
-- (result.second)              repr  (repr (toCcc @Inc f)) :: a -> b :* (Del a -+> Del b)
-- (result.second) (       repr.repr) (repr (toCcc @Inc f)) :: a -> b :* (Del a -> Del b)
-- (result.second) (inRepr.repr.repr) (repr (toCcc @Inc f)) :: a -> b :* (Delta a -> Delta b)

inc :: forall a b . (a -> b) -> (a -> Delta a -> Delta b)
inc :: forall a b. (a -> b) -> a -> Delta a -> Delta b
inc a -> b
f = ((b, Delta a -> Delta b) -> Delta a -> Delta b)
-> (a -> (b, Delta a -> Delta b)) -> a -> Delta a -> Delta b
forall b c a. (b -> c) -> (a -> b) -> a -> c
result (b, Delta a -> Delta b) -> Delta a -> Delta b
forall a b. (a, b) -> b
snd ((a -> b) -> a -> (b, Delta a -> Delta b)
forall a b. (a -> b) -> a -> b :* (Delta a -> Delta b)
andInc a -> b
f)
{-# INLINE inc #-}