On 21.11.2014 15:00, Christian Sternagel wrote:
Hi Dmitriy,
thanks for another round of clarification (I should really reread old
emails before referring to them).
On 11/21/2014 02:43 PM, Dmitriy Traytel wrote:
In general, why not create map-functions that allow to map over *all*
type parameters. (As I understand it, this was done just a few month
ago. What where the reasons for the change?).
There was no change, our map functions always have ignored the dead
parameters. You are confusing this with phantom variables (which used to
be dead, but are now live, e.g. in "datatype 'a ref = Ref addr" from
Imperative_HOL)
You are right of course. Sorry for the confusion!
When we last brought up this point, Dmitriy suggested that users that
use "dead" in their datatypes know what they are doing and that it is
not a problem when packages "break" on such types. However, in IsaFoR
we sometimes kill type parameters just because otherwise the (huge)
datatype declaration would take to much resources (in terms of memory
and time). Still, there is no compelling reason (as far as I see) to
not having compare- and/or show-functions for those types. Wouldn't it
be generally useful to always have "total" map-functions (and
appropriately plug in "id"s in the internal BNF constructions)?.
Let me cite the relevant part of my email that you refer to.
On 13.11.2014 15:40, Dmitriy Traytel wrote:
I would not care too much about such dead annotations. If a user made
a variable dead explicitly, she might be aware that this has some
disadvantages, so it is ok for some automatic tool to refuse working.
A more interesting question is if you can/want to handle datatypes
where the dead variable naturally arises, e.g., trees nested through
functions:
Now, that I see your concrete application, I believe the answer to my
question is "no". I.e. "(show, show) tree" is not an instance of show
(just as"(show, show) fun" is not). This means that you do care about
the dead parameters!
When you use the dead annotation for efficiency, guess where the
efficiency comes from---it comes mainly from not generating set
functions, generating a "smaller" map-function, and proving no (or less)
theorems about them.
Alas, no free lunch :)
I conclude that in our situation (i.e., comparators and
show-functions) it is natural to not support datatypes with dead type
parameters. Would you agree?
Yes.
Dmitriy
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
