Calling Java from Idris

Calling static methods

import System.FFI

%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

import System.FFI

%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 System.FFI
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.

Accessing fields

import System.FFI

data Point : Type where [external]

-- Get an instance field
%foreign "jvm:#x(java/awt/Point int),java/awt/Point"
prim_getX : Point -> PrimIO Int

-- Set an instance field
%foreign "jvm:#=x(java/awt/Point int void),java/awt/Point"
prim_setX : Point -> Int -> PrimIO ()

-- Get a static field
%foreign "jvm:#MAX_VALUE(int),java/lang/Integer"
intMax : Int

-- Set a static field
%foreign "jvm:#=bar(java/lang/String void),io/github/mmhelloworld/helloworld/Main"
prim_setBar : String -> PrimIO ()

Field foreign specifiers start with #. To mutate fields, foreign specifier starts with #=. Instance field accessors will have an additional parameter to pass the instance.

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.

Class literals

classLiteral function can be used to get Java’s Class instances for JVM types.

Main> :module Java.Lang
Imported module Java.Lang
Main> :t classLiteral
Java.Lang.classLiteral : Class ty

import Java.Lang

main : IO ()
main = do
  printLn !(Object.toString $ classLiteral {ty=Int})
  printLn !(Object.toString $ classLiteral {ty=Integer})
  printLn !(Object.toString $ classLiteral {ty=String})

The above example prints:

"int"
"class java.math.BigInteger"
"class java.lang.String"

JVM reference equality

Reference equality should be avoided in Idris but it might be useful to interface with Java, for example, for overriding equals method in Idris.

Main> :module Java.Lang
Imported module Java.Lang
Main> :exec printLn (jvmRefEq "foo" "foo")
True
Main> :exec printLn (jvmRefEq "foo" ("fo" ++ "o"))
False