Скажем, у нас есть функция merge, которая просто объединяет два списка:
Order : Type -> Type
Order a = a -> a -> Bool
merge : (f : Order a) -> (xs : List a) -> (ys : List a) -> List a
merge f xs [] = xs
merge f [] ys = ys
merge f (x :: xs) (y :: ys) = case x `f` y of
True => x :: merge f xs (y :: ys)
False => y :: merge f (x :: xs) ys
и мы хотели бы доказать что-нибудь умное, например, что объединение двух непустых списков приводит к непустому списку:
mergePreservesNonEmpty : (f : Order a) ->
(xs : List a) -> (ys : List a) ->
{auto xsok : NonEmpty xs} -> {auto ysok : NonEmpty ys} ->
NonEmpty (merge f xs ys)
mergePreservesNonEmpty f (x :: xs) (y :: ys) = ?wut
Проверка типа отверстия wut дает нам
wut : NonEmpty (case f x y of True => x :: merge f xs (y :: ys) False => y :: merge f (x :: xs) ys)
Имеет смысл до сих пор! Итак, давайте продолжим и разделим регистр, как предполагает этот тип:
mergePreservesNonEmpty f (x :: xs) (y :: ys) = case x `f` y of
True => ?wut_1
False => ?wut_2
Кажется разумным надеяться, что типы wut_1 и wut_2 будут соответствовать соответствующим ветвям выражения случая merge (поэтому wut_1 будет что-то вроде NonEmpty (x :: merge f xs (y :: ys)), что может быть мгновенно выполнено ), но наши надежды не оправдались: типы такие же, как и для оригинального wut.
Действительно, похоже, единственный способ - использовать with -класс:
mergePreservesNonEmpty f (x :: xs) (y :: ys) with (x `f` y)
mergePreservesNonEmpty f (x :: xs) (y :: ys) | True = ?wut_1
mergePreservesNonEmpty f (x :: xs) (y :: ys) | False = ?wut_2
В этом случае типы будут такими, как ожидалось, но это приводит к повторению аргументов функции для каждой ветви with (и все становится хуже, когда with становится вложенным), плюс with, похоже, не играет хорошо с неявными аргументами (но это, вероятно, само по себе стоит вопроса).
Итак, почему case здесь не поможет, есть ли какие-то причины, помимо чисто практической реализации, которые не соответствуют его поведению с поведением with, и есть ли другие способы написания этого доказательства?