如何在Scala中证明爆炸原理？
如何在Scala中证明爆炸原理？
提问于 2018-10-23 05:15:55
在Scala中，我如何证明没有构造函数的类型的值后面有任何东西？我希望对值进行模式匹配，并让Scala告诉我没有模式可以匹配，但我愿意接受其他建议。这里有一个简短的例子来说明为什么它会很有用。
证明否定
在Scala中，可以在类型级别上定义自然数，例如使用Peano编码。
sealed trait Nat
sealed trait Zero extends Nat
sealed trait Succ[N <: Nat] extends Nat由此，我们可以定义一个数字为偶数意味着什么。零是偶数，任何比偶数多2的数字也是偶数。
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[_] => ???
}编译器会很高兴地告诉我，我给出的所有情况都不可能出现错误pattern type is incompatible with expected type，但是将match块留空将是编译错误。
有什么方法可以建设性地证明这一点吗？如果空模式匹配是可行的-我会接受任何版本的Scala，甚至宏或插件，只要我在类型驻留时仍然得到空模式匹配的错误。也许我找错了树，是不是一个模式匹配了错误的想法-- EFQ可以用其他方式显示吗？
注:可以用另一个(但等价的)均匀性定义来证明一个是奇数-但这不是重点。一个简短的例子说明为什么需要EFQ：
sealed trait Bottom
def `bottom implies anything`(btm: Bottom): Any = ???回答 1
Stack Overflow用户
回答已采纳
发布于 2018-10-31 12:21:40
在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))页面原文内容由Stack Overflow提供。腾讯云小微IT领域专用引擎提供翻译支持
原文链接：
https://stackoverflow.com/questions/52937865
复制相关文章
相似问题
腾讯云开发者
