Amélia Liao @amy@types.pl

7:14 and I've succeeded in cooking some spaghetti

menacing

ya girl's refactoring

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: https://github.com/agda/agda/issues/3690

[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

or

?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...

Look at my cat Melog

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

Recovering from type errors is totally doable actually

It's getting evil-er

I am not doing good, actually — I am doing evil

suffering from this

He is Melog

Looks like my cube ideas work after all 😄

Thanks for everything, Edinburgh 👋

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

Ahh so that's how Agda is designed

Is this anything?

what does this MEAN my guy

Github notifications with threatening auras