code generator does not support recursor '....rec' yet

Stream: new members

[Kevin Cheung]

To better understanding recursors, I wrote the following:

namespace Foo

inductive Weekend where
  | sunday : Weekend
  | saturday : Weekend

#check @Weekend.rec.{1} (fun _weekend => Nat) 0 6 -- Weekend.rec 0 6 : Weekend → ℕ
#reduce @Weekend.rec.{1} (fun _weekend => Nat) 0 6 Weekend.saturday -- 6
def f := @Weekend.rec.{1} (fun _weekend => Nat) 0 6 Weekend.saturday
-- code generator does not support recursor 'Foo.Weekend.rec' yet,
-- consider using 'match ... with' and/or structural recursion

end Foo

In practice, I certainly will use match ... with. But I am wondering what the technical reasons are for not (yet) supporting the way f is defined above.

[Henrik Böving]

The reason is that recursors allow for surprising performance. If you run e.g. List.rec to e.g. implement isEmpty you will forcibly have to iterate through the entire list. That's because the cons case forcibly requires you to provide the result of applying the function recursively already, even if you don't use it. Note that a simple use def analysis that eliminates this recursive call if it is not required does not suffice here because maybe your cons case contains an if-then-else that only accesses the recursive call in one situation etc. Furthermore you would probably also expect that the recursive call would be only done once instead of multiple times whenever you refer to the recursive result, so simply bubbling the call to its use sites would also not be correct.

So in summary there is a non trivial transformation required to turn code using recursors into code that probably doesn't have surprising performance characteristcs.

[Florent Schaffhauser]

You can also consult #lean4 > Non-dependent recursor.

[Kevin Cheung]

Thank you for the pointer. The part about recCompiled being a workaround is something that I still don't quite understand; (i.e. I don't understand why it is a workaround that works.) Could I DM you for insights?

[Kajani Kaunda]

Thank you Riccardo. Learning the ropes!

[Kevin Cheung]

Does match ... with make use of .rec?

[Henrik Böving]

Yes and no, the way that the code generator/logic Schism works is as follows: Lean initially does some pre processing on your def before turning it into something called a PreDefinition. At this point the code is still using match syntax and some other goodies but is already a bit desugared. Then the dataflow splits into two parts:

1. One part goes to the code generator, the code generator turns the match into a case split on data that is available at runtime and does the recursive calls directly etc.
2. The other part goes into the logic, this is the component you interact with when proving things. This code path turns match into a construct that is based on recursors because recursors are primitive parts of the axioms that Lean operates with. This version is then the one that is actually used in all the proofs, type checking, etc.

[Florent Schaffhauser]

I'm inclined to say no, but maybe an expert can weigh in.

[Florent Schaffhauser]

Oh, there you are :sweat_smile:

[Henrik Böving]

Note that this approach is not necessarily the thing you must do, for example Coq uses a different desugaring of match that has different properties.

[Kevin Cheung]

Interesting. I didn't know I am going down into a rabbit hole.

[Florent Schaffhauser]

The way I see it is match performs pattern-matching to try and define a function T -> X (or more generally a dependent function (t : T) -> F t for some type family F : T -> Type), while T.rec can be viewed as a function that returns a function from T to X (or more generally a dependent function). In that sense, T.rec. gives you a method that may or may not work to define your function. Pattern-matching can in principle be used to define a function out an inductive type and indeed it is used in the definition of the function returned by T.rec.

[Florent Schaffhauser]

Kevin Cheung said:

Thank you for the pointer. The part about recCompiled being a workaround is something that I still don't quite understand; (i.e. I don't understand why it is a workaround that works.) Could I DM you for insights?

If you have a particular example of an inductive type T in mind, I think you can probably define a function T.rec' by hand, and then use that to construct dependent functions out of T.

[Henrik Böving]

and indeed it is used in the definition of the function returned by T.rec.

No, T.rec is a primitive in Lean, it does not carry a definition, it is a postulate that is auto generated for each inductive based on the rules of the type theory. On the logic side you cannot desugar more than T.rec

[Kevin Cheung]

I think I just need a bit of time to digest all the dependent type theory stuff. It's all new to me.

[Henrik Böving]

Just to clarify this @Flo (Florent Schaffhauser) , the logic of Lean has no clue what a match is, match is merely surface level syntax. The logic only knows what recursors are and how they are supposed to compute. The elaborator (which is the component that reduces surface level syntax down to core logic terms) knows how to turn a match into one or multiple calls to a recursor.

[Florent Schaffhauser]

Henrik Böving said:

and indeed it is used in the definition of the function returned by T.rec.

No, T.rec is a primitive in Lean, it does not carry a definition, it is a postulate that is auto generated for each inductive based on the rules of the type theory. On the logic side you cannot desugar more than T.rec

Yes, but what I meant is, if you take for instance List.rec, then the dependent function f : (L : List R) -> F L that it induces, starting from a term h1 : F List.nil and a function h2 : (a : R) -> (l : List R) -> F l -> F (a :: l), should be defined as follows:

fun (L : List R) => match L with
| List.nil => h1
| List.cons a l => h2 a l (f l)

[Henrik Böving]

It has the same computation rules yes (mostly because this quite literally lowers to an application of List.rec to h1 and h2), but it is not defined in this way.

[Florent Schaffhauser]

I see, thanks!

[Florent Schaffhauser]

Henrik Böving said:

Just to clarify this Flo (Florent Schaffhauser) , the logic of Lean has no clue what a match is, match is merely surface level syntax. The logic only knows what recursors are and how they are supposed to compute. The elaborator (which is the component that reduces surface level syntax down to core logic terms) knows how to turn a match into one or multiple calls to a recursor.

Oh, I see! This explains why the keyword match was always a bit mysterious :sweat_smile: Thanks for the explanation :thank_you:

[Kevin Cheung]

So there is a bit of magic behind match. Good to know.

[Florent Schaffhauser]

Right, if I understand correctly, the magic is what Henrik Böving was explaining above: https://leanprover.zulipchat.com/#narrow/stream/113489-new-members/topic/code.20generator.20does.20not.20support.20recursor.20'.2E.2E.2E.2Erec'.20yet/near/450185470

[Kyle Miller]

If you use set_option pp.match false you can turn off match expression pretty printing. Each match is a special function (known as a "matcher", fittingly enough) that logically is backed by a recursor but which the compiler knows how to compile.

[Kyle Miller]

#print List.head
/-
def List.head.{u} : {α : Type u} → (as : List α) → as ≠ [] → α :=
fun {α} x x_1 ↦
  match x, x_1 with
  | a :: tail, x => a
-/

set_option pp.match false
#print List.head
/-
def List.head.{u} : {α : Type u} → (as : List α) → as ≠ [] → α :=
fun {α} x x_1 ↦ List.head.match_1 (fun x x ↦ α) x x_1 fun a tail x ↦ a
-/
#print List.head.match_1
/-
def List.head.match_1.{u_1, u_2} : {α : Type u_1} →
  (motive : (x : List α) → x ≠ [] → Sort u_2) →
  (x : List α) →
  (x_1 : x ≠ []) →
  ((a : α) → (tail : List α) → (x : a :: tail ≠ []) → motive (a :: tail) x) →
  motive x x_1 :=
fun {α} motive x x_1 h_1 ↦
  List.casesOn (motive := fun x ↦ (x_2 : x ≠ []) → motive x x_2) x (fun x ↦ absurd ⋯ x)
    (fun head tail x ↦ h_1 head tail x) x_1
-/