SoundLogic (May 14 2024 at 01:34): 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?
Pierre Courtieu (Oct 08 2024 at 06:28):Since no answers was given to your message I just wanted to say that I think you nail a common problem with type classes. They are quite difficult to put in place. You may solve some of your problems by using Typeclasses eauto := (bfs). temporarily. Using this setting globally would probably trigger problems elsewhere.
In short: I sympathize.
Maybe @Matthieu Sozeau could give a hint on the context thing.
Gaëtan Gilbert (Oct 08 2024 at 06:34):If I have Decidable A -> Decidable B, getting PropDecidable A -> PropDecidable B for free is very desirable.
but forall A B, (Decidable A -> Decidable B) -> PropDecidable A -> PropDecidable B is not provable is it? (without axiom of choice)
Last updated: Oct 13 2024 at 01:02 UTC