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.

  • 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 - invokedynamic targeting Function interface

    Nil arity function

    Memoized lambda

  • Tail recursion is eliminated using JVM’s GOTO (while loop equivalent in Java). For the following code, sum 50000 wouldn’t overflow the stack. See Self tail recursion 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 100000 wouldn’t overflow the stack. See Mutual tail recursion 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 Idris functions can be exported to Java as static functions, instance functions and constructors. Java classes with fields can be created. Java annotations can be generated as well. See Calling Idris from Java for more details.