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 的东西。

那么，这个可以表达吗？如果是这样，怎么办？

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

Answer 1

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