Home » forums » LtU Forum

What's a definition of "type" that beginners can understand?

I am teaching a large first-year progamming course in Python, and I am curious to know if anyone has any suggestions for a good definition of "type" that would be appropriate for students who haven't yet finished their first programming course.

By Toby Donaldson at 2004-10-23 04:52 | LtU Forum | previous forum topic | next forum topic | other blogs | 19995 reads

Comment viewing options

Select your preferred way to display the comments and click "Save settings" to activate your changes.

Curry-Howard?

If they have mathematical background (we had some on the first year) then "propositions as types" slogan may be good for them. Without even mentioning Curry-Howard isomorphism, it seems quite natural to think of types as of (unary) predicates, and of assertions that such value has such type as of propositions.

Set-theoretic interpretation follows smoothly - one can alternatively interpret types as sets of values that satisfy the predicates.

If one thinks of predicates and sets as different representations of the same, then these definitions coincide.

By Andris Birkmanis at Sat, 2004-10-23 12:07 | login or register to post comments

Well...

What's wrong with the intuitivu meaning of the word? The type is the type of thing. For example, number, string, symbol, truth value, function, or some user-defined type like person, coordiate, polygon, etc.

By inglorion at Sat, 2004-10-23 17:32 | login or register to post comments

Static property

Guaranteed (by the implementation and semantics) to be true at all times.

By Ehud Lamm at Sat, 2004-10-23 17:59 | login or register to post comments

Are you suggesting that type

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

By cdiggins at Wed, 2004-10-27 08:06 | login or register to post comments

Here's a fable by John Reynolds...

...from the introduction to his 1983 paper "Types, Abstraction, and Parametric Polymorphism". I really like it.

Once upon a time, there was a university with a peculiar tenure policy. All faculty were tenured, and could only be dismissed for moral turpitude. What was peculiar was the definition of moral turpitude: making a false statement in class. Needless to say, the university did not teach computer science. However, it had a renowned department of mathematics.

One semester, there was such a large enrollment in complex variables that two sections were scheduled. In one section, Professor Descartes announced that a complex number was an ordered pair of reals, and that two complex numbers were equal when their corresponding components were equal. He went on to explain how to convert reals into complex numbers, what "i" was, how to add, multiply, and conjugate complex numbers, and how to find their magnitude.

In the other section, Professor Bessel announced that a complex number was an ordered pair of reals the first of which was nonnegative, and that two complex numbers were equal if their first components were equal and either the first components were zero or the second components differed by a multiple of 2π. He then told an entirely different story about converting reals, "i", addition, multiplication, conjugation, and magnitude.

Then, after their first classes, an unfortunate mistake in the registrar's office caused the two sections to be interchanged. Despite this, neither Descartes nor Bessel ever committed moral turpitude, even though each was judged by the other's definitions. The reason was that they both had an intuitive understanding of type. Having defined complex numbers and the primitive operations upon them, thereafter they spoke at a level of abstraction that encompassed both of their definitions.

The moral of this fable is that:

Type structure is a syntactic discipline for enforcing levels of abstraction.
By neelk at Sat, 2004-10-23 18:15 | login or register to post comments

Love it

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

By Ehud Lamm at Sat, 2004-10-23 18:27 | login or register to post comments

You're probably right that th

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.

By neelk at Sat, 2004-10-23 19:26 | login or register to post comments

Abstraction

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.

By Ehud Lamm at Sat, 2004-10-23 20:03 | login or register to post comments

I don't think I understand it either

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).

By Dominic Fox at Sat, 2004-10-23 19:38 | login or register to post comments

Thumbs up.

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.

By Frank Atanassow at Sun, 2004-10-24 14:32 | login or register to post comments

The fable is misleading. Both

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.

By cdiggins at Wed, 2004-10-27 08:14 | login or register to post comments

Are big-endian and little-endian ints the same or 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?

By Dominic Fox at Wed, 2004-10-27 11:42 | login or register to post comments

definition plus experience

You can use an intuitive definition such as
  a category of values with common behavior or purpose
that will be a little helpful. Learning what it means will come with experience during the course.

'Type' has a tension for many of us in this forum, because a language like Python does not support attribution of types to expressions. You can point to a part of a program and ask, "Is the type of this function call a number, or a string?" and in Python the answer could be "Sometimes a number and sometimes a string." Type is an execution-time property as far as Python is concerned.

Other languages insist on giving each expression a type. But even in Python it's pretty easy to teach this. When I taught Scheme to my son, I required him to document the type of each function, e.g. "function from list of number to number". It's not hard to grasp, and see that it can be more useful saying that the type is plain "function" (as the Python language would have it).

The earlier-mentioned function call can be given the type "number or string", suggestive of the connection of types with logic. The students would need to distinguish between "Python type" and "logical type".

