タイプチェッカーおよびエバリュエーターとして Agda を使用して、システム F でいくつかの定義をテストしたいと思います。
教会の自然数を紹介する私の最初の試みは、次のように書くことでした
Num = forall {x} -> (x -> x) -> (x -> x)
これは、通常のタイプ エイリアスと同じように使用されます。
zero : Num
zero f x = x
ただし、 の定義はNum型 (種類?) チェックを行いません。それを機能させ、システム F 記法にできるだけ近づけるための最も適切な方法は何ですか?