Calling Java from Idris
Calling static methods
%foreign "jvm:toBinaryString(int java/lang/String),java/lang/Integer"
intToBinaryString : Int -> String
main : IO ()
main = printLn $ intToBinaryString 128
The foreign specifier starting with jvm:
indicates a JVM function invocation.
There may be other runtime specifiers on the same function which will be ignored by the Idris JVM compiler.
The specifier starts with the static method name and then specifies the argument types and return type.
Last part is the class name. JVM types use /
to separate package parts which is the JVM representation of a class
unlike Java’s .
(dot).
Calling instance methods
%foreign "jvm:.substring(java/lang/String int int java/lang/String),java/lang/String"
substring : String -> Int -> Int -> String
main : IO ()
main = printLn $ substring "foobarbaz" 3 6
This is similar to static method call except that the method name starts with a dot and the type of first argument is the type of instance that the method will be invoked on.
Calling constructors
import Java.Lang
import Java.Util
namespace ArrayList
export
data ArrayList : Type -> Type where [external]
%foreign "jvm:<init>(java/util/ArrayList),java/util/ArrayList"
prim_new : PrimIO (ArrayList a)
export %inline
new : HasIO io => io (ArrayList elemTy)
new = primIO prim_new
main : IO ()
main = do
list <- ArrayList.new
printLn !(toString list)
Foreign specifier for constructors start with <init>
which is the JVM name for constructors.
Similar to method calls, constructors specify argument types and return type. In this case, we invoke a zero-argument
constructor returning java/util/ArrayList.
Inheritance
Idris JVM allows calling methods from interfaces or parent classes through Inherits
interface.
Inherits
interface doesn’t have any functions to implement but is just a marker interface for foreign types.
We already saw an example of inheritance above that calls toString
from Object
class on an ArrayList instance.
Here is a detailed example showing the hierarchy between Java’s Collection
, List
and ArrayList
:
namespace Collection
export
data Collection : Type -> Type where [external]
%foreign "jvm:.add(i:java/util/Collection java/lang/Object Bool),java/util/Collection"
prim_add : Collection a -> a -> PrimIO Bool
%foreign "jvm:.size(i:java/util/Collection int),java/util/Collection"
prim_size : Collection a -> PrimIO Int
export %inline
add : HasIO io => obj -> elemTy -> (Inherits obj (Collection elemTy)) => io Bool
add collection elem = primIO $ prim_add (subtyping collection) elem
export %inline
size : (HasIO io, Inherits obj (Collection elemTy)) => obj -> io Int
size {elemTy} collection = primIO $ prim_size {a=elemTy} (subtyping collection)
namespace JList
export
data JList : Type -> Type where [external]
%foreign "jvm:.get(i:java/util/List int java/lang/Object),java/util/List"
prim_get : JList a -> Int -> PrimIO a
export %inline
get : (HasIO io, Inherits list (JList elemTy)) => list -> Int -> io elemTy
get list index = primIO $ prim_get (subtyping list) index
public export
Inherits (JList a) (Collection a) where
public export
Inherits obj (JList a) => Inherits obj (Collection a) where
namespace ArrayList
export
data ArrayList : Type -> Type where [external]
%foreign "jvm:<init>(java/util/ArrayList),java/util/ArrayList"
prim_new : PrimIO (ArrayList a)
export %inline
new : HasIO io => io (ArrayList elemTy)
new = primIO prim_new
public export
Inherits (ArrayList a) (JList a) where
main : IO ()
main = do
list <- ArrayList.new {elemTy=String}
ignore $ add list "hello"
ignore $ add list "world"
elem <- JList.get {elemTy=String} list 1
printLn elem
printLn !(size {elemTy=String} list)
printLn !(toString list)
Here, we create an ArrayList instance and call get method from List and methods from Collection such as add and size. We are able to pass ArrayList instance to the List and Collection functions because of Inherits interface instances for ArrayList. Another note: In JVM, invoking methods on interface is different from class methods invocation so the foreign specifiers on interface methods have i: prefix for the first parameter that represents the instance that the methods are called on.