Skip to content

Instantly share code, notes, and snippets.

Embed
What would you like to do?
Heterogeneous difference lists
{-# 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
{-# 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)
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment