Skip to content

Instantly share code, notes, and snippets.

What would you like to do?
Dependently-typed Iterable
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')
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) { = as;
this.n = n;
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);
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment