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 }