Prompted by recent discussions, I got the boundary scavenging prototype back to roughly where it used to be. Demo attached!

If you want the details:

  • Boundary information is not associated with clauses, but with interaction points

  • This information is collected during unification, by looking at equations which are headed by a metavariable and "in the pattern fragment, modulo endpoints" (i.e.: all arguments are variables, which must be distinct, or i0/i1)

  • A problem like this doesn't give a unique solution, but it does give a partial solution: it's a face of a partial element which the meta must extend (internally I don't represent these as Partials... yet). A spine like this can still be inverted [1], by skipping over endpoints, so the RHS can be put in the meta's context

  • When printing, we can show the user this information

  • Bonus: Unsolved boundary constraints aren't shown to the user (strictly speaking they shouldn't be highlighted, either, but it's a WIP). Might be too much, but I decided to suppress any unsolved constraint that's headed by an interaction meta

  • Bonus: Since the equations we recover are in the meta's context, we can print the value of the term at each face, too! This closes a very old feature request:

[1]: One of the many reasons trying to extend the pattern fragment sucks is that now there's ambiguity over how to abstract over the RHS:

?0 A x y p i0 = p i0

should this invert to

?0 := λ A x y p i (i = i0) → p i0


?0 := λ A x y p i (i = i0) → p i

but happily in this case it doesn't matter (I use the former). Now to test the hell out of the fancy substitutions I'm inventing...

This weekend's project is off to a strong start IMO!

Btw, don't be fooled: that's just toggling between a few reduction levels I hardcoded, not a proper implementation of reducing the subexpression at point.. that would be implementable but it'd be a bit of a faff right now.

Oh also the implementation is a right mess right now because all this is doing is bumping an integer variable and re-rendering the error message. That's something I want to implement but preferably without going full reflex spider on the pretty printer

I think this will make Agda easier to use, or at least make errors a bit easier to parse at a glance

screenshot without description 

Recovering from type errors is totally doable actually

I thought I was playing a silly little game about looking for my brother not receiving a violent call-out for my teenage years

Show older

A Mastodon instance for programming language theorists and mathematicians. Or just anyone who wants to hang out.