scala - 使用无形状的Scala证明自然数加法的关联性

以下代码是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, B, C] {
    case (Nat._0, b, c) => refl[Sum[B, C]#Out]
  }
  implicit def caseSucc[K <: Nat, B <: Nat, C <: Nat] = ???
}

我在归纳方面遇到麻烦，并使Scala意识到有2种可能的情况需要递归。编码这部分有技巧吗？

最佳答案

使用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, Nat, 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, M, P] {
    val proof: Plus[M,P] === Plus[M,P] = Leibniz.refl
  }

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