[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