For many programmers, the type system of a programming language
serves two purposes:
* Requires you to write annoying annotations in the source
code.
* Complains about perfectly good programs.
A
vast amount of research on type theory has been done by our neighbors
in LFCS and their friends. Unfortunately, this research is highly
abstract and largely impenetrable to the working computer scientist.
The type systems of most common languages, such as C, C++, and Java,
are simple, weak, and make little use of existing theory.
I
will give a brief introduction to formal type systems, focusing not
just on what they are, but how they can be used in practical
applications. I will describe how types are related to
description logics
and ontologies, and give a few ideas (which hopefully spark some
discussion) on how types could be applied to agent dialogues and the
semantic web.