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
datatype 'a y = Y "'a y x" | Y'
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.
This archive was generated by a fusion of
Pipermail (Mailman edition) and