Thanks for the several interesting replies. I think I am learning what "lazy" means, but there seems to be embedded in it a presupposition that the order in which new expressions are introduced in a computation is something that one does not carefully plan. It still seems to me to be possible that the developing languages are partly the legacy of an epoch when computational power was qualitatively less than now. I was especially heartened to see the lack of support for St. John's position "in the beginning was the word", especially in view of the recent attempts by physicists to revive that idealist position. Many of us have long instinctively believed that language should fit concepts and concepts should fit reality. Bill ************************************************************ F. William Lawvere, Professor emeritus Mathematics Department, State University of New York 244 Mathematics Building, Buffalo, N.Y. 14260-2900 USA Tel. 716-645-6284 HOMEPAGE: http://www.acsu.buffalo.edu/~wlawvere ************************************************************ On Fri, 20 Mar 2009, Robin Cockett wrote:
Peter Selinger wrote:
I hope that these examples help to dispell the view that untyped languages, or lazy languages, are some kind of "practical hack" invented by programmers and implementors that don't really fit any mathematical model. Or, as Robin put it, "whose relation to standard mathematical settings is surprisingly remote". Actually, the contrary is very much true, and category theory is a large part of the reason. [The same cannot, of course, be said for such languages as C, Fortran, Perl, or Visual Basic, which actually *are* practical hacks with no mathematical model. That is precisely why theoreticians study Haskell or ML or Scheme or the lambda calculus or Agda or Charity and so forth.]
Well I certainly did not intend to imply (or I think say) that lazy functional languages (Haskell) or other strict languages (the ML family) are hacks! Absolutely not -- gosh I would loose my job!!!
Clearly I should be clearer on what I did not say!
For example I should be clear that things "whose relation to standard mathematical settings is surprisingly remote" can be (in fact usually are) extremely mathematical and important to the development of mathematical thought! When I said that producing something from nothing "may be a bit of a shock to a mathematician" this was not saying that, therefore it is not mathematical: the fact that Fermat's last theorem was proven may also have shocked a good few mathematicians who had not expected it. In this case it is a shock in the sense that naively a mathematician may not have considered carefully what setting he was actually in ...
I certainly did want to emphasize the sense in which a program language can be an exploration of a particular perspective (Mathematics by other means). Furthermore, that there is a creative tension between implementation (which, in case anyone thinks otherwise, is -- if done well -- /very/ mathematical: for example in the case of the lambda calculus rests on the now extensive theory of rewriting) and semantics, which I view as prescriptive mathematics (typified by set theory and logic of the 1900s) in which one asserts far reaching axioms hoping madly that they are "right" -- or at least useful.
Computer Scientists probably understand this best as simply the difference between a bottom-up and top-down approach -- played out perhaps on a slightly broader canvas -- and would instantly recognize the importance of both (as I am sure would mathematicians).
Of course, it is nice if the two approaches meet. (And if I did not know Peter better I might think that he is saying that the whole business is nicely sewn up ... nothing could be further from the truth! Of course he didn't say this. It only may have sounded like he did! ;-) )
If you will now forgive me for being a little colorful to reemphasize a point ... (then that is definitely it from me!)
The prescriptive approach, of course, is extremely arrogant: it says "this is what I want" and "this is how the world should be". It was typified by the development of set theory whose the aim was to a pin down exactly what God had intended once and for all. Of course, the real danger to this, much more serious than getting it wrong -- you can always fix that -- is that God is actually playing with a number of settings and hasn't really settled on which one he likes best! The Greeks understood this perfectly 8-) .
This is where Category Theory slips into the picture: it is clearly stupid to study just one setting (unless God makes up his mind suddenly) instead lets just study them all! Now in the process of dredging through God's basement (where he keeps his discarded ideas) it would definitely be rather disheartening if we found the lambda calculus (after all that is where HE keeps his discarded ideas)! So let us suppose that this does not happen ... but that we do find ("hiding under the wreckage of set theory" Paul Taylor quickly adds) a really nice implementable category which has a simple axiomatization and resembles the sort of naive mathematics that everyone uses. Wouldn't it just be tempting to pull it out and implement it anyway? ... and, strictly as a market ploy of course, put about that God had had an off day and had made a mistake?
The point is that even if there is a base computational reality, we are in the altogether strange situation that we don't actually have to accept it! Computation, just like mathematics, is open to prescription. We can still choose to work in more restrictive settings where getting around (in some ways) may be easier (or safer). And this is a important aspect of programming language and semantics research ... in particular, being Turing complete is /not /an absolute requirement of a programming language (it is certainly something which one can ask about a language!).
Far from the semantical/prescriptive approach to computation being dead, it is more alive than ever ... this is not an argument against computability, however, it IS an argument for the important role of Category Theory in Computer Science for helping us to understand the relationship between settings we might want to implement (... on which I think Peter agrees!)
-robin