DerivativesOfTypes.hs

{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}

main = print ()

-- generic types
data Zero r
data One r = Unit
data X r = Rec r
data K a r = Wrap a
data (f :+: g) r = InjL (f r) | InjR (g r)
data (f :*: g) r = f r :.: g r

-- lets you do anonymous types just like
--   js lets you have anonymous functions
-- function foo() { ... }
-- function () { ... }

type family Deriv (f :: * -> *) :: * -> *
type instance Deriv Zero  = Zero
type instance Deriv One   = Zero
type instance Deriv (K a) = Zero
type instance Deriv X     = One
type instance Deriv (f :+: g) =
  Deriv f :+: Deriv g
type instance Deriv (f :*: g) =
  (Deriv f :*: g) :+: (f :*: Deriv g)



data BinF r = T | F
type BinF' = One :+: One -- aka Two!

data BinFDeriv r
type BinFDeriv' = Zero
type DerivBinF'' = Deriv BinF'

data NatF r = Ze | Suc r
type NatF' = One :+: X -- 1 + x

data NatFDeriv r = InSuc
type NatFDeriv' = One -- 1
type NatFDeriv'' = Deriv NatF'

data ListF a r = Nil | Cons a r
type ListF' a = One :+: (K a :*: X)
  -- 1 + a*x

data ListFDeriv a r = InCons a
type ListFDeriv' a = K a
  -- a
type ListFDeriv'' a = Deriv (ListF' a)

ex :: ListFDeriv'' Bool String
ex = _

data TreeF a r = Leaf a | Branch r r
type TreeF' a = K a :+: (X :*: X)
  -- a + x*x

data TreeFDeriv a r = InBranchL r
                    | InBranchR r
type TreeFDeriv' a = X :+: X
type TreeFDeriv'' a = Deriv (TreeF' a)
  -- x + x{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}

main = print ()

-- generic types
data Zero r
data One r = Unit
data X r = Rec r
data K a r = Wrap a
data (f :+: g) r = InjL (f r) | InjR (g r)
data (f :*: g) r = f r :.: g r

-- lets you do anonymous types just like
--   js lets you have anonymous functions
-- function foo() { ... }
-- function () { ... }

type family Deriv (f :: * -> *) :: * -> *
type instance Deriv Zero  = Zero
type instance Deriv One   = Zero
type instance Deriv (K a) = Zero
type instance Deriv X     = One
type instance Deriv (f :+: g) =
  Deriv f :+: Deriv g
type instance Deriv (f :*: g) =
  (Deriv f :*: g) :+: (f :*: Deriv g)



data BinF r = T | F
type BinF' = One :+: One -- aka Two!

data BinFDeriv r
type BinFDeriv' = Zero
type DerivBinF'' = Deriv BinF'

data NatF r = Ze | Suc r
type NatF' = One :+: X -- 1 + x

data NatFDeriv r = InSuc
type NatFDeriv' = One -- 1
type NatFDeriv'' = Deriv NatF'

data ListF a r = Nil | Cons a r
type ListF' a = One :+: (K a :*: X)
  -- 1 + a*x

data ListFDeriv a r = InCons a
type ListFDeriv' a = K a
  -- a
type ListFDeriv'' a = Deriv (ListF' a)

ex :: ListFDeriv'' Bool String
ex = _

data TreeF a r = Leaf a | Branch r r
type TreeF' a = K a :+: (X :*: X)
  -- a + x*x

data TreeFDeriv a r = InBranchL r
                    | InBranchR r
type TreeFDeriv' a = X :+: X
type TreeFDeriv'' a = Deriv (TreeF' a)
  -- x + x