-
Notifications
You must be signed in to change notification settings - Fork 9
/
TypeEq.java
500 lines (425 loc) · 16.7 KB
/
TypeEq.java
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
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
382
383
384
385
386
387
388
389
390
391
392
393
394
395
396
397
398
399
400
401
402
403
404
405
406
407
408
409
410
411
412
413
414
415
416
417
418
419
420
421
422
423
424
425
426
427
428
429
430
431
432
433
434
435
436
437
438
439
440
441
442
443
444
445
446
447
448
449
450
451
452
453
454
455
456
457
458
459
460
461
462
463
464
465
466
467
468
469
470
471
472
473
474
475
476
477
478
479
480
481
482
483
484
485
486
487
488
489
490
491
492
493
494
495
496
497
498
499
500
package org.derive4j.hkt;
/**
* Provide witnesses of equality between two types (propositional equality) using the Leibnizian equality definition.
* TypeEq instances do not have any effect on values: they only expose a sometimes hidden fact:
* that two types are the same and can be safely substituted with one another in any context (ie. type constructors).
*
* TypeEq instance are safe alternative to type casting and can be used to implements generalized algebraic data types.
*
* @param <A> a type {@link A}.
* @param <B> a type {@link B} which is guaranteed to be same as {@link A}.
* @see <a href="http://portal.acm.org/citation.cfm?id=583852.581494">Typing Dynamic Typing</a>
* @see <a href="http://typelevel.org/blog/2014/09/20/higher_leibniz.html">Higher TypeEq</a>
* @see <a href="https://github.com/ekmett/eq">Leibnizian type equality in Haskell</a>
*/
public abstract class TypeEq<A, B> implements __2<TypeEq.µ, A, B> {
/** Serve as type constructor witness of TypeEq. */
public enum µ {}
private TypeEq() {
}
/**
* Equality is reflexive: a type is equal to itself.
*
* @param <A> any type.
* @return a TypeEq representing the reflexive equality.
*/
public static <A> TypeEq<A, A> refl() {
// The only possible implementation, the identity:
return new TypeEq<A, A>() {
@Override public <f> __<f, A> subst(final __<f, A> fa) {
return fa;
}
};
}
/**
* Recover the concrete type of a higher kinded TypeEq value.
* The cast safety is guaranteed by the hkt type checker.
*
* @param hkTypeEq the higher kinded TypeEq.
* @param <A> a type {@link A}.
* @param <B> a type {@link B} which is guaranteed to be same as {@link A}.
* @return the same TypeEq, casted to the corresponding concrete type.
*/
public static <A, B> TypeEq<A, B> ofHkt(__<__<TypeEq.µ, A>, B> hkTypeEq) {
return (TypeEq<A, B>) hkTypeEq;
}
/**
* Reify the higher kinded type equality:<pre>
* {@code __<__<µ, A>, B} =:= {@code TypeEq<A, B}
* </pre>
* that is guaranteed by the hkt type checker.
*
* @param <A> a type {@link A}.
* @param <B> a type {@link B} which is guaranteed to be same as {@link A}.
* @return a TypeEq instance witness of the type equality.
*/
@SuppressWarnings("unchecked")
public static <A, B> TypeEq<__<__<TypeEq.µ, A>, B>, TypeEq<A, B>> hkt() {
return (TypeEq) refl();
}
/**
* Safe cast to __2. (guaranteed by the hkt type checker).
*/
public static <f, A, B> __2<f, A, B> as__2(__<__<f, A>, B> fab) {
return (__2<f, A, B>) fab;
}
/**
* Reify the higher kinded type equality:<pre>
* {@code __2<f, A, B> =:= __<__<f, A>, B>}</pre>
* that is guaranteed by the hkt type checker.
*
* @param <A> before last type variable.
* @param <B> last type variable.
* @return a TypeEq instance witness of the type equality.
*/
@SuppressWarnings("unchecked")
public static <f, A, B> TypeEq<__<__<f, A>, B>, __2<f, A, B>> __2() {
return (TypeEq) TypeEq.refl();
}
/**
* Safe cast to __3. (guaranteed by the hkt type checker).
*/
public static <f, A, B, C> __3<f, A, B, C> as__3(__<__<__<f, A>, B>, C> fabc) {
return (__3<f, A, B, C>) fabc;
}
/**
* Reify the higher kinded type equality:<pre>
* {@code __<__<__<f, A>, B>, C>} =:= {@code __3<f, A, B, C>}</pre>
* that is guaranteed by the hkt type checker.
*
* @param <A> the antepenultimate type variable
* @param <B> before last type variable.
* @param <C> last type variable.
* @return a TypeEq instance witness of the type equality.
*/
@SuppressWarnings("unchecked")
public static <f, A, B, C> TypeEq<__<__<__<f, A>, B>, C>, __3<f, A, B, C>> __3() {
return (TypeEq) TypeEq.refl();
}
/**
* Safe cast to __4. (guaranteed by the hkt type checker).
*/
public static <f, A, B, C, D> __4<f, A, B, C, D> as__4(__<__<__<__<f, A>, B>, C>, D> fabcd) {
return (__4<f, A, B, C, D>) fabcd;
}
/**
* Reify the higher kinded type equality:<pre>
* {@code __<__<__<__<f, A>, B>, C>, D>} =:= {@code __4<f, A, B, C, D>}</pre>
* that is guaranteed by the hkt type checker.
*
* @return a TypeEq instance witness of the type equality.
*/
@SuppressWarnings("unchecked")
public static <f, A, B, C, D> TypeEq<__<__<__<__<f, A>, B>, C>, D>, __4<f, A, B, C, D>> __4() {
return (TypeEq) TypeEq.refl();
}
/**
* Safe cast to __5. (guaranteed by the hkt type checker).
*/
public static <f, A, B, C, D, E> __5<f, A, B, C, D, E> as__5(__<__<__<__<__<f, A>, B>, C>, D>, E> fabcde) {
return (__5<f, A, B, C, D, E>) fabcde;
}
/**
* Reify the higher kinded type equality:<pre>
* {@code __<__<__<__<__<f, A>, B>, C>, D>, E>} =:= {@code __5<f, A, B, C, D, E>}</pre>
* that is guaranteed by the hkt type checker.
*
* @return a TypeEq instance witness of the type equality.
*/
@SuppressWarnings("unchecked")
public static <f, A, B, C, D, E> TypeEq<__<__<__<__<__<f, A>, B>, C>, D>, E>, __5<f, A, B, C, D, E>> __5() {
return (TypeEq) TypeEq.refl();
}
/**
* Safe cast to __6. (guaranteed by the hkt type checker).
*/
public static <f, A, B, C, D, E, F> __6<f, A, B, C, D, E, F> as__6(__<__<__<__<__<__<f, A>, B>, C>, D>, E>, F> fabcdef) {
return (__6<f, A, B, C, D, E, F>) fabcdef;
}
/**
* Reify the higher kinded type equality:<pre>
* {@code __<__<__<__<__<__<f, A>, B>, C>, D>, E>, F>} =:= {@code __6<f, A, B, C, D, E, F>}</pre>
* that is guaranteed by the hkt type checker.
*
* @return a TypeEq instance witness of the type equality.
*/
@SuppressWarnings("unchecked")
public static <f, A, B, C, D, E, F> TypeEq<__<__<__<__<__<__<f, A>, B>, C>, D>, E>, F>, __6<f, A, B, C, D, E, F>> __6() {
return (TypeEq) TypeEq.refl();
}
/**
* Safe cast to __7. (guaranteed by the hkt type checker).
*/
public static <f, A, B, C, D, E, F, G> __7<f, A, B, C, D, E, F, G> as__7(__<__<__<__<__<__<__<f, A>, B>, C>, D>, E>, F>, G>
fabcdefg) {
return (__7<f, A, B, C, D, E, F, G>) fabcdefg;
}
/**
* Reify the higher kinded type equality:<pre>
* {@code __<__<__<__<__<__<__<f, A>, B>, C>, D>, E>, F>, G>} =:= {@code __7<f, A, B, C, D, E, F, G>}</pre>
* that is guaranteed by the hkt type checker.
*
* @return a TypeEq instance witness of the type equality.
*/
@SuppressWarnings("unchecked")
public static <f, A, B, C, D, E, F, G> TypeEq<__<__<__<__<__<__<__<f, A>, B>, C>, D>, E>, F>, G>, __7<f, A, B, C, D, E, F, G>> __7() {
return (TypeEq) TypeEq.refl();
}
/**
* Safe cast to __8. (guaranteed by the hkt type checker).
*/
public static <f, A, B, C, D, E, F, G, H> __8<f, A, B, C, D, E, F, G, H> as__8(__<__<__<__<__<__<__<__<f, A>, B>, C>, D>, E>, F>, G>, H> fabcdefgh) {
return (__8<f, A, B, C, D, E, F, G, H>) fabcdefgh;
}
/**
* Reify the higher kinded type equality:<pre>
* {@code __<__<__<__<__<__<__<__<f, A>, B>, C>, D>, E>, F>, G>, H>} =:= {@code __8<f, A, B, C, D, E, F, G, H>}</pre>
* that is guaranteed by the hkt type checker.
*
* @return a TypeEq instance witness of the type equality.
*/
@SuppressWarnings("unchecked")
public static <f, A, B, C, D, E, F, G, H> TypeEq<__<__<__<__<__<__<__<__<f, A>, B>, C>, D>, E>, F>, G>, H>, __8<f, A, B, C, D, E, F, G, H>> __8() {
return (TypeEq) TypeEq.refl();
}
/**
* Safe cast to __9. (guaranteed by the hkt type checker).
*/
public static <f, A, B, C, D, E, F, G, H, I> __9<f, A, B, C, D, E, F, G, H, I> as__9(__<__<__<__<__<__<__<__<__<f, A>, B>, C>, D>, E>, F>, G>, H>, I> fabcdefghi) {
return (__9<f, A, B, C, D, E, F, G, H, I>) fabcdefghi;
}
/**
* Reify the higher kinded type equality:<pre>
* {@code __<__<__<__<__<__<__<__<__<f, A>, B>, C>, D>, E>, F>, G>, H>, I>} =:= {@code __9<f, A, B, C, D, E, F, G, H, I>}</pre>
* that is guaranteed by the hkt type checker.
*
* @return a TypeEq instance witness of the type equality.
*/
@SuppressWarnings("unchecked")
public static <f, A, B, C, D, E, F, G, H, I> TypeEq<__<__<__<__<__<__<__<__<__<f, A>, B>, C>, D>, E>, F>, G>, H>, I>, __9<f, A, B, C, D, E, F, G, H, I>> __9() {
return (TypeEq) TypeEq.refl();
}
/**
* Leibnizian equality states that two things are equal if you can substitute one for the other in all contexts.
*
* @param fa a term whose type last parameter is {@link A}.
* @param <f> type constructor witness of {@code fa} type.
* @return the input value with {@link A} substituted by {@link B} in its type.
*/
public abstract <f> __<f, B> subst(__<f, A> fa);
/**
* If two things are equal you can convert one to the other (safe cast).
*
* @param a a value of type {@link A} that will be coerced into type {@link B}.
* @return the same value, after type coercion.
*/
public final B coerce(A a) {
return Identity.ofHkt(subst(new Identity<>(a))).runIdentity;
}
/**
* Equality is transitive.
*
* @param that another TypeEq to compose with.
* @param <C> left operand of the transitive type equality.
* @return the composition of the TypeEq instances.
*/
public final <C> TypeEq<C, B> compose(TypeEq<C, A> that) {
return new TypeEq<C, B>() {
@Override public <f> __<f, B> subst(__<f, C> fa) {
return TypeEq.this.subst(that.subst(fa));
}
};
}
/**
* Equality is transitive.
*
* @param that another TypeEq to be composed with.
* @param <C> right operand of the transitive type equality.
* @return the composition of the TypeEq instances.
*/
public final <C> TypeEq<A, C> andThen(TypeEq<B, C> that) {
return that.compose(this);
}
/**
* Equality is symmetric.
*
* @return the type equality seen from the other side.
*/
public final TypeEq<B, A> symm() {
return Symm.ofHkt(subst(new Symm<>(refl()))).typeEq;
}
/**
* The type equality can be lifted into any type constructor.
*
* @param <f> a type constructor witness.
* @return the type equality in the context of the specified type constructor.
*/
public final <f> TypeEq<__<f, A>, __<f, B>> lift() {
return Lift.ofHkt(subst(new Lift<>(TypeEq.<__<f, A>>refl()))).unlift;
}
/**
* The type equality can be lifted into any type constructor, at any position.
*
* @param <f> a type constructor witness.
* @param <C> the last type variable (not substituted).
* @return the type equality in the context of the specified type constructor.
*/
public final <f, C> TypeEq<__<__<f, A>, C>, __<__<f, B>, C>> lift2() {
return Lift2.ofHkt(subst(new Lift2<>(TypeEq.<__<__<f, A>, C>>refl()))).unlift2;
}
/**
* Type equalities can be lifted into any type constructor, at any positions.
*
* @param cd a type equality witness for last type variable of any type constructor.
* @param <C> the last type variable before substitution.
* @param <D> the last type variable after substitution.
* @return a factory to lift the TypeEq instances into any type constructor.
*/
public final <C, D> Lift2TypeEq<A, C, B, D> lift2(TypeEq<C, D> cd) {
return new Lift2TypeEq<A, C, B, D>(this, cd);
}
/**
* The type equality can be lifted into any type constructor, at any position.
*
* @param <f> a type constructor witness.
* @param <C> the before last type variable (not substituted).
* @param <D> the last type variable (not substituted).
* @return the type equality in the context of the specified type constructor.
*/
public final <f, C, D> TypeEq<__<__<__<f, A>, C>, D>, __<__<__<f, B>, C>, D>> lift3() {
return Lift3.ofHkt(subst(new Lift3<>(TypeEq.<__<__<__<f, A>, C>, D>>refl()))).unlift3;
}
/**
* Type equalities can be lifted into any type constructor, at any positions.
*
* @param cd a type equality witness for before last type variable of any type constructor.
* @param ef a type equality witness for last type variable of any type constructor.
* @param <C> the before last type variable before substitution.
* @param <D> the before last type variable after substitution.
* @param <E> the last type variable before substitution.
* @param <F> the last type variable after substitution.
* @return a factory to lift the TypeEq instances into any type constructor.
*/
public final <C, D, E, F> Lift3TypeEq<A, C, E, B, D, F> lift3(TypeEq<C, D> cd, TypeEq<E, F> ef) {
return new Lift3TypeEq<A, C, E, B, D, F>(this, cd, ef);
}
/**
* Type inference helper class:
* allow to lift two TypeEq instances into any type constructor.
*
* @param <A> the before last type variable before substitution.
* @param <C> the last type variable before substitution.
* @param <B> the before last type variable after substitution.
* @param <D> the last type variable after substitution.
*/
public static final class Lift2TypeEq<A, C, B, D> {
private final TypeEq<A, B> ab;
private final TypeEq<C, D> cd;
Lift2TypeEq(TypeEq<A, B> ab, TypeEq<C, D> cd) {
this.ab = ab;
this.cd = cd;
}
/**
* Lift two TypeEq instances into a type constructor.
*
* @param <f> a type constructor witness.
* @return the type equalities in the context of the type constructor.
*/
public <f> TypeEq<__<__<f, A>, C>, __<__<f, B>, D>> lift() {
TypeEq<__<__<f, A>, C>, __<__<f, B>, C>> abLift = ab.lift2();
TypeEq<__<__<f, B>, C>, __<__<f, B>, D>> cdLift = cd.lift();
return new TypeEq<__<__<f, A>, C>, __<__<f, B>, D>>() {
@Override public <f2> __<f2, __<__<f, B>, D>> subst(__<f2, __<__<f, A>, C>> fa) {
return cdLift.subst(abLift.subst(fa));
}
};
}
}
/**
* Type inference helper class:
* allow to lift three TypeEq instances into any type constructor.
*
* @param <A> the antepenultimate type variable before substitution.
* @param <C> the before last type variable before substitution.
* @param <E> the last type variable before substitution.
* @param <B> the antepenultimate type variable after substitution.
* @param <D> the before last type variable after substitution.
* @param <F> the last type variable after substitution.
*/
public static final class Lift3TypeEq<A, C, E, B, D, F> {
private final TypeEq<A, B> ab;
private final TypeEq<C, D> cd;
private final TypeEq<E, F> ef;
Lift3TypeEq(TypeEq<A, B> ab, TypeEq<C, D> cd, TypeEq<E, F> ef) {
this.ab = ab;
this.cd = cd;
this.ef = ef;
}
/**
* Lift three TypeEq instances into a type constructor.
*
* @param <f> a type constructor witness.
* @return the type equalities in the context of the type constructor.
*/
public <f> TypeEq<__<__<__<f, A>, C>, E>, __<__<__<f, B>, D>, F>> lift() {
TypeEq<__<__<__<f, A>, C>, E>, __<__<__<f, B>, C>, E>> abLift = ab.lift3();
TypeEq<__<__<__<f, B>, C>, E>, __<__<__<f, B>, D>, E>> cdLift = cd.lift2();
TypeEq<__<__<__<f, B>, D>, E>, __<__<__<f, B>, D>, F>> efLift = ef.lift();
return new TypeEq<__<__<__<f, A>, C>, E>, __<__<__<f, B>, D>, F>>() {
@Override public <f2> __<f2, __<__<__<f, B>, D>, F>> subst(__<f2, __<__<__<f, A>, C>, E>> fa) {
return efLift.subst(cdLift.subst(abLift.subst(fa)));
}
};
}
}
private static class Identity<A> implements __<Identity.µ, A> {
final A runIdentity;
Identity(A runIdentity) {
this.runIdentity = runIdentity;
}
static <A> Identity<A> ofHkt(__<µ, A> hkId) {
return (Identity<A>) hkId;
}
enum µ {}
}
private static class Symm<A, B> implements __2<Symm.µ, A, B> {
final TypeEq<B, A> typeEq;
Symm(TypeEq<B, A> typeEq) {
this.typeEq = typeEq;
}
static <A, B> Symm<A, B> ofHkt(__<__<µ, A>, B> hkSymm) {
return (Symm<A, B>) hkSymm;
}
enum µ {}
}
private static class Lift<f, A, B> implements __3<Lift.µ, f, A, B> {
final TypeEq<__<f, A>, __<f, B>> unlift;
Lift(TypeEq<__<f, A>, __<f, B>> unlift) {
this.unlift = unlift;
}
static <f, A, B> Lift<f, A, B> ofHkt(__<__<__<µ, f>, A>, B> hkLift) {
return (Lift<f, A, B>) hkLift;
}
enum µ {}
}
private static class Lift2<f, C, A, B> implements __4<Lift2.µ, f, C, A, B> {
final TypeEq<__<__<f, A>, C>, __<__<f, B>, C>> unlift2;
Lift2(TypeEq<__<__<f, A>, C>, __<__<f, B>, C>> unlift2) {
this.unlift2 = unlift2;
}
static <f, C, A, B> Lift2<f, C, A, B> ofHkt(__<__<__<__<µ, f>, C>, A>, B> hkLift2) {
return (Lift2<f, C, A, B>) hkLift2;
}
enum µ {}
}
private static class Lift3<f, C, D, A, B> implements __5<Lift3.µ, f, C, D, A, B> {
final TypeEq<__<__<__<f, A>, C>, D>, __<__<__<f, B>, C>, D>> unlift3;
Lift3(TypeEq<__<__<__<f, A>, C>, D>, __<__<__<f, B>, C>, D>> unlift3) {
this.unlift3 = unlift3;
}
static <f, C, D, A, B> Lift3<f, C, D, A, B> ofHkt(__<__<__<__<__<µ, f>, C>, D>, A>, B> hkLift3) {
return (Lift3<f, C, D, A, B>) hkLift3;
}
enum µ {}
}
}