Add support for Generalized Algebraic Data Types

[jbgi]

This probably requires a new specialized annotation, but it would be really cool if adt4j could help to define GADTs in Java!
This is what I am after: https://gist.github.com/jbgi/208a1733f15cdcf78eb5

[sviperll]

I've tried to explore what is possible: https://gist.github.com/sviperll/61fa58616b1d7bfb325c

I'll think about it.

[sviperll]

I think I can add full support for GADTs (so it'a a massive work...) with the help of special equality proof type.

We can define a special class in adt4j codebase and use it to derive additional type information almost without any run-time overhead.

public class Eq<A, B> {

    @SuppressWarnings(value = "rawtypes")
    private static final Eq INSTANCE = new Eq();

    @SuppressWarnings(value = "unchecked")
    public static <T> Eq<T, T> prove() {
        return INSTANCE;
    }

    private Eq() {
    }

    @SuppressWarnings(value = "unchecked")
    public A castForward(B b) {
        return (A) b;
    }

    @SuppressWarnings(value = "unchecked")
    public B castBackward(A a) {
        return (B) a;
    }

}

we can use it's presence as an argument to visitor methods to provide correct and type-safe casts. Instances of this class can be used to write type-safe visitors, that can use provided cast-methods.

@ParametersAreNonnullByDefault
@WrapsGeneratedValueClass(visitor = GADT2Visitor.class)
public abstract class GADT2<T> extends GADT2Base<T> {
    private GADT2(GADT2Base<T> base) {
        super(base);
    }

    public abstract <R> R accept(GADT2Visitor<T, R> visitor);

    T eval() {
        return accept(new GADT2Visitor<T, T>() {
            @Override
            public <A, B> T lambda(Function<A, B> function, Eq<T, Function<A, B>> proof) {
                return proof.castForward(function);
            }

            @Override
            public <U> T apply(GADT2<Function<U, T>> function, GADT2<U> argument) {
                return function.eval().apply(argument.eval());
            }

            @Override
            public T number(int n, Eq<T, Integer> proof) {
                return proof.castForward(n);
            }

            @Override
            public T plus(GADT2<Integer> a, GADT2<Integer> b, Eq<T, Integer> proof) {
                return proof.castForward(a.eval() + b.eval());
            }

            @Override
            public T isLessOrEqual(GADT2<Integer> a, GADT2<Integer> b, Eq<T, Boolean> proof) {
                return proof.castForward(a.eval() <= b.eval());
            }

            @Override
            public T if_(GADT2<Boolean> condition, GADT2<T> iftrue, GADT2<T> iffalse) {
                return condition.eval() ? iftrue.eval() : iffalse.eval();
            }
        });
    }


    @GenerateValueClassForVisitor(wrapperClass = GADT2.class)
    @Visitor(resultVariableName = "R")
    public interface GADT2Visitor<T, R> {
        <A, B> R lambda(Function<A, B> function, Eq<T, Function<A, B>> proof);
        <U> R apply(GADT2<Function<U, T>> function, GADT2<U> argument);
        R number(int n, Eq<T, Integer> constr);
        R plus(GADT2<Integer> a, GADT2<Integer> b, Eq<T, Integer> proof);
        R isLessOrEqual(GADT2<Integer> a, GADT2<Integer> b, Eq<T, Boolean> proof);
        R if_(GADT2<Boolean> condition, GADT2<T> iftrue, GADT2<T> iffalse);
    }
}

[jbgi]

Interesting! I see this encoding add the castBackward capability compared to my original gist. What is the use case for it?

[sviperll]

It's basically your original gist. The difference is that if we define special type for refied type-equality constaints we can actually use this information to generate expected constructor methods with correct type-signature.

Here is an example of generated code:

class GADT2Base<T> {
    private <A, B, T> GADT<T> lambda(Function<A, B> function, Eq<T, Function<A, B>> proof) {
        ...
    }

    // Type signature of generated method is derived using type-arguments of Eq type
    public <A, B> GADT<Function<A, B>> lambda(Function<A, B> function) {
        return lambda<A, B, Function<A, B>>(function, Eq.prove());
    }
}

[sviperll]

Though castBackward is added here for completeness, I think there should be an example of it's usefullness, but I can't imaging it right away :)

[jbgi]

