On Wed, Oct 15, 2014 at 7:32 AM, Andreas Abel
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
Fab! In 10 years once I'm fearsome like Andreas I shall take a tilt at Agdaizing David-Milan. Meanwhile I wonder if Agda can perform the following proof-to-proof transformation. Let's let-expand Andreas-dropl like this: ns `isSuffixOfA` hs = let delta = dropl ns hs in ns == dropl delta hs Recall dropl ns hs ~ drop (length ns) hs. But needle longer than haystack is a D.O.A. If only there was a kill-switch we could flip. Cue Maybe as exceptions lite to provide just the thing: ns `isSuffixOfA` hs = fromMaybe False $ do delta <- dropm ns hs return $ ns == dropl delta hs Here's dropm and note how dropl ns hs ~ fromMaybe [] $ dropm ns hs. dropm :: [b] -> [a] -> Maybe [a] dropm (_:xs) (_:ys) = dropm xs ys dropm [] ys = Just ys dropm _ [] = Nothing -- xs longer than ys I put it to you that this new, improved, effectivized version is equivalent to David-Milan. Not forgetting that the right combinators will do-desugar back to a one-liner. Indeed the benchmarks show that M-A-d still pips out D-M in short-long. Best of all, the gap in everything else has shrunk to small single digits. E.g. short-short has narrowed from 9% to 2%: benchmarking simple shortNeedle in shortHaystack/Milan time 136.3 ns (136.2 ns .. 136.3 ns) 1.000 R² (1.000 R² .. 1.000 R²) mean 136.3 ns (136.3 ns .. 136.4 ns) std dev 222.5 ps (36.51 ps .. 466.3 ps) benchmarking simple shortNeedle in shortHaystack/Abel time 139.7 ns (139.6 ns .. 139.9 ns) 1.000 R² (1.000 R² .. 1.000 R²) mean 139.7 ns (139.6 ns .. 139.9 ns) std dev 477.6 ps (296.8 ps .. 782.9 ps) benchmarking simple shortNeedle in longHaystack/Milan time 44.91 μs (44.91 μs .. 44.92 μs) 1.000 R² (1.000 R² .. 1.000 R²) mean 44.91 μs (44.91 μs .. 44.92 μs) std dev 14.94 ns (12.14 ns .. 20.34 ns) benchmarking simple shortNeedle in longHaystack/Abel time 43.57 μs (43.57 μs .. 43.58 μs) 1.000 R² (1.000 R² .. 1.000 R²) mean 43.58 μs (43.57 μs .. 43.60 μs) std dev 32.49 ns (11.69 ns .. 64.84 ns) benchmarking simple longNeedle in shortHaystack/Milan time 118.3 ns (118.3 ns .. 118.3 ns) 1.000 R² (1.000 R² .. 1.000 R²) mean 118.3 ns (118.3 ns .. 118.3 ns) std dev 17.68 ps (13.54 ps .. 23.11 ps) benchmarking simple longNeedle in shortHaystack/Abel time 120.0 ns (120.0 ns .. 120.0 ns) 1.000 R² (1.000 R² .. 1.000 R²) mean 120.0 ns (120.0 ns .. 120.0 ns) std dev 12.54 ps (8.954 ps .. 16.97 ps) benchmarking simple longNeedle in longHaystack/Milan time 46.64 μs (46.63 μs .. 46.67 μs) 1.000 R² (1.000 R² .. 1.000 R²) mean 46.66 μs (46.65 μs .. 46.67 μs) std dev 40.74 ns (29.39 ns .. 59.83 ns) benchmarking simple longNeedle in longHaystack/Abel time 47.25 μs (47.23 μs .. 47.26 μs) 1.000 R² (1.000 R² .. 1.000 R²) mean 47.25 μs (47.24 μs .. 47.26 μs) std dev 22.33 ns (18.24 ns .. 27.98 ns) benchmarking simple shortNeedle in shortHaystack/Milan time 136.3 ns (136.2 ns .. 136.3 ns) 1.000 R² (1.000 R² .. 1.000 R²) mean 136.3 ns (136.3 ns .. 136.4 ns) std dev 222.5 ps (36.51 ps .. 466.3 ps) benchmarking simple shortNeedle in shortHaystack/Abel time 139.7 ns (139.6 ns .. 139.9 ns) 1.000 R² (1.000 R² .. 1.000 R²) mean 139.7 ns (139.6 ns .. 139.9 ns) std dev 477.6 ps (296.8 ps .. 782.9 ps) benchmarking simple shortNeedle in longHaystack/Milan time 44.91 μs (44.91 μs .. 44.92 μs) 1.000 R² (1.000 R² .. 1.000 R²) mean 44.91 μs (44.91 μs .. 44.92 μs) std dev 14.94 ns (12.14 ns .. 20.34 ns) benchmarking simple shortNeedle in longHaystack/Abel time 43.57 μs (43.57 μs .. 43.58 μs) 1.000 R² (1.000 R² .. 1.000 R²) mean 43.58 μs (43.57 μs .. 43.60 μs) std dev 32.49 ns (11.69 ns .. 64.84 ns) benchmarking simple longNeedle in shortHaystack/Milan time 118.3 ns (118.3 ns .. 118.3 ns) 1.000 R² (1.000 R² .. 1.000 R²) mean 118.3 ns (118.3 ns .. 118.3 ns) std dev 17.68 ps (13.54 ps .. 23.11 ps) benchmarking simple longNeedle in shortHaystack/Abel time 120.0 ns (120.0 ns .. 120.0 ns) 1.000 R² (1.000 R² .. 1.000 R²) mean 120.0 ns (120.0 ns .. 120.0 ns) std dev 12.54 ps (8.954 ps .. 16.97 ps) benchmarking simple longNeedle in longHaystack/Milan time 46.64 μs (46.63 μs .. 46.67 μs) 1.000 R² (1.000 R² .. 1.000 R²) mean 46.66 μs (46.65 μs .. 46.67 μs) std dev 40.74 ns (29.39 ns .. 59.83 ns) benchmarking simple longNeedle in longHaystack/Abel time 47.25 μs (47.23 μs .. 47.26 μs) 1.000 R² (1.000 R² .. 1.000 R²) mean 47.25 μs (47.24 μs .. 47.26 μs) std dev 22.33 ns (18.24 ns .. 27.98 ns) Whether the 2% difference is due to Maybe's injecting additional bottoms is anyone's guess. Worth investigating is whether a core-to-core transformation can snap shut the gap, but 2% is already magnificent testimony to the efficacy of compositional, transformational, effectful programming that's uniquely Haskell. -- Kim-Ee