Re: Proposal: Make a very slight change to the semantics of Data.List.isSuffixOf

Rowing back, I first did the proofs for Variant 1: drop (length ys - length xs) ys == xs Variant 2: drop (length (drop (length xs) ys)) ys == xs Here is the one for Variant 1: open import Data.List open import Data.List.Properties open import Data.Nat using (ℕ; zero; suc; _+_; pred; _∸_) open import Data.Nat.Properties open import Data.Nat.Properties.Simple open import Data.Product open import Relation.Binary.PropositionalEquality as ≡ open ≡-Reasoning -- Two trivial lemmata about append. postulate append-nil : ∀{A : Set} (xs : List A) → xs ++ [] ≡ xs append-assoc : ∀{A : Set} (xs ys zs : List A) → xs ++ (ys ++ zs) ≡ (xs ++ ys) ++ zs -- Logical definition of suffix. _IsSuffixOf_ : ∀{A} → List A → List A → Set ys IsSuffixOf zs = ∃ λ xs → xs ++ ys ≡ zs -- Lemma: drop always returns a suffix. drop-suffix : ∀{A : Set} (n : ℕ) (xs : List A) → drop n xs IsSuffixOf xs drop-suffix 0 xs = [] , refl drop-suffix (suc n) [] = [] , refl drop-suffix (suc n) (x ∷ xs) with drop-suffix n xs ... | ws , p = (x ∷ ws) , cong (λ zs → x ∷ zs) p -- Lemma: dropping after prefixing is the identity. drop-prefix : ∀{A : Set} (ws xs : List A) → drop (length ws) (ws ++ xs) ≡ xs drop-prefix [] xs = refl drop-prefix (w ∷ ws) xs = drop-prefix ws xs -- Variant 1: compute candiate for xs being suffix ys by -- -- drop (length ys - length xs) ys module LengthDiff where -- Soundness of suffix-test. drop-monus-suffix : ∀{A : Set} (xs ys : List A) → drop (length ys ∸ length xs) ys ≡ xs → xs IsSuffixOf ys drop-monus-suffix xs ys p = subst (λ ws → ws IsSuffixOf ys) p (drop-suffix (length ys ∸ length xs) ys) -- Lemma: Substracting the length of an added suffix -- gives the length of the original list. length-monus-suffix : ∀{A : Set} (ws xs : List A) → length (ws ++ xs) ∸ length xs ≡ length ws length-monus-suffix ws xs = begin length (ws ++ xs) ∸ length xs ≡⟨ cong (λ l → l ∸ length xs) (length-++ ws) ⟩ length ws + length xs ∸ length xs ≡⟨ m+n∸n≡m (length ws) (length xs) ⟩ length ws ∎ -- Lemma: Dropping the a prefix computed from the length of the whole list. drop-prefix+- : ∀{A : Set} (ws xs : List A) → drop (length (ws ++ xs) ∸ length xs) (ws ++ xs) ≡ xs drop-prefix+- ws xs = begin drop (length (ws ++ xs) ∸ length xs) (ws ++ xs) ≡⟨ cong (λ l → drop l (ws ++ xs)) (length-monus-suffix ws xs) ⟩ drop (length ws) (ws ++ xs) ≡⟨ drop-prefix ws xs ⟩ xs ∎ -- Completeness of suffix-test. suffix-drop-monus : ∀{A : Set} (xs ys : List A) → xs IsSuffixOf ys → drop (length ys ∸ length xs) ys ≡ xs suffix-drop-monus xs .(ws ++ xs) (ws , refl) = drop-prefix+- ws xs On 14.10.2014 23:24, Andreas Abel wrote:

It would be interesting to compare the correctness arguments for the different versions of isSuffixOf. I gave the dropl-version a try in Agda, but it is not trivial, I could not finish in 90 min. Here is a start:

open import Data.List open import Data.Product

open import Relation.Binary.PropositionalEquality as ≡

postulate append-[] : ∀{A : Set} {xs : List A} → xs ++ [] ≡ xs cong-tail : ∀{A : Set} {x y : A} {xs ys} → x ∷ xs ≡ y ∷ ys → xs ≡ ys

dropL : ∀{A B : Set} → List A → List B → List B dropL [] ys = ys dropL xs [] = [] dropL (x ∷ xs) (y ∷ ys) = dropL xs ys

dropL-is-drop-length : ∀{A B : Set} (xs : List A) (ys : List B) → dropL xs ys ≡ drop (length xs) ys dropL-is-drop-length [] ys = refl dropL-is-drop-length (x ∷ xs) [] = refl dropL-is-drop-length (x ∷ xs) (y ∷ ys) = dropL-is-drop-length xs ys

