22
私の質問は、おそらく例の形で説明するのが最も簡単です：マッチング
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の機能が "タイプナットの破壊"という見出しの下にあることに気付きました。彼らは何とかタイプレベルで使用されることを意味していますか？私はそうは思わないだろう...しかし、主に私はどのように見ることができないので。 :)
右。私はちょうどこのコードをチェックできるようにGHC 7.6をインストールしました。あなたのコメントで述べた2つの問題は、GHCによって警告されています。謝罪。 （私は自分の答えに '削除'ボタンを押したので、今すぐ直接コメントすることはできません）。 – macron
引数が機能するかもしれないので終了条件をエンコードするようですが（https://gist.github.com/a39ce17ca47798b0f0efを参照）、n == 1のときだけ成功するようです。私は7.6ではなく、ymmvというタイプナットブランチでこれを試しました。 –
'isZero'関数と' isEven'関数は、同様の名前のGADTを構成します。これは、用語レベルで型レベルの述語にアクセスできるようにします。つまり、型関数ではなく、通常のterm-level関数で必要なマッチングを行う方法です。 ：[ –