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

head

tail

Length

the same as hAppend

hAppend' below is implemented using the same idea

Alternative implementation of hAppend. Demonstrates HFoldr

Note:

x :: HList a

means: forall a. x :: HList a

hEnd x

means: exists a. x :: HList a

List termination

Building lists

like foldl

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

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

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

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 ('[] *)))

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.

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)

Same as hMap only a different implementation.

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

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

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.

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:

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.

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

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

It is a pure type-level operation

could be an associated type if HEq had one

Same as hMapOut Id

the same as map Just

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

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

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

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

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

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