I would say that it's not always possible. It's probably "possible" if you put about half the invariant in the type and half the invariant in documentation, of course, but that's a much weaker claim!

Java is in an interesting place in that its type system is rudimentary but not unpowerful. C is a more useful didactic target---there really do exist invariants which can be encoded in Haskell types but could never be encoded in C types!

Another huge target is parametricity. You can write Java code which is "maybe sort of parametric" but it really isn't and subsequently you can never trust it because of the existence of things like global reference equality and hash codes (in the least).

Finally, there are expressivity concerns. Java cannot encode as many things in its type language as something like Agda (to make a clear comparison). You can simply note that Java's type equality is nowhere nearly as developed as Agda's!

As an example of using Java to indicate a fairly non-trivial invariant and comparing that implementation to Scala, Haskell, and C# consider Tony Morris' challenge

http://tonymorris.github.io/blog/posts/understanding-practic...

Thanks for the link. I've been wondering how to lift N-D operations into the type system. If I write with NumPy

  x = r_[:n].reshape((3, -1, n/15))[:, :2].sum(axis=-1)

a compiler could figure out that the shape of x is (3, 2) and allow

  y = x + randn(m, 1, 2)

while forbidding

  z = y - r_[:7]

With NumPy you have to wait for a runtime error, and only if the shapes can't be broadcast. We're not even talking correct use of dimensions, etc.

I suppose this may have been tackled in Haskell in the Repa library, but I'd need to read papers like

http://benl.ouroborus.net/papers/repa/repa-icfp2010.pdf

to know. Hence my question if we could lift this into the type system in a conventional language, but I don't think it's possible in a general way.

I'm not sure what the notation you're using represents, but it looks like you're talking about matrices of a known size. What that's an example of is dependent types, where types can be parameterized by values, and not just types. For example, a (2D) matrix is parameterized by what it contains, and its dimensions. The former is a type but the latter are values. Without dependent types (or some subset of their capability) you can't represent this matrix type; you'd just have to check at runtime that no out-of-bounds access was occurring, so no; I don't think you could put this in a conventional language (without some crazy gymnastics, perhaps involving macros or similar). However, with dependent types, this is absolutely possible to statically guarantee that no out-of-bounds access will occur at runtime.