RFC: custom recursors

[nomeata]

Proposal

In a language that compiles pattern matching down to recursor theroems, it seems natural to be able to define custom recursors and have pattern matching and induction work just as before. Here are some use-cases (and I invite interested parties to expand):

• Arrays as stacks.

  I switched some code that was maintaining a stack from using Lists to arrays for performance reasons, and going from pattern matching to if … then … else and isEmpty and pop and back made it more ugly. It would be great if I could somehow use patterns .empty and .snoc xs s (possibly with nicer syntax) in match statements.o

• Fin n.

  This is defined as a subtype of Nat, which is a nice definitions. But some programs and proofs would benefit from being able to pattern match on the Fin n directly.

  In fact, there are two possible recursions that might be useful useful here (going from 0 up, or going from the last one down, changing n along the way). It would be good to have both.

• Refactoring.

  The List.Forall₂ predicate is defined inductively. It could have been defined recursively over the input lists, which would provide us with some (presumably) nice defeqs. But such a change would affect a lot of code – unless one could prove the existing constructors and induction principle with the new definition and set it up so that by induction and match work as before.

TODO (help welcome): Propose concrete syntax/commands/semantics.

Community Feedback

• Desire for inductive Fin n
• Refactoring List.Forall₂

Impact

Add :+1: to issues you consider important. If others benefit from the changes in this proposal being added, please ask them to add :+1: to it.

[david-christiansen]

• Backwards compatibility - some changes to datatypes could be be made in a way so that their old interface is still available, decreasing migration costs. For instance, a change from an inductively-defined Fin to the efficient subtype-based version wouldn't have had to break any code.

[alexkeizer]

There is some precedent for this in the induction tactic, which does allow custom recursors with induction ... using myRecursor. I'd propose we mirror that syntax for pattern matching as match ... using myRecursor with .... For example:

let i : Fin n := _
match i using Fin.succRec with
  | Fin.zero    => _
  | Fin.succ i  => _

[digama0]

The trouble with that is that cases and induction are only a single level destructuring, while match can do nested pattern matching. Where do you put recursors for subsequent matches?

[alexkeizer]

Personally, I would say it's already an improvement to be able to customize only the top-level match, without nesting. We could set a limitation that a single match statement can use only one recursor per type to destructure. Then the using ... syntax generalizes to taking a list of recursors.

let is : List (Fin n) := _
match is using List.reverseRecOn, Fin.succRec with
  | List.concat is (Fin.zero)   => _
  | List.concat is (Fin.succ i) => _
  | []                         => _

That would mean that we disallow the scenario where we have, e.g., a Sum (Fin n) (Fin m), where we would like to destructure with Fin.succRecOn in one case, but Fin.reverseInduction recursor in the other, in a single match. However, one can always rewrite such a nested match into multiple matches.

let i : Sum (Fin n) (Fin m) := _
match i with
  | .inl i => match i using Fin.succRecOn with
    | Fin.succ i => _
    | Fin.zero   => _
  | .inr j => match j using Fin.reverseInduction with
     | Fin.castSucc i => _
     | Fin.last            => _

Do you foresee many situations where we would have multiple recursors for the same type in a single match?

[nomeata]

Personally I'd be more inclined to explore the direction where each custom recursor has its own exclusive set of “constructors” from which the recursor is inferred. This avoids the need for explicit using and works nestedly, even in examples like yours.

[alexkeizer]

That's a nice idea! But, we should be careful to not make totality checking too complicated. We could say that when tagging an eliminator with the @[eliminator] attribute, the user can also specify a number of "key" constructors subject to the condition that it is not a constructor (key or otherwise) in any other tagged eliminator.

Then, whenever a key constructor occurs in a match it's directly clear which recursor to use. If there are multiple key constructors (from different recursors), this is always an error. We could keep the using ... syntax (either with a single recursor, or with a list) as an override for the eliminators that are not allowed to be tagged under these rules (which should not be too common).

[nomeata]

override for the eliminators that are not allowed to be tagged under these rules (which should not be too common).

Merely uncommon, or fully avoidable? When would it not be possible, not even with introducing new “constructors” that are just equal to existing one, but give you new names to associate with the eliminator?

[alexkeizer]

Good point! At first, I wondered if duplicating the constructors would lead to having to duplicate theorems as well, but since we're talking about term-mode match these constructors should only show up in expected types, where it's not super harmful.

Does that mean you're arguing against having the match ... using ... syntax at all?

[nomeata]

If we can do without, yes.

[Kiiyya]

Here are some use-cases (and I invite interested parties to expand)

One big application of this would be for fancier inductive types, such as inductive-inductive types (IITs), which are very useful when formalising type theory. This repo reduces IITs to Lean's mutual inductive types, and derives a recursor (see example). You can use the derived recursors directly, but being able to pattern match on them would be very nice. The motives can refer to other motives, for example in Con.rec (motiveCon : Con → Type) (motiveTy : {Γ : Con} → motiveCon Γ → Ty Γ → Type) ..., which I don't know how well it would fit into the existing pattern matching code.