私の質問は、おそらく例を挙げて説明するのが最も簡単でしょう。
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 番目のインスタンスは拒否されます。 は(+)、それ自体が型ファミリであるため、引数で使用できないためです。ただし、Nats のマッチングに通常使用される や は存在しないようですSucc。
では、これを表現することはできるのでしょうか。もしできるとしたら、どのように表現すればよいのでしょうか。
アップデートisZeroとisEven関数がGHC.TypeLits「type-nats の破壊」という見出しの下にあります。これらは、何らかの形で型レベルで使用されることを意図しているのでしょうか? おそらくそうではないと思いますが、主な理由は、その方法がわからないからです。:)
ベストアンサー1
これは TypeNats の現在の実装における既知の問題だと思います。しかし、現在対応中です。以下をご覧ください。https://plus.google.com/117760254622432568621/posts/iMYU2SMViay