\ forall(∀)在签名中实际意味着什么？

Question

从我收集到的有关agda的信息中,我(显然是错误地)得出的结论? {A}相当于{A : Set}.现在我注意到了

flip : ? {A B C} -> (A -> B -> C) -> (B -> A -> C)

是无效的(关于Set\omega的东西反过来似乎是一些内部的东西,但是

flip : {A B C : Set} -> (A -> B -> C) -> (B -> A -> C)

很好.任何人都可以为我清除这个吗？

Answer 1

那是因为? {A}实际上只是一个语法糖{A : _},它要求编译器A自动填充类型.

这对Sets 只有很好的效果,因为你可以:

{A : Set}
{A : Set?}
{A : Set?}
-- etc.

事实上,所有这些都是您定义中的有效类型.?当下面的东西可以通过它的使用明确地确定时,真的才有意义.

例如,考虑这个定义:

data List (A : Set) : Set where
  -- ...

map : ? {A B} ? (A ? B) ? List A ? List B
map = -- ...

类型A必须是Set,因为List只适用于Sets.

然而,因为它只是一个糖,{A : _}这意味着它不仅仅是Sets的工作.

_+_ : ? ? ? ? ?
_+_ = -- ...

comm : ? x y ? x + y ? y + x
comm = -- ...

或者也许是最常见的用例:

map : ? {a b} {A : Set a} {B : Set b} ? (A ? B) ? List A ? List B

的类型a和b是Level; 这称为宇宙多态性.