Generic Programming With DataKinds

Generic.lhs

> {-# LANGUAGE DataKinds, GADTs, TypeFamilies, TypeOperators #-}

> import Prelude hiding (Functor, succ)

> infixl 1 :+
> infixl 2 :.

> data Type = Unit | (:+) Type Type | (:.) Type Type | Rec Functor

> infixl 1 :++
> infixl 2 :..

> data Functor = K Type | I | (:++) Functor Functor | (:..) Functor Functor

> infixl 0 :$

> type family (:$) (fu :: Functor) (ty :: Type) :: Type

> type instance K ty :$ t = ty

> type instance I :$ ty = ty

> type instance (f1 :++ f2) :$ t = (f1 :$ t) :+ (f2 :$ t)

> type instance (f1 :.. f2) :$ t = (f1 :$ t) :. (f2 :$ t)

> data Data ty where
>   Unique :: Data Unit
>   Inl :: Data t1 -> Data (t1 :+ t2)
>   Inr :: Data t2 -> Data (t1 :+ t2)
>   Split :: Data t1 -> Data t2 -> Data (t1 :. t2)
>   In :: Data (f :$ Rec f) -> Data (Rec f)

> type Nat = Rec (K Unit :++ I)

> nil :: Data (Rec (K Unit :++ f))
> nil = In (Inl Unique)

> succ :: Data Nat -> Data Nat
> succ = In . Inr

> type List t = Rec (K Unit :++ K t :.. I)

> cons :: Data ty -> Data (List ty) -> Data (List ty)
> cons = curry $ In . Inr . uncurry Split

> sizeOf :: Data a -> Int
> sizeOf Unique = 0
> sizeOf (Inl x) = 1 + sizeOf x
> sizeOf (Inr x) = 1 + sizeOf x
> sizeOf (Split x y) = sizeOf x + sizeOf y
> sizeOf (In x) = sizeOf x

> eq :: Data a -> Data a -> Bool
> eq Unique Unique = True
> eq (Inl x) (Inl y) = eq x y
> eq (Inr x) (Inr y) = eq x y
> eq (Split x y) (Split z w) = eq x z && eq y w
> eq (In x) (In y) = eq x y
> eq _ _ = False