As for the Reynolds story and abstraction, Python has classes and modules, but I'm unsure how much they are able to hide the implementation details, e.g. of a complex number class. Even so, the programmer can create a class which is understood by its users as a type.

By Scott Turner at Sun, 2004-10-24 03:05 | login or register to post comments

Type definition

A type is a semantic classification of a set of values.

By cdiggins at Sun, 2004-10-24 17:37 | login or register to post comments

Intensionality

The key difference between types and sets is that types carry some intensional information, typically, but not necessarily, indicating what types are for and what manipulations/transformations on types are intended.

The obvious point of difference is empty sets/types: the set of Klingons and the set of even prime numbers greater than 10 are the same, but the types are very different.

By Charles A Stewart at Mon, 2004-10-25 10:51 | login or register to post comments

Quite logically

A similar situation appears in logic - there are many propositions, but all of them can be seen as just names for either true or false (with different mapping between names and booleans for different models).

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 :-)

By Andris Birkmanis at Mon, 2004-10-25 12:45 | login or register to post comments

Sense and denotation

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.

By Charles A Stewart at Wed, 2004-10-27 11:51 | login or register to post comments

Semantic Classification implies Intensional Information

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.

By cdiggins at Mon, 2004-10-25 15:38 | login or register to post comments

Less is more

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.

By Charles A Stewart at Wed, 2004-10-27 11:53 | login or register to post comments

Semantic => Meaning

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).

By cdiggins at Wed, 2004-10-27 16:48 | login or register to post comments

Oops, I meant intensional, not intentional

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.

By Charles A Stewart at Thu, 2004-10-28 08:21 | login or register to post comments

Revisiting the definition of type

"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.

By cdiggins at Sat, 2004-12-04 18:56 | login or register to post comments

Peircian semiotics?

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

By marco at Sun, 2004-12-05 09:49 | login or register to post comments

Saussure's Structuralism?

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 ).

By Jillis ter Hove at Sun, 2004-12-05 18:24 | login or register to post comments

False Analogy

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.

By cdiggins at Mon, 2004-12-06 00:33 | login or register to post comments

A type is a label associated

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;

By cdiggins at Mon, 2004-12-06 00:18 | login or register to post comments

Collection of Methods

How about: a collection of methods (operations) that you can perform on any instance of that type.

For example, with strings you can (1) concatenate one string to another, to produce a new string; (2) take a substring of one string to produce a new string; etc. With numbers, you can (1) add one number to another to get a new number; (2) subtract one number from another to get a new number; etc. [You'd have to refine this to distinguish ints, reals, etc.]

This is why (you say to your students) you can concatenate two strings (say "abc" and "def", to get "abcdef") but you can't add them together. And it is why you can add to numbers (say, 1 and 2, to get 3) but you can't concatenate them to get 12.

This gives you a nice entre for pointing out that addition and concatenation are NOT the same thing (you can't concatenate 1 and 2 to get 12), and also for introducing the topic of type conversion (you CAN concatenate str(1) and str(2) to get "12").

By Stephen Ferg at Mon, 2004-10-25 13:33 | login or register to post comments

ADTs

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".

By Andrei Formiga at Tue, 2004-10-26 15:09 | login or register to post comments

It might just be my mathematical inclination...

I'd just tell them the straight definition.

Which seems to not exist from the disagreement in responses.

Even when a definition is complex, I've always had a better understanding and grasp of what something is when I have the definition. It also halts expending class time on debating whether something does or does not fulfill the definition and instead turns it in to an opportunity to teach how it does or does not fulfill the definition.

Again, that might just be my mathematical inclination and my irritation with a programming class that didn't use definitions and the teacher was generally wishy-washy and imprecise. This caused ambiguity in the appropriate answers to questions on tests and wasted class time. Also, I had taken a more advanced course which required students to unlearn concepts because they were taught them incorrectly and then later had taken this lower course where they taught the concepts incorrectly.

By Bryce Riner at Wed, 2004-10-27 19:30 | login or register to post comments

a straight definition

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"?

By Scott Turner at Thu, 2004-10-28 01:55 | login or register to post comments

Did they take Biology?

If your students have taken biology, what's wrong with using biological taxonomy? Granted, the analogy only works well with simple concepts. However, you're not jumping into structs and pointers at the beginning, right? ;-)

Just don't start with a rigorous definition at the beginning. In my experience, too many teachers think that they need to define everything with complete precision before teaching the concepts. That confuses students too often. As long as they understand those concepts will be refined later, a simpler and easier to understand definition often fufills the purpose. That way, you can focus on the important parts for a particular application.

By Quantum Jim at Thu, 2004-10-28 04:06 | login or register to post comments