types - Agda 。冒号前后的参数

Question

定义数据类型时，我可以在冒号前“传递”一些参数。

data Image_э_  { A B : Set} : (f : A → B) →  B → Set where
   im : {f : A → B} → (x : A) → Image f э f x

但由于未知原因，我似乎无法在函数声明中执行此操作。

exIm {A B : Set} : {f : A → B}{y : B} → Image f э y → B
exIm {y = y} _ = y

在冒号前后传递参数的根本区别是什么？老实说，我不知道为什么会有人想在冒号之前传递参数，以及它能带来什么好处。也许，这样的数据类型定义使得冒号前的参数在构造函数中可见。

Answer 1

I have no idea why would anyone want to pass parameters before colonand what advantages it can give.

在冒号之前传递的数据类型声明参数在范围内数据类型定义的主体。

我认为这是一个很好的功能请求。我们可以有例如

typeOf {A : Set} : A -> Set
typeOf a = A -- A is in scope because `{A : Set}` was before the colon

所以请随时打开一个新问题来建议更改:https://github.com/agda/agda/issues