Path: utzoo!utgpu!news-server.csri.toronto.edu!rpi!zaphod.mps.ohio-state.edu!swrinde!mips!decwrl!asylum!osc!jgk From: jgk@osc.COM (Joe Keane) Newsgroups: comp.lang.functional Subject: Re: Applications for lazy functional languages Summary: You can't test for bottom. Keywords: strict Message-ID: <4705@osc.COM> Date: 2 Apr 91 23:49:07 GMT References: <4682@osc.COM> <8413@skye.cs.ed.ac.uk> <6853@rex.cs.tulane.edu> Reply-To: jgk@osc.COM (Joe Keane) Distribution: comp Organization: Versant Object Technology, Menlo Park, CA Lines: 66 In article <6853@rex.cs.tulane.edu> fs@caesar.cs.tulane.edu (Frank Silbermann) writes: >By the way, does the _formal_ theory of typed lambda calculus accept >constructor-based primitive functions defined via rewrite-rules? >For example, in the lambda-notation of denotational semantics, >one can _force_ any primitive function `f: A->B' to be strict >simply by defining f(BOT_A) = BOT_B. It's not that simple. In general you can't define f(BOT_A). In a fully lazy system, its value is determined by the values at other points. If don't want to be fully lazy, which is what you're asking for, you can make it less determined. You can never make it more determined. Really this is a semantic argument, rather than something provided in your type system. I've posted about this subject before, so i won't repeat what i said then. Bottom is the least determined value, and it must be consistent with other values which are more determined. Basically, i'd say you shouldn't think of bottom as `fails to terminate', but rather as `status unknown'. In fact you can detect some cases of failure to terminate, and give them new values in your type system. Then if you know that some expression fails to terminate, it's not bottom. Of course you can never hope to catch all cases. >One can even use this method >to define a strict version of function application. I would say that strictness is a property of specific primitive combinators, rather than something you can specify in your type system. You can use strict primitive combinators to force evaluation of some expression, even if you don't use its value. Suppose we define a combinator with HOLD x y = x, but we say that it's strict in y. In other words, it computes x and y in some order or in parallel, and when both values are available it returns the first. There are many ways to simulate this, depending on what primitives you have available. For example, if x and y are numbers you could define it as HOLD x y = 0*x+y. This assumes that the multiplication primtive is strict in both arguments. If it's too smart, this won't work. So let's just assume HOLD is a primitive. This combinator makes a lot more sense when you consider it temporally. It `holds up' the value x until y is ready. This provides a way to synchronize two values, which is useful if we want to write them out to disk together or something like that. The idea is that we only want to write them both out if they're both ready, otherwise we don't want to write anything. You can see the similarity to database transactions. If we extend this to include side-effects (and switch the parameters), we get normal sequential execution. This combinator would be exactly the same as the comma operator in C or the semicolon `operator' in Pascal. If you want to execute a C program with combinators, this is exactly what you do. But then you can change the semantics to be more lazy, by removing the strictness. This gives you dead code elimination and common subexpression elimination, the usual C compiler stuff. The interesting thing is that this makes a `new' C where more things terminate. For example, the following function returns 0: int foo() { while (1); return 0; } -- Joe Keane, supercombinator hacker