
Hi [statutory math warning: calculus, comonads]
On 15 Feb 2008, at 03:15, Cale Gibbard wrote:
I know Bulat will be terribly disappointed by my suggestion to make an addition to Data.List ;) but I mentioned the following couple of functions on #haskell and got some positive response that they were things other people ended up writing all the time as well, so I decided I'd propose them here as additions to Data.List and see what kind of reaction I got:
These selectors ring a bell with me. In Nottingham, Morningside, and a few other places, they're known as instances of "Hancock's cursor down operator" as documented here: http://sneezy.cs.nott.ac.uk/containers/blog/?p=20 More Haskellily than that blog article, the general form is (more or less, and therein lies another story...) down :: Deriv f f' => f x -> f (x, f' x) where Deriv is the usual differential operator calculating from a container its type of one-hole contexts. The effect of down is to decorate each x-element of an (f x)-structure with its own context, thus calculating the collection of ways in which one can visit an element, zipper style. The name makes sense in the context where you're navigating some tree structure given by the fixpoint of f, but "select" is probably a less loaded choice. This generalisation may be too far away from what looks like (and is) a handy pair of list functions, so I wouldn't blame anyone from adding them to the library largely as is. I just thought I'd mention the wedge of which they are the thin end. Second things first:
-- | The 'selectSplit' function takes a list and produces a list of -- triples consisting of a prefix of the list, the element after it, -- and the remainder of the list. selectSplit :: [a] -> [([a],a,[a])] selectSplit [] = [] selectSplit (x:xs) = ([],x,xs) : [(x:lys,y,rys) | (lys,y,rys) <- selectSplit xs]
This guy corresponds to instance Deriv [] (Prod [] []) where newtype Prod f g x = Prod (f x, g x) That is, a one-hole context in a list is a pair of lists---the elements before the hole, the elements after the hole.
-- | The 'select' function takes a list and produces a list of pairs -- consisting of an element of the list together with a list of the -- remaining elements. select :: [a] -> [(a,[a])] select [] = [] select (x:xs) = (x,xs) : [(y,x:ys) | (y,ys) <- select xs]
This one, as confirmed by its example usage
As a side note, the state transformer makes it relatively easy to pick n elements using this: pick n = runStateT . replicateM n . StateT $ select
is somehow seeing lists as *bags*, ie, finite multisets, or lists under arbitrary permutation. newtype Bag x = Bag [x] The power series expansion of Bag is an old pal: Bag x = 1 + x + x^2/2! + x^3/3! + ... representing the choice of an n-tuple, but not distingushing the n! ways in which it can be ordered. Correspondingly instance Deriv Bag Bag a one-hole context in a jumbled collection of elements is a jumbled collection of the remaining elements.
If the order of the pairs in the MTL is fixed in the future in order to better reflect the available instances of Functor/etc., at that point we may want to consider flipping the pairs in the result of select to match.
It's tempting to suggest something like data Deriv f f' => Selection f f' x = x :@ f' x and then select :: Deriv f f' => f x -> f (Selection f f' x) but it may be too grotty for normal use. My motivation is to get my hands on the fact that Deriv f f' => Comonad (Selection f f') where the comonad operations make sense like this: counit :: Selection f f' x -> x returns the selected element cojoin :: Selection f f' x -> Selection f f' (Selection f f' x) decorates each element in the selection with the context in which *it* would be selected, showing you your possible sideways moves (including staying put, ie, decorating the selected element with its existing context). So, the original plug :: Selection f f' x -> f x is "up", cojoin is "sideways" and select is "down". Er, um, applications of these things? I have some. You can find one in a draft I must get around to putting words in: http://strictlypositive.org/Holes.pdf http://strictlypositive.org/Holes.lhs It's a bit enigmatic at the moment, but basically Lucas Dixon suggested to me that (as people who do a lot of substitution) we might benefit from making it quicker to jump over large closed chunks of terms: from the root of a term, he wanted, in constant time to get one of: (0) a guarantee the term is closed (1) the position of its only variable (2) the node where paths to at least two variables diverge The derivative allows us to build a representation of terms where the root is connected to other interesting points by "tubes": lists of one-hole contexts through closed stuff. The compression algorithm which makes an ordinary term into a tube network makes key usage of Hancock's "down" operator: we're looking for the "all subterms closed but one" pattern, so we want to search the possible decompositions of each node. Perhaps "differentiate" is the right name? Oops. I seem to have got a bit carried away. Apologies Conor