Доказательство того, что два натуральных числа не равны?

Question

Использование типа 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]] {} 
} 

Answer 1

Использование Shapeless =:!= - это самый простой способ выполнить это, но это не очень обобщаемо (что, если вам нужно показать, что два числа отличаются друг от друга и т. Д.?), И часто, когда я начинаю использовать его, я в конечном итоге переход к классу пользовательского типа.

Ваш NEq отсутствует только одна штука - у вас есть базовые чехлы, но вам необходим индуктивный шаг. Вы знаете, что Succ никогда не _0, но вы также знаете, что два Succ s не то же самое, если их содержание не то же самое:

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

Это будет работать, как ожидалось.

Answer 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, только в том случае, если вы хотите, чтобы проверить его во время выполнения для некоторых причина.