[isabelle-dev] BNF: dead or alive?

[Dmitriy Traytel]

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