implemented_by and rec

Stream: lean4

[Joachim Breitner]

I was playing around a bit with implemented_by, to see if I can completely swap out the representation of a type (like with Array and List), but staying within lean (so not extern + C code).
But it seems that my attribute [implemented_by RArray.rec_unsafe] RArray.rec which swaps out the implementation of the recursor did not affect how a pattern matching is compiled. Are pattern matches not compiled via the types recursers, or where else did my thinking go wrong?

Here is what I tried:

inductive RArray (α : Type _) where
  | nil : RArray α
  | snoc : RArray α → α → RArray α

unsafe def RArray.nil_unsafe {α} : RArray α :=
  unsafeCast (Array.empty : Array α)

unsafe def RArray.snoc_unsafe {α} : RArray α → α → RArray α :=
  unsafeCast (fun as a => as.push a : Array α → α → Array α)

unsafe def RArray.rec_unsafe.{u, u_1} {α : Type u_1} {motive : RArray α → Sort u} (nil : motive RArray.nil)
  (snoc : (a : RArray α) → (a_1 : α) → motive a → motive (RArray.snoc a a_1)) (t : RArray α) : motive t :=
  let t' := (unsafeCast t : Array α)
  if h : t'.size - 1 < t'.size then
    let x := t'[t'.size -1]
    let t2 := (unsafeCast t'.pop : RArray α)
    (unsafeCast (snoc t2 x (RArray.rec_unsafe nil snoc t2)) : motive t)
  else
    (unsafeCast nil : motive t)

attribute [implemented_by RArray.nil_unsafe] RArray.nil
attribute [implemented_by RArray.snoc_unsafe] RArray.snoc
attribute [implemented_by RArray.rec_unsafe] RArray.rec

def RArray.sum : RArray Nat → Nat
  | .nil => 0
  | .snoc xs x => xs.sum + x

def RArray.map {α β} (f : α → β) : RArray α → RArray β
  | .nil => .nil
  | .snoc xs x => .snoc (xs.map f) (f x)

[Joachim Breitner]

Ah, I also have to override casesOn!

attribute [implemented_by RArray.casesOn_unsafe] RArray.casesOn

[Joachim Breitner]

So here is my attempt at defining a data type that looks like an inductive Snoc list (nice for proofs, nice for functional programming with pattern matching) but its implementation is backed by Array, and allows fast conversion to and from Array (hardly tested, though):

/-- A snoc list, inductive -- nice for proofs and funcitonal programming -/
inductive RArray (α : Type _) where
  | nil : RArray α
  | snoc : RArray α → α → RArray α

/- Some conversions -/

def RArray.toRevList {α} : RArray α → List α
  | .nil => []
  | .snoc xs x => x :: xs.toRevList

def RArray.toList {α} (xs : RArray α) : List α :=
  xs.toRevList.reverse

def RArray.toArray {α} (xs : RArray α) : Array α :=
  xs.toList.toArray

def RArray.fromRevList {α} : List α → RArray α
  | [] => .nil
  | .cons x xs => snoc (RArray.fromRevList xs) x

def RArray.fromList {α} (xs : List α) : RArray α :=
  RArray.fromRevList xs.reverse

def RArray.fromArray {α} (a : Array α) : RArray α :=
  .fromList a.toList

/- Some example functions -/

def RArray.sum : RArray Nat → Nat
  | .nil => 0
  | .snoc xs x => xs.sum + x

def RArray.map {α β} (f : α → β) : RArray α → RArray β
  | .nil => .nil
  | .snoc xs x => .snoc (xs.map f) (f x)

/- Replacement definitions for the fundamental constants of the type, backing the type with an
Array -/

unsafe def RArray.nil_unsafe {α} : RArray α :=
  unsafeCast (Array.empty : Array α)

unsafe def RArray.snoc_unsafe {α} : RArray α → α → RArray α :=
  unsafeCast (fun as a => as.push a : Array α → α → Array α)

unsafe def RArray.rec_unsafe.{u, u_1} {α : Type u_1} {motive : RArray α → Sort u} (nil : motive RArray.nil)
  (snoc : (a : RArray α) → (a_1 : α) → motive a → motive (RArray.snoc a a_1)) (t : RArray α) : motive t :=
  let t' := (unsafeCast t : Array α)
  if h : t'.size - 1 < t'.size then
    let x := t'[t'.size -1]
    let t2 := (unsafeCast t'.pop : RArray α)
    (unsafeCast (snoc t2 x (RArray.rec_unsafe nil snoc t2)) : motive t)
  else
    (unsafeCast nil : motive t)

unsafe def RArray.casesOn_unsafe.{u, u_1} {α : Type u_1} {motive : RArray α → Sort u} (t : RArray α)
  (nil : motive RArray.nil) (snoc : (a : RArray α) → (a_1 : α) → motive (RArray.snoc a a_1))
      : motive t :=
  let t' := (unsafeCast t : Array α)
  if h : t'.size - 1 < t'.size then
    let x := t'[t'.size -1]
    let t2 := (unsafeCast t'.pop : RArray α)
    (unsafeCast (snoc t2 x) : motive t)
  else
    (unsafeCast nil : motive t)

attribute [implemented_by RArray.nil_unsafe] RArray.nil
attribute [implemented_by RArray.snoc_unsafe] RArray.snoc
attribute [implemented_by RArray.rec_unsafe] RArray.rec
attribute [implemented_by RArray.casesOn_unsafe] RArray.casesOn

/- Faster conversion functions -/

unsafe def RArray.fromArray_unsafe {α} (a : Array α) : RArray α := unsafeCast a
attribute [implemented_by RArray.fromArray_unsafe] RArray.fromArray

unsafe def RArray.toArray_unsafe {α} (a : RArray α) : Array α := unsafeCast a
attribute [implemented_by RArray.toArray_unsafe] RArray.toArray

Of course, it’s quite scary how much unsafe there is in the code. I wonder if there could be a more principled approach to such data type refinements. Maybe what I am looking for is data type refinement like in Isabelle. Is that possible, or on the horizon?

[David Thrane Christiansen]

I've been thinking for some time that it might be useful to have first-class support for alternative recursors, a la Epigram. For instance, Lean's representation of Fin is non-bizarre - it's a Nat at runtime - but programming with it is manifestly less convenient than the inductive version. It would be great to be able to prove the inductive version's induction principle, and then use it with ordinary match expressions, whether by some kind of using modifier or by having Lean select the appropriate induction principle from the set of patterns employed.

This could be a nice hack for backwards compatibility too.

[Joachim Breitner]

That also sounds nice – then we could simply have a “snoc-view on Arrays” recursor directly, no separate type needed.

[Joachim Breitner]

How hard would alternative recursers be? The equation compiler would have to know which “constructors” belong to which recursor, at least in the simple case where each recursor has its own set of constructors used in patterns. Are other components involved?

[David Thrane Christiansen]

Not that I know of, but I'm not the one to ask

[Jun Yoshida]

I found a mysterious attribute recursor in the core. Although nothing uses it currently, was it created for this purpose?

[David Thrane Christiansen]

I'd expect a nice API to be something like:

def Fin.zero : Fin (n + 1) := ...
def Fin .succ : Fin n -> Fin (n + 1) := ...
def Fin.someOtherEliminator : {p : (n : Nat) -> Fin n -> Type u} -> ((n : Nat) -> p (n + 1) fzero) -> ...
register_matcher Fin.somOtherEliminator for Fin.zero, Fin.succ

where it would then create the corresponding casesOn and noConfusion stuff.

[Eric Wieser]

@Jun Yoshida: I think that attribute is used to override the recursion principle for induction and/or cases, but it doesn't work for match

[Jun Yoshida]

@Eric Wieser Regarding the current lean4, Std, and Mathlib repositories, I don't think any other functions use recursorAttribute, so it is not even an alternative of eliminator attribute; i.e. neither induction nor cases care recursor attribute.