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

Question

在 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())

但我无法证明 one 不是偶数，即使编译器可以告诉我 Base 和 Step 都不能属于该类型。

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

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

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

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

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

Answer 1

Ex falso quodlibet 表示 "from contradiction, anything follows"。在标准的 Curry-Howard 编码中，Nothing 对应于假的，所以下面这个简单的函数实现了这个原理爆炸：

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

编译通过，因为Nothing无所不能，可以代替任何东西（A）。

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

There is no proof for `X`

由此可见

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

不正确。它不仅对于 intuitionistic/constructive 逻辑是不正确的，而且在一般情况下也是如此：只要您的系统可以 count，那么是无法证明的真实陈述，所以在每一个一致的 Peano naturals 系统必须有一些语句 X 这样 X 无法证明（由 Goedel），并且他们的否定 X => _|_ 也无法证明（通过一致性）。

看来您在这里需要的是某种 "inversion lemma"（在 Pierce 的 "Types and Programming Languages" 意义上），它限制了某些类型的术语的构造方式，但是我在 Scala 的类型系统中没有看到任何东西可以为您提供这种引理的类型级编码。

Answer 2

在 Scala 中可能无法证明 ex falso 为任意无人居住的类型，但仍有可能证明 Even[Succ[Zero]] => Nothing。我的证明只需要对您的 Nat 定义进行少量修改即可解决 Scala 中缺失的功能。这是：

import scala.language.higherKinds

case object True
type not[X] = X => Nothing

sealed trait Nat {
  // These dependent types are added because Scala doesn't support type-level
  // pattern matching, so this is a workaround. Nat is otherwise unchanged.
  type IsZero
  type IsOne
  type IsSucc
}
sealed trait Zero extends Nat {
  type IsZero = True.type
  type IsOne = Nothing
  type IsSucc = Nothing
}
sealed trait Succ[N <: Nat] extends Nat {
  type IsZero = Nothing
  type IsOne = N#IsZero
  type IsSucc = True.type
}

type One = Succ[Zero]

// These definitions should look familiar.
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]]]

// A version of scalaz.Leibniz.===, adapted from
// https://typelevel.org/blog/2014/07/02/type_equality_to_leibniz.html.
sealed trait ===[A <: Nat, B <: Nat] {
  def subst[F[_ <: Nat]](fa: F[A]): F[B]
}

implicit def eqRefl[A <: Nat] = new ===[A, A] {
  override def subst[F[_ <: Nat]](fa: F[A]): F[A] = fa
}

// This definition of evenness is easier to work with. We will prove (the
// important part of) its equivalence to Even below.
sealed trait _Even[N <: Nat]
sealed case class _Base[N <: Nat]()(
  implicit val nIsZero: N === Zero) extends _Even[N]
sealed case class _Step[N <: Nat, M <: Nat](evenM: _Even[M])(
  implicit val nIsStep: N === Succ[Succ[M]]) extends _Even[N]

// With this fact, we only need to prove not[_Even[One]] and not[Even[One]]
// will follow.
def `even implies _even`[N <: Nat]: Even[N] => _Even[N] = {
  case b: Base => _Base[Zero]()
  case s: Step[m] =>
    val inductive_hyp = `even implies _even`[m](s.evenN) // Decreasing on s
    _Step[N, m](inductive_hyp)
}

def `one is not zero`: not[One === Zero] = {
  oneIsZero =>
    type F[N <: Nat] = N#IsSucc
    oneIsZero.subst[F](True)
}

def `one is not _even` : not[_Even[One]] = {
  case base: _Base[One] =>
    val oneIsZero: One === Zero = base.nIsZero
    `one is not zero`(oneIsZero)
  case step: _Step[One, m] =>
    val oneIsBig: One === Succ[Succ[m]] = step.nIsStep
    type F[N <: Nat] = N#IsOne
    oneIsBig.subst[F](True)
}

def `one is odd`: not[Even[One]] =
  even1 => `one is not _even`(`even implies _even`(even1))

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

How to prove the principle of explosion (ex falso sequitur quodlibet) in Scala?

scala

proof

type-level-computation

curry-howard

证明否定