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 A1,...,An are types then (A1,...,An) 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!
A type is a named set of values, where a name is a string over some finite alphabet such as Unicode.
Note that this says nothing about nominal vs. structural typing: "a structure consisting of an integer named 'x' and an integer named 'y'" is just as good a type name as "Point".
Ensuring that all types have names makes sure that there are only an enumerably infinite number of types, since there are only an enumerably infinite number of names.
> A type is a named set of values, where a name is a string > over some finite alphabet such as Unicode.
Does a type need to be a value? At least conceptually, this seems too narrow. I don't think of functions as values but many languages have a function type.
> > A type is a named set of values, where a name is a > string > > over some finite alphabet such as Unicode. > > Does a type need to be a value? At least conceptually, > this seems too narrow. I don't think of functions as > values but many languages have a function type.
I meant, does a member of a type need to be a value?
You might have noticed that the idea of "types" originated from correcting the naive notion of sets ( please also correct the link to the encyclopedia article! ). Instead of defining types intensionally they are defined formally as a filter for ill typed set expressions. Hence they do not simply classify entities ( that's what sets are for ) but they are used to express which terms are created by following certain rules ( type system ). My understanding of types in programming languages is that they constitute a refinement of syntax by semantics. Expressions that are otherwise syntactically correct can be sorted out because they lead to computations that get stuck. "Stuckness" is a part of the ideology of type theorists. Instead of becoming stuck a programmer can accept certain type faults and find meaningfull continuations within the catch-clause of the exception handler - I remember vaguely a polemics by Douglas Hofstadter in GEB about type theory as a desparate manner to lock intelligent beings into the rules of non-reflective formal systems. It takes no wonder that Hofstadter strongly advocated Lisp/Scheme. These days we might be more fascinated by using type expressions as expressions for defining invariants and for purpose of pattern matching.
> > A type is a named set of values, where a name is a string over some finite alphabet such as Unicode.
> Does a type need to be a value?
I actually liked the definition of a named set of values, although some C++ template metaprogramming techniques create new types that don't do anything other than tell the compiler things (like with CRTP: http://en.wikipedia.org/wiki/Curiously_recurring_template_pattern ). I guess you could fudge and say that, as needed, the value might be "null" orthe value may not be contained in the implementation of the type, but rather be out-of-band (that is, the existence of the type in a particular situation is the important information).
> You might have noticed that the idea of "types" originated > from correcting the naive notion of sets ( please also > correct the link to the encyclopedia article! ). Instead > of defining types intensionally they are defined formally > as a filter for ill typed set expressions.
You are right, this is a very pertinent piece of information that should be included in the definition. I have now added "Types are used to filter non-legal relations and propositions.".
...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?).
If all a film critic had to say about "An Inconvenient Truth" was that the film maker hadn't defined "Inconvenient", we wouldn't ask them to make films and we wouldn't bother reading their film criticism :-)
afaict Nothing in your original posting indicated what difficulty the lack of a definition for "Types" caused you in understanding the book. If the lack of definition did indeed cause difficulty then you might provide that example to the author so he can consider the suggestion.
otoh If you simply wish to have a definition of "Types" and were disappointed that the book didn't contain one, maybe you should have checked if it included a glossary before forking-out the $70.
Previous Topic
