Calling Idris from Java

Exporting Idris Functions

%export """
    jvm:public static replicate
    {
        "enclosingType": "idris/String",
        "arguments": [{"type": "BigInteger"}, {"type": "char"}],
        "returnType": "String"
    }
    """
exportStringReplicate : Nat -> Char -> String
exportStringReplicate = String.replicate

This code exports replicate function from Data.String Idris module. The export block starting with %export needs to specify which Java class the function should belong to, argument types and return type. As Idris Nat maps to Java’s BigInteger in the JVM bytecote, first argument type is BigInteger.

This is how it looks in the Java code:

import static java.math.BigInteger.TEN;

public class Main {

    public static void main(String[] args) {
        System.out.println(idris.String.replicate(TEN, 'A'));
    }

}

The code prints AAAAAAAAAA as expected.

JVM Import Aliases

In the example above, we need to specify types in the export block in a few places like enclosingType, arguments and returnType. Annotations would be another place which we will cover later. If we are exporting multiple Idris functions, we don’t want to repeat the types everywhere. We can use import aliases to avoid repeating the fully qualified names of types.

%export
    """
    jvm:import
    idris/data/List IdrisList
    idris/data/Maybe IdrisMaybe
    idris/prelude/Show
    """
jvmImports : List String
jvmImports = []

The export block defines three imports and aliases. The Idris function that defines the export block name must be named jvmImports. With this, the export functions can simply use IdrisList, IdrisMaybe and Show instead of fully qualified exported Java names. Note that the last import idris/prelude/Show doesn’t provide an explicit alias but the last part of qualified name would implicitly serve as alias.

These imports can be used with any export functions defined in the current namespace and any descendant namespaces. For example, if helloworld.foo defines this export block, all the functions in helloworld.foo and helloworld.foo.bar namespaces can use the aliases.

Export Idris Types

To be able to export functions with Idris types, Idris types need to be exported as well. This is necessary so that we don’t depend on compiler generated interal types in Java. Another reason is that Idris compiler optimizes certain types. For example, data Color = Red | Green doesn’t have a Color type at runtime. Instead Red and Green are just integers which Java code shouldn’t rely on.

%export
    """
    jvm:export
    idris/data/List
    helloworld/Color
    """
typeExports : List String
typeExports = []

Similar to jvmExports block explained above, typeExports is a special export function that exports Idris types to Java. The function must be named typeExports. These exported types can then be used in other exported functions in current namespace as well as any descendant namespaces similar to jvmImports.

Exporting Idris functions with Generic Types

%export
    """
    jvm:import
    idris/data/List IdrisList
    """
jvmImports : List String
jvmImports = []

%export
    """
    jvm:export
    IdrisList
    """
typeExports : List String
typeExports = []

%export """
    jvm:public static nil
    {
        "enclosingType": "IdrisList",
        "returnType": "IdrisList"
    }
    """
idrisNil : List a
idrisNil = []

%export """
    jvm:public static cons
    {
        "enclosingType": "IdrisList",
        "arguments": [{"type": "Object"}, {"type": "IdrisList"}],
        "returnType": "IdrisList"
    }
    """
idrisCons : a -> List a -> List a
idrisCons = (::)

Here we are exporting Idris’s [] and :: functions from List module. The code also exports List type itself under class idris/data/List for Java using typeExports function. Also note that the exported functions and exported types make use of import alias IdrisList through jvmImports.

This is how we use the functions in Java:

import idris.data.List;

import static idris.data.List.cons;
import static idris.data.List.nil;

public class Main {

    public static void main(String[] args) {
        List idrisIntList = cons(23, cons(45, nil()));
        System.out.println(idrisIntList);
    }

}

The code prints something like idris.data.List@506e1b77 as we don’t have toString method defined. We will see next how we can use Idris Show interface to print Idris List for different element types.

Exporting Idris functions with type class instances

Idris type class instances can be exported to Java. This will be useful to call Idris functions that require implicit values of type class instances. The type class parameters will be passed explicitly from Java.

%export """
    jvm:public static show
    {
        "enclosingType": "idris/Int",
        "returnType": "Show"
    }
    """
showInt : Show Int
showInt = %search

Here we are returning the Show instance for Int type. Similarly we can return type class instances that require other type class instances as well. For example, Show instance for List a needs Show instance for a.

%export """
    jvm:public static show
    {
        "enclosingType": "IdrisList",
        "arguments": [{"type": "Show"}],
        "returnType": "Show"
    }
    """
exportShowList : Show a => Show (List a)
exportShowList = %search

Now we can export the show function to Java and pass the type class instances to print Idris List Int.

%export """
    jvm:public static show
    {
        "enclosingType": "Show",
        "arguments": [{"type": "Show"}, {"type": "Object"}],
        "returnType": "String"
    }
    """
