*To*: Christian Sternagel <christian.sternagel at uibk.ac.at>*Subject*: Re: [isabelle] Defining Union Types*From*: Andreas Lochbihler <andreas.lochbihler at kit.edu>*Date*: Wed, 27 Jul 2011 14:31:41 +0200*Cc*: Tobias Nipkow <nipkow at in.tum.de>, cl-isabelle-users at lists.cam.ac.uk*In-reply-to*: <4E2FF4C6.1030109@uibk.ac.at>*References*: <CAAPnxw1oeghO4nx43XsDD4z4X5ZW2D02ejnfK=vLb_JEx=Bz2A@mail.gmail.com> <4E2E53A8.7090705@in.tum.de> <4E2E66A4.2040406@gmail.com> <4E2F1FD5.7020408@in.tum.de> <4E2FF4C6.1030109@uibk.ac.at>*User-agent*: Mozilla/5.0 (X11; U; Linux x86_64; en-US; rv:1.9.2.13) Gecko/20101208 Thunderbird/3.1.7

> But what is really needed? Haskell does not offer Projl/r at allbut 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.

(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 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?

datatype 'a err = Error | OK 'a definition Raise_error :: "String.literal => 'a err" where "Raise_error msg = Error" code_datatype Raise_error OK

Andreas

cheers chrisTobias 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!

-- Karlsruher Institut für Technologie IPD Snelting Andreas Lochbihler wissenschaftlicher Mitarbeiter Adenauerring 20a, Geb. 50.41, Raum 031 76131 Karlsruhe Telefon: +49 721 608-47399 Fax: +49 721 608-48457 E-Mail: andreas.lochbihler at kit.edu http://pp.info.uni-karlsruhe.de

**Follow-Ups**:**Re: [isabelle] Defining Union Types***From:*Christian Sternagel

**References**:**[isabelle] Defining Union Types***From:*Alfio Martini

**Re: [isabelle] Defining Union Types***From:*Tobias Nipkow

**Re: [isabelle] Defining Union Types***From:*Tobias Nipkow

**Re: [isabelle] Defining Union Types***From:*Christian Sternagel

- Previous by Date: Re: [isabelle] Defining Union Types
- Next by Date: Re: [isabelle] Defining Union Types
- Previous by Thread: Re: [isabelle] Defining Union Types
- Next by Thread: Re: [isabelle] Defining Union Types
- Cl-isabelle-users July 2011 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list