I see. In derive4j I use any type that is isomorphic to Function<A, B> -> T as valid reified constraint (but is is a easier to do in derive4j because it only support java 8). eg. https://github.com/derive4j/derive4j/blob/master/examples/src/main/java/org/derive4j/exemple/Term.java#L88
which generate https://gist.github.com/jbgi/ea92a70751782e204c46

Eq (aka Leibniz) would be useful in a language supporting higher kinded polymorphism, but probably not so much in java. It also introduce a runtime dependency...

[sviperll]

Do you treat the name id as a special one to use it as a type-cast?

[jbgi]

no, any parameter that is at the end of the parameter list and which is a functional interface isomorphic to Function<A, B> -> T will do.

[sviperll]

Is there some formal rule for this? What about data types with multiple type parameters?

[jbgi]

I need to write the spec of the heuristic that find GADT constraint parameters. It should work for also when multiple type parameters and also multiple constraints (if you find a counter-example let me know). I will post the spec here when done.
Edit: currently derive4j does not support parametrized visitor methods (lambda and apply cases) need to see how to work that out.

[sviperll]

@jbgi Is it ever possible to somehow push for higher-kinded polymorphism in Java? You seems to be an active member of functionaljava community. I think functionaljava community should strive to get HKP in Java.

What is the most common workaround for missing higher-kinded type-variables. In context of GADT, we may desire to implement clone function. Here is some code. The problem is that I can't write typeEquality function that is to promote type equality of type-arguments to type-application... It cause compile-time error even thought I thought that type-casts can overcome any type-system constraints in Java...

public abstract class GADT2<T> /* extends GADT2Base<T> */ {
    public static <A, B> GADT2<Function<A, B>> lambda(final Function<A, GADT2<B>> function) {
        /* ... */
    }

    public static <T, U> GADT2<U> apply(final GADT2<Function<T, U>> function, final GADT2<T> argument) {
        /* ... */
    }

    public static GADT2<Integer> number(int n) {
        /* ... */
    }

    public static GADT2<Integer> plus(final GADT2<Integer> a, final GADT2<Integer> b) {
        /* ... */
    }

    public static GADT2<Boolean> isLessOrEqual(final GADT2<Integer> a, final GADT2<Integer> b) {
        /* ... */
    }

    public static <T> GADT2<T> if_(final GADT2<Boolean> cond, final GADT2<T> a, final GADT2<T> b) {
        /* ... */
    }

    public static <T, U> TypeEquality<GADT2<T>, GADT2<U>> typeEquality(TypeEquality<T, U> proof) {
        return (TypeEquality<GADT2<T>, GADT2<U>>)TypeEquality.<GADT2<T>>prove(); // Compile-time error...
    }

    GADT2(/* GADT2Base<T> base */) {
        // super(base);
    }

    public abstract <R> R accept(GADT2Visitor<T, R> visitor);

    T eval() {
        /* ... */
    }

    GADT2<T> cloneGADT2() {
        return accept(new GADT2Visitor<T, GADT2<T>>() {
            @Override
            public <A, B> GADT2<T> lambda(Function<A, GADT2<B>> function, TypeEquality<T, Function<A, B>> proof) {
                return GADT2.typeEquality(proof).cast(GADT2.<A, B>lambda(function));
            }

            @Override
            public <U> GADT2<T> apply(GADT2<Function<U, T>> function, GADT2<U> argument) {
                return GADT2.apply(function, argument);
            }

            @Override
            public GADT2<T> number(int n, TypeEquality<T, Integer> proof) {
                return GADT2.typeEquality(proof).cast(GADT2.number(n));
            }

            @Override
            public GADT2<T> plus(GADT2<Integer> a, GADT2<Integer> b, TypeEquality<T, Integer> proof) {
                return GADT2.typeEquality(proof).cast(GADT2.plus(a, b));
            }

            @Override
            public GADT2<T> isLessOrEqual(GADT2<Integer> a, GADT2<Integer> b, TypeEquality<T, Boolean> proof) {
                return GADT2.typeEquality(proof).cast(GADT2.isLessOrEqual(a, b));
            }

            @Override
            public GADT2<T> if_(GADT2<Boolean> condition, GADT2<T> trueValue, GADT2<T> falseValue) {
                return GADT2.if_(condition, trueValue, falseValue);
            }
        });
    }

