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
usable.
Yes indeed. That's what I meant.

> 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 "more official" if you didn't have to use the cumbersome prefix.

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?

cheers

chris


Tobias

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
lemmas).

cheers

chris


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.

Tobias

Am 26/07/2011 03:57, schrieb Alfio Martini:
Dear Isabelle Users,

Do we have in Isabelle something like a union (sum) type constructor
with
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.

Many thanks!








This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.