Constrained heterogeneous list

Question

I searched Hackage and couldn't find anything like the following but it seems to be fairly simple and useful. Is there a library that contains sort of data type?

data HList c where
  (:-) :: c a => a -> HList c
  Nil :: HList c

All the HLists I found could have any type, and weren't constrained.

If there isn't I'll upload my own.

Answer 1

I'm not sure this data type is useful...

• If you really want a to be existentially qualified, I think you should use regular lists. The more interesting data type here would be Exists, although I'm certain there are variants of it all over package Hackage already:

  data Exists c where
    Exists :: c a => a -> Exists c
  

  Then, your HList c is isomorphic to [Exists c] and you can still use all of the usual list based functions.

• On the other hand, if you don't necessarily want a in the (:-) :: c a => a -> HList c to be existentially qualified (having it as such sort of defies the point of the HList), you should instead define the following:

  data HList (as :: [*]) where
    (:-) :: a -> HList as -> HList (a ': as)
    Nil :: HList '[]
  

  Then, if you want to require that all entries of the HList satisfy c, you can make a type class to witness the injection from HList as into [Exists c] whose instance resolution only works if all the types in the HList satisfy the constraint:

  class ForallC as c where
    asList :: HList as -> [Exists c]
  
  instance ForallC '[] c where
    asList Nil = []
  
  instance (c a, ForallC as c) => ForallC (a ': as) c where
    asList (x :- xs) = Exists x : asList xs
  

Answer 2

The generics-sop package offers this out of the box.

A heterogeneous list can be defined in generics-sop by using

data NP :: (k -> *) -> [k] -> * where
  Nil  :: NP f '[]
  (:*) :: f x -> NP f xs -> NP f (x ': xs)

and instantiating it to the identity type constructor I (from generics-sop) or Identity (from Data.Functor.Identity).

The library then offers the constraint All such that e.g.

All Show xs => NP I xs

is the type of a heterogeneous list where all contained types are in the Show class. Conceptually, All is a type family that computes the constraint for every element in a type-level list:

type family All (f :: k -> Constraint) (xs :: [k]) :: Constraint where
  All c '[]       = ()
  All c (x ': xs) = (c x, All c xs)

(Only that in the actual definition, All is additionally wrapped in a type class so that it can be partially applied.)

The library furthermore offers all sorts of functions that traverse and transform NPs given a common constraint.

Answer 3

What you really want is

data HKList :: (k -> *) -> [k] -> * where
  Nil  :: HKList f '[]
  (:*) :: f x -> HKList f xs -> HKList f (x ': xs)

Which you can use either as an ordinary heterogeneous list

type HList = HKList Identity

Or with extra information of some constant type e attached to each value (or other interesting functors)

HKList ((,) e)

Or with extra information captured in a dictionary

data Has c a where
    Has :: c a => a -> Has c a

type ConstrainedList c = HKList (Has c)

Or keep lists of only captured constraints

data Dict1 :: (k -> Constraint) -> k -> * where
  Dict1 :: c k => Dict1 c k

Which you can use to define the idea of all of a list of types satisfying a constraint

class All c xs where
  dicts :: HKList (Dict1 c) xs

instance All c '[] where
  dicts = Nil

instance (All c xs, c x) => All c (x ': xs) where
  dicts = Dict1 :* dicts

Or anything else you can do with a kind k -> *

You can freely convert between working with All c xs => HList xs and HKList (Has c) xs

zipHKList :: (forall k. f k -> g k -> h k) -> HKList f xs -> HKList g xs -> HKList h xs
zipHKList _ Nil Nil = Nil
zipHKList f (x :* xs) (y :* ys) = f x y :* zipHKList f xs ys

allToHas :: All c xs => HKList Identity xs -> HKList (Has c) xs
allToHas xs = zipHKList f dicts xs
  where
    f :: Dict1 c k -> Identity k -> Has c k
    f Dict1 (Identity x) = Has x

hasToAll :: HKList (Has c) xs -> Dict (All c xs)
hasToAll Nil = Dict
hasToAll (Has x :* xs) =
  case hasToAll xs of
    Dict -> Dict

full code

I've written this a few times before for various projects, but I didn't know it was in a library anywhere until Kosmikus pointed out that it's in generics-sop.