我试图使用匹配类型在 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
是特征。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)]
识别为同一类型。也许这就是造成问题的原因? (斯卡斯蒂)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 => _
分支不能被跳过,因为
I
的值是
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
。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