Evidence that two natural numbers are not equal?

Question

Using Shapeless's Nat type, how can I derive evidence that two natural numbers are not equal?

This is what I have so far, but it only proves that a given Nat is not equal to 0. How can I prove that any two Nat values are not equal?

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]] {}
}

score 3 · Accepted Answer · answered Aug 16 '15 at 15:42

Using Shapeless's =:!= is the easiest way to accomplish this, but it's not very generalizable (what if you need to show that two numbers differ by one, etc.?), and often when I start out using it I end up switching to a custom type class.

Your NEq is only missing one piece—you've got the base cases, but you need the inductive step. You know that a Succ is never _0, but you also know that two Succs aren't the same if their contents aren't the same:

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]] {}
}

This will work as expected.

score 1 · Answer 2 · edited May 23 '17 at 11:52

Why not:

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

Example:

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]
                 ^

See also: Type constraint for type inequality in scala

And this, just in case if you want to check it in runtime for some reason.

Evidence that two natural numbers are not equal?

2 Answers2