如何使用匹配类型实现 SKI 组合器演算? [英] How to implement the SKI combinator calculus with match types?

问题描述

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

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 是特质.

特质 S性状K特质一类型 R[T] = T 匹配 {case (((S,x),y),z) =>R[((x,z),(y,z))]case ((K,x),y) =>R[x]情况(I，x)=>R[x]情况(a，b)=>R[a] 匹配 {案例`a` =>(a, R[b])案例_ =>R[(R[a], R[b])]}情况T＝＞吨}

但是，以下两行无法编译(出于同样的原因)(Scastie):

val 检查:(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))].显然，如果它是嵌套的，它不会减少该术语.这很奇怪，因为我尝试了相同的方法，但使用了实际的运行时函数，并且它似乎可以正常工作 (斯卡斯蒂).

case 对象 S案例对象K案例对象 Idef r(t: Any): Any = t match {case (((S,x),y),z) =>r(((x,z),(y,z)))case ((K,x),y) =>r(x)情况(I，x)=>r(x)情况(a，b)=>r(a) 匹配 {案例`a` =>(a, r(b))情况c＝＞(c, r(b))}案例_ =>吨}

println(r(((S, I), I), K))) 的输出是 (K,K)，正如预期的那样.

有趣的是，删除 K 的规则让它编译，但它不识别 (K, K) 和 R[(K, K)] 为同一类型.也许这就是导致问题的原因?(Scastie)

def check2: (K, K) = ???: R[(K, K)]//找到:R[(K, K)]//必填:(K, K)

解决方案

S、K 和 I 不是不相交的.K 与 I 等交叉点有人居住:

println(new K with I)

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

type IsK[T] = T 匹配 {情况K＝＞真的案例_ =>错误的}@main def main() = println(valueOf[IsK[I]])

因为case K =>_ 分支不能被跳过，因为有 I 的值 是 Ks.所以，例如在你的情况下 R[(K, K)] 卡在 case (I, x) =>_，因为有一些(K, K)同时也是(I, x)s(例如(new K with I, new K {})).你永远不会遇到 case (a,b) =>_，这将带我们到 (K, K).

您可以使 S、K 和 I classes，这使它们不相交，因为您不能同时从两个 class 继承.

S 类K级一级类型 R[T] = T 匹配 {case (((S,x),y),z) =>R[((x,z),(y,z))]case ((K,x),y) =>R[x]情况(I，x)=>R[x]情况(a，b)=>R[a] 匹配 {案例`a` =>(a, R[b])案例_ =>R[(R[a], R[b])]}情况T＝＞吨}@main def main(): Unit = {println(隐式[R[(K, K)] =:= (K, K)])println(隐式[R[(((S,I),I),K)] =:= (K, K)])}

Scastie

另一种解决方案是让它们都成为单例类型:

对象 S;类型 S = S.type对象K；类型 K = K.type对象我;类型 I = I.type//或者，见鬼类型 S = 0类型 K = 1类型 I = 2

I was trying to implement the SKI combinator calculus in Dotty using match types.

A quick description of the SKI combinator calculus:

• S, K, and I are terms
• (xy) is a term if x and y are terms and is like function application
• (((Sx)y)z) (same asSxyz) returns xz(yz) (same as (xz)(yz))
• ((Kx)y) (same as Kxy) returns x
• (Ix) returns x

Below is what I used (R reduces the term as much as possible). A term (xy) is written as a tuple (x,y), and S, K, and I are traits.

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
}

However, the following 2 lines don't compile (both for the same reason) (Scastie):

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

The error says that it required (K,K) but found R[((I, K), (I, K))]. I expected it first see the S and turn it into (IK)(IK), or R[((I,K),(I,K))], after which it should match the evaluation of the first (I, K) and see that it is K, which is not the same as (I, K), making it return R[(R[(I,K)], R[(I,K)])], which becomes R[(K,K)], which becomes just (K,K).

However, it doesn't go beyond R[((I,K),(I,K))]. Apparently, it does not reduce the term if it's nested. This is odd, because I tried the same approach but with an actual runtime function, and it appears to work properly (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
}

The output from println(r((((S, I), I), K))) is (K,K), as expected.

Interestingly enough, removing the rule for K lets it compile, but it doesn't recognize (K, K) and R[(K, K)] as the same type. Perhaps this is what is causing the problem? (Scastie)

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

解决方案

S, K, and I are not disjoint. The intersections K with I etc. are inhabited:

println(new K with I)

In a match type, a case is only skipped when the types are disjoint. So, e.g. this fails:

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

because the case K => _ branch cannot be skipped, since there are values of I that are Ks. So, e.g. in your case R[(K, K)] gets stuck on case (I, x) => _, since there are some (K, K)s that are also (I, x)s (e.g. (new K with I, new K {})). You never get to the case (a,b) => _, which would take us to (K, K).

You can make S, K, and I classes, which makes them disjoint, since you can't inherit from two classes at once.

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

Another solution is making them all singleton types:

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

这篇关于如何使用匹配类型实现 SKI 组合器演算?的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！