私の質問は、おそらく例の形で説明するのが最も簡単です。
type family Take (n :: Nat) (xs :: [k]) :: [k]
type instance Take 0 xs = '[]
type instance Take (n+1) (x ': xs) = x ': Take n xs
ただし、ここでの2番目のインスタンスは拒否されます。これは(+)、型族自体であるため、引数で使用できないためです。Succしかし、Natsのマッチングに通常使用されるものはないようです。
だから、これを表現することができます。もしそうなら、どのように？
更新します。isZeroのとisEven関数GHC.TypeLitsが「Destructingtype-nats」という見出しの下にあることに気付きました。どういうわけかタイプレベルで使用するためのものですか？私はそうは思わないでしょう…しかし、主に私が方法を見ることができないからです。:)