Summary
My most recent post has sparked some debate. I thought I'd put my money where my mouth is and try to define type.

---

Advertisement

In my latest blog post Authors and Computer Scientists Scared of Definitions? I use the example of the lack of a definition of type in Pierce's book Types and Programming Languages as a source of frustration. As is traditional with online debates I was asked to define type myself (I wonder if film critics are ever asked to make films?).

At http://plato.stanford.edu/entries/type-theory we can get a great primer on type theory from the Stanford Encyclopedia of Philosophy. There is actually a rigorous definitions of type given, which I summarize as follows:

A type is a classification of individuals, propositions, and relations. There are two basic types: i (the type of individuals) and o (the type of propositions). If A₁,...,A_n are types then (A₁,...,A_n) is the type of the n-ary relation over objects of the respective types. Types are used to filter non-legal relations and propositions.

To understand this in simpler terms, realize that a function is a binary relation. So a function from the type T to the type U has the type (T, U). This is written using more modern notation as T->U.

Feel free to discuss!

Talk Back!

Have an opinion? Readers have already posted 8 comments about this weblog entry. Why not add yours?

RSS Feed

If you'd like to be notified whenever Christopher Diggins adds a new entry to his weblog, subscribe to his RSS feed.

Digg | del.icio.us | Reddit

About the Blogger

Christopher Diggins is a software developer and freelance writer. Christopher loves programming, but is eternally frustrated by the shortcomings of modern programming languages. As would any reasonable person in his shoes, he decided to quit his day job to write his own ( www.heron-language.com ). Christopher is the co-author of the C++ Cookbook from O'Reilly. Christopher can be reached through his home page at www.cdiggins.com.