StackOverflow2013

Note that there are some explanatory texts on larger screens.

plurals

PO
text
Body
copied!<p>The Wikipedia page on <a href="http://en.wikipedia.org/wiki/Mogensen%e2%80%93Scott_encoding" rel="nofollow">Scott encoding</a> has some useful insights. The short version is, what you're referring to is the Church encoding, and your "hypothetical pattern-match encoding" is the Scott encoding. Both are sensible ways of doing things, but the Church encoding requires lighter type machinery to use (in particular, it does not require recursive types).</p> <p>The proof that the two are equivalent uses the following idea:</p> <pre><code>churchfold :: (a -> b -> b) -> b -> [a] -> b churchfold _ z [] = z churchfold f z (x:xs) = f x (churchfold f z xs) scottfold :: (a -> [a] -> b) -> b -> [a] -> b scottfold _ z [] = z scottfold f _ (x:xs) = f x xs scottFromChurch :: (a -> [a] -> b) -> b -> [a] -> b scottFromChurch f z xs = fst (churchfold g (z, []) xs) where g x ~(_, xs) = (f x xs, x : xs) </code></pre> <p>The idea is that since <code>churchfold (:) []</code> is the identity on lists, we can use a Church fold that produces the list argument it is given as well as the result it is supposed to produce. Then in the chain <code>x1 `f` (x2 `f` (... `f` xn) ... )</code> the outermost <code>f</code> receives a pair <code>(y, x2 : ... : xn : [])</code> (for some <code>y</code> we don't care about), so returns <code>f x1 (x2 : ... : xn : [])</code>. Of course, it also has to return <code>x1 : ... : xn : []</code> so that any more applications of <code>f</code> could also work.</p> <p>(This is actually a little similar to the proof of the mathematical principle of <a href="http://en.wikipedia.org/wiki/Mathematical_induction#Complete_induction" rel="nofollow">strong (or complete) induction</a>, from the "weak" or usual principle of induction).</p> <p>By the way, your <code>Bool r</code> type is a bit too big for real Church booleans – e.g. <code>(+) :: Bool Integer</code>, but <code>(+)</code> isn't really a Church boolean. If you enable <code>RankNTypes</code> then you can use a more precise type: <code>type Bool = forall r. r -> r -> r</code>. Now it is forced to be polymorphic, so genuinely only contains two (ignoring <code>seq</code> and bottom) inhabitants – <code>\t _ -> t</code> and <code>\_ f -> f</code>. Similar ideas apply to your other Church types, too.</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