接着上次的内容,既然已经证明了scalatype level programming的能力是图灵完备的,为了能使用这种能力,自然需要Bool和自然数。

Boolean

其实关于实现形式,在之前的lambda验算里面就有。

lambda

lambda

仿照这个形式,

1
2
3
4
5
6
7
8
9
10
11
12
13
sealed trait Bool {
type IF[T <: Up, F <: Up, Up]
}
sealed trait True extends Bool {
// lambda x.lambda y.x
type IF[T <: Up, F <: Up, Up] = T
}
sealed trait False extends Bool {
// lambda x.lambda y.y
type IF[T <: Up, F <: Up, Up] = F
}

然后,实现&&||这种操作

1
2
3
4
5
object Bool {
type &&[A <: Bool, B <: Bool] = A# IF[B, False, Bool]
type ||[A <: Bool, B <: Bool] = A# IF[True, B, Bool]
type Not[A <: Bool] = A# IF[False, True, Bool]
}

最后,实现一个将Bool类型转为具体Boolean的值的函数。

1
2
3
4
5
6
7
8
class BoolRep[B <: Bool](val value: Boolean)
implicit val falseRep: BoolRep[False] =
new BoolRep[False](false)
implicit val trueRep: BoolRep[True] =
new BoolRep[True](true)
def toBoolean[B <: Bool](implicit b: BoolRep[B]) = b.value

可以试一下

1
2
3
4
5
toBoolean[True && False || Not[False]]
// res: Boolean = true
type Num = True# IF[Int, Double, Bool]
val i: Num = 13.3 // raise Error

Peano number

Haskell里面本来就有相关的实现,可以看这里

先定义数字和零

1
2
3
4
5
6
7
8
9
10
11
12
sealed trait Nat {
type Match[NoZero[N <: Nat] <: Up, IfZero <: Up, Up] <: Up
type Compare[N <: Nat] <: Comparison
}
sealed trait _0 extends Nat {
type Match[NoZero[_ <: Nat] <: Up, IfZero <: Up, Up] = IfZero
type ConstLT[_] = LT
type Compare[N <: Nat] = N# Match[ConstLT, EQ, Comparison]
}

然后定义后继,从而得到自然数

1
2
3
4
5
6
7
8
9
10
sealed trait Succ[N <: Nat] extends Nat {
type Match[NoZero[_ <: Nat] <: Up, IfZero <: Up, Up] = NoZero[N]
type Compare[O <: Nat] = O# Match[N# Compare, GT, Comparison]
}
type _1 = Succ[_0]
type _2 = Succ[_1]
type _3 = Succ[_2]
type _4 = Succ[_3]

然后先定义一个辅助函数,用来判断是不是零,这里就要用到上面的Bool了,

1
2
3
4
5
6
type ConstFalse[A] = False
type Is0[A <: Nat] = A# Match[ConstFalse, True, Bool]
implicitly[Is0[_1] =:= False]
implicitly[Is0[_2] =:= True]

有了这些操作之后,我们想要把自然数的操作都引入到这个系统里来。

先看看和Bool紧密相关的comparsion

先定义比较之后的结果

1
2
3
4
5
6
7
8
9
sealed trait Comparison {
type Match[IfLT <: Up, IfEQ <: Up, IfGT <: Up, Up] <: Up
type gt = Match[False, False, True, Bool]
type ge = Match[False, True, True, Bool]
type eq = Match[False, True, False, Bool]
type le = Match[True, True, False, Bool]
type lt = Match[True, False, False, Bool]
}

然后定义比较的操作

1
2
3
4
5
6
7
8
9
sealed trait GT extends Comparison {
type Match[IfLT <: Up, IfEQ <: Up, IfGT <: Up, Up] = IfGT
}
sealed trait LT extends Comparison {
type Match[IfLT <: Up, IfEQ <: Up, IfGT <: Up, Up] = IfLT
}
sealed trait EQ extends Comparison {
type Match[IfLT <: Up, IfEQ <: Up, IfGT <: Up, Up] = IfEQ
}

最后,定义实际的操作。

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
sealed trait Nat {
type Match[NoZero[N <: Nat] <: Up, IfZero <: Up, Up] <: Up
type Compare[N <: Nat] <: Comparison
}
sealed trait _0 extends Nat {
type Match[NoZero[_ <: Nat] <: Up, IfZero <: Up, Up] = IfZero
type ConstLT[_] = LT
type Compare[N <: Nat] = N# Match[ConstLT, EQ, Comparison]
}
sealed trait Succ[N <: Nat] extends Nat {
type Match[NoZero[_ <: Nat] <: Up, IfZero <: Up, Up] = NoZero[N]
type Compare[O <: Nat] = O# Match[N# Compare, GT, Comparison]
}

这里的O和N实际是相互进行递归。每一次MatchCompare的调用,其实就是把NO都减了一次1,最后,如果N边变成0,就是_0调用CompareN调用Match。反之类似。

接下来,就改构造代数的运算。




X