Data.HList.HList

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 where

Constructors

HNil :: HList `[]`

HCons :: e -> HList l -> HList (e : l)

Instances

(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:

• lazy pattern matches are allowed
• type inference is better if you want to directly pattern match see stackoverflow post here

data HNil'

Constructors

HNil'

Instances

Eq HNil'

TypeRepsList HNil'

data HCons' a b

Constructors

HCons' a b

Instances

(Eq a, Eq b) => Eq (HCons' a b)

(TypeRepsList xs, Typeable x) => TypeRepsList (HCons' x xs)

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

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

Associated Types

type Prime a :: *

type UnPrime b :: [*]

Methods

prime :: HList a -> Prime a

unPrime :: Prime a -> HList a

Instances

ConvHList ([] *)

ConvHList as => ConvHList (: * a as)

Basic list functions

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

head

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

tail

type family HLength x :: HNat

Length

hLength :: HList l -> Proxy (HLength l)

Append

type family HAppendList l1 l2 :: [k]

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

the same as hAppend

Alternative append

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

hAppend' below is implemented using the same idea

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

Alternative implementation of hAppend. Demonstrates HFoldr

data FHCons

Constructors

FHCons

Instances

(~ * 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''
  where
   hAppend :: l -> l' -> l''

The instance following the normal append

 instance HList l => HAppend HNil l l
  where
   hAppend HNil l = l

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

Reversing HLists

type family HRevApp l1 l2 :: [k]

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

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

A nicer notation for lists

hEnd :: HList l -> HList l

Note:

x :: HList a

means: forall a. x :: HList a

hEnd x

means: exists a. x :: HList a

List termination

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

Building lists

class HBuild' l r where

Methods

hBuild' :: HList l -> r

Instances

~ [*] l' (HRevApp * l ([] *)) => HBuild' l (HList l')

HBuild' (: * a l) r => HBuild' l (a -> r)

examples

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
H[True]

>>> let x = hBuild True 'a' in hEnd x
H[True, 'a']

>>> let x = hBuild True 'a' "ok" in hEnd x
H[True, 'a', "ok"]

historical

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
 True

folds

foldr

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

class HFoldr f v l r where

Methods

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

Instances

~ * 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 where

Methods

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

Instances

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 where

Methods

hFoldr1 :: f -> HList l -> r

Instances

(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'

foldl

class HFoldl f z xs r where

like foldl

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

Methods

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

Instances

~ * z z' => HFoldl f z ([] *) z'

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

unfold

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)

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

class HUnfold' p res where

Associated Types

type HUnfoldR p res :: [*]

Methods

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

Instances

HUnfold' p HNothing

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

replicate

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

Methods

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

Instances

HReplicate HZero e

HReplicate n e => HReplicate (HSucc n) e

type family HReplicateR n e :: [k]

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

concat

class HConcat a where

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 :: [*]

Methods

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

Instances

HConcat ([] *)

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

type family UnHList a :: [*]

traversing HLists

producing HList

map

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'

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
lr
  :: (Read y, Read y1) =>
     HList ((':) * String ((':) * String ('[] *)))
     -> HList ((':) * y ((':) * y1 ('[] *)))

>>> :t rl
rl
  :: (Read y, Read y1) =>
     HList ((':) * String ((':) * String ('[] *)))
     -> HList ((':) * y ((':) * y1 ('[] *)))

>>> :t ls
ls
  :: (Show y, Show y1) =>
     HList ((':) * y ((':) * y1 ('[] *)))
     -> HList ((':) * String ((':) * String ('[] *)))

>>> :t sl
sl
  :: (Show y, Show y1) =>
     HList ((':) * y ((':) * y1 ('[] *)))
     -> HList ((':) * String ((':) * String ('[] *)))

newtype HMap f

Constructors

HMap f

Instances

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')

class SameLength' es1 es2

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.

Instances

~ [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

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)

Instances

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

class HMapAux f l r where

Methods

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

Instances

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

Constructors

MapCar f

Instances

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

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

Same as hMap only a different implementation.

appEndo . mconcat . map Endo

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

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

sequence

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

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

http://www.haskell.org/pipermail/haskell-cafe/2006-October/018708.html

http://www.haskell.org/pipermail/haskell-cafe/2006-October/018784.html

Maybe

>>> 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']

List

>>> hSequence $ [1] `HCons` ['c'] `HCons` HNil
[H[1, 'c']]

Methods

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

Instances

Applicative m => HSequence m ([] *) ([] *)

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

newtype LiftA2 f

Constructors

LiftA2 f

Instances

(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

Constructors

Mapcar f

Instances

(~ * 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]

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

mapM

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

 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 ()

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]

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.

hNats :: HList l -> Proxy (HNats l)

Membership tests

class HMember e1 l b | e1 l -> b

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

Instances

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 -> b

Instances

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

HMember' k True e1 l True

type family HMemberP pred e1 l :: Bool

type family HMemberP' pred e1 l pb :: Bool

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

Another type-level membership test

class HMemberM e1 l r | e1 l -> r

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

Instances

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 -> r

Instances

(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 -> r

Instances

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 -> n

It is a pure type-level operation

Instances

(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 -> n

Instances

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 -> b

could be an associated type if HEq had one

Instances

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 b

Intersection based on HTMember

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

Methods

hTIntersect :: HList l1 -> HList l2 -> HList l3

Like intersect

Instances

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 where

Methods

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

Instances

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 where

Same as hMapOut Id

Methods

hList2List :: HList l -> [e]

Instances

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 where

the same as map Just

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

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

Methods

toHJust :: HList l -> HList l'

Instances

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'

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 where

Associated Types

type FromHJustR l :: [*]

Methods

fromHJust :: HList l -> HList (FromHJustR l)

Instances

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'

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

data HFromJust

Constructors

HFromJust

Instances

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

Annotated lists

data HAddTag t

Constructors

HAddTag t

Instances

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

data HRmTag

Constructors

HRmTag

Instances

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

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

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

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

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 where

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 :: [*]

type HSplitF l :: [*]

Methods

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

Instances

HSplit ([] *)

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

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