Последовательность над разнородным списком в Haskell

Во-первых, здесь ошибка:

type family Map (f :: * -> *) (xs :: [*]) where
    Map f '[] = '[]
    Map f (x ': xs) = (f x) ': Map f xs
                             --^^^^^-- we need this

После того, как это исправлено, проблема в том, что нам нужно действовать по индукции по ins, а не по Map f ins. Для этого нам нужен одноэлементный тип:

data SList :: [*] -> * where
    SNil  :: SList '[] 
    SCons :: SList zs -> SList ( z ': zs )

а затем дополнительный аргумент:

hSequence :: Applicative m => SList ins -> HList (Map m ins) -> m (HList ins)
hSequence SNil         HNil        = pure HNil
hSequence (SCons ins') (x :> rest) = (:>) <$> x <*> hSequence ins' rest

Теперь это компилируется. Сопоставление SNil / SCons уточняет ins либо до '[], либо до z ': zs, так что Map m ins также можно развернуть на один шаг. Это позволяет нам сделать рекурсивный вызов.

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

class SingList ins where
    singList :: SList ins

instance SingList '[] where
    singList = SNil

instance SingList zs => SingList (z ': zs) where
    singList = SCons singList

hSequence2 :: (Applicative m, SingList ins)
              => HList (Map m ins) -> m (HList ins)
hSequence2 = hSequence singList

Этот GADT сохраняет корешок («длину») списков уровней типов после стирания типов:

data Spine (xs :: [k]) :: Type where
  NilSpine :: Spine '[]
  ConsSpine :: Spine xs -> Spine (x : xs)

Отсюда мы можем доказать следующие леммы:

mapNil' :: forall f xs. Map f xs ~ '[] => Spine xs -> xs :~: '[]
mapNil' NilSpine = Refl

type family Head (xs :: [k]) :: k where Head (x : _) = x
type family Tail (xs :: [k]) :: [k] where Tail (_ : xs) = xs
data MapCons f y ys xs =
  forall x xs'. (xs ~ (x : xs'), y ~ f x, ys ~ Map f xs') => MapCons
mapCons' :: forall f xs y ys. Map f xs ~ (y : ys) => Spine xs -> MapCons f y ys xs
mapCons' (ConsSpine _) = MapCons

Теперь Spine — это одноэлементное семейство: Spine xs имеет ровно одно значение для каждого xs. Поэтому мы можем стереть его.

mapNil :: forall f xs. Map f xs ~ '[] => xs :~: '[]
mapNil = unsafeCoerce Refl -- safe because mapNil' exists
mapCons :: forall f xs y ys. Map f xs ~ (y : ys) => MapCons f y ys xs
mapCons = unsafeCoerce MapCons -- safe because mapCons' exists

Затем эти леммы можно использовать для определения вашей функции:

hSequence :: forall m ins. Applicative m => HList (Map m ins) -> m (HList ins)
hSequence HNil | Refl <- mapNil @m @ins = pure HNil
hSequence (x :> rest) | MapCons <- mapCons @m @ins = (:>) <$> x <*> hSequence rest

Начав с Spine, мы можем построить обоснование того, почему наша логика работает. Затем мы можем стереть весь одноэлементный мусор, который нам не нужен во время выполнения. Это расширение того, как мы используем типы для обоснования того, почему наши программы работают, а затем стираем их во время выполнения. Важно написать mapNil' и mapCons', чтобы мы знали, что то, что мы делаем, работает.

HList довольно громоздкий тип. Вместо этого я рекомендую использовать что-то вроде этого, похожего на vinyl.

{-# language PolyKinds, DataKinds, GADTs, ScopedTypeVariables, RankNTypes, TypeOperators #-}
import Data.Kind
import Control.Applicative

infixr 4 :>

-- Type is the modern spelling of the * kind
data Rec :: [k] -> (k -> Type) -> Type 
where
  Nil :: Rec '[] f
  (:>) :: f a -> Rec as f -> Rec (a ': as) f

htraverse
  :: forall (xs :: [k]) (f :: k -> Type) (g :: k -> Type) m.
     Applicative m
  => (forall t. f t -> m (g t))
  -> Rec xs f -> m (Rec xs g)
htraverse _f Nil = pure Nil
htraverse f (x :> xs) =
  liftA2 (:>) (f x) (htraverse f xs)

Если хотите, вы можете определить

hsequence
  :: forall (xs :: [k]) (g :: k -> Type) m.
     Applicative m
  => Rec xs (Compose m g) -> m (Rec xs g)
hsequence = htraverse getCompose

Обратите внимание, что

HList xs ~= Rec xs Identity