时间戳

首页 > 解决方案 > 如何在 Scala 中证明爆炸原理（ex falso sequitur quodlibet）？

scala - 如何在 Scala 中证明爆炸原理（ex falso sequitur quodlibet）？

问题描述

如何在 Scala 中显示没有构造函数的类型的值有任何结果？我想对值进行模式匹配，让 Scala 告诉我没有模式可以匹配，但我愿意接受其他建议。这是一个简短的例子，说明它为什么有用。

证明否定

在 Scala 中，可以在类型级别定义自然数，例如使用 Peano 编码。

sealed trait Nat
sealed trait Zero extends Nat
sealed trait Succ[N <: Nat] extends Nat

由此我们可以定义一个数字是偶数的含义。零是偶数，任何比偶数多二的数也是偶数。

sealed trait Even[N <: Nat]
sealed case class Base() extends Even[Zero]
sealed case class Step[N <: Nat](evenN: Even[N]) extends Even[Succ[Succ[N]]]

由此我们可以证明例如二是偶数：

val `two is even`: Even[Succ[Succ[Zero]]] = Step(Base())

但是我无法证明一个不是偶数，即使编译器可以告诉我既不Base也Step不能存在于该类型中。

def `one is odd`(impossible: Even[Succ[Zero]]): Nothing = impossible match {
  case _: Base => ???
  case _: Step[_] => ???
}

编译器会很高兴地告诉我，我给出的任何情况都不可能出现 error pattern type is incompatible with expected type，但是将match块留空将是一个编译错误。

有什么方法可以建设性地证明这一点？如果空模式匹配是要走的路 - 我会接受任何版本的 Scala 甚至是宏或插件，只要在类型被占用时我仍然会收到空模式匹配的错误。也许我在叫错树，模式是否匹配错误的想法 - EFQ 可以以其他方式显示吗？

注意：证明一个是奇数可以用另一个（但等效的）均匀度定义来完成——但这不是重点。一个简短的例子说明为什么需要 EFQ：

sealed trait Bottom
def `bottom implies anything`(btm: Bottom): Any = ???

标签： scalaprooftype-level-computationcurry-howard

解决方案

Ex falso quodlibet的意思是“从矛盾中，一切都随之而来”。在标准的 Curry-Howard 编码中，Nothing对应 falsehood，所以下面的简单函数实现了爆炸的原理：

def explode[A]: Nothing => A = n => n

它可以编译，因为它Nothing是如此无所不能，以至于它可以替代任何东西（A）。

但是，这不会给您带来任何好处，因为您最初的假设是

There is no proof for `X`

它遵循

There must be proof for `X => _|_`

是不正确的。这不仅对于直觉/建设性逻辑是不正确的，而且在一般情况下：只要您的系统可以计数，就会有无法证明的真实陈述，因此在每个具有 Peano 自然的一致系统中，必须有一些X 无法X证明的陈述（由 Goedel），并且它们的否定 X => _|_也不能被证明（通过一致性）。

似乎您在这里需要的是某种“反转引理”（在 Pierce 的“类型和编程语言”的意义上），它限制了某些类型的术语可以构造的方式，但我不明白Scala 类型系统中任何可以为您提供此类引理的类型级编码的东西。

推荐阅读