StackOverflow2013

Note that there are some explanatory texts on larger screens.

plurals

PO
text
Body
copied!<p>You're muddying things a little bit regarding nontermination. Falsity is represented by <em>uninhabited types</em>, which by definition can't be non-terminating because there's nothing of that type to evaluate in the first place.</p> <p>Non-termination represents <em>contradiction</em>--an inconsistent logic. An inconsistent logic will of course <a href="http://en.wikipedia.org/wiki/Principle_of_explosion" rel="noreferrer">allow you to prove</a> <a href="http://xkcd.com/704/" rel="noreferrer">anything</a>, including falsity, however.</p> <p>Ignoring inconsistencies, type systems typically correspond to an <a href="http://en.wikipedia.org/wiki/Intuitionistic_logic" rel="noreferrer">intuitionistic logic</a>, and are by necessity <a href="http://en.wikipedia.org/wiki/Constructivism_(mathematics)" rel="noreferrer">constructivist</a>, which means certain pieces of classical logic can't be expressed directly, if at all. On the other hand this is useful, because if a type is a valid constructive proof, then a term of that type is a <em>means of constructing whatever you've proven the existence of</em>.</p> <p>A major feature of the constructivist flavor is that <strong>double negation</strong> is not equivalent to non-negation. In fact, negation is rarely a primitive in a type system, so instead we can represent it as implying falsehood, e.g., <code>not P</code> becomes <code>P -> Falsity</code>. Double negation would thus be a function with type <code>(P -> Falsity) -> Falsity</code>, which clearly is not equivalent to something of just type <code>P</code>.</p> <p>However, there's an interesting twist on this! In a language with parametric polymorphism, type variables range over all possible types, including uninhabited ones, so a fully polymorphic type such as <code>∀a. a</code> is, in some sense, almost-false. So what if we write double almost-negation by using polymorphism? We get a type that looks like this: <code>∀a. (P -> a) -> a</code>. Is that equivalent to something of type <code>P</code>? <strong>Indeed it is</strong>, merely apply it to the identity function. </p> <p>But what's the point? Why write a type like that? Does it <em>mean</em> anything in programming terms? Well, you can think of it as a function that already has something of type <code>P</code> somewhere, and needs you to give it a function that takes <code>P</code> as an argument, with the whole thing being polymorphic in the final result type. In a sense, it represents a <strong>suspended computation</strong>, waiting for the rest to be provided. In this sense, these suspended computations can be composed together, passed around, invoked, whatever. This should begin to sound familiar to fans of some languages, like Scheme or Ruby--because what it means is that <strong>double-negation corresponds to <a href="http://en.wikipedia.org/wiki/Continuation-passing_style" rel="noreferrer">continuation-passing style</a></strong>, and in fact the type I gave above is exactly the continuation monad in Haskell.</p>

Querying!

Guidance

An individual column

Larger individual text columns get their own page to allow for proper reading.

SQuiL has stopped working due to an internal error.

If you are curious you may find further information in the browser console, which is accessible through the devtools (F12).

Reload