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

问题描述

我试图使用匹配类型在Dotty中实现SKI combinator calculus。

SKI组合器演算的快速描述：

• S，K和I是术语
如果(xy)和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,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),K)]
val check2: (K,K) = ??? : R[((I,K),(I,K))]

该错误表明它需要(K,K)但找到了R[((I,K))]。我希望它首先看到S，然后将其变成(IK)(IK)或R[((I,K))]，之后它应该与第一个(I,K)的求值相匹配，并看到它是K，与(I,K)不同，使其返回R[(R[(I,K)],R[(I,K)])]，它变成R[(K,K)]，而变成(K,K)。

但是，它不能超过R[((I,K))]。显然，它不会减少嵌套的术语。这很奇怪，因为我尝试了相同的方法，但是使用了实际的运行时功能，并且看来工作正常（Scastie）。

case object S
case object K
case object I

def r(t: Any): Any = t match {
  case (((S,z) => r(((x,z)))
  case ((K,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,K)))的输出为(K,K)。

足够有趣的是，删除K的规则可以对其进行编译，但是不能将(K,K)和R[(K,K)]识别为同一类型。也许这是引起问题的原因？ （Scastie）

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

解决方法

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 => _分支，因为存在{em>是 I的{​​{1}}值。因此，例如在您的情况下，K被卡在R[(K,K)]上，因为存在 某些case (I,x) => _也是(K,K)（例如(I,x) ）。您永远不会进入(new K with I,new K {})，而这会带我们去case (a,b) => _。

您可以创建(K,K)，S和K I，这使它们不相交，因为您不能从两个class继承一次。

class

Scastie

另一种解决方案是使它们成为所有单例类型：

class S
class K
class I

type R[T] = T match {
  case (((S,x),y),z) => R[((x,z),(y,z))]
  case ((K,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),K)])
}