scala - 如何使用匹配类型实现 SKI 组合器演算？

Question

我试图实现 SKI combinator calculus在 Dotty 中使用匹配类型。
SKI 组合子演算的快速描述:

S , K , 和 I是条款

(xy)是一个术语 if x和 y是术语，就像函数应用程序

(((Sx)y)z) (与 Sxyz 相同)返回 xz(yz) (与 (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
}

但是，以下两行无法编译(出于同样的原因)( 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)]作为相同的类型。也许这就是导致问题的原因？ ( Scastie )

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

Answer 1

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 => _不能跳过分支，因为存在 I 的值是 K s。所以，例如在你的情况下 R[(K, K)]卡在 case (I, x) => _ , 因为有一些 (K, K) s 也是 (I, x) s(例如 (new K with I, new K {}) )。您永远无法访问 case (a,b) => _ ，这将带我们到 (K, K) .
您可以制作 S , K , 和 I class es，这使它们不相交，因为您不能从两个 class 继承立即。

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)])
}

Scastie
另一种解决方案是使它们全部为单例类型:

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