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

скажем, у меня есть

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

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

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


boilerplate haskell dependent-type idris proof-of-correctness
person ulidtko    schedule 31.01.2016    source источник
comment
Многие из старых идиом Haskell не меняются в системах с зависимой типизацией. Сделайте недопустимые состояния непредставимыми удержаниями и на уровне типов: я не думаю, что вы даже должны иметь возможность создавать эти невозможные типы. Я бы, вероятно, структурировал этот пример как (что-то примерно похожее) на тип фруктов, из которых можно делать вино data WineFruit = Grape | Apple и другие фрукты data Fruit = WineFruit WineFruit | Banana | Orange | Lemon.   -  person Benjamin Hodgson♦    schedule 03.02.2016
comment
@BenjaminHodgson, этот подход начинает разваливаться, когда вы хотите добавить PieFruit, SaladFruit, WeaponFruit и т. д.   -  person dfeuer    schedule 15.02.2016
comment
Учитывая, что вы находитесь в idris, почему вы определяете тип данных для WineStock? Разве вы не можете просто определить isWineStock как функцию уровня значения и использовать ее в доказательствах, где это уместно?   -  person sclv    schedule 19.03.2016

Ответы (1)


arrow_upward
4
arrow_downward

@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 (я использовал индуктивный тип, а не псевдоним типа, чтобы Идрис не разворачивал его в контексте дыры; так его легче читать).

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
person gallais    schedule 01.07.2017