leanprover
RFC: new versus old code generator issue
Since nightly-2025-06-21 the file CoreM.lean changed line 670 to defValue := true.
The new code generator does not want to generate code any more for the some of my code.
I am referring to https://github.com/LucDuponcheelAtGitHub/PSBP
Agreed, I am using the unsafe keyword because the type system cannot infer termination.
The mwe code below contains sequentialFibonacci and parallelFibonacci.
Both are written in terms of declarations. Their materializations
(according to implementations that define the declarations) come later.
sequentialFibonacci is not impacted, but parallelFibonacci is impacted.
Therefore I guess that the difference is, somehow, related to Task.
Here are some possibilities to solve this
- have two releases : one with the old code generator one with the new code generator (this does not look to me like the right way to proceed)
- somehow provide a compiler/interpreter option to choose between the old one and the new one (also sub-optimal, but workable for me)
- look into the issue and find out where and why the new one does not want to generate code
All comments are welcome
class Functional
(program : Type → Type → Type) where
asProgram {α β : Type} :
(α → β) → program α β
export Functional (asProgram)
class Functorial
(program : Type → Type → Type) where
andThenF {α β γ : Type} :
program α β → (β → γ) → program α γ
export Functorial (andThenF)
infixl:50 " >-> " => andThenF
class Sequential
(program : Type → Type → Type) where
andThenP {α β γ : Type} :
program α β → program β γ → program α γ
export Sequential (andThenP)
infixl:50 " >=> " => andThenP
class Creational
(program : Type → Type → Type) where
sequentialProduct {α β γ : Type} :
program α β → program α γ → program α (β × γ)
export Creational (sequentialProduct)
infixl:60 " &&& " => sequentialProduct
class Conditional
(program : Type → Type → Type) where
sum {α β γ : Type} :
program γ α → program β α → program (γ ⊕ β) α
export Conditional (sum)
infixl:55 " ||| " => sum
class Parallel (program : Type → Type → Type) where
parallel {α β γ δ : Type} :
program α γ → program β δ → program (α × β) (γ × δ)
export Parallel (parallel)
infixl:60 " |&| " => parallel
def identity
[Functional program] :
program α α :=
asProgram λ α => α
def let_
[Functional program]
[Sequential program]
[Creational program] :
program α β → program (α × β) γ → program α γ :=
λ αpβ αaβpγ => identity &&& αpβ >=> αaβpγ
def if_
[Functional program]
[Sequential program]
[Creational program]
[Conditional program] :
program α Bool →
program α β →
program α β →
program α β :=
λ αpb t_apβ f_apβ =>
let_ αpb $
asProgram (
λ αab => match αab with
| ⟨α, true⟩ => .inl α
| ⟨α, false⟩ => .inr α
) >=>
t_apβ ||| f_apβ
def dup
[Functional program] :
program α (α × α) :=
asProgram λ α => (α, α)
def parallelProduct {α β γ : Type}
[Functional program]
[Sequential program]
[Parallel program] :
program α β → program α γ → program α (β × γ) :=
λ αpβ αpγ => dup >=> αpβ |&| αpγ
infixl:60 " &|& " => parallelProduct
def isZeroF: Nat → Bool := (. == 0)
def isOneF : Nat → Bool := (. == 1)
def oneF : Nat → Nat := λ _ => 1
def minusOneF : Nat → Nat := λ n => n - 1
def minusTwoF : Nat → Nat := λ n => n - 2
def addF : Nat × Nat → Nat :=
λ ⟨n, m⟩ => n + m
def multiplyF : Nat × Nat → Nat := λ ⟨n, m⟩ => n * m
def isZero
[Functional program] :
program Nat Bool :=
asProgram isZeroF
def isOne
[Functional program] :
program Nat Bool :=
asProgram isOneF
def one
[Functional program] :
program Nat Nat :=
asProgram oneF
def minusOne
[Functional program] :
program Nat Nat :=
asProgram minusOneF
def minusTwo
[Functional program] :
program Nat Nat :=
asProgram minusTwoF
def add
[Functional program] :
program (Nat × Nat) Nat :=
asProgram addF
unsafe def sequentialFibonacci
[Functional program]
[Sequential program]
[Creational program]
[Conditional program] :
program Nat Nat :=
if_ isZero one $
if_ isOne one $
(minusOne >=> sequentialFibonacci) &&&
(minusTwo >=> sequentialFibonacci) >=>
add
unsafe def parallelFibonacci
[Functional program]
[Sequential program]
[Creational program]
[Conditional program]
[Parallel program] :
program Nat Nat :=
if_ isZero one $
if_ isOne one $
(minusOne >=> parallelFibonacci) &|&
(minusTwo >=> parallelFibonacci) >=>
add
structure FromComputationValuedFunction
(computation : (Type → Type)) (α β : Type) where
toComputationValuedFunction : α → computation β
instance [Applicative computation] :
Functional
(FromComputationValuedFunction computation) where
asProgram :=
λ αfβ => ⟨λ α => pure $ αfβ α⟩
instance [Functor computation] :
Functorial
(FromComputationValuedFunction computation) where
andThenF :=
λ ⟨αfcβ⟩ βfγ => ⟨λ α => βfγ <$> αfcβ α⟩
instance [Applicative computation] :
Creational
(FromComputationValuedFunction computation) where
sequentialProduct :=
λ ⟨αfcβ⟩ ⟨αfcγ⟩ =>
⟨λ α => .mk <$> αfcβ α <*> αfcγ α⟩
instance [Monad computation] :
Sequential
(FromComputationValuedFunction computation) where
andThenP :=
λ ⟨αfcβ⟩ ⟨βfcγ⟩ =>
⟨λ α => αfcβ α >>= βfcγ⟩
def foldSum {γ β α : Type}
(γfα : γ → α)
(βfα : β → α)
(sum : γ ⊕ β) : α :=
match sum with
| .inl tc => γfα tc
| .inr tb => βfα tb
instance :
Conditional
(FromComputationValuedFunction computation) where
sum :=
λ ⟨γfγα⟩ ⟨βfγα⟩ =>
⟨foldSum γfγα βfγα⟩
class MonadAsync
(computation : Type → Type) where
async {α : Type} (ufα : Unit → α) : computation α
result {α : Type} (cα : computation α) : α
export MonadAsync (async result)
abbrev Sync := Id
abbrev SyncProgram := FromComputationValuedFunction Sync
def materializeSync : SyncProgram α β → (α → β) :=
λ ⟨αfaβ⟩ α => αfaβ α
abbrev Async := Task
instance : Monad Async where
pure := Task.pure
bind := Task.bind
instance : MonadAsync Async where
async := Task.spawn
result := λ tα => tα.get
abbrev AsyncProgram :=
FromComputationValuedFunction Async
def materializeAsync {α β : Type} :
AsyncProgram α β → (α → β) :=
λ ⟨αftβ⟩ α => (αftβ α).get
def combine
{γ δ : Type}
[Applicative computation] :
computation γ → computation δ → computation (γ × δ) :=
λ cγ cδ => Prod.mk <$> cγ <*> cδ
infixl:50 " <×> " => combine
instance
[Monad computation]
[MonadAsync computation] :
Parallel (FromComputationValuedFunction computation) where
parallel := λ ⟨αfcγ⟩ ⟨βfcδ⟩ =>
⟨λ ⟨α, β⟩ =>
async (λ (_: Unit) => αfcγ α) >>=
λ cγ =>
async (λ (_: Unit) => βfcδ β) >>=
λ cδ =>
cγ <×> cδ⟩
unsafe def syncFibonacci :=
materializeSync sequentialFibonacci
unsafe def asyncFibonacci :=
materializeAsync parallelFibonacci
#eval syncFibonacci 10
-- #eval asyncFibonacci 10
The issue seems pretty obvious:
def parallelFibonacci._at_.asyncFibonacci.spec_0 : obj :=
let x_1 : obj := isZero._at_.parallelFibonacci._at_.asyncFibonacci.spec_0.spec_0;
let x_2 : obj := one._at_.parallelFibonacci._at_.asyncFibonacci.spec_0.spec_1;
let x_3 : obj := isOne._at_.parallelFibonacci._at_.asyncFibonacci.spec_0.spec_2;
let x_4 : obj := parallelFibonacci._at_.asyncFibonacci.spec_0;
inc x_4;
let x_5 : obj := pap parallelFibonacci._at_.asyncFibonacci.spec_0._lam_0 x_4;
let x_6 : obj := pap parallelFibonacci._at_.asyncFibonacci.spec_0._lam_1 x_4;
let x_7 : obj := add._at_.parallelFibonacci._at_.asyncFibonacci.spec_0.spec_8;
let x_8 : obj := pap parallelFibonacci._at_.asyncFibonacci.spec_0._lam_2 x_5 x_6 x_7;
inc x_2;
let x_9 : obj := if_._at_.parallelFibonacci._at_.asyncFibonacci.spec_0.spec_9._redArg x_3 x_2 x_8;
let x_10 : obj := if_._at_.parallelFibonacci._at_.asyncFibonacci.spec_0.spec_9._redArg x_1 x_2 x_9;
ret x_10
The type of the specialization becomes a function type here but the compiler doesn't introduce the variable so we get infinite recursion. Something similar happens to syncFibonacci although the compiler can avoid it slightly by needing to create a lambda sooner (Task.bind adds indirection that allows it to delay creating lambdas).
cc @zwarich
Hello Rob23oba and zwarich,
So what's the conclusion?
Changing the code of Task.bind so that it does not allow delaying creating lambdas)?
How did it work before the nightly-2025-06-21 build?
Maybe, Task should be considered to only be an Applicative rather than a Monad.
I mean, it suffices to have a Task.seq instead of a Task.bind.
After all, when spawning two tasks, it is only necessary to combine them using
a function of type Task α × Task β → Task (α × β) which Task.seq and Task.map can do together
as below (assuming appropriate Functor and Applicative instances are defined for Task)
def combine
{α β : Type}
[Applicative c] :
c α → c β → c (α × β) :=
λ cα cβ => Prod.mk <$> cα <*> cβ
.. just my 2 cents ...
Hello Rob23oba and zwarich,
Maybe I exaggerated a bit by writing that only a Task.seq is needed in general.
For my specific use case, parallel program combination, Task.seq suffices.
Actually, that might not be quite the problem, since FromComputationValuedFunction isn't quite a function type. If you define
def FromComputationValuedFunction
(computation : Type → Type) (α β : Type) :=
α → computation β
instead, then everything works fine. I'll let @zwarich see then how this differs to what the old compiler did and whether we consider this a regression.
Rob23oba, great, using your suggestion
it works with leanprover/lean4:nightly-2025-06-20 and
leanprover/lean4:nightly-2025-06-21 but not withleanprover/lean4:nightly-2025-06-22 ... (???) ...
Hello Rob23oba and zwarich,
good news, using abbrev (to really be sure that we are dealing with a function) as in
abbrev computationValuedFunction
(computation : Type → Type) (α β : Type) :=
α → computation β
the example seems to work with leanprover/lean4:stable.
So, maybe, the issue can be closed.
Thanks so much guys !!!
FYI: try #eval asyncFibonacci 24 and you'll see (e.g. using htop that Lean keeps all cores busy)
I'm not quite sure about using abbrev here, that might cause problems later. There shouldn't be any difference between def and abbrev for the compiler here though; for me it seems to work with def on leanprover/lean4:v4.23.0.
Rob23oba, I tried def with the stable version myself and it worked!
thx!!
Why would abbrev cause problems later?
abbrev simply defines computationValuedFunction computation α β as a synonym of α → computation β, or am I missing something here?
The problem is that when we turn computationValuedFunction computation α β into α → computation β it doesn't look like program x y anymore so there might be some problems with unification.
fair enough
I am busy now converting the code of my PSBP library
https://github.com/LucDuponcheelAtGitHub.
the impact on the MWE was minimal,
but PSBP (which can be seen as a programming course for Lean itself)
also has theorems (many using simp but also many using calc that need to be adapted)
anyway: YOU ARE MY HERO !!
Updating may code base (almost mechanically) results in type ambiguity errors like
Ambiguous term
αpγ >=> γpδ
Possible interpretations:
αpγ >=> γpδ : computationValuedFunction computation α δ
αpγ >=> γpδ : α → computation δ
Well, yes, those types are essentially the same now.
Lean seems to have problems with the def change (also with the abbrev one for that matter)
which Lean did not have with my structure approach (kind of putting the function in a box).
So the question remains:
how did the parallel Task based version worked before nightly-2025-06-21
end not after, while the sequential kept on working? Maybe there was an essential
different design choice (maybe for a good reason). And, maybe, also approaching
Task the Applicative way may be compatible with that reason while keeping the
parallel Task based fibonacci working.
just my 2 cents
Oh, this is because >=> already exists as notation for Bind.kleisliLeft as an infixr:55. Similarly, &&& is infixl:60 for bitwise and, ||| is infixl:55 for bitwise or, <&> is infixr:100 for Functor.mapRev and * is infixl:70 for multiplication. If you don't care about those operations, you can:
- Disable and override (allows for different precedence):
macro_rules | `($_ >=> $_) => Lean.Macro.throwError "disabled" infixl:55 " >=> " => andThenP - Override semantics (keeps precedence though):
macro_rules | `($a >=> $b) => `(andThenP $a $b)
Since &&& and ||| are most likely not ambiguous in your case (e.g. bitwise and probably won't work when productSeq does), you don't need to care about them. But >=> and <&> have potential for collision so you should probably disable+override them (Ideally put namespace PBSP at the top of every file after the imports and use scoped macro_rules and scoped infixl to make sure anyone using your library can decide not to use those overrides). I'm not sure about multiplication, maybe use a different symbol?
Rob23oba, I am going to present a new MWE asap where the type issues occur (but there are only 24 hours in a day). I will try to solve the issues myself (using your suggestions), but I am not sure if I fully know where to put what in the code. Anyway, you may wish to help me once I have presented the new MWE. Thanks in advance.
Rob23oba, as far as trying to produce a MWE, your
macro_rules
| `($_ >=> $_) => Lean.Macro.throwError "disabled"
infixl:55 " >=> " => andThenP
suggestion solved the issue.
Let's hope for the best for the rest of my code.
Rob23oba,
my whole codebase has been refactored, using your suggestion
macro_rules
| `($_ >=> $_) => Lean.Macro.throwError "disabled"
thx
now I need to sync the documentation
Frankly, without your help I would not have been able to solve the issue in 1000 years.
I had never heard of those macro_rules.
I know that macro programming is possible in Lean but there it stops.