search

agda / agda-stdlib

The Agda standard library
https://wiki.portal.chalmers.se/agda/Libraries/StandardLibrary
Other
561 stars 234 forks source link

Very dependent map #2373

Closed JacquesCarette closed 3 weeks ago

JacquesCarette commented 2 months ago

Closes #833 .

The names, of course, are up for debate! (And, now that I think of it, I should probably add a property or two of them in this same PR).

jamesmckinna commented 2 months ago

Re: naming Is it possible to reconcile the name choices for this PR, and the general principles in #278 ?

JacquesCarette commented 2 months ago

I guess this would push towards naming the first one simply map? Except that Data.Product.Base already has such a thing, and it is much less dependent.

My feeling is that #278 deals with the case of "normally dependent" naming -- here the functions really are absurdly dependent. So they seem like they'd need their own, new column. Interestingly, the various type families in dep-map are left implicit, and Agda seems happy enough with that. Having said that, I tried to apply dep-map to non-dependent cases, and it all became a giant yellow party.

In other words, we don't need the results of @gallais 's #278 experiment to know that we can't make these very-dependent version the 'default' with the most basic name.

JacquesCarette commented 2 months ago

Thanks - these are all great suggestions. (The h i actually come from me cutting and pasting from elsewhere in stdlib, but I'll accept the blame for not relabeling). Will implement as soon as I have a moment.

jamesmckinna commented 1 month ago

I think we're there now! Would you be happy to merge @MatthewDaggitt ?