Work around for "Code generator support for recursors"

Stream: general

[Ash]

I have been trying to work my way up to implementing "Generic Programming with Indexed Functors" by Andres Löh in Lean. I have a prototype that type checks and can represent List types.

Here is a minimal example:

namespace Ex

-- a "type code" data structure
-- inhabitants of `Poly` themselves represent / are interpreted as a type,
-- and that type is inhabited by `PolyExt`s
inductive Poly : (I J : Type u) → Type (u+1) where
| PSEmpty : Poly I J
| PSUnit : Poly I J
| PSI (i : I) : Poly I J
| PSSum (l r : Poly I J) : Poly I J
| PSProd (l r : Poly I J) : Poly I J
| PSFix : Poly (I ⊕ J) J → Poly I J

-- helper functions for `PolyExt`'s constructor `.PEMu`
abbrev polyLiftSum : Poly I J → Poly (I ⊕ J) J
| .PSUnit => .PSUnit
| .PSSum l r => .PSSum (polyLiftSum l) (polyLiftSum r)
| .PSProd l r => .PSProd (polyLiftSum l) (polyLiftSum r)
| .PSFix a => .PSFix (polyLiftSum a)
| .PSEmpty => .PSEmpty
| .PSI i => .PSI (.inl i)

abbrev partialApp {I J : Type u} : Poly (I ⊕ J) J → Poly I J → Poly I J
| .PSUnit, _ => .PSUnit
| .PSSum l r, x => .PSSum (partialApp l x) (partialApp r x)
| .PSProd l r, x => .PSProd (partialApp l x) (partialApp r x)
| .PSFix a, x => .PSFix (partialApp a (polyLiftSum x))
| .PSI (.inl i), _ => .PSI i
| .PSI (.inr _), x => x
| .PSEmpty, _ => .PSEmpty

-- represents a term that inhabits a type specified by a `Poly` type code
-- parameterized by `f`, a family indexed by `I`.
inductive PolyExt : {I J : Type u} → (f : I → Type _) → Poly I J → Type (u+1) where
| PEUnit : PolyExt f .PSUnit
| PEI {f : I → Type _} (x : f i) : @PolyExt I J f (.PSI i)
| PESumL (a : PolyExt f l) : PolyExt f (.PSSum l r)
| PESumR (b : PolyExt f r) : PolyExt f (.PSSum l r)
| PEProd : PolyExt f l → PolyExt f r → PolyExt f (.PSProd l r)
| PEMu : PolyExt f (partialApp P (.PSFix P)) → PolyExt f (.PSFix P)

abbrev ListF : Poly (Unit ⊕ Unit) Unit := .PSSum .PSUnit (.PSProd (.PSI (.inl .unit)) (.PSI (.inr .unit)))
abbrev List : Poly Unit Unit := .PSFix ListF

abbrev nil {A : Type _} : PolyExt (λ _ => A) List :=
  .PEMu (.PESumL .PEUnit)

abbrev ex {A : Type _} : PolyExt (λ _ => A) List :=
  .PEMu (
    by
      simp[partialApp, polyLiftSum, WellFounded.fix, WellFounded.fixF, InvImage, WellFoundedRelation.rel, Acc.rec]
      -- a lot of unanticipated terms here - what is going on? desugaring?
      sorry
      )

abbrev cons {A : Type _} (x : A) (t : PolyExt (λ _ => A) List) : PolyExt (λ _ => A) List :=
  .PEMu (.PESumR (.PEProd (.PEI x) t))

abbrev ex_2_1_nil :=
  cons 2 (cons 1 nil)

end Ex

Unfortunately, I'm getting the following error for the cons and nil definitions: (Lean v4.22)

code generator does not support recursor 'Acc.rec' yet, consider using 'match ... with' and/or structural recursion

I'm not sure how to triage this. My hypothesis is that during elaboration, Acc and WellFounded are introduced through desugaring - though I do not know why codegen doesn't support it. Issue #2049 appears to be related, but I don't know how to work around it. Could someone help point me in the right direction?

