Recursive functions, algebraically---improvements & changes

[ahubers]

Reviews: https://github.com/IaFP/Rome-paper/tree/main/POPL25.

Changes recommended by the reviewers, explicitly

...

Changes recommended by the reviewers, implicitly

...

Changes that strengthen our case

• An operational semantics.
• Restore strong normalization: remove fix term and use combinators. N.b. Even with these changes, your semantics will remain partial because of Agda's positivity checker. I see the type-level potatoes as a necessity to bypass positivity checking, and hence the semantics is partial. (Even with partiality/delay monads, this doesn't change.) What you could do is change your return type from Maybe to an existential on bound: there exists a gas level such that this function produces a type/term. But this sounds like sized types, to be honest.