构造枚举类型的荒谬断言证明时，有什么技巧可以摆脱样板代码？

Question

假设我有

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

以及该类型的谓词条件,

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

"which doesn't hold for Banana, Orange, Lemon and others." -> "这不适用于香蕉、橙子、柠檬和其他水果。" "It can be said that this defines WineStock as a predicate on Fruit; WineStock Grape is true (since we can construct a value/proof of that type: CanonicalWine) as well as WineStock Apple, but WineStock Banana is false, since that type is not inhabited by any values/proofs." -> "可以说这将WineStock定义为Fruit的一个谓词；WineStock Grape为true（因为我们可以构造该类型的值/证据：CanonicalWine），WineStock Apple也是true，但WineStock Banana为false，因为该类型没有任何值/证据。"

---

那么，我该如何有效地使用Not (WineStock Banana)，Not (WineStock Lemon)等呢？除了Grape和Apple构造函数外，对于每个Fruit构造函数，我似乎都不得不在某个地方编写一个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

请注意：

• 代码重复性高，
• 当谓词定义增长并获得更多构造函数时，行数将爆炸。 想象一下 Fruit 定义中有许多甜的替代品时，Not (Sweet Lemon) 证明就会变得非常冗长。

因此，这种方法似乎不太令人满意，几乎是不切实际的。

是否有更优雅的方法？

- ulidtko

---

许多旧的Haskell习语在依赖类型的系统中并没有改变。 "使非法状态无法表示" 在类型层面上也适用：我认为您甚至不应该能够构造这些不可能的类型。 我可能会将此示例结构化为（大致类似于）可以制作葡萄酒的水果类型 data WineFruit = Grape | Apple，以及其他水果类型 data Fruit = WineFruit WineFruit | Banana | Orange | Lemon。 - Benjamin Hodgson

@BenjaminHodgson，当你想要添加"PieFruit"、"SaladFruit"、"WeaponFruit"等时，该方法开始变得不可行了。 - dfeuer

既然你在使用 Idris，为什么要定义一个 WineStock 的数据类型呢？你不能只定义一个值级别的函数 isWineStock 并在适当的证明中使用它吗？ - sclv

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 确保元素 x 满足属性 p（我使用归纳类型而不是类型别名，这样Idris在上下文中不会展开它；这样更容易阅读）。

isnt prf 在类型检查器能够自动生成证明 p a = False 的情况下（通过 Refl 或上下文中的假设），驳回伪造的证明 prf。

有了这些，您可以通过仅枚举正面案例并添加一个万能匹配来开始定义属性。

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

- gallais