[Haskell-cafe] Re: Why is there no splitBy in the list module?

[Robert Dockins]

On Jul 20, 2006, at 1:31 PM, Jon Fairbairn wrote:

> On 2006-07-13 at 10:16BST I wrote:
>> Hooray!  I've been waiting to ask "Why aren't we asking what
>> laws hold for these operations?"
>
> Having thought about this for a bit, I've come up with the
> below. This is intended to give the general idea -- it's not
> polished code, and I'm not at all wedded to the names I've
> used, and it almost certainly should be split up.

[snip an interesting new take on splitting strings]

>
> -- Jón Fairbairn                              Jon.Fairbairn at  
> cl.cam.ac.uk

Inspired by this, I've hacked together my own version, based around  
the ideas of list deforestation.  I've taken some liberties with the  
function names.  In particular, I've split Jon's 'parts' function  
into two pieces, called 'classify' and 'parts'.  Code follows.  I  
haven't tested it a lot, but things seem to work in ghci.  In  
particular I've not tested the RULES.  I have no idea if this is  
better or not in terms of performance, but it seems a little cleaner  
to me.


Rob Dockins

Speak softly and drive a Sherman tank.
Laugh hard; it's a long way to the bank.
           -- TMBG





{-# OPTIONS -fglasgow-exts  #-}
module Parts where

import GHC.Exts
import Data.Char

data PartList a
   = LeftPart  a (PartList a)
   | RightPart a (PartList a)
   | PartNil

foldrParts :: (a -> b -> b) -> (a -> b -> b) -> b -> PartList a -> b
foldrParts l r n (LeftPart  x xs) = l x (foldrParts l r n xs)
foldrParts l r n (RightPart x xs) = r x (foldrParts l r n xs)
foldrParts l r n PartNil = n

buildParts :: (forall b. (a -> b -> b) -> (a -> b -> b) -> b -> b) ->  
PartList a
buildParts g = g LeftPart RightPart PartNil

{-# RULES
"foldrParts/buildParts"  forall l r z (g::forall b. (a->b->b) -> (a- 
 >b->b) -> b -> b) .
          foldrParts l r z (buildParts g) = g l r z
"foldrParts/id"
          foldrParts LeftPart RightPart PartNil = id
   #-}

classify :: (a -> Bool) -> [a] -> PartList a
classify p zs = buildParts (\l r n -> foldr (\x xs -> if p x then r x  
xs else l x xs) n zs)

parts :: PartList a -> PartList [a]
parts = foldrParts fLeft fRight PartNil
where
    fLeft x xs = LeftPart
           (case xs of (LeftPart y _ ) -> x:y; _ -> x:[])
           (case xs of (LeftPart _ ys) ->  ys; _ -> xs)

    fRight x xs = RightPart
           (case xs of (RightPart y _ ) -> x:y; _ -> x:[])
           (case xs of (RightPart _ ys) ->  ys; _ -> xs)

partsSep :: PartList a -> PartList [a]
partsSep = foldrParts fLeft fRight PartNil
where
    fLeft  x xs = RightPart [] xs
    fRight x xs = RightPart
           (case xs of (RightPart y _ ) -> x:y; _ -> x:[])
           (case xs of (RightPart _ ys) ->  ys; _ -> xs)

fromParts :: PartList a -> [a]
fromParts xs = build (\c n -> foldrParts c c n xs)

{-
loose proof, ignore seq...

forall p xs. fromParts (classify p xs)

   === build (\c n -> foldrParts c c n (classify p  
xs)                          (definition of fromParts)
   === build (\c n -> foldrParts c c n (buildParts (\l r n - 
 >                   (definition of classify)
              foldr (\x xs -> if p x then r x xs else l x xs) n xs)))
   === build (\c n -> foldr (\x xs -> if p x then c x xs else c x xs)  
n xs)     (deforestation conjecture)
   === build (\c n -> foldr (\x xs -> c x xs) n  
xs)                             (by indifference on p x)
   === foldr (\x xs -> (:) x xs) []  
xs)                                         (definition of build)
   === foldr (:) []  
xs                                                          (eta  
contraction)
   ===  
xs                                                                       
  (well known)
-}

{-
forall p xs.  concat (fromParts (parts (classify p xs)))

   === concat (fromParts (foldrParts fLeft fRigth PartNil (classify p  
xs)))      (definition of parts)
   === concat (fromParts (foldrParts fLeft fRigth PartNil (buildParts  
(\l r n -> (definition of classify)
              foldr (\x xs -> if p x then r x xs else l x xs) n  
xs)))            (deforestation conjecture)
   === concat (fromParts (foldr
                 (\x xs -> if p x then fRight x xs else fLeft x xs)  
PartNil xs))
   === concat (build (\c n -> foldrParts c c n  
(foldr                            (definition of fromParts)
                 (\x xs -> if p x then fRight x xs else fLeft x xs)  
PartNil xs)))
   === foldr (++) [] (build (\c n -> foldrParts c c n  
(foldr                     (definition of concat)
                 (\x xs -> if p x then fRight x xs else fLeft x xs)  
PartNil xs)))
   === foldrParts (++) (++) []  
(foldr                                            (list deforestation)
                 (\x xs -> if p x then fRight x xs else fLeft x xs)  
PartNil xs)))

	??? I think the rest of the proof can go through via the  
approximation lemma, or maybe some more inlining is sufficient...

   === xs
-}


splitBy :: (a -> Bool) -> [a] -> [[a]]
splitBy p = fromParts . parts . classify p

contiguousParts :: (a -> Bool) -> [a] -> [[a]]
contiguousParts p xs = build (\c n -> foldrParts (\_ x -> x) c n  
(parts (classify p xs)))

segmentsSatisfying :: (a -> Bool) -> [a] -> [[a]]
segmentsSatisfying p = fromParts . partsSep . classify p

splitOn :: Eq a => a -> [a] -> [[a]]
splitOn x = splitBy (==x)

words :: String -> [String]
words = contiguousParts isAlphaNum

lines :: String -> [String]
lines = segmentsSatisfying (/= '\n')