haskell - 在枚举上构建 absurd 谓词的证明时，有什么技巧可以摆脱样板文件？

Question

假设我有

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

以及该类型的谓词，

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

不适用于 Banana , Orange , Lemon和别的。

它 can be said这定义了 WineStock作为 Fruit 的谓词; WineStock Grape为真(因为我们可以构造该类型的值/证明: CanonicalWine)以及 WineStock Apple , 但是 WineStock Banana是错误的，因为该类型没有任何值/证明。

那么，我该如何有效地使用 Not (WineStock Banana) , Not (WineStock Lemon) ， ETC？似乎对于每个 Fruit Grape 之外的构造函数和 Apple ，我不得不编写一个拆分为 WineStock 的案例，某处，充满了 impossible年代:

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