Frederik Hanghøj Iversen
2018-01-22 11:04:47 UTC
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.
(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.
--
Regards
*Frederik HanghÞj Iversen*
Regards
*Frederik HanghÞj Iversen*