From 47bc0c16fec3c91dc1635ac6f42fe457e58fc41c Mon Sep 17 00:00:00 2001 From: Jim Pryor Date: Sat, 27 Nov 2010 20:11:38 -0500 Subject: [PATCH] expand zipper-lists-contin Signed-off-by: Jim Pryor --- zipper-lists-continuations.mdwn | 43 ++++++++++++++++++++++++++++++++++++++--- 1 file changed, 40 insertions(+), 3 deletions(-) diff --git a/zipper-lists-continuations.mdwn b/zipper-lists-continuations.mdwn index edc3359d..2e84616a 100644 --- a/zipper-lists-continuations.mdwn +++ b/zipper-lists-continuations.mdwn @@ -219,11 +219,48 @@ Here's a way to persuade yourself that it will have the right behavior. First, i Now let's think about what this does. It's a wrapper around `u`. In order to behave as the list which is the result of mapping `f` over each element of `u`, and then joining (`concat`ing) the results, this wrapper would have to accept arguments `k` and `z` and fold them in just the same way that the list which is the result of mapping `f` and then joining the results would fold them. Will it? -... MORE... +Suppose we have a list' whose contents are `[1; 2; 4; 8]`---that is, our list' will be `fun f z -> f 1 (f 2 (f 4 (f 8 z)))`. We call that list' `u`. Suppose we also have a function `f` that for each `int` we give it, gives back a list of the divisors of that `int` that are greater than 1. Intuitively, then, binding `u` to `f` should give us: + concat (map f u) = + concat [[]; [2]; [2; 4]; [2; 4; 8]] = + [2; 2; 4; 2; 4; 8] -Our theory is that this monad should be capable of exactly -replicating the behavior of the standard List monad. Let's test: +Or rather, it should give us a list' version of that, which takes a function `k` and value `z` as arguments, and returns the right fold of `k` and `z` over those elements. What does our formula + + fun k z -> u (fun a b -> f a k b) z + +do? Well, for each element `a` in `u`, it applies `f` to that `a`, getting one of the lists: + + [] + [2] + [2; 4] + [2; 4; 8] + +(or rather, their list' versions). Then it takes the accumulated result `b` of previous steps in the fold, and it folds `k` and `b` over the list generated by `f a`. The result of doing so is passed on to the next step as the accumulated result so far. + +So if, for example, we let `k` be `+` and `z` be `0`, then the computation would proceed: + + 0 ==> + right-fold + and 0 over [2; 4; 8] = 2+4+8+0 ==> + right-fold + and 2+4+8+0 over [2; 4] = 2+4+2+4+8+0 ==> + right-fold + and 2+4+2+4+8+0 over [2] = 2+2+4+2+4+8+0 ==> + right-fold + and 2+2+4+2+4+8+0 over [] = 2+2+4+2+4+8+0 + +which indeed is the result of right-folding + and 0 over `[2; 2; 4; 2; 4; 8]`. If you trace through how this works, you should be able to persuade yourself that our formula: + + fun k z -> u (fun a b -> f a k b) z + +will deliver just the same folds, for arbitrary choices of `k` and `z` (with the right types), and arbitrary list's `u` and appropriately-typed `f`s, as + + fun k z -> List.fold_right k (concat (map f u)) z + +would. + +For future reference, we might make two eta-reductions to our formula, so that we have instead: + + let l'_bind = fun k -> u (fun a -> f a k);; + +Let's make some more tests: l_bind [1;2] (fun i -> [i, i+1]) ~~> [1; 2; 2; 3] -- 2.11.0