Types vs classes: what is the difference?

In the context of programming languages, why distinguish types and classes? People seem to use these two terms interchangeably. Is this because there is no or little difference, or this is by mistake?

Comment viewing options

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

Constructor ?

As far as I can tell, a class is exactly the combination of a type, a (possibly trivial) constructor and optionally a subtyping relation.

Of course, in OOP languages, classes are types, while most types are not classes. In pure object languages, by opposition (e.g. Smalltalk, Scala, perhaps Python), every type maps to a class.

So, why do people confuse types and classes ? Probably because in Java, it's easier to explain first that both are the same and only later to distinguish between primitive/unboxed types and classes/boxed types.

Sets and Types?

somewhat relevant... what is the difference between types (in programming languages) and sets (in mathematics)?

if my guess (that every value has a unique type but classes destroy that via subtyping) is correct, what is the difference between classes and sets?

Subtyping vs. Subclassing

There is an interesting reading Subtyping vs. Subclassing.
It shed some light for me on the subject, and I think there is a connection with math too. I personally think of types as of sets of values. That's why in my opinion classes are not types, because they defined by behavior. So can anybody please confirm this?

Types are not sets

While you could design a language in which types are sets (see the old Ontic thread), the two are not identified. Andreas Rossberg said it the best: "types are formulas in a logic, not sets", where the logic is the type system of the language we are talking about. Classes are types. In fact, the most important quality of any type is its behavior.

Types are not sets?

Doesn't that need to be stated more carefully? If you take the set of all constructible values in some polymorphically typed language (this will be a countable set), then you can identify each type with the subset of values of that type. In this construction, types are sets. It is true that the type of functions from type A to type B will not consist of the set of all functions from set A to set B (certainly not if A is infinite), but "types are not sets" seems like an oversimplification. That there is not a trivial interpretation of types as sets seems expected since since you can construct the "function" f x = not (f x) in many languages.

"types are not sets" usually

"types are not sets" usually means "types are not unstructured sets". Saying types are sets is "trivially" true considering Set Theory's foundational role.

I assumed the statement

I assumed the statement "types are not sets" was supposed to mean "arrows between types do not correspond to arrows in the category of sets and therefore the category of types is not the category of sets." The reason I was objecting to that abbreviation is that I think it is reasonable to think of types as sets of values. The only caveat is that not all functions between sets are themselves values (if there are other caveats required, I'd love to find out about them). Yes, all sorts of things can be constructed from sets, but it's usually not such a simple construction.

Types are more than just sets

Problems of the types-as-sets-of-values view are at least:


  • It does not easily scale to less trivial type systems: for instance, polymorphic types have no direct set-theoretic interpretation (for impredicative polymorphism, the sets-of-values interpretation would violate well-foundedness).

  • It totally ignores crucial notions like abstract types and similar concepts of user-defined types, which is what makes most type systems interesting in practice.

  • It also cannot explain richer uses of type systems where types are used to express properties of programs, e.g. via dependent types.

The slogan "Types are not sets" was the title of a 1973 POPL paper by Morris, which discussed the second point.

Types as sets

I was going to reply to you in another thread in which you pointed back to this post, but I think it's easier just to reply here. I'm working on a system in which types are annotations which denote set membership. I tend to not be particularly careful in using the term "type" to refer to either the annotation or the denoted set of terms. So in that sense, a type is more than a set in my system - the annotation can be used to drive inference or implicit value selection. But I think your objections to types as sets are deeper than that, and I don't really agree with them:

Your bullet one, I guess refers to the Reynolds result that polymorphism is not set theoretic. I haven't looked at the paper yet, but the abstract says the result is that the usual set theoretic model for the simply typed lambda calculus cannot be extended to a set theoretic model of a system with impredicative polymorphism. The slogan I'd prefer to extract from that result is not "types are not sets", but rather "computations are not functions." Consider the untyped lambda calculus. Clearly /\ != /\ -> /\, if -> means the set of all functions.

For your second bullet to be a problem, you must assume that it's the job of types to enforce abstraction. As I've indicated elsewhere, I don't believe this is the only option. Theories that specify the relationships between types and values in a module do a fine job of abstraction. User defined types can be constructed locally and then exposed through a theory that exposes only their visible properties.

I don't understand your third bullet. What program properties can't you express as membership in an appropriate set?

Hopefully I'll have a write-up of the system I'm building sometime soon, if I can get some time.

What program properties

What program properties can't you express as membership in an appropriate set?

I suppose I must ask: to which terms do you apply the 'type' annotations? If you mean value terms (by which I mean: things you can assign to a variable), then I do not see how you can express any of the following as set-membership:

  • Linear typing. (Substructural typing in general, though linear typing is certainly the favorite example.)
  • Dataflow security typing for information assurance, including types used in zero-knowledge proofs of security properties. This may also include proper ADTs, and sealed values (sealer/unsealer).
  • Effect typing, which describes how a value is obtained or constructed rather than the value itself.

OTOH, if you mean to say that the 'terms' so annotated describe the program-expressions rather than values, then I believe you should be careful about clarifying this. Andreas's objection was to "types-as-sets-of-values". Not many languages have first-class everything to the degree you can assert that arbitrary program-expressions are values.

Oops

Yes, I was overly broad in that question - I was particularly interested in the "e.g. dependent types" aspect of his comment. I have a different story in mind for substructural types and the like, and agree there are some properties of programs that aren't just about sets of values.

Re: Types as sets

The slogan I'd prefer to extract from that result is not "types are not sets", but rather "computations are not functions." Consider the untyped lambda calculus. Clearly /\ != /\ -> /\, if -> means the set of all functions.

"Computations" are not the issue -- you can give a straightforward set-theoretic model for the simply-typed lambda calculus. The issue indeed is (impredicative) polymorphism, whose natural interpretation would be the function space mapping [edit: the set of all] (interpretations of) types to (interpretations of) types -- yielding a cardinality inconsistency, because these functions have to be types, too. You can work around that in several ways, e.g. using domain theoretic models or stratification through step indices, but then types are no longer sets of values.

For your second bullet to be a problem, you must assume that it's the job of types to enforce abstraction.

Well, in most typed languages it is (part of) their job. That is not saying that abstraction cannot be achieved in other ways, but that's besides the point w.r.t. the majority of languages, and types as a general concept. (I also happen to think that types should be used for abstraction, but that's equally besides the point. :-) )

