From bc0e79fbcaa154e9ad21998c495d771f59cad814 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Gr=C3=A9goire=20Neuville?= Date: Thu, 25 May 2017 22:40:57 +0200 Subject: [PATCH 1/2] Make TypeEq and its inner types interfaces --- src/main/java/org/derive4j/hkt/TypeEq.java | 467 +++++++++------------ 1 file changed, 199 insertions(+), 268 deletions(-) diff --git a/src/main/java/org/derive4j/hkt/TypeEq.java b/src/main/java/org/derive4j/hkt/TypeEq.java index f66275e..7649ac4 100644 --- a/src/main/java/org/derive4j/hkt/TypeEq.java +++ b/src/main/java/org/derive4j/hkt/TypeEq.java @@ -13,28 +13,149 @@ * @see Higher TypeEq * @see Leibnizian type equality in Haskell */ -public abstract class TypeEq implements __2 { +@SuppressWarnings("Convert2MethodRef") +public interface TypeEq extends __2 { + /** Type constructor witness of TypeEq. */ + enum µ {} - /** Serve as type constructor witness of TypeEq. */ - public enum µ {} + /** + * 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 type constructor witness of {@code fa} type. + * @return the input value with {@link A} substituted by {@link B} in its type. + */ + __ subst(__ 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. + */ + default B coerce(A a) { + return Id.narrow(subst((Id) () -> a)).__(); + } + + /** + * Equality is transitive. + * + * @param that another TypeEq to compose with. + * @param left operand of the transitive type equality. + * @return the composition of the TypeEq instances. + */ + default TypeEq compose(TypeEq that) { + return TypeEq.ofHkt(subst(that)); + } + + /** + * Equality is transitive. + * + * @param that another TypeEq to be composed with. + * @param right operand of the transitive type equality. + * @return the composition of the TypeEq instances. + */ + default TypeEq andThen(TypeEq that) { + return that.compose(this); + } + + /** + * Equality is symmetric. + * + * @return the type equality seen from the other side. + */ + default TypeEq symm() { + final Symm symm = () -> refl(); + + return Symm.narrow(subst(symm)).__(); + } + + /** + * The type equality can be lifted into any type constructor. + * + * @param a type constructor witness. + * @return the type equality in the context of the specified type constructor. + */ + default TypeEq<__, __> lift() { + final Lift _refl = () -> refl(); + + return Lift.narrow(subst(_refl)).__(); + } + + /** + * The type equality can be lifted into any type constructor, at any position. + * + * @param a type constructor witness. + * @param the last type variable (not substituted). + * @return the type equality in the context of the specified type constructor. + */ + default TypeEq<__<__, C>, __<__, C>> lift2() { + return lift2(refl()); + } + + /** + * 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 the last type variable before substitution. + * @param the last type variable after substitution. + * @return a factory to lift the TypeEq instances into any type constructor. + */ + default TypeEq<__<__, C>, __<__, D>> lift2(TypeEq cd) { + final Lift2_1 _refl = () -> refl(); - private TypeEq() { + final Lift2_1 lift2_1 = Lift2_1.narrow(subst(_refl)); + + final Lift2 lift2 = () -> lift2_1.__(); + + return Lift2.narrow(cd.subst(lift2)).__(); + } + + /** + * The type equality can be lifted into any type constructor, at any position. + * + * @param a type constructor witness. + * @param the before last type variable (not substituted). + * @param the last type variable (not substituted). + * @return the type equality in the context of the specified type constructor. + */ + default TypeEq<__<__<__, C>, D>, __<__<__, C>, D>> lift3() { + return lift3(refl(), refl()); + } + + /** + * 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 the before last type variable before substitution. + * @param the before last type variable after substitution. + * @param the last type variable before substitution. + * @param the last type variable after substitution. + * @return a factory to lift the TypeEq instances into any type constructor. + */ + default TypeEq<__<__<__, C>, E>, __<__<__, D>, F>> lift3(TypeEq cd + , TypeEq ef) { + final Lift3_1 _refl = () -> refl(); + + final Lift3_1 lift3_1 = Lift3_1.narrow(subst(_refl)); + + final Lift3_2 lift3_2 = () -> lift3_1.__(); + + final Lift3_2 lift3_2_1 = Lift3_2.narrow(cd.subst(lift3_2)); + + final Lift3 lift3 = () -> lift3_2_1.__(); + + return Lift3.narrow(ef.subst(lift3)).__(); } /** * Equality is reflexive: a type is equal to itself. * - * @param any type. + * @param any type. * @return a TypeEq representing the reflexive equality. */ - public static TypeEq refl() { - // The only possible implementation, the identity: - return new TypeEq() { - @Override public __ subst(final __ fa) { - return fa; - } - }; - } + static TypeEq refl() { return HktId::id; } /** * Recover the concrete type of a higher kinded TypeEq value. @@ -45,7 +166,7 @@ public static TypeEq refl() { * @param 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 TypeEq ofHkt(__<__, B> hkTypeEq) { + static TypeEq ofHkt(__<__, B> hkTypeEq) { return (TypeEq) hkTypeEq; } @@ -60,14 +181,14 @@ public static TypeEq ofHkt(__<__, B> hkTypeEq) { * @return a TypeEq instance witness of the type equality. */ @SuppressWarnings("unchecked") - public static TypeEq<__<__, B>, TypeEq> hkt() { - return (TypeEq) refl(); + static TypeEq<__<__, B>, TypeEq> hkt() { + return (TypeEq) TypeEq.refl(); } /** * Safe cast to __2. (guaranteed by the hkt type checker). */ - public static __2 as__2(__<__, B> fab) { + static __2 as__2(__<__, B> fab) { return (__2) fab; } @@ -148,7 +269,7 @@ public static TypeEq<__<__<__<__<__, B>, C>, D>, E>, __ /** * Safe cast to __6. (guaranteed by the hkt type checker). */ - public static __6 as__6(__<__<__<__<__<__, B>, C>, D>, E>, F> fabcdef) { + static __6 as__6(__<__<__<__<__<__, B>, C>, D>, E>, F> fabcdef) { return (__6) fabcdef; } @@ -160,15 +281,15 @@ public static __6 as__6(__<__<__<__<_ * @return a TypeEq instance witness of the type equality. */ @SuppressWarnings("unchecked") - public static TypeEq<__<__<__<__<__<__, B>, C>, D>, E>, F>, __6> __6() { + static TypeEq<__<__<__<__<__<__, B>, C>, D>, E>, F>, __6> __6() { return (TypeEq) TypeEq.refl(); } /** * Safe cast to __7. (guaranteed by the hkt type checker). */ - public static __7 as__7(__<__<__<__<__<__<__, B>, C>, D>, E>, F>, G> - fabcdefg) { + static __7 as__7(__<__<__<__<__<__<__, B>, C>, D>, E>, F>, G> + fabcdefg) { return (__7) fabcdefg; } @@ -180,7 +301,7 @@ public static __7 as__7(__<__<_ * @return a TypeEq instance witness of the type equality. */ @SuppressWarnings("unchecked") - public static TypeEq<__<__<__<__<__<__<__, B>, C>, D>, E>, F>, G>, __7> __7() { + static TypeEq<__<__<__<__<__<__<__, B>, C>, D>, E>, F>, G>, __7> __7() { return (TypeEq) TypeEq.refl(); } @@ -188,7 +309,7 @@ public static TypeEq<__<__<__<__<__<__<__, B>, C> /** * Safe cast to __8. (guaranteed by the hkt type checker). */ - public static __8 as__8(__<__<__<__<__<__<__<__, B>, C>, D>, E>, F>, G>, H> fabcdefgh) { + static __8 as__8(__<__<__<__<__<__<__<__, B>, C>, D>, E>, F>, G>, H> fabcdefgh) { return (__8) fabcdefgh; } @@ -200,7 +321,7 @@ public static __8 as__8(_ * @return a TypeEq instance witness of the type equality. */ @SuppressWarnings("unchecked") - public static TypeEq<__<__<__<__<__<__<__<__, B>, C>, D>, E>, F>, G>, H>, __8> __8() { + static TypeEq<__<__<__<__<__<__<__<__, B>, C>, D>, E>, F>, G>, H>, __8> __8() { return (TypeEq) TypeEq.refl(); } @@ -208,7 +329,7 @@ public static TypeEq<__<__<__<__<__<__<__<__, /** * Safe cast to __9. (guaranteed by the hkt type checker). */ - public static __9 as__9(__<__<__<__<__<__<__<__<__, B>, C>, D>, E>, F>, G>, H>, I> fabcdefghi) { + static __9 as__9(__<__<__<__<__<__<__<__<__, B>, C>, D>, E>, F>, G>, H>, I> fabcdefghi) { return (__9) fabcdefghi; } @@ -220,281 +341,91 @@ public static __9 a * @return a TypeEq instance witness of the type equality. */ @SuppressWarnings("unchecked") - public static TypeEq<__<__<__<__<__<__<__<__<__, B>, C>, D>, E>, F>, G>, H>, I>, __9> __9() { + static TypeEq<__<__<__<__<__<__<__<__<__, B>, C>, D>, E>, F>, G>, H>, I>, __9> __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 type constructor witness of {@code fa} type. - * @return the input value with {@link A} substituted by {@link B} in its type. - */ - public abstract __ subst(__ 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 left operand of the transitive type equality. - * @return the composition of the TypeEq instances. - */ - public final TypeEq compose(TypeEq that) { - return new TypeEq() { - @Override public __ subst(__ fa) { - return TypeEq.this.subst(that.subst(fa)); - } - }; - } - - /** - * Equality is transitive. - * - * @param that another TypeEq to be composed with. - * @param right operand of the transitive type equality. - * @return the composition of the TypeEq instances. - */ - public final TypeEq andThen(TypeEq that) { - return that.compose(this); - } - - /** - * Equality is symmetric. - * - * @return the type equality seen from the other side. - */ - public final TypeEq symm() { - return Symm.ofHkt(subst(new Symm<>(refl()))).typeEq; - } - - /** - * The type equality can be lifted into any type constructor. - * - * @param a type constructor witness. - * @return the type equality in the context of the specified type constructor. - */ - public final TypeEq<__, __> lift() { - return Lift.ofHkt(subst(new Lift<>(TypeEq.<__>refl()))).unlift; - } - - /** - * The type equality can be lifted into any type constructor, at any position. - * - * @param a type constructor witness. - * @param the last type variable (not substituted). - * @return the type equality in the context of the specified type constructor. - */ - public final TypeEq<__<__, C>, __<__, C>> lift2() { - return Lift2.ofHkt(subst(new Lift2<>(TypeEq.<__<__, 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 the last type variable before substitution. - * @param the last type variable after substitution. - * @return a factory to lift the TypeEq instances into any type constructor. - */ - public final Lift2TypeEq lift2(TypeEq cd) { - return new Lift2TypeEq(this, cd); - } - - /** - * The type equality can be lifted into any type constructor, at any position. - * - * @param a type constructor witness. - * @param the before last type variable (not substituted). - * @param the last type variable (not substituted). - * @return the type equality in the context of the specified type constructor. - */ - public final TypeEq<__<__<__, C>, D>, __<__<__, C>, D>> lift3() { - return Lift3.ofHkt(subst(new Lift3<>(TypeEq.<__<__<__, C>, D>>refl()))).unlift3; - } +// ################ Type inference helpers - /** - * 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 the before last type variable before substitution. - * @param the before last type variable after substitution. - * @param the last type variable before substitution. - * @param the last type variable after substitution. - * @return a factory to lift the TypeEq instances into any type constructor. - */ - public final Lift3TypeEq lift3(TypeEq cd, TypeEq ef) { - return new Lift3TypeEq(this, cd, ef); - } +interface HktId { + static __ id(__ ft) { return ft; } +} - /** - * Type inference helper class: - * allow to lift two TypeEq instances into any type constructor. - * - * @param the before last type variable before substitution. - * @param the last type variable before substitution. - * @param the before last type variable after substitution. - * @param the last type variable after substitution. - */ - public static final class Lift2TypeEq { - - private final TypeEq ab; +interface Id extends __ { + enum µ {} - private final TypeEq cd; + A __(); - Lift2TypeEq(TypeEq ab, TypeEq cd) { - this.ab = ab; - this.cd = cd; - } + static Id narrow(__ a) { return (Id) a; } +} - /** - * Lift two TypeEq instances into a type constructor. - * - * @param a type constructor witness. - * @return the type equalities in the context of the type constructor. - */ - public TypeEq<__<__, C>, __<__, D>> lift() { +interface Symm extends __2 { + enum µ {} - TypeEq<__<__, C>, __<__, C>> abLift = ab.lift2(); - TypeEq<__<__, C>, __<__, D>> cdLift = cd.lift(); + TypeEq __(); - return new TypeEq<__<__, C>, __<__, D>>() { - @Override public __, D>> subst(__, C>> fa) { - return cdLift.subst(abLift.subst(fa)); - } - }; - } + static Symm narrow(__<__, B> _lift) { + return (Symm) _lift; } +} - /** - * Type inference helper class: - * allow to lift three TypeEq instances into any type constructor. - * - * @param the antepenultimate type variable before substitution. - * @param the before last type variable before substitution. - * @param the last type variable before substitution. - * @param the antepenultimate type variable after substitution. - * @param the before last type variable after substitution. - * @param the last type variable after substitution. - */ - public static final class Lift3TypeEq { - - private final TypeEq ab; - - private final TypeEq cd; - - private final TypeEq ef; +interface Lift extends __3 { + enum µ {} - Lift3TypeEq(TypeEq ab, TypeEq cd, TypeEq ef) { - this.ab = ab; - this.cd = cd; - this.ef = ef; - } + TypeEq<__, __> __(); - /** - * Lift three TypeEq instances into a type constructor. - * - * @param a type constructor witness. - * @return the type equalities in the context of the type constructor. - */ - public TypeEq<__<__<__, C>, E>, __<__<__, D>, F>> lift() { - - TypeEq<__<__<__, C>, E>, __<__<__, C>, E>> abLift = ab.lift3(); - TypeEq<__<__<__, C>, E>, __<__<__, D>, E>> cdLift = cd.lift2(); - TypeEq<__<__<__, D>, E>, __<__<__, D>, F>> efLift = ef.lift(); - - return new TypeEq<__<__<__, C>, E>, __<__<__, D>, F>>() { - @Override public __, D>, F>> subst(__, C>, E>> fa) { - return efLift.subst(cdLift.subst(abLift.subst(fa))); - } - }; - } + static Lift narrow(__<__<__, A>, X> _lift) { + return (Lift) _lift; } +} - private static class Identity implements __ { - - final A runIdentity; - - Identity(A runIdentity) { - this.runIdentity = runIdentity; - } +interface Lift2_1 extends __4 { + enum µ {} - static Identity ofHkt(__<µ, A> hkId) { - return (Identity) hkId; - } + TypeEq<__<__, B>, __<__, B>> __(); - enum µ {} + static Lift2_1 narrow(__<__<__<__, A>, B>, X> lift1) { + return (Lift2_1) lift1; } +} - private static class Symm implements __2 { +interface Lift2 extends __5 { + enum µ {} - final TypeEq typeEq; + TypeEq<__<__, B>, __<__, X>> __(); - Symm(TypeEq typeEq) { - this.typeEq = typeEq; - } - - static Symm ofHkt(__<__<µ, A>, B> hkSymm) { - return (Symm) hkSymm; - } - - enum µ {} + static Lift2 narrow(__<__<__<__<__, A>, B>, C>, X> lift2) { + return (Lift2) lift2; } +} - private static class Lift implements __3 { - - final TypeEq<__, __> unlift; +interface Lift3_1 extends __5 { + enum µ {} - Lift(TypeEq<__, __> unlift) { - this.unlift = unlift; - } + TypeEq<__<__<__, B>, C>, __<__<__, B>, C>> __(); - static Lift ofHkt(__<__<__<µ, f>, A>, B> hkLift) { - return (Lift) hkLift; - } - - enum µ {} + static Lift3_1 narrow(__<__<__<__<__, A>, B>, C>, X> lift3) { + return (Lift3_1) lift3; } +} - private static class Lift2 implements __4 { - - final TypeEq<__<__, C>, __<__, C>> unlift2; - - Lift2(TypeEq<__<__, C>, __<__, C>> unlift2) { - this.unlift2 = unlift2; - } +interface Lift3_2 extends __6 { + enum µ {} - static Lift2 ofHkt(__<__<__<__<µ, f>, C>, A>, B> hkLift2) { - return (Lift2) hkLift2; - } + TypeEq<__<__<__, B>, C>, __<__<__, X>, C>> __(); - enum µ {} + static Lift3_2 narrow(__<__<__<__<__<__, A>, B>, C>, D>, X> lift3) { + return (Lift3_2) lift3; } +} - private static class Lift3 implements __5 { +interface Lift3 extends __7 { + enum µ {} - final TypeEq<__<__<__, C>, D>, __<__<__, C>, D>> unlift3; + TypeEq<__<__<__, B>, C>, __<__<__, E>, X>> __(); - Lift3(TypeEq<__<__<__, C>, D>, __<__<__, C>, D>> unlift3) { - this.unlift3 = unlift3; - } - - static Lift3 ofHkt(__<__<__<__<__<µ, f>, C>, D>, A>, B> hkLift3) { - return (Lift3) hkLift3; - } - - enum µ {} + static Lift3 narrow(__<__<__<__<__<__<__, A>, B>, C>, D>, E>, X> lift3) { + return (Lift3) lift3; } - -} \ No newline at end of file +} From 4f0b2de0544db2ef68e77115829fed25d668ea7f Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Gr=C3=A9goire=20Neuville?= Date: Thu, 25 May 2017 22:40:57 +0200 Subject: [PATCH 2/2] Make TypeEq and its inner types interfaces --- src/main/java/org/derive4j/hkt/TypeEq.java | 481 +++++++++------------ 1 file changed, 206 insertions(+), 275 deletions(-) diff --git a/src/main/java/org/derive4j/hkt/TypeEq.java b/src/main/java/org/derive4j/hkt/TypeEq.java index f66275e..dfeb63c 100644 --- a/src/main/java/org/derive4j/hkt/TypeEq.java +++ b/src/main/java/org/derive4j/hkt/TypeEq.java @@ -13,28 +13,149 @@ * @see Higher TypeEq * @see Leibnizian type equality in Haskell */ -public abstract class TypeEq implements __2 { +@SuppressWarnings("Convert2MethodRef") +public interface TypeEq extends __2 { + /** Type constructor witness of TypeEq. */ + enum µ {} - /** Serve as type constructor witness of TypeEq. */ - public enum µ {} + /** + * 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 type constructor witness of {@code fa} type. + * @return the input value with {@link A} substituted by {@link B} in its type. + */ + __ subst(__ 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. + */ + default B coerce(A a) { + return Id.narrow(subst((Id) () -> a)).__(); + } + + /** + * Equality is transitive. + * + * @param that another TypeEq to compose with. + * @param left operand of the transitive type equality. + * @return the composition of the TypeEq instances. + */ + default TypeEq compose(TypeEq that) { + return TypeEq.ofHkt(subst(that)); + } + + /** + * Equality is transitive. + * + * @param that another TypeEq to be composed with. + * @param right operand of the transitive type equality. + * @return the composition of the TypeEq instances. + */ + default TypeEq andThen(TypeEq that) { + return that.compose(this); + } + + /** + * Equality is symmetric. + * + * @return the type equality seen from the other side. + */ + default TypeEq symm() { + final Symm symm = () -> refl(); + + return Symm.narrow(subst(symm)).__(); + } + + /** + * The type equality can be lifted into any type constructor. + * + * @param a type constructor witness. + * @return the type equality in the context of the specified type constructor. + */ + default TypeEq<__, __> lift() { + final Lift _refl = () -> refl(); + + return Lift.narrow(subst(_refl)).__(); + } + + /** + * The type equality can be lifted into any type constructor, at any position. + * + * @param a type constructor witness. + * @param the last type variable (not substituted). + * @return the type equality in the context of the specified type constructor. + */ + default TypeEq<__<__, C>, __<__, C>> lift2() { + return lift2(refl()); + } + + /** + * 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 the last type variable before substitution. + * @param the last type variable after substitution. + * @return a factory to lift the TypeEq instances into any type constructor. + */ + default TypeEq<__<__, C>, __<__, D>> lift2(TypeEq cd) { + final Lift2_1 _refl = () -> refl(); - private TypeEq() { + final Lift2_1 lift2_1 = Lift2_1.narrow(subst(_refl)); + + final Lift2 lift2 = () -> lift2_1.__(); + + return Lift2.narrow(cd.subst(lift2)).__(); + } + + /** + * The type equality can be lifted into any type constructor, at any position. + * + * @param a type constructor witness. + * @param the before last type variable (not substituted). + * @param the last type variable (not substituted). + * @return the type equality in the context of the specified type constructor. + */ + default TypeEq<__<__<__, C>, D>, __<__<__, C>, D>> lift3() { + return lift3(refl(), refl()); + } + + /** + * 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 the before last type variable before substitution. + * @param the before last type variable after substitution. + * @param the last type variable before substitution. + * @param the last type variable after substitution. + * @return a factory to lift the TypeEq instances into any type constructor. + */ + default TypeEq<__<__<__, C>, E>, __<__<__, D>, F>> lift3(TypeEq cd + , TypeEq ef) { + final Lift3_1 _refl = () -> refl(); + + final Lift3_1 lift3_1 = Lift3_1.narrow(subst(_refl)); + + final Lift3_2 lift3_2 = () -> lift3_1.__(); + + final Lift3_2 lift3_2_1 = Lift3_2.narrow(cd.subst(lift3_2)); + + final Lift3 lift3 = () -> lift3_2_1.__(); + + return Lift3.narrow(ef.subst(lift3)).__(); } /** * Equality is reflexive: a type is equal to itself. * - * @param any type. + * @param any type. * @return a TypeEq representing the reflexive equality. */ - public static TypeEq refl() { - // The only possible implementation, the identity: - return new TypeEq() { - @Override public __ subst(final __ fa) { - return fa; - } - }; - } + static TypeEq refl() { return HktId::id; } /** * Recover the concrete type of a higher kinded TypeEq value. @@ -45,7 +166,7 @@ public static TypeEq refl() { * @param 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 TypeEq ofHkt(__<__, B> hkTypeEq) { + static TypeEq ofHkt(__<__, B> hkTypeEq) { return (TypeEq) hkTypeEq; } @@ -60,14 +181,14 @@ public static TypeEq ofHkt(__<__, B> hkTypeEq) { * @return a TypeEq instance witness of the type equality. */ @SuppressWarnings("unchecked") - public static TypeEq<__<__, B>, TypeEq> hkt() { - return (TypeEq) refl(); + static TypeEq<__<__, B>, TypeEq> hkt() { + return (TypeEq) TypeEq.refl(); } /** * Safe cast to __2. (guaranteed by the hkt type checker). */ - public static __2 as__2(__<__, B> fab) { + static __2 as__2(__<__, B> fab) { return (__2) fab; } @@ -81,14 +202,14 @@ public static __2 as__2(__<__, B> fab) { * @return a TypeEq instance witness of the type equality. */ @SuppressWarnings("unchecked") - public static TypeEq<__<__, B>, __2> __2() { + static TypeEq<__<__, B>, __2> __2() { return (TypeEq) TypeEq.refl(); } /** * Safe cast to __3. (guaranteed by the hkt type checker). */ - public static __3 as__3(__<__<__, B>, C> fabc) { + static __3 as__3(__<__<__, B>, C> fabc) { return (__3) fabc; } @@ -103,14 +224,14 @@ public static __3 as__3(__<__<__, B>, C> fabc) { * @return a TypeEq instance witness of the type equality. */ @SuppressWarnings("unchecked") - public static TypeEq<__<__<__, B>, C>, __3> __3() { + static TypeEq<__<__<__, B>, C>, __3> __3() { return (TypeEq) TypeEq.refl(); } /** * Safe cast to __4. (guaranteed by the hkt type checker). */ - public static __4 as__4(__<__<__<__, B>, C>, D> fabcd) { + static __4 as__4(__<__<__<__, B>, C>, D> fabcd) { return (__4) fabcd; } @@ -122,14 +243,14 @@ public static __4 as__4(__<__<__<__, B>, C> * @return a TypeEq instance witness of the type equality. */ @SuppressWarnings("unchecked") - public static TypeEq<__<__<__<__, B>, C>, D>, __4> __4() { + static TypeEq<__<__<__<__, B>, C>, D>, __4> __4() { return (TypeEq) TypeEq.refl(); } /** * Safe cast to __5. (guaranteed by the hkt type checker). */ - public static __5 as__5(__<__<__<__<__, B>, C>, D>, E> fabcde) { + static __5 as__5(__<__<__<__<__, B>, C>, D>, E> fabcde) { return (__5) fabcde; } @@ -141,14 +262,14 @@ public static __5 as__5(__<__<__<__<__ TypeEq<__<__<__<__<__, B>, C>, D>, E>, __5> __5() { + static TypeEq<__<__<__<__<__, B>, C>, D>, E>, __5> __5() { return (TypeEq) TypeEq.refl(); } /** * Safe cast to __6. (guaranteed by the hkt type checker). */ - public static __6 as__6(__<__<__<__<__<__, B>, C>, D>, E>, F> fabcdef) { + static __6 as__6(__<__<__<__<__<__, B>, C>, D>, E>, F> fabcdef) { return (__6) fabcdef; } @@ -160,15 +281,15 @@ public static __6 as__6(__<__<__<__<_ * @return a TypeEq instance witness of the type equality. */ @SuppressWarnings("unchecked") - public static TypeEq<__<__<__<__<__<__, B>, C>, D>, E>, F>, __6> __6() { + static TypeEq<__<__<__<__<__<__, B>, C>, D>, E>, F>, __6> __6() { return (TypeEq) TypeEq.refl(); } /** * Safe cast to __7. (guaranteed by the hkt type checker). */ - public static __7 as__7(__<__<__<__<__<__<__, B>, C>, D>, E>, F>, G> - fabcdefg) { + static __7 as__7(__<__<__<__<__<__<__, B>, C>, D>, E>, F>, G> + fabcdefg) { return (__7) fabcdefg; } @@ -180,7 +301,7 @@ public static __7 as__7(__<__<_ * @return a TypeEq instance witness of the type equality. */ @SuppressWarnings("unchecked") - public static TypeEq<__<__<__<__<__<__<__, B>, C>, D>, E>, F>, G>, __7> __7() { + static TypeEq<__<__<__<__<__<__<__, B>, C>, D>, E>, F>, G>, __7> __7() { return (TypeEq) TypeEq.refl(); } @@ -188,7 +309,7 @@ public static TypeEq<__<__<__<__<__<__<__, B>, C> /** * Safe cast to __8. (guaranteed by the hkt type checker). */ - public static __8 as__8(__<__<__<__<__<__<__<__, B>, C>, D>, E>, F>, G>, H> fabcdefgh) { + static __8 as__8(__<__<__<__<__<__<__<__, B>, C>, D>, E>, F>, G>, H> fabcdefgh) { return (__8) fabcdefgh; } @@ -200,7 +321,7 @@ public static __8 as__8(_ * @return a TypeEq instance witness of the type equality. */ @SuppressWarnings("unchecked") - public static TypeEq<__<__<__<__<__<__<__<__, B>, C>, D>, E>, F>, G>, H>, __8> __8() { + static TypeEq<__<__<__<__<__<__<__<__, B>, C>, D>, E>, F>, G>, H>, __8> __8() { return (TypeEq) TypeEq.refl(); } @@ -208,7 +329,7 @@ public static TypeEq<__<__<__<__<__<__<__<__, /** * Safe cast to __9. (guaranteed by the hkt type checker). */ - public static __9 as__9(__<__<__<__<__<__<__<__<__, B>, C>, D>, E>, F>, G>, H>, I> fabcdefghi) { + static __9 as__9(__<__<__<__<__<__<__<__<__, B>, C>, D>, E>, F>, G>, H>, I> fabcdefghi) { return (__9) fabcdefghi; } @@ -220,281 +341,91 @@ public static __9 a * @return a TypeEq instance witness of the type equality. */ @SuppressWarnings("unchecked") - public static TypeEq<__<__<__<__<__<__<__<__<__, B>, C>, D>, E>, F>, G>, H>, I>, __9> __9() { + static TypeEq<__<__<__<__<__<__<__<__<__, B>, C>, D>, E>, F>, G>, H>, I>, __9> __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 type constructor witness of {@code fa} type. - * @return the input value with {@link A} substituted by {@link B} in its type. - */ - public abstract __ subst(__ 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 left operand of the transitive type equality. - * @return the composition of the TypeEq instances. - */ - public final TypeEq compose(TypeEq that) { - return new TypeEq() { - @Override public __ subst(__ fa) { - return TypeEq.this.subst(that.subst(fa)); - } - }; - } - - /** - * Equality is transitive. - * - * @param that another TypeEq to be composed with. - * @param right operand of the transitive type equality. - * @return the composition of the TypeEq instances. - */ - public final TypeEq andThen(TypeEq that) { - return that.compose(this); - } - - /** - * Equality is symmetric. - * - * @return the type equality seen from the other side. - */ - public final TypeEq symm() { - return Symm.ofHkt(subst(new Symm<>(refl()))).typeEq; - } - - /** - * The type equality can be lifted into any type constructor. - * - * @param a type constructor witness. - * @return the type equality in the context of the specified type constructor. - */ - public final TypeEq<__, __> lift() { - return Lift.ofHkt(subst(new Lift<>(TypeEq.<__>refl()))).unlift; - } - - /** - * The type equality can be lifted into any type constructor, at any position. - * - * @param a type constructor witness. - * @param the last type variable (not substituted). - * @return the type equality in the context of the specified type constructor. - */ - public final TypeEq<__<__, C>, __<__, C>> lift2() { - return Lift2.ofHkt(subst(new Lift2<>(TypeEq.<__<__, 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 the last type variable before substitution. - * @param the last type variable after substitution. - * @return a factory to lift the TypeEq instances into any type constructor. - */ - public final Lift2TypeEq lift2(TypeEq cd) { - return new Lift2TypeEq(this, cd); - } - - /** - * The type equality can be lifted into any type constructor, at any position. - * - * @param a type constructor witness. - * @param the before last type variable (not substituted). - * @param the last type variable (not substituted). - * @return the type equality in the context of the specified type constructor. - */ - public final TypeEq<__<__<__, C>, D>, __<__<__, C>, D>> lift3() { - return Lift3.ofHkt(subst(new Lift3<>(TypeEq.<__<__<__, C>, D>>refl()))).unlift3; - } +// ################ Type inference helpers - /** - * 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 the before last type variable before substitution. - * @param the before last type variable after substitution. - * @param the last type variable before substitution. - * @param the last type variable after substitution. - * @return a factory to lift the TypeEq instances into any type constructor. - */ - public final Lift3TypeEq lift3(TypeEq cd, TypeEq ef) { - return new Lift3TypeEq(this, cd, ef); - } +interface HktId { + static __ id(__ ft) { return ft; } +} - /** - * Type inference helper class: - * allow to lift two TypeEq instances into any type constructor. - * - * @param the before last type variable before substitution. - * @param the last type variable before substitution. - * @param the before last type variable after substitution. - * @param the last type variable after substitution. - */ - public static final class Lift2TypeEq { - - private final TypeEq ab; +interface Id extends __ { + enum µ {} - private final TypeEq cd; + A __(); - Lift2TypeEq(TypeEq ab, TypeEq cd) { - this.ab = ab; - this.cd = cd; - } + static Id narrow(__ a) { return (Id) a; } +} - /** - * Lift two TypeEq instances into a type constructor. - * - * @param a type constructor witness. - * @return the type equalities in the context of the type constructor. - */ - public TypeEq<__<__, C>, __<__, D>> lift() { +interface Symm extends __2 { + enum µ {} - TypeEq<__<__, C>, __<__, C>> abLift = ab.lift2(); - TypeEq<__<__, C>, __<__, D>> cdLift = cd.lift(); + TypeEq __(); - return new TypeEq<__<__, C>, __<__, D>>() { - @Override public __, D>> subst(__, C>> fa) { - return cdLift.subst(abLift.subst(fa)); - } - }; - } + static Symm narrow(__<__, B> _lift) { + return (Symm) _lift; } +} - /** - * Type inference helper class: - * allow to lift three TypeEq instances into any type constructor. - * - * @param the antepenultimate type variable before substitution. - * @param the before last type variable before substitution. - * @param the last type variable before substitution. - * @param the antepenultimate type variable after substitution. - * @param the before last type variable after substitution. - * @param the last type variable after substitution. - */ - public static final class Lift3TypeEq { - - private final TypeEq ab; - - private final TypeEq cd; - - private final TypeEq ef; +interface Lift extends __3 { + enum µ {} - Lift3TypeEq(TypeEq ab, TypeEq cd, TypeEq ef) { - this.ab = ab; - this.cd = cd; - this.ef = ef; - } + TypeEq<__, __> __(); - /** - * Lift three TypeEq instances into a type constructor. - * - * @param a type constructor witness. - * @return the type equalities in the context of the type constructor. - */ - public TypeEq<__<__<__, C>, E>, __<__<__, D>, F>> lift() { - - TypeEq<__<__<__, C>, E>, __<__<__, C>, E>> abLift = ab.lift3(); - TypeEq<__<__<__, C>, E>, __<__<__, D>, E>> cdLift = cd.lift2(); - TypeEq<__<__<__, D>, E>, __<__<__, D>, F>> efLift = ef.lift(); - - return new TypeEq<__<__<__, C>, E>, __<__<__, D>, F>>() { - @Override public __, D>, F>> subst(__, C>, E>> fa) { - return efLift.subst(cdLift.subst(abLift.subst(fa))); - } - }; - } + static Lift narrow(__<__<__, A>, X> _lift) { + return (Lift) _lift; } +} - private static class Identity implements __ { - - final A runIdentity; - - Identity(A runIdentity) { - this.runIdentity = runIdentity; - } +interface Lift2_1 extends __4 { + enum µ {} - static Identity ofHkt(__<µ, A> hkId) { - return (Identity) hkId; - } + TypeEq<__<__, B>, __<__, B>> __(); - enum µ {} + static Lift2_1 narrow(__<__<__<__, A>, B>, X> lift1) { + return (Lift2_1) lift1; } +} - private static class Symm implements __2 { +interface Lift2 extends __5 { + enum µ {} - final TypeEq typeEq; + TypeEq<__<__, B>, __<__, X>> __(); - Symm(TypeEq typeEq) { - this.typeEq = typeEq; - } - - static Symm ofHkt(__<__<µ, A>, B> hkSymm) { - return (Symm) hkSymm; - } - - enum µ {} + static Lift2 narrow(__<__<__<__<__, A>, B>, C>, X> lift2) { + return (Lift2) lift2; } +} - private static class Lift implements __3 { - - final TypeEq<__, __> unlift; +interface Lift3_1 extends __5 { + enum µ {} - Lift(TypeEq<__, __> unlift) { - this.unlift = unlift; - } + TypeEq<__<__<__, B>, C>, __<__<__, B>, C>> __(); - static Lift ofHkt(__<__<__<µ, f>, A>, B> hkLift) { - return (Lift) hkLift; - } - - enum µ {} + static Lift3_1 narrow(__<__<__<__<__, A>, B>, C>, X> lift3) { + return (Lift3_1) lift3; } +} - private static class Lift2 implements __4 { - - final TypeEq<__<__, C>, __<__, C>> unlift2; - - Lift2(TypeEq<__<__, C>, __<__, C>> unlift2) { - this.unlift2 = unlift2; - } +interface Lift3_2 extends __6 { + enum µ {} - static Lift2 ofHkt(__<__<__<__<µ, f>, C>, A>, B> hkLift2) { - return (Lift2) hkLift2; - } + TypeEq<__<__<__, B>, C>, __<__<__, X>, C>> __(); - enum µ {} + static Lift3_2 narrow(__<__<__<__<__<__, A>, B>, C>, D>, X> lift3) { + return (Lift3_2) lift3; } +} - private static class Lift3 implements __5 { +interface Lift3 extends __7 { + enum µ {} - final TypeEq<__<__<__, C>, D>, __<__<__, C>, D>> unlift3; + TypeEq<__<__<__, B>, C>, __<__<__, E>, X>> __(); - Lift3(TypeEq<__<__<__, C>, D>, __<__<__, C>, D>> unlift3) { - this.unlift3 = unlift3; - } - - static Lift3 ofHkt(__<__<__<__<__<µ, f>, C>, D>, A>, B> hkLift3) { - return (Lift3) hkLift3; - } - - enum µ {} + static Lift3 narrow(__<__<__<__<__<__<__, A>, B>, C>, D>, E>, X> lift3) { + return (Lift3) lift3; } - -} \ No newline at end of file +}