Understanding typeclass search & outParams

Stream: general

[Mirek Olšák]

I am planning to teach Lean, so I tried to dig deeper to a few topics, one of them is typeclass search. Originally, I thought that it does search similar to logical-programming (like prolog), but it seems that it never can have the full strength of prolog because it needs to know the direction of information flow given by outParam, correct?
I tried the following implemention of a sum using a logical program:

class PrologSum (a : Nat) (b : outParam Nat) (c : outParam Nat) where
  reason : String

instance (a : Nat) : PrologSum a 0 a where
  reason := s!"base {a}"
instance (a b : Nat) (c : Nat) [h : PrologSum a b c] : PrologSum a b.succ c.succ where
  reason := s!"{h.reason}, update {a} {b}+1 {c}+1"

class EvalPrologSum (a b : Nat) where
  c : Nat
  reason : String
instance (a b c : Nat) [h : PrologSum a b c] : EvalPrologSum a b where
  c := c
  reason := h.reason

class EvalPrologDiff (c a : Nat) where
  b : Nat
  reason : String
instance (a b c : Nat) [h : PrologSum a b c] : EvalPrologDiff c a where
  b := b
  reason := h.reason

#eval (inferInstance : PrologSum 2 2 4)    -- A
#eval (inferInstance : EvalPrologSum 2 2)  -- B
#eval (inferInstance : EvalPrologDiff 4 2) -- C
#eval (fun {x} [PrologSum 2 2 x] _ ↦ x) () -- D
#eval (fun {x} [PrologSum 2 x 4] _ ↦ x) () -- E

Then I looked at which examples succeed, and which fail based on the type annotation for variables b & c, and I got a bit confused.

  A        B        C        D        E
* * *    . * *    . . .    . . *    . . .
* * *    . * *    * * *    . . *    . . .
* * .    . * *    * * *    . . .    * * .

`*` = Success
`.` = Fail
Row    1 / 2 / 3 = b : Nat / semiOutParam Nat / outParam Nat
Column 1 / 2 / 3 = c : Nat / semiOutParam Nat / outParam Nat
-/

When both b, c are outParams, why does case A fail (I thought it is the most basic one), while both B, C succeed? Also, I was a bit surprised that D is so much harder than B (and analogously E than C), why? Is there another one-liner that could emulate B without having to build a new typeclass?

[Anne Baanen]

The best way to see how Lean chooses to look for instances is by enabling set_option trace.Meta.synthInstance true (and sometimes also set_option trace.Meta.isDefEq true if you want to know why an instance fails to apply). For example, for case A we see:

[Meta.synthInstance] ❌️ PrologSum 2 2 4 ▼
  [] new goal PrologSum 2 _tc.0 _tc.1 ▶
  [] ✅️ apply instPrologSumOfNatNat to PrologSum 2 0 2 ▼
    [tryResolve] ✅️ PrologSum 2 0 2 ≟ PrologSum 2 0 2
    [answer] ✅️ PrologSum 2 0 2
  [] ❌️ result type
        PrologSum 2 0 2
      is not definitionally equal to
        PrologSum 2 2 4
  [] result <not-available>

In words: instance search is called with a goal of type PrologSum 2 2 4. It immediately turns the outParams into metavariables: _tc.0 and _tc.1 and finds a solution for the problem of the form PrologSum 2 _ _, namely 2 + 0 = 2. Then it checks that this matches the goal, and errors.

