阿格达.冒号之前/之后的参数 [英] Agda. Parameters before/after colon

问题描述

在定义数据类型时，我可以通过"冒号前的一些参数.

When defining a data type, I can "pass" some parametrs before the colon.

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

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

But I seem to be unable to do this in function declarations for unknown reason.

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

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

What is the fundamental difference between passing parameters before and after the colon? To be honest, I have no idea why would anyone want to pass parameters before colon and what advantages it can give. Maybe, such definitions of a data type makes the parameters before the colon visible in the constructors.

推荐答案

我不知道为什么有人想在冒号之前传递参数以及它可以带来什么优势.

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

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

In a data type declaration parameters passed before the colon are in scope in the body of the data type definition.

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

I think this would be a good feature request. We could have e.g.

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

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

So feel free to open a new issue suggesting the change: https://github.com/agda/agda/issues

这篇关于阿格达.冒号之前/之后的参数的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！