[PRL] the "success" of types

[Matthias Felleisen]

On May 19, 2006, at 11:50 AM, Matthias Felleisen wrote and answers, too:

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

I thought I'd elaborate this point a bit, because it isn't historical 
as I stated.

When you write down Floyd-Hoare invariants, you typical express them in 
a first-order logic whose variables are shared with the program. This 
latter idea works reasonably well for flat values (denotationally 
speaking) but the very moment you have compound values or procedures or 
complex argument-passing protocols (by-name, by-reference, etc) you are 
having problems. (Hint: denotationally these things are higher-order 
values or at least not directly flat values in a reasonably complex 
language.)

The "first-order logic" part causes worse problems, however. If you 
open any book on FH approaches, especially the reasonably popular 
Dijkstra or Gries books, and you read them with an open mind, you often 
see references to uninterpreted symbols in these logical statements. 
"Everyone" knows what they mean: ! is factorial; length(l) computes the 
length of the list; etc. If you wanted to be formal about this so that 
an algorithm can check it, you would write a -- (purely) functional 
program to extend the first-order logic. Only then the meaning of these 
invariant statements becomes clear and unambiguous.

Let me rephrase this: FP is necessary to state invariants in ImpP.

;; ----

Just in case it isn't clear: I am not arguing against stating 
invariants in imperative programming. I am only arguing against buying 
the "types did it all, and nobody else was around" story and dumping 
the functional programming idea.

-- Matthias, don't forget your roots