[FOM] Mizar's type system

[Anthony Coulter]

Freek Wiedijk writes:
 > Relatedly, Mizar shows that there is no conflict between
 > "working in raw ZFC" and a "typed formalism".  In Mizar
 > everything is a "raw ZFC" set, while everything is fully
 > typed as well.

     I like Mizar's handling of subtypes, where integers are reals and
not a separate set equipped with an injection into the reals. But in a
way the Mizar type feels like a redundant concept---mathematically at
least, unary predicates can be used for the same purpose. Presumably
the "type" concept was separated out from the regular predicates for
reasons of convenience. I would like to see a complete list of such
conveneniences, from the perspective that a predicate-only type system
will have to recreate all of these conveniences before it can be "as
nice as Mizar."

     (Note: My understanding of the Mizar type system is based on
section 1.3.4 of [1] and a cursory scanning of the MML. I do not have
a deep familiarity with the system, so please correct me if I get
anything wrong here!)

The strengths of types over predicates appear to be:

1. You can quantify over them, that is, you can use a syntactic con-
    struct resembling "For all integers x, P[x]" instead of the more
    cumbersome "For all x, if x is an integer then P[x]".

2. Mizar can automate a lot of tedious type inferences (e.g. if m and
    n are integers, then m*(m+n+1) is also an integer) so that you can
    infer "P[m*(m+n+1)]" from "For all integers x, P[x]" without extra
    manual steps.

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.

There are two things I had assumed a priori to be advantages of the
Mizar type system, but on further investigation don't appear to be:

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.]

5. In traditional programming situations, a good type system will help
    the user catch a lot of errors at compile time. This advantage *may*
    apply to Mizar as well; I honestly don't know because I'm not a
    serious Mizar user. But I get the impression from reference [1] that
    type errors are more likely to result from not importing enough
    other articles than they are to result from the user making an error
    while trying to figure out how to write a formula.

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.

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?

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:

a. A way to quantify over unary predicates, so that people can write
    "For all odd x: P[x]" where "odd[x]" is a predicate
b. A way to quantify over n-ary predicates with the last (n-1) slots
    filled in, so that people can write:
    "For all x in S: P[x]" (where "in[x, S]" is a predicate) or
    "For all x < n: P[x]" (where "x < n" is a predicate)
c. A way to manipulate these bounded quantifiers that doesn't require
    them to be nonempty. (This goes a step beyond Mizar in convenience;
    the idea is that "For all x in EmptySet: P[x]" ought to be as easy
    to work with as "For all x in S" when S is a nonempty set.
d. Mechanisms for automatically inferring that m*(m+n+1) is an integer
    whenever m and n are (without making the user explicitly cite the
    theorem that the sum or product of two integers is an integer on
    every line where it is used).
e. Some sort of function overloading? (If numbers and polynomials are
    ultimately the same sort of object, i.e. well-founded ZFC sets,
    then maybe overloading the word "divides" to provide different
    definitions isn't actually the best way to go; it might be better
    to insist that people use either "integerdivides" or
    "polynomialdivides", and work on finding syntactic tricks to
    reduce the amount of typing in such situations.)

Does this sound about right? Or am I missing some other important
advantages to the Mizar type system?

Regards,
Anthony

[1] Freek Wiedijk, "Writing a Mizar article in nine easy steps"
     www.cs.ru.nl/~freek/mizar/mizman.pdf