Lambda the Ultimate

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?

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.

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 means "types are not unstructured sets". Saying types are sets is "trivially" true considering Set Theory's foundational role.

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.

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.
  

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

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.

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

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

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

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.