[ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]
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
