[isabelle-dev] (Re-)introducing set as a type constructor rather than as mere abbreviation

[Jasmin Christian Blanchette]

Am 19.08.2011 um 00:00 schrieb Stefan Berghofer:

> thanks for your excellent report, I fully agree with this view. There is
> often a tradeoff between executability and conciseness / abstractness of
> specifications, so I don't think it is a good idea to tweak the logic in
> such a way that it is more suitable for code generation.

Indeed, I think a general point can be made here, and not just about code generation. In the last couple of years, we've run into situations in Quickcheck, Nitpick, the code generator, and perhaps more, where we felt the need for sets as different from functions. However, there is no guarantee that all the people who talked about "sets vs. functions" meant, or needed, the same thing!

For Nitpick (and code generation I guess), it helps to know whether a predicate is a finite set or not. However, we can't expect the entire world to understand "'a set" as a finite set built from {} by adding elements one by one -- and what's the type constructor for the complement of such a set anyway? For Nitpick, Alex and I solved the problem generally by inferring "finite sets" as well as "complements of finite sets" in addition to plain functions [1, sect. 6]. Needless to say, we're in better shape with our robust inference than by just crossing our fingers, hoping that the user distinguishes between "'a set" and "'a => bool" the way we intend to.

Jasmin

[1] http://www4.in.tum.de/~blanchet/jar2011-mono.pdf