Add MRaise typeclass
This is an alternative to MFail in #488. It allows a monad to present a general error raising mechanism. This includes an example instantiation for option. I didn't do the work of #488 to completely replace MGuard, but if we decide to use this instead of MFail, we can merge the two patches.
Merge request reports
Activity
1204 1204 Notation "'guard' P 'as' H ; z" := (mguard P (λ H, z)) 1205 1205 (at level 20, z at level 200, only parsing, right associativity) : stdpp_scope. 1206 1206 1207 (** For any monad that had a builtin way to raise an exception *) 1208 Class MRaise (E : Type) (M : Type → Type) := mraise : ∀ {A}, E → M A. I'm not entirely convinced "error" is a good term, because this can also be used, for example, for discarding a possible execution in a non-deterministic context (when you realize late that the current execution is actually impossible), in which case what you raise is not error. An example of this in the list monad as the most basic non-determinism monad is to return the empty list. One could have a label type "discard" and decide that
mraise discardmeans the empty list. I intend to do something similar in my development. Although I agree this happens much less often than a regular error case.std++ conventions have had some inspiration from Haskell.
Does this thing have a name in Haskell? I see there is
MonadErrorandthrowErrorin https://hackage.haskell.org/package/mtl-2.2.2/docs/Control-Monad-Error.htmlHaskell
MonadErroris a bit more than this, because it also allows catching errors. But thethrowErrorpart of it is exactly this proposal.However, the reason I liked
MRaiseis that all the others monadic typeclasses,MRet,MBind, andMJoinare verbs about actions that you can do with the monad, and therefore the corresponding term-level function is also a verbmret,mbind,mjoin(With "return" being abbreviated as "ret" ofc). If we keep this consistent naming, the function name would bemerrorwhich is a bit weird because it's not a verb. DoingmthrowerrorormThrowErrorormRaiseErroris a bit inconsistent with how all the other monads are named. I think being able to guess the typeclass term-level action from the typeclass name is a nice property that we should probably try to keep.Alternatively we can do
MThrowandmthrowwhich is basically the same asMRaisebut with a different verb. This has the advantage of having one verb in common with the Haskell counterpart
mentioned in merge request !488 (closed)
If you think it's a good idea. I'll copy #488 commits in my branch and then do this as a modification to preserve @adamAndMath authorship on the original commit (especially all the bits about changing the syntax of
guardeverywhere)Fine to me if it's fine to @adamAndMath.
Out of curiosity: What is the "right" way for two people (say, you and Adam) to work on a merge request together in Gitlab?
-
Out of curiosity: What is the "right" way for two people (say, you and Adam) to work on a merge request together in Gitlab?
- They could work on a branch they can both push to (one can grant other people access to one's own fork)
- One can make MRs against the MR branch (e.g. https://gitlab.mpi-sws.org/adamAndMath/stdpp/-/tree/adamAndMath/mfail)
I think it makes most sense if @adamAndMath gives you permission to push to his branch
I made this MR for converting
MFailintoMThrowin Adam's MR@adamAndMath Do you want to merge it into yours? It's been hanging for a week
@jung @robbertkrebbers should I just make a new MR to this repo with the content of both @adamAndMath and my conversion to
MThrow? @adamAndMath commits would still be under his name of courseThe new MR is #522
1204 1204 Notation "'guard' P 'as' H ; z" := (mguard P (λ H, z)) 1205 1205 (at level 20, z at level 200, only parsing, right associativity) : stdpp_scope. 1206 1206 1207 (** For any monad that had a builtin way to raise an exception *) 1208 Class MRaise (E : Type) (M : Type → Type) := mraise : ∀ {A}, E → M A. 1209 Global Arguments mraise {_ _ _ _} _ : assert. 1210 Global Instance: Params (@mraise) 4 := {}. 1211 Global Hint Mode MRaise ! ! : typeclass_instances. 1212 1213 (** We use unit as the error content for monads that can report an error without 1214 payload like an option *) 1215 Definition mfail `{MRaise () M} {A} : M A := mraise (). 1216 1217 (** mguard or, like mguard but one can specify the error in case of failure *) 1218 Definition mguard_or `{MRaise E M} P {dec : Decision P} {A} 1219 (e : E) (f : P → M A) : M A := I would write this in the same style as
mguardin !488 (closed), i.e., let it returnM Pinstead of having the continuationP → M A.Edited by Robbert Krebbers
1204 1204 Notation "'guard' P 'as' H ; z" := (mguard P (λ H, z)) 1205 1205 (at level 20, z at level 200, only parsing, right associativity) : stdpp_scope. 1206 1206 1207 (** For any monad that had a builtin way to raise an exception *) 1208 Class MRaise (E : Type) (M : Type → Type) := mraise : ∀ {A}, E → M A. 1209 Global Arguments mraise {_ _ _ _} _ : assert. 1210 Global Instance: Params (@mraise) 4 := {}. 1211 Global Hint Mode MRaise ! ! : typeclass_instances. 1212 1213 (** We use unit as the error content for monads that can report an error without 1214 payload like an option *) 1215 Definition mfail `{MRaise () M} {A} : M A := mraise (). 1215 Definition mfail `{MRaise () M} {A} : M A := mraise (). 1216 1217 (** mguard or, like mguard but one can specify the error in case of failure *) 1218 Definition mguard_or `{MRaise E M} P {dec : Decision P} {A} 1219 (e : E) (f : P → M A) : M A := 1220 match decide P with 1221 | left p => f p 1222 | right _ => mraise e 1223 end. 1224 Notation "'guard' P 'or' e ; z" := (mguard_or P e (λ _, z)) 1225 (at level 20, z at level 200, only parsing, right associativity) : stdpp_scope. 1226 Notation "'guard' P 'or' e 'as' H ; z" := (mguard_or P e (λ H, z)) 1227 (at level 20, z at level 200, only parsing, right associativity) : stdpp_scope. 1228 1229 (* mfail replaces MGuard *) 1230 Global Instance mguard_mfail `{MRaise () M} : MGuard M := I suppose this and below is temporary code and would be replaced by proper code once merged with !488 (closed)?
mentioned in merge request adamAndMath/stdpp!1 (merged)
mentioned in merge request !522 (merged)
Replaced by #522