This is how it works for any outParam: any concrete values are first erased and replaced with metavariables, and then the resulting type will be checked. The reason, as I understand it, that Lean is implemented this way is to make instance synthesis and unification independent from each other. If a suble change in elaboration means that unification assigns slightly different values, we want the instance search algorithm to still work the same and not start returning different answers. (There is a similar phenomenon where an instance can already be (partially) found through unification, but this partial answer is not taken into account when synthesizing the new one: it's only checked when synthesis is complete.

semiOutParams, like outParams, include a promise that after a successful instance synthesis, they will be metavariable-free. Unlike outParams, however, they can already be assigned at the start of instance search. They will, as a result, not assign metavariables created outside of the context of the instance search. (Which is why D fails for semiOutParams.)

From a user's perspective, the rule for outParams is that there should be only one solution for any goal, no matter which assignments to (semi)outParams are made.

[Mirek Olšák]

Thanks! I think it makes sense. The (semi)OutParam is needed to enable prolog-like search with open metavariables, but both options have some difficulties in interacting with the external query. outParam ignores the input, and semiOutParam disallows assigning external metavariables.

[Mirek Olšák]

But now, I got confused by another example, what is so special about 2+2 in the following example (term reduction)? I tried to enable trace.Meta.isDefEq but I am unsure which line is responsible for it.

class myClass (x : Nat) where
  value : Nat

instance cinst1 : myClass 4 := ⟨ 1 ⟩
instance cinst2 : myClass (2+2) := ⟨ 2 ⟩
instance cinst3 : myClass (2*2) := ⟨ 3 ⟩
instance cinst4 : myClass (2^2) := ⟨ 4 ⟩
instance cinst5 : myClass (id 4) := ⟨ 5 ⟩

set_option trace.Meta.synthInstance true
set_option trace.Meta.isDefEq true

#instances myClass (4)    -- 1, 2
#instances myClass (2+2)  -- 2
#instances myClass (2*2)  -- 3, 2
#instances myClass (2^2)  -- 4, 2
#instances myClass (id 4) -- 5, 2

[Aaron Liu]

It's the first one that got tried?

[Mirek Olšák]

I wouldn't say so. If I comment out the line with 2+2 instance, every expression is only matched with itself.

[Aaron Liu]

check the discr tree keys

[Aaron Liu]

one of these is not like the others

class myClass (x : Nat) where
  value : Nat

instance cinst1 : myClass 4 := ⟨ 1 ⟩
instance cinst2 : myClass (2+2) := ⟨ 2 ⟩
instance cinst3 : myClass (2*2) := ⟨ 3 ⟩
instance cinst4 : myClass (2^2) := ⟨ 4 ⟩
instance cinst5 : myClass (id 4) := ⟨ 5 ⟩

#discr_tree_key cinst1
#discr_tree_key cinst2
#discr_tree_key cinst3
#discr_tree_key cinst4
#discr_tree_key cinst5

[Mirek Olšák]

That actually makes sense as a reason why it behaves that way.

[Mirek Olšák]

But not really why (2+2) gets translated into a joker

[Mirek Olšák]

It might not be worth it digging much deeper but it is a peculiar curiosity :slight_smile: .

[Robin Arnez]

Offsets (e.g. Nat.succ x, x + n) are jokers to e.g. allow

instance instNeZeroSucc {n : Nat} : NeZero (n + 1) := ⟨succ_ne_zero n⟩

to match NeZero 4

[Mirek Olšák]

So the conclusion is: when we want to match a natural number using definitional equality, and not exact structure, add +0 :slight_smile:

[Jovan Gerbscheid]

It seems that the #instances command doesn't actually do the required unification, because instance search isn't allowed to unfold definitions such as id. (but the standard operations on Nat are treated specially, so they are an exception to this rule)

[Jovan Gerbscheid]

Type class search operates in the reducible_and_instances transparency, which means that instances and definitions marked @[reducible] will be unfolded.

[Mirek Olšák]

Do you know if proper logical programming is possible through typeclass inference? I know it is not the intention but as an exercise, I tried to write a basic intuistionistic solver through it but the search still feels too much out of my control. I am not sure how to make forced moves (like Prolog's cuts) such as "If you see it is an implictaion, always intro, and do not try anything else", or more importantly, "If the assumption is already present in the context, do not add it." I thought that a combination of outParams and prioritys could it, it works in basic examples but in a more complex setup, it breaks, and is hard to follow.
IntuSolve.lean

[François G. Dorais]

You probably don't want to use Prop directly because matching on Prop is flaky. It's better to define a prop-like inductive type and evaluate into Prop when you need it.

[Mirek Olšák]

I am a bit hesitant to write it with a custom inductive, then the hard problem will be even more unreadable (so I will be unsure if I made a mistake)... And the matching seems working to me, only that sometimes I get multiple equal assumptions, and I don't understand how (maybe it decided to backtrack?)...

[Mirek Olšák]

Why exactly is it flaky?

[Jovan Gerbscheid]

Maybe @François G. Dorais means that unifying proofs is flaky, because unification might decide to not assign metavariables, and use proof irrelevance instead. But unifying propositions is fine.

[Aaron Liu]

Mirek Olšák said:

Do you know if proper logical programming is possible through typeclass inference? I know it is not the intention but as an exercise, I tried to write a basic intuistionistic solver through it but the search still feels too much out of my control. I am not sure how to make forced moves (like Prolog's cuts) such as "If you see it is an implictaion, always intro, and do not try anything else", or more importantly, "If the assumption is already present in the context, do not add it." I thought that a combination of outParams and prioritys could it, it works in basic examples but in a more complex setup, it breaks, and is hard to follow.
IntuSolve.lean

Note that the typeclass system is not designed for this. For example, it will only use a hypothesis if it appears in the goal, since it only discovers them by unification.

[Aaron Liu]

see also the docstring for docs#Fact

[Mirek Olšák]

I know, I know,
Mirek Olšák said:

I know it is not the intention but

[Mirek Olšák]

I do not intend it as a lean automation, rather a toy solver in a similar way as one could try to write a sokoban solver, or anything similar.

[Mirek Olšák]

I also tried @[default_instance] but that doesn't seem to have any effect -- Lean is always happy to build a ∧ a with AddToAnd.combine a a : AddToAnd a a (a ∧ a)

[Aaron Liu]

what are you trying to do

[Aaron Liu]

what's the problem here

[Mirek Olšák]

I tried to write a logical program that operates on "states" of the form (Ctx Goal : Prop), where Ctx is a conjunction of assumptions, and Goal is the current Goal. I want to ensure that I never get repeated assumption in Ctx, so I implemented AddToAnd which should skip the double assumption. However, this skipping is not reliable, when I look at the trace of the last problem, I eventually get ✅️ apply AddToAnd.combine to AddToAnd a a (a ∧ a) which I was trying to avoid.

[Aaron Liu]

Do you really really want to use typeclass for this?

[Mirek Olšák]

Yes, but if you say it is not possible, ok. I was curious how typeclasses & logical programming relate.

[Mirek Olšák]

Is it really that uncommon in typeclass practice that you want to prevent usage of a certain rule with a certain pattern?

[Mirek Olšák]

But answer "You cannot implement prolog-like cuts with typeclasses." is a knowledge I am happy with.

[Aaron Liu]

Mirek Olšák said:

Is it really that uncommon in typeclass practice that you want to prevent usage of a certain rule with a certain pattern?

I have never come across such a situation before

[François G. Dorais]

Mirek Olšák said:

But answer "You cannot implement prolog-like cuts with typeclasses." is a knowledge I am happy with.

That is correct: there are no prolog-like cuts with type classes in Lean. However, Lean type classes also don't do linear resolution in the strict sense. So cuts wouldn't necessarily work as expected from the prolog point of view.