HList- Heterogeneous lists

Safe HaskellNone




The HList library

(C) 2004, Oleg Kiselyov, Ralf Laemmel, Keean Schupke

Basic declarations for typeful heterogeneous lists.

Excuse the unstructured haddocks: while there are many declarations here some are alternative implementations should be grouped, and the definitions here are analgous to many list functions in the Prelude.


Heterogeneous type sequences

The easiest way to ensure that sequences can only be formed with Nil and Cons is to use GADTs The kind [*] is list kind (lists lifted to types)

data HList l whereSource


HNil :: HList `[]` 
HCons :: e -> HList l -> HList (e : l) 


(HEq * e1 e b, HDeleteManyCase * b e1 e l l1) => HDeleteMany * e1 (HList (: * e l)) (HList l1) 
HDeleteMany k e (HList ([] *)) (HList ([] *)) 
(HOccurs e l, HProject l (HList l')) => HProject l (HList (: * e l')) 
(HOccurrence e (: * x y) l', HOccurs' e l') => HOccurs e (HList (: * x y)) 
HExtend e (HList l) 
~ [*] l' (HRevApp * l ([] *)) => HBuild' l (HList l') 
(ConvHList l, Eq (Prime l)) => Eq (HList l)

this comparison is two traversals

(Data x, Data (HList xs), Typeable (HList (: * x xs)), TypeablePolyK [*] (: * x xs)) => Data (HList (: * x xs)) 
TypeablePolyK [*] ([] *) => Data (HList ([] *)) 
(Show e, Show (HList l)) => Show (HList (: * e l)) 
Show (HList ([] *)) 
TypeRepsList (Record xs) => Typeable (HList xs) 
HProject (HList l) (HList ([] *)) 
HAppend (HList l1) (HList l2) 
ApplyAB f e e' => ApplyAB (MapCar f) (e, HList l) (HList (: * e' l)) 
Apply (FHUProj sel ns) (HList l, Proxy HNat (HSucc n)) => Apply (Proxy Bool False, FHUProj sel ns) (HList (: * e l), Proxy HNat n) 
Apply (Proxy Bool True, FHUProj sel ns) (HList (: * e l), Proxy HNat n) 
(~ * ch (Proxy Bool (HBoolEQ sel (KMember n ns))), Apply (ch, FHUProj sel ns) (HList (: * e l), Proxy HNat n)) => Apply (FHUProj sel ns) (HList (: * e l), Proxy HNat n) 
Apply (FHUProj sel ns) (HList ([] *), n) 
(~ * (HList (: * x y)) z, HZip3 xs ys zs) => HZip3 (: * x xs) (: * (HList y) ys) (: * z zs) 

Alternative representation

HNil' and HCons' are the older ADT-style. This has some advantages over the GADT:

data HNil' Source



data HCons' a b Source


HCons' a b 


