Bottom type | EPFL Graph Search

Are you an EPFL student looking for a semester project?

Work with us on data science and visualisation projects, and deploy your project as an app on top of GraphSearch.

In type theory, a theory within mathematical logic, the bottom type of a type system is the type that is a subtype of all other types. Where such a type exists, it is often represented with the up tack (⊥) symbol. When the bottom type is empty, a function whose return type is bottom cannot return any value, not even the lone value of a unit type. In such a language, the bottom type may therefore be known as the zero or never type. In the Curry–Howard correspondence, an empty type corresponds to falsity. In subtyping systems, the bottom type is a subtype of all types. It is dual to the top type, which spans all possible values in a system. If a type system is sound, the bottom type is uninhabited and a term of bottom type represents a logical contradiction. In such systems, typically no distinction is drawn between the bottom type and the empty type, and the terms may be used interchangeably. If the bottom type is inhabited, its terms[s] typically correspond to error conditions such as undefined behavior, infinite recursion, or unrecoverable errors. In Bounded Quantification with Bottom, Pierce says that "Bot" has many uses: In a language with exceptions, a natural type for the raise construct is raise ∈ exception -> Bot, and similarly for other control structures. Intuitively, Bot here is the type of computations that do not return an answer. Bot is useful in typing the "leaf nodes" of polymorphic data structures. For example, List(Bot) is a good type for nil. 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, the null type is the universal subtype of reference types. null is the only value of the null type; and it can be cast to any reference type. However, the null type is not a bottom type as described above, it is not a subtype of int and other primitive types. A type system including both Top and Bot seems to be a natural target for type inference, allowing the constraints on an omitted type parameter to be captured by a pair of bounds: we write S

About this result

This page is automatically generated and may contain information that is not correct, complete, up-to-date, or relevant to your search query. The same applies to every other page on this website. Please make sure to verify the information with EPFL's official sources.

Related concepts (3)

Void type

The void type, in several programming languages derived from C and Algol68, is the return type of a function that returns normally, but does not provide a result value to its caller. Usually such functions are called for their side effects, such as performing some task or writing to their output parameters. The usage of the void type in such context is comparable to procedures in Pascal and syntactic constructs which define subroutines in Visual Basic. It is also similar to the unit type used in functional programming languages and type theory.

Haskell

Haskell (ˈhæskəl) is a general-purpose, statically-typed, purely functional programming language with type inference and lazy evaluation. Designed for teaching, research, and industrial applications, Haskell has pioneered a number of programming language features such as type classes, which enable type-safe operator overloading, and monadic input/output (IO). It is named after logician Haskell Curry. Haskell's main implementation is the Glasgow Haskell Compiler (GHC).

Unit type

In the area of mathematical logic and computer science known as type theory, a unit type is a type that allows only one value (and thus can hold no information). The carrier (underlying set) associated with a unit type can be any singleton set. There is an isomorphism between any two such sets, so it is customary to talk about the unit type and ignore the details of its value. One may also regard the unit type as the type of 0-tuples, i.e. the of no types. The unit type is the terminal object in the of types and typed functions.