我试图用匹配类型在dotty中实现ski组合子演算。
ski combinator微积分的快速描述: 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)
1条答案
按热度按时间5hcedyr01#
S
,K
,和I
不是不相交的。十字路口K with I
等有人居住:在匹配类型中,仅当类型不相交时才跳过大小写。例如,这失败了:
因为
case K => _
无法跳过分支,因为存在I
是的K
s。比如说,你的情况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
class
是的,这使得它们不相交,因为你不能从两个继承class
一下子就有了。斯卡斯蒂
另一个解决方案是使它们都是单例类型: