4

我试图使用匹配类型在 Dotty 中实现SKI 组合器演算。

SKI 组合微积分的简要说明：

  • S, K, 和I是项
  • (xy)is an term if xand yare terms and is like 函数应用
  • (((Sx)y)z)(same as Sxyz) 返回xz(yz)(same as (xz)(yz))
  • ((Kx)y)（相同Kxy）返回x
  • (Ix)返回x

以下是我使用R的（尽可能减少术语）。一个术语(xy)被写成一个元组(x,y), 和S, K, 和I是特征。

trait S
trait K
trait I

type R[T] = T match {
  case (((S,x),y),z) => R[((x,z),(y,z))]
  case ((K,x),y) => R[x]
  case (I,x) => R[x]
  case (a,b) => R[a] match {
    case `a` => (a, R[b])
    case _ => R[(R[a], R[b])]
  }
  case T => T
}

但是，以下 2 行无法编译（出于相同的原因）（Scastie）：

val check: (K, K) = ??? : R[(((S,I),I),K)]
val check2: (K, K) = ??? : R[((I,K),(I,K))]

该错误说它需要(K,K)但找到R[((I, K), (I, K))]。我希望它首先看到 S 并将其变成(IK)(IK)，或者R[((I,K),(I,K))]，之后它应该匹配第一个的评估(I, K)并看到它是K，这与(I, K)使其返回R[(R[(I,K)], R[(I,K)])]，它成为R[(K,K)]，它成为正义(K,K)。

然而，它并没有超越R[((I,K),(I,K))]。显然，如果它是嵌套的，它不会减少术语。这很奇怪，因为我尝试了相同的方法，但使用了实际的运行时函数，而且它似乎工作正常（Scastie）。

case object S
case object K
case object I

def r(t: Any): Any = t match {
  case (((S,x),y),z) => r(((x,z),(y,z)))
  case ((K,x),y) => r(x)
  case (I,x) => r(x)
  case (a,b) => r(a) match {
    case `a` => (a, r(b))
    case c => (c, r(b))
  }
  case _ => t
}

正如预期的那样，来自println(r((((S, I), I), K)))的输出。(K,K)

有趣的是，删除它的规则K让它可以编译，但它不能识别(K, K)和R[(K, K)]作为同一类型。也许这就是导致问题的原因？（斯卡斯蒂）

def check2: (K, K) = ??? : R[(K, K)]
//Found:    R[(K, K)]
//Required: (K, K)
4

1 回答 1

6

S, K, 并且I不相交。十字路口K with I等有人居住：

println(new K with I)

在匹配类型中，仅当类型不相交时才会跳过大小写。所以，例如这失败了：

type IsK[T] = T match {
  case K => true 
  case _ => false
}
@main def main() = println(valueOf[IsK[I]])

因为case K => _分支不能被跳过，因为它的值是Is 。因此，例如，在您的情况下会卡在 s 上，因为有些s 也是s （例如）。你永远不会到达，这将带我们去。 KR[(K, K)]case (I, x) => _(K, K)(I, x)(new K with I, new K {})case (a,b) => _(K, K)

您可以制作S、K和I classes，这会使它们不相交，因为您不能class一次从两个 es 继承。

class S
class K
class I

type R[T] = T match {
  case (((S,x),y),z) => R[((x,z),(y,z))]
  case ((K,x),y) => R[x]
  case (I,x) => R[x]
  case (a,b) => R[a] match {
    case `a` => (a, R[b])
    case _ => R[(R[a], R[b])]
  }
  case T => T
}

@main def main(): Unit = {
  println(implicitly[R[(K, K)] =:= (K, K)])
  println(implicitly[R[(((S,I),I),K)] =:= (K, K)])
}

斯卡斯蒂

另一种解决方案是将它们全部设为单例类型：

object S; type S = S.type
object K; type K = K.type
object I; type I = I.type
// or, heck
type S = 0
type K = 1
type I = 2
于 2020-08-24T19:32:25.517 回答