# Re: [isabelle] Code generation for reverse sorting

Hi Christian,
Here are my thoughts about List.sort & friends:

`a) The first problem with List.sort and friends is that they are defined in the type class
``linorder, although their definitions could be made as well in the type class ord. Three
``years ago (2ada2be850cb), I have moved all the operations for red-black trees (RBT) into
``the linorder type class, precisely because I wanted to use them with other ordering
``relations. Ideally, the same should be done for List.sort and friends.
`

`For the time being, you can still avoid some of the overheads by using the foundational
``constant linorder.sort_key, which takes the order as an additional argument. So, you can
``pass in the dual order. With a single interpretation for the dual order, you should get
``all the theorems you need. You can even define an abbreviation for it:
`
interpretation dual!: linorder "op â" "op > :: _ :: linorder â _" by(rule dual_linorder)
abbreviation "rsort == linorder.sort_key op â (Îx. x)"

`Unfortunately, code generation does not work out of the box, because the code setup has
``only been done for the type-class based instance. If List.sort was defined in the type
``class ord, one could simply re-declare the code equations (as I did for the RBT operations
``in my AFP entry Containers). Alternatively, you can prove that sort & friends are
``parametric (as Peter did for RBT operations in his AFP entry Collections) and exploit
``parametricity like he does, but my feeling is that this again requires unconditional
``equations, i.e., a definition in ord.
`

`b) The second problem is that we want to implement List.sort with different algorithms
``during code generation. For linear orders, this is no problem, because the result is
``unique. However, if we pass in a non-linear order, the outcome might depend on the
``algorithm. Thus, we can only do program refinement for linear orders. In that view, even
``if we move List.sort to the type class ord, we still have problems, because we cannot
``prove the code equations for arbitrary ordering relations any more.
`

`Ideally, we should separate the proving part from the code generation part. AFAICS, the
``following should work.
`

`1. Move List.sort and friends to type class ord. For ease of use and compatibility, we can
``add sign constraints such that type inference infers the linorder sort constraints for
``List.sort.
`
2. Define a type 'a linorder of linear orders using typedef and an embedding
linorder_of :: "'a :: linorder itself => 'a linorder"

`3. Define operations for sorting lists that are parametrised with the order from the type
``'a linorder. Prove equations like "List.sort_key == sort_key_impl TYPE('a)".
`

`4. Adapt all the implementations for sorting such that they refine sort_key_impl rather
``than List.sort_key.
`

`Apart from sorting, such a setup could be used for further improvements to the generated
``code. For example, one could refine the type 'a linorder to provide a comparator instead
``of a comparison operation.
`

`I guess such a change requires quite a lot of work to be carried out on the whole
``repository. At the moment, I do not have the time to carry all this out, but if the issue
``is pressing for you, you might want to try it yourself. But before you start, we should
``also ask Florian on his opinion.
`
Best,
Andreas
On 03/10/15 21:59, Christian Sternagel wrote:

Dear all,
for those of you who do not regularly check stackoverflow but might have
an answer to my question there (yes I am looking at you Florian ;) ) I'm
brazenly posting the link to my question here
http://stackoverflow.com/q/32926842/476803
In short, my question is: What is the easiest way to generate code for a
sorting algorithm that sorts its argument in reverse order, while
building on top of the existing List.sort?
cheers
chris

*This archive was generated by a fusion of
Pipermail (Mailman edition) and
MHonArc.*