系统 F 教堂数字在 Agda答案

【问题标题】：System F Church numerals in Agda系统 F 教堂数字在 Agda
【发布时间】：2019-06-06 13:55:31
【问题描述】：

我想使用 Agda 作为我的类型检查器和评估器来测试系统 F 中的一些定义。

我第一次尝试介绍 Church 自然数是通过写作

Num = forall {x} -> (x -> x) -> (x -> x)

这将像常规类型别名一样使用：

zero : Num
zero f x = x

但是Num 的定义没有类型（种类？）检查。使其工作并尽可能接近系统 F 表示法的最合适方法是什么？

【问题讨论】：

错误是什么？如果将{-# OPTIONS --type-in-type #-} 放在文件顶部会怎样？
这个特定示例的错误是piSort (univSort _3) (λ _ → piSort (piSort _3 (λ _ → _3)) (λ _ → piSort _3 (λ _ → _3))) !=< Set → Set of type univSort (piSort (univSort _3) (λ _ → piSort (piSort _3 (λ _ → _3)) (λ _ → piSort _3 (λ _ → _3)))) when checking that the expression ∀ {x} → (x → x) → x → x has type Set → Set

【解决方案1】：

以下将进行类型检查

Num : Set₁
Num = forall {x : Set} -> (x -> x) -> (x -> x)

zero : Num
zero f x = x

但是正如您看到的Num : Set₁，这可能会成为一个问题，您需要--type-in-type

【讨论】：