假设我有
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)
证明就会变得非常冗长。
因此,这种方法似乎不太令人满意,几乎是不切实际的。
是否有更优雅的方法?
data WineFruit = Grape | Apple
,以及其他水果类型data Fruit = WineFruit WineFruit | Banana | Orange | Lemon
。 - Benjamin HodgsonWineStock
的数据类型呢?你不能只定义一个值级别的函数isWineStock
并在适当的证明中使用它吗? - sclv