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