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

问题描述 投票:0回答:1

考虑以下自然数的定义。

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 不知道要使用哪个隐式值。我怎样才能使这项工作?

scala implicit dependent-type scala-2.13 peano-numbers
1个回答
1
投票

首先,不要把

()
放在
implicit def indZ[P[_ <: Nat]]()
里。隐式
implicit def indZ[P[_ <: Nat]]()
implicit def indZ[P[_ <: Nat]]
非常不同

如何为元组编写隐式数字

方便介绍

type Z = Z.type
。然后你可以只写
Z
而不是
Z.type
.

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

implicit def indZ
implicit def indS
,Scala 知道隐式
indZ
indS(indZ)
indS(indS(indZ))
、...但它不能生成未知长度的隐式
indS(...(indS(indZ)))
。因此,使用基于隐式的归纳逻辑,您可以证明固定
N
(如
Z
S[Z]
S[S[Z]]
、...)的定理,但不能证明任意
N
(或任意
N
但具有固定长度的隐式)。在那些你有任意
N
的地方你应该添加一个证据(隐式参数)
Alg[P] => P[N]
,稍后将检查具体的
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)))

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

Alg[P] => P[N]
。函数类型对隐式起着特殊的作用,它们用于隐式转换,并且此类隐式的解析与所有其他类型的隐式略有不同

隐式视图不起作用-我的隐式定义应该受到指责吗?

在 scala 中,是否存在隐式视图无法传播到其他隐式函数的情况?

使用编译期宏调用scala函数时,编译错误时如何顺利进行failover?

Scala Kleisli 在 IntelliJ 中抛出错误

解析隐式转换的类型推断有哪些隐藏规则?

这在 Scala 3 中已修复(尽管目前比 Scala 2 有更多限制,例如,目前不可能隐式转换为路径相关类型)https://docs.scala-lang.org/scala3/reference/contextual /conversions.html

引入新的类型类

TC[P[_ <: N], N <: Nat]
并在
TC[P, N]
而不是标准功能类型
Alg[P] => P[N]
.

上构建归纳逻辑会更好

了解如何调试隐式(在编译时)很重要

在 scala 2 或 3 中,是否可以在运行时调试隐式解析过程?

© www.soinside.com 2019 - 2024. All rights reserved.