[Aaron Liu]

the problem is partialApp which is using well-founded recursion

[Ash]

Aaron Liu said:

the problem is partialApp which is using well-founded recursion

Could you elaborate? My understanding is that something like Coq's Program Fixpoint could be going on, where a well founded relation is added under the hood to show termination. It's not very obvious to me how that is occurring here.

[Aaron Liu]

also why did you make them abbrevs

[Aaron Liu]

Ash said:

Aaron Liu said:

the problem is partialApp which is using well-founded recursion

Could you elaborate? My understanding is that something like Coq's Program Fixpoint could be going on, where a well founded relation is added under the hood to show termination. It's not very obvious to me how that is occurring here.

The termination checker infers a sizeOf function and pulls back the well-foundedness of < from Nat

[Aaron Liu]

May I ask what's up with the I ⊕ J? Why do you need I ⊕ J?

[Ash]

Aaron Liu said:

May I ask what's up with the I ⊕ J? Why do you need I ⊕ J?

I'm not sure if I can do the best job explaining it. But the idea is that you could tie a knot similarly to how you would do with ListF and Fix in Haskell.
https://www.cambridge.org/core/journals/journal-of-functional-programming/article/indexed-containers/FB9C7DC88A65E7529D39554379D9765F
This paper describes how there is both an input and output type index for indexed containers, and indexed containers are sort of the more general form of what I'm trying to accomplish, and what is happening in the GPIF paper.
The idea is that the "J" in the "I ⊕ J" gets replaced with recursive positions when you tie the recursive knot.

The code is sort of a prototype right now, so I'm not doing anything really with the 2nd type index J.

[Aaron Liu]

Is there any other design you can use which puts a free variable in that position instead of I ⊕ J? It's causing

cannot use specified measure for structural recursion:
  its type Ex.Poly is an inductive family and indices are not variables
    Poly (I ⊕ J) J

[Ash]

Aaron Liu said:

The termination checker infers a sizeOf function and pulls back the well-foundedness of < from Nat

Thanks, how were you able to deduce that? Does lean do this for all recursive functions?

[Henrik Böving]

The code generator is perfectly capable (or at least, supposed to be, looking at this) of handling situations where Acc.rec was used due to a particular termination proof, the only situation in which it should error out is when the user purposefully introduced Acc.rec themselves. I'd say that the fact that Acc.rec occurs in the input to the code generator is instead likely a bug.

[Ash]

Aaron Liu said:

Is there any other design you can use which puts a free variable in that position instead of I ⊕ J? It's causing

cannot use specified measure for structural recursion:
  its type Ex.Poly is an inductive family and indices are not variables
    Poly (I ⊕ J) J

I'd have to put more thought into it. How are you getting this error message?

[Aaron Liu]

Ash said:

Aaron Liu said:

The termination checker infers a sizeOf function and pulls back the well-foundedness of < from Nat

Thanks, how were you able to deduce that? Does lean do this for all recursive functions?

Lean does this for most functions which are done by well-founded recursion (so not for structural recursion)

[Aaron Liu]

Ash said:

Aaron Liu said:

Is there any other design you can use which puts a free variable in that position instead of I ⊕ J? It's causing

cannot use specified measure for structural recursion:
  its type Ex.Poly is an inductive family and indices are not variables
    Poly (I ⊕ J) J

I'd have to put more thought into it. How are you getting this error message?

I went to partialApp and put termination_by structural x y => x below

[Aaron Liu]

another option would be to make the I and J indicies in Poly into parameters

[Ash]

Aaron Liu said:

another option would be to make the I and J indicies in Poly into parameters

This will break PSFix constructor unfortunately

[Aaron Liu]

yes but that constructor is evil

[Ash]

GPIF's formulation in Agda is slightly different, but their definition I believe uses induction-recursion, so I can't directly translate it to lean.

[Ash]

Thank you for your help, I'll have to mull this over some more

[Ash]

