Re: [Haskell-cafe] Is take behaving correctly?
pref_eq k xs ys = take k xs == take k ys This seems to be a straightforward implementation with good properties. Actually, no, at least not if implemented naively. I choosed this example, since I stumbled on this question last week. Reputable mathematicians doing combinatorics on words are using exactly this definition! (Karhumäki, Harju) There are others (Holub), that use the (to the computer scientist) nicer(?) pref_eq 0 _ _ = True pref_eq _ _ [] = False pref_eq _ [] _ = False pref_eq k (x:xs) (y:ys) = x == y pref_eq (k-1) xs ys And as you guess it, there are lemmata (and probably theorems), that hold for one of the definitions only... Later, the mathematicians agree upton to call the first version pref_eq and the second pref_eq_proper. And yes, you are right, just to change the behavior of take would not solve this issue. My topic was really more like don't leap into coding a function before you know what it means as you pointed out with nice words :-) This is not the main topic of the thread (is this true?) but we are in a cafe, so from time to time one adds some cents... /BR ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Is take behaving correctly?
take 1000 [1..3] still yields [1,2,3] You can think about take n as: Take as much as possible, but at most n elements. This behavior has some nice properties as turned out by others, but there are some pitfalls. We have length . take n /= const n in general, instead only length . take n `elem` map const [0..n] holds. Therefore head . length n is unsafe for all n, even strict positive ones. Moreover, it is easy to produce tricky code. Assume you want to know, whether the prefixes of length k are equal and write pref_eq k xs ys = take k xs == take k ys This seems to be a straightforward implementation with good properties. Now play a bit with it: Prelude pref_eq 3 ab abc False Prelude pref_eq 3 ab ab True Prelude map (pref_eq 3 ab) $ Data.List.inits abc [False,False,True,False] Uhh, this is not what everybody expects at first glance. In particular, if pref_eq k xs ys == False then *not* necessarily pref_eq k xs (init ys) == False. As always, quickCheck is your friend to assure (or reject) such a property. /BR ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Is take behaving correctly?
Hi folks On 12 Sep 2007, at 00:38, Brent Yorgey wrote: On 9/11/07, PR Stanley [EMAIL PROTECTED] wrote: Hi take 1000 [1..3] still yields [1,2,3] I thought it was supposed to return an error. [..] If for some reason you want a version that does return an error in that situation, you could do something like the following: take' n _ | (n = 0) = [] take' n [] | (n 0) = error take': list too short | otherwise = [] take' n (x:xs) = x : take' (n-1) xs I'm not sure why you'd want that, though. The standard implementation gracefully handles all inputs, and usually turns out to be what you want. There are two sides to this form of grace, though. I'll grant you, it's quite hard to pull off a successful fraud without a degree of aplomb. I always hope that key invariants and hygiene conditions can be built into the static semantics of programs, but where that's impractical somehow, I prefer if the dynamic behaviour makes it as easy as possible to assign the blame for errors. In such circumstances, I'd like operations to complain about bogus input, rather than producing bogus output. These GIGO problems do bite in real life. I spent a long time finding a bug in somebody else's typechecker which boiled down to the silly mistake of zipping the wrong lists together. The right lists were guaranteed to match in length, but there was no reason for the wrong lists to do so. Problem: unless you were doing fairly wacky stuff, they both happened to have length zero. Once weirder things arrived, the discrepancies showed up and the truncations started happening, causing well-formed but ill-typed expressions to be generated by and propagated around the kernel of the system, which eventually choked in some essentially random place. We had many suspects before we found the culprit. If the programmer had used a version of zip which bombed in off-diagonal cases, we'd have been straight there. So I might very well consider having more than one version of take around, depending on my requirements for its use. I might even consider the more informative function which also returns the length of the shortfall. In a dependently typed setting, I wouldn't write take and drop: I'd equip lists with a view incorporating both, guaranteeing the length invariants and that the sublists actually append to the input. But where shame is unattainable, blame is really quite important. All the best Conor ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Is take behaving correctly?
On Wed, 12 Sep 2007, Conor McBride wrote: Hi folks On 12 Sep 2007, at 00:38, Brent Yorgey wrote: On 9/11/07, PR Stanley [EMAIL PROTECTED] wrote: Hi take 1000 [1..3] still yields [1,2,3] I thought it was supposed to return an error. [..] If for some reason you want a version that does return an error in that situation, you could do something like the following: take' n _ | (n = 0) = [] take' n [] | (n 0) = error take': list too short | otherwise = [] take' n (x:xs) = x : take' (n-1) xs I'm not sure why you'd want that, though. The standard implementation gracefully handles all inputs, and usually turns out to be what you want. I always hope that key invariants and hygiene conditions can be built into the static semantics of programs, but where that's impractical somehow, I prefer if the dynamic behaviour makes it as easy as possible to assign the blame for errors. In such circumstances, I'd like operations to complain about bogus input, rather than producing bogus output. Seconded. The List functions have some kind of scripting language semantics or C semantics, that is, consume almost every input, regardless of the meaning of the output, just in order to avoid error messages. Indeed there are some usages like taking a prefix of an infinite list (zip abc [1..]), where the current behaviour of 'zip' is useful. However it would be better to have versions of 'zip' to support these special cases. Ideally the equal length could be expressed in types, like zipInfInf :: InfiniteList a - InfiniteList b - InfiniteList (a,b) zipInf:: InfiniteList a - FiniteList n b - FiniteList n (a,b) zip :: FiniteList n a - FiniteList n b - FiniteList n (a,b) , which would need dependent types. These GIGO problems do bite in real life. I spent a long time finding a bug in somebody else's typechecker which boiled down to the silly mistake of zipping the wrong lists together. The right lists were guaranteed to match in length, but there was no reason for the wrong lists to do so. I had a bug which was due to the wrong order of applications of 'filter' and 'zip'. I had two lists 'a' and 'b' of the same length, where 'b' contained a condition for filtering, then I wrote zip a (filter p b) instead of filter (p . snd) $ zip a b The wrong version was temptingly short, but it matched the wrong elements. The bug had been catched early, if 'zip' would have checked the length of its inputs. ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Is take behaving correctly?
One idiom I rely on pretty often is (id tail) uncurry (zipWith f) to do pairwise binary operations (though I suspect an Applicative functor might be a better way to go?). E.g. my solution for ProjectEuler problem #18 (max sum of vertical path through a triangle of integers) is: f = curry $ second ((id tail) uncurry (zipWith max)) uncurry (zipWith (+) ) zeroes = repeat 0 maxTotal = foldr f zeroes Key to this idiom is that zipWith stops after the shortest element. Otherwise, I'd need an extra init function and have to test for empty lists. So there is at least one good reason for the way zipWith works. Dan Weston Conor McBride wrote: Hi folks On 12 Sep 2007, at 00:38, Brent Yorgey wrote: On 9/11/07, PR Stanley [EMAIL PROTECTED] wrote: Hi take 1000 [1..3] still yields [1,2,3] I thought it was supposed to return an error. [..] If for some reason you want a version that does return an error in that situation, you could do something like the following: take' n _ | (n = 0) = [] take' n [] | (n 0) = error take': list too short | otherwise = [] take' n (x:xs) = x : take' (n-1) xs I'm not sure why you'd want that, though. The standard implementation gracefully handles all inputs, and usually turns out to be what you want. There are two sides to this form of grace, though. I'll grant you, it's quite hard to pull off a successful fraud without a degree of aplomb. I always hope that key invariants and hygiene conditions can be built into the static semantics of programs, but where that's impractical somehow, I prefer if the dynamic behaviour makes it as easy as possible to assign the blame for errors. In such circumstances, I'd like operations to complain about bogus input, rather than producing bogus output. These GIGO problems do bite in real life. I spent a long time finding a bug in somebody else's typechecker which boiled down to the silly mistake of zipping the wrong lists together. The right lists were guaranteed to match in length, but there was no reason for the wrong lists to do so. Problem: unless you were doing fairly wacky stuff, they both happened to have length zero. Once weirder things arrived, the discrepancies showed up and the truncations started happening, causing well-formed but ill-typed expressions to be generated by and propagated around the kernel of the system, which eventually choked in some essentially random place. We had many suspects before we found the culprit. If the programmer had used a version of zip which bombed in off-diagonal cases, we'd have been straight there. So I might very well consider having more than one version of take around, depending on my requirements for its use. I might even consider the more informative function which also returns the length of the shortfall. In a dependently typed setting, I wouldn't write take and drop: I'd equip lists with a view incorporating both, guaranteeing the length invariants and that the sublists actually append to the input. But where shame is unattainable, blame is really quite important. All the best Conor ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Is take behaving correctly?
On 12 Sep 2007, at 8:08 pm, [EMAIL PROTECTED] wrote: take 1000 [1..3] still yields [1,2,3] You can think about take n as: Take as much as possible, but at most n elements. This behavior has some nice properties as turned out by others, but there are some pitfalls. One of the very nice properties is this: for all n = 0, m = 0 take m . take n = take (m+n) drop m . drop n = drop (m+n) And another is this: for all xs, n = 0 take n xs ++ drop n xs == xs length . take n /= const n in general, instead only length . take n `elem` map const [0..n] What we have is for all xs, n = 0 n = length xs = length (take n xs) == n Suppose we had the unsafe take. Would we then have length . take n == const n? NO! For some xs, (length . take n) xs would be bottom, while (const n) xs would be n. As far as I can see, the strongest statement about length that unsafeTake would satisfy is for all xs, n = 0 n = length xs = length (unsafeTake n xs) == n which is, mutatis mutandis, the SAME law that applies to the `take` we already have. Therefore head . length n is unsafe for all n, even strict positive ones. I'm assuming that should have been (head . take n). The thing is that (head . take n) fails when and only when (head . unsafeTake n) fails; the only difference is which function reports the error. Moreover, it is easy to produce tricky code. Assume you want to know, whether the prefixes of length k are equal and write pref_eq k xs ys = take k xs == take k ys This seems to be a straightforward implementation with good properties. Actually, no, at least not if implemented naively. (I wonder just how clever GHC is with this code? I can't check at the moment. After heroic efforts by my sysadmin, I was finally able to install the binary release of GHC 6.6.1, but (a) it assumes that gcc accepts a -fwrapv flag, which gcc 3.3.2 (TWW) does not accept, and (b) after patching that, gcc still chokes on the output of GHC.) The obvious question is what pref_eq k xs ys *should* do when xs or ys is not at least k long. Does it mean I believe xs and ys are at least k long: if they are, check their prefixes, if they aren't, raise an error or does it mean xs and ys are at least k long and their prefixes of length k are equal? Uhh, this is not what everybody expects at first glance. In particular, if pref_eq k xs ys == False then *not* necessarily pref_eq k xs (init ys) == False. As always, quickCheck is your friend to assure (or reject) such a property. That is certainly so, but the fundamental issue in this example is not what take does, but don't leap into coding a function before you know what it means. We've now seen three readings of what pref_eq means. In particular, pref_eq k xs ys = unsafeTake k xs == unsafeTake k ys would NOT satisfy the law that pref_eq k xs ys == False = pref_eq k xs (init ys) == False because pref_eq 2 [1,2] [1,3] == False but pref_eq 2 [1,2] [1] = undefined So fixing take would not, in this case, produce the desired behaviour. ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
[Haskell-cafe] Is take behaving correctly?
Hi take 1000 [1..3] still yields [1,2,3] I thought it was supposed to return an error. Any ideas? Thanks, Paul ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Is take behaving correctly?
On 9/11/07, PR Stanley [EMAIL PROTECTED] wrote: Hi take 1000 [1..3] still yields [1,2,3] I thought it was supposed to return an error. Any ideas? No, that's the behavior for take specified in the Haskell 98 report: http://haskell.org/onlinereport/standard-prelude.html -- take n, applied to a list xs, returns the prefix of xs of length n, -- or xs itself if n length xs. Cheers, Tim -- Tim Chevalier * catamorphism.org * Often in error, never in doubt Modesty...is both alien and irrelevant to people who are happy in themselves, in their beings, in their skins, their natures, their capacities.--Anne Sayre ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Is take behaving correctly?
On 9/11/07, PR Stanley [EMAIL PROTECTED] wrote: Hi take 1000 [1..3] still yields [1,2,3] I thought it was supposed to return an error. Any ideas? Thanks, Paul If for some reason you want a version that does return an error in that situation, you could do something like the following: take' n _ | (n = 0) = [] take' n [] | (n 0) = error take': list too short | otherwise = [] take' n (x:xs) = x : take' (n-1) xs I'm not sure why you'd want that, though. The standard implementation gracefully handles all inputs, and usually turns out to be what you want. Really, if I were you, instead of making a version take' as above, I would just use the standard take but check for the length of the list in the places where it matters. -Brent ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Is take behaving correctly?
I suppose I'm thinking of head or tail - e.g. head [] or tail []. I'm trying to write my own version of the find function. I have a few ideas but not quite sure which would be more suitable in the context of FP. Any advice would be gratefully received - e.g. do I use recursion, list comprehension or what? Thanks, Paul At 00:08 12/09/2007, you wrote: On 9/11/07, PR Stanley [EMAIL PROTECTED] wrote: Hi take 1000 [1..3] still yields [1,2,3] I thought it was supposed to return an error. Any ideas? No, that's the behavior for take specified in the Haskell 98 report: http://haskell.org/onlinereport/standard-prelude.html -- take n, applied to a list xs, returns the prefix of xs of length n, -- or xs itself if n length xs. Cheers, Tim -- Tim Chevalier * catamorphism.org * Often in error, never in doubt Modesty...is both alien and irrelevant to people who are happy in themselves, in their beings, in their skins, their natures, their capacities.--Anne Sayre ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Is take behaving correctly?
byorgey: On 9/11/07, PR Stanley [EMAIL PROTECTED] wrote: Hi take 1000 [1..3] still yields [1,2,3] I thought it was supposed to return an error. Any ideas? Thanks, Paul If for some reason you want a version that does return an error in that situation, you could do something like the following: take' n _ | (n = 0) = [] take' n [] | (n 0) = error take': list too short | otherwise = [] take' n (x:xs) = x : take' (n-1) xs And we'd call it unsafeTake, just like unsafeFromJust and unsafeTail :-) -- Don ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Is take behaving correctly?
On 9/11/07, Don Stewart [EMAIL PROTECTED] wrote: byorgey: On 9/11/07, PR Stanley [EMAIL PROTECTED] wrote: Hi take 1000 [1..3] still yields [1,2,3] I thought it was supposed to return an error. Any ideas? Thanks, Paul If for some reason you want a version that does return an error in that situation, you could do something like the following: take' n _ | (n = 0) = [] take' n [] | (n 0) = error take': list too short | otherwise = [] take' n (x:xs) = x : take' (n-1) xs And we'd call it unsafeTake, just like unsafeFromJust and unsafeTail :-) -- Don Hmm, that's funny, I don't recall ever hearing of those functions... =) ooo, Don has a shiny new e-mail address! -Brent ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Is take behaving correctly?
On Tue, Sep 11, 2007 at 07:38:18PM -0400, Brent Yorgey wrote: On 9/11/07, PR Stanley [EMAIL PROTECTED] wrote: Hi take 1000 [1..3] still yields [1,2,3] I thought it was supposed to return an error. Any ideas? Thanks, Paul If for some reason you want a version that does return an error in that situation, you could do something like the following: take' n _ | (n = 0) = [] take' n [] | (n 0) = error take': list too short | otherwise = [] take' n (x:xs) = x : take' (n-1) xs you could also do something like take' n xs = take n (xs ++ error I want more!) John -- John Meacham - ⑆repetae.net⑆john⑈ ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Is take behaving correctly?
Let me get this right, are you saying it's unsafe when it returns an error? Paul At 00:40 12/09/2007, you wrote: byorgey: On 9/11/07, PR Stanley [EMAIL PROTECTED] wrote: Hi take 1000 [1..3] still yields [1,2,3] I thought it was supposed to return an error. Any ideas? Thanks, Paul If for some reason you want a version that does return an error in that situation, you could do something like the following: take' n _ | (n = 0) = [] take' n [] | (n 0) = error take': list too short | otherwise = [] take' n (x:xs) = x : take' (n-1) xs And we'd call it unsafeTake, just like unsafeFromJust and unsafeTail :-) -- Don ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Is take behaving correctly?
prstanley: I suppose I'm thinking of head or tail - e.g. head [] or tail []. I'm trying to write my own version of the find function. I have a few ideas but not quite sure which would be more suitable in the context of FP. Any advice would be gratefully received - e.g. do I use recursion, list comprehension or what? Well, you want to filter all elements from a list that match a predicate, and then return Just the first match, or Nothing? find :: (a - Bool) - [a] - Maybe a Checking the current behaviour: find isSpace haskell is fun Just ' ' My first go would be something like this: ok, so let's start with 'filter': filter Char.isSpace haskell is fun Good, then the natural translation to the Maybe type: listToMaybe . filter isSpace $ haskell is fun Just ' ' And we're almost done. Just firing up QuickCheck: quickCheck $ \p (xs :: [Int]) - find p xs == listToMaybe (filter p xs) OK, passed 100 tests. Seems ok. I hope that gives some insight into the process of deriving Haskell implementations by building up a pipeline of pieces. -- Don ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Is take behaving correctly?
byorgey: On 9/11/07, Don Stewart [EMAIL PROTECTED] wrote: byorgey: On 9/11/07, PR Stanley [EMAIL PROTECTED] wrote: Hi take 1000 [1..3] still yields [1,2,3] I thought it was supposed to return an error. Any ideas? Thanks, Paul If for some reason you want a version that does return an error in that situation, you could do something like the following: take' n _ | (n = 0) = [] take' n [] | (n 0) = error take': list too short | otherwise = [] take' n (x:xs) = x : take' (n-1) xs And we'd call it unsafeTake, just like unsafeFromJust and unsafeTail :-) -- Don Hmm, that's funny, I don't recall ever hearing of those functions... =) ooo, Don has a shiny new e-mail address! And a shiny new job in a shiny new city :-) -- Don ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Is take behaving correctly?
prstanley: Let me get this right, are you saying it's unsafe when it returns an error? Partial functions may crash your program, so that's unsafe by some definitions, yep. We have tools that analyse programs for such bugs, in fact (Neil's `catch' program). -- Don ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Is take behaving correctly?
On Tue, 2007-09-11 at 16:48 -0700, Don Stewart wrote: byorgey: On 9/11/07, Don Stewart [EMAIL PROTECTED] wrote: byorgey: On 9/11/07, PR Stanley [EMAIL PROTECTED] wrote: Hi take 1000 [1..3] still yields [1,2,3] I thought it was supposed to return an error. Any ideas? Thanks, Paul If for some reason you want a version that does return an error in that situation, you could do something like the following: take' n _ | (n = 0) = [] take' n [] | (n 0) = error take': list too short | otherwise = [] take' n (x:xs) = x : take' (n-1) xs And we'd call it unsafeTake, just like unsafeFromJust and unsafeTail :-) -- Don Hmm, that's funny, I don't recall ever hearing of those functions... =) ooo, Don has a shiny new e-mail address! And a shiny new job in a shiny new city :-) In a new country. ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
