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