What fragment of Martin-Löf dependent type theory can be expressed using generic types in Java?

Question

I have recently come to realize that a number of problems I had a few years ago trying to implement various mathematical theories in Java came down to the fact that the typing system in Java is not sufficiently strong to model all of Martin-Löf dependent type theory.

Prior to Java 5 and generics, the only type theory you could do was through classes and interfaces, which give you arbitrary types built out of the ground types int,double,char and so on using product and function types. You can also build recursive types such as Lists, though not in a uniform way.

Using generics, you can do a bit more. You can now define List<T> as a function $$ \DeclareMathOperator{\Type}{Type}\Type\to\Type $$ and so we get higher order types.

This is not the end of the story, though. Using a generics trick, we can model some dependent product types. For example, we can define types of the form $$ \prod_{T\colon\Type}f(T) $$ using the syntax

public interface f<T extends f<T>>
{
  // We can now refer to T as much as we like
  // inside the class.  T has type f<T>.
}

As an example, we can model the basic underlying structure of a monoid (but not the associativity and unitality conditions) using a term of type $$ \prod_{T\colon\Type}T\times (T\to T\to T) $$ (i.e., a set $T$ with a designated unit element and a binary operation on $T$). Using Java generics, we can model this type:

public interface MonoidElement<T extends MonoidElement<T>>
{
  public T unit();

  public T mul(T op1, T op2);
}

However, when we try to model more complicated concepts, the type theory breaks down.

Is there a simple description of the fragment of MLTT corresponding to the types that can be built in the Java typing system?

Answer 1

There are a lot of misconceptions here. To begin, MLTT doesn't have subtypes, so Java is not going to simply be a fragment of it. It does not require dependent types to make either of the types you gave. A dependent type system doesn't need to have a "type" of types (a universe) in general (MLTT does have universes though), nor do you need dependent types to express those types. In a system like the polymorphic lambda calculus/System F, you can say $\forall T.T\times(T\to T\to T)$. Java doesn't have any equivalent to Type. A dependent type without an analog as a polymorphic type would be something like e.g. $\prod_{n:\mathsf{Nat}}\mathsf{Matrix}(n,n+1)$ or $\prod_{b:\mathsf{Bool}}\mathsf{if}\ b\ \mathsf{then}\ \mathsf{Nat}\ \mathsf{else}\ \mathsf{Bool}$.

It makes more sense to consider Java a fragment of System $\text{F}_{<:}$ which is not a dependent type system at all. Even then it is a rather weak fragment of it. There's a variant of System F called System F$\omega$ which supports full type level functions, essentially lambda at the type level (not to be confused with type-lambdas which relate the value and type levels and System F already has). Neither Java nor Haskell can do this. The only type level "functions" either (standard) Haskell or Java can make are compositions of uninterpreted functions. There is no computational behavior at the type level. Java is further restricted because it doesn't have (nor need) a kind system because it lacks higher-kinded types. That is, you can't have a type level "function" with "type" (i.e kind) $(\mathsf{Type}\to\mathsf{Type})\to\mathsf{Type}$ for example. This is why you can't make methods that operate over arbitrary monads in Java. Returning to just System F, System F has arbitrary rank types. This means you can nest $\forall$ as deeply as you like — you can use it freely. Neither Java nor Haskell (without extensions) supports this. I believe both of them can indirectly capture some higher rank types, but neither can express the type of Haskell's $\mathsf{runST}$ which requires extensions and is $\forall a.(\forall s.\mathsf{ST}\ s\ a) \to a$.

So Java is more expressive than the rank-1 types as captured by the Hindley-Milner type system but far less expressive than System $\text{F}_{<:}$. It doesn't support any form of dependent typing. Featherweight Java as introduced in Featherweight Java: A Minimal Core Calculus for Java and GJ by Igarashi, Pierce, and Wadler provides a simplified, idealized calculus specifically geared toward Java. There is almost certainly a paper that directly compares/reduces Featherweight Java to System $\text{F}_{<:}$. The upshot is Java's type system is not even remotely close to the power of MLTT. In terms of the lambda cube, ignoring subtyping, Java would be somewhere on the edge between $\lambda\!\!\to$, the simply typed lambda calculus, and $\lambda2$, System F. MLTT (or specifically the Calculus of Constructions) is $\lambda\text{P}\omega$, the corner opposite of $\lambda\!\!\to$. So describing Java in terms of MLTT would first require ignoring everything that made MLTT different from System F$\omega$ and then ignoring nearly everything that made System F$\omega$ different from System F.