[PRL] the "success" of types

[Matthias Felleisen]

[I have re-ordered Mitch's response and my response to him a bit. The 
;;; --- markers show where I moved up a segment.]

On May 19, 2006, at 11:35 AM, Mitchell Wand wrote:

> As Matthias correctly points out, the thesis under discussion should 
> be amended to "Sound type systems are a success story".  
>
>> 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 . 

Well, excuse my poor English. I thought "it" standing for "checking 
invariants for the programmer and finding bugs" was an obvious 
implication.

;;; ---


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

!!!!!!!!!!!!!!!!!!!!!!!!!ABSOLUTELY!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!

Their programming is so messed up that they need it much more than FP. 
Because it is so much harder to state/check invariants in ImpP, the FP 
types approach succeeded earlier. It is FP that enabled the success of 
type checking. Thanks for setting the argument up in a historical 
perspective.

;;; ---


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

That's of course bogus and not worthy of consideration. [It's almost as 
bad as discussing syntax.]

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

Okay.

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

1. McCarthy's work on "functional reasoning" predates 
Floyd-Hoare-Dijsktra by years. I can dig out his 1961-1963 papers.

2. So why has the checking of invariants been such a massive failure in 
imperative languages? Programmers have neither taken to writing down 
invariants; reasoning out their programs with wp, sp, wlp or other 
things; proving them correct with fancy pens etc.

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

I can't follow the argument.

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

1. I accept "impure functional programming" in the words of FP-zealots.

2. I also believe that mostly-functional but imperative when you need 
it is something that the FP people developed and that is the foundation 
of the "success" story.

3. Alan Kay writes that he wanted this form of programming for OO 
Smalltalk, but he didn't do it and didn't achieve it.

4. When this style of programming started leaping into mainstream 
languages (and will continue to move over), type checking there started 
to make sense.


-- Matthias