Some experiments

GADT.java

public interface GADT {
  // Self-indexed natural numbers
  sealed interface Nat<T extends Nat<T>> {
    Nat<T> self();
  }
  record Z() implements Nat<Z> {
    public Z self() {return this;}
  }
  record S<T extends Nat<T>>(Nat<T> pred) implements Nat<S<T>> {
    public S<T> self() {return this;}
  }

  sealed interface Fin<T extends Nat<T>> {
    Fin<T> self();
  }
  record FZ<T extends Nat<T>>() implements Fin<S<T>> {
    public FZ<T> self() {return this;}
  }
  record FS<T extends Nat<T>>(Fin<T> pred) implements Fin<S<T>> {
    public FS<T> self() {return this;}
  }

  static void instancesOf2() {
    // The only two canonical instances of finite set of cardinality 2
    Fin<S<S<Z>>> fs1 = new FZ<>();
    Fin<S<S<Z>>> fs2 = new FS<>(new FZ<>());

    Fin<S<Z>> test = new FZ<Z>();
    Fin<S<Z>> test2 = new FS<>(new FZ<>());
  }

  static void unit(Fin<S<Z>> fin) {
    System.out.println(switch (fin) {
      case FZ<Z> f -> "the only thing";
      case FS<Z>(var kid) -> switch (kid) {
      };
    });
  }

  static void empty(Fin<Z> fin) {
    System.out.println(switch (fin) {
      case FZ f -> "the only thing";
    });
  }
}