On Oct 14, 2014 9:05 AM, "Kim-Ee Yeoh" <ky3@atamo.com> 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?

I think we have different senses of what is easy to understand. We're all working on modifications of Andreas Abel's "naive" approach. I don't think the Reid Barton/Kim-Ee Yeoh modification is easier to understand than the David Feuer/Milan Straka one. In particular, your approach makes the weird long needle/short haystack case implicit, dumping it into the equality test. I also think the principle of least (bad) surprise applies: I wouldn't *expect* an overly long needle to be traversed in full and then the elements compared.

> 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?

I can't undo my understanding and say what I would have thought. But it's certainly a whole lot easier to understand than, say, the `permutations` or `sort` functions, and I could easily add two or three lines of explanation that would guide anyone to a correct interpretation.

> 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?

Let me know when the benchmarks and experimental results are in. Don't forget to get IRB approval for human trials.

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

I think we have an honest disagreement hear about what is "reasonable". I think it's unreasonable for [undefined, undefined] `isSuffixOf` [undefined] to be undefined, but you see it differently.

> 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.

The "long haystack" benchmark I used is actually much, much longer than a path name. My "short needle, short haystack" example is the one designed to test the pathname extension performance.

> 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.

;)