如何在 Scala 2.13 中定义自然数归纳法？

Question

考虑以下自然数的定义。

sealed trait Nat

final case object Z extends Nat

final case class[N <: Nat]() extends Nat

以及向量的以下定义。

sealed trait Vec[N <: Nat, +A]

final case object Nil extends Vec[Z.type, Nothing]

final case class Cons[N <: Nat, +A](head: A, tail: Vec[N, A]) extends Vec[S[N], A]

现在，我对自然数的归纳定义如下。

trait Alg[P[_ <: Nat]] {
  val z: P[Z.type]

  def s[N <: Nat](p: P[N]): P[S[N]]
}

def ind[N <: Nat, P[_ <: Nat]](alg: Alg[P])(implicit indN: Alg[P] => P[N]) = indN(alg)

implicit def indZ[P[_ <: Nat]](): Alg[P] => P[Z.type] = alg => alg.z

implicit def indS[N <: Nat, P[_ <: Nat]](implicit indN: Alg[P] => P[N]): Alg[P] => P[S[N]] = alg => alg.s(indN(alg))

而且，我想用它来定义一个创建固定大小向量的函数。

def rep[N <: Nat, A](head: A) = {
  type P[N <: Nat] = Vec[N, A]

  val alg = new Alg[P] {
    val z: P[Z.type] = Nil

    def s[N <: Nat](tail: P[N]): P[S[N]] = Cons(head, tail)
  }

  ind[N, P](alg) // No implicit view available from Alg[P] => P[N]
}

val vec = rep[S[S[S[Z.type]]], Int](37) // expected Cons(37, Cons(37, Cons(37, Nil)))

不幸的是，这不起作用。 Scala 不知道要使用哪个隐式值。我怎样才能使这项工作？

Answer 1

首先，不要把

()

放在

implicit def indZ[P[_ <: Nat]]()

里。隐式

implicit def indZ[P[_ <: Nat]]()

和

implicit def indZ[P[_ <: Nat]]

非常不同

如何为元组编写隐式数字

方便介绍

type Z = Z.type

。然后你可以只写

而不是

Z.type

.

Scala 不是真正的定理证明器。隐式不是那样解决的。如果您定义了

implicit def indZ

和

implicit def indS

，Scala 知道隐式

indZ

、

indS(indZ)

、

indS(indS(indZ))

、...但它不能生成未知长度的隐式

indS(...(indS(indZ)))

。因此，使用基于隐式的归纳逻辑，您可以证明固定

（如

、

S[Z]

、

S[S[Z]]

、...）的定理，但不能证明任意

（或任意

但具有固定长度的隐式）。在那些你有任意

的地方你应该添加一个证据（隐式参数）

Alg[P] => P[N]

，稍后将检查具体的

.

所以试试

class Rep[A](head: A) {
  type P[N <: Nat] = Vec[N, A]

  val alg = new Alg[P] {
    val z: P[Z] = Nil
    def s[N <: Nat](tail: P[N]): P[S[N]] = Cons(head, tail)
  }

  def apply[N <: Nat](implicit ev: Alg[P] => P[N]): P[N] = ind[N, P](alg)
  //                  ^^^^^^^^^^^^^^^^^^^^^^^^^^^ added
}

val vec = new Rep[Int](37)[S[S[S[Z]]]] // Cons(37, Cons(37, Cons(37, Nil)))

在函数类型的隐式上构建逻辑时要小心