Где полезен оператор Idris ==?

Вам по-прежнему нужно старое доброе равенство, потому что иногда вы ничего не можете доказать. Иногда даже не нужно доказывать. Рассмотрим следующий пример:

countEquals : Eq a => a -> List a -> Nat
countEquals x = length . filter (== x) 

Возможно, вы захотите просто подсчитать количество одинаковых элементов, чтобы показать пользователю некоторую статистику. Другой пример: тесты. Да, даже со строгой системой типов и зависимыми типами вы можете захотеть выполнить старые добрые модульные тесты. Итак, вы хотите проверить ожидания, и это довольно удобно делать с помощью оператора (==).

Я не буду писать полный список случаев, когда вам может понадобиться (==). Оператора равенства недостаточно для доказательства, но вам не всегда нужны доказательства.

(==) (как единственная составляющая функция интерфейса Eq) является функцией от типа T до Bool и подходит для рассуждений по уравнениям. Принимая во внимание, что x = y (где x : T и y : T) АКА «интенсиональное равенство» само по себе является типом и, следовательно, предложением. Вы можете и часто захотите переключаться между двумя разными способами выражения равенства для определенного типа.

x == y = True также является предложением и часто является промежуточным шагом между рассуждениями о (==) и рассуждениями о =.

Точные отношения между двумя типами равенства довольно сложны, и вы можете прочитать https://github.com/pdorrell/learning-idris/blob/9d3454a77f6e21cd476bd17c0bfd2a8a41f382b7/finished/EqFromEquality.idr для моей собственной попытки понять некоторые его аспекты. (Следует отметить, что даже если индуктивно определенный тип будет иметь определяемое интенсиональное равенство, вам все равно придется пройти через несколько обручей, чтобы доказать это, и еще несколько обручей, чтобы определить соответствующую реализацию Eq.)

Вот один из удобных фрагментов кода:

-- for rel x y, provide both the computed value, and the proposition that it is equal to the value (as a dependent pair)
has_value_dpair : (rel : t -> t -> Bool) -> (x : t) -> (y : t) -> (value: Bool ** rel x y = value)
has_value_dpair rel x y = (rel x y ** Refl)

Вы можете использовать его с конструкцией with, когда у вас есть значение, возвращаемое из rel x y, и вы хотите обосновать предложение rel x y = True или rel x y = False (а rel — это некоторая функция, которая может представлять понятие равенства между x и y).

(В этом ответе я предполагаю случай, когда (==) соответствует =, но вы можете полностью определить функцию (==), которая не соответствует =, например, при определении Setoid. Так что это еще одна причина для используйте (==) вместо =.)