在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"Destructing type-nats"标题下.它们是否意味着以某种方式在类型级别使用？我怀疑不会......但主要是因为我看不出怎么样.:)

Answer 1

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