> But what is really needed? Haskell does not offer Projl/r at all
but lefts, rights and paritionEithers.
In IsaFoR we use Sum_Type.Projr and Sum_Type.Projl. It would just feel
official" if you didn't have to use the cumbersome prefix.
Sum_Type.Projr and Sum_Type.Projl are the destructor view on datatypes,
which are necessarily partial. But most formalisations in Isabelle
follow the constructor view and use case expressions for destruction,
for which there is a reasonable setup (simp rules, split rules, etc.).
(Sum_Type.Projl x) is (almost) equivalent to (case x of Inl y => y) and
(Sum_Type.Projr x) to (case x of Inr y => y).
A not entirely related idea is the setup of an (executable) error
"+" (which is used heavily in IsaFoR for example).
I would recommend not to use sum types for such things, but introduce a
new type with an error element. This has the advantage that split rules
and the like can be applied more precisely. If sum types are used for
other notions in a formalisation, too, the general simplification and
split rules might slow break down proof automation because they also
apply to the other parts.
To this end I once tried to setup such a monad to use for partial
was heading towards a parsec-like parser combinator library; side
are not many deep properties I wanted to proof about this combinators,
but it is
just nice to be able to write also your parser in Isabelle when you
generation) but failed to complete since different error cases (i.e.,
containing different error messages) are not equal. Maybe this could be
generalized using some equivalence relation?
I suppose that the error messages are irrelevant to the proofs, so they
need not be part of the logic. If the error monad is a type constructor
of its own (rather than a sum type), you can identify all error cases in
the logic and handle the error messages in the code generator only.
Here's the idea:
datatype 'a err = Error | OK 'a
definition Raise_error :: "String.literal => 'a err"
where "Raise_error msg = Error"
code_datatype Raise_error OK
In the logic, all errors are the same "Error" value, but the generated
code uses Raise_error as constructor which also stores the error
message. Hence, the logical problem with different error messages no