如何在Idris中编写一个简单的基于列表的快速排序？
如何在Idris中编写一个简单的基于列表的快速排序？
提问于 2018-05-08 00:10:11
我只是想把下面的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)回答 2
Stack Overflow用户
回答已采纳
发布于 2018-05-08 05:39:42
问题是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]Stack Overflow用户
发布于 2018-05-11 01:26:42
澄清一下：List (Ord b)是Ord b的实现列表，而Ord b => List b是b的列表，b具有Ord b的接口约束。比较：
[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 = xsimps [ord1] : List (Ord Nat)和ords [1] : List Nat。
页面原文内容由Stack Overflow提供。腾讯云小微IT领域专用引擎提供翻译支持
原文链接：
https://stackoverflow.com/questions/50224043
复制相关文章
相似问题
腾讯云开发者