I've found a workaround for now, it turns out that I can avoid the Acc.rec making its way to the codegen by making partialApp a def instead of an abbrev or @[reducible] def.

This is less than ideal, since now I have to use tactic mode and apply simp [partialApp] to get the type checker to be happy, but now I don't run into the same codegen issue.

Here's the full thing with the only changes being partialApp is now a def, and nil and cons definitions must now use tactic mode and apply simp [partialApp].

namespace Ex

-- a "type code" data structure
-- inhabitants of `Poly` themselves represent / are interpreted as a type,
-- and that type is inhabited by `PolyExt`s
inductive Poly : (I J : Type u) → Type (u+1) where
| PSEmpty : Poly I J
| PSUnit : Poly I J
| PSI (i : I) : Poly I J
| PSSum (l r : Poly I J) : Poly I J
| PSProd (l r : Poly I J) : Poly I J
| PSFix : Poly (I ⊕ J) J → Poly I J

-- helper functions for `PolyExt`'s constructor `.PEMu`
abbrev polyLiftSum : Poly I J → Poly (I ⊕ J) J
| .PSUnit => .PSUnit
| .PSSum l r => .PSSum (polyLiftSum l) (polyLiftSum r)
| .PSProd l r => .PSProd (polyLiftSum l) (polyLiftSum r)
| .PSFix a => .PSFix (polyLiftSum a)
| .PSEmpty => .PSEmpty
| .PSI i => .PSI (.inl i)

-- `abbrev` changed to `def` - note: `@[reducible]` encounters same issues as `abbrev`
def partialApp {I J : Type u} : Poly (I ⊕ J) J → Poly I J → Poly I J
| .PSUnit, _ => .PSUnit
| .PSSum l r, x => .PSSum (partialApp l x) (partialApp r x)
| .PSProd l r, x => .PSProd (partialApp l x) (partialApp r x)
| .PSFix a, x => .PSFix (partialApp a (polyLiftSum x))
| .PSI (.inl i), _ => .PSI i
| .PSI (.inr _), x => x
| .PSEmpty, _ => .PSEmpty

-- represents a term that inhabits a type specified by a `Poly` type code
-- parameterized by `f`, a family indexed by `I`.
inductive PolyExt : {I J : Type u} → (f : I → Type _) → Poly I J → Type (u+1) where
| PEUnit : PolyExt f .PSUnit
| PEI {f : I → Type _} (x : f i) : @PolyExt I J f (.PSI i)
| PESumL (a : PolyExt f l) : PolyExt f (.PSSum l r)
| PESumR (b : PolyExt f r) : PolyExt f (.PSSum l r)
| PEProd : PolyExt f l → PolyExt f r → PolyExt f (.PSProd l r)
| PEMu : PolyExt f (partialApp P (.PSFix P)) → PolyExt f (.PSFix P)

abbrev ListF : Poly (Unit ⊕ Unit) Unit := .PSSum .PSUnit (.PSProd (.PSI (.inl .unit)) (.PSI (.inr .unit)))
abbrev List : Poly Unit Unit := .PSFix ListF

abbrev nil {A : Type _} : PolyExt (λ _ => A) List :=
  .PEMu (by simp[partialApp]; apply (PolyExt.PESumL .PEUnit))

abbrev cons {A : Type _} (x : A) (t : PolyExt (λ _ => A) List) : PolyExt (λ _ => A) List :=
  .PEMu (by simp[partialApp]; apply (PolyExt.PESumR (.PEProd (.PEI x) t)))

abbrev ex_2_1_nil :=
  cons 2 (cons 1 nil)

end Ex

Two questions:

• Is there an alternative to the by simp [partialApp]; ... syntax to get the function to unfold here, while still having partialApp be a def?
• @Henrik Böving, does this help narrow it down enough that I could possibly file an issue about Acc.rec making its way into the codegen?

Thanks

[Henrik Böving]

You should've already felt free to open a bug without providing a workaround^^ So sure go ahead!