Liste hétérogène contrainte

Question

J'ai cherché Hackage et je n'ai pas pu trouver quelque chose comme ce qui suit, mais il semble être assez simple et utile. Y a-t-il une bibliothèque qui contient une sorte de type de données?

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

Tous les HLists que j'ai trouvés pouvaient avoir n'importe quel type, et n'étaient pas limités.

Si ce n'est pas le cas, je téléchargerai le mien.

Answer 1

Je ne suis pas sûr que ce type de données est utile ...

• Si vous voulez vraiment a pour être qualifié existentiellement, je pense que vous devriez utiliser des listes régulières. Le type de données plus intéressant serait ici Exists, même si je suis certain qu'il existe des variantes de celui-ci sur tout package Hackage déjà:

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

  Ensuite, votre HList c est isomorphe à [Exists c] et vous pouvez toujours utiliser tous les fonctions habituelles basées sur une liste.

• D'autre part, si vous ne voulez pas nécessairement a dans le (:-) :: c a => a -> HList c être existentiellement qualifiés (ayant comme tel défie toute sorte de point de HList), vous devriez plutôt définir les éléments suivants:

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

  Ensuite, si vous voulez exiger que toutes les entrées de la HList satisfont c, vous pouvez faire une classe de type à témoin l'injection de HList as en [Exists c] dont la résolution par exemple ne fonctionne que si tous les types du HList satisfont la contrainte:

  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

Le paquet generics-sop offre ce hors de la boîte.

Une liste hétérogène peut être définie en utilisant generics-sop

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

et l'instancier au constructeur de type ayant une identité I (de generics-sop) ou Identity (de Data.Functor.Identity).

La bibliothèque offre alors la contrainte All telle que par ex.

All Show xs => NP I xs 

est le type d'une liste hétérogène où tous les types contenus sont dans la classe Show. Conceptuellement, All est une famille de type qui calcule la contrainte pour chaque élément dans une liste au niveau du type:

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

(uniquement que dans la définition réelle, All est en outre enveloppé dans une classe de type afin qu'il puisse être partiellement appliquée.)

La bibliothèque offre en outre toutes sortes de fonctions qui traversent et transforment NP s étant donné une contrainte commune.

Answer 3

Qu'est-ce que vous voulez vraiment est

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

que vous pouvez utiliser soit comme une liste hétérogène ordinaire

type HList = HKList Identity 

Ou avec des informations supplémentaires d'un certain type constant e attaché à chaque valeur (ou un autre intéressant foncteurs)

HKList ((,) e) 

Ou avec des informati sur capturé dans un dictionnaire

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

type ConstrainedList c = HKList (Has c) 

Ou garder des listes de ne capturées contraintes

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

que vous pouvez utiliser pour définir l'idée de tous une liste de types satisfaisant une contrainte

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 

Ou toute autre chose que vous pouvez faire avec un type k -> *

Vous pouvez fre ely convertir entre le travail avec All c xs => HList xs et 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

Je l'ai écrit plusieurs fois avant pour divers projets, mais je ne savais pas qu'il était dans une bibliothèque nulle part tant que Kosmikus pointed out that it's in generics-sop.