-- Logical definition of suffix:

_IsSuffixOf_ : ∀{A} → List A → List A → Set ys IsSuffixOf zs = ∃ λ xs → xs ++ ys ≡ zs

dropL-suffix : ∀{A B : Set} (xs : List A) (ys : List B) → dropL xs ys IsSuffixOf ys dropL-suffix [] ys = [] , refl dropL-suffix (x ∷ xs) [] = [] , refl dropL-suffix (x ∷ xs) (y ∷ ys) with dropL-suffix xs ys ... | ws , p = (y ∷ ws) , cong (λ zs → y ∷ zs) p

-- This is one direction, rather easy:

dropL-dropL-suffix : ∀{A : Set} (xs ys : List A) → dropL (dropL xs ys) ys ≡ xs → xs IsSuffixOf ys dropL-dropL-suffix xs ys p = subst (λ ws → ws IsSuffixOf ys) p (dropL-suffix (dropL xs ys) ys)

-- One more easy lemma:

dropL-diag : ∀{A : Set} (xs : List A) → dropL xs xs ≡ [] dropL-diag [] = refl dropL-diag (x ∷ xs) = dropL-diag xs

-- The other direction, hard:

suffix-dropL-dropL : ∀{A : Set} (xs ys : List A) → xs IsSuffixOf ys → dropL (dropL xs ys) ys ≡ xs suffix-dropL-dropL xs .xs ([] , refl) rewrite dropL-diag xs = refl suffix-dropL-dropL xs [] (w ∷ ws , ()) suffix-dropL-dropL [] (y ∷ ys) (w ∷ ws , p) = dropL-diag ys suffix-dropL-dropL (x ∷ xs) (y ∷ ys) (w ∷ ws , p) = {!suffix-dropL-dropL (x ∷ xs) ys (ws , cong-tail p)!}

-- stuck here.

On 14.10.2014 15:05, Kim-Ee Yeoh wrote:

...

David,

To paraphrase Kernighan, ascertaining correctness is twice as hard as writing a program in the first place. So if you're as clever as possible with your code, how will you know it's even correct?

