Comparison of basic length-indexed vectors in Haskell and Java

Dependent.hs

{-# LANGUAGE GADTs, TypeFamilies, DataKinds, TypeOperators, StandaloneDeriving #-}

module Dependent where

data Nat = Z | S Nat

data Vec (n :: Nat) a where
  Nil :: Vec Z a
  Cons :: a -> Vec n a -> Vec (S n) a

deriving instance Show a => Show (Vec n a)

type family (+) (n :: Nat) (m :: Nat) where
  Z + m = m
  S n + m = S (n + m)

append :: Vec n a -> Vec m a -> Vec (n + m) a
append Nil ys = ys
append (Cons x xs) ys = Cons x (append xs ys)

main :: IO ()
main = do
  putStrLn "\nRunning...\n"
  let vec1 = Cons "a" (Cons "b" Nil)
  let vec2 = Cons "c" (Cons "d" (Cons "e" Nil))
  print vec1
  print (append vec1 vec2)

Dependent.java

package dependent;
import static dependent.Dependent.Nat.*;
import static dependent.Dependent.Nat.Plus.*;
import static dependent.Dependent.Vec.*;

public interface Dependent {
    public static sealed interface Nat<n extends Nat> permits Z, S {
        // We're using these as Nat types *and* as corresponding singletons
        public static record Z() implements Nat<Z> {}
        public static record S<n extends Nat>(n pred) implements Nat<S<n>> {}

        public static Nat<Z> Z() {return new Z();}
        public static <n extends Nat> Nat<S<n>> S(n pred) {return new S<>(pred);}

        public static sealed interface Plus<n extends Nat, m extends Nat, npm extends Nat>
            permits PZ, PS {
                public static record PZ<m extends Nat>() implements Plus<Z, m, m> {}
                public static record
                    PS<n extends Nat, m extends Nat, npm extends Nat>(Plus<n, m, npm> p)
                        implements Plus<S<n>, m, S<npm>> {}

                public static <m extends Nat> Plus<Z, m, m> PZ() {return new PZ<>();}
                public static <n extends Nat, m extends Nat, npm extends Nat>
                    Plus<S<n>, m, S<npm>> PS(Plus<n, m, npm> p) {return new PS<>(p);}
            }
    }

    public static sealed interface Vec<n extends Nat, a> permits Nil, Cons {
        public static record Nil<a>() implements Vec<Z, a> {}
        public static record Cons<n extends Nat, a>(a head, Vec<n, a> tail)
                implements Vec<S<n>, a> {}

        public static <a> Vec<Z, a> Nil() {return new Nil<>();}
        public static <a, n extends Nat> Vec<Nat.S<n>, a> Cons(a head, Vec<n, a> tail) {
            return new Cons<>(head, tail);
        }

        public static <n extends Nat, m extends Nat, npm extends Nat, a> Vec<npm, a>
            append(Vec<n, a> xs, Vec<m, a> ys, Plus<n, m, npm> p) {
                if (xs instanceof Nil nil && p instanceof PZ pz) {
                    // Java thinks this is unsafe :( not sure how to fix that
                    return (Vec<npm, a>)ys;
                } else if (xs instanceof Cons cons && p instanceof PS ps) {
                    // unfortunately this will allow you to call append with ps
                    // instead of ps.p, which would be unsafe
                    // I'm not sure why you can do it
                    return Cons(cons.head, append(cons.tail, ys, ps.p));
                }
                // other cases shouldn't be possible but Java doesn't know :(
                throw new RuntimeException("Impossible");
            }
    }

    public static void main(String[] args) {
        System.out.println("\nRunning...\n");
        var vec1 = Cons("a", Cons("b", Nil()));
        var vec2 = Cons("c", Cons("d", Cons("e", Nil())));
        System.out.println(vec1);
        // Have to construct the type level computation manually, but Java will
        // make sure it is correct
        // If you use a function that returns an existential containing a proof
        // you might be able to avoid having to compute it manually
        System.out.println(append(vec1, vec2, PS(PS(PZ()))));
    }
}