auto-ffi for java classes / object model

[jjl]

i'm currently looking at reflection. i've knocked up a little bit of clojure with a library i wrote a few years ago tnat inspects java.lang.reflect and i'm going to attempt to generate idris bindings for the contents of it, which ought to be a good start at bootstrapping everything else from within idris.

i'm not entirely sure how field access works, but i think i've got a handle on how you're dealing with objects and inheritance.

the plan is ultimately to be able to generate fairly raw bindings to standard java library classes from within idris itself, calling into the java standard library to do all the reflection. eventually maybe we could have some sort of elaborator reflection or something for it possibly (in idris 1 i suppose it would have been type providers, but they're gone and Elab doesn't appear to have a way to run IO actions). even before this, it raises some questions, however...

• type parameters? they don't really exist in the jvm, just in java, but there's also a reason they're there. perhaps they belong in a slightly higher level binding?
• varargs?
• primitive arrays (varargs?)
• probably more things i haven't worked out yet

[mmhelloworld]

I've been thinking about this feature as well for Idris 2. Idris 1 JVM backend had auto FFI bindings using type providers. We can't use type providers anymore but we can generate Idris code as you mentioned. I did something similar for Frege too.

Type parameters can be supported (Example). Varargs, primitive arrays and passing Java lambdas are not yet supported in the JVM backend so they need to be added later for auto FFI