aya-dev
aya-dev copied to clipboard
aya-prover
Unification in Typeclass Resolution
Say in type class resolution, we meet the following instance
instance FTrans {A B C} {{ab: F A B}} {{bc: F B C}} : F A C
and we have the resolution problem F X Y. In the description of the tabled typeclass resolution paper, it will generate two subgoals on this instance: F X ?M and F ?M Y.
However the ?M does not behave exactly like a metavariable. Namely, it can have multiple ~~temporary~~ [worse, may be not temporary because both solutions may be applicable to the remaining subgoal] solutions: if we have instances F X Z1 and F X Z2, then ?M equates to both in the resolution process.
Should we change how our metavariable works? Or should we use another kind of syntactic construct for this purpose?
@re-xyr Imho instance search and implicit inference are different anyway, so I'll prefer using another construct
I have another problem: If we have a function f : {A B C : Set} {{I : K A B C}} -> ... and class K {A B : Set} {out C : Set} where out signs the lift of meta constraint (i.e, I will be resolved after A and B solved but will not wait for C), then the problem we need to resolve is F A B ?M where ?M meta. However this conflicts with the previous discussion that ?M should be a separate construct.
I thought about what does it mean when an instance matches a problem (i.e. reduces the problem into zero or more subgoals). The type of the instance may contain [bound variables, free variables] (TODO: can it contain metavariables? I think we should prohibit this). The problem may contain [free variables, metavariables]. Note: here free variables includes references to defs. We say the instance matches the problem iff we can find a most general unifier that may contain both bound variables and metavariables, but not free variables.
instance FTrans {A B C} {{ab: F A B}} {{bc: F B C}} : F A C -- Bound A, C.
instance Fxy : F X Y -- Free X, Y.
Fxy does not match problem F Z1 Z2 because the most general unifier X -> Z1, Y -> Z2 contains free variables. FTrans however does match F Z1 Z2.
Like if someone deliberately leaves holes in the type of their instance.
Then how are these instances tycked?
Maybe we should seriously consider adding most general unifiers...
I agree. It is useful anyway
Maybe we can also implement RTT, making our type theory to some extent extensional...
Then how are these instances tycked?
Edge case alert:
class F (A : Set) {}
instance : F _ {}
Then the instance should raise a type error saying that unsolved meta at location
Are you interested in implementing it?
Yes.
aya-prover/aya-prover-proto#503 when
Then the instance should raise a type error saying that unsolved meta at location
Because meta should be solved within the definition? btw, this is why I posted https://twitter.com/fun_ext/status/1401468891474268162
aya-prover/aya-prover-proto#503 when
I think its unrelated to most general unifiers but this weekend maybe
Then the instance should raise a type error saying that unsolved meta at location
Because meta should be solved within the definition? btw, this is why I posted https://twitter.com/fun_ext/status/1401468891474268162
I suggest asking in AK's discord server. Have you joined it yet?
aya-prover/aya-prover-proto#503 when
I think its unrelated to most general unifiers but this weekend maybe
Ik but I'm very looking forward to it
I suggest asking in AK's discord server. Have you joined it yet?
No. Could you invite me?
I suggest asking in AK's discord server. Have you joined it yet?
No. Could you invite me?
https://discord.gg/89c3EXtx
I suggest asking in AK's discord server. Have you joined it yet?
I'm afraid of speaking in front of strange ppl. How should I ask a question?
I suggest just add this single restriction: No Unsolved Meta In Instance Type
But another problem: Should restriction be checked after checking the head or the body? If the head, then it won't be possible to write this perfectly reasonable instance
instance Add _ {
_+_ (m n : Nat) => m +N n
}
If the body, then how should we typecheck
instance Add _ {
_+_ (m n : Nat) => match m, n of
zero, n => zero
suc m, n => suc (m + n) -- This instance search how?
}
?
So maybe not "No Unsolved Meta In Instance Type", but "Ignore Instances With Unsolved Metas"?
Basically we can accept only these two kinds of mappings: [meta in problem -> term in instance type, bound variable in instance type -> term in meta]. Maybe we can instead check if the final most general unifier only contains these two kinds of mappings and not worry about whether metas are present in instance types.