Heterogeneous, compile time, list

Question

I have a list of heterogeneous types (or at least what I mean):

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

Now, given input type b , I want to go through all the Bits plates with type b and sum them, ignoring the other plates with type b' /= b :

 class Monoid r => EncodeBit br | b -> r where encodeBit :: b -> r class AbstractFoldable aMulti r where manyFold :: r -> aMulti -> r instance (EncodeBit br, 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 does not want anything. And not without reason, since both copies of the ad have the same head. Question: What is the correct way to fold over Bits with an arbitrary type?

Note: the above example is compiled with

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

Answer 1

Responding to your comment:

In fact, I can do it if I can filter a heterogeneous list by type. Is it possible?

You can filter a heterogeneous list by type if you add a Typeable constraint to b .

The basic idea is that we will use Data.Typeable cast :: (Typeable a, Typeable b) => a -> Maybe b to determine if each item in the list has a specific type. For each item in the list, a Typeable constraint is Typeable . Instead of creating a new list type with this built-in restriction, we will be able to check whether the All types in the list correspond to some restrictions.

Our goal is to make the next exit of the program [True,False] , filtering a heterogeneous list only for its Bool elements. I will continue to post language extensions and imports with the first snippet they need 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 pretty 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 in a heterogeneous Typeable list, get a list of those things of a particular Typeable type.

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

To do this, we need to develop the concept of All things in the list of types that satisfy some restriction. We will store the dictionaries for satisfied constraints in GADT , which either captures the constraint constraint and constraint dictionary for the All tail, or proves that the list is empty. The list of types satisfies the restriction for All elements if we can write dictionaries for it.

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

DList does have a list of dictionaries. DCons captures a dictionary for the constraint applied to the head element ( ctx h ), and all dictionaries for the rest of the list ( All ctx t ). We cannot get tail dictionaries 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 that applies to all its elements.

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

If the head of the list satisfies the constraint and the whole tail also, then everything in the list satisfies the constraint.

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

Now we can write ofType , which requires forall for scope 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 xt) = maybeToList (cast x) ++ ofType' (dtail d) t ofType' DNil HNil = [] 

We HList along with our dictionaries using maybeToList . cast maybeToList . cast and concatenate the results. We can make this explicit with RankNTypes .

 {-# LANGUAGE RankNTypes #-} import Data.Monoid (Monoid, (<>), mempty) zipDHWith :: forall cwl p. (All cl, Monoid w) => (forall a. (ca) => a -> w) -> pc -> HList l -> w zipDHWith fpl = zipDHWith' (allDict pl) l where zipDHWith' :: forall l. (All cl) => DList cl -> HList l -> w zipDHWith' d@DCons (HCons xt) = fx <> 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