在 GHC 7.6 中匹配类型级别 Nat答案

【问题标题】：Matching on type level Nat in GHC 7.6在 GHC 7.6 中匹配类型级别 Nat
【发布时间】：2012-09-17 16:30:13
【问题描述】：

我的问题可能最容易用例子来解释：

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 函数位于“Destructing type-nats”标题下。它们是否打算以某种方式在类型级别使用？我怀疑不会……但主要是因为我不知道该怎么做。 :)

【问题讨论】：

对。我刚刚安装了 GHC 7.6 以便能够检查此代码，并且您在下面的 cmets 中提到的两个问题都被 GHC 标记了。道歉。（我在答案上按下了“删除”按钮，所以现在无法直接评论）。
似乎将终止条件编码为参数可能有效（请参阅gist.github.com/a39ce17ca47798b0f0ef），但它似乎只有在 n==1 时才会成功。我在 type-nats 分支上试过这个，而不是在 7.6 上，所以 ymmv。
isZero 和 isEven 函数构造了名称相似的 GADT，它们可以访问术语级别的类型级别谓词。换句话说，这是一种在常规术语级别函数中进行匹配的方法，而不是类型函数。 :[

【解决方案1】：

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

【讨论】：