T11754.hs 765 Bytes
Newer Older
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28
{-# LANGUAGE TypeOperators, UndecidableSuperClasses, KindSignatures,
TypeFamilies, FlexibleContexts #-}

module T11754 where

import Data.Kind
import Data.Void

newtype K a x = K a
newtype I   x = I x

data (f + g) x = L (f x) | R (g x)
data (f × g) x = f x :×: g x

class Differentiable (D f) => Differentiable f where
  type D (f :: Type -> Type) :: Type -> Type

instance Differentiable (K a) where
  type D (K a) = K Void

instance Differentiable I where
  type D I = K ()

instance (Differentiable f, Differentiable f) => Differentiable (f + f) where
  type D (f + f) = D f + D f

instance (Differentiable f, Differentiable f) => Differentiable (f × f) where
  type D (f × f) = (D f × f) + (f × D f)