Ograniczona lista heterogeniczna

Question

Szukałem hackage i nie mogłem znaleźć niczego podobnego, ale wydaje się ono dość proste i użyteczne. Czy istnieje biblioteka zawierająca rodzaj danych?

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

Wszystkie znalezione przeze mnie HLists mogły mieć dowolny typ i nie były ograniczone.

Jeśli nie, prześlę własne.

Answer 1

nie jestem pewien, że ten typ danych jest przydatna ...

• Jeśli naprawdę chcesz a być egzystencjalnie kwalifikacje, myślę, że należy użyć zwykłych list. Im bardziej interesujący typ danych tutaj byłoby Exists, chociaż jestem pewien, że są wariantami tego wszystkiego nad pakietu Hackage już:

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

  Następnie Twój HList c jest izomorficzna [Exists c] i nadal można korzystać ze wszystkich standardowe funkcje oparte na listach.

• Z drugiej strony, jeśli nie koniecznie chcą a w (:-) :: c a => a -> HList c być egzystencjalnie kwalifikacje (mający go jako taki rodzaj przeciwstawia punkt HList), należy zamiast definiować następujące:

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

  Następnie, jeśli chcesz, aby wszystkie wpisy z HList zaspokoić c, można dokonać klasę typu świadkami zastrzyk z HList as do [Exists c] którego instancja rozdzielczości działa tylko wtedy, gdy wszystkie typy w HList spełniają ograniczenia:

  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

Pakiet generics-sop oferuje to po wyjęciu z pudełka.

niejednorodna lista ta może być zdefiniowana w generics-sop stosując

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

i uruchamianiu do konstruktora typu tożsamość I (z generics-sop) lub Identity (od Data.Functor.Identity).

Biblioteka następnie oferuje ograniczenie All takie, że np.

All Show xs => NP I xs 

jest rodzaj heterogenicznego listy gdzie wszystkie typy są zawarte w klasie Show. Koncepcyjnie, All to rodzinny typ, który oblicza ograniczenie dla każdego elementu na liście Typ szczebla:

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

(Tylko, że w aktualnej definicji All dodatkowo owinięte w klasie typu tak, że może być częściowo zastosowane.)

Biblioteka oferuje ponadto wiele funkcji, które przechodzą i przekształcają się na wspólne ograniczenie.

Answer 3

Co naprawdę chcesz to

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

które można wykorzystać zarówno jako zwykły listy heterogenicznej

type HList = HKList Identity 

Albo z dodatkowymi informacjami o pewnej stałej typu e dołączonym do każdej wartości (lub inny interesujący funktorzy)

HKList ((,) e) 

Lub z dodatkowymi informacjami na ujęte w słowniku

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

type ConstrainedList c = HKList (Has c) 

Albo przechowuje wykazy tylko przechwyconych ograniczeń

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

które można wykorzystać do zdefiniowania pojęcia wszystkich z listy typów spełniających ograniczenie

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 

Lub cokolwiek innego, co możesz zrobić z pewnym rodzajem k -> *

Możesz fre ely konwersji pomiędzy pracę z All c xs => HList xs i 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

Pisałem to kilka razy, zanim na różne projekty, ale nie wiedziałem, że był w bibliotece nigdzie aż Kosmikus pointed out that it's in generics-sop.