如何在Idris中编写基于列表的简易快速排序？

首先来看你提供的原Haskell快速排序实现：

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

你提到已经写出了和Haskell版本基本一致的Idris代码，核心需要修正的是有序类型的约束写法——Idris里的Ord是类型类约束，不能直接作为List的元素类型，正确的类型签名需要把约束放在函数箭头的前面。

修正后的完整Idris代码如下：

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

简单解释下类型部分的差异：

• Idris的Ord b => List b -> List b和Haskell的Ord a => [a] -> [a]写法对应，都是声明函数需要元素类型满足Ord约束，才能使用<和>=这类比较操作
• 你之前写的List (Ord b)是错误的，因为Ord不是具体类型，而是描述类型具备排序能力的约束，不能作为List的元素类型

内容的提问来源于stack exchange，提问作者bbarker