在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

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

那么，这个能否表达呢？如果可以，应该如何表达？

更新。我注意到GHC.TypeLits中的isZero和isEven函数位于“Destructing type-nats”标题下。它们是否打算在类型层面上使用？我怀疑不是……但主要是因为我看不出如何做到。:)

- Andy Morris

---

好的。我刚刚安装了 GHC 7.6 版本来检查这段代码，你在下面评论中提到的两个问题都被 GHC 指出了。非常抱歉。（我按了“删除”按钮，所以现在无法直接对其进行评论）。 - macron

似乎将终止条件编码为参数可能有效（请参见https://gist.github.com/a39ce17ca47798b0f0ef），但仅在n == 1时才成功。我已经在type-nats分支上尝试过了，而不是7.6版本，所以你的情况可能会有所不同。 - Nathan Howell

isZero和isEven函数构造了同名的GADTs，这些GADTs可以在术语级别上访问类型级谓词。换句话说，这是一种在常规术语级函数中进行所需匹配的方法，而不是一种类型函数。 - C. A. McCann

Answer 1

我认为这是当前TypeNats实现中已知的问题。但正在进行修复，请查看：https://plus.google.com/117760254622432568621/posts/iMYU2SMViay

- michalt

---

谷歌加(Google Plus)已经终止。这个问题的现状是什么？ - Lemming