如何询问Scala是否存在所有类型参数实例化的证据？

html5 • • 问答

给定以下 Peano 数的类型级加法函数

sealed trait Nat
class O extends Nat
class S[N <: Nat] extends Nat

type plus[a <: Nat, b <: Nat] = a match
  case O => b
  case S[n] => S[n plus b]

说我们想证明定理

对于所有自然数 n，n + 0 = n

也许可以这样指定

type plus_n_0 = [n <: Nat] =>> (n plus O) =:= n

那么在为定理提供证据时，我们可以很容易地向 Scala 编译器询问特定情况下的证据

summon[plus_n_O[S[S[O]]]]  // ok, 2 + 0 = 2

但是我们如何询问 Scala 是否可以为 的所有实例生成证据[n <: Nat]，从而提供 的证明plus_n_0？

回答

这是一种可能的方法，它是对这一段的字面解释的尝试：

当证明一个E:N?U关于所有自然数的陈述时，只要证明它 for0和 for就足够了succ(n)，假设它对 成立n，即我们构造ez:E(0)和es:?(n:N)E(n)?E(succ(n))。

来自HoTT 书（第 5.1 节）。

这是在下面的代码中实现的计划：

  • 制定证明“某些性质P适用于所有自然数”的陈述意味着什么。下面，我们将使用

     trait Forall[N, P[n <: N]]:
   inline def apply[n <: N]: P[n]

    其中apply-method的签名本质上是说“对于所有n <: N，我们可以生成“的证据P[n]。

    请注意，该方法声明为inline. 这是确保 的证明?n.P(n)在运行时具有建设性和可执行性的一种可能方法（但是，请参阅手动生成见证条款的替代提案的编辑历史记录）。

  • 假设某种自然数的归纳原理。下面，我们将使用以下公式：

     If
    P(0) holds, and
    whenever P(i) holds, then also P(i + 1) holds,
 then
    For all `n`, P(n) holds

    我相信derive使用一些元编程工具应该可以实现这样的归纳原则。

  • 写出归纳原理的基本情况和归纳情况的证明。

  • ???

  • 利润

代码如下所示：

sealed trait Nat
class O extends Nat
class S[N <: Nat] extends Nat

type plus[a <: Nat, b <: Nat] <: Nat = a match
  case O => b
  case S[n] => S[n plus b]

trait Forall[N, P[n <: N]]:
  inline def apply[n <: N]: P[n]

trait NatInductionPrinciple[P[n <: Nat]] extends Forall[Nat, P]:
  def base: P[O]
  def step: [i <: Nat] => (P[i] => P[S[i]])
  inline def apply[n <: Nat]: P[n] =
    (inline compiletime.erasedValue[n] match
      case _: O => base
      case _: S[pred] => step(apply[pred])
    ).asInstanceOf[P[n]]

given liftCoUpperbounded[U, A <: U, B <: U, S[_ <: U]](using ev: A =:= B):
  (S[A] =:= S[B]) = ev.liftCo[[X] =>> Any].asInstanceOf[S[A] =:= S[B]]

type NatPlusZeroEqualsNat[n <: Nat] = (n plus O) =:= n

def trivialLemma[i <: Nat]: ((S[i] plus O) =:= S[i plus O]) =
  summon[(S[i] plus O) =:= S[i plus O]]

object Proof extends NatInductionPrinciple[NatPlusZeroEqualsNat]:
  val base = summon[(O plus O) =:= O]
  val step: ([i <: Nat] => NatPlusZeroEqualsNat[i] => NatPlusZeroEqualsNat[S[i]]) = 
    [i <: Nat] => (p: NatPlusZeroEqualsNat[i]) =>
      given previousStep: ((i plus O) =:= i) = p
      given liftPreviousStep: (S[i plus O] =:= S[i]) =
        liftCoUpperbounded[Nat, i plus O, i, S]
      given definitionalEquality: ((S[i] plus O) =:= S[i plus O]) =
        trivialLemma[i]
      definitionalEquality.andThen(liftPreviousStep)

def demoNat(): Unit = {
  println("Running demoNat...")
  type two = S[S[O]]
  val ev = Proof[two]
  val twoInstance: two = new S[S[O]]
  println(ev(twoInstance) == twoInstance)
}

它编译、运行和打印：

true

这意味着我们已经成功地在类型为 的可执行证据项上调用了递归定义的方法two plus O =:= two。

一些进一步的评论

  • 这trivialLemma是必要的，以便summons 内部的 other givens 不会意外生成递归循环，这有点烦人。
  • 需要单独的liftCo-method for S[_ <: U]，因为=:=.liftCo不允许具有上限类型参数的类型构造函数。
  • compiletime.erasedValue+inline match太棒了！它会自动生成某种运行时小工具，允许我们对“已擦除”类型进行模式匹配。在我发现这一点之前，我试图手动构建适当的见证条款，但这似乎根本没有必要，它是免费提供的（请参阅编辑历史以了解手动构建见证条款的方法）。
以上是如何询问Scala是否存在所有类型参数实例化的证据？的全部内容。
THE END
分享
二维码
< <上一篇
下一篇>>