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

On 18/11/2015 11:56, Jasmin Blanchette wrote:
When I read "some" I wondered what that means. Experimentally I found:

datatype t1 = A bool
==> size (A True) = 0

datatype 'a t2 = A 'a
==> size (A True) = 1

I understand why, but I am not convinced this difference in behaviour is beneficial for users of size.

Beneficial as opposed to what?

Detrimental. In the above example an abstraction step now changes the behaviour of size.

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. You can of course view that as an advantage of the new definition of size.

And of course, the old way of doing things required two "primrec" definitions instead of one "primrec" and one simple "definition".

That is an implementation advantage.

The raison d'etre of the old size function were termination proofs and for those it works slightly better than the new schema. On the other hand there is the relationship to size_t that seems to be useful in at least one case. Hence I am not saying we must go back to the previous definitions. 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. Let me assume in your favour that the change had no negative effect in the distribution and the AFP and that the problems in IsaFor only showed up later.


If I could go back in time, I'm still not sure if we would go for 100% compatibility with the old package or for the current scheme, but I would have brought it up for discussion on "isabelle-users". I suspect the outcome of the discussion would have been "don't fix it if it ain't broken".

In other words, the old package defined "size" and "size_list" (or rather, back then, "list_size") independently of each other, with some anomalies. IIRC, a constructor like "C 'a" used to count as 0 for "size" (instead of 1 now) and as "1 + f a" (where a is C's argument of type 'a) for "size_list". I thought this was crazy, but experience has shown that the old definition often gave better automation in termination proofs, as the IsaFoR developers discovered when porting their theories to the new package.

I could have told you that because that is one of the reasons for the old design. Experience, not only doctrine.

I believe you are mistaking lethargy for strategy.

If the old design had been documented in any way, it might have helped me understand it and replicate it. But not only it wasn't documented, the odd behavior looked so much like an oversight (in terms of both behavior and code) that it didn't cross my mind to ask around. Had I realized for one second that there might be a deeper reason for the behavior, I would have not hesitated to bring this up.

If there is a strong consensus in favor of restoring the old behavior, it wouldn't be terribly hard for me to change things to how they used to be. But from what I understand, the porting pains where not very big and are now behind us, and the new behavior is actually useful sometimes (cf. Andreas's solution and Manuel's "foolproof" comment).


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

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