具有DataKinds的类型级映射

Question

我有一个常见的模式，其中我有一个类型级别的列表，类型为[ * ]，我想将一种类型构造器应用于列表中的每个元素，其类型为* -> *。例如，我想将类型'[Int, Double, Integer]更改为'[Maybe Int, Maybe Double, Maybe Integer]。

这是我尝试实现类型级别map的方式。

{-# LANGUAGE TypeFamilies, MultiParamTypeClasses, FlexibleInstances, FlexibleContexts, TypeOperators, DataKinds, ScopedTypeVariables, GADTs #-}

-- turns a type list '[b1, b2, b3]
-- into the type list '[a b1, a b2, a b3]
class TypeMap (a :: * -> *) (bs :: [*]) where
    type Map a bs :: [*]

instance TypeMap a '[b] where
    type Map a '[b] = '[a b]

instance TypeMap a (b1 ': b2 ': bs) where
    type Map a (b1 ': b2 ': bs) = ((a b1) ': (Map a (b2 ': bs)))


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

class Foo as where
    toLists :: HList as -> HList (Map [] as)

instance Foo '[a] where
    toLists (HCons a HNil) = HCons [a] HNil

instance (Foo (a2 ': as)) =>  Foo (a1 ': a2 ': as) where
    toLists (HCons a as) = 
        let as' = case (toLists as) of
                    (HCons a2 as'') -> HCons [head a2] as'' -- ERROR
        in HCons [a] as'

这导致出现错误。

Could not deduce (a3 ~ [t0])
    from the context (Foo ((':) * a2 as))
      bound by the instance declaration at Test.hs:35:10-50
    or from ((':) * a1 ((':) * a2 as) ~ (':) * a as1)
      bound by a pattern with constructor
                 HCons :: forall a (as :: [*]).
                          a -> HList as -> HList ((':) * a as),
               in an equation for `toLists'
      at Test.hs:36:14-23
    or from (Map [] as1 ~ (':) * a3 as2)
      bound by a pattern with constructor
                 HCons :: forall a (as :: [*]).
                          a -> HList as -> HList ((':) * a as),
               in a case alternative
      at Test.hs:38:22-34
      `a3' is a rigid type variable bound by
           a pattern with constructor
             HCons :: forall a (as :: [*]).
                      a -> HList as -> HList ((':) * a as),
           in a case alternative
           at Test.hs:38:22
    Expected type: HList (Map [] ((':) * a2 as))
      Actual type: HList ((':) * [t0] as2)
    In the return type of a call of `HCons'
    In the expression: HCons [head a2] as''
    In a case alternative: (HCons a2 as'') -> HCons [head a2] as''

我已经尝试添加了大量的类型注释，但错误基本上仍然是一样的：GHC甚至无法推断HList的第一个元素是一个（普通）列表。我在这里做了什么傻事吗？做了一些非法的事情吗？还是有其他解决方法？

- crockeea

---

为什么你没有一个 TypeMap a [] 实例？ - Daniel Wagner

@DanielWagner 同意，这些实例可能应该是针对 '[] 和 (a ': as)。 - crockeea

Answer 1

当你写下时，这与你用来定义Map的递归不一致...这只有在尝试TypeMap长度不为1或2的列表时才会导致错误。此外，在您的情况下，使用类型族更加简洁。

type family TypeMap (a :: * -> *) (xs :: [*]) :: [*]
type instance TypeMap t '[] = '[]
type instance TypeMap t (x ': xs) = t x ': TypeMap t xs

请注意，这基本上是直接翻译的内容：

map f [] = []
map f (x:xs) = f x : map f xs

- aavogt

---

感谢指出类型族解决方案；这比类更清晰。 - crockeea

Answer 2

使您的代码编译的最小更改是将 [a] 和 b1:b2:bs 的实例更改为 [] 和 b:bs 的实例。

instance TypeMap a '[] where
    type Map a '[] = '[]

instance TypeMap a (b ': bs) where
    type Map a (b ': bs) = a b ': Map a bs

- Daniel Wagner

---

@Eric 我怀疑问题是这样的：你的递归调用匹配了 HCons，这意味着你期望递归类型级别调用也会使 cons 单元格很容易地出现。但由于有两个可能的实例可供选择，这并不是很明显——它涉及到 GHC 对类型类封闭性的一些推理，而 GHC 不应该（也许不应该）去做。通过修复，如果在 TypeMap 的参数中有一个 cons 单元格很容易地出现，那么 GHC 只能选择一个实例，因此它会选择它。 - Daniel Wagner