Skip to content

Instantly share code, notes, and snippets.

@GregRos

GregRos/BottomTypeExamples.md

Last active August 29, 2015 14:17
Show Gist options
  • Star 0 You must be signed in to star a gist
  • Fork 0 You must be signed in to fork a gist
  • Save GregRos/03cae0af26d70682f868 to your computer and use it in GitHub Desktop.
Save GregRos/03cae0af26d70682f868 to your computer and use it in GitHub Desktop.
Download ZIP
Raw
BottomTypeExamples.md

Scala

Scala bottom type

scala.Nothing

Common Lisp

Common Lisp

Wikipedia

Wiki definition

Type Theory

Type Theory (unattributed)

"Types and Programming Languages, Benjamin C. Pierce, pg 191-192, Sec 15.4:

The first thing to notice is that Bot is empty—there are no closed values of type Bot. If there were one, say v, then the subsumption rule... [proof]... The syntax makes it clear that v cannot be both a function and a record, and so assuming that [v is of type Bot] has led us to a contradiction

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment