HList与DataKinds,种类不可推销

Question

我有这个代码片段,它使用了大量的GHC扩展:

{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}

import GHC.Exts (Constraint)

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

type family All (p :: * -> Constraint) (xs :: HList [*]) :: Constraint where
    All p Nil = ()
    All p (Cons x xs) = (p x, All p xs)

GHC抱怨说:

 ‘HList’ of kind ‘[*] -> *’ is not promotable
    In the kind ‘HList [*]’

为什么我不能提升HList为一种？我得到使用GHC同样的错误7.8.2和7.11.

当然,使用内置'[]工作正常:

type family All (p :: * -> Constraint) (xs :: [*]) :: Constraint where
    All p '[]       = ()
    All p (x ': xs) = (p x, All p xs)

我想使用自己的,HList而不是'[]因为实际的HList支持附加,看起来像这样:

type family (:++:) (xs :: [*]) (ys :: [*]) where
    '[] :++:  ys = ys
     xs :++: '[] = xs
    (x ': xs) :++: ys = x ': (xs :++: ys)

data HList :: [*] -> * where
    Nil  :: HList '[]
    Cons :: a -> HList l -> HList (a ': l)
    App  :: Hlist a -> HList b -> HList (a :++: b)

编辑:主要目标是推断GHC

(All p xs, All p ys) ==> All p (xs :++: ys)

这样我就可以写了

data Dict :: Constraint -> * where
    Dict :: c => Dict c

witness :: Dict (All p xs) -> Dict (All p ys) -> Dict (All p (xs :++: ys))
witness Dict Dict = Dict

我曾希望为追加类型级别列表添加一个显式表示可以帮助我实现这一目标.还有另一种说服GHC的方法吗？

Answer 1

我现在看到的问题是如何写出证据(All p xs, All p ys) => All p (xs :++: ys).答案是,通过归纳,当然!

我们真正想要写的函数的类型是

allAppend :: (p :: Constraint) -> (xs :: [*]) -> (ys :: [*]) 
          -> (All p xs, All p ys) -> All p (xs :++: ys)

但是Haskell没有依赖类型."伪造"依赖类型通常意味着有证人带有类型存在的证据.这使事情有点乏味,但目前没有别的办法.我们已经有了一份名单的证人xs- 确切地说HList xs.对于约束,我们将使用

data Dict p where Dict :: p => Dict p

然后我们可以将蕴涵写成一个简单的函数:

type (==>) a b = Dict a -> Dict b 

所以我们的类型变成:

allAppend :: Proxy p -> HList xs -> HList ys 
          -> (All p xs, All p ys) ==> (All p (xs :++: ys))

该函数的主体非常简单 - 请注意每个模式如何allAppend匹配定义中的每个模式:++::

allAppend _ Nil _  Dict = Dict  
allAppend _ _  Nil Dict = Dict 
allAppend p (Cons _ xs) ys@(Cons _ _) Dict = 
  case allAppend p xs ys Dict of Dict -> Dict 

相反的蕴涵All p (xs :++: ys) => (All p xs, All p ys)也成立.实际上,函数定义是相同的.