Summary
Have you ever noticed how most text when discussing computer sciences concepts fails miserably to properly define the terms they discuss?
Advertisement
I am always frustrated by how hard it is to find good definitions for concepts in computer science. Is is because people are too scared to commit to a single definition? Is it because it's too hard?
Here is the most recent example I came across from Stack Computers the New Wave, an old textbook online about stacks:
1.2 WHAT IS A STACK?
LIFO stacks, also known as "push down" stacks, are the conceptually simplest way of saving information in a temporary storage location for such common computer operations as mathematical expression evaluation and recursive subroutine calling.
It's a book about stacks, and he couldn't even provide a satisfactory definition of stacks. Here are the logical problems with his definition:
He doesn't even try to define a stack, he starts by defining a "LIFO stack".
He doesn't say what it is, he says that it is the best way of doing fubar.
This fubar that he claims LIFO stacks are best at, is only a tiny example of what stacks are good for.
However the most frustrating lack of a definition I have found is in the most recent book purchase I made, Types and Programming Languages by Benjamin Pierce. This guy is quoted left, right and center to me by various "type theorists", but he fails to define in his $70 book what a "type" is. Instead he defines what a "type system" is. How can you define a system of fubar, without defining the fubar? I find that unacceptable. I demand that computer science authors and scientists define their terms clearly and unequivocally.
I am not sure what motivates this failure to define things, but I suspect it may be fear. If we define something, then somebody else can come along and actually prove us wrong, but if we done't define something then we can always modify our definitions as we go.
he fails to define in his $70 book what a "type" is Does he define what a Programming Language is?
I demand that computer science authors and scientists define their terms clearly and unequivocally Lead by example!
"24.1 What Are Types? A type is any property of a program that we can establish without executing the program." p239 "Programming Languages: Application and Interpretation" http://www.cs.brown.edu/~sk/Publications/Books/ProgLangs/
> he fails to define in his $70 book what a "type" > is > Does he define what a Programming Language is?
Not that I noticed ... but for some reason I feel more lenient about that. Programming language is arguably self-defining: a language for defining programs.
> I demand that computer science authors and scientists > define their terms clearly and unequivocally > Lead by example!
What, you mean stop whining and start doing? ;-)
Actually, I have actually started work on a rather ambitious book, the working title is The Fundamentals of Programming, which will make a fair attempt at defining basic computer science terms. I plan on making it freely available online.
> "24.1 What Are Types? > A type is any property of a program that we can > establish without executing the program." > p239 "Programming Languages: Application and > Interpretation" > http://www.cs.brown.edu/~sk/Publications/Books/ProgLangs/ > > That's kind-of interesting ;-)
That is interesting, but overly broad to serve as a useful definition. Types are most interesting when looking at the expression level which is not obvious from that definition. Krishnamurti however goes on to say:
"A type labels every expression in the language, recording what kind of value evaluating that expression will yield. That is, types describe invariants that hold for all executions of a program. They approximate this information in that they typically record only what kind of value the expression yields, not the precise value itself."
This I think is a decent definition of what a type is as far as modern static type theory goes. There are still some weaknesses, for instance even though a type is a set of values it is not neccessarily an approximation. It is a rather precise representation of a set of possible values.
Dynamic typing is also overlooked of course, but that is not uncommon. Type theorists for the most part dismiss all forms of runtime tagging of values as being facile or as one fellow put it to me "merely a syntax of values" (translation: not worth calling a type).
Remember, Diggins is now working at Microsoft as a technical writer. Something tells me that (and working on the C++ Cookbook) has a lot to do with how he views documentation nowadays.
As for the quesiton of why definitions are hard to come by, I've always thought it was an example of lazy evaluation in the real world. Don't compute the definition until you're sure you need it; alowing you to explore the question with fewer preconceptions. Of course, (1) you'd expect somebody writing a book to have gotten around to computing that definition, and (2) this lazy evaluation leads to a lot of misunderstandings because of the fudge factor involved.
> Not that I noticed ... but for some reason I feel more > lenient about that. Programming language is arguably > self-defining: a language for defining programs.
Your outrage is starting to seem a little whimsical - perhaps the author judged that someone picking up a heavy-weight expensive tome titled "Types and Programming Languages" would have some notion what was meant both by "Types" and by "Programming Languages".
> > I demand that computer science authors and > scientists > > define their terms clearly and unequivocally > > Lead by example! > > What, you mean stop whining and start doing? ;-)
For example, your definition of types.
-snip- > That is interesting, but overly broad to serve as a useful > definition.
Apparently it's a useful definition for Krishnamurti's purpose, whether it's a useful definition for some purpose you have in mind is a different matter.
-snip- > Dynamic typing is also overlooked of course, but that is > not uncommon. Type theorists for the most part dismiss all > forms of runtime tagging of values as being facile or as > one fellow put it to me "merely a syntax of values" > (translation: not worth calling a type).
Is it possible you're being a little hasty in that judgement? Have you fully assessed "Programming Languages: Application and Interpretation"?
It seems a bit unlikely to me that a book which introduces PL features by implementing interpreters in Scheme would overlook dynamic typing. Maybe it depends on your definition of types :-)
Now if its a bun fight you really want, have a look at the Computer Science definitions on Wikipedia. Especially interesing reading is the history of changes and the discussion pages - some of those are quite hillarious.
However, I tend to agree that a lot of 'serious' texts fail to either define their terms, or define them in such a way as to be hard to understand or simply wierd.
I'm glad I'm not the only one who noticed this. The less they define, the less you have anything concrete to argue against. In the computing world, this is critical for most theorists.
I think a type is the interpretation of data. By interpretation, I mean how the data in question is to be used along with what operations are valid on it.
I find 'int' is not really a type. What is it? A number, ok? But what is it used for? Is it a distance, pixels, socket number, etc? If that were also defined, then it'd be more of a true type, IMNSHO. Classes don't qualify because the members don't tell anything to the compiler. You can overload operators, but it's an ad-hoc solution.
I agree with Chris on this issue. It's erroneous to assume that a reader has the same understanding of what is meant by a core concept within a text you have written, within reason. There a many terms in computer science which have different meanings to different people.
I am not sure what motivates this failure to define things, but I suspect it may be fear. If we define something, then somebody else can come along and actually prove us wrong, but if we done't define something then we can always modify our definitions as we go.
When I read through the book, I didn't notice the lack of a definition for what a "type" is. Examples are often much more illuminating than examples and I think that a rigorous definition at the beginning of the book would not have been useful. The book's structure seemed, to me, well optimized for education.
I'm not sure why I didn't notice the missing definition and you did, but I suspect it may be you were reading the book with a more confrontational attitude. Now that's not necessarily a bad thing, but I think that optimizing the book to withstand such confrontation would have made it less valuable to a reader like me.
> "A type is any property of a program that we can > establish without executing the program."
I know it's subjective but that looks like a pretty concise definition to me.
> "A type labels every expression in the language, > recording what kind of value evaluating that expression > will yield. That is, types describe invariants that hold > for all executions of a program. They approximate this > information in that they typically record only what kind > of value the expression yields, not the precise value > itself."
I'm not intending to be critical but... This definition describes type usage rather than what a type is. I don't think the definition of a type should prescribe the way it is used.
In addition, either the first or second sentence is redundant, since the second sentence is a reiteration and clarification of the first. The third sentence includes the word "approximate" in such a way as to imply a type's descrition of an invariant is incomplete is some way. Also, the word "typically" in that sentence implies that the whole definition is incomplete by implying there are other undefined 'atypical' types.
> > "A type is any property of a program that we can > > establish without executing the program." > > I know it's subjective but that looks like a pretty > concise definition to me.
Doesn't that depend on how you define 'property'? I would say 'halts' is a property of an application that can be determined without executing the program.
> I agree with Chris on this issue. It's erroneous to assume > that a reader > has the same understanding of what is meant by a core > concept within > a text you have written, within reason. There a many terms > in computer > science which have different meanings to different people.
That's why Pierce doesn't give a definition of what types really are ( a type ontology ) but presents a short motivational introduction and moves on to deal with types formally. This is a typical mathematical style where hemeneutic strategies are excluded and only hints are provided what all the fuzz is about. The adaequacy of this approach depends of course on how language designers deal with their own understanding of "types" and type-check/inference algorithms and whether they make progress. For instance the relationship between expressions and runtime tags in dynamically typed languages is far from being clear or explored in depth. One might just wonder about this omission.
> However the most frustrating lack of a definition I have > found is in the most recent book purchase I made, <i>Types > and Programming Languages</i> by Benjamin Pierce. This guy > is quoted left, right and center to me by various "type > theorists", but he fails to define in his $70 book what a > "type" is. Instead he defines what a "type system" is. How > can you define a system of fubar, without defining the > fubar? I find that unacceptable. I demand that computer > science authors and scientists define their terms clearly > and unequivocally.
I was thinking about this and I'm not sure it's correct that you cannot define a 'fubar system' without first defining a 'fubar'. Can you define 'word' without defining language? Isn't a language basically a 'word system'?
However the most frustrating lack of a definition I have found is in the most recent book purchase I made, Types and Programming Languages by Benjamin Pierce. This guy is quoted left, right and center to me by various "type theorists", but he fails to define in his $70 book what a "type" is. Instead he defines what a "type system" is. How can you define a system of fubar, without defining the fubar? I find that unacceptable.
A type is something that is defined by a type system. Every type system defines its own notion of type. There is no formal definition of type outside of a type system.
> > > "A type is any property of a program that we can > > > establish without executing the program." > > > > I know it's subjective but that looks like a pretty > > concise definition to me. > > Doesn't that depend on how you define 'property'? I would > say 'halts' is a property of an application that can be > determined without executing the program.
Yes, it is a very inclusive definition, possibly too inclusive. So, as you've pointed out, you could legitimately say that there are two types of program, those that halt and those that don't. I think that that's a valid interpretation of the definition. A useful interpretation? I couldn't say.
Flat View: This topic has 53 replies
on 4 pages
[
1234
|
»
]
Previous Topic
