On Sat, 1 Dec 2012, Andreas Abel wrote:
On 30.11.12 7:14 PM, Henning Thielemann wrote:
Agda uses isLeft and isRight in some QuickCheck properties. And then there is this application:
do -- ps0 :: [NamedArg ParseLHS] ps0 <- mapM classPat ps let (ps1, rest) = span (isLeft . namedArg) ps0 (p2, ps3) <- uncons rest -- when (null rest): no field pattern or def pattern found guard $ all (isLeft . namedArg) ps3 let (f, lhs) = fromR p2 (ps', _:ps'') = splitAt (length ps1) ps return $ Right (f, LHSProj x ps' lhs ps'')
Looks at least interesting ... :-)
Well, maybe this code could be improved, avoiding isLeft and fromR(ight).
Basically, what I want to to here is: - I have a list of things: ps - I have a classification of these things into Left and Right: classPat - I want to succeed if exactly one of these things is classified as a Right - I want to extract that Right thing, modify it a bit: lhs - I want to obtain all the Left things unchanged: ps' and ps''
Since you know that everything in ps' and ps'' is Left, I guess it would be more precise to return the value without the Left constructor, right?
These standard functions do not do the job: - partitionEithers: loses the order of my things - lefts/rights: ditto
right
The crux here is that the standard list functions like filter, span, break etc. use "Bool" as decision type. They would be more general with Either, using Left as falsehood and Right as truth.
span :: (a -> Either b c) -> [a] -> ([c], [a]) break :: (a -> Either b c) -> [a] -> ([b], [a])
Since you do not use the 'b' type in 'span' and the 'c' type in 'break' we would certainly prefer: spanMaybe :: (a -> Maybe c) -> [a] -> ([c], [a]) breakMaybe :: (a -> Maybe b) -> [a] -> ([b], [a]) However for your application, something with an Either "predicate" would be actually more appropriate. Like breakEither :: (a -> Either b c) -> [a] -> ([b], Maybe (c, [a]))
How would you do it?
E.g. I would try to avoid the irrefutable pattern (_:ps''), since it is a potential source of an error. For now I can only come up with a mix of explicit recursion and standard library functions (partitionEithers): import Data.Tuple.HT (mapFst) import Control.Monad (guard) import Data.Either (partitionEithers) breakEither :: (a -> Either b c) -> [a] -> ([b], Maybe (c, [a])) breakEither f = let go [] = ([], Nothing) go (e : es) = case f e of Left x -> mapFst (x :) $ go es Right x -> ([], Just (x, es)) in go splitAtSingleRight :: [Either a b] -> Maybe ([a], b, [a]) splitAtSingleRight xs = case breakEither id xs of (as, msuffix) -> do (c,es) <- msuffix case partitionEithers es of (ls, rs) -> guard (null rs) >> return (as, c, ls)