exportShow : Show a => a -> String
exportShow = show

Here is a complete example in Idris and Java:

module Main

import Data.String
import Data.List

%export
    """
    jvm:import
    idris/String IdrisString
    idris/data/List IdrisList
    idris/data/Maybe IdrisMaybe
    idris/prelude/Show
    helloworld/Color
    """
jvmImports : List String
jvmImports = []

%export
    """
    jvm:export
    IdrisList
    IdrisMaybe
    Show
    Color
    """
typeExports : List String
typeExports = []

%export """
    jvm:public static nil
    {
        "enclosingType": "IdrisList",
        "returnType": "IdrisList"
    }
    """
idrisNil : List a
idrisNil = []

%export """
    jvm:public static cons
    {
        "enclosingType": "IdrisList",
        "arguments": [{"type": "Object"}, {"type": "IdrisList"}],
        "returnType": "IdrisList"
    }
    """
idrisCons : a -> List a -> List a
idrisCons = (::)

%export """
    jvm:public static show
    {
        "enclosingType": "idris/Int",
        "returnType": "Show"
    }
    """
showInt : Show Int
showInt = %search

%export """
    jvm:public static show
    {
        "enclosingType": "IdrisString",
        "returnType": "Show"
    }
    """
showString : Show String
showString = %search

data Color = Red | Green | Blue

Show Color where
    show Red = "Red"
    show Green = "Green"
    show Blue = "Blue"

%export """
    jvm:public static red
    {
        "enclosingType": "Color",
        "returnType": "Color"
    }
    """
red : Color
red = Red

%export """
    jvm:public static green
    {
        "enclosingType": "Color",
        "returnType": "Color"
    }
    """
green : Color
green = Green

%export """
    jvm:public static blue
    {
        "enclosingType": "Color",
        "returnType": "Color"
    }
    """
blue : Color
blue = Blue

%export """
    jvm:public static show
    {
        "enclosingType": "Color",
        "returnType": "Show"
    }
    """
exportShowColor : Show Color
exportShowColor = %search

%export """
    jvm:public static show
    {
        "enclosingType": "Color",
        "arguments": [{"type": "Color"}],
        "returnType": "String"
    }
    """
showColor : Color -> String
showColor = show

%export """
    jvm:public static show
    {
        "enclosingType": "IdrisList",
        "arguments": [{"type": "Show"}],
        "returnType": "Show"
    }
    """
exportShowList : Show a => Show (List a)
exportShowList = %search

%export """
    jvm:public static just
    {
        "enclosingType": "IdrisMaybe",
        "arguments": [{"type": "Object"}],
        "returnType": "IdrisMaybe"
    }
    """
exportJust : a -> Maybe a
exportJust = Just

%export """
    jvm:public static nothing
    {
        "enclosingType": "IdrisMaybe",
        "returnType": "IdrisMaybe"
    }
    """
exportNothing : Maybe a
exportNothing = Nothing

%export """
    jvm:public static show
    {
        "enclosingType": "IdrisMaybe",
        "arguments": [{"type": "Show"}],
        "returnType": "Show"
    }
    """
exportShowMaybe : Show a => Show (Maybe a)
exportShowMaybe = %search

%export """
    jvm:public static show
    {
        "enclosingType": "Show",
        "arguments": [{"type": "Show"}, {"type": "Object"}],
        "returnType": "String"
    }
    """
exportShow : Show a => a -> String
exportShow = show

%export """
    jvm:public static replicate
    {
        "enclosingType": "IdrisString",
        "arguments": [{"type": "BigInteger"}, {"type": "char"}],
        "returnType": "String"
    }
    """
exportStringReplicate : Nat -> Char -> String
exportStringReplicate = String.replicate

main : IO ()
main = pure ()

Java calling the Idris functions:

 1 package hello;
 2
 3 import helloworld.Color;
 4 import idris.Int;
 5 import idris.data.List;
 6 import idris.data.Maybe;
 7 import idris.prelude.Show;
 8
 9 import static helloworld.Color.blue;
