Eindhoven, 1 September 1994.
In his email of 25 August 1994 W.M. Farmer describes the usage of
types and sorts in IMPS. I like to remark that this is very close
to what is presented in the typed set version of the Mathematical
Vernacular (let me call it MV87) as published in
N.G. de Bruijn, The Mathematical Vernacular, a language
for mathematics with typed sets.
In: Proceedings of the Workshop on Programming Logic,
Editors Peter Dybjer et. al. Report 37,
Programming Methodology Group, ISSN 0282-2083.
University of G\"{o}teborg and Chalmers University
of Technology (1987).
This report did not have the sections with examples and remarks
of the older MV version, but in the new edition (in "Selected
Papers on Automath", to appear in the North Holland series Studies
in Logic), these sections (in adapted form) will be added.
MV87 uses the word "substantive" instead of "types" and
"sorts". Having a particular substantive, one can form
sub-substantives, but never the other way round. Reading a book from
the beginning onwards, one can see, for every substantive that
appears, what the original biggest substantive was. In the
metalanguage that biggest one is called the "archetype". These
archetypes are needed as the types when implementing MV87 in a typed
language, but in the books they are not explicitly mentioned. One of
the advantages is that there are possibilities to embed a finished
book into a book with bigger archetypes without having to change
anything.
One can introduce primitive substantives (like Hilbert did with
"line" and "point"), and those are archetypes. One can also introduce
substantive variables, like "let xi be any substantive". These are
archetypes during their lifetime, but it is allowed to substitute any
substantive for them, archetypical or not. This system was called
"Archetype Anonymous". I do not know whether IMPS gives that same
amount of freedom. I wonder what the difference with PVS would be.
From a given archetype one can get a hierarchy of subtypes later
in the book, but one can never get to supertypes of the archetype.
That is to say, not in the way we write books by adding lines at the
end only. If we want to get to supertypes we have to change things
earlier in the book.
N.G. de Bruijn