Case in point: the infinite lists wrinkle that you started the thread with. /At a glance/ what do the general recursion versions (yours and Milan's) evaluate to on infinite lists? What are the benchmarks on the time it takes for a haskell programmer to figure them out? Would they not jump at the greater affordance of reasoning with Andreas's compositions?

Meaning and reasonableness have always been the hallmarks of core libs.

Least of all, since it's so losering to benchmark the wrong thing, see below on how Andreas-dropl no.1 beats out David-Milan by the tiniest sliver in short-needle-long-haystack. Like checking file extensions in pathnames that we saw in Andreas's Agda code. Here a concrete app brings real meaning to the timings as opposed to optimizing for vaporware. Watch them Agdaists fall off their chairs when they hit the speed boost.

Don't mean to preach to the choir. Only layin' down the facts for the sake of the archive that every boiled haskeller knows to switch datatypes if isSuffixOf becomes the bottleneck.

benchmarking simple shortNeedle in shortHaystack/lib time 176.6 ns (176.4 ns .. 177.0 ns) 1.000 R² (1.000 R² .. 1.000 R²) mean 176.6 ns (176.5 ns .. 176.9 ns) std dev 596.3 ps (318.4 ps .. 1.096 ns)

benchmarking simple shortNeedle in shortHaystack/Milan time 135.6 ns (135.6 ns .. 135.6 ns) 1.000 R² (1.000 R² .. 1.000 R²) mean 135.6 ns (135.6 ns .. 135.6 ns) std dev 45.49 ps (23.88 ps .. 79.14 ps)

benchmarking simple shortNeedle in shortHaystack/Abel time 145.6 ns (142.5 ns .. 149.5 ns) 0.996 R² (0.996 R² .. 0.997 R²) mean 147.3 ns (144.8 ns .. 150.0 ns) std dev 8.616 ns (8.070 ns .. 9.037 ns) variance introduced by outliers: 76% (severely inflated)

benchmarking simple shortNeedle in longHaystack/lib time 71.12 μs (71.08 μs .. 71.15 μs) 1.000 R² (1.000 R² .. 1.000 R²) mean 71.12 μs (71.08 μs .. 71.16 μs) std dev 142.7 ns (115.6 ns .. 186.3 ns)

benchmarking simple shortNeedle in longHaystack/Milan time 45.00 μs (44.99 μs .. 45.00 μs) 1.000 R² (1.000 R² .. 1.000 R²) mean 45.00 μs (45.00 μs .. 45.01 μs) std dev 21.04 ns (15.62 ns .. 28.75 ns)

benchmarking simple shortNeedle in longHaystack/Abel time 43.68 μs (43.68 μs .. 43.70 μs) 1.000 R² (1.000 R² .. 1.000 R²) mean 43.69 μs (43.68 μs .. 43.69 μs) std dev 18.29 ns (12.79 ns .. 27.76 ns)

benchmarking simple longNeedle in shortHaystack/lib time 396.3 ns (396.2 ns .. 396.6 ns) 1.000 R² (1.000 R² .. 1.000 R²) mean 396.6 ns (396.3 ns .. 397.0 ns) std dev 1.106 ns (707.9 ps .. 1.662 ns)

benchmarking simple longNeedle in shortHaystack/Milan time 117.9 ns (117.9 ns .. 118.0 ns) 1.000 R² (1.000 R² .. 1.000 R²) mean 117.9 ns (117.9 ns .. 117.9 ns) std dev 49.08 ps (30.66 ps .. 75.20 ps)

benchmarking simple longNeedle in shortHaystack/Abel time 125.6 ns (125.6 ns .. 125.6 ns) 1.000 R² (1.000 R² .. 1.000 R²) mean 125.6 ns (125.6 ns .. 125.6 ns) std dev 35.17 ps (19.08 ps .. 58.78 ps)

benchmarking simple longNeedle in longHaystack/lib time 71.98 μs (71.92 μs .. 72.03 μs) 1.000 R² (1.000 R² .. 1.000 R²) mean 71.93 μs (71.85 μs .. 72.00 μs) std dev 247.4 ns (199.9 ns .. 305.3 ns)

benchmarking simple longNeedle in longHaystack/Milan time 47.26 μs (47.24 μs .. 47.29 μs) 1.000 R² (1.000 R² .. 1.000 R²) mean 47.28 μs (47.27 μs .. 47.29 μs) std dev 35.43 ns (28.70 ns .. 45.80 ns)

benchmarking simple longNeedle in longHaystack/Abel time 47.44 μs (47.43 μs .. 47.45 μs) 1.000 R² (1.000 R² .. 1.000 R²) mean 47.44 μs (47.44 μs .. 47.45 μs) std dev 16.81 ns (10.63 ns .. 28.75 ns)

benchmarking use shortNeedle in shortHaystack/lib time 617.9 ns (616.8 ns .. 618.7 ns) 1.000 R² (1.000 R² .. 1.000 R²) mean 617.9 ns (616.9 ns .. 618.4 ns) std dev 2.295 ns (977.3 ps .. 3.747 ns)

benchmarking use shortNeedle in shortHaystack/Milan time 570.7 ns (570.6 ns .. 570.8 ns) 1.000 R² (1.000 R² .. 1.000 R²) mean 570.7 ns (570.6 ns .. 570.7 ns) std dev 194.8 ps (154.1 ps .. 262.9 ps)

benchmarking use shortNeedle in shortHaystack/Abel time 576.8 ns (575.5 ns .. 579.5 ns) 1.000 R² (1.000 R² .. 1.000 R²) mean 576.5 ns (575.7 ns .. 578.9 ns) std dev 5.133 ns (149.4 ps .. 9.882 ns)

benchmarking use shortNeedle in longHaystack/lib time 194.4 μs (192.0 μs .. 195.9 μs) 0.999 R² (0.999 R² .. 1.000 R²) mean 190.9 μs (190.2 μs .. 191.9 μs) std dev 2.789 μs (1.938 μs .. 3.452 μs)

benchmarking use shortNeedle in longHaystack/Milan time 169.3 μs (164.6 μs .. 171.8 μs) 0.997 R² (0.996 R² .. 0.998 R²) mean 160.1 μs (158.1 μs .. 162.6 μs) std dev 7.419 μs (5.720 μs .. 8.512 μs) variance introduced by outliers: 46% (moderately inflated)

benchmarking use shortNeedle in longHaystack/Abel time 166.4 μs (162.9 μs .. 168.4 μs) 0.998 R² (0.997 R² .. 0.999 R²) mean 159.1 μs (157.5 μs .. 161.0 μs) std dev 5.903 μs (4.471 μs .. 6.721 μs) variance introduced by outliers: 35% (moderately inflated)

benchmarking use longNeedle in shortHaystack/lib time 828.0 ns (827.8 ns .. 828.2 ns) 1.000 R² (1.000 R² .. 1.000 R²) mean 828.0 ns (827.9 ns .. 828.2 ns) std dev 582.1 ps (339.9 ps .. 970.5 ps)

benchmarking use longNeedle in shortHaystack/Milan time 550.0 ns (550.0 ns .. 550.1 ns) 1.000 R² (1.000 R² .. 1.000 R²) mean 550.0 ns (550.0 ns .. 550.1 ns) std dev 223.1 ps (97.52 ps .. 438.8 ps)

benchmarking use longNeedle in shortHaystack/Abel time 562.1 ns (562.1 ns .. 562.2 ns) 1.000 R² (1.000 R² .. 1.000 R²) mean 562.1 ns (562.1 ns .. 562.2 ns) std dev 109.5 ps (74.48 ps .. 182.3 ps)

benchmarking use longNeedle in longHaystack/lib time 195.7 μs (193.3 μs .. 197.3 μs) 0.999 R² (0.999 R² .. 1.000 R²) mean 191.9 μs (191.1 μs .. 193.0 μs) std dev 3.065 μs (2.169 μs .. 3.825 μs)

benchmarking use longNeedle in longHaystack/Milan time 170.6 μs (165.7 μs .. 173.4 μs) 0.996 R² (0.995 R² .. 0.998 R²) mean 160.8 μs (158.6 μs .. 163.5 μs) std dev 7.928 μs (6.085 μs .. 9.063 μs) variance introduced by outliers: 49% (moderately inflated)

benchmarking use longNeedle in longHaystack/Abel time 170.4 μs (165.4 μs .. 173.2 μs) 0.996 R² (0.995 R² .. 0.997 R²) mean 160.5 μs (158.3 μs .. 163.3 μs) std dev 8.066 μs (6.200 μs .. 9.280 μs) variance introduced by outliers: 50% (moderately inflated)

This is 64-bit on a recent i5.

I appreciate learning something new from this discussion, so to pay it forward please find attached a self-contained lhs for your nano-tweaking pleasure.

-- Kim-Ee

On Tue, Oct 14, 2014 at 6:02 AM, David Feuer mailto:david.feuer@gmail.com> wrote:

I've switched my allegiance from my own version to Milan's, because it's a tad faster, and also less verbose. One thing to watch out for: although I don't particularly like this, the current version in Data.List makes [] `isSuffixOf` undefined = True. Unless there's a general consensus that this doesn't matter, we need to preserve it.

I don't think Milan's version is too terribly verbose. I tested something very similar to your #1 that was proposed on IRC by Reid Barton, and the numbers just didn't look too wonderful. I don't think Milan's version is too terribly verbose, and I think it's clearer than your #2. As for the depth of caring about speed, I generally disagree with you: lists are actually very good for some purposes, and, moreover, even when they're *not*, people use them anyway and then other people wait for that code to run.

On Mon, Oct 13, 2014 at 6:10 PM, Kim-Ee Yeoh mailto:ky3@atamo.com> wrote:

On Tue, Oct 14, 2014 at 1:17 AM, David Feuer mailto:david.feuer@gmail.com> wrote:

I've done the benchmarks and the results are clear: the implementation I gave is faster than the one you gave and the one in Data.List in all cases. Yours is usually faster than the one in Data.List, but slower for very short lists.

The 2x factor you're seeing over Andreas's diminishes once we put slightly more effort into an apples-to-apples comparison.

1. Instead of drop (length xs) ys, let's define the equivalent

dropl :: [b] -> [a] -> [a] dropl (_:xs) (_:ys) = dropl xs ys dropl [] ys = ys dropl xs [] = []

i.e. dropl xs ys ~ drop (length xs) ys.

Now with Andreas's original version:

xs `isSuffixOfA` ys = xs == dropl (dropl xs ys) ys

that 2x gap narrows down to 10% for most cases.

2. There's that fast path which you optimize for, where the needle is patently too long to be in the haystack. To narrow the semantic gap, we can write

dropm :: [b] -> [a] -> Maybe [a] dropm (_:xs) (_:ys) = dropm xs ys dropm [] ys = Just ys dropm _ [] = Nothing

xs `isSuffixOfA` ys = maybe False id $ do zs <- dropm xs ys ws <- dropm zs ys -- ws = needle-sized slice of the end of haystack return $ xs == ws

Now, the long-needle-short-haystack case also becomes merely 10% off.

I'm -1 on both your proposal and the no.2 code because it's too much verbosity for uncertain gain. The benchmarks look good, but is the function even the bottleneck? For folks that care deeply about speed, lists is almost always the wrong datatype anyway.

I'm weakly +1 on no.1 because it beats the current double reverse definition!

-- Kim-Ee

_______________________________________________ Libraries mailing list Libraries@haskell.org http://www.haskell.org/mailman/listinfo/libraries

-- Andreas Abel <>< Du bist der geliebte Mensch. Department of Computer Science and Engineering Chalmers and Gothenburg University, Sweden andreas.abel@gu.se http://www2.tcs.ifi.lmu.de/~abel/