tag:blogger.com,1999:blog-11295132.post1951702690940196029..comments2018-02-12T01:50:07.787-08:00Comments on A Neighborhood of Infinity: How many functions are there from () to ()? (Updated)Dan Piponihttps://plus.google.com/107913314994758123748noreply@blogger.comBlogger19125tag:blogger.com,1999:blog-11295132.post-35583612515019932852008-02-15T10:26:00.000-08:002008-02-15T10:26:00.000-08:00yin,In Haskell, every type has a _|_. But in a co...yin,<BR/><BR/>In Haskell, every type has a _|_. But in a completely lazy context, \x -> _|_ is indistinguishable from _|_. So I do mean 3, not 4.sigfpehttps://www.blogger.com/profile/08096190433222340957noreply@blogger.comtag:blogger.com,1999:blog-11295132.post-11285444867329214342008-02-14T23:28:00.000-08:002008-02-14T23:28:00.000-08:00I guess you can safely remove the line:* 3 in a la...I guess you can safely remove the line:<BR/><BR/>* 3 in a lazy language like Haskell when working completely lazily<BR/><BR/>So it looks more consistent. Because even we use `seq', Haskell is still a lazy language. It doesn't change at all with the way we use it. _|_ is an inhabitant of ()->(), just like _|_ is an inhabitant of any type.Yinhttps://www.blogger.com/profile/09057963026824934993noreply@blogger.comtag:blogger.com,1999:blog-11295132.post-65627791018378106652008-02-14T08:04:00.000-08:002008-02-14T08:04:00.000-08:00Great post, I never realized the complexity in suc...Great post, I never realized the complexity in such simple functions. But I managed to write an f4:<BR/><BR/>import System.IO.Unsafe<BR/>import Control.Exception<BR/><BR/>f4 x = unsafePerformIO $ Control.Exception.catch (evaluate x >> return loop) (\_ -> return ())<BR/><BR/>f4 loop does equal (), but f4 () will throw an exception (usual bottom behaviour) only if loop has already been evaluated, otherwise it goes into an infinite loop and never returns. Your f3 has this strange behaviour as well...but I guess they are both _|_?monadinousnoreply@blogger.comtag:blogger.com,1999:blog-11295132.post-23853238111688092992008-02-10T18:05:00.000-08:002008-02-10T18:05:00.000-08:00Olivier,My definition of monotone appears to agree...Olivier,<BR/><BR/>My definition of monotone appears to agree with the computer science literature I have at home. But I agree, it's different from what a mathematician would say.sigfpehttps://www.blogger.com/profile/08096190433222340957noreply@blogger.comtag:blogger.com,1999:blog-11295132.post-54807553822488340712008-02-10T18:01:00.000-08:002008-02-10T18:01:00.000-08:00Lot of useful feedback. When I get a moment I'll a...Lot of useful feedback. When I get a moment I'll add some corrections in response. This really is a minefield of a topic even though it seems to trivial!sigfpehttps://www.blogger.com/profile/08096190433222340957noreply@blogger.comtag:blogger.com,1999:blog-11295132.post-61093685760354889162008-02-10T00:20:00.000-08:002008-02-10T00:20:00.000-08:00Now all you need to do is addamb :: () -> () -> ()...Now all you need to do is add<BR/><BR/>amb :: () -> () -> ()<BR/><BR/>amb p q executes p and q in parallel, and terminates just as soon as either one of p and q terminates<BR/><BR/>Note that with amb, it's possible to execute an infinite number of expressions in parallel to see whether at least one of them terminates. You just give half the processor time to the first, one quarter to the second, one eighth to the third etc. But one cannot verify that they all terminate, one can only do that for a finite number of expressions.<BR/><BR/>Hmm, logical "or" over infinite sets, logical "and" over finite sets. Smells like some kind of topological space...ashley-yhttp://ashley-y.livejournal.com/noreply@blogger.comtag:blogger.com,1999:blog-11295132.post-10203613814324136582008-02-09T20:23:00.000-08:002008-02-09T20:23:00.000-08:00Your functions fx remind me my domains and categor...Your functions fx remind me my domains and category when we where trying to find models for PCF, parallel PCF, the definition of parallel-or...<BR/>Haaa.Axioplasebakarika.netnoreply@blogger.comtag:blogger.com,1999:blog-11295132.post-72869851790671920642008-02-09T17:33:00.000-08:002008-02-09T17:33:00.000-08:00Your definition of monotone is deviant: a monotone...Your definition of monotone is deviant: a monotone function is one that does not change direction, no more no less: it can be monotonely increasing or monotonely decreasing. Furthermore with just 2 points all functions are monotone anyhow.Oliviernoreply@blogger.comtag:blogger.com,1999:blog-11295132.post-58404258387857246172008-02-09T13:47:00.000-08:002008-02-09T13:47:00.000-08:00That's a nice post, Dan.To go on a little further,...That's a nice post, Dan.<BR/><BR/>To go on a little further, "Tis a maxim tremendous, but trite" (Lewis Carroll) that any funtion f: () -> () is determined by its values at _|_ and (). This means that<BR/><BR/> f x = f_|_ or x and f()<BR/><BR/>(please excuse my lack of fluency in Haskell).<BR/><BR/>This equation is known as the Phoa Principle,<BR/>after Wesley Phoa, who wrote one of the first theses on Synthetic Domain Theory in c1990 under the supervision of Martin Hyland in Cambridge. However, Wes is now busy making lots of money.<BR/><BR/>Anyway, it turns out that this very simple equation makes the difference between mere lambda calculus and a theory of topology.<BR/><BR/>On the other hand, some "real mathematicians" may think that this page is entirely about empty set theory. There is another space with a non-Hausdorff topology that plays an import role in real analysis, called the <B>ascending reals</B>. This is in many ways similar to the Sierpinski space.<BR/>For an introduction to it, please see<BR/><A HREF="http://PaulTaylor.EU/ASD/lamcra/scott.html" REL="nofollow">here</A>.Paul Taylornoreply@blogger.comtag:blogger.com,1999:blog-11295132.post-2846200321741680252008-02-09T08:34:00.000-08:002008-02-09T08:34:00.000-08:00> So it's nice to try to find a mathematical formu...> So it's nice to try to find a mathematical formulation of what a procedure is so that looks like a function. And that's what this post is about.<BR/><BR/>The point was that functions are only mathematical entities. Even if the programming language is a "functional" one, the term "function" is overloaded to mean "procedure" (well, not to be confused with Pascal procedures).<BR/><BR/>That is, even if the notation is mathematical (which can be very convenient), it is only a description of a way to mechanically compute the function. <BR/><BR/>I agree that f1 and f2 compute the function you want, which is the only function f : () -> (), but f3 doesn't, because it doesn't terminate.<BR/><BR/>The problem with f1 is the way you call it. It is not f1 that gets into an infinite loop, but the evaluation of its argument.stefan.ciobacahttps://www.blogger.com/profile/03428807808381312083noreply@blogger.comtag:blogger.com,1999:blog-11295132.post-62888952579508393482008-02-09T07:43:00.000-08:002008-02-09T07:43:00.000-08:00> Now if you think in these terms, you are simply ...> Now if you think in these terms, you are simply describing three different procedure<BR/><BR/>But Haskell 'procedures' look a lot like functions in so many ways. So it's nice to try to find a mathematical formulation of what a procedure is so that looks like a function. And that's what this post is about.sigfpehttps://www.blogger.com/profile/08096190433222340957noreply@blogger.comtag:blogger.com,1999:blog-11295132.post-16947574635516001792008-02-09T00:18:00.000-08:002008-02-09T00:18:00.000-08:00This comment has been removed by a blog administrator.Matt Helligehttps://www.blogger.com/profile/14443679835760653518noreply@blogger.comtag:blogger.com,1999:blog-11295132.post-65757970182737575452008-02-09T00:16:00.000-08:002008-02-09T00:16:00.000-08:00Great post! Looking forward to more...I've been to...Great post! Looking forward to more...<BR/><BR/>I've been toying for awhile with the idea of an actual introduction to Haskell along these lines. "A Very Abstract Approach to Haskell" or something similar. It would be a very weird introduction, I guess, but there's more than enough normal ones by now. I have the idea of starting with 1 and 0 (unit and bottom) and building types-first from there, in a (literally) logical fashion. Anyway I find this kind of stuff edifying, fun and inspiring all at once. Keep it up!<BR/><BR/>And finally, to Michael, we should certainly say something about the existence of certain fixed points, and maybe even that least and greatest fixed points coincide? This leads to a bunch of other requirements that dcpo "just happens" to satisfy, doesn't it? I'm nearly at the end of my knowledge here, though...Matt Helligehttps://www.blogger.com/profile/14443679835760653518noreply@blogger.comtag:blogger.com,1999:blog-11295132.post-31733936661616948732008-02-08T22:42:00.000-08:002008-02-08T22:42:00.000-08:00luke,Good point.My answer to that is that if we're...luke,<BR/><BR/>Good point.My answer to that is that if we're using seq then we've stepped out of the pure lazy component of Haskell and we're playing by yet another set of rules. I'll have to think about how that fits into the grand scheme and clarify what I say.sigfpehttps://www.blogger.com/profile/08096190433222340957noreply@blogger.comtag:blogger.com,1999:blog-11295132.post-7757345163175453982008-02-08T22:04:00.000-08:002008-02-08T22:04:00.000-08:00To turn your post inside out, we might say that "p...To turn your post inside out, we might say that "picking a category in which types correspond to objects and values to arrows is a fun challenge". Since f4 is not decidable, we want to choose a category that has no arrow for f4.<BR/><BR/>The category of sets and functions doesn't work because f4 is a perfectly good set-function; fortunately, the category <A HREF="http://en.wikipedia.org/wiki/Complete_partial_order" REL="nofollow">Dcpo</A> of complete partial orders and directed-suprema-preserving functions looks more promising - it seems to have exactly the arrows we need for for all the values we think should exist in the type of functions from S -> S.<BR/><BR/>In particular, f1, f2, and f3 are all included but f4 is excluded because it fails to commute with sup; i.e. f4( sup {_|_, ()} ) != sup f4({_|_, ()}).<BR/><BR/>Next, if we wanted strict functions, we should require that our arrows be continuous (not just sup-preserving). This would rule out f2. <BR/><BR/>Finally, total functions are boring here because there's exactly one set-function from {()} -> {()} and it's definitely continuous.<BR/><BR/>What other properties make it seem that the category of Dcpos w/ sup-preserving functions as arrows is a hospitable place for Haskellites?Michael Stonehttps://www.blogger.com/profile/05322254915965832369noreply@blogger.comtag:blogger.com,1999:blog-11295132.post-76553490379311711382008-02-08T21:44:00.000-08:002008-02-08T21:44:00.000-08:00I was a bit puzzled at first, but now it seems nat...I was a bit puzzled at first, but now it seems natural.<BR/><BR/>There may be a point in making the distinction between a function and a procedure, as per Brian Harvey in Berkeley CS 61A.<BR/><BR/>A function is the mathematical thing, while a procedure is the thing (i.e. code) that describes how to compute a function. You may have several procedures that compute the same function, or you may have a function for which there is no procedure to compute it.<BR/><BR/>Now if you think in these terms, you are simply describing three different procedures, which is not at all weird. The procedures f1 and f2 are not the same because in the first case (f1) you ask Haskell to actually evaluate the argument (even though, per haskell semantics, the actually evaluation of the argument will happen sometime in the future, when you actually need it).<BR/><BR/>And the third procedure is nothing more than an infinite loop.<BR/><BR/>The type system of Haskell (or any other practical language) doesn't guarantee that a procedure that has type say t1 -> t2 actually returns a value of type t2, but it guarantees that *if the evaluation ends* the resulting value will be of the t2.<BR/><BR/>Hmm. Nice food for thought.stefan.ciobacahttps://www.blogger.com/profile/03428807808381312083noreply@blogger.comtag:blogger.com,1999:blog-11295132.post-87495828737319836232008-02-08T21:38:00.000-08:002008-02-08T21:38:00.000-08:00f3 and f5 are not indistinguishable.f3 `seq` () = ...f3 and f5 are not indistinguishable.<BR/><BR/>f3 `seq` () = ()<BR/>f5 `seq` () = _|_Lukehttps://www.blogger.com/profile/09807388788677769669noreply@blogger.comtag:blogger.com,1999:blog-11295132.post-29106768989447593072008-02-08T21:16:00.000-08:002008-02-08T21:16:00.000-08:00Ah, never mind. I get it now.Ah, never mind. I get it now.Luishttps://www.blogger.com/profile/13270576199551144751noreply@blogger.comtag:blogger.com,1999:blog-11295132.post-78908575156125509342008-02-08T20:57:00.000-08:002008-02-08T20:57:00.000-08:00I'm confused about your f1. Did you mean to define...I'm confused about your f1. Did you mean to define it as "f1 x = ()"?Luishttps://www.blogger.com/profile/13270576199551144751noreply@blogger.com