understanding a recursor for a simple inductive type

Stream: new members

[rzeta0]

The following is a simplified inductive type based on a bigger example from TPIL4:

import Mathlib.Tactic

inductive Weekend where
 | sunday : Weekend
 | monday : Weekend


#check Weekend.rec

The output from #check is:

Weekend.rec.{u} {motive : Weekend → Sort u} (sunday : motive Weekend.sunday) (monday : motive Weekend.monday)
  (t : Weekend) : motive t

I'm trying to do two things: (1) understand what a recursor is (my preconception was that it was an iterator), and (2) understand what the above output actually means.

I'd welcome help on those 2 things.

My own attempt is this - the following is likely wrong:

• Weekend.rec.{u} {motive : Weekend → Sort u} means Weekend is a type, not a term.
• motive is not defined so is a placeholder for a function that maps from Weekend to some other type u.
• IF sunday and monday are in the co-domain of that function motive, and t is of type Weekend THEN that function motive can be applied to t (interpreted as any t in Weekend)

Not sure what that last bullet point actually means. I know Kevin Buzzard's blog tries to explain this but it was beyond my brain sadly.

[Ruben Van de Velde]

High level, the purpose of a recursor is to define a function whose domain is (in this case) Weekend, by specifying how the function acts on each variant

[Ruben Van de Velde]

So if I eat one pizza on Sunday and two pizzas on Monday, you can define a function Weekend → Nat that returns how many pizzas I had by writing

noncomputable def pizzas (d : Weekend) : Nat :=
  Weekend.rec
    (sunday := 1)
    (monday := 2)
    d

[Ruben Van de Velde]

In this case, motive is fun _ => Nat

[rzeta0]

Thanks Ruben. Let me dig a bit deeper.

The pizzas function maps elements of Weekendto a natural number.

The definition you've kindly provided uses Weekend.rec and not match d with to make clearer what recursor does.

Looking at your example, my initial assumption that a recursor is an iterator that provides access to every element of an inductive type (lazily, perhaps) seems correct. Is it?

And the match d with is syntax sugar for what you have written?

[Ruben Van de Velde]

Depends on what you mean by "iterator", I suppose :)

[Kyle Miller]

If you're familiar with object-oriented programming design patterns, recursors implement the visitor pattern. The recursor is the visit method.

Rather than passing a single object to visit, in Lean we pass multiple arguments. The arguments could in principle be the methods of a visitor object.

[Vlad Tsyrklevich]

@Kyle Miller Thanks, this is a nice description. Makes me wish there were a dictionary for translating functional patterns into their imperative equivalents