The first code block reads like a definition, or the 'what' of quicksort, which has to be fleshed out using the 'how' of quicksort. And it just so happens that 'what' is declarative, and 'how' is imperative (i.e., do this, do that, that's how).
Speaking of which, there is a definition of, not quicksort, but sort itself, and it goes something like this:
'sort is a map that takes a sequence S of orderable items, to one of its permutations P such that for every two adjacent elements e1, e2 in P, e1 < e2'
I'm not familiar with Haskell syntax but I'm sure this definition can be encoded in Haskell. Actually imperatively speaking, this is a sort algorithm itself, the very less discussed (probably because of very high complexity) 'permutation sort', i.e. you keep permuting the input sequence and keep checking your e1/e2 condition until it is satisfied.
So we can define sort, but then we can specify a language to not compute based on that definition but instead pick from one of the preferable computation schemes that are also defined in that langauge (quicksort, mergesort, etc, etc). But then we specify not to use the definition of that scheme but instead use an algorithm for it (e.g., the imperative algorithm for quicksort).
I guess this is a form of semantic layering, something that I'm interested in as a topic of study.
I can't find it now, but there is this article/blog somewhere where the author writes only two functions: One tests if a list is sorted and the other generates a seemingly unspecified permutation of a list.
Then they combine the two in some simple way, and out pops a sorting function with no "how" specification. Due to laziness, the testing function "drives" how the permutation function picks its elements and the whole thing devolves to selection sort.
If anyone remembers the source for this, please post it.
That's where formal proofs come into play, because you need to somehow show that the implementation actually does what the definition states. Since Haskell isn't a proof checker you can't use it for this. The newish and very promising looking language Idris [1], which is very similar to Haskell, can actually do this because of having dependent types. Upon a quick search I found this great example [2] of a proof that insertion sort does indeed return the list sorted, all in the type system. I can really recommend Type Driven Development [3], a recently released book on development in Idris.
Well, if you decides like the GP does, that the definition is the Haskell code, it's not a proof checker, but it's an automatic proof writer that (except from bugs on GHC) is expected to write correct proofs.
It would also be interesting to extend this language to the one that also has partial conditions satisfied, e.g.:
- We have a set S of tuples (a,b,c) sorted by (a,b)
- We would like to sort S by (a,b,c)
- Therefore we only need to only sort subsets (a,b,cx)
By the way, permutation sort would be reducing the sorting algorithm to a problem of search in the configuration space of N variables. Speaking generally, you may reduce any problem to a search problem; so this doesn't only work for sorting.
Speaking of which, there is a definition of, not quicksort, but sort itself, and it goes something like this:
'sort is a map that takes a sequence S of orderable items, to one of its permutations P such that for every two adjacent elements e1, e2 in P, e1 < e2'
I'm not familiar with Haskell syntax but I'm sure this definition can be encoded in Haskell. Actually imperatively speaking, this is a sort algorithm itself, the very less discussed (probably because of very high complexity) 'permutation sort', i.e. you keep permuting the input sequence and keep checking your e1/e2 condition until it is satisfied.
So we can define sort, but then we can specify a language to not compute based on that definition but instead pick from one of the preferable computation schemes that are also defined in that langauge (quicksort, mergesort, etc, etc). But then we specify not to use the definition of that scheme but instead use an algorithm for it (e.g., the imperative algorithm for quicksort).
I guess this is a form of semantic layering, something that I'm interested in as a topic of study.