Stream: Coq users

Topic: Typeclasses and 'contexts'


view this post on Zulip SoundLogic (May 14 2024 at 01:34):

So, in my work I keep winding up with different 'contexts' for instances. For example, if we take the full Decidable P with a bool rep and everything, we also wind up with PropDecidable P which is the propositional squash of that, SPropDecidable P (the strict propositional squash of that), and DNDecidable P (the double negation squash of that, which actually holds for all types).

Then depending on what the actual goal is, some of these can be reinterpreted as each other. For example, when the goal is in Prop, PropDecidable P can fill in for Decidable P.

In general there are all these contexts (maybe these are modalities? I'm not quite sure what a modality is), but typeclass instance search seems like a huge pain with them.

If I have Decidable A -> Decidable B, getting PropDecidable A -> PropDecidable B for free is very desirable.

I've been trying to set up an elaborate typeclass system for making this at least easier to work with, with a thing like

Class InContext@{s sr|u ur|} (T : Type@{s|u}) (R : Type@{sr|ur}) : Type@{sr | max(u,ur)}
  := with_context : (T -> R) -> R.

That way PropDecidable P is forall (R : Prop), InContext (Decidable P) R, and I can work with things... well actually it still winds up pretty awful. I can add specific classes I create bidirectional cut instances with to at least make InPropContext and so on so I can generalize a bit easier, but the whole thing remains a pretty big pain.

And even if I get all this setup, I have to manually lift and apply things at the right time at least somewhat. If something just asks for a Decidable P, I can't purely let it get automatically filled in the way instances normally do, I have to first use the with_context boilerplate.

Polymorphism at least becomes a little possible. I can't figure out a general way for it to go from a declared instance A -> B and a declared instance InContext A R to solve InContext B R, but if I turn everything into forall R, InContext A R -> InContext B R then it... works out at least sort of.

Still, this is a lot of pain and boilerplate, without even getting into how things behave around foralls of finite types.

Is there a better way? And what are the relevant keywords for this topic?


Last updated: Jun 18 2024 at 23:01 UTC