Re: [mizar] Once more: empty types

[Freek Wiedijk <freek@cs.ru.nl>]

Hi Josef,

>If there is any reason to be "unhappy", then it is for me
>the lack of relevant arguments for "only nonempty types".

Well, once you allow possibly empty types then no one will
ever prove an existential cluster again.

>Also, sometimes it really is the case, that more relevant
>arguments "are in the heads" of people like Andrzej, and
>it's just difficult to communicate them, and they may have
>a point after all :-).

There very well might be, and I would love to be convinced.

However in Coq we _do_ have types that can be empty (in
fact they are essential there for doing logic), and I never
saw any problem _there_ with them...  So I would be very
surprised if there was a good argument for only having non
empty types.  You can do serious formalizations when all
types are allowed to be empty.

I can imagine that they are needed for permissive functor
definitions.  (In HOL you need non emptiness of types for
the choice operator; and permissive functor definitions are
closely related to that.)  But I don't mind having the system
to require _those_ types to be required to be non empty.
(Who uses permissive functor definitions anyway?)

Freek