Talk:Bottom type

A bunch of stuff was removed with the comment "don't make the intro CS-centric, please." However, the only cited references is Pierce's "Types and Programming Languages." I'm okay with separating CS specific view points from a more general logical notion of the bottom type - but we need references. Also, in the process of removing the CS view point from the lede a lot of good stuff was removed including references to the top type and unit types. I'm reinstating some of that stuff, but will shuffle it around a bit. —Preceding unsigned comment added by 70.187.129.176 (talk) 21:31, 24 October 2008 (UTC)[reply]

Common sense!!!

Whoever doesn't understand the need for this edit should WAKE UP! Michael Hardy (talk) 21:48, 5 April 2009 (UTC)[reply]

How are null references bottom?

Article says:

Bot is a natural type for the "null pointer" value (a pointer which does not point to any object) of languages like Java: in Java, null is a value of every reference type, which is just the same as saying "null ∈ Bot."

This seems to be wrong in several ways: First, bottom is defined to be a subtype of every type, not merely a subtype of every reference type. Second, nothing about the definition of bottom says that it is the unique subtype of all types. Third, bottom is a type which has no values, so the null pointer cannot be a value of type bottom. (It can be a value of a unit type.)

Can anyone explain why the reference believes otherwise? --FOo (talk) 06:04, 30 January 2010 (UTC)[reply]

Actually the reference said List(Bot) for the null pointer, and talked about using Bot for uninitialized pointers. Don't know if that helps but I might as well fix the article to be say what it cites. Dmcq (talk) 10:35, 30 January 2010 (UTC)[reply]

Pierce is presumably assuming a type system with no "primitive" distinction, it's not a law of nature that there be one. The real challenge is making the null value behave like a bottom so that for any (strict) f, f(null) = ⊥. In many languages null can be compared using equality or a special isnull operator. —Preceding unsigned comment added by 204.14.239.166 (talk) 22:21, 26 July 2010 (UTC)[reply]

At the very least, the present text

List[Bot] is a natural type for the "null pointer" value [...]

is not a correct citation from Pierce. The original paper says:

Bot is a natural type for the "uninitialized pointer" value of languages like Java: saying that "null has every type" is just the same as "null \in Bot."\footnote{Strictly speaking, Java's null value has all \emph{object} types, but not types like integer or array. The language studied here does not capture this refinement.}

(Please excuse the TeX commands; I am not familiar with Wiki markups.) Esumii (talk) 12:30, 27 March 2013 (UTC)[reply]

1. In the paper, Pierce chooses to disregard non-reference types for pedagogical purposes. AFAIK, Java's type system doesn't have a dedicated type "Null". If it did, Null would indeed not be a "minimal type" in - just a "minimal reference type". 2. The bottom type is not necessarily unique. A type system may or may not have a minimal type, but if it has two, they are both subtypes of each other by definition. 3. Bottom may certainly have values. But if the type system has *any* empty types, the bottom type must be a subtype and therefore must also be empty. — Preceding unsigned comment added by 174.20.133.198 (talk) 19:26, 23 October 2022 (UTC)[reply]

removed relation to halting problem

I removed this text:

In a Turing-complete language, it is not generally possible to assert that a function will halt and return rather than looping forever. For instance, a function whose type states that it will return an integer may in fact not return. In order to theoretically account for this possibility, the bottom type is considered a subtype of integer (and, indeed, all types): a function declared as returning integer does not violate the type system if it instead loops forever.

For many given functions, the halting problem is easily solved, but that's irrelevant. The bottom type would describe a function that does not return, which is not only easier to verify, but very useful to specify. Anyway, how did integers enter the discussion? Potatoswatter (talk) 07:04, 28 August 2010 (UTC)[reply]

The text was completely correct and should not have been removed; OTOH, nothing about the comment above is correct ... e.g., the halting problem is unsolvable; that some functions can be shown to halt is indeed irrelevant. (The deleted comment correctly states that it is not generally possible to determine whether a function halts--which is another way of saying that the halting problem is not solvable. There is not a separate "halting problem" for each function, as the person above seems to think.) And the answer to the question of how integers entered the discussion is obvious from the text "For instance ...". Editors with no understanding of a subject and lacking basic reading comprehension should obtain consensus before removing material. -- Jibal (talk) 19:36, 17 April 2022 (UTC)[reply]

Article is incorrect

Even bottom types always have exactly one value, namely whatever state a bottom typed entity is in. — Preceding unsigned comment added by 82.139.81.0 (talk) 17:50, 17 November 2012 (UTC)[reply]

No, the article is not incorrect, and the comment here is gibberish ... there is no state that an "entity" with type Bot can be in. And if bottom typed entities could be in various states, then Bot would have more than one value. In any case, this page is not for the expression of the random beliefs of uninformed editors ... if you have a citation of a reliable source supporting your claim then provide it. -- Jibal (talk) 19:47, 17 April 2022 (UTC)[reply]

Rust's "!" is not quite bottom

Rust has removed the bottom type. See this issue: https://github.com/rust-lang/rust/issues/14973 and this pull request: https://github.com/rust-lang/rust/pull/17603 and also this related issue, for fallout: https://github.com/rust-lang/rust/issues/20172

It's been replaced by the notion of "diverging functions" which never return. This includes functions which panic and functions which loop forever or issue a process abort.

Haskell - Data.Void is one of at least two approaches to bottom

See - https://wiki.haskell.org/Bottom. I don't have enough expertise on this to disambiguate between the two. Furiousviki (talk) 09:24, 12 April 2024 (UTC)[reply]