scala - 你怎么说一个证明是空类型的(即假)

Question

我想编写一个将 Nat 作为参数的函数，并且仅当此 nat 不能被三整除时才返回此 nat。

例如 :

def myFunction[N <: Nat](n :N)(implicit ev: /* what do I put here that say not divible by 3 ? */): N = n

要做到这一点，我必须写一些东西说“N 不能被 _3 整除”，或者“Mod.Aux[N, _3,_0] 是空类型”

我怎么能在无形中做到这一点？

Answer 1

在这种特殊情况下，最简单的方法可能就是使用 =:!= (但请注意，您需要一个新的类型参数):

import shapeless._, nat._, ops.nat.Mod

def myFunction[N <: Nat, R <: Nat](n: N)
  (implicit mod: Mod.Aux[N, _3, R], neq: R =:!= _0) = n

更一般地，将这种约束表示为类型类并不太难:

trait NotDivBy3[N <: Nat]

object NotDivBy3 {
  implicit def notDivBy3[N <: Nat]: NotDivBy3[N] = new NotDivBy3[N] {}

  implicit def notDivBy3Ambig[N <: Nat]
    (implicit ev: Mod.Aux[N, _3, _0]): NotDivBy3[N] = unexpected
}

def myFunction[N <: Nat: NotDivBy3](n: N) = n

或者更一般地说:

trait DoesntHave[N <: Nat, Prop[_ <: Nat]]

object DoesntHave {
  implicit def doesntHave[N <: Nat, Prop[_ <: Nat]]: DoesntHave[N, Prop] =
    new DoesntHave[N, Prop] {}

  implicit def doesntHaveAmbig[N <: Nat, Prop[_ <: Nat]]
    (implicit ev: Prop[N]): DoesntHave[N, Prop] = unexpected
}

type Mod3Is0[N <: Nat] = Mod.Aux[N, _3, _0]
type NotDivBy3[N <: Nat] = DoesntHave[N, Mod3Is0]

def myFunction[N <: Nat: NotDivBy3](n: N) = n

这两种解决方案都使用与 =:!= 相同的机器。 (即，它们依赖于这样一个事实，即如果 Scala 编译器有两个无法确定优先级的候选者，它将无法找到隐式值)。

我可能倾向于采用第二种方法，除非我发现我需要很多这样的相同类型的约束，在这种情况下，第三种可能更简洁。