[TYPES] types

[Gershom Bazerman]

On 5/12/14, 5:54 PM, Cody Roux wrote:
> [ The Types Forum, 
> http://lists.seas.upenn.edu/mailman/listinfo/types-list ]
>
> As others have noted, tracing historical shifts in points of view is 
> quite difficult. I somehow feel that the "Lawvere" part of the 
> "Curry-Howard-Lawvere-isomorphism" is at the heart of the real shift 
> from a "prohibitive" point of view to a "prescriptive" point of view.
>
Thanks, Vladimir for your very interesting question. It is really a 
shame that (as far as I know) there is not a comprehensive article or 
book that we could turn to on this material. To follow up on the 
"Lawvere part", Goguen and the ADJ group developed initial algebra 
semantics as an algebraic theory of abstract data types in the early-mid 
1970s, directly inspired by Lawvere's work in semantics. Goguen and 
Burstall went on to develop the CLEAR specification language, which 
elaborated these ideas, and as far as I know algebraic data types proper 
were first implemented in HOPE (described in Burstall, MacQueen, 
Sannella, 1980). It seems to me that the shift from data-types-as-hiding 
(the "abstract" notion of modularity) to 
data-types-as-presenting-actions (algebraic data types) is an example of 
precisely that shift from restriction to possibility that we're looking 
for.

(However, I am confused by the reference to "Curry-Howard-Lawvere" as I 
thought the isomorphism proper [via cartesian closed categories] was due 
to Lambek? Is this a mistype, or was Lawvere more involved in that 
portion of the story than I realize?)

In skimming papers looking for ideas here, I ran into a very funny 
counterexample as well. Reynolds' 1972 "Definitional Interpreters for 
Higher-Order Programming Languages" praises Scott semantics as follows: 
"The central technical problem that Scott has solved is to define 
functions that are not only higher-order, but also _typeless_, so that 
any function may be applied to any other function, including itself." 
 From a modern perspective, this of course reads as very strange praise. 
But, I suppose (since I am too young to _know_), at the time it must 
have seemed that being typeless was essential to allowing general 
recursion, higher order functions, etc.

Cheers,
Gershom