如何问Scala类型参数的所有实例化是否都存在证据? [英] How to ask Scala if evidence exists for all instantiations of type parameter?

问题描述

在Peano编号上提供以下类型级别的加法功能

Given the following type-level addition function on Peano numbers

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

for all natural numbers n, n + 0 = n

也许可以这样指定

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

然后，在为定理提供证据时，我们可以轻松地向Scala编译器寻求特定情况下的证据

then when it comes to providing evidence for theorem we can easily ask Scala compiler for evidence in particular cases

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

但是我们怎么问Scala是否可以为 [n< ;: Nat] 的所有实例生成证据，从而提供 plus_n_0 的证据?

but how can we ask Scala if it can generate evidence for all instantiations of [n <: Nat], thus providing proof of plus_n_0?

推荐答案

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

Here is one possible approach, which is an attempt at a literal interpretation of this paragraph:

当证明关于所有自然数的语句 E:N→U 时，足以证明 0 和 succ(n)，假设它适用于 n ，即我们构造 ez:E(0)和 es:∏(n:N)E(n)→E(succ(n)).

When proving a statement E:N→U about all natural numbers, it suffices to prove it for 0 and for succ(n), assuming it holds for n, i.e., we construct ez:E(0) and es:∏(n:N)E(n)→E(succ(n)).

来自 HoTT书(第5.1节).

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

Here is the plan of what was implemented in the code below:

• 计算出对某些属性 P 对所有自然数均成立"的陈述进行证明的含义.下面，我们将使用

• Formulate what it means to have a proof for a statement that "Some property P holds for all natural numbers". Below, we will use

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

其中 apply 方法的签名实际上表示对于所有 n< ;: N ，我们可以生成 P [n] ".

where the signature of the apply-method essentially says "for all n <: N, we can generate evidence of P[n]".

请注意，该方法已声明为 inline .这是确保∀nP(n)的证明在运行时具有建设性和可执行性的一种可能方法(但是，请参阅编辑历史以获取具有人工生成的见证词的替代建议).

Note that the method is declared to be inline. This is one possible way to ensure that the proof of ∀n.P(n) is constructive and executable at runtime (However, see edit history for alternative proposals with manually generated witness terms).

为自然数假设某种归纳原理.下面，我们将使用以下公式:

Postulate some sort of induction principle for natural numbers. Below, we will use the following formulation:

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

我相信可以使用一些元编程工具来推导这样的归纳原理.

I believe that it should be possible to derive such induction principles using some metaprogramming facilities.

为归纳原理的基本情况和归纳情况编写证明.

Write proofs for the base case and the induction case of the induction principle.

???

利润

代码如下:

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)
}

它可以编译，运行和打印:

It compiles, runs, and prints:

true

表示我们已经成功调用了递归定义类型为 two加O =:= O 的可执行证据项的方法.

meaning that we have successfully invoked the recursively defined method on the executable evidence-term of type two plus O =:= O.

一些其他评论

• trivialLemma 是必需的，这样其他 give 内部的 summon 不会意外生成递归循环，这有点烦人
• 需要用于 S [_< ;: U] 的单独的 liftCo 方法，因为 =:=.liftCo 不允许具有上限类型参数的类型构造函数.
• compiletime.erasedValue + 内嵌匹配太棒了！它自动生成某种类型的运行时小控件，使我们能够对擦除"的文件进行模式匹配.类型.在我发现这一点之前，我曾尝试过手动构建适当的见证词，但这似乎根本没有必要，它是免费提供的(有关使用人工构建的见证词的方法，请参见编辑历史记录.)

• The trivialLemma was necessary so that summons inside of other givens don't accidentally generate recursive loops, which is a bit annoying.
• The separate liftCo-method for S[_ <: U] was needed, because =:=.liftCo does not allow type constructors with upper-bounded type parameters.
• compiletime.erasedValue + inline match is awesome! It automatically generates some sort of runtime-gizmos that allow us to do pattern matching on an "erased" type. Before I found this out, I was attempting to construct appropriate witness terms manually, but this does not seem necessary at all, it's provided for free (see edit history for the approach with manually constructed witness terms).

这篇关于如何问Scala类型参数的所有实例化是否都存在证据?的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！