    // @GenerateValueClassForVisitor(wrapperClass = GADT2.class)
    @Visitor(resultVariableName = "R")
    public interface GADT2Visitor<T, R> {
        <A, B> R lambda(Function<A, GADT2<B>> function, TypeEquality<T, Function<A, B>> proof);
        <U> R apply(GADT2<Function<U, T>> function, GADT2<U> argument);
        R number(int n, TypeEquality<T, Integer> constr);
        R plus(GADT2<Integer> a, GADT2<Integer> b, TypeEquality<T, Integer> proof);
        R isLessOrEqual(GADT2<Integer> a, GADT2<Integer> b, TypeEquality<T, Boolean> proof);
        R if_(GADT2<Boolean> condition, GADT2<T> trueValue, GADT2<T> falseValue);
    }
}

[sviperll]

Hmmm... We can make it work.... with cast to Object...

    public static <T, U> TypeEquality<GADT2<T>, GADT2<U>> typeEquality(TypeEquality<T, U> proof) {
        return (TypeEquality<GADT2<T>, GADT2<U>>)(Object)TypeEquality.<GADT2<T>>prove(); // Compile-time error...
    }

[sviperll]

Maybe we can implement some annotation processor to generate TypeEquality (aka Leibniz) class, and treat it like lack of higher-kinded polymorphism sin-bin, like this:

@ExtendsGeneratedTypeEqualityImplementation(
    typeConstructors1 = {GADT.class},
    typeConstructors2 = {Pair.class},
    typeConstructors3 = {...},
    typeConstructors4 = {...},
    typeConstructors5 = {...},
)
class TypeEquality<T, U> extends TypeEqualityBase<T, U> {
    TypeEquality(TypeEqualityBase<T, U> base) {
        super(base);
    }
}

And generated code will be:

class TypeEqualityBase<T, U> {
    public static <T> TypeEquality<T, T> prove() {
        // ...
    }

    // GADT listed as type constructor1
    public static <T, U> TypeEquality<GADT<T>, GADT<U>> toGADT(TypeEquality<T, U> proof) {
        // ...
    }

    public static <T, U> TypeEquality<T, U> fromGADT(TypeEquality<GADT<T>, GADT<U>> proof) {
        // ...
    }

    // Pair listed as type constructor2
    public static <T, U, V, W> TypeEquality<Pair<T, U>, Pair<V, W>> toPair(TypeEquality<T, V> proof1, TypeEquality<U, W> proof2) {
        // ...
    }

    public static <T, U> TypeEquality<T, U> fromPair1(TypeEquality<Pair<T, ?>>, Pair<U, ?>> proof) {
        // ...
    }

    public static <T, U> TypeEquality<T, U> fromPair2(TypeEquality<Pair<?, T>>, Pair<?, U>> proof) {
        // ...
    }

    public final T cast(U u) {
        return (T)u;
    }

    public final TypeEquality<U, T> reverse() {
        // ...
    }

}

[nobeh]

Thanks for thinking about this requirement. If I may, I'd like to come in with a different example into this context.

Let's consider this psuedo/modelling code:

data Map<A, B> = EmptyMap | InsertAssoc(Pair<A, B>, Map<A, B>);

which defines a Map data structure in ADT composed of an EmptyMap and an InsertAssoc operation. And, it is quite straightforward to map the above to:

@GenerateValueClassForVisitor
@Visitor(selfReferenceVariableName = "SELF", resultVariableName = "M")
public interface MapVisitor<M,SELF,A,B> {
  M EmptyMap();
  M InsertAssoc(Pair<A, B> argPair, SELF argMap);
}

Now, I have a different challenge to deal with, which generally is under the class of "pattern matching" which is addressed in this library by using the visitor pattern. Consider the following:

def Map<A, B> put(Map<A, B> ms, A k, B v) =
  case ms {
    EmptyMap => InsertAssoc(Pair(k, v), EmptyMap);
    InsertAssoc(Pair(k_, v_), ts) => if (k == k_)
      then
        InsertAssoc(Pair(k_, v), ts)     
      else 
        InsertAssoc(Pair(k_, v_), put_(ts, k, v))
      ;
  };

The above is a put function that defines how to an insert operation to a Map. My question is how would you generally translate this example of pattern matching with deep matching structure to a visitor pattern?

I thought that this might be relevant into this ticket but if not, please feel free to move into a new ticket.

[jbgi]

the more general workaround for HK types in java in Java is that every parametrized class implements a common marker interface namely HK<TC, A>:

public interface HK<TC, A> {}

This approach is used in https://github.com/DanielGronau/highj/blob/master/src/main/java/org/highj/_.java

The catch of HK types in java is that you have to write a static narrow method for each class, to retrieve the actual type from the HK realm:
eg. for List you would write:

