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

Dear Jasmin,

The only point I was trying to make is a very general one: In the absence of external documentation, the source code should be taken seriously or questioned but not just changed. I am sure we agree on this but in the light of the size discussion I felt it was worth reemphasizing on the list. No insult intended.


On 18/11/2015 13:43, Jasmin Blanchette wrote:
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.


Attachment: smime.p7s
Description: S/MIME Cryptographic Signature

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