Любые уловки, чтобы избавиться от шаблонного при построении доказательств абсурдного предиката на перечислениях?

Question

Допустим, у меня есть

data Fruit = Apple | Banana | Grape | Orange | Lemon | {- many others -}

и предикат этого типа,

data WineStock : Fruit -> Type where
    CanonicalWine : WineStock Grape
    CiderIsWineToo : WineStock Apple

который не подходит для Banana, Orange, Lemon и другие.

Можно сказать, что это определяет WineStock в качестве предиката Fruit; WineStock Grape верно (поскольку мы можем построить значение / доказательство этого типа: CanonicalWine) так же как WineStock Apple, но WineStock Banana ложно, так как этот тип не заселен никакими значениями / доказательствами.

---

Тогда, как я могу эффективно использовать Not (WineStock Banana), Not (WineStock Lemon), так далее? Кажется, что для каждого Fruit кроме конструктора Grape а также AppleЯ не могу помочь, но должен кодировать дело, разделенное на WineStockгде-то, полный impossibles:

instance Uninhabited (WineStock Banana) where
    uninhabited CanonicalWine impossible
    uninhabited CiderIsWineToo impossible

instance Uninhabited (WineStock Lemon) where
    uninhabited CanonicalWine impossible
    uninhabited CiderIsWineToo impossible

instance Uninhabited (WineStock Orange) where
    uninhabited CanonicalWine impossible
    uninhabited CiderIsWineToo impossible

Обратите внимание, что:

• код повторяется,
• LoC взорвется, когда определение предиката будет расти, получая больше конструкторов. Просто представьте Not (Sweet Lemon) доказательство, если предположить, что в Fruit определение.

Таким образом, этот способ не кажется вполне удовлетворительным, почти нецелесообразным.

Есть ли более элегантные подходы?

Answer 1

@slcv прав: использование функции, которая вычисляет, удовлетворяет ли фрукт свойство или нет, вместо построения различных индуктивных предикатов, позволит вам избавиться от этих издержек.

Вот минимальная настройка:

data Is : (p : a -> Bool) -> a -> Type where
  Indeed : p x = True -> Is p x

isnt : {auto eqF : p a = False} -> Is p a -> b
isnt {eqF} (Indeed eqT) = case trans (sym eqF) eqT of
                            Refl impossible

Is p x гарантирует, что собственность p держит элемент x (Я использовал индуктивный тип, а не псевдоним типа, чтобы Idris не раскрыла его в контексте дыры; так легче читать таким образом).

isnt prf отклоняет поддельное доказательство prf всякий раз, когда типограф проверяет p a = False автоматически (через Refl или предположение в контексте).

После того, как они у вас есть, вы можете начать определять свои свойства, перечисляя только положительные случаи и добавляя

wineFruit : Fruit -> Bool
wineFruit Grape = True
wineFruit Apple = True
wineFruit _     = False

weaponFruit : Fruit -> Bool
weaponFruit Apple  = True
weaponFruit Orange = True
weaponFruit Lemon  = True
weaponFruit _      = False

Вы можете определить свои исходные предикаты как вызовы псевдонимов типов Is с соответствующей функцией принятия решения:

WineStock : Fruit -> Type
WineStock = Is wineFruit

И, конечно же, isnt позволяет отклонить невозможные случаи:

dismiss : WineStock Orange -> Void
dismiss = isnt