Ограниченный неоднородный список

Я не уверен, что этот тип данных полезен...

• Если вы действительно хотите, чтобы a был квалифицирован экзистенциально, я думаю, вам следует использовать обычные списки. Более интересным типом данных здесь был бы Exists, хотя я уверен, что его варианты уже есть во всем package Hackage:

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

  Тогда ваш HList c изоморфен [Exists c], и вы по-прежнему можете использовать все обычные функции, основанные на списках.

• С другой стороны, если вы не обязательно хотите, чтобы a в (:-) :: c a => a -> HList c было экзистенциально квалифицированным (наличие такого рода противоречит точке HList), вы должны вместо этого определить следующее:

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

  Затем, если вы хотите потребовать, чтобы все записи HList удовлетворяли c, вы можете создать класс типов для свидетеля внедрения из HList as в [Exists c], разрешение экземпляра которого работает только в том случае, если все типы в HList удовлетворяют ограничению:

  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
  

Пакет generics-sop предлагает это из коробки.

Неоднородный список может быть определен в generics-sop с помощью

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

и инстанцировать его в конструкторе типа удостоверения I (из generics-sop) или Identity (из Data.Functor.Identity).

Затем библиотека предлагает ограничение All, например.

All Show xs => NP I xs

— это тип разнородного списка, в котором все содержащиеся типы относятся к классу Show. Концептуально All — это семейство типов, которое вычисляет ограничение для каждого элемента в списке на уровне типов:

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

(Только в фактическом определении All дополнительно обернут в класс типа, чтобы его можно было частично применить.)

Кроме того, библиотека предлагает всевозможные функции, которые проходят и преобразовывают NP с учетом общего ограничения.

То, что вы действительно хотите, это

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

Который можно использовать либо как обычный разнородный список

type HList = HKList Identity

Или с дополнительной информацией о некотором постоянном типе e, прикрепленном к каждому значению (или другим интересным функторам)

HKList ((,) e)

Или с дополнительной информацией, записанной в словаре

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

type ConstrainedList c = HKList (Has c)

Или сохраняйте списки только захваченных ограничений

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

Который вы можете использовать, чтобы определить идею всего списка типов, удовлетворяющих ограничению

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

Или что-нибудь еще, что вы можете сделать с добрым k -> *

Вы можете свободно переключаться между работой с All c xs => HList xs и 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

полный код

Я писал это несколько раз раньше для различных проектов, но я не знал, что это где-то есть в библиотеке, пока Kosmikus не указал, что это в generics-sop.