两个自然数不相等的证据？答案

【问题标题】：Evidence that two natural numbers are not equal?两个自然数不相等的证据？
【发布时间】：2015-08-16 23:42:03
【问题描述】：

使用 Shapeless 的 Nat 类型，我如何得出两个自然数不相等的证据？

这是我目前所拥有的，但它只证明给定的Nat 不等于0。如何证明任意两个Nat 值不相等？

trait NEq[A <: Nat, B <: Nat] extends Serializable

object NEq {
  def apply[A <: Nat, B <: Nat](implicit neq: A != B): NEq[A, B] = neq

  type !=[A <: Nat, B <: Nat] = NEq[A, B]

  implicit def neq1[B <: Nat] = new !=[Succ[B], _0] {}
  implicit def neq2[B <: Nat] = new !=[_0, Succ[B]] {}
}

【问题讨论】：

标签： scala shapeless

【解决方案1】：

使用 Shapeless 的 =:!= 是完成此任务的最简单方法，但它不是很通用（如果您需要证明两个数字相差 1 怎么办？），而且通常当我开始使用它时，我会结束向上切换到自定义类型类。

您的NEq 只缺少一件——您已经掌握了基本情况，但您需要归纳步骤。你知道Succ 永远不会是_0，但你也知道如果两个Succs 的内容不同，它们就不一样：

trait NEq[A <: Nat, B <: Nat] extends Serializable

object NEq {
  def apply[A <: Nat, B <: Nat](implicit neq: A != B): NEq[A, B] = neq

  type !=[A <: Nat, B <: Nat] = NEq[A, B]

  implicit def neq1[B <: Nat]: Succ[B] != _0 = new !=[Succ[B], _0] {}
  implicit def neq2[B <: Nat]: _0 != Succ[B] = new !=[_0, Succ[B]] {}

  implicit def neq3[A <: Nat, B <: Nat](implicit neq: A != B): Succ[A] != Succ[B] =
    new !=[Succ[A], Succ[B]] {}
}

这将按预期工作。

【讨论】：

【解决方案2】：

为什么不：

 def neq[A <: Nat, B <: Nat](implicit ev: A <:!< B) = ev

例子：

scala> neq[_1, _2]
res8: shapeless.<:!<[shapeless.nat._1,shapeless.nat._2] = shapeless.package$$anon$2@7db44dae

scala> neq[_1, _1]
<console>:15: error: ambiguous implicit values:
 both method nsubAmbig1 in package shapeless of type [A, B >: A]=> shapeless.<:!<[A,B]
 and method nsubAmbig2 in package shapeless of type [A, B >: A]=> shapeless.<:!<[A,B]
 match expected type shapeless.<:!<[shapeless.nat._1,shapeless.nat._1]
              neq[_1, _1]
                 ^

另请参阅：Type constraint for type inequality in scala

还有this，以防万一你出于某种原因想在运行时检查它。

【讨论】：