001 package fj.data.hlist; 002 003 import fj.F; 004 import fj.pre.Show; 005 006 /** 007 * A basic prelude of values lifted into the type system. 008 */ 009 @SuppressWarnings({"ALL"}) 010 public final class HPre { 011 private HPre() { 012 throw new UnsupportedOperationException(); 013 } 014 015 /** 016 * A type-level Boolean 017 */ 018 public static class HBool { 019 private HBool() { 020 } 021 } 022 023 /** 024 * Boolean true 025 */ 026 public static class HTrue extends HBool { 027 private HTrue() { 028 } 029 } 030 031 /** 032 * Boolean false 033 */ 034 public static class HFalse extends HBool { 035 private HFalse() { 036 } 037 } 038 039 private static final HTrue hTrue = new HTrue(); 040 private static final HFalse hFalse = new HFalse(); 041 042 /** 043 * Returns a boolean value whose type represents truth. 044 * 045 * @return a boolean value whose type represents truth. 046 */ 047 public static HTrue hTrue() { 048 return hTrue; 049 } 050 051 /** 052 * Returns a boolean value whose type represents falsehood. 053 * 054 * @return a boolean value whose type represents falsehood. 055 */ 056 public static HFalse hFalse() { 057 return hFalse; 058 } 059 060 /** 061 * Type-level boolean conjunction. A value of this type represents evidence that AB -> C 062 * 063 * @param <A> A boolean 064 * @param <B> A boolean 065 * @param <C> The logical implication of A and B 066 */ 067 public static final class HAnd<A extends HBool, B extends HBool, C extends HBool> { 068 private final C v; 069 070 private HAnd(final C v) { 071 this.v = v; 072 } 073 074 public C v() { 075 return v; 076 } 077 078 public static HAnd<HFalse, HFalse, HFalse> hAnd(final HFalse a, final HFalse b) { 079 return new HAnd<HFalse, HFalse, HFalse>(hFalse()); 080 } 081 082 public static HAnd<HTrue, HFalse, HFalse> hAnd(final HTrue a, final HFalse b) { 083 return new HAnd<HTrue, HFalse, HFalse>(hFalse()); 084 } 085 086 public static HAnd<HFalse, HTrue, HFalse> hAnd(final HFalse a, final HTrue b) { 087 return new HAnd<HFalse, HTrue, HFalse>(hFalse()); 088 } 089 090 public static HAnd<HTrue, HTrue, HTrue> hAnd(final HTrue a, final HTrue b) { 091 return new HAnd<HTrue, HTrue, HTrue>(hTrue()); 092 } 093 } 094 095 /** 096 * Type-level boolean disjunction. A value of this type represents evidence that A+B -> C 097 * 098 * @param <A> A boolean 099 * @param <B> A boolean 100 * @param <C> The logical implication of A or B 101 */ 102 public static final class HOr<A extends HBool, B extends HBool, C extends HBool> { 103 private final C v; 104 105 private HOr(final C v) { 106 this.v = v; 107 } 108 109 public C v() { 110 return v; 111 } 112 113 public static HOr<HFalse, HFalse, HFalse> hOr(final HFalse a, final HFalse b) { 114 return new HOr<HFalse, HFalse, HFalse>(hFalse()); 115 } 116 117 public static HOr<HTrue, HFalse, HTrue> hOr(final HTrue a, final HFalse b) { 118 return new HOr<HTrue, HFalse, HTrue>(hTrue()); 119 } 120 121 public static HOr<HFalse, HTrue, HTrue> hOr(final HFalse a, final HTrue b) { 122 return new HOr<HFalse, HTrue, HTrue>(hTrue()); 123 } 124 125 public static HOr<HTrue, HTrue, HTrue> hOr(final HTrue a, final HTrue b) { 126 return new HOr<HTrue, HTrue, HTrue>(hTrue()); 127 } 128 } 129 130 /** 131 * A type-level conditional. The type of the last parameter is implied by the first three. 132 * 133 * @param <T> A boolean 134 * @param <X> The type of Z if T is true. 135 * @param <Y> The type of Z if T is false. 136 * @param <Z> A type that is either X or Z, depending on T. 137 */ 138 public static final class HCond<T, X, Y, Z> { 139 private HCond(final Z z) { 140 this.z = z; 141 } 142 143 private final Z z; 144 145 public Z v() { 146 return z; 147 } 148 149 public static <X, Y> HCond<HFalse, X, Y, Y> hCond(final HFalse t, final X x, final Y y) { 150 return new HCond<HFalse, X, Y, Y>(y); 151 } 152 153 public static <X, Y> HCond<HTrue, X, Y, X> hCond(final HTrue t, final X x, final Y y) { 154 return new HCond<HTrue, X, Y, X>(x); 155 } 156 } 157 158 /** 159 * Type-level natural numbers. 160 */ 161 public abstract static class HNat<A extends HNat<A>> { 162 public abstract Show<A> show(); 163 164 public abstract Integer toInteger(); 165 166 public static HZero hZero() { 167 return new HZero(); 168 } 169 170 public static <N extends HNat<N>> HSucc<N> hSucc(final N n) { 171 return new HSucc<N>(n); 172 } 173 174 public static <N extends HNat<N>> N hPred(final HSucc<N> n) { 175 return n.pred; 176 } 177 } 178 179 /** 180 * Type-level zero 181 */ 182 public static final class HZero extends HNat<HZero> { 183 private HZero() { 184 } 185 186 public Show<HZero> show() { 187 return Show.showS(new F<HZero, String>() { 188 public String f(final HZero hZero) { 189 return "HZero"; 190 } 191 }); 192 } 193 194 public Integer toInteger() { 195 return 0; 196 } 197 } 198 199 /** 200 * A natural number N + 1 201 * 202 * @param <N> The predecessor of this number. 203 */ 204 public static final class HSucc<N extends HNat<N>> extends HNat<HSucc<N>> { 205 private HSucc(final N n) { 206 pred = n; 207 } 208 209 private final N pred; 210 211 public Show<HSucc<N>> show() { 212 return Show.showS(new F<HSucc<N>, String>() { 213 public String f(final HSucc<N> s) { 214 return "HSucc (" + s.show().showS(s) + ')'; 215 } 216 }); 217 } 218 219 public Integer toInteger() { 220 return 1 + pred.toInteger(); 221 } 222 } 223 224 /** 225 * Type-level equality. Represents evidence for X and Y being equal, or counterevidence against. 226 */ 227 public static final class HEq<X, Y, B extends HBool> { 228 private final B v; 229 230 private HEq(final B v) { 231 this.v = v; 232 } 233 234 public B v() { 235 return v; 236 } 237 238 /** 239 * Zero is equal to itself. 240 * 241 * @param a Zero 242 * @param b Zero 243 * @return Equality for Zero 244 */ 245 public static HEq<HZero, HZero, HTrue> eq(final HZero a, final HZero b) { 246 return new HEq<HZero, HZero, HTrue>(hTrue()); 247 } 248 249 /** 250 * Zero is not equal to anything other than zero. 251 */ 252 public static <N extends HNat<N>> HEq<HZero, HSucc<N>, HFalse> eq(final HZero a, final HSucc<N> b) { 253 return new HEq<HZero, HSucc<N>, HFalse>(hFalse()); 254 } 255 256 /** 257 * Zero is not equal to anything other than zero. 258 */ 259 public static <N extends HNat<N>> HEq<HSucc<N>, HZero, HFalse> eq(final HSucc<N> a, final HZero b) { 260 return new HEq<HSucc<N>, HZero, HFalse>(hFalse()); 261 } 262 263 /** 264 * A number is equal to another if their predecessors are equal. 265 */ 266 public static <N extends HNat<N>, NN extends HNat<NN>, B extends HBool, E extends HEq<N, NN, B>> 267 HEq<HSucc<N>, HSucc<NN>, B> eq(final HSucc<N> a, final HSucc<NN> b, final E e) { 268 return new HEq<HSucc<N>, HSucc<NN>, B>(e.v); 269 } 270 271 } 272 273 /** 274 * Type-level integer arithmetic 275 */ 276 public static final class HAdd<A extends HNat<A>, B extends HNat<B>, C extends HNat<C>> { 277 private final C sum; 278 279 private HAdd(final C sum) { 280 this.sum = sum; 281 } 282 283 /** 284 * The sum of zero and any other number is that number. 285 */ 286 public static <N extends HNat<N>> HAdd<HZero, HSucc<N>, HSucc<N>> add(final HZero a, final HSucc<N> b) { 287 return new HAdd<HZero, HSucc<N>, HSucc<N>>(b); 288 } 289 290 /** 291 * The sum of zero and any other number is that number. 292 */ 293 public static <N extends HNat<N>> HAdd<HSucc<N>, HZero, HSucc<N>> add(final HSucc<N> a, final HZero b) { 294 return new HAdd<HSucc<N>, HZero, HSucc<N>>(a); 295 } 296 297 /** 298 * The sum of numbers a and b is one greater than the sum of b and the predecessor of a. 299 */ 300 public static <N extends HNat<N>, M extends HNat<M>, R extends HNat<R>, H extends HAdd<N, HSucc<M>, R>> 301 HAdd<HSucc<N>, HSucc<M>, HSucc<R>> add(final HSucc<N> a, final HSucc<M> b, final H h) { 302 return new HAdd<HSucc<N>, HSucc<M>, HSucc<R>>(HNat.hSucc(h.sum)); 303 } 304 } 305 306 }