Dependent Types in Java

No, you generally can’t do dependent types in Java. However, there are some techniques that one can do to get some of the same benefits. The thing with any nominative type system is you can always just put more stuff in the name. It’s klunky and sometimes absurd, but it can work in many cases. Let’s take the classic situation of a List/Vector of a certain size.

Here’s an interface that we’ll have them all use:

package test.list; import fj.F; import fj.F2; public interface List extends Iterable { List map(F f); * List[ fold(F2]() [ f, B init); List]() [ add(A value); } ]()*

Note that there is no way to get a value from the list. That is deliberate. If you don’t know what size the list is, then you don’t know which indexes are safe to use to get an element. So, you can’t.

Fortunately, Java does have first order generic types, so we don’t have to put the type of the elements of the list into the name. But it can’t index on the length, so we do have to put that in the name.

Here’s an example of how one might implement a list of length 2:

package test.list; import java.util.Arrays; import java.util.Iterator; import fj.F; import fj.F2; public class List2implements List { private A v0; private A v1; public List2(A v0, A v1) { this.v0 = v0; this.v1 = v1; } @Override public Iterator iterator() { return Arrays.asList(v0, v1).iterator(); } @Override public List map(F f) { return new List2(f.f(v0), f.f(v1)); } @Override public * B fold(F2[ f, B init) { return f.f(v1, f.f(v0, init)); } @Override public List3]() [ add(A v2) { return new List3]() [(v0, v1, v2); } public A getV0() { return v0; } public A getV1() { return v1; } public void setV0(A newV0) { v0 = newV0; } public void setV1(A newV1) { v0 = newV1; } } ]()*

Some things to note:

  • Note that this is a mutable list. I did that because I think it’s less obvious that one can do a mutable list in this manner. An immutable one would be simpler to implement.
  • If one did this for a significant sized list, one would probably want to use a persistent data structure (PDS) to store the elements.
  • The map and fold implementations could be done in an abstract base class, using a reference to an array or PDS that was assigned in the subclass constructors
  • Element access is direct as methods, or it could be direct field access. You cannot access elements by passing in a numeric index because Java has no way to check at compile time that it is within the bounds of the list.

Some more examples would be useful. If there’s interest, I’ll perhaps do that in a followup post.