haskell - 在 GHC 7.6 中匹配类型级别 Nat

Question

我的问题可能最容易以示例的形式解释：

type family   Take (n :: Nat) (xs :: [k]) :: [k]
type instance Take 0     xs        = '[]
type instance Take (n+1) (x ': xs) = x ': Take n xs

但是，这里的第二个实例被拒绝，因为(+)本身是一个类型族，不能在参数中使用。但似乎没有任何Succ或任何东西通常用于匹配 Nats。

那么，这可以表达吗？如果是这样，如何？

更新。我注意到isZero和中的isEven函数在GHC.TypeLits“破坏类型nats”的标题下。它们是否打算以某种方式在类型级别使用？我怀疑不会……但主要是因为我不知道该怎么做。:)

score 5 · Accepted Answer

我认为这是当前 TypeNats 实现中的一个已知问题。但它正在处理中，请查看： https: //plus.google.com/117760254622432568621/posts/iMYU2SMViay

1 回答 1