[isabelle-dev] BNF: dead or alive?

[Christian Sternagel]

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?

cheers

chris