[PRL] the "success" of types

Matthias Felleisen matthias at ccs.neu.edu
Fri May 19 10:37:21 EDT 2006


Mitch made fun of my challenge to the holy gospel of "types are a 
success story" at the beginning of Viktor's talk. While I considered 
discussing this with him privately, I think a "public" discussion will 
benefit everyone else more.

My thesis is simple: it isn't so much a success of types but of 
functional-programming-with-types, even if this happens in languages 
that appear to require state changes. As such, "types are a success" is 
demeaning to the functional half, which I consider far more important 
than the type half.

Arguments:

1. C++ has a type system. I consider this type system deceitful. It is 
at best insidious, misleading programmers into thinking that something 
(some part) is correct about their program.

2. Argument 1 forces us to rephrase the point as "safe type systems are 
a success story."

3. But even this isn't enough. It is easy to imagine Pascal without 
variants and with garbage collection. Indeed, for all I know, some 
successors did so. I have no doubt that this kind of language is only a 
minor improvement over the untyped version.

4. Why? Types encode invariants and type systems check them (possibly 
with some inference). The richer the type system, the more we know 
about the program. This works really well when your communication 
channels are described with rich types because computation really is 
the communication of values from one place to another.

4a. In a functional language/program, the channels are completely 
explicit even for the smallest unit of abstraction: a function. Your 
types say what comes in; your result types say what comes out. You can 
check this. And over the past couple of decades we have learned that 
it's easy to communicate even polymorphic values along those channels.

4b. In an imperative world. your programs tend to communicate values 
via imperative channels (boxes, fields, state variables). It is only 
when we learned to communicate non-trivial values via these channels 
(i.e., objects) that types began to play some decent role here.

BUT, to this day, we don't communicate values with polymorphic types 
(i.e., ('a -> 'b)) via such channels; we stick with ground values.

Furthermore, I would argue that when you begin to send complex objects 
via imperative channels, you're beginning to approximate ML and Scheme 
from the 1970s, the kind of functional programming that I have in mind.

In summary, reasoning about the flow of values is what programmers do. 
When channels are "obvious" for abstractions, it's easy to reason (and 
statically analyze); when channels are implicit and long-distance, it 
becomes hard. This is all about functional programming at least as much 
as it is about types.

Attributing the success to types and not to a move to a more 
applicative style of programming is selling short your history and your 
parentage.

-- Matthias







More information about the PRL mailing list