matchingSub is Comonadic (obviously!)

So!

Today’s 1HaskellADay problem was an interesting NP-hard problem ... until I reread the problem statement carefully, then it became trivial. ‘Consecutive’ is the keyword here that unlocked the puzzle for me, eventually.

The heart of the algorithm here is simple enough. It says, in words, ‘are these next n numbers in the list the sum specified?’ If they are, return them as a solution, if they are greater, return nothing, if they are less than the sum, keep trying.

Those are the words, here is the implementation:

inquiry :: Int -> Int -> DList Int -> [Int] -> [Int]

inquiry _ _ _ [] = []

inquiry goal sub accum (next : rest) =

   let tote = sub + next

       naccum = accum << next

   in  case (compare tote goal) of

          LT -> inquiry goal tote naccum rest

          EQ -> dlToList naccum

          GT -> []

Simple enough, and I use a difference list as an accumulator, just because that’s how I roll (and the fact, too, that difference lists append an element in constant time is sweet!)

So, now all we need to do is move an index over the list to test each possible scenario.

Enter the (Comonad) Dragon

Of course, iterating over a list, keeping the context of the list itself active can be done functionally in many ways, but what suggested itself to me right away was the Comonad.

The Comonad of the list is the list itself and all of its tails, and this is exactly the paradigm we need to solve this problem simply, so, writing matchingSub became simply a comonadic extension:

matchingSub’ :: Int -> [Int] -> [[Int]]

matchingSub’ goal domain =

   domain =>> inquiry goal 0 emptyDL

Now, this doesn’t quite give the requested solution sets for the given examples, as it returns the empty list as ‘no solution,’ not ‘nothing at all’ as requested, but filtering out the empty list is easy enough: we just need a predicate to test if the list is not empty and then return only the lists of answers:

isCons :: [a] -> Bool

isCons [] = False

isCons _ = True

matchingSub :: Int -> [Int] -> [[Int]]

matchingSub goal = filter isCons . matchingSub’ goal

And there we have it!

I like comonads. They’re sweet!

Okay, prove it, buster!

(Who is this 'buster'-person, by the way, and why is he always having to prove things?)

All the above code is in Haskell programming, but it is also mutually-translatable to and from Idris. Nearly the same syntax (intentionally so), and nearly the same semantics (Idris's eager evalution looks and tastes very much like Haskell's normal order evaluation).

In Haskell, we'd hand-verify the above with the provided samples and we're done. We'd run it through quickcheck to be done-done.

In Idris, we can prove that what we specified is actually (heh: 'actually') correct in its implementation.

So, let's prove it.

prvSample : (expected : List (List Int)) 

            -> (actual : List (List Int))

            -> (so (expected == actual)) -> ()

prvSample expected actual pred = ()

Using the 'so' assertion, we're (almost) done.

Let's run our sample-set through our prover, such that it is:

sample1 : ()

sample1 = (prvSample [[1..4]]

                     (matchingSub 10 [1..5])) oh

sample2 : ()

sample2 = (prvSample [[1,1], [1,1]] 

                     (matchingSub 2 $ replicate 3 1)) oh

sample3 : ()

sample3 = (prvSample [[1,1], [1,1]]

                     (take 2 $ matchingSub 2 $ repeat 1)) oh

Code compiles? Yes? We're done: we've delivered functionality as specified.

Sweet!