creates a HList of Proxies

Add Proxy to a type

>>> let x = undefined :: HList (AddProxy [Char,Int])
>>> :t x
x :: HList '[Proxy Char, Proxy Int]

inverse of AddProxy

head

tail

last

Length, but see HLengthEq instead

hAppend' below is implemented using the same idea

Alternative implementation of hAppend. Demonstrates HFoldr

a version of hReverse that does not allow the type information to flow backwards

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]

Sometimes the result type can fix the type of the first argument:

>>> hReplicate Proxy () :: HList '[ (), (), () ]
H[(),(),()]

However, with HReplicate all elements must have the same type, so it may be easier to use HList2List:

>>> list2HList (repeat 3) :: Maybe (HList [Int, Int, Int])
Just H[3,3,3]

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

HReplicate produces lists that can be converted to ordinary lists

>>> let two = hSucc (hSucc hZero)
>>> let f = Fun' fromInteger :: Fun' Num Integer

>>> :t applyAB f
applyAB f :: Num b => Integer -> b

>>> hReplicateF two f 3
H[3,3]

>>> hReplicateF Proxy f 3 :: HList [Int, Double, Integer]
H[3,3.0,3]

This function behaves like iterate, with an extra argument to help figure out the result length

>>> let three = hSucc (hSucc (hSucc hZero))
>>> let f = Fun Just :: Fun '() Maybe

>>> :t applyAB f
applyAB f :: a -> Maybe a

f is applied to different types:

>>> hIterate three f ()
H[(),Just (),Just (Just ())]

It is also possible to specify the length later on, as done with Prelude.iterate

>>> let take3 x | _ <- hLength x `asTypeOf` three = x
>>> take3 $ hIterate Proxy f ()
H[(),Just (),Just (Just ())]

Like concat but for HLists of HLists.

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

>>> let a = hEnd $ hBuild 1 2 3
>>> let b = hEnd $ hBuild 'a' "abc"
>>> hConcat $ hBuild a b
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.

>>> :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 case) 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 ..., Read ...) => HList '[String, String] -> HList '[..., ...]

>>> :t rl
rl
  :: (Read ..., Read ...) => HList '[String, String] -> HList '[..., ...]

>>> :t ls
ls
  :: (Show ..., Show ...) => HList '[..., ...] -> HList '[String, String]

>>> :t sl
sl
  :: (Show ..., Show ...) => HList '[..., ...] -> HList '[String, String]

hMap constrained to HList

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

hSequence2 is not recommended over hSequence since it possibly doesn't allow inferring argument types from the result types. Otherwise this version should do exactly the same thing.

The DataKinds version needs a little help to find the type of the return HNil, unlike the original version, which worked just fine as

hSequence l = hFoldr ConsM (return HNil) l

compare hMapOut f with hList2List . hMap f

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

The following is a similar type-only membership test It uses the user-supplied curried type equality predicate pred

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

hMapOut id is similar, except this function is restricted to HLists that actually contain a value (so the list produced will be nonempty). This restriction allows adding a functional dependency, which means that less type annotations can be necessary.

Prism [s] [t] (HList s) (HList t)

Prism' [a] (HList s)

where s ~ HReplicateR n a

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.

This implementation is shorter.

Annotate list with a type-level Boolean

hFlag :: HMapCxt (HAddTag (Proxy True)) l r => HList l -> HList r

Analogus to Data.List.partition snd. See also HPartition

>>> let (.=.) :: p x -> y -> Tagged x y; _ .=. y = Tagged y
>>> hSplit $ hTrue .=. 2 .*. hTrue .=. 3 .*. hFalse .=. 1 .*. 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

splitAt

setup

>>> let two = hSucc (hSucc hZero)
>>> let xsys = hEnd $ hBuild 1 2 3 4

If a length is explicitly provided, the resulting lists are inferred

>>> hSplitAt two xsys
(H[1,2],H[3,4])

>>> let sameLength_ :: SameLength a b => r a -> r b -> r a; sameLength_ = const
>>> let len2 x = x `sameLength_` HCons () (HCons () HNil)

If the first chunk of the list (a) has to be a certain length, the type of the Proxy argument can be inferred.

>>> case hSplitAt Proxy xsys of (a,b) -> (len2 a, b)
(H[1,2],H[3,4])

helper for HSplitAt

a better way to write HLength xs ~ n because:

1. it works properly with ghc-7.10 (probably another example of ghc bug #10009)
2. it works backwards a bit in that if n is known, then xs can be refined:

>>> undefined :: HLengthEq xs HZero => HList xs
H[]

HLengthGe xs n says that HLength xs >= n.

unlike the expression with a type family HLength, ghc assumes xs ~ (aFresh ': bFresh) when given a constraint HLengthGe xs (HSucc HZero)

HAppendList1 xs ys xsys is the type-level way of saying xs ++ ys == xsys

used by HSplitAt

analog of stripPrefix

Iso (HList v) (HList v') a b

Iso' (HList v) a

tails

inits