From mboxrd@z Thu Jan 1 00:00:00 1970 X-Msuck: nntp://news.gmane.io/gmane.science.mathematics.categories/180 Path: news.gmane.org!not-for-mail From: Robin Cockett Newsgroups: gmane.science.mathematics.categories Subject: Re: Functions in programming Date: Wed, 18 Mar 2009 20:32:26 -0600 Message-ID: Reply-To: Robin Cockett NNTP-Posting-Host: lo.gmane.org Mime-Version: 1.0 Content-Type: text/plain; charset=ISO-8859-1; format=flowed Content-Transfer-Encoding: 7bit X-Trace: ger.gmane.org 1237470635 12594 80.91.229.12 (19 Mar 2009 13:50:35 GMT) X-Complaints-To: usenet@ger.gmane.org NNTP-Posting-Date: Thu, 19 Mar 2009 13:50:35 +0000 (UTC) To: Bill Lawvere , categories@mta.ca Original-X-From: categories@mta.ca Thu Mar 19 14:51:43 2009 Return-path: Envelope-to: gsmc-categories@m.gmane.org Original-Received: from mailserv.mta.ca ([138.73.1.1]) by lo.gmane.org with esmtp (Exim 4.50) id 1LkIeW-0006Ro-1d for gsmc-categories@m.gmane.org; Thu, 19 Mar 2009 14:51:20 +0100 Original-Received: from Majordom by mailserv.mta.ca with local (Exim 4.61) (envelope-from ) id 1LkHxe-00041g-MP for categories-list@mta.ca; Thu, 19 Mar 2009 10:07:02 -0300 Original-Sender: categories@mta.ca Precedence: bulk Xref: news.gmane.org gmane.science.mathematics.categories:180 Archived-At: I am not sure whether you got a response to this ... here is my attempt. Bill Lawvere wrote: > > Question: Do the various programming languages explicitly > implement the indispensible ingredient of categorical > semantics, that every map has a unique codomain? SO (you are right) the first problem is that usually maps (as a category theorist is thinking of such) are not what is implemented. Functional programming languages, for example, originate from combinatory algebra and the \lambda-calculus ... typing is only really introduced retrospectively as useful sugar on this underlying structure ... what is implemented is application -- or at least a particular rewriting/reduction process of application. A function A -> B is then a just a term which can be typed to be of type A -> B which can be applied to a term of type A to reduce (maybe) to something of type B ... application (as rewriting) is definitely the primitive and typing is retrospective (although very nice and useful). However, at this stage it does /look/ deceptively categorical as one does define f :: A -> B! And, of course that has led people to look at how one might interpret this as actually categorical ... and, of course, thereby hangs a lot of excellent work! However, what emerges is something whose relation to standard mathematical settings is surprisingly remote. Lazy evaluation (mixed with non-termination/partiality) is definitely partly to blame for this ... > > I don't know the technical meaning of "lazy"; was it an > attempt to avoid the processing speed and ram needed to > take account of the composition with inclusion maps, > etcetera? Lazy evaluation is basically a reduction strategy for the lambda calculus. It is a graph reduction strategy (you need a machine model with pointers) which does a "by-name"/"by need" evaluation with sharing of subexpressions which are duplicated in the rewriting process. Sharing arises as in the reduction S x y z => x z (y z) if z is a big structure you don't want to duplicate it so you "share" it ... and this means also you can share any rewriting you do on that structure. In terms of the rewriting steps required on the lambda calculus this reduction strategy is optimal ... however, in storage requirements it is often not optimal (so sometimes a "by-value" reduction will do better under this criterion). One feature of this rewriting technique is that it never looks at subterms which will be eliminated. E.g. in K x y => x the contents of y will never be inspected (as there is apparently no need). Of course, this is all well and good, except, when y had happened to be a term which did not terminate (i.e. had no support) , suddenly now one can produce something very definite from nothing! Of course this is what Miles Gould pointed out with a really simple Haskell program (lovely!). Even if you define the initial type "correctly" you can still write five :: Initial -> Int five _ = 5 and actually get 5 from nowhere! Of course, this really will not seem at all mysterious to a Haskell programmer who will mutter about strictness and bottoms. But it may be a bit of a shock to a mathematician! -robin P.S. Steve Vickers and Stevenson pointed out Chairman Mao plagiarized O:-) : According to the Penguin Dictionary of quotations: Karl von Clausewitz (1780-1831): "War is nothing more than the continuation of politics by other means".