StackOverflow2013

Note that there are some explanatory texts on larger screens.

plurals

PO
text
Body
copied!<blockquote> <p>They're densely packed with assumptions that I've read the latest in whatever branch of discrete math, category theory or abstract algebra is popular this week. (If I never read the words "consult the paper whatever for details of implementation" again, it will be too soon.)</p> </blockquote> <p>Er, and what about simple first-order logic? <code>forall</code> is pretty clearly in reference to <a href="http://en.wikipedia.org/wiki/Universal_quantifier" rel="noreferrer">universal quantification</a>, and in that context the term <a href="http://en.wikipedia.org/wiki/Existential_quantifier" rel="noreferrer">existential</a> makes more sense as well, though it would be less awkward if there were an <code>exists</code> keyword. Whether quantification is effectively universal or existential depends on the placement of the quantifier relative to where the variables are used on which side of a function arrow and it's all a bit confusing.</p> <p>So, if that doesn't help, or if you just don't like symbolic logic, from a more functional programming-ish perspective you can think of type variables as just being (implicit) <em>type</em> parameters to the function. Functions taking type parameters in this sense are traditionally written using a capital lambda for whatever reason, which I'll write here as <code>/\</code>. </p> <p>So, consider the <code>id</code> function:</p> <pre><code>id :: forall a. a -> a id x = x </code></pre> <p>We can rewrite it as lambdas, moving the "type parameter" out of the type signature and adding inline type annotations:</p> <pre><code>id = /\a -> (\x -> x) :: a -> a </code></pre> <p>Here's the same thing done to <code>const</code>:</p> <pre><code>const = /\a b -> (\x y -> x) :: a -> b -> a </code></pre> <p>So your <code>bar</code> function might be something like this:</p> <pre><code>bar = /\a -> (\f -> ('t', True)) :: (a -> a) -> (Char, Bool) </code></pre> <p>Note that the type of the function given to <code>bar</code> as an argument depends on <code>bar</code>'s type parameter. Consider if you had something like this instead:</p> <pre><code>bar2 = /\a -> (\f -> (f 't', True)) :: (a -> a) -> (Char, Bool) </code></pre> <p>Here <code>bar2</code> is applying the function to something of type <code>Char</code>, so giving <code>bar2</code> any type parameter other than <code>Char</code> will cause a type error.</p> <p>On the other hand, here's what <code>foo</code> might look like:</p> <pre><code>foo = (\f -> (f Char 't', f Bool True)) </code></pre> <p>Unlike <code>bar</code>, <code>foo</code> doesn't actually take any type parameters at all! It takes a function that <em>itself</em> takes a type parameter, then applies that function to two <em>different</em> types.</p> <p>So when you see a <code>forall</code> in a type signature, just think of it as a <strong>lambda expression for type signatures</strong>. Just like regular lambdas, the scope of <code>forall</code> extends as far to the right as possible, up to enclosing parenthesis, and just like variables bound in a regular lambda, the type variables bound by a <code>forall</code> are only in scope within the quantified expression.</p> <hr> <p><em>Post scriptum</em>: Perhaps you might wonder--now that we're thinking about functions taking type parameters, why can't we do something more interesting with those parameters than put them into a type signature? The answer is that we can!</p> <p>A function that puts type variables together with a label and returns a new type is a <em>type constructor</em>, which you could write something like this:</p> <pre><code>Either = /\a b -> ... </code></pre> <p>But we'd need completely new notation, because the way such a type is written, like <code>Either a b</code>, is already suggestive of "apply the function <code>Either</code> to these parameters".</p> <p>On the other hand, a function that sort of "pattern matches" on its type parameters, returning different values for different types, is a <em>method of a type class</em>. A slight expansion to my <code>/\</code> syntax above suggests something like this:</p> <pre><code>fmap = /\ f a b -> case f of Maybe -> (\g x -> case x of Just y -> Just b g y Nothing -> Nothing b) :: (a -> b) -> Maybe a -> Maybe b [] -> (\g x -> case x of (y:ys) -> g y : fmap [] a b g ys [] -> [] b) :: (a -> b) -> [a] -> [b] </code></pre> <p>Personally, I think I prefer Haskell's actual syntax...</p> <p>A function that "pattern matches" its type parameters and returns an arbitrary, existing type is a <em>type family</em> or <em>functional dependency</em>--in the former case, it even already looks a great deal like a function definition.</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