考虑以下自然数的定义。
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 不知道要使用哪个隐式值。我怎样才能使这项工作?
首先,不要把
()
放在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]
. 上构建归纳逻辑会更好
了解如何调试隐式(在编译时)很重要