Haskell中的异类列表序列

Question

考虑以下的定义HList：

infixr 5 :>
data HList (types :: [*]) where
  HNil :: HList '[]
  (:>) :: a -> HList l -> HList (a:l)

还有一个Map用于映射类型级别列表的类型族：

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

现在，我想定义的sequence等价性HList。我的尝试看起来像

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

但是我得到这样的错误：

Could not deduce: ins ~ '[]
       from the context: Map m ins ~ '[]
         bound by a pattern with constructor: HNil :: HList '[]

对我来说，似乎编译器不确定如果Map m返回[]某个列表，则列表为空。可悲的是，我看不出有任何办法可以说服这一事实。在这种情况下我该怎么办？

---

我正在使用8.6.5具有以下扩展名的GHC ：

{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeOperators #-}

Answer 1

首先，这里有一个错误：

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可以是未折叠的一个步骤，以及。这使我们可以进行递归调用。

和往常一样，我们可以通过合适的类型类删除其他单例参数。我有合理的把握，其中一些可以自动利用该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