haskell - 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

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

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 在某个列表上返回 [] 则该列表为空。可悲的是，我看不出有什么方法可以说服它相信这一事实。这种情况我该怎么办？

<小时/>

我正在使用 GHC 8.6.5 和以下扩展:

{-# 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