In type theory, the empty type or absurd type, typically denoted is a type with no terms. Such a type may be defined as the nullary coproduct (i.e. disjoint sum of no types). It may also be defined as the polymorphic type For any type , the type is defined as . As the notation suggests, by the Curry–Howard correspondence, a term of type is a false proposition, and a term of type is a disproof of proposition P. A type theory need not contain an empty type. Where it exists, an empty type is not generally unique. For instance, is also uninhabited for any inhabited type .
Attributes | Values |
---|
rdfs:label
| |
rdfs:comment
| - In type theory, the empty type or absurd type, typically denoted is a type with no terms. Such a type may be defined as the nullary coproduct (i.e. disjoint sum of no types). It may also be defined as the polymorphic type For any type , the type is defined as . As the notation suggests, by the Curry–Howard correspondence, a term of type is a false proposition, and a term of type is a disproof of proposition P. A type theory need not contain an empty type. Where it exists, an empty type is not generally unique. For instance, is also uninhabited for any inhabited type . (en)
|
dcterms:subject
| |
Wikipage page ID
| |
Wikipage revision ID
| |
Link from a Wikipage to another Wikipage
| |
dbp:wikiPageUsesTemplate
| |
has abstract
| - In type theory, the empty type or absurd type, typically denoted is a type with no terms. Such a type may be defined as the nullary coproduct (i.e. disjoint sum of no types). It may also be defined as the polymorphic type For any type , the type is defined as . As the notation suggests, by the Curry–Howard correspondence, a term of type is a false proposition, and a term of type is a disproof of proposition P. A type theory need not contain an empty type. Where it exists, an empty type is not generally unique. For instance, is also uninhabited for any inhabited type . If a type system contains an empty type, the bottom type must be uninhabited too, so no distinction is drawn between them and both are denoted . (en)
|
prov:wasDerivedFrom
| |
page length (characters) of wiki page
| |
foaf:isPrimaryTopicOf
| |
is Link from a Wikipage to another Wikipage
of | |
is foaf:primaryTopic
of | |