I have a list of heterogeneous types (or at least that's what I have in mind):

```
data Nul
data Bits b otherBits where
BitsLst :: b -> otherBits -> Bits b otherBits
NoMoreBits :: Bits b Nul
```

Now, given an input type `b`

, I want to go through all the slabs of `Bits`

with type `b`

and summarize them, ignoring other slabs with type `b' /= b`

:

```
class Monoid r => EncodeBit b r | b -> r where
encodeBit :: b -> r
class AbstractFoldable aMulti r where
manyFold :: r -> aMulti -> r
instance (EncodeBit b r, AbstractFoldable otherBits r) =>
AbstractFoldable (Bits b otherBits ) r where
manyFold r0 (BitsLst bi other) = manyFold (r0 `mappend` (encodeBit bi)) other
manyFold b0 NoMoreBits = b0
instance AbstractFoldable otherBits r =>
AbstractFoldable (Bits nb otherBits ) r where
manyFold r0 (BitsLst _ other) = manyFold r0 other
manyFold b0 NoMoreBits = b0
```

But the compiler wants none of it. And with good reason, since both instance declarations have the same head. Question: what is the correct way of folding over `Bits`

with an arbitrary type?

Note: the above example is compiled with

```
{-# LANGUAGE MultiParamTypeClasses,
FunctionalDependencies,
GADTs,
DataKinds,
FlexibleInstances,
FlexibleContexts
#-}
```

# Best How To :

Answering your comment:

Actually, I can do if I can filter the heterogeneous list by type. Is that possible?

You can filter the heterogeneous list by type if you add a `Typeable`

constraint to `b`

.

The main idea is we will use `Data.Typeable`

's `cast :: (Typeable a, Typeable b) => a -> Maybe b`

to determine if each item in the list is of a certain type. This will require a `Typeable`

constraint for each item in the list. Instead of building a new list type with this constraint built in, we will make the ability to check if `All`

types in a list meet some constraint.

Our goal is to make the following program output `[True,False]`

, filtering a heterogeneous list to only its `Bool`

elements. I will endevour to place the language extensions and imports with the first snippet they are needed for

```
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE TypeOperators #-}
example :: HList (Bool ': String ': Bool ': String ': '[])
example = HCons True $ HCons "Jack" $ HCons False $ HCons "Jill" $ HNil
main = do
print (ofType example :: [Bool])
```

`HList`

here is a fairly standard definition of a heterogeneous list in haskell using `DataKinds`

```
{-# LANGUAGE GADTs #-}
{-# LANGUAGE KindSignatures #-}
data HList (l :: [*]) where
HCons :: h -> HList t -> HList (h ': t)
HNil :: HList '[]
```

We want to write `ofType`

with a signature like "if `All`

things in a heterogeneous list are `Typeable`

, get a list of those things of a specific `Typeable`

type.

```
import Data.Typeable
ofType :: (All Typeable l, Typeable a) => HList l -> [a]
```

To do this, we need to develop the notion of `All`

things in a list of types satisfying some constraint. We will store the dictionaries for satisfied constraints in a `GADT`

that either captures both the head constraint dictionary and constraints for `All`

of the the tail or proves that the list is empty. A type list satisfies a constraint for `All`

it's items if we can capture the dictionaries for it.

```
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE ConstraintKinds #-}
-- requires the constraints† package.
-- Constraint is actually in GHC.Prim
-- it's just easier to get to this way
import Data.Constraint (Constraint)
class All (c :: * -> Constraint) (l :: [*]) where
allDict :: p1 c -> p2 l -> DList c l
data DList (ctx :: * -> Constraint) (l :: [*]) where
DCons :: (ctx h, All ctx t) => DList ctx (h ': t)
DNil :: DList ctx '[]
```

`DList`

really is a list of dictionaries. `DCons`

captures the dictionary for the constraint applied to the head item (`ctx h`

) and all the dictionaries for the remainder of the list (`All ctx t`

). We can't get the dictionaries for the tail directly from the constructor, but we can write a function that extracts them from the dictionary for `All ctx t`

.

```
{-# LANGUAGE ScopedTypeVariables #-}
import Data.Proxy
dtail :: forall ctx h t. DList ctx (h ': t) -> DList ctx t
dtail DCons = allDict (Proxy :: Proxy ctx) (Proxy :: Proxy t)
```

An empty list of types trivially satisfies any constraint applied to all of its items

```
instance All c '[] where
allDict _ _ = DNil
```

If the head of a list satisfies a constraint and all of the tail does too, then everything in the list satisfies the constraint.

```
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE UndecidableInstances #-}
instance (c h, All c t) => All c (h ': t) where
allDict _ _ = DCons
```

We can now write `ofType`

, which requires `forall`

s for scoping type variables with `ScopedTypeVariables`

.

```
import Data.Maybe
ofType :: forall a l. (All Typeable l, Typeable a) => HList l -> [a]
ofType l = ofType' (allDict (Proxy :: Proxy Typeable) l) l
where
ofType' :: forall l. (All Typeable l) => DList Typeable l -> HList l -> [a]
ofType' [email protected] (HCons x t) = maybeToList (cast x) ++ ofType' (dtail d) t
ofType' DNil HNil = []
```

We are zipping the `HList`

together with its dictionaries with `maybeToList . cast`

and concatenating the results. We can make that explicit with `RankNTypes`

.

```
{-# LANGUAGE RankNTypes #-}
import Data.Monoid (Monoid, (<>), mempty)
zipDHWith :: forall c w l p. (All c l, Monoid w) => (forall a. (c a) => a -> w) -> p c -> HList l -> w
zipDHWith f p l = zipDHWith' (allDict p l) l
where
zipDHWith' :: forall l. (All c l) => DList c l -> HList l -> w
zipDHWith' [email protected] (HCons x t) = f x <> zipDHWith' (dtail d) t
zipDHWith' DNil HNil = mempty
ofType :: (All Typeable l, Typeable a) => HList l -> [a]
ofType = zipDHWith (maybeToList . cast) (Proxy :: Proxy Typeable)
```

†constraints