[PRL] the "success" of types

[Matthias Felleisen]

Mitch and I had a private discussion. Here is what we agreed on:

1. There are N-2 unsound type systems that aren't a success.

2. There are two major industrial type systems that are safe/sound: 
Java and C#. These also use parametric polymorphism.

3. Both the idea of safety and parametric polymorphism came from FP. 
And FP empowered research on those more than ImpP or OOP.
3a. We didn't agree that Gosling read Milner's paper and therefore 
decided to make Java safe and sound. I think that the type research in 
FP and its application to OOP (esp the attacks on Eiffel's lack of 
safety) created the necessary awareness in the form of a "cultural 
climate."

4. So yes, types for the longest time stood atop the shoulders of FP 
research.

5. GC also leaped from FP to OOP in Java.

6. Very little else has leaped from FP. More type stuff exists that 
could be used. [My own hunch is that these things will evolved directly 
inside of OOP, based on Feather/Middle/ClassicJava. Ownership types 
come to mind.]

I do think it's still fair to say that Mitch wouldn't say FP is a part 
of the success story. I will maintain that w/o functional programming 
we wouldn't have seen the progress in types research that influenced 
the last 10 years.

-- Matthias

On May 19, 2006, at 2:57 PM, John Clements wrote:

>
> On May 19, 2006, at 8:35 AM, Mitchell Wand wrote:
>
>>
>> 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.
>
>
> WARNING: the following synopsis is obvious to Very Smart People (tm).
>
>
> If I understand Matthias correctly, then his claim is this:
>
>
> 1) both functional and imperative programs communicate values between 
> different parts of the program.
>
> 2) in a functional style, this is generally done by passing a value to 
> a function.  In an imperative style, this is often done by putting a 
> value in an existing cell.
>
> 3) You can model functional languages using imperative languages if 
> you see "passing a value" as "putting a value in a fresh cell."
>
> BUT!
>
> In this model, you get a short-lived cell for each parameter, rather 
> than a long-lived existing cell as you might in an imperative 
> language.
>
>
> So what?
>
>
> MF:  Well, type systems allow us to be much more specific about this 
> shorter-lived cell (e.g., using parametric polymorphism).
>
> MW: But invariants can play this same role in an imperative program.
> (is this a correct reading)?
>
> MF : But programmers are too lazy to write down such invariants unless 
> they're forced to, and imperative languages make it easy to just 
> assign a nice wide type to the cell and not worry about it. And that's 
> why most of the recent work on types is motivated by functional 
> programming languages.
>
> End synopsis.
>
> Is this a reasonable synopsis?
>
>
> John Clements
>