Email Gateway (Aug 18 2022 at 17:56): Email Gateway (Aug 18 2022 at 17:56):From: Alfio Martini <alfio.martini@acm.org>
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!
Email Gateway (Aug 18 2022 at 17:56):From: Brian Huffman <brianh@cs.pdx.edu>
Hello Alfio,
Yes, there is a sum type 'a + 'b, which has constructors Inl :: 'a =>
'a + 'b and Inr :: 'b => 'a + 'b.
I am a bit surprised that this type is mentioned nowhere in the
tutorial. However it is documented in "What's in Main", which is found
on the Isabelle documentation page:
http://isabelle.in.tum.de/documentation.html
Inl and Inr are used in lots of places in the example theories that
come with the distribution; just use grep.
Email Gateway (Aug 18 2022 at 17:56):From: Tobias Nipkow <nipkow@in.tum.de>
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
Email Gateway (Aug 18 2022 at 17:56):From: Christian Sternagel <christian.sternagel@uibk.ac.at>
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
Email Gateway (Aug 18 2022 at 17:56):From: Alfio Martini <alfio.martini@acm.org>
Thank you all for the quick replies!
Cheers
Email Gateway (Aug 18 2022 at 17:57):From: Tobias Nipkow <nipkow@in.tum.de>
Before we define a new type we should rather make the existing one more
usable. But what is really needed? Haskell does not offer Projl/r at all
but lefts, rights and paritionEithers.
Tobias
Email Gateway (Aug 18 2022 at 17:57):From: Christian Sternagel <christian.sternagel@uibk.ac.at>
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!
Email Gateway (Aug 18 2022 at 17:57):From: Andreas Lochbihler <andreas.lochbihler@kit.edu>
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.
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.). For example,
(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).
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 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?
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 longer occurs.
Andreas
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!
Email Gateway (Aug 18 2022 at 17:57):From: Christian Sternagel <christian.sternagel@uibk.ac.at>
On 07/27/2011 02:31 PM, Andreas Lochbihler wrote:
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.
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.).
For example,
(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).
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
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?
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
longer occurs.
This looks nice. However, we do compose error messages incrementally
(i.e., add more precise information to errors at different places). I do
not immediately see how this could be achieved with a single error
constructor. Any hints?
cheers
chris
Andreas
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!
Email Gateway (Aug 18 2022 at 17:57):From: Andreas Lochbihler <andreas.lochbihler@kit.edu>
Dear Christian,
In code equations, you can "pattern-match" on the pseudo-constructor
Raise_error. If you need more structured types than String.literal, the
following with phantom type variables should work for you:
datatype ('a, 'b) err = Error | OK 'b
definition Raise_error :: "'a => ('a, 'b) err"
where [simp]: "Raise_error msg = Error"
code_datatype Raise_error OK
primrec more_info :: "('a, 'b) err => ('a * String.literal, 'b) err"
where
"more_info Error = Error"
| [code]: "more_info (OK b) = (OK b)"
lemma more_info_Raise_error [code]:
"more_info (Raise_error a) = Raise_error (a, STR ''info'')"
by simp
Cheers,
Andreas
Last updated: Apr 26 2024 at 20:16 UTC