Heterogeneous difference lists

HDList.hs

{-# LANGUAGE DataKinds #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE StandaloneKindSignatures #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}
module HDList where

import qualified Control.Category as Cat (Category(..))
import Data.Function (on)
import Data.Kind (Type)
import qualified HList as HList
import HList (HList(..), AllC, type (++))
import Prelude hiding (head)

type HDList :: [Type] -> [Type] -> Type
newtype HDList xs ys = UnsafeHDList { unsafeApplyHDList :: HList xs -> HList ys }

instance AllC Eq ys => Eq (HDList '[] ys) where
  (==) = (==) `on` toList

instance AllC Show ys => Show (HDList '[] ys) where
  showsPrec p hdl =
    showParen (p > 10) $
      showString "fromList " . shows (toList hdl)

instance Cat.Category HDList where
  id = empty
  (.) = append

fromList :: HList xs -> HDList ys (xs ++ ys)
fromList = UnsafeHDList . (HList.++)

toList :: HDList '[] ys -> HList ys
toList = ($ Nil) . unsafeApplyHDList

empty :: HDList xs xs
empty = UnsafeHDList id

singleton :: x -> HDList xs (x:xs)
singleton = UnsafeHDList . (:>)

cons :: y -> HDList xs ys -> HDList xs (y:ys)
cons x xs = UnsafeHDList $ (x :>) . unsafeApplyHDList xs

snoc :: HDList (x:xs) ys -> x -> HDList xs ys
snoc xs x = UnsafeHDList $ unsafeApplyHDList xs . (x :>)

append :: HDList ys zs -> HDList xs ys -> HDList xs zs
append xs ys = UnsafeHDList $ unsafeApplyHDList xs . unsafeApplyHDList ys

head :: HDList '[] (y:ys) -> y
head ys = case toList ys of
  y :> _ -> y

tail :: HDList '[] (y:ys) -> HList ys
tail ys = case toList ys of
  _ :> ys -> ys

HList.hs

{-# LANGUAGE DataKinds #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE StandaloneDeriving #-}
{-# LANGUAGE StandaloneKindSignatures #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}
module HList where

import Data.Kind (Constraint, Type)
import Prelude hiding ((++))

type HList :: [Type] -> Type
data HList xs where
  Nil :: HList '[]
  (:>) :: x -> HList xs -> HList (x:xs)
infixr 5 :>

deriving instance AllC Eq xs   => Eq (HList xs)
deriving instance AllC Show xs => Show (HList xs)

type AllC :: (k -> Constraint) -> [k] -> Constraint
type family AllC f xs where
  AllC _ '[]    = ()
  AllC f (x:xs) = (f x, AllC f xs)

type (++) :: [a] -> [a] -> [a]
type family xs ++ ys where
  '[]    ++ ys = ys
  (x:xs) ++ ys = x:(xs ++ ys)
infixr 5 ++

(++) :: HList xs -> HList ys -> HList (xs ++ ys)
Nil       ++ ys = ys
(x :> xs) ++ ys = x :> (xs ++ ys)