idris - 如何在 Idris 中编写一个简单的基于列表的快速排序？

Question

我只是尽力将以下 Haskell 翻译为 Idris(我不是在寻找效率或正确性证明):

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

这是我的 Idris 代码，除了需要告诉 Idris 我们正在处理有序类型之外，它与 Haskell 基本没有变化:

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

但是，我显然做错了。我看到问题中有答案 Quicksort in Idris ，但形式有点不同 - 我想了解当前方法有什么问题。我上面的代码给出了错误:

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)

Answer 1

问题是 Prelude.Applicative.guard (用于列表推导式中的防护的函数)无法找到 Ord 类型类的实现。

这告诉我们，我们没有添加(或添加错误)类型类约束。如果我们将您的代码更改为此代码，它应该可以工作:

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