Not as exciting as it sounds. I plan on using this to make a Scala or Idris project.
Both J and Agda are obscure functional languages. J introduced to the world the concept of "function rank", which allows you to specify function application over arbitrary subcollections of regular collections. Sadly, J is dynamically typed (and also hard to read - it's called a ``write-only'' language). Fully capturing the kinds of shape transformations going on requires a dependently typed programming language.