[isabelle-dev] BNF: dead or alive?

[Dmitriy Traytel]

Hi Christian,

On 21.11.2014 14:09, Christian Sternagel wrote:
> Dear list,
>
> sorry for the subject ;)
>
> René and I are currently at adapting the Show(_Generator) entry of the 
> AFP to the new datatype package. And again we stumbled across some 
> difficulties we already encountered when adapting the Order_Generator 
> (and which are not resolved yet).
>
> I think it best to first demonstrate what I intend to achieve and why 
> our "recipe" looks as it does. So please bear with me.
>
> The goal is, for a given datatype, say "'a list", to automatically 
> generate a show-function, i.e., of type
>
> (nat => 'a => shows) => nat => 'a list => shows
>
> that can be used to convert lists into a string-representation (where 
> "shows" is an abbreviation for "string => string" and the additional 
> "nat" argument is there to indicate whether the result should be 
> parenthesized).
>
> Moreover this construction should work via plain 'primrec' (since 
> otherwise the jungle of cong-rules and set-simps that looms ahead is 
> too daunting). Lets come back to lists:
>
> primrec showsp_list :: "('a => nat => shows) => nat => 'a list => shows"
> where
>   "showsp_list s p Nil = shows_string ''Nil''" |
>   "showsp_list s p (Cons x xs) =
>     shows_pl p o shows_string ''Cons'' o shows_space o
>       s 1 x o shows_space o
>       showsp_list s 1 xs o
>     shows_pr p"
>
> Well, this works fine. Now a slightly more complex datatype
>
> datatype 'a tree = Tree 'a "'a tree list"
>
> and its show-function:
>
> primrec showsp_tree :: "(nat ⇒ 'a ⇒ shows) ⇒ nat ⇒ 'a tree ⇒ shows"
> where
>   "showsp_tree s p (Tree x y) =
>     shows_pl p o shows_string ''Tree'' o shows_space o
>       showsp_list (showsp_tree s) 1 y o
>     shows_pr p"
>
> But wait a minute. This results in:
>
> primrec error:
>   Invalid map function in "showsp_list (showsp_tree s) 1"
>
> Which is the reason for doing everything a little bit different. 
> Namely, we start with show-functions that assume that all type 
> parameters where already replaced by "shows" (we call them partial 
> show-functions, because parts of their argument are already turned 
> into "shows"). Then the above turns into:
>
> primrec pshowsp_list :: "nat ⇒ shows list ⇒ shows"
> where
>   "pshowsp_list p Nil = shows_string ''Nil''" |
>   "pshowsp_list p (Cons x xs) =
>     shows_pl p o shows_string ''Cons'' o shows_space o
>       x o shows_space o
>       pshowsp_list 1 xs o
>     shows_pr p"
>
> primrec pshowsp_tree :: "nat ⇒ shows tree ⇒ shows"
> where
>   "pshowsp_tree p (Tree x y) =
>     shows_pl p o shows_string ''Tree'' o shows_space o
>       pshowsp_list 1 (map (pshowsp_tree 1) y) o
>     shows_pr p"
>
> And we obtain our originally desired functions by
>
> definition "showsp_list s p xs = pshowsp_list p (map (s 1) xs)"
> definition "showsp_tree s p t = pshowsp_tree p (map_tree (s 1) t)"
Looks reasonable so far.

>
> This seems to work pretty well as long as there are no dead type 
> parameters involved. *HOWEVER*, how should we go about turning some 
> datatype "(dead 'a, 'b) dt" into "(shows, shows) dt" if their is no 
> way of mapping the "'a"?
>
> 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)

> 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:
>
> datatype ('a, 'b) tree = Node 'a "'b => ('a, 'b) tree"
>
> under the assumption that you have the map function for tree which 
> would be contravariant in 'b, i.e. of type "('a => 'c) => ('d => 'b) 
> => ('a, 'b) tree => ('c, 'd) tree". If the answer to this question is 
> yes, then BNF's indeed don't quite capture the right notion of maps 
> for you, and you might want to resort to the database collected by the 
> functor command. If the answer is no, this means that you do care 
> about the (truly) dead variables.
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.

This hijacks a semantic notion of being dead (which was originally used 
only for contravariant parameters such as 'a in 'a => 'b) for the cause 
of efficiency---of course it comes with some limitations.

> Maybe unrelated: The datatype declaration
>
> datatype (dead 'a, 'b) dlist = DNil | DCons "'a" "'b" "('a, 'b) dlist"
>
> work, but
>
> datatype (dead 'a, 'b) dlist = DNil | DCons "'a × 'b" "('a, 'b) dlist"
>
> results in an internal tactic failure.
Thanks for the report! The tactic failure comes from the size plugin 
(which we will repair soon). Temporarily one can disable the plugin to 
get this declaration through.

datatype (plugins del: size) (dead 'a, 'b) dlist = DNil | DCons "'a × 
'b" "('a, 'b) dlist"

Dmitriy