我想使用 Agda 作为我的类型检查器和评估器来测试系统 F 中的一些定义。
我第一次尝试介绍 Church 自然数是通过写作
Num = forall {x} -> (x -> x) -> (x -> x)
这将像常规类型别名一样使用：
zero : Num
zero f x = x
然而，定义Num不输入（种类？）检查。使其工作并尽可能接近系统 F 表示法的最合适方法是什么？
问问题
105 次
我想使用 Agda 作为我的类型检查器和评估器来测试系统 F 中的一些定义。
我第一次尝试介绍 Church 自然数是通过写作
Num = forall {x} -> (x -> x) -> (x -> x)
这将像常规类型别名一样使用：
zero : Num
zero f x = x
然而，定义Num不输入（种类？）检查。使其工作并尽可能接近系统 F 表示法的最合适方法是什么？