Lambda the Ultimate

Are you suggesting that type is any static property that is true at all times?

Great story. I am not sure it will be understood by first-years though.

You're probably right that they won't understand it as a definition, but they can probably understand it as a capstone idea that organizes the concrete examples they've been working with throughout the course.

The idea of type as an interface which can be satisfied by many different implementations is really important for basically all real programming, and one that is a good idea to emphasize from the beginning. Abstraction is really one of the fundamental ideas of programming. A student doesn't need to understand contextual equivalences or parametricity theorems in order to benefit from information hiding, and learning to think about types as interfaces is a very beautiful way of disciplining programming.

I guess it should be obvious from what I wrote here in the past that I have no argument with you about the importance of abstraction.

Is the second professor's account of complex numbers based on polar co-ordinates, or something like that?

(I do remember that the first time I ever encountered the word "isomorphism" it was in the context of a discussion of the relationship between operations on complex numbers and transformation of Cartesian co-ordinates using matrix multiplication).

I'm Frank Atanassow, and I approve this message.

Dominic wrote: Is the second professor's account of complex numbers based on polar co-ordinates, or something like that?

Yes. Descartes introduced Cartesian coordinates. I don't know if Bessel introduced polar coordinates, but it seems that certain Bessel functions are called cylinder functions.

The fable is misleading. Both Bessel and Descartes defined different types. Two types may have the same primitive operations and same representations, and may be used interchangeably, but are still different.

Even "primitive" types may be allowed to have different underlying representations. To give another example: is an ASCII string represented by a null-terminated array of chars the same type as an ASCII string represented by a long giving the length of the string followed by an array of chars with no terminator?

In your example, the sets are the same only in some models, but can differ in others, this is why we say the types are different.

I can easily imagine a world in which the set of Klingons and the set of even prime numbers greater than 10 are very different :-)

PS: this is my interpretation of what I learned from some papers linked from LtU - I might be wrong as I never passed any formal tests on this matter :-)

I sort of agree with this. I don't think it is right to say that propositions are names for truth values, but I would say that it is the normal purpose of propositions to pick out truth-values. This leads into an idea in philosophical logic, which I think is the most important idea in philosophy for computer scientists to be aware of: Frege's distinction between "Sinn" (sense) and "Bedeutung" (denotation).

There's a not-very-good account of this distinction at Wikipedia: sense and reference. I hope to get a chance to begin sorting it out in the next few days.

That is the reason the definition includes the terms "semantic classification". The set in of itself is assigned some arbitrary semantic meaning to differentiate it from other sets that may or may not be precisely the same.

The analogy is in natural language some word sets can only be classified according to the semantic context.

I think type is even more general than that: I don't think the intentional information need even be meaningful; there need be nothing "semantic" about it at all. It can be a label or a colour, if you like.

This isn't a trivial point: I think the concept of type is even more fundamental than the concept of semantics.

Intentional information by definition implies meaning. The definition of mean is "To be used to convey". In the case of intentional information, what is conveyed is intent.

Nonetheless, you are implying that a type be used to categorize without meaning? A type devoid of all meaning would be a completely arbitrary set of values, and would have no use in a software program. This would be simply a set of values, and not a type in any meaningful sense (pun not-intended).

My mistake: I meant intensional (ie. not extensional, ie. something over and beyond what members there are), and not intentional, in my last post.

This would be simply a set of values,

No, if it were then the notion of set and type would coincide. What distinguishes the notion of type from set is that there is more to it than its membership condition. I agree that the notion of type only becomes interesting when that additional information is meaningful, but even in the other case, at its most general, I would still count it as a type.

There are lots of definitions of type running around in this forum. I think a post (or maybe an article linked to by a post) setting them all out and explaining their interrelationships would be a good thing.

"What distinguishes the notion of type from set is that there is more to it than its membership condition."

I agree.

"I agree that the notion of type only becomes interesting when that additional information is meaningful, but even in the other case, at its most general, I would still count it as a type."

Any information by defintion would make the type meaningful. The meaning is the information that is conveyed.

The American Heritage® Dictionary of the English Language defines meaning as "Something that is conveyed or signified; sense or significance." which for me clearly encompasses all information, whether it be intensional or extensional.

I think of a type as a label. The best explanation I can give of a type is in terms of Peircian pragmatism/semiotics (study of signs, an old hobby which I am blatantly going to misrepresent below) which distinguishes between:

1. the sign, that would be the label (of an expresssion)
2. its object, that would be its meaning (say set-theoretic, or structured bits)
3. and its interpretant, well I guess that would be us.

The discussion seems to involve mostly 1 & 2, where most people (3) have different interpretations (2's) associated with type (1).

However, since types can be studied as a theory of labels (say meaningless structures associated with other structures), I would say the best definition of a type would be label (of something).

A type is a label associated with a structure; the label may have meaning.

Cheers, Marco

The swiss linguist Saussure approached texts in a very analytical manner. He fathered, the mostly french movement, of Structuralism: http://en.wikipedia.org/wiki/Structuralism

Saussure divides language into 2 component-parts. When I write the word dog it produces the inscription dog, but also the concept or mental image of a dog: a four-legged canine creature. He calls the first the signifier and the second the signified. Together ( like 2 sides of a sheet of paper or a coin ) they make up the sign. He then goes on to argue that the relationship between signifier and signified is completly arbitrary. The word dog for instance has no dog-like qualities whatsoever, there is no reason why the signifier dog should produce the signified: a four-legged canine. The signifier dog could just as easily produce the signifier: a four-legged feline. On the basis of this result he the argues that therefore the meaning is not the result of an essential correspondence between signifier and signified, it is rather the result of difference and relationship.

Based on Saussure's ideas i think of variables as being sign's. A variable's constituents are therefore a signifier and a signified, with the signifier being the type ( and by default the signified the value ). A signifier can be a structured definition in other sign's or signifier's. This is needed, for example, to produce the term: a four-legged canine. Four-legged and canine are also complex structures of meaning and value.

Maybe it would have been easier to say that things in programming languages that can denote values will have descriptions of what those values are. This is what i call a type. But these signifier's are not defined in equalities with the signified. But a type is marked as being so in respect to All other current types within "it's system". This also holds for the signified's ( or value's ).

Based on Saussure's ideas i think of variables as being sign's. A variable's constituents are therefore a signifier and a signified, with the signifier being the type.

This is a false analogy. Not all values are variables. Not all values are typed. Not all types have values.

But these signifier's are not defined in equalities with the signified. But a type is marked as being so in respect to All other current types within "it's system". This also holds for the signified's ( or value's ).

Computer science has types and values, not signs, signifiers and signifieds. Why confuse the point by introducing language from an entirely unrelated field of study, i.e. linguistics.

A type is a label associated with a structure; the label may have meaning.

A label conveys information, therefore it has meaning by the definition of the word "meaning", i.e.
something that is conveyed or signified;

You described a definition for ADTs (Abstract Data Types). The operations on the type are emphasized, and the representation is de-emphasized. I believe that's interesting to consider the representation of some types, so I wouldn't use that as a general definition for "type".

For a straight definition, Pierce's textbook defines type system rather than type. A type system classifies phrases of a program statically, without running the program. In this context, a classification is called a type. Thus, "type" doesn't have a standalone definition; it would be like defining "scalar" without learning vectors.

However, given that they're using Python for the class, one would not expect them to be learning type systems with mathematical rigor. If that's the case, I don't see harm in providing an intutive definition of "type", as long as the teacher doesn't present it as if it were cast in concrete. Do we consider geometry students handicapped because they arrive for the course with a preconceived definition of "line"?