[FOM] Mizar's type system

[Freek Wiedijk]

Dear Anthony,

>But in a way the Mizar type feels like a redundant
>concept---mathematically at least, unary predicates can
>be used for the same purpose.

Foundationally that's fully correct.  Pragmatatically it
makes a world of a difference.

Only it's not only unary predicates, (n+1)-ary predicates
correspond to dependent types with n variables.
And dependent types are *really* useful if you want to
formalize mathematics (ha!)

>Presumably the "type" concept was separated out from the
>regular predicates for reasons of convenience.

I think it was the other way around: the Mizar
people consider their system to be a generalization of
many-sorted logic.  That also "explains" their non-emptiness
requirements.

>I would like to see a complete list of such conveneniences,

I think you pretty much got them all.

>(Note: My understanding of the Mizar type system is based on
>section 1.3.4 of [1] and a cursory scanning of the MML.

There also is
<http://www.cs.ru.nl/~freek/mizar/miztype.pdf>
although I doubt it will add much for you.

>3. You can overload symbols, so that "x divides y" has
>   one meaning when x and y are numbers and a different
>   one when they are polynomials.

FWIW: this is _really_ nice to have.  The Mizar types
are about overloading as much as about type checking and
predicate inference.

>4. The type system *could* concievably enforce function domains by
>   wiring them into the type system, via something like:
>   "let a be Real; let b be non zero Real; func div(a,b) = ..."
>   [But Mizar does not appear to do this, at least with regards to
>    division by zero.]

That's about how the MML is organised, not about the
type system.  But it just is too inconvenient to do it
like this, because type changes ("reconsider") only are
possible on the proof step level, and not in expressions
(there are no proof terms or things like TCCs!)

>Then there's a weakness of Mizar types:
>
>6. Types must be nonempty; that is, you must prove that at least one
>   object has a certain type before you're allowed to use that type
>   for anything. (I assume that Mizar is using Skolem constants and
>   functions internally, and the restriction to nonempty types is
>   needed to justify that technique.) Ordinary predicates do not
>   suffer from this constraint because they're not coupled so closely
>   to quantifiers.

This is the reason I stopped using Mizar.  I tried hard
to convince Andrzej Trybulec and the other Mizar users at
the time that this was a huge defect, but they did not see
the point.

Josef Urban tells me that it would be a rather small change
to the system to allow non-empty types as well, but I'm
not sure we'll ever see that experiment.

>Now, when it comes to logic, I'm personally comfortable with "sorts"
>(i.e. "hard types" that are not interconvertible; think "many-sorted
>logic") and, like I said earlier, ordinary predicates. So when I try
>to imagine an ideal proof-checker, I look for solutions that involve
>only these concepts, and not a separate type mechanism. How close am
>I to having something workable?

I don't see how this would be different from
Mizar-types-that-don't-need-be-non-empty, but maybe I'm
missing something?

Another thing might be to somehow "identify" types and
classes, so to not have a distinction between the set of
natural numbers (as a class) and the type of natural numbers.
But then you would need to talk about set theory to be able
to talk about the semantics of Mizar.  The nice thing about
the current Mizar is that it's just classical first order
predicate logic, the set theory is only a library on top
of that, and in principle any theory can be used with the
system.  For instance a student of mine, Allan van Hulst,
wrote his master's thesis about using Mizar to formalize a
proof by Albert Visser of the Schroder-Bernstein theorem
in adjunctive class theory (which is a very weak form of
set theory).

So he didn't use the Mizar types, he really relativized
all quantors.  He could have had nice types (interpreted
on the foundational level as predicates, of course), but
he considered it less obvious that he really was working
in that untyped set theory, if he would do that.

>Assuming my list above is complete (please, someone, tell me what I'm
>missing if it's incomplete!) I could theoretically replicate all of
>the "nice" features of types with sorts and ordinary predicates by
>providing the following features:
[...]

So having sorts and predicates seems duplicate, why not work
in an untyped world then?  It sounds a bit HOLZF-ish to me.
And I think you underestimate the amount of "inference" about
the predicates-as-types that is going on in Mizar.  If you
would add all that, how would it then that be different
from having a "separate type mechanism"?  That _is_ the
separate type mechanism!

Freek