search

jonsterling / racket-grit

Grit: the kernel around which a PRL forms
Other
3 stars 0 forks source link

Judgments with multiple outputs #11

Open jonsterling opened 7 years ago

david-christiansen commented 7 years ago

Why do we need multiple outputs, rather than e.g. a pair of outputs?

jonsterling commented 7 years ago

@david-christiansen Do you mean, why not have the extract itself be a pair, and then have a judgment for deconstructing this piece by piece? Or something else?

If the former, then that is a way to simulate the thing that I want. But ultimately it would be more seamless if it were integrated into the refinement apparatus, since the simulation also would require special "destruction" rules to be applied in order to one of the extracts out. In the end, I think the restriction to a single output is artificial... On paper, the multiple-output view works better anyway (because of the connection with Lawvere theories).

david-christiansen commented 7 years ago

Yes, I meant the former. But it does seem that multi-output would be cleaner.

jonsterling commented 7 years ago

OK, cool. In RedPRL, which supports only one output, I do a trick kind of like what you suggest (but in a more ad hoc way than you suggest) and it works alright; but I don't think it's practical for some more fancy ideas that I've been having lately...

In particular, I have this sick idea that I want to try out for a "two-dimensional PRL", where the truth/inhabitation judgments output twin elements, and you can use various rules to indirectly affect either side. This gives you a lot of control, and should enable us to eliminate the duplication between inhabitation judgments and structural equality judgments (and their rules!), replacing the latter with a bunch of derivable rules.

david-christiansen commented 7 years ago

Nice!

jonsterling commented 7 years ago

I think in order to do this systematically, we'd have to add sigma types to the LF and maybe adjust the lambda abstraction to do deep pattern matches on products in the style of focusing, which makes things a bit more complicated.

Maybe we should hold off, and think about using macros and helpers to paper over the bureaucracy of the encoding under the current order...