class List<A> implements HK<List<?>, A> {
  static <A> List<A> narrow(HK<List<?>, A> hkList) {
    return (List) hkList;
  }
}

note that it also scales to multiple type variables:

public class Either<A, B> implements HK<HK<Either<?, ?>, A>, B> {
    public static <A, B> Either<A, B> narrow(HK<HK<Either<?, ?>, A>, B> hkEither) {
        return (Either) hkEither;
    }
}

Also note that subtyping does not play well with this approach, : you cannot have both List<A> implements HK<List<?>, A> and ArrayList<A> extends List<A> implements HK<ArrayList<?>, A>.

The plan to bring HK types to Java would be to extract the classes at the root of https://github.com/DanielGronau/highj/tree/master/src/main/java/org/highj (maybe with some renaming) into a separate project that would allow HK interoperability between multiple java projects.

The good news is that adt4J or derive4J could generate the narrow method for us (and also generate/ensure a correct inheritance of the HK interface.

WDYT?

[sviperll]

I was actually talking about native HK support by Java compiler...

Year, I know about marker-interface solution, but I don't like it

• it lacks static guarantees;
• inheritance story is somewhat ugly...
• it requires correct implementation of narrow and even though we can generate it in adt4 or derive4j, we may what to implement HK for custom class or even some externally defined class...

What do you think about about generating single TypeEquality class with functions for each required type-constructor?

[jbgi]

@sviperll Java will optimistically gains native sum types by 2025. Not sure I will still be alive to see native support for HK... but I agree with your points.
Leibnitz could be a useful addition to FunctionalJava. Not sure if generating it would be useful.
Here is how I could see things going relatively to an adt generator:
The following class exist in some library (let's say functional-java):

public abstract class Leibniz<A, B> {
    private Leibniz() {super();}

    public abstract B subst(A a);

    // Should be the only way to instantiate a Leibniz:
    public static <A> Leibniz<A, A> refl() {
        return new Leibniz<A, A>() {
            @Override
            public A subst(final A a) {
                return a;
            }
        };
    }
}

Then the adt generator compensate for the lack of HK support by generating, eg for List:

    public static <A, B> Leibniz<List<A>, List<B>> liftLeibniz(Leibniz<A, B> evidence) {
        return (Leibniz) Leibniz.refl();
    }

or for Either:

    public static <A, B, X> Leibniz<Either<A, B>, Either<X, B>> liftLeibnizA(Leibniz<A, X> evidence) {
        return (Leibniz) Leibniz.refl();
    }

    public static <A, B, X> Leibniz<Either<A, B>, Either<A, X>> liftLeibnizB(Leibniz<A, X> evidence) {
        return (Leibniz) Leibniz.refl();
    }

There is still a lot of casting going on, so I'm not sure it is an improvement over the more general marker interface solution...
Eg. With HK marker interface above we could have something like:

public interface Leibniz<A, B> extends HK<HK<Leibniz<?, ?>, A>, B> {

    class TypeLambda<TC, TCA,TCB, A, B> implements HK<HK<TypeLambda<TC, TCA, TCB, ? ,?>, A>, B> {

        HK<HK<TC, HK<TCA, A>>, HK<TCB, B>> wrapped;

        TypeLambda(HK<HK<TC, HK<TCA, A>>, HK<TCB, B>> res) {
            this.wrapped = res;
        }

        static <TC, TCA, TCB, A, B> TypeLambda<TC,TCA, TCB, A, B> narrow(
                HK<HK<TypeLambda<TC, TCA, TCB, ?, ?>, A>, B> hkLambda) {
            return (TypeLambda) hkLambda;
        }
    }

    <TC> HK<TC, B> subst(HK<TC, A> fa);

    static <TC, A, B> Leibniz<HK<TC, A>, HK<TC, B>> lift(Leibniz<A, B> ab) {
        return narrow(TypeLambda.narrow(ab.subst(new TypeLambda<>(Leibniz.<HK<TC, A>>refl()))).wrapped);
    }

    static <A,B> Leibniz<A, B> narrow(HK<HK<Leibniz<?, ?>, A>, B> hkLeibniz) {
        return (Leibniz) hkLeibniz;
    }

    // The only possible implementation :
    static <A> Leibniz<A, A> refl() {
        return new Leibniz<A, A>() {
            @Override
            public <TC> HK<TC, A> subst(final HK<TC, A> fa) {
                return fa;
            }
        };
    }
}

(adapted from http://typelevel.org/blog/2014/07/02/type_equality_to_leibniz.html)
But overall I think that java is not worth the effort..

[sviperll]

Following our discussion, I've implemented somewhat almost type-safe emulation of higher-kinded types with corresponding generic Functor and Monad interfaces. See higher-kinded-java repository, All type casts are located in single utility class Type.

Higher-kinded types can be easily created with no type-casts required in the source code and with type-checks that provide almost full type-safety.

I can see two problems with this

1. type safety is not full, it's almost full and there is a big difference :)
2. type equality proofs are still required in source code and they can be unwieldy

@Override
public <CAAT extends Monad<TypeConstructor, List<?>, CAAT, CAT>,
        CAT extends Monad<TypeConstructor, List<?>, CAT, T>, T>
                 CAT join(CAAT values) {
    Type.Equality<CAAT, List<CAT>> equality1 =
            Type.Equality.<TypeConstructor, List<?>, CAAT, List<CAT>, CAT>obviousForConstructorApplication();
    Type.Equality<CAT, List<T>> equality2 =
            Type.Equality.<TypeConstructor, List<?>, CAT, List<T>, T>obviousForConstructorApplication();
    Type.Equality<List<CAT>, List<List<T>>> equality3 =
            equality2.<TypeConstructor, List<?>, List<CAT>, List<List<T>>>toTypeConstructorApplication();
    Type.Equality<CAAT, List<List<T>>> equality4 =
            equality1.merge(equality3);

    return equality2.cast(List.join(equality4.reverse().cast(values)));
}

[jbgi]

Interesting. but it looks like javac does not keep-up with you and gives up pretty easily, because this compile:

  public static void main(String[] args) {
    Monad.Util<List.TypeConstructor, List<?>> monad = List.empty().monad();
    System.out.println(unitOneIsString(monad));
  }

  static <C extends Type.Constructor<C, CA>, CA extends Monad<C, CA, ? extends CA, ?>>
  String unitOneIsString(Monad.Util<C, CA> monad) {
    return monad.unit(1);
  }

It should of course be a type error.
If it were a type error then I think the correct return type would be Monad<C, CA, ?, Integer> but then I face this problem:

  public static void main(String[] args) {
    Monad.Util<List.TypeConstructor, List<?>> monad = List.empty().monad();
    Monad<List.TypeConstructor, List<?>, ?, Integer> unitOne = unitOne(monad);
    List<Integer> unitOneList = ??? // how to recover a List<Integer> from a Monad<List.TypeConstructor, List<?>, ?, Integer> ?
    System.out.println(unitOneList);
  }

  static <C extends Type.Constructor<C, CA>, CA extends Monad<C, CA, ? extends CA, ?>>
  Monad<C, CA, ?, Integer> unitOne(Monad.Util<C, CA> monad) {
    return monad.unit(1);
  }

There may be something wrong in my type signatures... but I think this scenario should be covered by a HKT encoding.

[sviperll]

You should just type List<Integer>

  public static void main(String[] args) {
    Monad.Util<List.TypeConstructor, List<?>> monad = List.empty().monad();
    List<Integer> unitOne = ThisClass.<List.TypeConstructor, List<?>, List<Integer>>unitOne(monad);
    System.out.println(unitOneList);
  }

  static <C extends Type.Constructor<C, CA>, CA extends Monad<C, CA, ? extends CA, ?>, CAT extends Monad<C, CA, CAT, Integer>>
  CAT unitOne(Monad.Util<C, CA> monad) {
    return monad.unit(1);
  }

[sviperll]

Lack of type error seems strange and bad though

[jbgi]

I see, the type variables of my unitOne were not enough. note that the tyoe error allso accur at call site:

String unitOneIsString = Main.unitOne(monad);

There is also the problem of F bounded polymorphism that is not completely type safe, ie you can write

class Option<T> implements Type.ConstructorApplication<List.TypeConstructor, List<?>, Option<T>, T> {  }

or

class Option<T> implements Type.ConstructorApplication<List.TypeConstructor, List<?>, List<T>, T> {  }

There is also the task of generalising to multiple type variables. I get the impression that this is going to be wild with this approach ;)
For now, I think the verbosity of type variables and the problem of unsafe cast make the approach rather impractical. (highj has the same problems to a different extend)

[sviperll]

You can't write

class Option<T> implements Type.ConstructorApplication<List.TypeConstructor, List<?>, Option<T>, T> {  }

We obtain requirement for CAT type argument to extend CA type argument given that single type can implement interface only once.

Still your second example type-checks... and this seems a hard problem. But having the lack of proper declaration checking we can give up on it entirely and obtain a somewhat simpler scheme without "type-constructor phantom type" and get closer to highj encoding.

class Option<T> implements Type.ConstructorApplication<Option<?>, Option<T>, T> {  }

The advantage over highj still remains. We require no type-casts in user's code.

But the downfall... I still can't understand how javac type-checks

String unitOneIsString = Main.unitOne(monad);

I can't make it type-check with explicit type-parameters. Is it a bug? Does javac construct some inexpressible recursive types internally? This one line ruins it all :)

[jbgi]

Yeah, looks like soundness guarantee is a hard problem for compilers. See also scala/scala3#50 (comment) and the whole thread.

[jbgi]

But maybe, by giving-up on F-Bounded polymorphism we can recover the lost soundness? and also that would make the encoding more scalable to multiple type variables.

[sviperll]

I've introduced Self interface, see last commit. It somewhat helps with type-checking... But it requires some discipline...

[jbgi]

FYI, an annotation processor is being worked on to add type-safety to the highj encoding. See derive4j/hkt#1 (input welcomed).

[sviperll]

@jbgi You seem to be interested in this topic. I don't know where else to write about this, so I continue to discuss the possibilities of higher-kinded Java programming here.

I've been experimenting with different encodings and I've come up with some new scheme with the ergonomics I mostly like. It is currently presented in higher-kinded-java repository

Basically It's a highj encoding, but with existential type twist. You can get a taste of using it as a library by looking at the Main.java source code.

All operations which require higher-kinded types are performed on Type.App type (You seems to like underscore as a name for this). What I propose is to forbid for users to implement this type(interface) or to manually construct it's instances. The way to use this interface is with the help of some annotation processor, like this:

@ImplementsGeneratedTypeSupportInterface
public interface List<T> extends GeneratedListTypeSupport<T> {
    // GeneratedListTypeSupport interface is generated by annotation processor
    // no additional code is required to implement GeneratedListTypeSupport

    // Ordinary list definition
}

When you implement such generated interface you get a way to use Type.App.
When you implement TypeSupport interface, your class/interface obtain subclass TypeConstructor with field get and you can use it like this:

    List.TypeConstructor.Is<?> proof = List.TypeConstructor.get;

List.TypeConstructor.Is is also generated by annotation processor. List.TypeConstructor.Is object is parametrized by a wildcard-argument. And this is the major difference from highj. The only way to actually use this object is to capture this wildcard:

    <L> void playWithListType(List.TypeConstructor.Is<L> proof) {
    }

    void run() {
        List.TypeConstructor.Is<?> proof = List.TypeConstructor.get;
        playWithListType(proof);
    }

And only after you have captured a wildcard you can use Type.App objects:

    <L> void playWithListType(List.TypeConstructor.Is<L> proof) {
        Type.App<L, Integer> typeApp = proof.convertToTypeApp(List.of(3));
        List<Integer> list = proof.convertToList(typeApp);
    }

    void run() {
        List.TypeConstructor.Is<?> proof = List.TypeConstructor.get;
        playWithListType(proof);
    }

You can't do it without capturing wildcard into some type-variable.

    void run() {
        List.TypeConstructor.Is<?> proof = List.TypeConstructor.get;
        Type.App<?, Integer> typeApp = proof.convertToTypeApp(List.of(3));

        // Compile-time error can't unify two different captured types
        List<Integer> list = proof.convertToList(typeApp);
    }

So, basically this captured type variable is a proof that Type.App instance is created by the same type-constructor-is-object and can be safely transformed back into a List. And you can't do anything without capturing since List.TypeConstructor.get field is actually parametrized with wildcard-type-argument.

Having this framework at your disposal it's easy to get your Monads with type-safe implementations (List, Optional)

Rawtypes, manual instantiation of Type.App interface and plain old casts
can all circumvernt type-safety and cause ClassCastException
But all these features are expected to be inherently unsafe.

Manual instantiation of Type.App interface can be made visibly unsafe
we can add method like

    void pleaseDoNotImplementMeItIsUnsafe();

to make it obviously and visibly unsafe.

The remaining piece of a puzzle is an annotation processor to actually generate required code, but it seems not so difficult to implement