[Agda] Infix-notation and TDNR

[Frederik Hanghøj Iversen]

I just discovered a new feature in Agda. I don't know what's it's called
(haven't been able to find any documentation on it) so let me just name it
Type-Directed Name-space Resolution (TDNR).

The feature I'm talking about it the one that e.g lets you project a field
`Object` of a term `ℂ` of type `Category` that has this field like so:

ℂ .Object

What I would like to do is use the infix version of this. So for instance
for a field `_⊕_` I would like to express the distributive properties of
functors like so:

func→ (g (ℂ .⊕) f) ≡ func→ g (𝔻 .⊕) func→ f

Or perhaps even with backticks (as in Haskell) like so:

func→ (g `ℂ .⊕` f) ≡ func→ g `𝔻 .⊕` func→ f

In stead I am left with writing it like so:

func→ (ℂ ._⊕_ g f) ≡ 𝔻 ._⊕_ (func→ g) (func→ f)

Which is not so readable.

I've attached an MWE.

[a.j.rouvoet]

You can locally declare two modules with the same name as the record
instances
to accomplish what you want; e.g.:

  record Functor (ℂ : Category) (𝔻 : Category) : Set where
    module ℂ = Category ℂ
    module 𝔻 = Category 𝔻
    field
      distrib : {A B C : ℂ.Object} {g : ℂ.Arrow B C} {f : ℂ.Arrow A B}
→ func→ (g ℂ.⊕ f) ≡ (func→ g) 𝔻.⊕ (func→ f)


Regards,

Arjen

Post by Frederik Hanghøj Iversen
I just discovered a new feature in Agda. I don't know what's it's
called (haven't been able to find any documentation on it) so let me
just name it Type-Directed Name-space Resolution (TDNR).
The feature I'm talking about it the one that e.g lets you project a
field `Object` of a term `ℂ` of type `Category` that has this field
     ℂ .Object
What I would like to do is use the infix version of this. So for
instance for a field `_⊕_` I would like to express the distributive
    func→ (g (ℂ .⊕) f) ≡ func→ g (𝔻 .⊕) func→ f
    func→ (g `ℂ .⊕` f) ≡ func→ g `𝔻 .⊕` func→ f
    func→ (ℂ ._⊕_ g f) ≡ 𝔻 ._⊕_ (func→ g) (func→ f)
Which is not so readable.
I've attached an MWE.
--
Regards
/Frederik HanghÞj Iversen/
_______________________________________________
Agda mailing list
https://lists.chalmers.se/mailman/listinfo/agda

[Sandro Stucki]

The feature is called "postfix projections", BTW.

https://github.com/agda/agda/issues/1963

Cheers
/Sandro


On Jan 22, 2018 1:07 PM, "a.j.rouvoet" <***@gmail.com> wrote:

You can locally declare two modules with the same name as the record
instances
to accomplish what you want; e.g.:

record Functor (ℂ : Category) (𝔻 : Category) : Set where
module ℂ = Category ℂ
module 𝔻 = Category 𝔻
field
distrib : {A B C : ℂ.Object} {g : ℂ.Arrow B C} {f : ℂ.Arrow A B} →
func→ (g ℂ.⊕ f) ≡ (func→ g) 𝔻.⊕ (func→ f)


Regards,

Arjen

On 01/22/2018 12:04 PM, Frederik HanghÞj Iversen wrote:

I just discovered a new feature in Agda. I don't know what's it's called
(haven't been able to find any documentation on it) so let me just name it
Type-Directed Name-space Resolution (TDNR).

The feature I'm talking about it the one that e.g lets you project a field
`Object` of a term `ℂ` of type `Category` that has this field like so:

ℂ .Object

What I would like to do is use the infix version of this. So for instance
for a field `_⊕_` I would like to express the distributive properties of
functors like so:

func→ (g (ℂ .⊕) f) ≡ func→ g (𝔻 .⊕) func→ f

Or perhaps even with backticks (as in Haskell) like so:

func→ (g `ℂ .⊕` f) ≡ func→ g `𝔻 .⊕` func→ f

In stead I am left with writing it like so:

func→ (ℂ ._⊕_ g f) ≡ 𝔻 ._⊕_ (func→ g) (func→ f)

Which is not so readable.

I've attached an MWE.