StackOverflow2013

Note that there are some explanatory texts on larger screens.

plurals

PO
text
Body
copied!<blockquote> <p>Can anybody <em>completely</em> explain the forall keyword in clear, plain English?</p> </blockquote> <p><strong>No.</strong> (Well, maybe Don Stewart can.)</p> <p>Here are the barriers to a simple, clear explanation or <code>forall</code>:</p> <ul> <li><p>It's a quantifier. You have a to have at least a little logic (predicate calculus) to have seen a universal or existential quantifier. If you've never seen predicate calculus or are not comfortable with quantifiers (and I have seen students during PhD qualifying exams who are not comfortable), then for you, there's no easy explanation of <code>forall</code>.</p></li> <li><p>It's a <em>type</em> quantifier. If you haven't seen <a href="http://en.wikipedia.org/wiki/System_F" rel="noreferrer">System F</a> and gotten some practice writing polymorphic types, you're going to find <code>forall</code> confusing. Experience with Haskell or ML is not enough, because normally these languages omit the <code>forall</code> from polymorphic types. (In my mind, this is a language-design mistake.)</p></li> <li><p>In Haskell in particular, <code>forall</code> is used in ways that I find confusing. (I'm not a type theorist, but my work brings me in contact with a <em>lot</em> of type theory, and I'm quite comfortable with it.) For me, the main source of confusion is that <code>forall</code> is used to encode a type that I myself would prefer to write with <code>exists</code>. It's justified by a tricky bit of type isomorphism involving quantifiers and arrows, and every time I want to understand it, I have to look things up and work out the isomorphism myself.</p> <p>If you are not comfortable with the idea of type isomorphism, or if you don't have any practice thinking about type isomorphisms, this use of <code>forall</code> is going to stymie you.</p></li> <li><p>While the general concept of <code>forall</code> is always the same (binding to introduce a type variable), the details of different uses can vary significantly. Informal English is not a very good tool for explaining the variations. To really understand what's going on, you need some mathematics. In this case the relevant mathematics can be found in Benjamin Pierce's introductory text <em>Types and Programming Languages</em>, which is a very good book.</p></li> </ul> <p>As for your particular examples,</p> <ul> <li><p><code>runST</code> <em>should</em> make your head hurt. Higher-rank types (forall to the left of an arrow) are rarely found in the wild. I encourage you to read the paper that introduced <code>runST</code>: <a href="http://research.microsoft.com/en-us/um/people/simonpj/papers/lazy-functional-state-threads.ps.Z" rel="noreferrer">"Lazy Functional State Threads"</a>. This is a really good paper, and it will give you a much better intuition for the type of <code>runST</code> in particular and for higher-rank types in general. The explanation take several pages, it's very well done, and I'm not going to try to condense it here.</p></li> <li><p>Consider</p> <pre><code>foo :: (forall a. a -> a) -> (Char,Bool) bar :: forall a. ((a -> a) -> (Char, Bool)) </code></pre> <p>If I call <code>bar</code>, I can simply pick any type <code>a</code> that I like, and I can pass it a function from type <code>a</code> to type <code>a</code>. For example, I can pass the function <code>(+1)</code> or the function <code>reverse</code>. You can think of the <code>forall</code> as saying "I get to pick the type now". (The technical word for picking the type is <em>instantiating</em>.)</p> <p>The restrictions on calling <code>foo</code> are much more stringent: the argument to <code>foo</code> <em>must</em> be a polymorphic function. With that type, the only functions I can pass to <code>foo</code> are <code>id</code> or a function that always diverges or errors, like <code>undefined</code>. The reason is that with <code>foo</code>, the <code>forall</code> is to the left of the arrow, so as the caller of <code>foo</code> I don't get to pick what <code>a</code> is—rather it's the <em>implementation</em> of <code>foo</code> that gets to pick what <code>a</code> is. Because <code>forall</code> is to the left of the arrow, rather than above the arrow as in <code>bar</code>, the instantiation takes place in the body of the function rather than at the call site.</p></li> </ul> <p><strong>Summary:</strong> A <em>complete</em> explanation of the <code>forall</code> keyword requires math and can be understood only by someone who has studied the math. Even partial explanations are hard to understand without math. But maybe my partial, non-math explanations help a little. Go read Launchbury and Peyton Jones on <code>runST</code>!</p> <hr> <p><strong>Addendum:</strong> Jargon "above", "below", "to the left of". These have nothing to do with the <em>textual</em> ways types are written and everything to do with abstract-syntax trees. In the abstract syntax, a <code>forall</code> takes the name of a type variable, and then there is a full type "below" the forall. An arrow takes two types (argument and result type) and forms a new type (the function type). The argument type is "to the left of" the arrow; it is the arrow's left child in the abstract-syntax tree.</p> <p>Examples:</p> <ul> <li><p>In <code>forall a . [a] -> [a]</code>, the forall is above the arrow; what's to the left of the arrow is <code>[a]</code>.</p></li> <li><p>In</p> <pre><code>forall n f e x . (forall e x . n e x -> f -> Fact x f) -> Block n e x -> f -> Fact x f </code></pre> <p>the type in parentheses would be called "a forall to the left of an arrow". (I'm using types like this in an optimizer I'm working on.)</p></li> </ul>

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