10 import static helloworld.Color.green;
11 import static helloworld.Color.red;
12 import static idris.data.List.cons;
13 import static idris.data.List.nil;
14 import static idris.data.Maybe.just;
15 import static idris.data.Maybe.nothing;
16 import static idris.prelude.Show.show;
17 import static java.math.BigInteger.TEN;
18
19 public class Main {
20
21     public static void main(String[] args) {
22         List idrisIntList = cons(23, cons(45, nil())); // Create an Idris list of integers
23         List idrisStringList = cons("foo", cons("bar", nil()));
24
25         // Create an Idris list of Colors defined as data Color = Red | Green | Blue
26         List idrisColorList = cons(red().toIdris(), cons(blue().toIdris(), nil()));
27
28         // Get Show instance for Idris List given a show Instance of Int
29         Show intListShow = List.show(Int.show());
30         Show stringListShow = List.show(idris.String.show());
31         Show colorShow = Color.show();
32         Show colorListShow = List.show(colorShow);
33         Show colorMaybeShow = Maybe.show(colorShow);
34
35         System.out.println(show(intListShow, idrisIntList.toIdris()));
36         System.out.println(show(stringListShow, idrisStringList.toIdris()));
37         System.out.println(show(colorListShow, idrisColorList.toIdris()));
38
39         System.out.println(show(colorShow, green().toIdris()));
40         System.out.println(Color.show(blue()));
41
42         System.out.println(show(colorMaybeShow, just(green().toIdris()).toIdris()));
43         System.out.println(show(colorMaybeShow, nothing().toIdris()));
44         System.out.println(idris.String.replicate(TEN, 'A'));
45     }
46
47 }

This is the output:

[23, 45]
["foo", "bar"]
[Red, Blue]
Green
Blue
Just Green
Nothing
AAAAAAAAAA

Here line numbers 29-33 retrieve type class instances for different types and the instances are passed in the lines below when show function is called. Another thing to note here is that when we call generic Idris functions, Idris types that are wrapped in Java types needs to be converted before passing to Idris functions. For example, line 23 passes String values directly but line 26 passes Color values after calling toIdris to generic cons function. Same logic applies at line 35 while passing idris.data.List to show. If the function type is monomorphic, we don’t need to explicitly convert. For example, line 40 passes blue() directly to monomorphic Color.show.

Exporting Idris Types and Functions with Java Annotations

Idris types and functions can be exported to Java with annotations which will help integrate with some Java frameworks such as Spring Boot.

 1%export
 2    """
 3    jvm:import
 4    org/springframework/web/bind/annotation/GetMapping Get
 5    org/springframework/web/bind/annotation/PostMapping Post
 6    io/github/mmhelloworld/helloworld/Employee
 7    io/github/mmhelloworld/helloworld/EmployeeController
 8    io/github/mmhelloworld/helloworld/EmployeeRepository
 9    io/github/mmhelloworld/helloworld/PayrollConfiguration
10    io/github/mmhelloworld/helloworld/PayrollApplication
11    org/springframework/context/annotation/Configuration
12    org/springframework/web/bind/annotation/RestController
13    org/springframework/web/bind/annotation/RequestBody
14    org/springframework/boot/CommandLineRunner
15    org/springframework/boot/SpringApplication
16    org/springframework/boot/autoconfigure/SpringBootApplication
17    org/springframework/context/annotation/Bean
18    org/springframework/stereotype/Component
19    java/util/List
20    """
21jvmImports : List String
22jvmImports = []
23
24-- Spring boot controller that defines REST endpoints
25namespace EmployeeController
26
27    %export """
28            jvm:public EmployeeController
29            {
30                "annotations": [
31                    {"NoArgsConstructor": {}},
32                    {"RestController": {}}
33                ]
34            }
35            """
36    public export
37    EmployeeController : Type
38    EmployeeController = Struct "io/github/mmhelloworld/helloworld/EmployeeController" []
39
40    -- GET endpoint to retrieve all the employees
41    %export """
42         jvm:public getEmployees
43         {
44             "annotations": [
45                 {"Get": ["/employees"]}
46             ],
47             "enclosingType": "EmployeeController",
48              "arguments": [
49                  {
50                      "type": "EmployeeController"
51                  }
52              ],
53              "returnType": "List<Employee>"
54         }
55     """
56    employees : EmployeeController -> PrimIO (JList Employee)
57    employees _ = toPrim $ run getEmployees
58
59    -- POST endpoint to save an employee given a JSON payload
60    %export """
61         jvm:public saveEmployee
62         {
63             "annotations": [
64                 {"Post": ["/employee"]}
65             ],
66             "enclosingType": "EmployeeController",
67             "arguments": [
68                 {
69                     "type": "EmployeeController"
70                 },
71                 {
72                     "type": "Employee",
73                     "annotations": [
74                        {"RequestBody": {}}
75                     ]
76                 }
77             ],
78             "returnType": "Employee"
79         }
80     """
81    saveEmployee : EmployeeController -> Employee -> PrimIO Employee
82    saveEmployee _ employee = toPrim $ run (PayrollApp.saveEmployee employee)

The above code exports a Spring Boot controller with @RestController annotation and two REST endpoint functions annotated with @GetMapping and @PostMapping allowing to retrieve all employees and save an employee respectively. Also note that line 73 provides an annotation to the second function parameter allowing the Idris function to receive a POST body mapping to Employee JSON. See here for a complete Spring Boot example written completely in Idris.