Search code examples
typesparameterssyntaxagda

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.

Solution

  • 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

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