add telescopes and a bit of theory about them

I think the basic definitions are pretty solid by now, though I am still fighting with making high-level telescope-based definitions that have nice pretty-printing.

Open question: Telescopes generalize hlists to the dependent case. Should we get rid of hlists? Does anyone want to attempt porting hlist users over to telescopes? Restricting the dependency can actually be useful because it makes them easier to use.

added 1 commit

• 27620704 - add telescopes and a bit of theory about them

Compare with previous version

I have a branch of Iris using these to add telescopic BI binders and proofmode support at https://gitlab.mpi-sws.org/FP/iris-coq/tree/ci/ralf/telescopes (currently that still copies this file, but of course when this gets merged, that copy will be removed).

Does anyone want to attempt porting hlist users over to telescopes?

Doe they even exist ;) I think I used hlists internally in the proofmode back in the days, but that's gone AFAIK.

They still seem to be used in ltac_tactics.

Oh, right, they are used for the arguments of iSpecialize (foo $! ...). Not sure how easy it's to port them, but feel free to try.

I don't think we use bi_hforall and bi_hexist anywhere though.

feel free to try.

I'd rather spend my time on telescopes in logical atomicity TBH. I'm already way behind on that.

added 1 commit

• 0509f5a9 - add telescopes and a bit of theory about them

Compare with previous version

added 1 commit

• 5e9c82ab - add telescopes and a bit of theory about them

Compare with previous version

Hm, I just realized I am not entirely consistent with my naming of functions. Some are called tfun_* and some are called tele_*. I don't have a strong preference either way.

added 1 commit

• 7f827e9a - add telescopes and a bit of theory about them

Compare with previous version

All right I named everything consistently, and also added a notation that turned out useful for the atomic triples.

added 1 commit

• 79874db5 - address review nits

Compare with previous version

added 1 commit

• 836fdfec - tweak re-binding notation

Compare with previous version

added 1 commit

• f2292a3e - show that tele_app ∘ tele_bind is an identity; remove unused strange fmap instance

Compare with previous version

resolved all discussions

All discussions resolved.

More comments needed. tele_arg_id is also unused.

Well yeah... this is mostly a curiosity with a funny type. I can remove it if you want.

Either write a comment why it's interesting (I don't quite get what's funny/surprising about it ;)), or remove please.

Well it's the identity function of the -t> function space.

oh, that makes sense. Do we also have composition?

changed this line in version 9 of the diff

Good question. I now added at least a proof that this is actually an identity.

Now we also have a composition. :)

Nice!

added 1 commit

• db84c646 - show that tele_app ∘ tele_bind is an identity; remove unused strange fmap instance

Compare with previous version

added 3 commits

• b0e5c5f3 - add telescopes and a bit of theory about them
• 7ecfa30c - show that tele_app ∘ tele_bind is an identity; remove unused strange fmap instance
• ed94cec2 - also provide a composition for the function space

Compare with previous version

added 3 commits

• 49b04e85 - add telescopes and a bit of theory about them
• cee2597b - show that tele_app ∘ tele_bind is an identity; remove unused strange fmap instance
• 4933fa76 - also provide a composition for the function space

Compare with previous version

resolved all discussions

I think I'm happy to merge!

Awesome. :) Thanks for the great feedback!

Would you like me to squash it into one commit? The 3 commits we have right now are at least a bit meaningful.

The 3 commits we have right now are at least a bit meaningful.

They have enough meaning, so no need to squash.

mentioned in commit 5bcfb8b0

merged

All right, merged.

The Iris side of this depends on https://gitlab.mpi-sws.org/FP/iris-coq/merge_requests/150.

Oh, right, they are used for the arguments of iSpecialize (foo $! ...). Not sure how easy it's to port them, but feel free to try.

FYI, you nerdsniped me into briefly trying this. However, Coq's type inference is entirely unable to cope with all the extra freedom it gets when these things can be dependent, so everything falls apart. I don't think we can use telescopes there with the current unification algorithm; maybe after the new one got merged.