Theories that specify the relationships between types and values in a module do a fine job of abstraction.

Maybe I misunderstand what you are saying, but module theories are type theories, so how do they affect anything?

I don't understand your third bullet. What program properties can't you express as membership in an appropriate set?

Admittedly, I don't remember what exactly I had in mind when I wrote this, but it probably was more about giving a set-theoretic interpretation to something like dependent types, which may be "even harder" than for polymorphic types.

[Edit: plus, of course, what David said. ;-)]

Re: Re: Fwd: Re: Types as sets

"Computations" are not the issue -- you can give a straightforward set-theoretic model for the simply-typed lambda calculus.

I assume the model of STLC that you're talking about interprets "A -> B" as the set of all functions from set A to set B. When we try to model polymorphism as set theoretic, and fail, I'd rather put the blame on this assumption that every set theoretic function should be a valid computation than on the assumption that types are sets.

whose natural interpretation would be the function space mapping

That's an interpretation, but I don't think it's the right one. In the types as sets approach we want to classify untyped terms into sets according to which properties they have. Well, the model for untyped lambda calculus is not a set theoretic function space, because of those cardinality issues you mention. So if the goal is to reason over arbitrary computations, that's a non starter.

Maybe I misunderstand what you are saying, but module theories are type theories, so how do they affect anything?

I'm afraid I'm probably botching the established lingo. I just mean that you can specify the theories that entities satisfy as a way of encapsulating details.

but it probably was more about giving a set-theoretic interpretation to something like dependent types, which may be "even harder" than for polymorphic types.

I think that it's not particularly harder. I'll try to post a writeup of my setup sometime soon.

I'm not so sure...

... but it seems like that article makes a specious argument. Basically (as I read it) the main thrust is that subclasses may typecheck correctly in the language but fail to respect the interface contract of the superclass. This isn't a problem that directly relates to implementation inheritance, or to equating inheritance and subtyping.

The notion of type signaturess in the language the author picks (C++) doesn't include invariants on the types or pre/postconditions on functions/methods. As a result, the language can't statically check that the (implicitly described but not explicity specified to the compiler) contract is being satisfied by the subclass. Clearly if class invariants and pre/posconditions aren't part of your language's type system, then its type checker isn't going to catch it for you when you violate them.

The author seems to be anticipating that argument by saying that they had written tests to confirm that the CBag class obeyed its contract, and that the CSet class initially passed those tests. They demonstrate that adding a new test (by way of making an old test use the interface in a different way) shows a failure of the CSet class to satisfy a CBag invariant. This, to me, seems to point to the inadequacy of the initial test suite to check the desired contract. CSet obeyed the contract that was being checked for at the time it was implemented; adding to the contract after the fact is not fair play.

Having your language be incapable of statically checking some interface contract has *nothing* to do with implementation inheritance. I can define a instance of, say, the Monad typeclass in Haskell that typechecks according to the definitions of Monad but doesn't objey all of the monad identities -- no implementation inheritance required.

Both words are used equivocally

In Haskell, for example, "class" means "class of types". Attempting to aggregate all the various mathematical and informatical uses of the terms "set", "class", and "type" into three universal categories, and then asking how these categories interrelate, is like trying to distinguish beer, properly so called, from ale, properly so called. Go have one instead.

Classes are factories

Most of the type-challenged languages found in the mainstream tend to mingle the two together. But conceptionally, they are rather orthogonal: classes are factories for objects, while types describe the properties of objects (in OO usually the set of messages they understand). Note in particular that classes are found in many untyped languages.

See OCaml for an example of a typed language that properly separates these concepts. There, typing and subtyping are completely independent of classes and subclassing. Classes are merely a convenient - but not exclusive - way to create objects (and declare type abbreviations). Subclassing gives you code inheritence, while subtyping is fully structural "interface inclusion".

These terms are language-dependent

They don't have a fixed, language-independent meaning, although of course their uses in various languages are related.

Look in "The Theory of Classification" by Tony Simons

IMHO, Tony gives a good explanation on what is type and what is class.
http://lambda-the-ultimate.org/node/1332

Alternative theory of classificaton

At one time I was impressed with Formal Concept Analysis which is refreshingly different from OOP ideas. Take for example classification of living things. Suppose you play biologist (botanist) role and are asked to classify some species. You just list them all together with their properties in a matrix, then check mark each object against corresponding properties. If you do that in context explorer software (free) it would output a nice hierarchy of classes.