Would you shed light on "undefined values" please?
Hi Folks, In this book [1] the author defines the term "bottom": In order that we can say that, without exception, every syntactically well-formed expression denotes a value, it is convenient to introduce a special symbol (upside down T), pronounced 'bottom', to stand for the undefined value of a particular type. In particular, the value of infinity is the undefined value (bottom) of type Integer, and 1/0 is the undefined value (bottom) of type Float. Hence we can assert that 1/0 = bottom. He defines infinity as this: infinity :: Integer infinity = infinity + 1 The author says this when discussing the Bool datatype: It follows that there are not two but three Boolean values, namely False, True, and bottom. In fact, every datatype declaration introduces an extra anonymous value, the undefined value of the datatype. What is the undefined value (bottom) of type Bool? What is the undefined value (bottom) of type String? If I create my own datatype: data MyBool = F | T What is the undefined value (bottom) of type MyBool? I am not clear why "bottom" is an important concept. Would you explain please? /Roger [1] Introduction to Functional Programming using Haskell by Richard Bird
Howdy,
I am not clear why "bottom" is an important concept. Would you explain please?
I've been getting into this myself lately. Here's what I've been reading: http://en.wikibooks.org/wiki/Haskell/Denotational_semantics http://blog.ezyang.com/2010/12/hussling-haskell-types-into-hasse-diagrams/ Let us know if you find anything else! Arlen
Hi Roger,
As Bird says himself in your second quotation, every datatype
declaration introduces an extra anonymous value, the undefined value
of the datatype."
In haskell, this is true. This special 'bottom' value is actually
represented by the value 'undefined'. You can see this definition in
the haskell libraries:
http://hackage.haskell.org/packages/archive/base/latest/doc/html/Prelude.htm...
It's rather unimportant that the documentation says 'undefined is a
special case of error' - the interesting part about undefined *is its
type*
undefined :: a
which is rather strange. This would seem to indicate that undefined
can in fact be used in any place to represent any concrete type.
That's correct. In fact, this type merely means that undefined is an
inhabitant of *every* possible type. That is, all of the following
values typecheck, because 'undefined' inhabits all types:
v1 = undefined :: Int
v2 = undefined :: String
v3 = undefined :: Bool
v4 = undefined :: MyBool -- your version of Bool
All types in haskell have 'bottom' as one of their members. But since
haskell is lazy, what happens if you try to evaluate an 'undefined'?
You get an error and the program terminates prematurely. But every
type in haskell has at least a single inhabitant: bottom. This is
true, even with 'empty' data types:
data Foo -- no constructors
Indeed, the type 'Foo' has no values/constructors that inhabit it! So
there is no explicit value/constructor you could use to construct a
value of type 'Foo.' But despite the lack of constructors, there is
still a way to construct a value of type 'Foo' - bottom:
v5 = undefined :: Foo
As a theoretical concept bottom is, I believe, tied a bit more into
denotational semantics and in particular, domain theory (someone
please correct me if I am wrong.) You can find a good bit of stuff
about the formal semantics of programming languages - including domain
theory - in a book like one by Glenn Winksel, "The Formal Semantics of
Programming Languages" and many others. There are also various
writings that discuss such topics with specific relation to Haskell,
such as the links Arlen Cuss gave.
On Thu, Jun 23, 2011 at 5:35 PM, Costello, Roger L.
Hi Folks,
In this book [1] the author defines the term "bottom":
In order that we can say that, without exception, every syntactically well-formed expression denotes a value, it is convenient to introduce a special symbol (upside down T), pronounced 'bottom', to stand for the undefined value of a particular type. In particular, the value of infinity is the undefined value (bottom) of type Integer, and 1/0 is the undefined value (bottom) of type Float. Hence we can assert that 1/0 = bottom.
He defines infinity as this:
infinity :: Integer infinity = infinity + 1
The author says this when discussing the Bool datatype:
It follows that there are not two but three Boolean values, namely False, True, and bottom. In fact, every datatype declaration introduces an extra anonymous value, the undefined value of the datatype.
What is the undefined value (bottom) of type Bool?
What is the undefined value (bottom) of type String?
If I create my own datatype:
data MyBool = F | T
What is the undefined value (bottom) of type MyBool?
I am not clear why "bottom" is an important concept. Would you explain please?
/Roger
[1] Introduction to Functional Programming using Haskell by Richard Bird
_______________________________________________ Beginners mailing list Beginners@haskell.org http://www.haskell.org/mailman/listinfo/beginners
-- Regards, Austin
On Thu, Jun 23, 2011 at 18:35, Costello, Roger L.
It follows that there are not two but three Boolean values, namely False, True, and bottom. In fact, every datatype declaration introduces an extra anonymous value, the undefined value of the datatype.
What is the undefined value (bottom) of type Bool?
What is the undefined value (bottom) of type String?
bottomString = bottomString ++ bottomString
is one way to formulate it. More generally
undefined :: a undefined = let x = x in x -- a computation that never produces a value
The reason _|_ is significant is that a type that admits it as a value can be computed lazily. If your type does not allow for _|_ then it is strict; anything that touches it in any way when it is invalid (an infinite loop, exception, or other effect that is not producing an actual value; this is the effective definition of "bottom") will fail immediately. A "lifted" type (one which allows _|_) will only loop / throw an exception / dump core / set the building on fire / whatever when something actually demands that value. Some practical uses of this: - since _|_ inhabits every lifted type, the definition of "undefined" that I provided above can be used as a stub during development, and will always typecheck; - similarly, the computation
error :: String -> a
(whose implementation can't be expressed within the language) throws a runtime exception, and can be used anywhere that a lifted type is permitted (anywhere, in standard Haskell). - "undefined" in particular is useful as a placeholder when only the type is significant. See "asTypeOf" as an example of this. (It could be argued that this case really wants "_" to function as a pseudo-value instead of just as a pattern, but that has its own problems.)
If I create my own datatype:
data MyBool = F | T
What is the undefined value (bottom) of type MyBool?
_|_ is not, in general, expressible within Haskell itself except in terms of infinite loops or runtime exceptions; it's not like SQL's NULL, it's a "not-value". In this case, the easy way to generate a bottom for your type is
myBoolBottom :: MyBool myBoolBottom = let x = x in x
(Remember that "let" is recursive in Haskell; the above expression will try to compute "x", which will try to compute "x", which will ... in reality, the GHC runtime will notice that the computation for "x" immediately re-enters itself and will compute 'error "<<loop>>"' in its place, raising a runtime exception.) GHC and several other Haskell compilers support unlifted types, which are strict. Every program uses one, in fact; in GHC, IO is an unlifted tuple. The primary explicit use of them is UArray/STArray, which are the equivalent of arrays in strict languages. -- brandon s allbery allbery.b@gmail.com wandering unix systems administrator (available) (412) 475-9364 vm/sms
Brandon Allbery
The reason _|_ is significant is that a type that admits it as a value can be computed lazily. If your type does not allow for _|_ then it is strict;
That's actually not quite right. Strictness and bottom are only loosely related in that strictness is defined in terms of bottom. You get a concept of strictness once you have functions (value constructors with arguments are functions), otherwise it doesn't make much sense. They are related in that some expressions can yield defined values in nonstrict semantics, where they would give you bottom in strict ones, namely in this specific case: f ⊥ ≠ ⊥ In strict semantics this is impossible, because this is definitely a nonstrict function. Bottom arises, as soon as a language is total. This is related to the halting problem. Bottom is the value, which is never computed in the sense that it never results. Only nontotal languages (like Agda) can prevent bottom values from appearing. In other words, every type in Haskell is lifted and there is no way around that. The type of 'undefined' proves that. In fact you cannot express the undefined value in Agda. On the other hand in Haskell it's trivial to express: undefined :: a undefined = undefined Greets, Ertugrul -- nightmare = unsafePerformIO (getWrongWife >>= sex) http://ertes.de/
On Fri, Jun 24, 2011 at 08:13:26AM +0200, Ertugrul Soeylemez wrote:
Bottom arises, as soon as a language is total. This is related to the halting problem. Bottom is the value, which is never computed in the sense that it never results. Only nontotal languages (like Agda) can prevent bottom values from appearing.
That is a funny use of the word "total"; I think you mean "Turing-complete". "Total" is usually used of languages in which it is only possible to define total functions -- such as Agda. Haskell is non-total since it is possible to define non-total, i.e. partial, functions, which are undefined for some inputs. -Brent
Brent Yorgey
Bottom arises, as soon as a language is total. This is related to the halting problem. Bottom is the value, which is never computed in the sense that it never results. Only nontotal languages (like Agda) can prevent bottom values from appearing.
That is a funny use of the word "total"; I think you mean "Turing-complete". "Total" is usually used of languages in which it is only possible to define total functions -- such as Agda. Haskell is non-total since it is possible to define non-total, i.e. partial, functions, which are undefined for some inputs.
Indeed, i flipped the meanings. =) Greets, Ertugrul -- nightmare = unsafePerformIO (getWrongWife >>= sex) http://ertes.de/
Costello, Roger L. wrote:
In this book [1] the author defines the term "bottom":
In order that we can say that, without exception, every syntactically well-formed expression denotes a value, it is convenient to introduce a special symbol (upside down T), pronounced 'bottom', to stand for the undefined value of a particular type. In particular, the value of infinity is the undefined value (bottom) of type Integer, and 1/0 is the undefined value (bottom) of type Float. Hence we can assert that 1/0 = bottom.
He defines infinity as this:
infinity :: Integer infinity = infinity + 1
The author says this when discussing the Bool datatype:
It follows that there are not two but three Boolean values, namely False, True, and bottom. In fact, every datatype declaration introduces an extra anonymous value, the undefined value of the datatype.
What is the undefined value (bottom) of type Bool?
What is the undefined value (bottom) of type String?
If I create my own datatype:
data MyBool = F | T
What is the undefined value (bottom) of type MyBool?
I am not clear why "bottom" is an important concept. Would you explain please?
Bottom, _|_, is a little trick to do precisely what Bird said, namely "make every expression denote a value". As you know, in Haskell, you can reason about programs by comparing their values. For instance, we have 4+5 = 10-1 = length [0..8] = sum (replicate 3 3) because all these expressions denote the value 9, a number. But there are expressions that should be numbers, yet aren't. Examples: sum [1..] let loop = 2-loop in loop What value do they have? Certainly not 1 or 5 or some other number. We do want them to have a value, though, so we have to invent one: _|_ . More precisely, every expression that does not terminate denotes the value _|_. (Actually, we have to invent one for every type: _|_ :: String, _|_ :: Bool, _|_ :: MyBool, etc. because we can only compare values of the same type.) The rules for calculating with _|_ are presented here: http://en.wikibooks.org/wiki/Haskell/Denotational_semantics Best regards, Heinrich Apfelmus -- http://apfelmus.nfshost.com
participants (7)
-
Arlen Cuss -
austin seipp -
Brandon Allbery -
Brent Yorgey -
Costello, Roger L. -
Ertugrul Soeylemez -
Heinrich Apfelmus