Higher-order unification is pretty hard when you also have eta-equality for record types and definitional proof irrelevance. There's just too many ways for variables to disguise themselves as other things.

For example, consider a constraint _f u =?= v : B where u : A:

  • If u is a variable x, then we can just solve it with _f := \(x : A) -> v.

  • If u is eta-equivalent to a specific variable x, say u = (fst x , snd x), then we can eta-contract it and still solve the equation.

  • If the type of u is a unit type, then it is eta-equivalent to any variable of the same type, so if there are two variables x : A and y : A then we don't know which one to eta-expand u to. Luckily, in this case it does not really matter since we can just prune the dependency of the metavariable and solve it as _f = \(_ : A) -> v.

  • The fun really starts when you add definitional proof irrelevance into the mix. If the type A is in Prop (or sProp for the roosters here) then u is definitionally equal to any variable of type A, but also pruning the dependency of the metavariable could now lose solutions since A might be an empty type! So what do you do then, do you just try all the variables in the context to see if they have the right type? What if there's a variable in the context of a record type that has a (possibly nested) field of type A? Do we then need to first eta-expand the context variable? If there are multiple choices, do we then need to pick one that makes the variables in the arguments to the metavariable linear? This all feels way too complex and ad-hoc.

Here's the example that made me go down this rabbit hole, for those who are curious:

The actual unsolved constraint I am getting is the following:

a = _a_42 (x≢y = (λ z → record { irr = _ })) (blocked on _a_42)

@agdakx Does higher-order unification correspond to anything that humans do (but are not aware of it)?

@andrejbauer Agda uses higher-order unification to figure out the values of implicit arguments, and I believe human brains might be using a similar algorithm intuitively when reading mathematical notation. Though I would expect the human version to be much messier and reliant on heuristics. It's similar to how a human solves a sudoku vs how a computer would solve it: they have very different computational constraints and hence use very different algorithms, but in the end they should both get to the unique solution (if one exists).

@agdakx @andrejbauer indeed that's how I read math texts: due to my lack of math education (and poor English reading skill) I usually have lesser knowledge the author expects me to, and I'll have to delay the understanding of particular notation/concept until later text tells me more explicitly about it. But it's getting better

@agdakx I think the most concise description of the SProp situation is: strengthening in the presence of SProp is undecidable because it depends on inhabitation.

Unification depends on strengthening in many places (e.g. occurrence checking) so we can't hope for completeness even in the simplest pattern fragment.

I think this an instance of a classic design issue tradeoff, where it can be preferable to keep your automatic analysis/inference/solver dumber in order for the users to better predict the outcome.

The philosophy we follow in Agda is that we only solve metavariables if there is a unique solution (up to definitional equality). So the user does not have to care about the details of the unification: if it finds a solution, it is THE solution. But I admit that irrelevance complicates the picture by making even the pattern fragment undecidable.

Sign in to participate in the conversation

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