Re: [isabelle] "Unfolding" the sum-of-products encoding of datatypes



>> Returning 1 in both cases would be even less compatible (esp. for list), and returning 0 in both cases is -- well -- precisely the old behavior, which doesn't have the nice "foolproof" property mentioned by Andreas, and for which I can easily construct an example like yours above that exhibits an odd difference in behavior (which is even less regular and intelligible).
> 
> I assume by "exhibits an odd difference in behavior" you mean some term involving both size and size_t? They were never claimed or intended to have a fixed relationship.

If you define type U by nesting through type T, the "size" function of U will depend on "size_T" -- hence there is a connection between the two. The lack of uniformity of the old definition is visible in examples such as

    (* with Isabelle2014 *)

    datatype 'a x = X 'a

    thm x.size

    datatype 'a y = Y "'a y x" | Y'

    thm y.size

    value "size (X Y')"       -- "returns 0"
    value "size (Y (X Y'))"   -- "returns 2"

> But your argument that this feature was not documented and seemed crazy to you and that thus you felt free to change it shows a cavalier attitude towards source code.

The tone of some of your emails reveals a cavalier attitude towards the people who work or worked for or with you. We have had instances of passive-aggressive emails from your part regarding minor points of datatypes (minor compared with the scale of the whole BNF entreprise), some of it on-list, some off-list. You will remember how this ended. Because you had the courage to apologize, you came out of the deal as an (even) greater man in my eyes than before.

I had reasons to believe this would be the first and last time we would be going into that loop, but alas the same nonconstructive pattern is arising again -- and again in connection with the datatypes.

I would greatly appreciate if you could keep your comments -- whether on-list or off-list -- to objective observations, as opposed to a procès d'intention. I don't know what I've done to you to deserve this; clearly, I must have done something to annoy you, but I doubt it has anything to do with the "size" function. I would appreciate if you could tell it to me frankly off-list rather than through insinuations on-list.

I'm in Nancy this week. You can also pick up the phone if you think this would be more helpful. The phone number is on my web page.

> Let me assume in your favour

(No comment on this condescending phrase.)

> that the change had no negative effect in the distribution and the AFP

It had one negative effect on one AFP entry (Fitting), which was nearly trivial to work around.

> and that the problems in IsaFor only showed up later.

That's correct.

Jasmin





This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.