[Refactoring] Remove prismatic error handling from Ck/Cek machines #7116
Conversation
SeungheonOh
force-pushed
the
seungheonoh/6160-evaluation
branch
from
578a6b5 to
d8e4539
Compare
SeungheonOh
changed the title
SeungheonOh
added
Refactoring
No Changelog Required
|
/benchmark validation |
|
Click here to check the status of your benchmark. |
|
Comparing benchmark results of 'validation' on 'f17c02cb9' (base) and 'd8e453994' (PR) Results table
|
SeungheonOh
force-pushed
the
seungheonoh/6160-evaluation
branch
from
d8e4539 to
d22e54a
Compare
SeungheonOh
force-pushed
the
seungheonoh/6160-evaluation
branch
from
d22e54a to
ab0ef1b
Compare
SeungheonOh
force-pushed
the
seungheonoh/6160-evaluation
branch
from
ab0ef1b to
65b1759
Compare
|
/benchmark nofib |
|
Click here to check the status of your benchmark. |
|
Comparing benchmark results of 'validation' on 'f17c02cb9' (base) and '65b17597f' (PR) Results table
|
|
Click here to check the status of your benchmark. |
|
I think this is in reasonable margins of error. |
|
Comparing benchmark results of 'nofib' on 'f17c02cb9' (base) and '65b17597f' (PR) Results table
|
| @@ -199,7 +198,7 @@ instance tyname ~ TyName => KnownTypeAst tyname DefaultUni Void where | |||
| instance UniOf term ~ DefaultUni => MakeKnownIn DefaultUni term Void where | |||
| makeKnown = absurd | |||
| instance UniOf term ~ DefaultUni => ReadKnownIn DefaultUni term Void where | |||
| readKnown _ = throwing _StructuralUnliftingError "Can't unlift to 'Void'" | |||
| readKnown _ = throwStructuralUnliftingError "Can't unlift to 'Void'" | |||
There was a problem hiding this comment.
I'd decouple error construction from throwing:
| readKnown _ = throwStructuralUnliftingError "Can't unlift to 'Void'" | |
| readKnown _ = throwError $ structuralUnliftingError "Can't unlift to 'Void'" |
| -- | Same as 'readKnown', but the cause of a potential failure is the provided term itself. | ||
| readKnownSelf | ||
| :: (ReadKnown val a, AsUnliftingEvaluationError err, AsEvaluationFailure err) | ||
| => val -> Either (ErrorWithCause err val) a | ||
| readKnownSelf val = fromRightM (throwBuiltinErrorWithCause val) $ readKnown val | ||
| {-# INLINE readKnownSelf #-} | ||
|
|
There was a problem hiding this comment.
Is this change related to the task or is it an opportunistic improvement?
There was a problem hiding this comment.
It's not possible to define this function without prismatic error type constraint unless I have a copy of this function per error type.
Instead, I removed this function entirely and handled error when readKnown is used where error type is actually realized
There was a problem hiding this comment.
Gotcha! Thanks for the clarification.
| @@ -401,7 +401,7 @@ instance (KnownBuiltinTypeIn DefaultUni term Integer, Integral a, Bounded a, Typ | |||
| -- TODO: benchmark an alternative 'integerToIntMaybe', modified from @ghc-bignum@ | |||
| if fromIntegral (minBound :: a) <= i && i <= fromIntegral (maxBound :: a) | |||
| then pure . AsInteger $ fromIntegral i | |||
| else throwing _OperationalUnliftingError . MkUnliftingError $ fold | |||
| else throwOperationalUnliftingError . MkUnliftingError $ fold | |||
There was a problem hiding this comment.
| else throwOperationalUnliftingError . MkUnliftingError $ fold | |
| else throwError . mkUnliftingError $ fold |
(Don't apply, this is an example of idea)
There was a problem hiding this comment.
It would be throwError . operationalUnliftingError . mkUnliftingError but I get the idea
There was a problem hiding this comment.
What sticks into my eye is the repetion of UnliftingError in operationalUnliftingError . mkUnliftingError.
Given 2 facts:
operationalUnliftingErroris alreadyUnliftingError-aware.- There is only one constructor to create an unlifting error:
MkUnliftingError.
I infer that operationalUnliftingError couldn't be composed with anything other than the one and only MkUnliftingError.
It seems to make sense to squash operationalUnliftingError . mkUnliftingError into
mkOperationalUnliftingError as a first step once (freeing users from doing it over and over again), and then realising that UnliftingError is always operational and this knowledge doesn't need to be repeated per-usage, it could be simplified even further down to mkUnliftingError (but with a composed type), wdyt?
Alternatively,
how about more radical naming throwError . operational . unlifting ? Reads very nice in context.
There was a problem hiding this comment.
Ah, yes UnliftingError ~ Text anyways, and on other cases we were just relying on IsString UnliftingError anyways. Making operationalUnliftingError :: Text -> BuiltinError would be most reasonable; I agree.
| :: Maybe (Term TyName Name uni fun ()) | ||
| -> BuiltinError | ||
| -> CkEvaluationException uni fun | ||
| builtinErrorToCkEvaluationException cause = |
There was a problem hiding this comment.
Observation: you're not factoring in throwing an exception here (which arguably makes more sense for exception than for errors!)
There was a problem hiding this comment.
I intentionally prevented myself from making any semantic changes on error types.
There was a problem hiding this comment.
I didn't mean to change the CkEvaluationException type (I could have, but that wasn't my point).
I meant this direction of change builtinErrorToCkEvaluationException -> throwBuiltinErrorToCkEvaluationException.
The PR doesn't follow this path consistently.
plutus-core/untyped-plutus-core/src/UntypedPlutusCore/Evaluation/Machine/Cek/Internal.hs
Outdated
Show resolved
Hide resolved
There was a problem hiding this comment.
Thanks for demonstrating that prisms boilerplate could be simplified away without remorse!
My main concern is about decoupling error construction from error throwing:
I much prefer a set of "lifting" constructors that don't throw, e.g. throwError . fooBarBazError instead of throwFooBarBazError as its more compositional without much syntactic difference.
SeungheonOh
force-pushed
the
seungheonoh/6160-evaluation
branch
from
65b1759 to
dddf411
Compare
SeungheonOh
force-pushed
the
seungheonoh/6160-evaluation
branch
from
dddf411 to
57ceadc
Compare
SeungheonOh
force-pushed
the
seungheonoh/6160-evaluation
branch
from
57ceadc to
2652bf4
Compare
plutus-core/plutus-core/src/PlutusCore/Evaluation/Machine/Exception.hs
Outdated
Show resolved
Hide resolved
| ErrorWithCause | ||
| (bimap UnliftingMachineError (const CekEvaluationFailure) $ unUnliftingEvaluationError err) | ||
| cause | ||
| BuiltinEvaluationFailure -> ErrorWithCause (OperationalError CekEvaluationFailure) cause |
There was a problem hiding this comment.
Ok, if we refactor it slightly, we'll get
builtinErrorToCekEvaluationException cause = flip ErrorWithCause cause . \case
BuiltinUnliftingEvaluationError err ->
bimap UnliftingMachineError (const CekEvaluationFailure) $ unUnliftingEvaluationError err
BuiltinEvaluationFailure -> OperationalError CekEvaluationFailureat which point we see that there's a conversion between BuiltinError and EvaluationError structural operational for certain structural and operational.
So could you please turn that into a type class? Just this conversion. And then we can have nice things again (throwBuiltinErrorWithCause and readKnownSelf).
There was a problem hiding this comment.
I'm personally not a huge fan of adding a whole type class for this, but unless we want to change(or merge) CekUserError and CkUserError, I can't think of a better way without code duplication I previously had.
There was a problem hiding this comment.
It's not the code duplication that I particularly hate here, it's that it propagates into user space in a non-trivial way (where by "user" I mostly mean "someone who writes tests"). readKnownSelf is a handy thing, I don't want to lose it. If it was only about the machines, I'd swallow the pill.
We can't unify CkEvaluationError and CekEvaluationError into a single type. It's pretty much a coincidence that both are based on MachineError, we could've had (and did have) an evaluator that isn't an abstract machine. Plus, CekUserError and CkUserError do differ, since the CK machine can't with an out-of-budget error.
plutus-core/plutus-core/src/PlutusCore/Evaluation/ErrorWithCause.hs
Outdated
Show resolved
Hide resolved
SeungheonOh
force-pushed
the
seungheonoh/6160-evaluation
branch
from
2652bf4 to
6ba24f0
Compare
SeungheonOh
force-pushed
the
seungheonoh/6160-evaluation
branch
from
6ba24f0 to
b691ee1
Compare
SeungheonOh
force-pushed
the
seungheonoh/6160-evaluation
branch
from
b691ee1 to
905303e
Compare
SeungheonOh
force-pushed
the
seungheonoh/6160-evaluation
branch
from
905303e to
901578a
Compare
SeungheonOh
force-pushed
the
seungheonoh/6160-evaluation
branch
from
901578a to
80e2c5d
Compare
|
@effectfully We can merge this if everything looks good |
Closes #6160
Removes prismatic error handling from Ck/Cek machine implementations.
There is a very minor performance degradation, and I don't know where it's coming from. I'll see if I can dig into ghc core tomorrow