Welcome to Idris JVM’s documentation!
Idris 2 is a purely functional programming language with first class types. Idris JVM compiles Idris programs to JVM bytecode enabling Idris programs to be run on the JVM. Idris JVM backend is written in Idris and compiled with JVM backend so the compiler itself is self hosting and runs on Java 8 or above.
Overview
Idris JVM compiles Idris programs into Java 8 bytecode. The compiler is self hosting so the compiler itself is written in Idris and runs on the JVM.
Install
Download the latest Idris 2 JVM release from releases page.
Extract the archive and add
idris2launcher script directory<EXTRACTED_DIRECTORY_ROOT>/exectoPATH.Create an environment variable
IDRIS2_PREFIXpointing to<EXTRACTED_DIRECTORY_ROOT>/env
Hello World
module Main
data Tree a = Leaf
| Node (Tree a) a (Tree a)
inorder : Tree a -> List a
inorder Leaf = []
inorder (Node left a right) = inorder left ++ [a] ++ inorder right
tree : Tree String
tree = Node
(Node
(Node Leaf "3" Leaf)
"+"
(Node Leaf "7" Leaf))
"/"
(Node Leaf "2" Leaf)
main : IO ()
main = printLn $ inorder tree
Compile
idris2 helloworld.idr -o main
Run
% build/exec/main
["3", "+", "7", "/", "2"]
Idris basic types are mapped to Java types. Idris modules and functions are compiled into Java classes and static methods respectively.
Idris
JVM
Int8, Int16, Int32, Int, Bits8, Bits16, Bits32, Bool
int
Int64, Bits64
long
Double
double
Nat, Integer
BigInteger
Char
char
String
String
Module, Namespace
Class
Function
Static methods
Lambda
Java 8 lambda -
invokedynamictargetingFunctioninterfaceNil arity function
Memoized lambda
Tail recursion is eliminated using JVM’s
GOTO(whileloop equivalent in Java). For the following code,sum 50000wouldn’t overflow the stack. See Tail Call Optimization for more details.
sum : Nat -> Nat
sum n = go 0 n where
go : Nat -> Nat -> Nat
go acc Z = acc
go acc n@(S k) = go (acc + n) k
Non-recursive tail calls are handled using trampolines. For the following code,
isOdd 100000wouldn’t overflow the stack. See Tail Call Optimization for more details.
mutual
isEven : Nat -> Bool
isEven Z = True
isEven (S k) = isOdd k
isOdd : Nat -> Bool
isOdd Z = False
isOdd (S k) = isEven k
FFI - Calling Java from Idris: From Idris, invoking Java static methods, instance methods, constructors are all supported. An example is shown below. See Calling Java from Idris for more details.
%foreign "jvm:toBinaryString(int java/lang/String),java/lang/Integer"
intToBinaryString : Int -> String
main : IO ()
main = printLn $ intToBinaryString 128
FFI - Calling Idris from Java - This is currently in progress.
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.
Tail Call Optimization
Idris JVM backend optimizes tail recursion, both self and mutual tail calls. Self tail calls are eliminated using JVM’s
GOTO and mutual tail calls are eliminated using trampolines. Here we will see examples for each of those cases and
how they are compiled into JVM bytecode.
Self tail recursion
This example demonstrates self tail recursion in go function. This program wouldn’t overflow the stack if it is
called with large values like 50000 as the recursive call would be essentially turned into a loop in the bytecode.
sum : Nat -> Nat
sum n = go 0 n where
go : Nat -> Nat -> Nat
go acc Z = acc
go acc n@(S k) = go (acc + n) k
main : IO ()
main = printLn (sum 50000)
Bytecode
The following bytecode shows how this is compiled into. In the bytecode, the function call in tail position would be
replaced with GOTO so the function doesn’t call itself instead it transfers the control back to the beginning of
the function with updated argument values for next iteration as shown in the last five lines of the bytecode.
public static java.lang.Object $n2810$7795$go(java.lang.Object, java.lang.Object, java.lang.Object);
Code:
0: aload_2
1: checkcast #71 // class java/math/BigInteger
4: astore_3
5: iconst_m1
6: istore 4
8: aload_3
9: invokevirtual #241 // Method java/math/BigInteger.hashCode:()I
12: lookupswitch { // 1
0: 32
default: 48
}
32: aload_3
33: getstatic #234 // Field java/math/BigInteger.ZERO:Ljava/math/BigInteger;
36: invokevirtual #245 // Method java/math/BigInteger.equals:(Ljava/lang/Object;)Z
39: ifeq 48
42: iconst_0
43: istore 4
45: goto 48
48: iload 4
50: lookupswitch { // 1
0: 68
default: 70
}
68: aload_1
69: areturn
70: aload_2
71: checkcast #71 // class java/math/BigInteger
74: getstatic #248 // Field java/math/BigInteger.ONE:Ljava/math/BigInteger;
77: invokevirtual #252 // Method java/math/BigInteger.subtract:(Ljava/math/BigInteger;)Ljava/math/BigInteger;
80: astore 5
82: aload_1
83: checkcast #71 // class java/math/BigInteger
86: aload_2
87: checkcast #71 // class java/math/BigInteger
90: invokevirtual #255 // Method java/math/BigInteger.add:(Ljava/math/BigInteger;)Ljava/math/BigInteger;
93: astore 6
95: aload 5
97: astore 7
99: aload 6
101: astore_1
102: aload 7
104: astore_2
105: goto 0
Decompiled Java code
The decompiled Java code below shows bit more clearly that the recursive call is eliminated with a loop in the last default block.
public static Object $n2810$7795$go(Object arg$0, Object arg$1, Object arg$2) {
while(true) {
BigInteger constantCaseExpr0 = (BigInteger)arg$2;
int hashCodePosition1 = -1;
switch (constantCaseExpr0.hashCode()) {
case 0:
if (constantCaseExpr0.equals(BigInteger.ZERO)) {
hashCodePosition1 = 0;
}
default:
switch (hashCodePosition1) {
case 0:
return arg$1;
default:
Object e$0 = ((BigInteger)arg$2).subtract(BigInteger.ONE);
BigInteger tailRecArg2 = ((BigInteger)arg$1).add((BigInteger)arg$2);
arg$1 = tailRecArg2;
arg$2 = e$0;
}
}
}
}
Mutual tail recursion
The example below shows two functions isEven and isOdd calling each other. This is compiled using trampolines
where the actual function calls are replaced with constructor TcContinue and the result is returned in TcDone.
The constructor TcContinue will have an index indicating which function to call and the arguments for
the function. There will be a top-level function in Idris JVM runtime called tailRec which iterates as long as
TcContinue object is returned and returns the result when it gets a TcDone object.
This basically ensures that the functions don’t call each other and we trade off the heap for the stack to hold the
function arguments. This works for any number of functions, not just two, calling each other in tail position.
mutual
isEven : Nat -> Bool
isEven Z = True
isEven (S k) = isOdd k
isOdd : Nat -> Bool
isOdd Z = False
isOdd (S k) = isEven k
Decompiled Java code
In the decompiled code below, the Idris top-level function isOdd simply calls the runtime function tailRec that
iterates between mutually recursive functions. $tcOpt$1 determines which tail-call optimized function to call based
on the TcContinue constructor id, and the function is passed to tailRec which keeps on calling this function until
it encounters TcDone. isEven$tc1 and isOdd$tc2 are the tail-call optimized versions of respective Idris
functions where the recursive call is replaced with TcContinue and the result is returned in TcDone.
public static Object isOdd(Object arg$0) {
return Runtime.tailRec(Main::$tcOpt$1, new TcContinue_1(2, arg$0));
}
public static Object $tcOpt$1(Object $a$0) {
Object $a$0 = (IdrisObject)$a$0;
Object arg$0;
switch ($a$0.getConstructorId()) {
case 1:
arg$0 = ((IdrisObject)$a$0).getProperty(0);
return isEven$tc1(arg$0);
case 2:
arg$0 = ((IdrisObject)$a$0).getProperty(0);
return isOdd$tc2(arg$0);
default:
return null;
}
}
public static Object isEven$tc1(Object arg$0) {
BigInteger constantCaseExpr0 = (BigInteger)arg$0;
int hashCodePosition1 = -1;
switch (constantCaseExpr0.hashCode()) {
case 0:
if (constantCaseExpr0.equals(BigInteger.ZERO)) {
hashCodePosition1 = 0;
}
default:
switch (hashCodePosition1) {
case 0:
return new TcDone(0, 1);
default:
Object e$0 = ((BigInteger)arg$0).subtract(BigInteger.ONE);
return new TcContinue_1(2, e$0);
}
}
}
public static Object isOdd$tc2(Object arg$0) {
BigInteger constantCaseExpr0 = (BigInteger)arg$0;
int hashCodePosition1 = -1;
switch (constantCaseExpr0.hashCode()) {
case 0:
if (constantCaseExpr0.equals(BigInteger.ZERO)) {
hashCodePosition1 = 0;
}
default:
switch (hashCodePosition1) {
case 0:
return new TcDone(0, 0);
default:
Object e$0 = ((BigInteger)arg$0).subtract(BigInteger.ONE);
return new TcContinue_1(1, e$0);
}
}
}
Functions can be both self and mutually tail recursive
A function can be both self and mutually tail recursive and both of the optimizations shown above would be applied in that case.
Consider this Idris function, for example, where it calls itself as well as another function which calls back:
mutual
isEven : Nat -> Bool
isEven Z = True
isEven (S k) = isOdd k
isOdd : Nat -> Bool
isOdd Z = False
isOdd (S (S k)) = isOdd k
isOdd (S k) = isEven k
Decompiled Java code
The JVM bytecode for this function will have a loop and trampoline as we can see in the following decompiled code. Here the last default block has TcContinue constructor in one branch and overwrites argument value in the other branch for next iteration.
public static Object isOdd$tc2(Object arg$0) {
while(true) {
BigInteger constantCaseExpr0 = (BigInteger)arg$0;
int hashCodePosition1 = -1;
switch (constantCaseExpr0.hashCode()) {
case 0:
if (constantCaseExpr0.equals(BigInteger.ZERO)) {
hashCodePosition1 = 0;
}
default:
switch (hashCodePosition1) {
case 0:
return new TcDone(0, 0);
default:
Object e$0 = ((BigInteger)arg$0).subtract(BigInteger.ONE);
BigInteger constantCaseExpr2 = (BigInteger)e$0;
int hashCodePosition3 = -1;
switch (constantCaseExpr2.hashCode()) {
case 0:
if (constantCaseExpr2.equals(BigInteger.ZERO)) {
hashCodePosition3 = 0;
}
default:
switch (hashCodePosition3) {
case 0:
return new TcContinue_1(1, e$0);
default:
Object e$1 = ((BigInteger)e$0).subtract(BigInteger.ONE);
arg$0 = e$1;
}
}
}
}
}
}