Зачем охраннику класс классов Ord в Идрисе?

Question

В другом вопросе ( Как написать простую быструю сортировку на основе списка в Idris? ), мне оставалось пытаться понять, почему Prelude.Applicative.guard требует Ord класс типов.

Guard определен вот так :

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

Глядя на Alternative интерфейс docs (на самом деле я не понимаю, как это определено в коде, но я не очень продвинулась в изучении Идриса), я тоже не понимаю, как это требует Ord.

Answer 1

guard не нуждается в ограничении Ord, а (<) в вашем предыдущем вопросе.Я дал там ответ на distingush между List (Ord b) и Ord b => List b.

Чтобы понять, почему guard жалуется на отсутствующее ограничение, посмотрите, как понимание монады обессахаривается.

[y | y <- xs, y < x] становится do {y <- xs; guard (y < x); pure y}.