select and selectSplit

[Conor McBride]

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