[PRL] the "success" of types

[Mitchell Wand]

As Matthias correctly points out, the thesis under discussion should be
amended to "Sound type systems are a success story".

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

I find it hard to even analyze this thesis, since I don't know what "it" is
.  Furthermore, the phrase

functional-programming-with-types, even [in] languages that appear to
> require state changes.
>

is insufficiently specific to allow meaningful argument.  If you apply a
little denotational semantics, every programming language is functional ;)


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

Perhaps a better way to make the point is that invariants force the
programmer to think declaratively about the behavior of his or her code.
I'd certainly accept that thesis (though I doubt that it would stand up to
detailed sociological study).

But this has nothing to do with "functional programming."   It is very clear
that Floyd, Hoare, Dijkstra et al thought about invariants as a way of
managing the complexity of state in imperative programs.  (and Floyd and
McCarthy were both at Stanford, if I remember correctly).

Functional programming has to do with expressive mechanism  (remember, we
are about *language*).   How do we specify the channels?  Functional
programming is one way of doing this; Java and imperative programming are
another.  Invariants (whether or not they are expressed through types) are
important for both, and we shouldn't conflate the benefits of
types/invariants with the benefits of functional programming.

Matthias wrote:

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.


but gives no rationale for this leap.

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

Yup.  Types and invariants are important whether your expressive mechanism
uses value-passing or state-modification.  Indeed, this argument makes it
sound like types are even more important for languages that express
themselves "imperatively" than for languages that express their ideas
"functionally".

--Mitch

On 5/19/06, Matthias Felleisen <matthias at ccs.neu.edu> wrote:

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
>
>
>
>
>
> _______________________________________________
> PRL mailing list
> PRL at lists.ccs.neu.edu
> https://lists.ccs.neu.edu/bin/listinfo/prl
>
-------------- next part --------------
HTML attachment scrubbed and removed