为什么守卫需要 Idris 中的 Ord 类型类？

Question

在另一个问题 (How to write a simple list-based quicksort in Idris?) 中，我试图理解为什么 Prelude.Applicative.guard 需要 Ord 类型类。

Guard 定义为like this:

guard : Alternative f => Bool -> f ()
guard a = if a then pure () else empty

查看Alternative 接口docs（我还没有真正理解它在代码中是如何定义的，但我在学习 Idris 方面还不是很远），我不明白它需要什么Ord 要么。

Answer 1

guard 单独不需要 Ord 约束，而是 (<) 在您的上一个问题中。我在那里给出了区分List (Ord b) 和Ord b => List b 的答案。

要了解guard 为何抱怨缺少约束，请查看monad comprehensions 是如何脱糖的。

[y | y <- xs, y < x] 变为 do {y <- xs; guard (y < x); pure y}。