-- Based on http://conal.net/blog/posts/differentiation-of-higher-order-types/

-- Single definitions giving both ADTs and ADKs (etc.) for objects
-- and functions:
data Obj :: level n. *n where
  Void :: Obj
  Unit :: Obj
  Sum :: Obj ~> Obj ~> Obj
  Prod :: Obj ~> Obj ~> Obj

data Fun :: level n. *n where
  Const :: Obj ~> Fun
  Id :: Fun
  SumF :: Fun ~> Fun ~> Fun
  ProdF :: Fun ~> Fun ~> Fun
  Comp :: Fun ~> Fun ~> Fun

-- Differentation on values:
der :: Fun -> Fun
der Id = Const Unit
der (Const x) = Const Void
der (SumF f g) = SumF (der f) (der g)
der (ProdF f g) = SumF (ProdF (der f) g) (ProdF f (der g))
der (Comp g f) = ProdF (Comp (der g) f) (der f)

-- Differentation on types, kinds etc:
der' :: level a. Fun_(1+a) ~> Fun_(1+a)
{der' Id} = Const Unit
{der' (Const x)} = Const Void
{der' (SumF f g)} = SumF {der' f} {der' g}
{der' (ProdF f g)} = SumF (ProdF {der' f} g) (ProdF f {der' g})
{der' (Comp g f)} = ProdF (Comp {der' g} f) {der' f}

{- (Would be great if one could write
      der :: level a. Fun_(a) ~> Fun_(a)
   and get der and der' as one function but unfortunately this doesn't compile. -}