agda - 在 agda 中的类型签名中的任意评估

Question

所以我有另一个“简单”的阿加问题。我想要一个使用任意评估作为前提和结果的证明。但我认为我对类型系统的了解不足以做到这一点。

作为一个简单的例子

f : {S : Set} -> (a : S) 
 -> ( R : S -> Set) 
 -> (R a)
f aa rr = rr aa

有编译错误

Set !=< rr aa of type Set1
when checking that the expression rr aa has type rr aa

当然

f : {S : Set} -> (a : S) 
 -> ( R : S -> Set) 
 -> Set
f aa rr = rr aa

编译得很好

一样

f : {S : Set} -> (a : S) 
 -> ( R : S -> Set) 
 -> (R a)
 -> (R a)
f _ _ ra = ra

(R a)在上下文中意味着什么？可以建造吗？它是如何建造的？

score 2 · Accepted Answer

在您的第一个示例中，表达式rr aa具有 type Set，因为它是将aatypeS应用于 type 函数rr的结果S -> Set。

您的函数的类型签名需要R a虽然的结果类型。给定参数的命名，预期的结果类型是rr aa. 类型检查器现在尝试将预期类型 ( rr aa) 与表达式类型 ( Set) 统一起来，但失败了。

事实上，上面给出的类型的函数将与类型理论不一致：

no-f : (f : {S : Set} → (a : S) → (R : S → Set) → R a) → ⊥
no-f f = f tt (λ _ → ⊥)

换句话说，假设存在上述类型的函数，则可以生成空类型（⊥）的元素。所以一般来说，你不能在R a没有额外要求的情况下构造类型元素。

上面使用的导入：

open import Data.Empty
open import Data.Unit

1 回答 1