\documentstyle [11pt] {article}

\newcommand{\mizar}{{\sc Mizar}}
\newcommand{\automath}{{\sc AutoMath}}
\newcommand{\qed}{{\sc QED}}
\newcommand{\mdisp}[1]{{\hspace*{.3in}\begin{minipage}[t]{5.7in}\vspace*{0.05ex}\
\begin{flushleft} \vskip-5mm {#1} \vspace*{2ex}\end{flushleft}\end{minipage}}}
                                 
\begin{document}

\title{To type or not to type\footnote{This is a short summary of my
 presentation at the QED Workshop II, Warsaw, 20-22 July 1995.}}

\author{Piotr Rudnicki
\thanks {Supported in part by NSERC Grant No. OGP9207.} \\
Department of Computing Science, The University of Alberta, \\
Edmonton, Alberta, Canada T6J 2H1. \\
{\tt email: piotr@cs.ualberta.ca}
}

\date{}

\maketitle

\section{Introduction}

N. G. de Bruijn in his letter to R. S. Boyer of August 19, 1994
which appeared at the \qed\ mailing list wrote:

\begin{quotation}
... in type systems like \automath\ the notion of elementhood can be seen
as typing.  Customers who like typed sets (let me call these customers
TSC's) introduce a real variable by a single block opener, like

\mdisp{\tt let x be real number} 
where {\tt real number} is taken as a type.  So for the TSC's
it is the introduction of a typed variable.  The customers who prefer to
think in terms of untyped sets (let me call them USC's), however, have to
order by means of two block openers:

\mdisp{\tt let x be a set}  
and
\mdisp{{\tt assume this x is a real number}.}
In their case we have to realize that {\tt x is a real number}
is the property of the set {\tt x}.  The first one of the two block
openers is the introduction of a typed variable (where the type is {\tt set}),
the second one is the assumption.
\end{quotation}

The word {\em type} is used with a number of different meanings and someone
noticed that for the use of {\em type} as above, probably one should
use {\em sort}.  In \mizar\ this notion is named {\em syntactic type}.

The question that we would like to address is: {\em What are the advantages
and disadvantages of using syntactic types?}

In \mizar\ one can work without syntactic types (types for short).  However,
the \mizar\ data base has been developed using a hierarchy of types as it
seems closer to everyday mathematical practice and the developers of
\mizar\ articles usually followed that practice as they knew it.

\section{What are syntactic types in \mizar?}

Let us look at an example of how the type of {\em finite sequence of X}
is defined.  In article {\tt FINSEQ\_1} we have the following definition:

\mdisp
{\small \tt
\ definition\ let\ D\ be\ set;\\
\ \ mode\ FinSequence\ of\ D\ ->\ FinSequence\ means\\
\ \ \ rng\ it\ c=\ D\ ;\\
\ \ existence\ \ proof \\
\ \ \ \ \ ::\ {\rm Here we have to demonstrate that there is an object of type}\\
\ \ \ \ \ ::\ {\tt FinSequence} {\rm whose range is a subset of {\tt D} }\\
\ \ end;\\
\ end;
}

{\tt FinSequence of} is a type constructor which given a specific set as
a parameter results in a type expression which can be used then to type
objects.  Later on we can then write:

\mdisp{\small \tt
\ let FST be FinSequence of NAT;
}

The denotation of {\tt FinSequence of NAT} is the set of all finite sequences
whose range is a subset of {\tt NAT}.  There is a substantial difference
between the above introduction of {\tt x} and the following:

\mdisp{\small \tt
\ let FSU be set;\\
\ assume FSU is FinSequence of NAT;
}

\noindent which can be characteristic of the USC at the de Bruijn's restaurant.
In \mizar, the typing expressed at the time of introducing an object
({\tt let ...}) is processed differently then the typing expressed in an
assumption.  The type information contained in the object declaration
is always automatically taken into account by the \mizar\ semantic analyzer
and inference checker, while the information contained in an assumption
must be explicitly referenced and is effective only for the inference
checker.

In the \mizar\ abstract of article {\tt FINSEQ\_1} the definition
of {\tt FinSequence of ...} appears as:

\mdisp{\small \tt
\ definition\ let\ D\ be\ set;\\
\ \ mode\ FinSequence\ of\ D\ ->\ FinSequence\ means\\
::\ FINSEQ\_1:\ def\ 4\\
\ rng\ it\ c=\ D\ ;\\
\ end;
}

\noindent and the label {\tt FINSEQ\_1:def 4} is used to make a reference to the
definiens of {\tt FinSequence of D} when needed.  (The proofs do not
appear in \mizar\ abstracts.)
The above definition says that {\tt FinSequence of D} is a {\tt FinSequence}
with an additional condition given by the definiens.  {\tt FinSequence} is
the mother type of {\tt FinSequence of D} and {\tt FinSequence of D} is
a subtype of {\tt FinSequence}.  Let us have a look at the definition
of {\tt FinSequence} (in its abstract format, without proof of existence):

\mdisp{\small \tt
definition\\
\ \ mode\ FinSequence\ is\ FinSequence-like\ Function;\\
end;
}

{\tt FinSequence} turns out to be a shorthand for a {\tt Function} with
the attribute {\tt FinSequence-like}.  This attribute, applicable to
{\tt Function} is defined as follows:

\mdisp{\small \tt
\ definition\\
\ \ mode\ FinSequence-like\ ->\ Function\ means\\
::\ FINSEQ\_1:\ def\ 2\\
\ ex\ n\ st\ dom\ it\ =\ Seg\ n\ ;\\
\ end;
}

The above is read: the domain of a {\tt FinSequence-like Function} is
equal to an initial segment of natural numbers.  And below we quote the
sequence of definitions that lead from the primitive notion of {\tt set}
to the notion of {\tt Function}, again we skip the correctness conditions:

\mdisp{\small \tt
definition\\
\ mode\ Relation-like\ ->\ set\ means\\
::\ RELAT\_1:\ def\ 1\\
\ \ x\ $\in$\ it\ implies\ ex\ y,z\ st\ x\ =\ {[}y,z];\\
end;
}

\mdisp{\small \tt
definition\\
\ mode\ Relation\ is\ Relation-like\ set;\\
end;\\
\ \\
definition\ let\ X\ be\ set;\\
\ pred\ X\ is\ Function-like\ means\\
::\ FUNCT\_1:\ def\ 1\\
\ for\ x,y1,y2\ st\ {[}x,y1]\ $\in$\ X\ \&\ {[}x,y2]\ $\in$\ X\ holds\ y1\ =\
 y2;\\
end;\\
\ \\
definition\\
\ cluster\ Relation-like\ Function-like\ set;\\
end;\\
\ \\
definition\\
\ mode\ Function\ is\ Function-like\ Relation-like\ Any;\\
end;
}

The \mizar\ semantic analyzer takes into account the entire
chain of mother types.  In particular, the object {\tt FST} introduced
above besides being a {\tt FinSequence of D}, is also a {\tt FinSequence},
a {\tt Function}, a {\tt Relation}, and of course a {\tt set} as {\tt set}
is the root of the tree of types.  All operations defined for a mother type
are applicable also to the subtype.  For instance, function application
is defined as follows:

\mdisp{\small \tt
\ definition let f be Function, x be Any; \\
\ \ func f.x -> Any means \\
\ :: FUNCT\_1: def 4 \\
\ [x,it] $\in$ f if x $\in$ dom f otherwise it = 0; \\
end;
}

And therefore we can write {\tt FST.10} which is always denoting.  Note, that
we must not write {\tt FSU.10} as function application requires that the left
argument of the dot is a function which does not follow from the declaration
of {\tt FSU} and no assumption regarding {\tt FSU} is taken into account by
the semantic analyzer.

Note that although {\tt FST.10} is denoting its type is {\tt Any},
({\tt Any} and {\tt set} are synonyms).  Can we force {\tt FST.10}
to be of type {\tt Nat}?  We found the definition of certain functor $\pi$
in the \mizar\ data base:

\mdisp{\small \tt
definition\ \\
\ \ let\ X\ be\ set,\ D\ be\ non\ empty\ set,\ p\ be\ PartFunc\ of\ X,\\
\ \ \ \ \ \ D,\ i\ be\
 Any;\\
\ assume\ \ i\ $\in$\ dom\ p;\\
\ func\ $\pi$(p,i)\ ->\ Element\ of\ D\ means\\
::\ FINSEQ\_4:\ def\ 4\\
\ \ \ it\ =\ p.i;\\
end;
}

However, we must not write {\tt $\pi$(FST,10)} yet, as {\tt FinSequence of NAT}
is not a partial function ({\tt PartFunc of NAT,NAT}) in the \mizar\ sense.
In fact, {\tt PartFunc} does not have {\tt Function} in the chain of its
mother types!  The mode (type constructor) {\tt PartFunc} has been derived
as follows:

\mdisp{\small \tt
definition\\
\ let\ X,Y;\\
\ mode\ Relation\ of\ X,Y\ ->\ Subset\ of\ {[}:X,Y:]\ means\\
::\ RELSET\_1:\ def\ 1\\
\ \ not\ contradiction;\\
end;\\
\ \\
definition\\
\ let\ X,Y;\\
\ cluster\ ->\ Relation-like\ Subset\ of\ {[}:X,Y:];\\
end;\\
\ \\
definition\ let\ X,Y;\\
\ \ cluster\ Function-like\ Relation\ of\ X,Y;\\
\ end;\\
\ \\
definition\ let\ X,Y;\\
\ \ mode\ PartFunc\ of\ X,Y\ is\ Function-like\ Relation\ of\ X,Y;\\
\ end;
}

How can we make \mizar\ treat a {\tt FinSequence of D} as a
{\tt PartFunc}?  For this we use a mechanism known as {\tt redefinition}
of modes.  First, we show that the attribute {\tt FinSequence-like}
is applicable to partial functions (article {\tt FINSEQ\_4}):

\mdisp{\small \tt
definition\ let\ D\ be\ set;\\
\ cluster\ FinSequence-like\ PartFunc\ of\ NAT,D:
}

\mdisp{\small \tt
\ \ existence\ proof \\
\ \ \ \ ::\ {\rm Here we have to show that there exists a partial function} \\
\ \ \ \ ::\ {\rm which is} FinSequence-like{\rm .} \\
end;
}

And now we can redefine {\tt FinSequence of D} as a {\tt PartFunc of NAT, D}.

\mdisp{\small \tt
definition\ let\ D\ be\ set;\\
\ redefine\ mode\ FinSequence\ of\ D\ ->\ FinSequence-like\ PartFunc\\
\ \ \ \ \  of\ NAT,D;
\\
\ \ coherence\ proof \\
\ \ \ \ ::\ {\rm Here we have to show that every {\tt FinSequence of D} is}\\
\ \ \ \ ::\ {\rm a {\tt PartFunc of NAT, D}} \\
end;
}

With this redefinition {\tt FST} besides being whatever it was before is also
a {\tt PartFunc of NAT, NAT} and the expression {\tt $\pi$(FST, 10)} is
correctly typed.

\section{Disadvantages of using syntactic types}

\begin{itemize}
        \item
Syntactic types are an additional complication of any proof-checking system
and as such decrease the reliability of the system and of its implementations.
        \item
There is the temptation to define new notions on types that are too narrow.
        \item
Type definitions need to be proven correct:
        \begin{itemize}
                \item
        Since types have non-empty denotations we have to prove existence of
        an object of a newly defined type.
                \item
        When we redefine the meaning of a type we have to prove coherence,
        namely that the type being redefined is coherent with the
        newly added mother type.
        \end{itemize}
        \item
The language must provide means for changing type of an object.
In \mizar\ this is done by the {\tt reconsider} construction.  For example:

\mdisp{\small \tt
let x be Nat; \\
. . . \\
reconsider x as Integer by INT\_1:9;
}

\noindent and from now on {\tt x} is treated as an {\tt Integer}.

Many a time the type change is performed by some artificially looking
manipulations like introduction of otherwise not needed casting function
or using existential quantifier and equality within a formula to ``smuggle''
information that an object of a type is equal to some object of a different
type.
\end{itemize}

\section{Advantages of using syntactic types}

\begin{itemize}
        \item
A collection of some objects may be too big to be a set;
however, we may introduce
a type to name the collection.  For example, we can define the type
{\tt Group} and objects of this type may have an arbitrary set as their
carrier, while there is no possibility to define the set of all groups in
\mizar.
        \item
The information carried by types of objects can be processed more efficiently
by a specialized machine rather than the general inference engine.
        \begin{itemize}
                \item
        Computing the possible types of an object and its attributes (subtypes)
        involves only sentential calculus.
                \item
        The number of possible unifications when the types are taken into
        account is substantially reduced.
        \end{itemize}
        \item
Types facilitate overloading of symbols.  For example, multiplication of
real numbers is announced as (in {\tt HIDDEN}):

\mdisp{\small \tt
definition\ let\ x,y\ be\ Element\ of\ REAL;\\
\ func\ x\ $\cdot$\ y\ ->\ Element\ of\ REAL;\\
\ \ commutativity;\\
end;
}

\noindent and later on characterized axiomatically in {\tt AXIOMS}.  However,
we can redefine this multiplication for natural numbers with a natural
result.  This is done in article {\tt NAT\_1} as follows:

\mdisp{\small \tt
\ definition\ let\ n,k;\\
\ redefine\\
\ \ func\ n\ $\cdot$\ k\ ->\ Nat\ ;\\
\ \ \ coherence\  proof\\
\ \ \ \ \ ::\ {\rm Here we have to prove that indeed when we multiply two}\\
\ \ \ \ \ ::\ {\rm natural numbers we obtain a natural number as a result.} \\
\ \ \ end;\\
\ end;\\
\ \\
}
        \item
Hidden arguments.  Not all arguments of a function or predicate have to be
explicitly mentioned---some may be inferred from types of explicit arguments.
In {\tt CAT\_1} we find the following definition of the composition of
morphisms in a category:

\mdisp{\small \tt
definition\ let\ C be Category; \\
\ \ \ \ \ \ \ \ \ \ \ let a,b,c be Object of C; \\
\ \ \ \ \ \ \ \ \ \ \ let f be Morphism of a, b; \\
\ \ \ \ \ \ \ \ \ \ \ let g be Morphism of b, c;\\
\ assume\ A:\ Hom(a,b)<>$\emptyset$\ \&\ Hom(b,c)<>$\emptyset$;\\
\ \ \ func\ g$\cdot$f\ ->\ Morphism\ of\ a,c\ means\\
\ \ \ . . . {\rm Definiens omitted}\\
\ existence\ proof {\rm Proof omitted}\ end;\\
\ uniqueness;\\
end;\\
\ \\
}

\noindent The pattern of the defined operation has two explicit arguments,
the morphisms in a category, and four implicit arguments that have to be
reconstructed from the explicit arguments to fit what is stated in the
definition.  It is hard to imagine stating explicitly all six arguments
when we use the composition of morphisms, which seems unavoidable if we
do not use syntactic types.
        \item
Reservations.  With types, we can announce that certain identifiers are used
to denote objects of specific types, and later when using the identifiers, we
do not have to repeat the typing information.  This feature of \mizar\ saves
a lot on writing, although some authors do not always use it.

\end{itemize}

\end{document}