Amélia Liao @amy@types.pl
Student of homotopy type theory and (higher) category theory (this account adheres to the implicit ∞-category convention).
I help maintain Agda Γ ⊢ 🐔, maintain the 1Lab 🧊🔬, and very occasionally write on my blog 👩🏫✍️
Joined Jan 2022
@andrejbauer @MartinEscardo @jonmsterling @ltchen This is also why unification in cubical Agda can still be very frustrating... if matching on a truncated higher inductive type, for example, the user knows exactly what term(s) to use to handle the truncation case. They expect Agda to know too --- but there are infinitely many possible solutions, especially since the metas I'm thinking of are only constrained on one endpoint.
Example: α i0 =?= x, x : A, and Ap : is-prop A. Do you solve α := refl? Why not α := Ap x x? Heuristics for trying to get rid of these range from "surprising" to "prohibitively expensive" to "incorrect".
This is orthogonal to the problem of constraint reporting in Cubical Agda, which Jon mentioned above — and is going away in the upcoming release! Most endpoint constraints will be reported under the Boundary heading in the goal display, though I wouldn't be surprised if you can get a constraint I haven't covered (even sticking to paths and HITs, even) — I'd consider those bugs in the boundary scavenging code, though.
@andrejbauer @MartinEscardo @jonmsterling @ltchen Then I say "that's why we have syntax for explicitly applying instance arguments."
The reason for avoiding this shortcut — we do this for all arguments, of course, not just instances — avoiding surprises coming from the implementation of the conversion checker. Bugs aside, Agda will never commit to a solution that has the potential to make future code not typecheck. The trivial class of examples is
foo _0 =?= foo 1
foo _0 =?= foo 2
Depending on what order we look at these constraints on, the other will fail — and if these arise from terms which are far away, the type error you get ("1 is not 2" or "2 is not 1", depending on the phase of the moon) would be surprising, frustrating, or both. This problem is only made worse by, e.g., postponement, pruning, eta-expansion, etc; all of which are required in practice.
By default, we chose not to surprise the user in inscrutable ways, at the cost of sometimes presenting them with easy-seeming problems (or worse, sometimes presenting them with these problems after a long while). More recently, we've implemented an option that allows users to be very confused very fast (--lossy-unification), if that's what they'd like
@MartinEscardo @jonmsterling @ltchen Part of the difference is from Lean using first-order unification. A conversion-checking problem of the form
Method instance_1 x y = Method ? x y
does not actually tell you anything about which instance should be selected to solve ?.
Amélia Liao
boosted
@JacquesC2 As others have noted, Presheaves exist as a place where we can talk about representability, which is a _really_ useful tool for doing internalization without tears.
When category theorists internalize, they generally define operations in the most “minimal” context possible, and then rely on precomposition to handle weakening the operations into an arbitrary context. This is pretty unnatural from the type-theoretic POV, where we prefer to define operations in an arbitrary context, and then state how substitution commutes through the operation. Categorically, this is defining a presheaf of structures, and then demanding that it be representable. See https://1lab.dev/Cat.Monoidal.Diagram.Monoid.Representable.html for a concrete example of this phenomena.
This insight is key to being able to avoid nightmarish pullbacks when trying to internalize categories, which only arise when we demand that composition be defined in the smallest context possible.
C23 adds a set of macros for doing checked addition, multiplication, and subtraction
They write the result to a pointer and returns false if the value written is correct (ie didn't overflow)
They return
false
to indicate
success
@totbwf purchasing a bag of NIST Standard Reference Lambda Abstractions
I found out that JTC1/SC22 had a working group called "binding techniques" and I'm gonna be honest I don't know enough words to express how disappointed I was to find out there is not, in fact, an ISO standard de Bruijn index
pretty sure i just managed to overthink my way into a migraine so i am going to log off and put as much space between me and light as possible
suddenly hit with an overwhelming sense of dread about what miracle i'm gonna have to pull to find a way to keep working on agda after october
New little Agda feature I'm cooking on the side (actually a second attempt...) got done enough in a day that I feel comfortable sharing the prototype:
https://github.com/agda/agda/pull/6669
@agdakx Not a fan of Eliminating-eliminating higher pattern-pattern matching? 🥲
just as i decide to go for a walk while agda compiles, it finishes. when did GHC add this feature
nothing can stop me from making extremely unfunny jokes about how the inductive-inductive version of [something] is called [something]-[something].
Whatever the next Agda issue is, it'll mark us being 2/3rds of the way to 10_000
Just want to make sure I'm not stepping on anyone's toes, I guess
If I know (of) someone who might be working on something I want to pursue, is it considered polite to reach out and ask whether.. well, first, they're actually working on that?
though I will say it's very unusual to break user code and go "Is my patch bad? No, it is the users who are wrong"
Normally when user code breaks with f ≠ g, and f, g are two adjacent variables in the context, it's because you messed up de Bruijn indices somewhere. Garden variety.
In this case it was the positivity checker just casually deciding to break transitivity of conversion by not using the polarity associated with the data type name, but with some secret info from god-knows-where. Lovecraftian
Pretty often I'll investigate a garden-variety Agda issue and end up revealing a lovecraftian Agda issue lurking right beneath
Student of homotopy type theory and (higher) category theory (this account adheres to the implicit ∞-category convention).
I help maintain Agda Γ ⊢ 🐔, maintain the 1Lab 🧊🔬, and very occasionally write on my blog 👩🏫✍️
Joined Jan 2022
