[FOM] Mizar's type system

[Josef Urban]

Dear Anthony,

I am lagging behind this thread and relying on Freek and others, so just this:

> Maybe `separate type mechanism' is the wrong phrase; my only real
> target is the `separate type concept.' I would prefer to avoid having
> to distinguish between "Nat the type" and "Nat the predicate;" I would
> prefer that only the predicate exist.

This is the case. Once you define the "type-predicates" "finite" and
"empty", you use them as predicates by saying "X is finite" and "X is
empty". This is really just syntactic (or in Andrzej Trybulec's world
"linguistic") sugar for "finite(X)" and "empty(X)". You never write
the latter.

The only difference is that these "type-predicates" allow additional
"type automation clauses" (in more recent systems one calls similar
things generally "type-class mechanisms"), such as making the type
checker always know that everything empty is also finite.

Sometimes you also want to have the *set* Nat (rather than the
"type-predicate"). In Mizar, creating it from small types is an easy
syntactic construct - for which you usually still want a suitable
user-friendly abbreviation.

> I accept the necessity of a
> separate mechanism for type inference. My impression of things is that
> the predicate logic is semidecidable but certain fragments of it are
> not only decidable but *efficiently* decidable. The type mechanism
> would automate proofs of some natural-seeming fragment, e.g. horn
> clauses plus conclusions about the type of a function based on the
> types of its arguments.

Yes that's basically it in Mizar - some horn clauses - see my MoMM
paper (4.2 and further): http://mws.cs.ru.nl/~urban/momm.pdf

> It would apply to *all* predicates, so when
> a theorem depends on whether b is zero, it wouldn't matter whether
> "b != 0" is expressed as an ordinary predicate or as a type that is
> quantified over---the proof checker would recognize a predicate as
> a predicate.

This is tried in the SPASS soft-type system, which indeed does some
auto-detection of some decidable fragments. In ITP, you cannot have it
all - it becomes too brittle and things break during large-library
refactoring (the auto-detected decidable fragment could differ a lot
after addition of a single fact). That's why this fragment is to
various extent explicitly written by the users. Obviously, this is an
interesting research topic - e.g., Georges Gonthier has done a lot
recently to have a lot of implicit typing which is still robust under
refactoring.

Best,
Josef