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

Скажем, у меня

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, где-то полное impossible s:

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 есть много сладких альтернатив.

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

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

Ответы

Ответ 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 всякий раз, когда typechecker может генерировать доказательство, что p a = False автоматически (через Refl или предположение в контексте).

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

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