How to write a simple list-based quicksort in Idri

问题:

I'm just trying to do the bare minimum to translate the following Haskell to Idris (I'm not looking for efficiency or proofs of correctness):

quicksort  []           =  []
quicksort (x:xs)        =  quicksort [y | y <- xs, y<x ]
                        ++ [x]
                        ++ quicksort [y | y <- xs, y>=x]

Here's the Idris code I have, which is essentially unchanged from the Haskell except for needing to tell Idris that we are dealing with Ordered types:

quicksort: List (Ord b) -> List (Ord b)
quicksort  []           =  []
quicksort (x::xs)       =  quicksort [y | y <- xs, y<x ]
                        ++ [x]
                        ++ quicksort [y | y <- xs, y>=x]

However, I'm apparently doing this wrong. I see there is an answer in the question at Quicksort in Idris , but the form is a bit different - I'd like to understand what is wrong with the current approach. My above code gives the error:

40 | quicksort (x::xs)       =  quicksort [y | y <- xs, y<x ]
   |                            ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ ...
When checking right hand side of quicksort with expected type
        List b

When checking an application of function Prelude.Applicative.guard:
        Can't find implementation for Ord (Ord b)

回答1:

The problem is that Prelude.Applicative.guard (function which is used for guards in list comprehensions) can't find implementation for Ord typeclass.

That tells us, that we haven't added (or added incorrectly) typeclass constraint. If we change your code to this one, it should work:

quicksort: Ord b => List b -> List  b
quicksort  []           =  []
quicksort (x::xs)       =  quicksort [y | y <- xs, y < x ]
                        ++ [x]
                        ++ quicksort [y | y <- xs, y >= x]

回答2:

To clarify: List (Ord b) is a list of implementations for Ord b, while Ord b => List b is a list of b where b has the interface constraint of Ord b. Compare:

[ord1] Ord Nat where
   compare Z (S n)     = GT
   compare (S n) Z     = LT
   compare Z Z         = EQ
   compare (S x) (S y) = compare @{ord1} x y

imps : List (Ord b) -> List (Ord b)
imps xs = xs

ords : Ord b => List b -> List b
ords xs = xs

With imps [ord1] : List (Ord Nat) and ords [1] : List Nat.