证明使用Scala无形的自然数增加的相关性

发布时间：2020-12-16 09:14:12 所属栏目：安全来源：网络整理

导读：以下代码是Idris： natAssociative : (a : Nat) - (b : Nat) - (c : Nat) - (a + b) + c = a + (b + c)natAssociative Z b c = the (b + c = b + c) reflnatAssociative (S k) b c = replace {P=x = S (k + b) + c = S x} (natAssociative k b c) refl 我很

以下代码是Idris：

natAssociative : (a : Nat) -> (b : Nat) -> (c : Nat) -> (a + b) + c = a + (b + c)
natAssociative Z b c = the (b + c = b + c) refl
natAssociative (S k) b c = replace {P=x => S (k + b) + c = S x} (natAssociative k b c) refl

我很难把这个翻译成无形的.我已经尝试了几个不同的编码,但我认为这是最有希望的开始：

import scalaz.Leibniz._
import shapeless.{ HNil,Nat,Succ,Poly3 }
import shapeless.Nat._
import shapeless.ops.nat._

object natAssociative extends Poly3 {
  implicit def case0[B <: Nat,C <: Nat]: Case[_0,B,C] = at[_0,C] {
    case (Nat._0,b,c) => refl[Sum[B,C]#Out]
  }
  implicit def caseSucc[K <: Nat,B <: Nat,C <: Nat] = ???
}

我感到困扰,Scala认识到我们有两种可能的情况来递归.有没有编码这个部分的技巧？

解决方法

随着Nat和Sum的定义在无形中,你不能真正证明任何东西.那是因为Sum不是函数,具有相同的参数,我们可以有不同的结果：

object Pooper {
  implicit def invalidSum: Sum[_1,_1] = new Sum[_1,_1] {
    type Out = _3
  }
}

但是,如果我们定义自然和总和有点不同：

package plusassoc

import scala.language.higherKinds
import scalaz.Leibniz

sealed trait Nat {
  type Add[A <: Nat] <: Nat // 1.add(5)
}

case class Zero() extends Nat {
  type Add[A <: Nat] = A
}

case class Succ[N <: Nat]() extends Nat {
  type Add[A <: Nat] = Succ[N#Add[A]]
}

// a for aliases
package object a {
  // Equality on nats
  type ===[A <: Nat,B <: Nat] = Leibniz[Nothing,A,B]

  type Plus[A <: Nat,B <: Nat] = A#Add[B]

  type One = Succ[Zero]
  type Two = Succ[One]
  type Three = Succ[Two]
}

import a._

Add(和Plus)现在表现良好的类型级别的功能.

然后我们可以写出Plus的关联性证明：

/*
  plus-assoc : ? n m p → (n + (m + p)) ≡ ((n + m) + p)
  plus-assoc zero m p = refl
  plus-assoc (suc n) m p = cong suc (plus-assoc n m p)
*/
trait PlusAssoc[N <: Nat,M <: Nat,P <: Nat] {
  val proof: Plus[N,Plus[M,P]] === Plus[Plus[N,M],P]
}

object PlusAssoc {
  implicit def plusAssocZero[M <: Nat,P <: Nat]: PlusAssoc[Zero,M,P] = new PlusAssoc[Zero,P] {
    val proof: Plus[M,P] === Plus[M,P] = Leibniz.refl
  }

  implicit def plusAssocSucc[N <: Nat,P <: Nat](implicit
    ih: PlusAssoc[N,P]): PlusAssoc[Succ[N],P] = new PlusAssoc[Succ[N],P] {
      // For some reason scalac fails to infer right params for lift :(
      val proof: Succ[Plus[N,P]]] === Succ[Plus[Plus[N,P]] = Leibniz.lift[
        Nothing,Nothing,Plus[N,P]],Plus[Plus[N,P]
      ](ih.proof)
    }
}

当我们依赖于隐含的情况时,我们必须测试,scalac可以真正使用我们的“规则”来构建证据：

import plusassoc._
import plusassoc.a._
import plusassoc.PlusAssoc._

implicitly[PlusAssoc[One,Two,Three]].proof
res0: ===[Plus[One,Plus[Two,Three]],Plus[Plus[One,Two],Three]] = scalaz.LeibnizFunctions$$anon$2@7b2c4c00
// with plusassoc.a. prefix skipped

（编辑：李大同）

【声明】本站内容均来自网络，其相关言论仅代表作者个人观点，不代表本站立场。若无意侵犯到您的权利，请及时与联系站长删除相关内容!