Dependently-typed Iterable

SizedIterable.java

package example;

import com.jnape.palatable.lambda.functions.builtin.fn2.Cons;
import com.jnape.palatable.lambda.functions.builtin.fn2.Snoc;

import java.util.Iterator;

import static com.jnape.palatable.lambda.functions.builtin.fn3.FoldLeft.foldLeft;
import static example.SizedIterable.Nat.s;
import static example.SizedIterable.Nat.stringify;
import static example.SizedIterable.Nat.z;
import static java.util.Collections.emptyList;

public class SizedIterable<A, N extends SizedIterable.Nat> implements Iterable<A> {

    public static interface Nat {

        public static interface OnePlus<N extends Nat> extends Nat.S<N> {}

        public static interface TwoPlus<N extends Nat> extends Nat.S<Nat.OnePlus<N>> {}

        public static interface ThreePlus<N extends Nat> extends Nat.S<Nat.TwoPlus<N>> {}

        public static interface FourPlus<N extends Nat> extends Nat.S<Nat.ThreePlus<N>> {}

        public static interface FivePlus<N extends Nat> extends Nat.S<Nat.FourPlus<? extends N>> {}

        public static interface SixPlus<N extends Nat> extends Nat.S<Nat.FivePlus<N>> {}

        public static interface SevenPlus<N extends Nat> extends Nat.S<Nat.SixPlus<N>> {}

        public static interface EightPlus<N extends Nat> extends Nat.S<Nat.SevenPlus<N>> {}

        public static interface NinePlus<N extends Nat> extends Nat.S<Nat.EightPlus<N>> {}

        public static interface TenPlus<N extends Nat> extends Nat.S<Nat.NinePlus<N>> {}

        public static interface TwentyPlus<N extends Nat> extends Nat.TenPlus<Nat.TenPlus<N>> {}

        public static interface One extends Nat.OnePlus<Nat.Z> {}

        public static interface Two extends Nat.OnePlus<Nat.One> {}

        public static interface Three extends Nat.OnePlus<Nat.Two> {}

        public static interface Four extends Nat.OnePlus<Nat.Three> {}

        public static interface Five extends Nat.OnePlus<Nat.Four> {}

        public static interface Six extends Nat.OnePlus<Nat.Five> {}

        public static interface Seven extends Nat.OnePlus<Nat.Six> {}

        public static interface Eight extends Nat.OnePlus<Nat.Seven> {}

        public static interface Nine extends Nat.OnePlus<Nat.Eight> {}

        public static interface Ten extends Nat.OnePlus<Nat.Nine> {}

        public static String stringify(SizedIterable<Character, SizedIterable.Nat.Two> chars) {
            return foldLeft(StringBuilder::append, new StringBuilder(), chars).toString();
        }

        public static void main(String[] args) {

            SizedIterable<Character, SizedIterable.Nat.TwoPlus<SizedIterable.Nat.Ten>> snoc = SizedIterable.<Character, SizedIterable.Nat.One, SizedIterable.Nat.Two, SizedIterable.Nat.Three, SizedIterable.Nat.Four, SizedIterable.Nat.Five>of('a', 'b', 'c', 'd', 'e')
                .<SizedIterable.Nat.Six>snoc('f')
                .<SizedIterable.Nat.Seven>snoc('f')
                .<SizedIterable.Nat.Eight>snoc('f')
                .<SizedIterable.Nat.Nine>snoc('f')
                .<SizedIterable.Nat.Ten>snoc('f')
                .<SizedIterable.Nat.OnePlus<SizedIterable.Nat.Ten>>snoc('f')
                .<SizedIterable.Nat.TwoPlus<SizedIterable.Nat.Ten>>snoc('f');

            System.out.println(stringify(SizedIterable.<Character>empty().<SizedIterable.Nat.One>snoc('1').snoc('2')));
        }

        public static SizedIterable.Nat.Z z() {
            return SizedIterable.Nat.Z.INSTANCE;
        }

        public static <N extends SizedIterable.Nat, SN extends SizedIterable.Nat.S<N>> SN s(N n) {
            return null;
        }

        public static interface Z extends SizedIterable.Nat {
            Z INSTANCE = new Z() {};
        }

        public static interface S<N extends SizedIterable.Nat> extends SizedIterable.Nat {

        }

    }

    private final Iterable<A> as;
    private final N           n;

    private SizedIterable(Iterable<A> as, N n) {
        this.as = as;
        this.n = n;
    }

    @Override
    public Iterator<A> iterator() {
        return as.iterator();
    }

    public static <A> SizedIterable<A, SizedIterable.Nat.Z> empty() {
        return new SizedIterable<>(emptyList(), z());
    }

    public <SN extends SizedIterable.Nat.S<N>> SizedIterable<A, SN> cons(A a) {
        return new SizedIterable<>(Cons.cons(a, as), s(n));
    }

    public <SN extends SizedIterable.Nat.S<? extends N>> SizedIterable<A, SN> snoc(A a) {
        return new SizedIterable<>(Snoc.snoc(a, as), (SN) s(n));
    }

    public static <A, One extends SizedIterable.Nat.S<SizedIterable.Nat.Z>> SizedIterable<A, One> of(A a) {
        return SizedIterable.<A>empty().cons(a);
    }

    public static <A, One extends SizedIterable.Nat.S<SizedIterable.Nat.Z>, Two extends SizedIterable.Nat.S<One>> SizedIterable<A, Two> of(A a, A b) {
        return SizedIterable.<A, One>of(a).snoc(b);
    }

    public static <A, One extends SizedIterable.Nat.S<SizedIterable.Nat.Z>, Two extends SizedIterable.Nat.S<One>, Three extends SizedIterable.Nat.S<Two>> SizedIterable<A, Three> of(A a, A b, A c) {
        return SizedIterable.<A, One, Two>of(a, b).snoc(c);
    }

    public static <A, One extends SizedIterable.Nat.S<SizedIterable.Nat.Z>, Two extends SizedIterable.Nat.S<One>, Three extends SizedIterable.Nat.S<Two>, Four extends SizedIterable.Nat.S<Three>> SizedIterable<A, Four> of(A a, A b, A c, A d) {
        return SizedIterable.<A, One, Two, Three>of(a, b, c).snoc(d);
    }

    public static <A, One extends SizedIterable.Nat.S<SizedIterable.Nat.Z>, Two extends SizedIterable.Nat.S<One>, Three extends SizedIterable.Nat.S<Two>, Four extends SizedIterable.Nat.S<Three>, Five extends SizedIterable.Nat.S<Four>> SizedIterable<A, Five> of(A a, A b, A c, A d, A e) {
        return SizedIterable.<A, One, Two, Three, Four>of(a, b, c, d).snoc(e);
    }
}