Re: [isabelle] Defining Union Types
On 07/26/2011 10:13 PM, Tobias Nipkow wrote:
Before we define a new type we should rather make the existing one more
Yes indeed. That's what I meant.
> But what is really needed? Haskell does not offer Projl/r at all
In IsaFoR we use Sum_Type.Projr and Sum_Type.Projl. It would just feel
"more official" if you didn't have to use the cumbersome prefix.
but lefts, rights and paritionEithers.
A not entirely related idea is the setup of an (executable) error monad
using "+" (which is used heavily in IsaFoR for example).
To this end I once tried to setup such a monad to use for partial
functions (I was heading towards a parsec-like parser combinator
library; side remark: there 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 use code generation) but failed
to complete since different error cases (i.e., Inl's containing
different error messages) are not equal. Maybe this could be generalized
using some equivalence relation?
Am 26/07/2011 09:03, schrieb Christian Sternagel:
Talking of the sum type... I think it would be good to have it more
easily accessible. Currently, e.g., I have to write "Sum_Type.Projr" to
get the right projection. As far as I can see it is mainly for internal
use of some packages. But something like Haskell's Either would be
useful for the library (together with a bunch of useful functions and
On 07/26/2011 07:42 AM, Tobias Nipkow wrote:
It is written "+" and defined in theory Sum_Type, which is part of Main.
It is hardly advertised because in most cases it is nicer to define your
own special datatype.
Am 26/07/2011 03:57, schrieb Alfio Martini:
Dear Isabelle Users,
Do we have in Isabelle something like a union (sum) type constructor
the corresponding injections?
I went through the tutorial and did not find use or reference to it. If
there is, can anyone point to an application
or a written example of this?
I assume there must be a simple way to do it.
This archive was generated by a fusion of
Pipermail (Mailman edition) and