Верхний тип в логике и информатике

Universal type in logic and computer science
In mathematical logic and computer science, some type theories and type systems include a top type that is commonly denoted with top or the symbol ⊤. The top type is sometimes called also universal type, or universal supertype as all other types in the type system of interest are subtypes of it, and in most cases, it contains every possible object of the type system. It is in contrast with the bottom type, or the universal subtype, which every other type is supertype of and it is often that the type contains no members at all.

Languages that are not object oriented usually have no universal supertype, or subtype polymorphism support. While Haskell purposefully lacks subtyping, it has several other forms of polymorphism including parametric polymorphism. The most generic type class parameter is an unconstrained parameter a (without a type class constraint). In Rust, <T: ?Sized> is the most generic parameter (<T> is not, as it implies the Sized trait by default). The top type is used as a generic type, more so in languages without parametric polymorphism. For example, before introducing generics in Java 5, collection classes in the Java library (excluding Java arrays) held references of type Object. In this way, any non intrinsic type could be inserted into a collection. The top type is also often used to hold objects of unknown type. The top type may also be seen as the implied type of non statically typed languages. Languages with run time typing often provide downcasting (or type refinement) to allow discovering a more specific type for an object at run time. In C++, downcasting from void * cannot be done in a safe way, where failed downcasts are detected by the language run time. In languages with a structural type system, the empty structure serves as a top type. For example, objects in OCaml are structurally typed; the empty object type (the type of objects with no methods), < >, is the top type of object types. Any OCaml object can be explicitly upcasted to this type, although the result would be of no use. Go also uses structural typing; and all types implement the empty interface: interface {}, which has no methods, but may still be downcast back to a more specific type.

The notion of top is also found in propositional calculus, corresponding to a formula which is true in every possible interpretation. It has a similar meaning in predicate calculus. In description logic, top is used to refer to the set of all concepts. This is intuitively like the use of the top type in programming languages. For example, in the Web Ontology Language (OWL), which supports various description logics, top corresponds to the class owl:Thing, where all classes are subclasses of owl:Thing. (the bottom type or empty set corresponds to owl:Nothing).