22
我的問題可能是最簡單的一個例子的形式來解釋：匹配的類型級NAT在GHC 7.6
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以便能夠檢查此代碼，並且您在下面的註釋中提到的兩個問題都由GHC標記。道歉。 （我按下了我的答案上的'刪除'按鈕，所以現在不能直接對它進行評論）。 – macron
看起來像編碼終止條件作爲參數可能工作（請參閱https://gist.github.com/a39ce17ca47798b0f0ef），但它似乎只有當n == 1時成功。我已經在type-nats分支上試過了，不是7.6，所以ymmv。 –
「isZero」和「isEven」函數構造了類似名稱的GADT，它可以在術語級別訪問類型級謂詞。換句話說，這是一種在常規術語級函數中進行匹配的方法，而不是類型函數。 ：[ –