Re: [mizar] weak types

[Josef Urban <urban@ktilinux.ms.mff.cuni.cz>]

> > The typical way to cope with the situation is to use permissiveness
> > 
> >  definition let G,H be Group such that
> > A: G,H are_isomorphic;
> >    mode Isomorphism of G,H means
> >     .....;
> >    existence by A;
> >  end;
> 
> But that does not apply to clusters, and clusters are more 
> frequent and usually preferable to modes (especially now, when the 
> nonclusterable attributes are gone). It fixes the type hierarchy, but 
> the price is that you have to drag along the assumptions, if you need the 
> definiens. So you can end up with funny implications like:
> 
> ex M being Cardinal st M is_measurable implies
> for N being MeasurableCardinal holds N is inaccessible. 

Actually we have (at least) two kinds of "permissive" definitions:
(1) Those with assumptions (like above)
(2) "per cases" definitions, like that of "Element of X":
    "it in X if X is non empty otherwise it is empty;"

If we rewrote (2) into the (1)-like format, it would be:
let X be set such that A: X is non empty;
mode Element of X means it in X;
existence by A;

One advantage of (2) is that the mode is specified even if the assumption 
is not satisfied, while for (1), we then just (implicitly) know that it is 
some non empty subclass of its parent type.

Other advantage of (2) is that it makes clusters possible, and 
often the assumptions do not have to be dragged along.

The problem starts with multiple inheritance (i.e. clusters):
say we have: "T_i is inhabited if C_i holds", "C1 implies C2", and 
"C1 implies C3". Things are fine if we assume C1, but bad if not - we may 
be unable to set a good default for T1. e.g. if "(C2 & C3) implies C1" 
holds.
 
The weak types (or clusters) could deal with this, are more intuitive 
(things are what they should be, or do not exist at all, not some strange 
default or a whole science of managing strange defaults),  
and could thus possibly also reduce the need for using the Global Choice.

Josef