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')