如何解决如何使用匹配类型实现SKI组合器演算?
我试图使用匹配类型在Dotty中实现SKI combinator calculus。
SKI组合器演算的快速描述:
-
S
,K
和I
是术语
如果 -
y
是一个术语 -
(((Sx)y)z)
(与Sxyz
相同)返回xz(yz)
(与(xz)(yz)
相同) -
((Kx)y)
(与Kxy
相同)返回x
-
(Ix)
返回x
(xy)
和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
另一种解决方案是使它们成为所有单例类型:
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)])
}
版权声明:本文内容由互联网用户自发贡献,该文观点与技术仅代表作者本人。本站仅提供信息存储空间服务,不拥有所有权,不承担相关法律责任。如发现本站有涉嫌侵权/违法违规的内容, 请发送邮件至 dio@foxmail.com 举报,一经查实,本站将立刻删除。