Home > Archive > Functional > May 2007 > Function Purity, Exceptions and Termination
You are viewing an archived Text-only version of the thread.
To view this thread in it's original format and/or if you want to reply to
this thread please [click here]
| Author |
Function Purity, Exceptions and Termination
|
|
|
| Hi there,
I'm a functional newbie, and I've been wondering a couple of things
about the purity of functions.
As I understand it, a function is pure if it:
1) Has no "side-effects."
2) Relies only on its arguments.
What I'd like to know is if a pure function can:
a) throw exceptions.
b) fail to terminate.
Intuitively, I think that the answer to (a) is yes. (Assuming that the
exception ctor/dtor are pure too). First, the exception by itself does
not create side effects. Second, the same exception would be thrown
given the same arguments.
I think one way to think about it is that throwing an exception creates
an additional return value option, so that:
int Foo() throws (a, b);
Would have a possible return set equivalent to union {int, a, b}. Is
this more or less correct?
And finally, I just wanted to know if function purity says anything
about termination. A function that doesn't terminate arguably *does*
have a side-effect, namely locking control flow. Therefore, I wondered
what functional languages like Haskell do in light of the halting problem.
Many thanks!
-Al-
| |
| Frederic Beal 2007-05-05, 8:02 am |
| On 2007-05-05, Al <two@haik.us> wrote:
> a) throw exceptions.
> b) fail to terminate.
>
> Intuitively, I think that the answer to (a) is yes. (Assuming that the
> exception ctor/dtor are pure too). First, the exception by itself does
> not create side effects. Second, the same exception would be thrown
> given the same arguments.
Depends on what you call «Â_functional programingÂ_». My definition
is that two calls of the same function with the same arguments always
produce the same result, if any. Then, if exception throwing is
deterministic, no problem.
> I think one way to think about it is that throwing an exception creates
> an additional return value option, so that:
>
> int Foo() throws (a, b);
>
> Would have a possible return set equivalent to union {int, a, b}. Is
> this more or less correct?
Rather correct. The idea of returning extra values is central to
encapsulating many program flow (and other) features in Haskell.
> And finally, I just wanted to know if function purity says anything
> about termination. A function that doesn't terminate arguably *does*
> have a side-effect, namely locking control flow. Therefore, I wondered
> what functional languages like Haskell do in light of the halting problem.
No, non-termination is not a problem, since being functional has nothing to
do with execution time. A function that would either return 2 or never
return, on a random basis, would still be purely functional.
--
Frederic
| |
| Paul Rubin 2007-05-05, 8:02 am |
| Al <two@haik.us> writes:
> And finally, I just wanted to know if function purity says anything
> about termination. A function that doesn't terminate arguably *does*
> have a side-effect, namely locking control flow. Therefore, I wondered
> what functional languages like Haskell do in light of the halting
> problem.
It's treated as having a special "value" called "bottom". There
is an article about this on wikibooks:
http://en.wikibooks.org/wiki/Haskel...ional_semantics
| |
| Frederic Beal 2007-05-05, 8:02 am |
| On 2007-05-05, Paul Rubin <> wrote:
> Al <two@haik.us> writes:
>
> It's treated as having a special "value" called "bottom".
Actually, bottom will represent many things, depending on the semantics
you are interested in. One is non-termination, another is program error.
A third one is unknown behaviour (which is slightly different from an
error). And so on.
--
Frederic
| |
| dan.doel@gmail.com 2007-05-05, 8:02 am |
| Frederic Beal wrote:
> No, non-termination is not a problem, since being functional has nothing to
> do with execution time. A function that would either return 2 or never
> return, on a random basis, would still be purely functional.
In fact, non-termination can be looked at as a side effect. Moggi
actually mentions it in one of his papers[1] on monads (which I
haven't read in its entirety, though I did notice this bit), and there
was a set of Epigram-related slides[2] that talked about a non-
termination monad going around some time last year.
In Moggi's case, the concern was that using beta and eta reduction to
prove equivalence of programs leaves you with a total language, and,
of course, Epigram wants to be total by design. However, some real
programs don't terminate, of course, and you can model that formally
using a non-termination monad, where M A = A + { _|_ }.
In Haskell, of course, every (boxed) type has bottom as a member
automatically. So, I suppose one could say that all Haskell programs
are implicitly run in a non-termination monad, similar to how one can
look at impure functional languages (or imperative languages, etc.) as
having implicit monadic semantics for assignment, I/O, exceptions,
continuations, etc.
But, of course, I suppose all the above depends heavily on your
definition of what exactly "pure" is in regards to functional
languages.
[1] http://www.disi.unige.it/person/Mog...blications.html <-- seems
to be a list of his papers. "Notions of computation and monads" is the
paper I was referring to.
[2] http://www.cs.nott.ac.uk/~txa/talks/bctcs06.pdf
| |
| Joachim Durchholz 2007-05-05, 8:02 am |
| Let me try to apply my current understanding of the issues involved.
Corrections welcome :-)
Al schrieb:
>
> As I understand it, a function is pure if it:
>
> 1) Has no "side-effects."
> 2) Relies only on its arguments.
There is a third definition:
3) Preserves semantics under inlining substitutions ("equational
reasoning").
> What I'd like to know is if a pure function can:
>
> a) throw exceptions.
Pure under interpretations (1) and (2).
Pure under (3) provided that you know how to inline code that catches
exceptions. (E.g. there might exist a language that has no provision for
catching an exception except at end-of-function; in this case, there is
no semantics-preserving inlining transformation, and you end up with
impure exceptions.)
> b) fail to terminate.
Under (1), it may be pure or impure, depending on what exactly you
consider to be a side effect.
E.g. when considering execution on a real machine, nontermination is a
kind of side effect. When considering an abstract calculus, if you can
infer that the call will not terminate, you can say the result is
"bottom" (roughly equivalent to Pascal's nil, often written as _|_), and
there's no side effect left (however, you might end up being unable to
decide whether a function terminates, so you're deep in a can of worms
even if you don't follow a stepwise evaluation procedure).
Under (2), it's pure.
Under (3), I'm not sure. Intuitively, I'd say that it's pure under that
interpretation, but I dimly recall that substitution can play nasty
tricks on termination (stuff that used to not terminate might suddenly
terminate for specific parameter constellations after a few rounds of
substitution, if you chose the "right" substitutions).
OTOH languages like Haskell are *defined* using a substitution rule,
which means that substitution is by definition semantics-preserving.
(Tentative conclusion: nontermination may be pure or impure, depending
on the language's semantics.)
Hope I  somebody. I certainly managed to confuse myself :-)
Regards,
Jo
| |
| rossberg@ps.uni-sb.de 2007-05-05, 8:02 am |
| On 5 Mai, 08:14, Al <t...@haik.us> wrote:
>
> As I understand it, a function is pure if it:
>
> 1) Has no "side-effects."
> 2) Relies only on its arguments.
"Purity" does not mean the same to all people. A more formal and more
general definition is that a function is pure when its 'behaviour'
does not depend on the choice of evaluation strategy (e.g. call-by-
value vs call-by-name reduction, and order of evaluation of
subexpressions - or "control flow" as you called it).
> What I'd like to know is if a pure function can:
>
> a) throw exceptions.
> b) fail to terminate.
Under the definition I gave above, neither of these is pure. The
function
f () = raise A + raise B
can observe order of evaluation of subexpressions, while
g () = let h x = 0 in h (diverge ())
can observe reduction strategy (will terminate with call-by-name or
call-by-need, but diverge with call-by-value).
There are many variations to the definition. The one above is often
used in mathematical contexts. In more operationally oriented settings
people often assume somewhat weaker definitions that fix the
evaluation strategy to a certain degree. E.g. for Haskell you take non-
strictness (call-by-name/need) for granted and thus can view non-
termination as pure, because it cannot be exploited to observe the
remaining degrees of freedem in evaluation order.
The story with exceptions is even more intricate. You can still
consider a raising function like f pure if the language provides no
way to actually *catch* the precise exception that has been raised and
thus observe it. Then you can pretend that f above actually raises a
*set* of exceptions {A,B}, and that set does not depend on evaluation
order. This is the approach Haskell takes, where functions actually
may raise exceptions, but you can only catch them within the impure IO
monad, which then makes a conceptionally non-deterministic choice as
to which exception it actually observes. (In the implementation of
course the choice is made at raise point, qua the implemented
evaluation order, and no set is ever constructed.)
- Andreas
| |
| Chris Smith 2007-05-05, 7:04 pm |
| <rossberg@ps.uni-sb.de> wrote:
> On 5 Mai, 08:14, Al <t...@haik.us> wrote:
>
> "Purity" does not mean the same to all people. A more formal and more
> general definition is that a function is pure when its 'behaviour'
> does not depend on the choice of evaluation strategy (e.g. call-by-
> value vs call-by-name reduction, and order of evaluation of
> subexpressions - or "control flow" as you called it).
How is this a useful definition of purity? It is trivial to give
examples in the pure lambda calculus whose behavior depends on the order
of evaluation. Specifically: there are infinitely many lambda terms
that have normal forms and reach them by normal order reduction; but
whose applicative order reduction never terminates. Are you really
saying that the pure lambda calculus is not purely functional?
--
Chris Smith
| |
| Chris Smith 2007-05-05, 7:04 pm |
| Al <two@haik.us> wrote:
> What I'd like to know is if a pure function can:
>
> a) throw exceptions.
> b) fail to terminate.
In general, I'd say: (a) no; (b) yes. This is assuming that, by "throw
exceptions", you mean a mechanism that allows the exception to propogate
to somewhere and then be caught and handled.
> Intuitively, I think that the answer to (a) is yes. (Assuming that the
> exception ctor/dtor are pure too). First, the exception by itself does
> not create side effects. Second, the same exception would be thrown
> given the same arguments.
>
> I think one way to think about it is that throwing an exception creates
> an additional return value option, so that:
>
> int Foo() throws (a, b);
>
> Would have a possible return set equivalent to union {int, a, b}. Is
> this more or less correct?
As you've probably observed to this point, this can be more of a
definitional matter than anything else. There is always a way of
describing the behavior of any real-world system using purely functional
concepts, but it may be very complex and involve global program
transformations. How complex do the transformations need to be before
refusing to accept the function as "pure"? Most people would draw the
line in such a way as to allow simple local transformations liek
syntactic sugar; but not transformations that propogate to other parts
of the program.
Exception handling is one case that would need a rather involved
transformation to make it operate only in terms of pure functional
concepts. Sure you can say that it's possible to convert an exception-
throwing function into a non-exception-throwing function with extra
possible return values. What that means, though, is that any function
that calls your exception-throwing function needs to be modified, too,
so that it responds appropriately when the "return value" is really an
exception. And then anything calling that one, too, must be similarly
modified, and so on.
It's certainly possible to do this transformation. Some functional
languages even make it rather easy. Haskell, for example, lets you do
it with monads and a special do-notation so that you don't actually have
to type all the stuff that threads the exception handling code
throughout a large part of your program. But that doesn't make it
purely functional, because the necessary transformation is still a big
deal.
If you accept anything that can be transformed into the purely
functional world as pure, then consider the following. Let's say my
function reads and assigns the value of global variable. Well, that's a
lot like saying that it takes an extra parameter (the value of the
variable before my function) and returns a tuple consisting of (a) its
old return value, and (b) the value of the global after the function is
done. So at least in a single-threaded context, global variables can be
modeled as transformations of programs into a purely functional setting.
That doesn't mean that using global variables is purely functional.
> And finally, I just wanted to know if function purity says anything
> about termination. A function that doesn't terminate arguably *does*
> have a side-effect, namely locking control flow. Therefore, I wondered
> what functional languages like Haskell do in light of the halting problem.
What Haskell does is defines a special value, called bottom or _|_, to
represent the result of a non-terminating computation. Bottom is a
potential value for all possible types (precisely because the halting
problem means that the type checker could never be sure that something
can't evaluate to bottom). Bottom can't be used in pattern matching
because, again, the halting problem means that it's impossible to know
at run time whether an expression has evaluated to bottom, or just isn't
done evaluating yet. Any time that value of bottom is forced by some
expression, the value of that expression is also bottom. It works out
just fine.
--
Chris Smith
| |
| rossberg@ps.uni-sb.de 2007-05-05, 7:04 pm |
| On 5 Mai, 15:12, Chris Smith <cdsm...@twu.net> wrote:
>
> How is this a useful definition of purity? It is trivial to give
> examples in the pure lambda calculus whose behavior depends on the order
> of evaluation. Specifically: there are infinitely many lambda terms
> that have normal forms and reach them by normal order reduction; but
> whose applicative order reduction never terminates.
No such terms exist in *typed* lambda calculi (unless you explicitly
add recursion) - which is what logicians usually work with. When used
as a logic, the semantics of a calculus should not depend on
evaluation strategy, and a calculus with non-termination is
inconsistent: you can prove anything. So in that context, there is
good reason to consider non-termination impure. The same obviously
holds when you want a programming language with strong logical
properties (consider dependently-typed PLs etc).
- Andreas
| |
| Geoffrey 2007-05-05, 7:04 pm |
| On May 5, 2:14 am, Al <t...@haik.us> wrote:
> Hi there,
>
> I'm a functional newbie, and I've been wondering a couple of things
> about the purity of functions.
>
> As I understand it, a function is pure if it:
>
> 1) Has no "side-effects."
> 2) Relies only on its arguments.
>
> What I'd like to know is if a pure function can:
>
> a) throw exceptions.
> b) fail to terminate.
>
Don't let them fool you, both cases are allowed in purely functional
code. In fact, there are probably other things that are possible that
aren't obvious.
***Any given function may return zero, one, or many times for each
call to it.***
Allowing that a function might never return to the calling function
(in light of continuations, this is easily accomplished), the only
question remains as to where program control has passed to. The
implications of a function returning multiple times (also trivial,
with continuations) are much broader. Showing that these are purely
functional programs is simply, by direct translation to CPS style.
Consider the following Scheme code: can you devise definitions of f
and g that cause this snippet to return false?
(let* ((x (f))
(y (f))
(z (g x y)))
(if (and (pair? x) (number? (car x)) (pair? y) (number? (car y)))
(= (car x) (car y))
#t))
Intuitively, you might say "no", because f must return the same result
for both executions. However, a more detailed study will reveal that
the continuations given to each call to f are in fact different,
meaning that the parameters are different, and thus that the return
values may be different.
So, using continuations, functions can very easily throw exceptions
and fail to terminate while maintaining the precepts of functional
programming.
| |
|
| Hi there,
Thanks to all for your replies! Glad to hear the many points of views on
the topic.
I'll have to read a couple again before I understand them well. It seems
that exceptions are allowed in most (all?) purely functional languages
(either formally, or through "hand waving"), but perhaps this is not
pure enough for some applications (e.g. typed lambda calculi).
Some of you mentioned this "Bottom" value in Haskell that seems to
permeate as an extra possibility in all types. I kind of understand what
it denotes, but I don't understand how such a value could result from a
non-terminating computation. Does the runtime actually wait until the
stack overflows before evaluating to this value? Otherwise, how does it
know when to do so? What if it's a function without a stack footprint:
inline void Foo() { while(1); }
Anyway, thanks very much again!
-Al-
| |
| David Formosa (aka ? the Platypus) 2007-05-06, 7:03 pm |
| On 5 May 2007 11:05:28 -0700, rossberg@ps.uni-sb.de
<rossberg@ps.uni-sb.de> wrote:
> On 5 Mai, 15:12, Chris Smith <cdsm...@twu.net> wrote:
>
> No such terms exist in *typed* lambda calculi (unless you explicitly
> add recursion) - which is what logicians usually work with.
> When used as a logic, the semantics of a calculus should not depend on
> evaluation strategy,
But that doesn't disprove the arguement. Untyped lambda calculus is
considered pure and some evaluation stratagies in lambda calculus do
not terminate. While you may feel that this is an undesirable feature
it doesn't change its purity.
> and a calculus with non-termination is inconsistent: you can prove
> anything.
I don't think that this follows. If you said that non-termination
makes a calculus incomplete I would not protest, but compleatness is
not the same as consistency.
| |
| Chris Smith 2007-05-06, 7:03 pm |
| Al <two@haik.us> wrote:
> Some of you mentioned this "Bottom" value in Haskell that seems to
> permeate as an extra possibility in all types. I kind of understand what
> it denotes, but I don't understand how such a value could result from a
> non-terminating computation. Does the runtime actually wait until the
> stack overflows before evaluating to this value?
No. You're confusing implementation with semantics. If an expression
"evaluates to bottom", it doesn't really physically evaluate to anything
at all. From a strictly implementation standpoint, "evaluates to
bottom" is sort of a euphemism for "never finishes, or perhaps
terminates the whole program".
The value of bottom is useful for specifying semantics. The semantics
of the language say that if an expression evaluates to bottom, then any
other expression that forces it will also evaluate to bottom. Now,
substitute either "goes into an infinite loop" or "terminates the
program" instead of the phrase "evaluates to bottom", and you'll see
that this is exactly what you'd expect.
Essentially, "bottom" doesn't exist in the physical plane of things.
But it's convenient to specify the semantics as if any expression has a
value. (For example, what's the type of an expression that can't have
any values? There's no good answer there.) So this pseudo-value is
introduced ONLY as a communication tool. Don't fool yourself into
thinking there's actually some bit pattern in memory that represents
"bottom", because there isn't.
> inline void Foo() { while(1); }
>
Or, in Haskell terminology, this would be "let x = x in x". This does
have a value of bottom... which means that it never finishes. (It's
definitively not an *alternative* to it never finishing, which is the
direction you were going.)
--
Chris Smith
| |
| Marshall 2007-05-06, 7:03 pm |
| On May 6, 3:17 pm, Chris Smith <cdsm...@twu.net> wrote:
> Al <t...@haik.us> wrote:
>
> No. You're confusing implementation with semantics. If an expression
> "evaluates to bottom", it doesn't really physically evaluate to anything
> at all. From a strictly implementation standpoint, "evaluates to
> bottom" is sort of a euphemism for "never finishes, or perhaps
> terminates the whole program".
>
> The value of bottom is useful for specifying semantics. The semantics
> of the language say that if an expression evaluates to bottom, then any
> other expression that forces it will also evaluate to bottom. Now,
> substitute either "goes into an infinite loop" or "terminates the
> program" instead of the phrase "evaluates to bottom", and you'll see
> that this is exactly what you'd expect.
>
> Essentially, "bottom" doesn't exist in the physical plane of things.
> But it's convenient to specify the semantics as if any expression has a
> value. (For example, what's the type of an expression that can't have
> any values? There's no good answer there.) So this pseudo-value is
> introduced ONLY as a communication tool. Don't fool yourself into
> thinking there's actually some bit pattern in memory that represents
> "bottom", because there isn't.
Nice explanation.
The terminology/euphemisms around bottom are a real impediment
to understanding, IMHO. "Evaluates to bottom" is really misleading,
if not actually outright wrong. Nobody seems to have any difficulty
with top as a type; why can't we just talk about bottom as a type,
rather than as a value? (Especially since it *isn't* a value.) Bottom
is the uninhabited type; there are no associated values.
We already have a really good term to describe functions
that don't complete with a value: they diverge.
Marshall
| |
| Joachim Durchholz 2007-05-06, 7:03 pm |
| Al schrieb:
> Some of you mentioned this "Bottom" value in Haskell that seems to
> permeate as an extra possibility in all types. I kind of understand what
> it denotes, but I don't understand how such a value could result from a
> non-terminating computation.
If you define Haskell's semantics by setting up an interpreter and
describing the evaluation steps, you'll simply get nontermination.
However, there's an alternative view: seeing each function definition as
an equation to be solved.
Consider the usual definition of the factorial function:
fac 1 = 1
fac N = fac (N - 1) * N
Mathematically, this is a set of equations that define the definition of
the 'fac' symbol.
In this definition, it does make sense to have something called
"bottom". It is applied for those equation sets that either have no
solution, or have "too many" solutions.
I.e.
f x = f (x - 1)
f 0 = 0
f 1 = 1
has no solution, so f is _|_.
Another example:
f x = f x
does not constrain f at all, the solution is the set of all functions,
which again is considered to "diverge".
In practice, you don't have "bottom", you simply have nontermination :-)
Regards,
Jo
| |
| Chris Smith 2007-05-07, 8:03 am |
| Marshall <marshall.spight@gmail.com> wrote:
> The terminology/euphemisms around bottom are a real impediment
> to understanding, IMHO. "Evaluates to bottom" is really misleading,
> if not actually outright wrong. Nobody seems to have any difficulty
> with top as a type; why can't we just talk about bottom as a type,
> rather than as a value? (Especially since it *isn't* a value.) Bottom
> is the uninhabited type; there are no associated values.
If people meant to talk about the type bottom in a theoretical sense,
I'm sure they would. You can't ban talking about the value, though.
That is something that seems to work with eager evaluation, but gets
difficult with lazy evaluation. In Haskell, I can write:
let f x = if x < 2 then () else undefined
xs = map f [1, 2, 3]
in length xs
And this evaluates to 3. 'xs' has a type of [()], and its value is
[ () , _|_ , _|_ ] (where _|_ is a representation of bottom). That
list, of course, is 3 elements long.
If you can explain that as simply without using bottom as a value, go
for it. Note that nothing here can be validly described as having the
type bottom. The types of everything (after type inference) are:
x :: (Num a, Ord a) => a
2 :: (Num a, Ord a) => a
() :: ()
undefined :: ()
the if statement :: ()
f :: (Num a, Ord a) => a -> ()
[1, 2, 3] :: (Num a, Ord a) => [a]
map :: (Num a, Ord a) => (a -> ()) -> [a] -> [()]
map f [1, 2, 3] :: [()]
xs :: [()]
length :: [a] -> Int
length xs :: Int
Without being able to talk about the value bottom, the best you can do
is talk about unevaluated expressions or thunks of some kind. But
that's a whole different concept that now needs to be introduced into
the semantics. Simply adding the value of bottom to our conceptual
vocabulary avoids that ugly necessity, and it still lets people who care
about the implementation build their own models of what's going on that
are more helpful to them.
> We already have a really good term to describe functions
> that don't complete with a value: they diverge.
The problem is that diverging is an action. In the example above,
nothing diverges, or the program wouldn't finish.
--
Chris Smith
| |
| Marshall 2007-05-07, 8:03 am |
| On May 6, 7:53 pm, Chris Smith <cdsm...@twu.net> wrote:
> Marshall <marshall.spi...@gmail.com> wrote:
>
> If people meant to talk about the type bottom in a theoretical sense,
> I'm sure they would. You can't ban talking about the value, though.
Small point: I'm not trying to "ban" anything; just trying to
determine
the most useful terminology. (Hey, weren't you the guy who was
trying to get the dynamic typing people to give up the term "dynamic
typing" a while back? :-)
> That is something that seems to work with eager evaluation, but gets
> difficult with lazy evaluation. In Haskell, I can write:
>
> let f x = if x < 2 then () else undefined
> xs = map f [1, 2, 3]
> in length xs
>
> And this evaluates to 3. 'xs' has a type of [()], and its value is
> [ () , _|_ , _|_ ] (where _|_ is a representation of bottom). That
> list, of course, is 3 elements long.
>
> If you can explain that as simply without using bottom as a value, go
> for it.
Some non-rhetorical questions:
What's wrong with using "undefined" everywhere you used
"bottom" above?
What happens when you try to evaluate undefined? Alternatively,
what is the sum of xs? Or, what is undefined + 1?
My expectation would be that either evaluating undefined
is an exceptional condition, or that undefined propagates
through the program. (I.e., undefined + 1 = undefined.)
But I don't speak Haskell very well; just enough to
order dinner without having the waiter laugh too hard.
> Note that nothing here can be validly described as having the
> type bottom. The types of everything (after type inference) are:
>
> x :: (Num a, Ord a) => a
> 2 :: (Num a, Ord a) => a
> () :: ()
> undefined :: ()
> the if statement :: ()
> f :: (Num a, Ord a) => a -> ()
> [1, 2, 3] :: (Num a, Ord a) => [a]
> map :: (Num a, Ord a) => (a -> ()) -> [a] -> [()]
> map f [1, 2, 3] :: [()]
> xs :: [()]
> length :: [a] -> Int
> length xs :: Int
>
> Without being able to talk about the value bottom, the best you can do
> is talk about unevaluated expressions or thunks of some kind. But
> that's a whole different concept that now needs to be introduced into
> the semantics.
Did we introduce anything new? We already had undefined, above.
> Simply adding the value of bottom to our conceptual
> vocabulary avoids that ugly necessity, and it still lets people who care
> about the implementation build their own models of what's going on that
> are more helpful to them.
Yeah, except that it isn't a value, and so the terminology now
confuses rather than informs. The meaning of the word "value"
is diluted, and that strikes me as not worth it.
>
> The problem is that diverging is an action. In the example above,
> nothing diverges, or the program wouldn't finish.
Assuming I accept your term "action", then yes, and that's
the *advantage* of using that term. You're trying to pick
a value from the empty set; that's not gonna work.
The interesting part in your list of the types of things was
the type of undefined, which is the unit type. If that's
accurate, then evaluating undefined should yield the
unit value, shouldn't it? That doesn't seem right to me;
How about, instead of saying "'xs' has a type of [()], and
its value is [ () , _|_ , _|_ ]" why don't we say "'xs' has a
type of [()], and the type of its values is [ () , _|_ , _|_ ]"?
It seems like the source of the problem you've identified
is laziness, not bottom.
Marshall
| |
| Dirk Thierbach 2007-05-07, 8:03 am |
| Marshall <marshall.spight@gmail.com> wrote:
> The terminology/euphemisms around bottom are a real impediment
> to understanding, IMHO. "Evaluates to bottom" is really misleading,
> if not actually outright wrong.
It's not misleading if you remember that "bottom" is a purely semantic
construct. So if anyone is talking about "evaluates to bottom", that
clearly means "the semantic function associated with that program has
bottom as a semantic value".
> Nobody seems to have any difficulty with top as a type; why can't we
> just talk about bottom as a type, rather than as a value?
Because it is a (semantic) value, and not a type :-) "Top" and
"bottom" are just the generic mathematical names for the largest and
least elements of an order. In Lisp, the usual type system is so weak
(sorry :-) that you need to introduce a top type to cover those cases
you cannot deal with otherwise. In semantics, you are normally not
interested in ordering types, but you are interested in interpreting
each type as a complete partial order of values. The smallest value in
such an interpretation is called "bottom", and the interpretation for
each type usually has such a value. OTOH, there is normally no largest
value (because the maximal values describe "complete" functions). And
the "bottoms" are important, because you need them to define fixpoints
(and hence, recursion).
Lisp types and values in denotational semantics are two different
worlds. Don't mix them.
> (Especially since it *isn't* a value.) Bottom is the uninhabited
> type; there are no associated values.
In semantics, you think very differently: There are a lot of types
that can be uninhabited, not just one, so it doesn't make sense to
speak about "the" uninhabited type. And types are not ordered, so it
doesn't make sense to use a special name for "it", either.
> We already have a really good term to describe functions
> that don't complete with a value: they diverge.
No, that describes a computation that doesn't finish. And if you
want to describe such a computation, it's indeed the better word.
But if you need a semantic value that is "undefined" and can in
principle cover anything from errors over non-termination to
"not yet known in an finite appromixation of a function", you use
"bottom".
If you haven't been exposed to deonational semantics yet, googling
for it may find some introduction.
- Dirk
| |
| Ingo Menger 2007-05-07, 8:03 am |
| On 7 Mai, 09:45, Marshall <marshall.spi...@gmail.com> wrote:
>
> Yeah, except that it isn't a value, and so the terminology now
> confuses rather than informs.
Yes, it is a value, conceptually. For it is not easy to describe the
semantics of the language when you have exceptions, for example. If
you have exceptions, then you must have control flow also, as well as
a notion of *first* and *then*.
With the imaginary value bottom (or undefined, if you prefer), it is
easier, since you only have to specify that the result of a function
that tries to deconstruct bottom is also bottom.
> How about, instead of saying "'xs' has a type of [()], and
> its value is [ () , _|_ , _|_ ]" why don't we say "'xs' has a
> type of [()], and the type of its values is [ () , _|_ , _|_ ]"?
Sorry, that's nonsense. When the type of xs is [()] that means
essentially that the type of all its elements is ().
| |
| rossberg@ps.uni-sb.de 2007-05-07, 8:03 am |
| "David Formosa (aka ? the Platypus)" wrote:
>
> But that doesn't disprove the arguement. Untyped lambda calculus is
> considered pure and some evaluation stratagies in lambda calculus do
> not terminate. While you may feel that this is an undesirable feature
> it doesn't change its purity.
As I said, the definition of purity depends on your application
domain. When doing computational logic, you are usually not much
interested in the untyped lambda calculus (and it not being
terminating is one of the reasons).
If you do not like that definition then go ahead, but you will have to
accept that there are fields where non-termination is considered an
effect nevertheless. This includes some work on programming language
semantics.
>
> I don't think that this follows. If you said that non-termination
> makes a calculus incomplete I would not protest, but compleatness is
> not the same as consistency.
As a logic, it makes it inconsistent, because you can use a diverging
term as a proof term for any formula you want, including False. By
Curry-Howard this is equivalent to having every type (including
"empty" ones) inhabited by _|_, as is the case in Haskell. Nothing to
do with completeness.
| |
| Matthias Blume 2007-05-07, 7:04 pm |
| Chris Smith <cdsmith@twu.net> writes:
> <rossberg@ps.uni-sb.de> wrote:
>
> How is this a useful definition of purity? It is trivial to give
> examples in the pure lambda calculus whose behavior depends on the order
> of evaluation. Specifically: there are infinitely many lambda terms
> that have normal forms and reach them by normal order reduction; but
> whose applicative order reduction never terminates. Are you really
> saying that the pure lambda calculus is not purely functional?
For certain definitions of purity (in particular, if you consider
non-termination an effect), yes.
On the other hand, the simply typed lambda calculus is pure, and so is
F2, among others.
Matthias
| |
| Matthias Blume 2007-05-07, 7:04 pm |
| "David Formosa (aka ? the Platypus)" <dformosa@usyd.edu.au> writes:
> On 5 May 2007 11:05:28 -0700, rossberg@ps.uni-sb.de
> <rossberg@ps.uni-sb.de> wrote:
>
> But that doesn't disprove the arguement. Untyped lambda calculus is
> considered pure and some evaluation stratagies in lambda calculus do
> not terminate. While you may feel that this is an undesirable feature
> it doesn't change its purity.
Of course, it all depends on how "purity" is defined.
>
> I don't think that this follows. If you said that non-termination
> makes a calculus incomplete I would not protest, but compleatness is
> not the same as consistency.
What he means is that the LOGIC that corresponds to the computational
calculus is inconsistent, because you can write a program that denotes
"bottom" -- which in turn corresponds to writing a proof that proves
"false".
Matthias
| |
| Matthias Blume 2007-05-07, 7:04 pm |
| Geoffrey <geoffrey.marchant@gmail.com> writes:
> On May 5, 2:14 am, Al <t...@haik.us> wrote:
>
> Don't let them fool you, both cases are allowed in purely functional
> code. In fact, there are probably other things that are possible that
> aren't obvious.
>
> ***Any given function may return zero, one, or many times for each
> call to it.***
>
> Allowing that a function might never return to the calling function
> (in light of continuations, this is easily accomplished), the only
> question remains as to where program control has passed to. The
> implications of a function returning multiple times (also trivial,
> with continuations) are much broader. Showing that these are purely
> functional programs is simply, by direct translation to CPS style.
>
> Consider the following Scheme code: can you devise definitions of f
> and g that cause this snippet to return false?
>
> (let* ((x (f))
> (y (f))
> (z (g x y)))
> (if (and (pair? x) (number? (car x)) (pair? y) (number? (car y)))
> (= (car x) (car y))
> #t))
>
> Intuitively, you might say "no", because f must return the same result
> for both executions. However, a more detailed study will reveal that
> the continuations given to each call to f are in fact different,
> meaning that the parameters are different, and thus that the return
> values may be different.
>
> So, using continuations, functions can very easily throw exceptions
> and fail to terminate while maintaining the precepts of functional
> programming.
Explicitly manipulating continuations (e.g., via call/cc) makes a
program impure.
| |
| Chris Smith 2007-05-07, 7:04 pm |
| Marshall <marshall.spight@gmail.com> wrote:
> Small point: I'm not trying to "ban" anything; just trying to
> determine the most useful terminology.
Sure, I didn't mean any such connotations there, as I hope you know.
You may substitute "you can't give up talking ...".
> (Hey, weren't you the guy who was
> trying to get the dynamic typing people to give up the term "dynamic
> typing" a while back? :-)
Yes, and proudly so. What's your point? ;)
> What's wrong with using "undefined" everywhere you used
> "bottom" above?
Nothing at all. If you'd like to call the value "undefined" instead of
"bottom", you won't run into any big problems except for communication.
> What happens when you try to evaluate undefined? Alternatively,
> what is the sum of xs? Or, what is undefined + 1?
>
> My expectation would be that either evaluating undefined
> is an exceptional condition, or that undefined propagates
> through the program. (I.e., undefined + 1 = undefined.)
> But I don't speak Haskell very well; just enough to
> order dinner without having the waiter laugh too hard.
Well, undefined evaluates to bottom, of course! ;) Okay, so there are
two perspectives again.
From an implementation perspective, what happens is that undefined is
initially left as an unevaluated expression or thunk. When you write
(undefined + 1), that becomes another unevaluated expression. Now, say
you want to do something that forces the value -- say, print it. Then
print tries to calculate 'undefined + 1', and the (+) operator for the
type will attempt to calculate the value of 'undefined'. The prelude
function undefined will then terminate the program with an error that
looks something like "********* Prelude: undefined".
(Actually, it will not necessarily terminate the whole program -- the IO
monad has a mechanism to catch these. IIRC, it's so formally messy that
the semantics of the language simply punts and describes that feature as
acting in a non-deterministic way, leaving it to a quality of
implementation issue to decide what to do.)
So that's the implementation perspective. From the perspective of
language semantics, though, things are much simpler. undefined has a
value of bottom. The addition operator on bottom yields bottom, so
(undefined + 1) also has a value of bottom. Finally, print bottom also
evaluates to bottom, so the whole program (assuming that print is the
whole program) evaluates to bottom. The semantics make no distinction
between abrupt termination and infinite looping, so either is allowed as
program behavior.
> Yeah, except that it isn't a value, and so the terminology now
> confuses rather than informs. The meaning of the word "value"
> is diluted, and that strikes me as not worth it.
Ah, but the whole point is that it acts exactly like a value, unless you
are looking from an implementation standpoint. What definition of value
are you looking out for, which is diluted here?
>
> Assuming I accept your term "action", then yes, and that's
> the *advantage* of using that term. You're trying to pick
> a value from the empty set; that's not gonna work.
But that is precisely the problem that's being solved. You're trying to
talk about behavior, but we'd like to avoid talking about behavior in
specifying the semantics. This is important because the actual behavior
of a language that does lazy evaluation is very difficult to predict or
describe. It becomes very useful to have a simple way to describe the
ultimate result, in a way that doesn't require tracing through the
actual behavior of the program.
> The interesting part in your list of the types of things was
> the type of undefined, which is the unit type. If that's
> accurate, then evaluating undefined should yield the
> unit value, shouldn't it? That doesn't seem right to me;
The unit type has two values: () and bottom. In this case, the value of
those terms is bottom, rather than ().
I'm realizing my types may have been a little misleading. Those were
the inferred types of expressions in this particular context. The
general type of undefined is (forall a. a), which means that it can be a
value of any type, without restriction. Because of the context (in
particular, the other branch of the if statement had the unit type), the
type inference for that particular program would assign it a value of ()
so that the type checking succeeds.
> How about, instead of saying "'xs' has a type of [()], and
> its value is [ () , _|_ , _|_ ]" why don't we say "'xs' has a
> type of [()], and the type of its values is [ () , _|_ , _|_ ]"?
Well, because the definition of a list is that its values all have the
same type. If xs has type [()], then any value of xs has the type (),
regardless of what the actual value is.
> It seems like the source of the problem you've identified
> is laziness, not bottom.
Absolutely. Bottom is part of the solution, not the problem. The
problem is that it's messy to specify language semantics in terms of a
model of behavior, and we'd prefer to do it with a simpler model. Lazy
evaluation, as is commonly the case, does indeed force the issue by
making a real semantics in terms of behavior nearly impossible.
--
Chris Smith
| |
| Chris Smith 2007-05-07, 7:04 pm |
| Matthias Blume <find@my.address.elsewhere> wrote:
> For certain definitions of purity (in particular, if you consider
> non-termination an effect), yes.
>
> On the other hand, the simply typed lambda calculus is pure, and so is
> F2, among others.
So, by definition, no general purpose programming language is pure?
Perhaps this is a useful definition in logic. How would it be useful in
talking about programming languages?
--
Chris Smith
| |
| rossberg@ps.uni-sb.de 2007-05-07, 7:04 pm |
| On 7 Mai, 17:09, Chris Smith <cdsm...@twu.net> wrote:
>
> So, by definition, no general purpose programming language is pure?
> Perhaps this is a useful definition in logic. How would it be useful in
> talking about programming languages?
It is useful when applied to individual functions or expressions. Two
examples:
1. Program transformations. Because evaluation order does not matter,
pure expressions (in the sense above) allow much more general
transformations (and thus optimizations). In particular, the compiler
could compute them at compile time.
2. Dependent Typing. When terms can be constituents of types then you
want to make sure that these terms are always terminating, as
otherwise type checking would be undecidable. A dependently typed PL
is thus likely to either ban non-terminating expressions altogether,
or at least restrict them to a non-termination monad (or,
equivalently, distinguish them via an effect system).
| |
| Marshall 2007-05-07, 7:04 pm |
| On May 7, 1:33 am, Ingo Menger <quetzalc...@consultant.com> wrote:
> On 7 Mai, 09:45, Marshall <marshall.spi...@gmail.com> wrote:
>
>
>
> Yes, it is a value, conceptually.
Well that's the question under discussion, isn't it? However
I maintain that bottom is a term in the type space, not
the value space. Saying it's a value is like saying list is
a value, or nat, or whatever.
> For it is not easy to describe the
> semantics of the language when you have exceptions, for example. If
> you have exceptions, then you must have control flow also, as well as
> a notion of *first* and *then*.
> With the imaginary value bottom (or undefined, if you prefer), it is
> easier, since you only have to specify that the result of a function
> that tries to deconstruct bottom is also bottom.
I'm much happier with calling it an "imaginary value."
>
> Sorry, that's nonsense. When the type of xs is [()] that means
> essentially that the type of all its elements is ().
Okay, then how about we say that the value of xs is
[(), undefined, undefined]?
Marshall
| |
| Marshall 2007-05-07, 7:04 pm |
| On May 7, 7:21 am, Chris Smith <cdsm...@twu.net> wrote:
> Marshall <marshall.spi...@gmail.com> wrote:
>
>
> Nothing at all. If you'd like to call the value "undefined" instead of
> "bottom", you won't run into any big problems except for communication.
Oh pooh, how is that a problem in communication? Certainly
it can't be as severe a problem as calling something a value
that is not a value. I found that quite a barrier to understanding,
and I have also seen a number of other people find it a barrier.
Terminology should be illuminating, not obfuscating.
>
>
> Well, undefined evaluates to bottom, of course! ;) Okay, so there are
> two perspectives again.
>
> From an implementation perspective, what happens is that undefined is
> initially left as an unevaluated expression or thunk. When you write
> (undefined + 1), that becomes another unevaluated expression. Now, say
> you want to do something that forces the value -- say, print it. Then
> print tries to calculate 'undefined + 1', and the (+) operator for the
> type will attempt to calculate the value of 'undefined'. The prelude
> function undefined will then terminate the program with an error that
> looks something like "********* Prelude: undefined".
I don't see how that's an implementation perspective. It sounded
like a discussion of the computational model. (Okay, maybe the
word "thunk" connotes implementation, but certainly laziness is
part of the computational model, so talking about unevaluatedness
is model-level.)
> (Actually, it will not necessarily terminate the whole program -- the IO
> monad has a mechanism to catch these. IIRC, it's so formally messy that
> the semantics of the language simply punts and describes that feature as
> acting in a non-deterministic way, leaving it to a quality of
> implementation issue to decide what to do.)
>
> So that's the implementation perspective. From the perspective of
> language semantics, though, things are much simpler. undefined has a
> value of bottom. The addition operator on bottom yields bottom, so
> (undefined + 1) also has a value of bottom. Finally, print bottom also
> evaluates to bottom, so the whole program (assuming that print is the
> whole program) evaluates to bottom. The semantics make no distinction
> between abrupt termination and infinite looping, so either is allowed as
> program behavior.
Allow me to propose a rewrite:
"undefined diverges. The addition operator on undefined diverges,
so (undefined + 1) also diverges. Finally, print undefined
also diverges, so the whole program (assuming that print is
the whole program) diverges."
Is there anything objectionable in that? Does it say the
same thing?
>
> Ah, but the whole point is that it acts exactly like a value, unless you
> are looking from an implementation standpoint. What definition of value
> are you looking out for, which is diluted here?
How about "member of a set?"
And anyway, saying "acts like a value" is a lot different
than saying "is a value."
>
>
>
> But that is precisely the problem that's being solved. You're trying to
> talk about behavior, but we'd like to avoid talking about behavior in
> specifying the semantics. This is important because the actual behavior
> of a language that does lazy evaluation is very difficult to predict or
> describe. It becomes very useful to have a simple way to describe the
> ultimate result, in a way that doesn't require tracing through the
> actual behavior of the program.
>
>
> The unit type has two values: () and bottom. In this case, the value of
> those terms is bottom, rather than ().
I strongly object. The unit type has one value. The unit type
has two subtypes, the unit type and bottom. The bottom type
has no values.
And if we go down that path saying something is a value that
is not a value, where does it end? Is there a type with only
one value? Is there a type with no values? Does the type
with no values have bottom as a value? Have all our boolean
operators become 3 valued now? Does
bottom op <anything> = bottom
always hold, or do we have to start considering that
true | bottom might be true? If not, then we have broken
a boolean invariant. Trust me, you *don't* want to end up
in 3VL land. And you still have to deal with infinite loops.
> I'm realizing my types may have been a little misleading. Those were
> the inferred types of expressions in this particular context. The
> general type of undefined is (forall a. a), which means that it can be a
> value of any type, without restriction. Because of the context (in
> particular, the other branch of the if statement had the unit type), the
> type inference for that particular program would assign it a value of ()
> so that the type checking succeeds.
Yes, I got that. Which works for me, since in the type lattice:
forall x: least_upper_bound(x, bottom) = x
>
> Well, because the definition of a list is that its values all have the
> same type. If xs has type [()], then any value of xs has the type (),
> regardless of what the actual value is.
Okay.
>
> Absolutely. Bottom is part of the solution, not the problem. The
> problem is that it's messy to specify language semantics in terms of a
> model of behavior, and we'd prefer to do it with a simpler model. Lazy
> evaluation, as is commonly the case, does indeed force the issue by
> making a real semantics in terms of behavior nearly impossible.
The solution is worse than the problem!
Any general computational model has to deal with divergence.
Marshall
| |
| Marshall 2007-05-07, 7:04 pm |
| On May 7, 7:21 am, Chris Smith <cdsm...@twu.net> wrote:
> Marshall <marshall.spi...@gmail.com> wrote:
>
> Nothing at all. If you'd like to call the value "undefined" instead of
> "bottom", you won't run into any big problems except for communication.
You mean, call the *effect* undefined.
I forgot to mention this:
"The warm fuzzy feeling you get when you've persuaded
your program to live in a total programming language
should not be underestimated. It's a strong static
guarantee-you can say that you've written a function
without having to pretend that _|_ is a value."
>From "Why Dependent Types Matter" --McBride et al
http://www.e-pig.org/downloads/ydtm.pdf
I think it was on this very newsgroup that I first heard
the idea of treating nontermination as an effect.
Marshall
| |
| Philippa Cowderoy 2007-05-07, 7:04 pm |
| On Mon, 7 May 2007, Marshall wrote:
> Well that's the question under discussion, isn't it? However
> I maintain that bottom is a term in the type space, not
> the value space. Saying it's a value is like saying list is
> a value, or nat, or whatever.
>
You seem to be confusing the bottom type (that is, the "least" type in the
subtyping hierarchy) with the bottom value (the one with the "least"
information). The value bottom is normally the only thing that inhabits
the type bottom, and a non-terminating value denotes the value bottom.
--
flippa@flippac.org
Ivanova is always right.
I will listen to Ivanova.
I will not ignore Ivanova's recomendations.
Ivanova is God.
And, if this ever happens again, Ivanova will personally rip your lungs out!
| |
| Marshall 2007-05-07, 7:04 pm |
| On May 7, 1:24 pm, Philippa Cowderoy <fli...@flippac.org> wrote:
> On Mon, 7 May 2007, Marshall wrote:
>
> You seem to be confusing the bottom type (that is, the "least" type in the
> subtyping hierarchy) with the bottom value (the one with the "least"
> information). The value bottom is normally the only thing that inhabits
> the type bottom, and a non-terminating value denotes the value bottom.
Having a different model, or using different terminology, is
not the same thing as being . I understand the denotation
of all that you wrote above, however I have objections.
Marshall
| |
| Philippa Cowderoy 2007-05-07, 7:04 pm |
| On Mon, 7 May 2007, Marshall wrote:
> On May 7, 1:24 pm, Philippa Cowderoy <fli...@flippac.org> wrote:
>
> Having a different model, or using different terminology, is
> not the same thing as being . I understand the denotation
> of all that you wrote above, however I have objections.
>
I wrote "seem to be confusing..." for a reason. The only objection that
actually seems to make any sense so far is to the overloading caused by
having two bottoms for two structures being discussed though - and in
practice there's a notational difference between the two when it matters.
Your use of undefined as a value makes no difference whatsoever, indeed
it's _|_ by definition - and the notion of a hierarchy of informational
content makes an awful lot of sense in a language like haskell. So where's
the issue?
--
flippa@flippac.org
Performance anxiety leads to premature optimisation
| |
| Marshall 2007-05-07, 10:03 pm |
| On May 7, 3:53 pm, Philippa Cowderoy <fli...@flippac.org> wrote:
> On Mon, 7 May 2007, Marshall wrote:
>
n the[color=darkred]
ts[color=darkred]
>
>
> I wrote "seem to be confusing..." for a reason.
Uh, I must not be getting it.
And while we're at it, how can a *value* be nonterminating?
A value is not a computation. Evaluating an expression might
be nonterminating, but a value can never terminate nor
diverge because a value can never execute. (You might say
that a lambda expression is both a value and something that
can execute, but it's not the lambda that executes; it's the
apply operator, which is not a value.)
> The only objection that
> actually seems to make any sense so far is to the overloading caused by
> having two bottoms for two structures being discussed though - and in
> practice there's a notational difference between the two when it matters.
Perhaps I'm unfamiliar with the notational difference. I am used to
seeing this glyph: _|_ or =E2=8A=A5 or what have you, used to describe the
bottom of a lattice in a math context and used to describe
undefinedness
in a CS context. The two terms can be completely consistent,
but not if we are going to say things that translate into talking
about the member of the empty set.
Doesn't it bother you to hear that the *unit* type contains *two*
values? To me it grates as much as hearing 1=3D2. In fact,
those two are really the same claim. On the other hand
if we say an expression of the unit type might return the
unit value or might diverge, there is no problem.
Would you consider 1/0 =3D bottom? Would you consider it
nonterminating? Would you consider it undefined? Only
the last of these makes sense to me.
> Your use of undefined as a value makes no difference whatsoever, indeed
> it's _|_ by definition - and the notion of a hierarchy of informational
> content makes an awful lot of sense in a language like haskell.
By hierarchy do you mean specifically lattice?
Note I wasn't saying undefined was a value; I was saying
"undefined" as in having no definition.
> So where's the issue?
I hope I have clarified.
> Performance anxiety leads to premature optimisation
Love it!
Marshall
| |
| Philippa Cowderoy 2007-05-07, 10:03 pm |
| | |
| Geoffrey 2007-05-08, 4:09 am |
| On May 7, 10:00 am, Matthias Blume <f...@my.address.elsewhere> wrote:
>
> Explicitly manipulating continuations (e.g., via call/cc) makes a
> program impure.
Why does the use of explicit continuations make a program impure?
After all, any program written to use call/cc can be transformed to
CPS style and be pure. So what makes it impure before the
transformation?
| |
| Matthias Blume 2007-05-08, 4:09 am |
| Geoffrey <geoffrey.marchant@gmail.com> writes:
> On May 7, 10:00 am, Matthias Blume <f...@my.address.elsewhere> wrote:
>
> Why does the use of explicit continuations make a program impure?
> After all, any program written to use call/cc can be transformed to
> CPS style and be pure. So what makes it impure before the
> transformation?
Every program that uses a mutable store can also be transformed into a
pure (store-passing) program.
One litmus test for purity is this: For e to be pure, any expression
let x = e in e'
where x does not occur free in e' must be equivalent to e'. If e can,
e.g., invoke a previously captured continuation, this is not the case.
Similarly, if e does not terminate, it is also not the case.
Matthias
| |
| Dirk Thierbach 2007-05-08, 4:09 am |
| Marshall <marshall.spight@gmail.com> wrote:
> On May 7, 1:33 am, Ingo Menger <quetzalc...@consultant.com> wrote:
[color=darkred]
> Well that's the question under discussion, isn't it?
No, it's not under discussion. There are (at least) two ways
to use "bottom": To denote the least type in a (say) Lisp type
system, or to denote the least semantic value of the interpretation
of a type in denotational semantics. If you don't like to google,
http://en.wikibooks.org/wiki/Haskel...ional_semantics
has an introduction, for example.
> However I maintain that bottom is a term in the type space, not the
> value space.
Just because you've seen only one usage, and not the other, doesn't
mean that the usage you know about is the only one.
- Dirk
| |
| Joachim Durchholz 2007-05-08, 4:09 am |
| Marshall schrieb:
> And while we're at it, how can a *value* be nonterminating?
> A value is not a computation.
Exactly.
_|_ is the value defined for nonterminating computations.
That definition is mathematical, and not implemented in any real-world
run-time system.
It does not serve any useful purpose for programs written in the
language (which will never reach a point where that value is ever
accessible), but it can be useful to simplify reasoning over properties
of the language or the programs written in it.
> Perhaps I'm unfamiliar with the notational difference. I am used to
> seeing this glyph: _|_ or ⊥ or what have you, used to describe the
> bottom of a lattice in a math context and used to describe
> undefinedness
> in a CS context. The two terms can be completely consistent,
They are, I'm sure :-)
> Would you consider 1/0 = bottom?
Yes.
> Would you consider it nonterminating?
Nontermination is just one case of "does not return a value".
Bottom is really an umbrella term for all cases where a function does
not evaluate to a value, such as: endless looping, undefined behaviour,
throwing an exception, and aborting the computation.
> Would you consider it undefined? Only
> the last of these makes sense to me.
The language can define that such situations result in undefined behaviour.
I think part of the confusion is that we have two kinds of "undefined"
here. One is stuff that's not defined by the language (a specification
bug); the other is if a language definition explicitly defines that the
result of certain constructs is undefined, but the construct is legal
anyway (sometimes useful, unavoidable in the presence of recursion
and/or loops, has dubious consequences).
>
> By hierarchy do you mean specifically lattice?
>
> Note I wasn't saying undefined was a value; I was saying
> "undefined" as in having no definition.
_|_ is a fiction in a sense. It's the value you assign to an expression
that does not have a value inside the language rules; some lines of
reasoning are easier that way.
(It's similar to the NaN's of floating-point arithmetic. Depending on
context, they are either an error indicator or a perfectly valid result;
there's no Right nor Wrong in this matter, it's a question of what
results you are interested in.)
Hope I have helped.
Regards,
Jo
| |
| Markus E Leypold 2007-05-08, 8:04 am |
|
Marshall <marshall.spight@gmail.com> writes:
>
> What's wrong with using "undefined" everywhere you used
> "bottom" above?
That "bottom" is established terminology in this case? Just a thought.
> My expectation would be that either evaluating undefined
> is an exceptional condition, or that undefined propagates
There is no "exceptional condition" in a purely functional
semantics. Just values of expressions.
> Assuming I accept your term "action", then yes, and that's
> the *advantage* of using that term. You're trying to pick
> a value from the empty set; that's not gonna work.
So how is "not gonna work" described when talking about evaluation in
a functional semantics?
> It seems like the source of the problem you've identified
> is laziness, not bottom.
The problem is not laziness, but impurity. Purity is the solution
:-). And there is no problem with bottom. At least not where you're
looking for it.
Regards -- Markus
| |
| Markus E Leypold 2007-05-08, 8:04 am |
|
Marshall <marshall.spight@gmail.com> writes:
> On May 7, 7:21 am, Chris Smith <cdsm...@twu.net> wrote:
>
> Oh pooh, how is that a problem in communication? Certainly
> it can't be as severe a problem as calling something a value
> that is not a value.
So -- what is a "value"? Bottom (_|_) in the case we're talking about,
is an element in the semantic domain (hope I got that right) of every
expression in certain denotational semantics. If elements of sets (we
are basically talking mathematics here) qualify as valuesm then it is
a value. If on the other side you accept as values are only things
that turn up during evaluation of an expression in an interpreter (or
any other implementation of a language), then you're missing a point
here: _|_ is basically used in describing language semantics (i.e. the
meaning of language constructs, not the _process_ of evaluation which
is a where time and temporal order come in).
Regards -- Markus
| |
| Markus E Leypold 2007-05-08, 8:04 am |
|
Marshall <marshall.spight@gmail.com> writes:
> Doesn't it bother you to hear that the *unit* type contains *two*
No.
> values? To me it grates as much as hearing 1=2. In fact,
> those two are really the same claim. On the other hand
> if we say an expression of the unit type might return the
> unit value or might diverge, there is no problem.
How do you describe "might diverge" in a mathematical notation based
on functions and sets (i.e. denotational semantics)?
> Note I wasn't saying undefined was a value; I was saying
> "undefined" as in having no definition.
But f x = f x has a definition. It's an expression. So what happens
when it meets the evaluator and how do you describe it?
Regards -- Markus
| |
| Markus E Leypold 2007-05-08, 8:04 am |
|
Marshall <marshall.spight@gmail.com> writes:
> On May 7, 3:53 pm, Philippa Cowderoy <fli...@flippac.org> wrote:
>
> Uh, I must not be getting it.
>
> And while we're at it, how can a *value* be nonterminating?
> A value is not a computation. Evaluating an expression might
> be nonterminating, but a value can never terminate nor
> diverge because a value can never execute. (You might say
> that a lambda expression is both a value and something that
> can execute, but it's not the lambda that executes; it's the
> apply operator, which is not a value.)
Denotational semantics. Do yourself a favour and read up on
denotational semantics first, then consider how you'd describe a
non-terminating computation (or an implementation dependent abortion
of computation).
My guess is, that before you lay some groundwork here, all attempts to
communicate will be in vain.
Regards -- Markus
| |
| Marshall 2007-05-09, 4:11 am |
| On May 7, 7:43 pm, Philippa Cowderoy <fli...@flippac.org> wrote:
> On Tue, 7 May 2007, Marshall wrote:
>
>
>
> Usually if a distinction needs making then the type is Bottom or otherwise
> fits in with typographical conventions for types.
Hmmm. I haven't run in to that. (Or if I have I haven't been
paying enough attention!) Thanks.
Most of my reading has been on operational semantics, and
the one Haskell book I've read (Craft of Functional Programming)
doesn't mention denotational semantics or bottom or make
more than a passing mention of undefined.
It seems I have some reading to do.
Marshall
| |
| Marshall 2007-05-09, 4:11 am |
| On May 8, 12:38 am, Joachim Durchholz <j...@durchholz.org> wrote:
>
> Hope I have helped.
Yes; thanks.
Marshall
| |
| Marshall 2007-05-09, 4:11 am |
| On May 7, 6:28 pm, Markus E Leypold >
> My guess is, that before you lay some groundwork here, all attempts to
> communicate will be in vain.
Yeah, I think you hit the nail on the head with that.
Marshall
| |
| Ben Rudiak-Gould 2007-05-09, 4:11 am |
| Joachim Durchholz wrote:
> In this definition, it does make sense to have something called
> "bottom". It is applied for those equation sets that either have no
> solution, or have "too many" solutions.
Actually bottom is only used for an underconstrained answer (too many
solutions), and top is used for an overconstrained answer (no solutions). So
in your first example,
> f x = f (x - 1)
> f 0 = 0
> f 1 = 1
f x is top, not bottom.
(Except that in Haskell semantics, only the first pattern counts since it
subsumes the other two, so the definition is equivalent to just f x = f
(x-1) and f x is indeed _|_.)
-- Ben
|
|
|
|
|