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.