CIP-0092? | First-class errors in Plutus

[L-as]

@michaelpj @effectfully

Rendered in branch

Initial discussion: #459 (comment)

[L-as]

Reply to #459 (comment) :

I hope the behaviour is more obvious given the explanation in this CIP?
The factorial implementation blows up because everything is still evaluated strictly.
The ifThenElse example doesn't because passing an error to it is entirely valid.

[L-as]

I realised another benefit: This allows optimising expensive1 || expensive2 into if expensive1 then True else expensive2, the reason being that the language is now truly pure (modulo traces, which we don't care about in optimisations).
This is evident by the fact that evaluating something doesn't matter wrt. transaction validity (modulo budgets, but optimisation already messes with that), so we can in fact in general entirely eliminate unused terms with this change.

We also fix the other issue I noted in IntersectMBO/plutus#4826, since const can now truly ignore the error!

This might be another (quite big?) reason to introduce this change to Plutus.

[effectfully]

@L-as

I hope the behaviour is more obvious given the explanation in this CIP?
The factorial implementation blows up because everything is still evaluated strictly.
The ifThenElse example doesn't because passing an error to it is entirely valid.

I understood the proposed behavior, but I was failing to understand the motivation for it. Now that I've read this CIP I do indeed understand the motivation, thanks a lot for writing it out.

I think I agree that doing what you suggest would be an improvement over the status quo. I wouldn't like the resulting system, but less so than the current one.

However to be completely frank, I believe chances of anybody being able to convince our academics to give up on canonicity and to convince our managers to overhaul the whole evaluation semantics of the language (i.e. the implementation, the spec and the formalization) are pretty slim. As such, I don't feel like it's a battle worth fighting. Plus, if we were to overhaul the whole evaluation semantics, I would prefer some other solution, perhaps something based on call-by-push-value. Or maybe even just making the language lazy.

Overall, I think that ship has sailed, unfortunately.

[L-as]

@effectfully

I believe chances of anybody being able to convince our academics to give up on canonicity

I don't see why it would be any different from the status quo wrt. canonicity.

I would prefer some other solution, perhaps something based on call-by-push-value. Or maybe even just making the language lazy.

I think we will likely find a better solution in the future, however, this is a very minor change that can be done without changing most of the ecosystem.

to overhaul the whole evaluation semantics of the language (i.e. the implementation, the spec and the formalization)

Well that's precisely what it isn't, I'd say! This is a minor change to the implementation, the spec, and the formalisation.

[mgajda]

Haskell and GHC had introduced pretty major overhaul to its errors and introduced more complex exceptions. So may there be a chance to do everything in a monad?

[L-as]

What do I need to do to get this in now with the new structure?

[rphair]

@L-as thanks for attending to this one. All changes below are to make the format & content consistent with newer CIPs (with 1 or 2 other suggestions beyond the formatting).

[rphair]

Suggested change

	- https://github.com/cardano-foundation/cips/pulls/?
	- https://github.com/cardano-foundation/CIPs/pull/469

[rphair]

(not a format correction, but an editorial question)

1. This is unclear whether these Plutus issues/PRs are closed to to this CIP method being followed (please confirm if so... I can't verify this from the issue/PR threads) or because their solutions share the premise of the CIP. Can you change "closed by this CIP" to a statement or paragraph that explains the relationship unambiguously?
2. Once we decide where this is going we can also link @nielstron about the stalled CIP-0091? | Don't force Built-In functions #459 to discuss whether candidate CIP-0091 should also be progressed (or deprecated).

[effectfully]

Once we decide where this is going we can also link @nielstron about the stalled #459 to discuss whether candidate CIP-0091 should also be progressed (or deprecated).

Michael proposed to merge it as Proposed and I don't see why we should do anything else to it. It seems reasonable, even though I highly doubt we're ever going to implement it, given that a very simple workaround exists.

[rphair]

@effectfully I think sinceif this is doable, but not likely to be done, it would make sense to put it through as Proposed after some cleanup from @L-as... rather than assign the currently not-yet-used Rejected status that e.g. Michael proposed for stalled candidate #336 (though a Rejected status could still be considered if everyone is in agreement about that).

[effectfully]

@rphair sorry, I was commenting about #459 specifically. If my suspicion regarding this CIP not being doable is confirmed (if!), then this CIP is a prime candidate for being rejected.

[rphair]

This list is too much detail for the Abstract and in fact is Motivation so should be moved down to that section.

[rphair]

Suggested change

	## Motivation
	## Motivation: why is this CIP necessary?

(standard as per CIP-0001)

[rphair]

Suggested change

	### Acceptance Criteria
	It would be needed to implement the necessary changes in `cardano-ledger` and `plutus`.
	### Implementation Plan
	### Acceptance Criteria
	It would be needed to implement the necessary changes in `cardano-ledger` and `plutus`.
	### Implementation Plan

We need more detail about how the both the Ledger & Plutus teams would be expected to verify this. I was hoping to use the similarly split #758 as an example, but that too has been stalled & is incomplete in that regard.

@zliu41 @lehins can you please provide some help about what exactly would be needed here for verification of this proposal?

[effectfully]

I've commented down below, I think this proposal can't work as written, so it can't be implemented and verified either. I may be wrong of course, so let's see what further discussion shows.

[rphair]

This is a proposed specification, so should be moved into that section (probably with a heading reinforcing your first statement that this method is hypothetical and/or illustrative).

[rphair]

Suggested change

	## Copyright
	[CC-BY-4.0]: https://creativecommons.org/licenses/by/4.0/legalcode
	[Apache-2.0]: http://www.apache.org/licenses/LICENSE-2.0
	## Copyright
	This CIP is licensed under [CC-BY-4.0].
	[CC-BY-4.0]: https://creativecommons.org/licenses/by/4.0/legalcode
	[Apache-2.0]: http://www.apache.org/licenses/LICENSE-2.0

we do need to choose one of these to display in the markup: I'm going to not suggest Apache since the code herein isn't intended for reuse.

[effectfully]

I wrote this last year:

I understood the proposed behavior, but I was failing to understand the motivation for it. Now that I've read this CIP I do indeed understand the motivation, thanks a lot for writing it out.

I wish I spelled out what convinced me, because rereading the CIP I'm not convinced that it would be worth doing that even given infinite resources for development. I was probably just sloppy last year.

One of the proposed changes is this:

Erase type abstractions and type applications entirely when going from TPLC to UPLC rather than turning them into delay and force.

But that just can't work. Take the following TPLC expression:

let factorial n = ifThenElse {forall a. integer} (\{_} -> n == 0) 1 (\{_} -> factorial (n - 1)) {()}
in factorial 2

If we erase all type abstractions and type applications from it while going from TPLC to UPLC, we'll get

let factorial n = ifThenElse (n == 0) 1 (factorial (n - 1))
in factorial 2

which is an infinite loop as the proposal acknowledges, unlike the original expression.

The proposal says

Very few people will make their own loopforever function to replicate the old error to write impure scripts.

but if you start erasing type abstractions and type applications left and right you'll get those loopforever functions all over the place without bothering to put them into the program manually.

@L-as

I don't see why it would be any different from the status quo wrt. canonicity.

You're proposing to add an axiom that every type is inhabited by the special ERROR construct, it's a textbook example of how to break canonicity, see e.g. this.

Can we have a formal model where that rule isn't an axiom, but rather an inherent part of the system, like "every type has an ERROR constructor, including even ->" and then elaborate TPLC/UPLC into that system? Maybe, but I doubt anybody is going to do it. It's a major change to the semantics of our languages. And having implemented and recently refactored the way we do error handling in the UPLC evaluator, I can assure you it's plenty of work, so I very much disagree with this:

Well that's precisely what it isn't, I'd say! This is a minor change to the implementation, the spec, and the formalisation.

If you believe it's a minor change anyway, we'd appreciate a branch implementing the proposed changes to handling of ERROR. We'll implement erasure of forces and delays ourselves just to meet you halfway.

[L-as]

Thanks, that’s a very concrete path forward. Maybe I’ll look at it when I have time.

[rphair]

@L-as the last comment (after a pessimistic review + a still-unaddressed request to update to the canonical document structure), now that a couple more months have gone by, suggests that you don't have the time to pursue this.

Ordinarily we would close it when an author doesn't have time to complete a CIP but I don't want to bury the work you & @effectfully have done to document this issue... so in the meantime I'm tagging this Abandoned which will close it later... if & when editors don't see any progress as apparently agreed after #469 (comment).

[L-as]

Thank you. I wouldn't necessarily say this will never happen, you should have a long-term view. I'm busy right now with some other open source stuff but when I have that done it's possible I will do this.

[L-as]

Rip