(Eq a, Eq b) => Eq (HCons' a b) 
(TypeRepsList xs, Typeable x) => TypeRepsList (HCons' x xs) 

class UnPrime (Prime a) ~ a => ConvHList a whereSource

conversion between GADT (HList) and ADT (HNil' HCons') representations

Associated Types

type Prime a :: *Source

type UnPrime b :: [*]Source


prime :: HList a -> Prime aSource

unPrime :: Prime a -> HList aSource


ConvHList ([] *) 
ConvHList as => ConvHList (: * a as) 

Basic list functions

hHead :: HList (e : l) -> eSource

hTail :: HList (e : l) -> HList lSource

type family HLength x :: HNatSource



type family HAppendList l1 l2 :: [k]Source

hAppendList :: HList l1 -> HList l2 -> HList (HAppendList l1 l2)Source

the same as hAppend

Alternative append

append' :: [a] -> [a] -> [a]Source

hAppend' below is implemented using the same idea

hAppend' :: HFoldr FHCons v l r => HList l -> v -> rSource

Alternative implementation of hAppend. Demonstrates HFoldr

data FHCons Source




(~ * x (e, HList l), ~ * y (HList (: * e l))) => ApplyAB FHCons x y 

Historical append

The original HList code is included below. In both cases we had to program the algorithm twice, at the term and the type levels.

The class HAppend
 class HAppend l l' l'' | l l' -> l''
   hAppend :: l -> l' -> l''

The instance following the normal append
 instance HList l => HAppend HNil l l
   hAppend HNil l = l

 instance (HList l, HAppend l l' l'')
       => HAppend (HCons x l) l' (HCons x l'')
   hAppend (HCons x l) l' = HCons x (hAppend l l')

Reversing HLists

type family HRevApp l1 l2 :: [k]Source

hRevApp :: HList l1 -> HList l2 -> HList (HRevApp l1 l2)Source

hReverse :: HList l1 -> HList (HRevApp * l1 ([] *))Source

A nicer notation for lists

hEnd :: HList l -> HList lSource


x :: HList a
means: forall a. x :: HList a
hEnd x
means: exists a. x :: HList a

List termination

hBuild :: HBuild' `[]` r => rSource

Building lists

class HBuild' l r whereSource


hBuild' :: HList l -> rSource


~ [*] l' (HRevApp * l ([] *)) => HBuild' l (HList l') 
HBuild' (: * a l) r => HBuild' l (a -> r) 


The classes above allow the third (shortest) way to make a list (containing a,b,c) in this case

 list = a `HCons` b `HCons` c `HCons` HNil
 list = a .*. b .*. c .*. HNil
 list = hEnd $ hBuild a b c
>>> let x = hBuild True in hEnd x
>>> let x = hBuild True 'a' in hEnd x
H[True, 'a']
>>> let x = hBuild True 'a' "ok" in hEnd x
H[True, 'a', "ok"]


the show instance has since changed, but these uses of 'hBuild'/'hEnd' still work

 HList> let x = hBuild True in hEnd x
 HCons True HNil
 HList> let x = hBuild True 'a' in hEnd x
 HCons True (HCons 'a' HNil)
 HList> let x = hBuild True 'a' "ok" in hEnd x
 HCons True (HCons 'a' (HCons "ok" HNil))
 HList> hEnd (hBuild (Key 42) (Name "Angus") Cow (Price 75.5))
 HCons (Key 42) (HCons (Name "Angus") (HCons Cow (HCons (Price 75.5) HNil)))
 HList> hEnd (hBuild (Key 42) (Name "Angus") Cow (Price 75.5)) == angus



Consume a heterogenous list. GADTs and type-classes mix well

class HFoldr f v l r whereSource


hFoldr :: f -> v -> HList l -> rSource


~ * v v' => HFoldr f v ([] *) v' 
(ApplyAB f (e, r) r', HFoldr f v l r) => HFoldr f v (: * e l) r'

uses ApplyAB not Apply

class HScanr f z ls rs whereSource


hScanr :: f -> z -> HList ls -> HList rsSource


HScanr f z ([] *) (: * z ([] *)) 
(ApplyAB f (x, r) s, HScanr f z xs (: * r rs)) => HScanr f z (: * x xs) (: * s (: * r rs)) 

class HFoldr1 f l r whereSource


hFoldr1 :: f -> HList l -> rSource


(ApplyAB f (e, r) r', HFoldr1 f (: * e' l) r) => HFoldr1 f (: * e (: * e' l)) r'

uses ApplyAB not Apply

~ * v v' => HFoldr1 f (: * v ([] *)) v' 


class HFoldl f z xs r whereSource

like foldl

>>> hFoldl (uncurry $ flip (:)) [] (1 `HCons` 2 `HCons` HNil)


hFoldl :: f -> z -> HList xs -> rSource


~ * z z' => HFoldl f z ([] *) z' 
(~ * zx (z, x), ApplyAB f zx z', HFoldl f z' xs r) => HFoldl f z (: * x xs) r 


Produce a heterogenous list. Uses the more limited Apply instead of App since that's all that is needed for uses of this function downstream. Those could in principle be re-written.

hUnfold :: (Apply p s, HUnfold' p (ApplyR p s)) => p -> s -> HList (HUnfold p s)Source

type HUnfold p s = HUnfoldR p (ApplyR p s)Source

class HUnfold' p res whereSource

Associated Types

type HUnfoldR p res :: [*]Source


hUnfold' :: p -> res -> HList (HUnfoldR p res)Source


HUnfold' p HNothing 
(Apply p s, HUnfold' p (ApplyR p s)) => HUnfold' p (HJust (e, s)) 


class HLength (HReplicateR n e) ~ n => HReplicate n e whereSource


hReplicate :: Proxy n -> e -> HList (HReplicateR n e)Source


type family HReplicateR n e :: [k]Source

would be associated with HReplicate except we want it to work with e of any kind, not just * that you can put into a HList. An "inverse" of HLength


class HConcat a whereSource

Like concat but for HLists of HLists.

Works in ghci... puzzling as what is different in doctest (it isn't -XExtendedDefaultRules)

 hConcat $ hBuild (hBuild 1 2 3) (hBuild 'a' "abc")

H[1, 2, 3, a, abc]

Associated Types

type HConcatR a :: [*]Source


hConcat :: HList a -> HList (HConcatR a)Source


HConcat ([] *) 
(~ * x (HList t), HConcat xs) => HConcat (: * x xs) 

type family UnHList a :: [*]Source

traversing HLists

producing HList


It could be implemented with hFoldr, as we show further below

hMap :: (HMapAux f as' bs', SameLength' * * as' bs', SameLength' * * bs' as') => f -> HList as' -> HList bs'Source

hMap is written such that the length of the result list can be determined from the length of the argument list (and the other way around). Similarly, the type of the elements of the list is propagated in both directions too.

Excuse the ugly types printed. Unfortunately ghc (still?) shows types like '[a,b] using the actual constructors involved (':) a ((':) b '[]) (or even worse when the kind variables are printed).

>>> :set -XNoMonomorphismRestriction
>>> let xs = 1 .*. 'c' .*. HNil
>>> :t hMap (HJust ()) xs
hMap (HJust ()) xs
  :: Num y => HList ((':) * (HJust y) ((':) * (HJust Char) ('[] *)))

These 4 examples show that the constraint on the length (2 in this cae) can be applied before or after the hMap. That inference is independent of the direction that type information is propagated for the individual elements.

>>> let asLen2 xs = xs `asTypeOf` (undefined :: HList '[a,b])
>>> let lr xs = asLen2 (applyAB (HMap HRead) xs)
>>> let ls xs = asLen2 (applyAB (HMap HShow) xs)
>>> let rl xs = applyAB (HMap HRead) (asLen2 xs)
>>> let sl xs = applyAB (HMap HShow) (asLen2 xs)
>>> :t lr
  :: (Read y, Read y1) =>
     HList ((':) * String ((':) * String ('[] *)))
     -> HList ((':) * y ((':) * y1 ('[] *)))
>>> :t rl
  :: (Read y, Read y1) =>
     HList ((':) * String ((':) * String ('[] *)))
     -> HList ((':) * y ((':) * y1 ('[] *)))
>>> :t ls
  :: (Show y, Show y1) =>
     HList ((':) * y ((':) * y1 ('[] *)))
     -> HList ((':) * String ((':) * String ('[] *)))
>>> :t sl
  :: (Show y, Show y1) =>
     HList ((':) * y ((':) * y1 ('[] *)))
     -> HList ((':) * String ((':) * String ('[] *)))

newtype HMap f Source


HMap f 


HMapCxt f as bs as' bs' => ApplyAB (HMap f) as bs 

type HMapCxt f as bs as' bs' = (HMapAux f as' bs', as ~ HList as', bs ~ HList bs', SameLength as' bs')Source

class SameLength' es1 es2 Source

Ensure two lists have the same length. We do case analysis on the first one (hence the type must be known to the type checker). In contrast, the second list may be a type variable.


~ [k1] es2 ([] k1) => SameLength' k k1 ([] k) es2 
(SameLength' k k1 xs ys, ~ [k1] es2 (: k1 y ys)) => SameLength' k k1 (: k x xs) es2 

class (SameLength' x y, SameLength' y x) => SameLength x y Source

symmetrical version of SameLength'. Written as a class instead of

 type SameLength a b = (SameLength' a b, SameLength' b a)

since ghc expands type synonyms, but not classes (and it seems to have the same result)


(SameLength' k1 k x y, SameLength' k k1 y x) => SameLength k k1 x y 

class HMapAux f l r whereSource


hMapAux :: SameLength l r => f -> HList l -> HList rSource


HMapAux f ([] *) ([] *) 
(ApplyAB f e e', HMapAux f l l', SameLength * * l l') => HMapAux f (: * e l) (: * e' l') 

alternative implementation

currently broken

newtype MapCar f Source


MapCar f 


ApplyAB f e e' => ApplyAB (MapCar f) (e, HList l) (HList (: * e' l)) 

hMapMapCar :: HFoldr (MapCar f) (HList `[]`) l l' => f -> HList l -> l'Source

Same as hMap only a different implementation.

appEndo . mconcat . map Endo

hComposeList :: HFoldr Comp (a -> a) l (t -> a) => HList l -> t -> aSource

>>> let xs = length .*. (+1) .*. (*2) .*. HNil
>>> hComposeList xs "abc"


class (Applicative m, SameLength a b) => HSequence m a b | a -> b, m b -> a whereSource

A heterogeneous version of

 sequenceA :: (Applicative m) => [m a] -> m [a]

Only now we operate on heterogeneous lists, where different elements may have different types a. In the argument list of monadic values (m a_i), although a_i may differ, the monad m must be the same for all elements. That's why we needed Data.HList.TypeCastGeneric2 (currently (~)). The typechecker will complain if we attempt to use hSequence on a HList of monadic values with different monads.

The hSequence problem was posed by Matthias Fischmann in his message on the Haskell-Cafe list on Oct 8, 2006



>>> hSequence $ Just (1 :: Integer) `HCons` (Just 'c') `HCons` HNil
Just H[1, 'c']
>>> hSequence $  return 1 `HCons` Just  'c' `HCons` HNil
Just H[1, 'c']
>>> hSequence $ [1] `HCons` ['c'] `HCons` HNil
[H[1, 'c']]


hSequence :: HList a -> m (HList b)Source


Applicative m => HSequence m ([] *) ([] *) 
(~ (* -> *) m1 m, Applicative m, HSequence m as bs) => HSequence m (: * (m1 a) as) (: * a bs) 

newtype LiftA2 f Source


LiftA2 f 


(ApplyAB f (x, y) z, ~ * mz (m z), ~ * mxy (m x, m y), Applicative m) => ApplyAB (LiftA2 f) mxy mz 

alternative implementation

producing homogenous lists

map (no sequencing)

This one we implement via hFoldr

newtype Mapcar f Source


Mapcar f 


(~ * l [e'], ApplyAB f e e', ~ * el (e, l)) => ApplyAB (Mapcar f) el l 

type HMapOut f l e = HFoldr (Mapcar f) [e] l [e]Source

hMapOut :: forall f e l. HMapOut f l e => f -> HList l -> [e]Source


hMapM :: (Monad m, HMapOut f l (m e)) => f -> HList l -> [m e]Source

 mapM :: forall b m a. (Monad m) => (a -> m b) -> [a] -> m [b]

Likewise for mapM_.

See hSequence if the result list should also be heterogenous.

hMapM_ :: (Monad m, HMapOut f l (m ())) => f -> HList l -> m ()Source

GHC doesn't like its own type. hMapM_ :: forall m a f e. (Monad m, HMapOut f a (m e)) => f -> a -> m () Without explicit type signature, it's Ok. Sigh. Anyway, Hugs does insist on a better type. So we restrict as follows:

Type-level equality for lists (HEq)

Ensure a list to contain HNats only

type family HNats l :: [HNat]Source

We do so constructively, converting the HList whose elements are Proxy HNat to [HNat]. The latter kind is unpopulated and is present only at the type level.

Membership tests

class HMember e1 l b | e1 l -> bSource

Check to see if an HList contains an element with a given type This is a type-level only test


HMember k e1 ([] k) False 
(HEq k e1 e b, HMember' k b e1 l br) => HMember k e1 (: k e l) br 

class HMember' b0 e1 l b | b0 e1 l -> bSource


HMember k e1 l br => HMember' k False e1 l br 
HMember' k True e1 l True 

type family HMemberP pred e1 l :: BoolSource

type family HMemberP' pred e1 l pb :: BoolSource

hMember :: HMember e l b => Proxy e -> Proxy l -> Proxy bSource

Another type-level membership test

class HMemberM e1 l r | e1 l -> rSource

Check to see if an element e occurs in a list l If not, return 'Nothing If the element does occur, return 'Just l1 where l1 is a type-level list without e


HMemberM k e1 ([] k) (Nothing [k]) 
(HEq k e1 e b, HMemberM1 k b e1 (: k e l) res) => HMemberM k e1 (: k e l) res 

class HMemberM1 b e1 l r | b e1 l -> rSource


(HMemberM k e1 l r, HMemberM2 k r e1 (: k e l) res) => HMemberM1 k False e1 (: k e l) res 
HMemberM1 k True e1 (: k e l) (Just [k] l) 

class HMemberM2 b e1 l r | b e1 l -> rSource


HMemberM2 k (Nothing [k]) e1 l (Nothing [k]) 
HMemberM2 k (Just [k] l1) e1 (: k e l) (Just [k] (: k e l1)) 

Staged equality for lists

removed. use Typeable instead

Find an element in a set based on HEq

class HFind e l n | e l -> nSource

It is a pure type-level operation


(HEq k e1 e2 b, HFind' k b e1 l n) => HFind k e1 (: k e2 l) n 

class HFind' b e l n | b e l -> nSource


HFind' k True e l HZero 
HFind k e l n => HFind' k False e l (HSucc n) 

Membership test based on type equality

class HTMember e l b | e l -> bSource

could be an associated type if HEq had one


HTMember k e ([] *) False 
(HEq * e e' b, HTMember * e l b', ~ Bool (HOr b b') b'') => HTMember * e (: * e' l) b'' 

hTMember :: HTMember e l b => e -> HList l -> Proxy bSource

Intersection based on HTMember

class HTIntersect l1 l2 l3 | l1 l2 -> l3 whereSource


hTIntersect :: HList l1 -> HList l2 -> HList l3Source

Like intersect


HTIntersect ([] *) l ([] *) 
(HTMember * h l1 b, HTIntersectBool b h t l1 l2) => HTIntersect (: * h t) l1 l2 

class HTIntersectBool b h t l1 l2 | b h t l1 -> l2 whereSource


hTIntersectBool :: Proxy b -> h -> HList t -> HList l1 -> HList l2Source


HTIntersect t l1 l2 => HTIntersectBool False h t l1 l2 
HTIntersect t l1 l2 => HTIntersectBool True h t l1 (: * h l2) 

Turn a heterogeneous list into a homogeneous one

class HList2List l e whereSource

Same as hMapOut Id


hList2List :: HList l -> [e]Source


HList2List ([] *) e 
HList2List l e => HList2List (: * e l) e 

With HMaybe

Turn list in a list of justs

class ToHJust l l' | l -> l', l' -> l whereSource

the same as map Just

>>> toHJust (2 .*. 'a' .*. HNil)
H[HJust 2, HJust 'a']
>>> toHJust2 (2 .*. 'a' .*. HNil)
H[HJust 2, HJust 'a']


toHJust :: HList l -> HList l'Source


ToHJust ([] *) ([] *) 
ToHJust l l' => ToHJust (: * e l) (: * (HJust e) l') 

toHJust2 :: (HMapAux (HJust ()) as' bs', SameLength' * * as' bs', SameLength' * * bs' as') => HList as' -> HList bs'Source

alternative implementation. The Apply instance is in Data.HList.FakePrelude. A longer type could be inferred. toHJust2 :: (HMap' (HJust ()) a b) => HList a -> HList b

Extract justs from list of maybes

class FromHJust l whereSource

Associated Types

type FromHJustR l :: [*]Source


FromHJust ([] *) 
FromHJust l => FromHJust (: * (HJust e) l) 
FromHJust l => FromHJust (: * HNothing l) 

alternative implementation

fromHJust2 :: (HMapAux HFromJust as' bs', SameLength' * * as' bs', SameLength' * * bs' as') => HList as' -> HList bs'Source

A longer type could be inferred. fromHJust2 :: (HMap' HFromJust a b) => HList a -> HList b

data HFromJust Source




~ * hJustA (HJust a) => ApplyAB HFromJust hJustA a 

Annotated lists

data HAddTag t Source


HAddTag t 


~ * et (e, t) => ApplyAB (HAddTag t) e et 

data HRmTag Source




~ * e' e => ApplyAB HRmTag (e, t) e' 

hAddTag :: (HMapAux (HAddTag t) as' bs', SameLength' * * as' bs', SameLength' * * bs' as') => t -> HList as' -> HList bs'Source

hRmTag :: (HMapAux HRmTag as' bs', SameLength' * * as' bs', SameLength' * * bs' as') => HList as' -> HList bs'Source

hFlag :: (HMapAux (HAddTag (Proxy Bool True)) as' bs', SameLength' * * as' bs', SameLength' * * bs' as') => HList as' -> HList bs'Source

Annotate list with a type-level Boolean hFlag :: HMap' (HAddTag (Proxy True)) l r => HList l -> HList r

Splitting by HTrue and HFalse

class HSplit l whereSource

Analogus to Data.List.partition snd

>>> hSplit $ (2,hTrue) .*. (3,hTrue) .*. (1,hFalse) .*. HNil
(H[2, 3],H[1])

it might make more sense to instead have LVPair Bool e instead of (e, Proxy Bool) since the former has the same runtime representation as e

Associated Types

type HSplitT l :: [*]Source

type HSplitF l :: [*]Source


hSplit :: HList l -> (HList (HSplitT l), HList (HSplitF l))Source


HSplit ([] *) 
HSplit l => HSplit (: * (e, Proxy Bool False) l) 
HSplit l => HSplit (: * (e, Proxy Bool True) l)