有了足够的预备知识,之后,下一个问题就是到底能不能做,我们常说c++的模板是图灵完备的,当然Scala也有这种能力。

Yes, We can

一开始给我说Scalatype level meta programmingTuring completeness,我是不相信的,不能你说它完备就完备,我得自己试一试。试一试,一般也就是从模拟图灵机、lambda calculus以及SKI combinator calculus中间搞一个。这三个里面最简单的自然是SKI了。(当然还有SK或者Iota这种更加简化的演算)

SKI Combinator Calculus

像之前介绍过的lambda calculus一样,SKI组合子演算是一个处理表达式的规则系统。图灵机作为描述计算的模型过于复杂,见识过lambda calculus的简介之后,我们会发现SKI组合子演算更加简洁。

lambda calculus中分为三种表达式:变量、函数以及调用,而SKI组合子演算只有两种表达式调用和字幕符号,而且规则也更加简单。顾名思义,SKI组合子是指S K I三个组合子,它们分别有自己的规约规则。

  • S[a][b][c]规约成a[c][b[c]],其实a``bc可以是任何SKI演算表达式的形式。

  • K[a][b]规约成a

  • I[a] 规约成 a

比如对于下面这个例子

  1. I[S][K][S][I[K]] -> S[K][S][I[K]] 规约I

  2. S[K][S][I[K]] -> S[K][S][K] 规约I

  3. S[K][S][K] -> K[K][S[K]] 规约S

  4. K[K][S[K]] -> K 归于K

递归用fixed point combinator

Type level SKI in Scala

对于整个SKI的实现,并不算困难,不过要注意的是规约的顺序,对于一般的normal form应该采用lazy,这在我们之前举得例子见过了。

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
sealed trait Term {
type ap[x <: Term] <: Term
type eval <: Term
}
// S combinator
trait S extends Term {
type ap[x <: Term] = S1[x]
type eval = S
}
trait S1[x <: Term] extends Term {
type ap[y <: Term] = S2[x, y]
type eval = S1[x]
}
trait S2[x <: Term, y <: Term] extends Term {
type ap[z <: Term] = S3[x, y, z]
type eval = S2[x, y]
}
trait S3[x <: Term, y <: Term, z <: Term] extends Term {
type ap[v <: Term] = eval# ap[v]
type eval = x# ap[z]# ap[y# ap[z]]# eval
}

先看看S combinator,首先定义Term,然后定义S,因为需要lazy,所以我们想办法把之后的值包裹起来,等到用的时候在通过eval计算。ap用来表示参数。

S[K][I][C]就可以用S# ap[K]# ap[I]# ap[c],也就说ap可以看做函数,对于S# ap[K]就会返回一个S1[K]

其他的项的形式就差不多了。

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
// The K combinator
trait K extends Term {
type ap[x <: Term] = K1[x]
type eval = K
}
trait K1[x <: Term] extends Term {
type ap[y <: Term] = K2[x, y]
type eval = K1[x]
}
trait K2[x <: Term, y <: Term] extends Term {
type ap[z <: Term] = eval# ap[z]
type eval = x# eval
}
// The I combinator
trait I extends Term {
type ap[x <: Term] = I1[x]
type eval = I
}
trait I1[x <: Term] extends Term {
type ap[y <: Term] = eval# ap[y]
type eval = x# eval
}

然后让我定义一些常量符号,方便测试

1
2
3
4
5
6
7
8
9
10
11
12
trait c extends Term {
type ap[x <: Term] = c
type eval = c
}
trait d extends Term {
type ap[x <: Term] = d
type eval = d
}
trait e extends Term {
type ap[x <: Term] = e
type eval = e
}

测试一下

1
2
3
4
5
// S[K][I][C]
implicitly[S# ap[K]# ap[I]# ap[c]# eval =:= c]
// I[S][K][S][I[K]]
implicitly[I# ap[S]# ap[K]# ap[S]# ap[I# ap[K]]# eval =:= K]

都能顺利编译通过。为了证明Turing completeness还需要一个关键的东西,就是递归。这里用fixed point combinator保证。

SKI中的fixed point也有好几种,其中一种可以长成这样,定义为b形式为S[K[a]][S[I][I]],具体应用

1
2
3
4
5
6
b = S[K[a]][S[I][I]][b]
= K[a][b][S[I][I][b]]
= a[S[I][I][b]]
= a[b[b]]
= a[b[b[b]]]
...

我们定义

1
type b[a <: Term] = S# ap[K# ap[a]]# ap[S# ap[I]# ap[I]]

为了方便检验递归的情况,定义An为应用了几层

1
2
3
4
5
6
7
8
9
10
11
12
13
14
trait A0 extends Term {
type ap[x <: Term] = c
type eval = A0
}
trait A1 extends Term {
type ap[x <: Term] = x# ap[A0]# eval
type eval = A1
}
trait A2 extends Term {
type ap[x <: Term] = x# ap[A1]# eval
type eval = A2
}

然后我们定义用来递归的函数

1
2
3
// 反转类型
type R = S# ap[K# ap[S# ap[I]]]# ap[K]
implicitly[R# ap[c]# ap[d]# eval =:= d# ap[c]# eval]

然后,将它喂给fixed point

1
2
3
4
5
6
type NN1 = b[R]# ap[b[R]]# ap[A0]
type NN2 = b[R]# ap[b[R]]# ap[A1]
type NN3 = b[R]# ap[b[R]]# ap[A2]
// 这里把N3换成任意一个都是对的
implicitly[NN3# eval =:= c]

这说明,这个函数可以执行任意次,我们再看一个没有给终止条件的例子。

1
2
3
4
5
6
7
8
9
10
11
12
13
trait An extends Term {
// 任何时候ap都返回递归调用
type ap[x <: Term] = x# ap[An]# eval
type eval = An
}
// 无穷递归
type NNn = b[R]# ap[b[R]]# ap[An]
// 编译报错
// Error:scalac: Error:
// org.jetbrains.jps.incremental.scala.remote.ServerException
// java.lang.StackOverflowError
implicitly[NNn =:= c]

至此,完全证明了Scalameta programming的能力是Turing completeness

下一步就是在这个系统里面构件布尔、数字等基本的结构了。




X