Fold over a heterogeneous, compile time, list

Question

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
#-}

Answer 1

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 foralls 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' d@DCons (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' d@DCons (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