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.

Reaganreagen

I haven't seen one either. I've worked on something like that a while ago, but I never had it in a form where I felt like it should be uploaded. Also, you can run into some weird corners of the type system exploring this. – Octopus

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
  

Cygnus

A related question, is "Exists" anywhere? I've uploaded "polydata" which is basically "Exists", but I might as well someone else's package if it already exists to save duplication hackage.haskell.org/package/polydata-0.1.0.0/docs/… – Reaganreagen

It's old but searching around there appears to be a package called exists... – Cygnus

Oh hang on, Exists and Poly are different. – Reaganreagen

@Cygnus To construct Exists c you need to find a single example a such that c a. To construct Poly c you must show that an a exists for all a such that c a. I think the terminology is Exists is "existentially quantified" and Poly is "universally quantified". – Engle

@Engle thanks! The haddock was tripping me up. Looking at the source code, I see what you mean. – Cygnus

I asked about whether your Exists type is in a library somewhere on IRC some time ago (conversation starts around 21:34). At that time nobody knew of a place that offered it, but folks did suggest some cute ideas. – Expulsive

Why not use a type family to build the constraint All c as (All c '[] = (); All c (a ': as) = (c a, All c as)) rather than converting from Hlist as to [Exist c] which makes you lose information about the as? – Theola

@Theola Just a matter of taste. The problem with doing that is how to use 'All' afterwards. – Cygnus

@Theola Note that ForallC as c also holds exactly when All c as holds too - its just also lets you do something with that information. – Cygnus

I don't see why you wouldn't be able to do something with All c as. You'd access constraints just like you access values in an HList: using an index. – Theola

@Theola I'm not sure I see what you mean, but I wish I did because it sounds interesting. Do you have some example somewhere of how this works for All (or something similar)? – Cygnus

What about something like this? gist.github.com/gallais/48b6dba11b1fd57d4a7386cfe502ff94 – Theola

@Theola Thanks! I see what you mean now. :) – Cygnus

I would argue that a type family All makes it much easier to actually use the constraints in practice than using just a type class. There's then no reason to first compute some term-level form where dictionaries are attached to values. – Noland

Quick update: a reddit post suggests the exists package for your Exists type. – Expulsive

@DanielWagner That package was already linked to in the second comment. :) – Cygnus

@Cygnus Yeesh, I must be blind! – Expulsive

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.

Noland

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.

Engle

As discussed in the other answers, I think you'd be somewhat better off with turning All into a type family and not explicitly computing the dicts, but just using them directly. For this purpose, generics-sop offers "constrained" versions of functions such as your zipHKList that can use and distribute an All constraint over the elements. – Noland