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
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
|
trait Term {
type ap[x <: Term] <: Term
type eval <: Term
}
// The 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] // error: not a legal path
type eval = x#ap[z]#ap[y#ap[z]]#eval // error: not a legal path // error: not a legal path
}
// 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] // error: not a legal path
type eval = x#eval // error: not a legal path
}
// 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] // error: not a legal path
type eval = x#eval // error: not a legal path
}
// Constants
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
}
case class Equals[A >: B <:B , B]()
object Test {
type T1 = Equals[Int, Int] // compiles fine
type T2 = Equals[String, Int] // error: Type argument String does not conform to upper bound Int
type T3 = Equals[I#ap[c]#eval, c]
type T3a = Equals[I#ap[c]#eval, d] // error: Type argument I1[c]#eval does not conform to upper bound d
// Ic -> c
type T4 = Equals[I#ap[c]#eval, c]
// Kcd -> c
type T5 = Equals[K#ap[c]#ap[d]#eval, c]
// KKcde -> d
type T6 = Equals[K#ap[K]#ap[c]#ap[d]#ap[e]#eval, d] // error: Type argument K2[K1[_ <: Term] @UnsafeNonvariant#x, e]#eval does not conform to upper bound d
// SIIIc -> Ic
type T7 = Equals[S#ap[I]#ap[I]#ap[I]#ap[c]#eval, c] // error: not a legal path // error: Type argument I1[_ <: Term]#eval#ap[_]#eval does not conform to upper bound c
// SKKc -> Ic
type T8 = Equals[S#ap[K]#ap[K]#ap[c]#eval, c]
// SIIKc -> KKc
type T9 = Equals[S#ap[I]#ap[I]#ap[K]#ap[c]#eval, K#ap[K]#ap[c]#eval] // error: Type argument K2[K1[_ <: Term] @UnsafeNonvariant#x, _ <: Term]#eval does not conform to upper bound K2[K, c]#eval
// SIKKc -> K(KK)c
type T10 = Equals[S#ap[I]#ap[K]#ap[K]#ap[c]#eval, K#ap[K#ap[K]]#ap[c]#eval] // error: Type argument K2[K1[_ <: Term] @UnsafeNonvariant#x, _ <: Term]#eval does not conform to upper bound K2[K1[K], c]#eval
// SIKIc -> KIc
type T11 = Equals[S#ap[I]#ap[K]#ap[I]#ap[c]#eval, K#ap[I]#ap[c]#eval] // error: not a legal path // error: Type argument I1[_ <: Term]#eval#ap[_]#eval does not conform to upper bound K2[I, c]#eval
// SKIc -> Ic
type T12 = Equals[S#ap[K]#ap[I]#ap[c]#eval, c]
// R = S(K(SI))K (reverse)
type R = S#ap[K#ap[S#ap[I]]]#ap[K]
type T13 = Equals[R#ap[c]#ap[d]#eval, d#ap[c]#eval] // error: Type argument S3[I, S2[I, _ <: Term] @UnsafeNonvariant#y, _ <: Term]#eval does not conform to upper bound d#eval
type b[a <: Term] = S#ap[K#ap[a]]#ap[S#ap[I]#ap[I]]
trait A0 extends Term {
type ap[x <: Term] = c
type eval = A0
}
trait A1 extends Term {
type ap[x <: Term] = x#ap[A0]#eval // error: not a legal path
type eval = A1
}
trait A2 extends Term {
type ap[x <: Term] = x#ap[A1]#eval // error: not a legal path
type eval = A2
}
type NN1 = b[R]#ap[b[R]]#ap[A0]
type T13a = Equals[NN1#eval, c] // error: Type argument Test.NN1#eval does not conform to upper bound c
// Double iteration
type NN2 = b[R]#ap[b[R]]#ap[A1]
type T14 = Equals[NN2#eval, c] // error: Type argument Test.NN2#eval does not conform to upper bound c
// Triple iteration
type NN3 = b[R]#ap[b[R]]#ap[A2]
type T15 = Equals[NN3#eval, c] // error: Type argument Test.NN3#eval does not conform to upper bound c
trait An extends Term {
type ap[x <: Term] = x#ap[An]#eval // error: not a legal path
type eval = An
}
// Infinite iteration: Smashes scalac's stack
type NNn = b[R]#ap[b[R]]#ap[An]
// type X = Equals[NNn#eval, c]
}
|
