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

[Gerwin Klein]

On 19/08/2011, at 8:10 AM, Stefan Berghofer wrote:

> Tobias Nipkow wrote:
>> Am 12/08/2011 11:27, schrieb Alexander Krauss:
>>> On 08/12/2011 07:51 AM, Tobias Nipkow wrote:
>>>> The benefits of getting rid of set were smaller than expected but quite
>>>> a bit of pain was and is inflicted.
>>> Do you know of any more pain, apart from what Florian already mentioned?
>> 
>> I think he omitted to mention type classes. It comes up again and again
>> on the mailing list.
> 
> Really? In the thread
> 
>  http://thread.gmane.org/gmane.science.mathematics.logic.isabelle.user/260/
> 
> cited by Brian and Alex, Brendan was worried about the fact that one could
> no longer declare arities for sets. In my reply to his mail, I pointed
> out that arities for sets could usually be rephrased as arities for functions
> and booleans. I also asked him to give a concrete example for an arity where
> this was not possible, but I never got a reply, so I assume that this is not
> so much of a problem.

Given his employer Brendan not giving an example is no real indication either way ;-)

I'm not convinced that any class that works for sets can be expressed nicely as a class on the function type and booleans. Splitting up the declaration over two types at least makes it hard to think about. You're right, though, that it may be less of a problem than we currently have the feeling it is. It hasn't prevented anything yet that we wanted to do at NICTA.

Should we ask a wider audience (isabelle-users) if anybody else has good reasons against/for a change?

Cheers,
Gerwin