monae
monae copied to clipboard
Adding monadic fixpoint to define Mu's quicksort
The definition of qperm function in the quicksort branch requires an interaction between fixpoints and binds to show its termination. Currently there is no such mechanism, and it seems hard to finish the definition.
One possible solution is in http://leventerkok.github.io/papers/mfix.pdf : the monadic fixpoint operator mfix. Let's see if this mfix can be added to monae with useful laws and if this enables quicksort.