如何在Scala中证明爆炸原理(ex falso sequitur quodlibet)？

发布时间：2020-12-16 18:13:48 所属栏目：安全来源：网络整理

导读：如何在 Scala中没有构造函数的类型的值中显示任何内容？我想对值进行模式匹配,并让Scala告诉我没有模式可以匹配,但我愿意接受其他建议.这是一个简短的例子,说明它有用的原因. 证明否定在Scala中,可以在类型级别定义自然数,例如与Peano编码. sealed trait Na

如何在 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[_] => ???
}

编译器很高兴地告诉我,我给出的所有情况都不可能与错误模式类型的预期类型不兼容,但是将匹配块保留为空将是编译错误.

有没有办法建设性地证明这一点？如果空模式匹配是要走的路 – 我会接受任何版本的Scala甚至是宏或插件,只要在类型有人居住时仍然会出现空模式匹配的错误.也许我正在咆哮错误的树,是一个模式匹配错误的想法 – EFQ可以以其他方式显示？

注意：证明一个是奇数可以用另一个(但等价的)均匀度定义来完成 – 但这不是重点.可能需要EFQ的简短示例：

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

解决方法

对于Scala中任意无人居住的类型,可能无法证明这一点,但仍有可能证明Even [Succ [Zero]] =>没有.我的证明只需对您的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))

（编辑：李大同）

【声明】本站内容均来自网络，其相关言论仅代表作者个人观点，不代表本站立场。若无意侵犯到您的权利，请及时与联系站长删除相关内容!