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

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 2

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