Limited heterogeneous list

Question

I was looking for Hackage and couldn't find anything like it, but it seems to be pretty simple and useful. Is there a library that contains a data type?

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

All found HList can be of any type and were not limited.

If I will not upload my own.

Answer 1

I am not sure if this data type is useful ...

• If you really want a be existentially qualified, I think you should use regular lists. The more interesting data type here will be Exists , although I'm sure there are options for all of this package Hackage already:

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

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

• On the other hand, if you do not want a in (:-) :: ca => a -> HList c be existentially qualified (if it ignores the HList point as such), you should instead define the following:

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

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

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

Answer 2

The generics-sop offers this out of the box.

A varied list can be defined in generics-sop using

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

and its instance for the constructor of the identical type I (from generics-sop ) or Identity (from Data.Functor.Identity ).

The library then offers an All constraint such that, for example,

 All Show xs => NP I xs 

is a type of heterogeneous list in which all contained types are in the Show class. It’s clear that All is a type family that computes a constraint for each element in the list of type types:

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

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

In addition, the library offers all kinds of functions that cross and transform the NP , taking into account the general restriction.

Answer 3

What do you really want

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

What you can use as a regular heterogeneous list

 type HList = HKList Identity 

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

 HKList ((,) e) 

Or with additional information recorded in the dictionary

 data Has ca where Has :: ca => a -> Has ca type ConstrainedList c = HKList (Has c) 

Or save lists of only fixed restrictions

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

What can you use to determine the idea of ​​an entire list of types that satisfy the constraint

 class All c xs where dicts :: HKList (Dict1 c) xs instance All c '[] where dicts = Nil instance (All c xs, cx) => All c (x ': xs) where dicts = Dict1 :* dicts 

Or anything else you can do with good k -> *

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

 zipHKList :: (forall k. fk -> gk -> hk) -> HKList f xs -> HKList g xs -> HKList h xs zipHKList _ Nil Nil = Nil zipHKList f (x :* xs) (y :* ys) = fxy :* zipHKList f xs ys allToHas :: All c xs => HKList Identity xs -> HKList (Has c) xs allToHas xs = zipHKList f dicts xs where f :: Dict1 ck -> Identity k -> Has ck 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 wrote this several times earlier for various projects, but I did not know that it was in the library anywhere until Cosmicus indicated that it was in generics-sop .