mmhelloworld

Idris JVM 0.7.0 Release

Happy to announce Idris JVM 0.7.0 release! In addition to enabling Idris 0.7.0 features for the JVM backend, this release also includes:

• Exporting Idris functions to Java static methods, instance methods and constructors.
• Exporting Java classes from Idris that can extend other classes and implement Java interfaces.
• Exporting functions and classes with Java annotations including function parameter annotations.
• Exporting type class instances and functions that make use of them to be able to be called from Java.

Documentation with examples that explain calling Idris functions from Java is available here: link.

Here is a complete example in Idris and Java for demonstration:

  module Main

  import Data.String
  import Data.List

  -- Define some import aliases to avoid repeating fully qualified name
  %export
      """
      jvm:import
      idris/String IdrisString
      idris/data/List IdrisList
      idris/data/Maybe IdrisMaybe
      idris/prelude/Show
      helloworld/Color
      """
  jvmImports : List String
  jvmImports = []

  -- Export Idris types to Java
  %export
      """
      jvm:export
      IdrisList
      IdrisMaybe
      Show
      Color
      """
  typeExports : List String
  typeExports = []

  -- Exports Idris List's nil constructor as a static method into generated Java class aliased by `IdrisList`
  %export """
      jvm:public static nil
      {
          "enclosingType": "IdrisList",
          "returnType": "IdrisList"
      }
      """
  idrisNil : List a
  idrisNil = []
  
  -- Exports Idris List's cons constructor as a static method into generated Java class aliased by `IdrisList`
  %export """
      jvm:public static cons
      {
          "enclosingType": "IdrisList",
          "arguments": [{"type": "Object"}, {"type": "IdrisList"}],
          "returnType": "IdrisList"
      }
      """
  idrisCons : a -> List a -> List a
  idrisCons = (::)

 -- Exports the Show typeclass instance for Idris Int type to Java
  %export """
      jvm:public static show
      {
          "enclosingType": "idris/Int",
          "returnType": "Show"
      }
      """
  showInt : Show Int
  showInt = %search

  - Exports the Show typeclass instance for Idris String type to Java
  %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"

  -- Exports Color constructors as static methods to Java under class Color.
  %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

  -- Exports Show typeclass instance to Java for Idris List given its element's Show typeclass instance
  %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:

    package hello;

    import helloworld.Color;
    import idris.Int;
    import idris.data.List;
    import idris.data.Maybe;
    import idris.prelude.Show;

    import static helloworld.Color.blue;
    import static helloworld.Color.green;
    import static helloworld.Color.red;
    import static idris.data.List.cons;
    import static idris.data.List.nil;
    import static idris.data.Maybe.just;
    import static idris.data.Maybe.nothing;
    import static idris.prelude.Show.show;
    import static java.math.BigInteger.TEN;

    public class Main {

        public static void main(String[] args) {
            List idrisIntList = cons(23, cons(45, nil())); // Create an Idris list of integers
            List idrisStringList = cons("foo", cons("bar", nil()));

            // Create an Idris list of Colors defined as data Color = Red | Green | Blue
            List idrisColorList = cons(red().toIdris(), cons(blue().toIdris(), nil()));

            // Get Show instance for Idris List given a show Instance of Int
            Show intListShow = List.show(Int.show());
            Show stringListShow = List.show(idris.String.show());
            Show colorShow = Color.show();
            Show colorListShow = List.show(colorShow);
            Show colorMaybeShow = Maybe.show(colorShow);

            // Use exported Idris Show instances to print Idris List for differnt element types
            System.out.println(show(intListShow, idrisIntList.toIdris()));
            System.out.println(show(stringListShow, idrisStringList.toIdris()));
            System.out.println(show(colorListShow, idrisColorList.toIdris()));

            System.out.println(show(colorShow, green().toIdris()));
            System.out.println(Color.show(blue()));

            System.out.println(show(colorMaybeShow, just(green().toIdris()).toIdris()));
            System.out.println(show(colorMaybeShow, nothing().toIdris()));
            System.out.println(idris.String.replicate(TEN, 'A'));
        }

    }

Here is the output:

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

With all of these things, we can now write a complete Spring Boot application as well in Idris! Example here.

Exporting Idris functions and types along with foreign function interface thus allows us to integrate Idris much easily into existing Java ecosystem.

Idris 2 Initial Release 0.2.1 for the JVM

There is now an initial version for Idris 2 - 0.2.1 for the JVM. This is compiled from Idris 2 JVM bootstrap version.

Changes:

• Compile initial Idris 2 compiler (0.2.1) with Idris 2 JVM bootstrap version targeting Java 8 bytecode
• Add JVM backend
• Support primitives such as system, IO, network, clock, buffer etc. for JVM backend
• Eliminate tail recursion
• Add debug information such as variable name, file name and line number in bytecode from Idris source
• Compile Idris modules to Java classes at the bytecode level, Idris top level functions to static Java methods and Idris lambdas into Java lambdas with invokedynamic implementing Java Function interface.
• Generate bytecode concurrently for modules
• Generate classes with toString and property getters for Idris constructors
• Infer types to avoid boxing and casting
• Compile Idris list into a Java list
• JVM foreign descriptors supporting static, instance, interface methods and constructor calls

To try it out:

• Unzip idris2-jvm-0.2.1-SNAPSHOT-20210720.zip from here https://github.com/mmhelloworld/Idris2/releases/tag/v0.2.1-SNAPSHOT-20210720
• Add bin directory to PATH variable
• Copy .idris2 directory containing Idris 0.2.1 packages into your home directory.

To compile and run:

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

$ idris2 Main.idr -o main

$ java -jar build/exec/main_app/main.jar
["3", "+", "7", "/", "2"]

Idris 2 Bootstrap Compiler on the JVM with a JVM backend

I am excited to announce that Idris 2 bootstrap compiler can now run on the JVM along with a JVM backend. Here is a REPL session:

$ idris2
     ____    __     _         ___                                           
    /  _/___/ /____(_)____   |__ \                                          
    / // __  / ___/ / ___/   __/ /     Version 0.1.1-786152de1
  _/ // /_/ / /  / (__  )   / __/      https://www.idris-lang.org           
 /___/\__,_/_/  /_/____/   /____/      Type :? for help                     

[BOOTSTRAP VERSION: No longer developed, except as a bootstrapping step.]
Welcome to Idris 2 on the JVM (Private Build OpenJDK 64-Bit Server VM, 1.8.0_275).  Enjoy yourself!
Main> "hello world"
"hello world"
Main> take 10 [25..]
[25, 26, 27, 28, 29, 30, 31, 32, 33, 34]
Main> :t map
Prelude.map : Functor f => (a -> b) -> f a -> f b
Main> :exec printLn "Hello Idris 2 on the JVM - this is printed from executing JVM bytecode from memory"
"Hello Idris 2 on the JVM - this is printed from executing JVM bytecode from memory"
Main> 

You may notice that the banner includes the JVM version that the Idris compiler is running on. Idris 2 for JVM can run on Java 8 or above. Since the compiler itself runs on the JVM, the last :exec command at line 16 above can directly interpret the generated bytecode on the compiler JVM, and the generated bytecode is loaded from memory without any file system footprint.

To try it out

Prerequisite: Java 8 or above

• Extract the zip from here
• Add idris2-boot-jvm/bin from extracted directory to PATH
• Run idris2. That’s all!

Features

• Eliminate tail recursion using JVM’s GOTO
• Trampoline non-self tail calls
• Support file, directory, array, IORef and buffer primitives.
• Analyse function dependencies to generate bytecode for only used functions from main
• Limited type inference on Idris IR to avoid boxing and typecasting in the generated bytecode
• Static and instance Java FFI method calls.
• Debug information (Idris source file and line numbers) in the bytecode from Idris IR

Currently, the goal for this bootstrap compiler is to be able to compile current Idris 2 so the items here could definitely be improved a lot and other features may be added to support the absolute minimum for building Idris 2.

Example

module Main

import System.FFI

-- Tail call is eliminated with GOTO
sum : Int -> Int
sum n = go 0 n where
  go : Int -> Int -> Int
  go acc 0 = acc
  go acc n = go (acc + n) (n - 1)

mutual
  -- Mutually recursive functions are trampolined
  -- keeping it simple with int instead of Nat which is compiled to Java BigInteger
  isOdd : Int -> Bool
  isOdd 0 = False
  isOdd n = isEven (n - 1)

  isEven : Int -> Bool
  isEven 0 = True
  isEven n = isOdd (n - 1)

-- Java instance method calls
%foreign jvm "java/lang/String" ".length"
jvmStringLength : String -> Int

-- Java static method calls
%foreign jvm "java/lang/Integer" "toBinaryString"
intToBinaryString : Int -> String

main : IO ()
main = do
  printLn $ sum 5000
  printLn $ isEven 100000
  printLn $ intToBinaryString 512
  printLn $ jvmStringLength "hello"

Compile

idris2 Main.idr -o main

The classes will be compiled into build/exec/main_app.

$ tree build/exec/main_app/
build/exec/main_app/
├── Main.class
├── Prelude
│   ├── $col$col.class
│   ├── Just.class
│   ├── Nil.class
│   ├── Nothing.class
│   ├── Open.class
│   ├── PrefixMinus.class
│   └── Show$spcat$spcPrelude$dotidr$col1260$col1--1284$col1__mkShow.class
├── Prelude.class
└── PrimIO.class

It compiles down to three main modules Main, Prelude and PrimIO. Rest of the classes are data classes for Idris constructors like Just, Nothing, Nil, :: etc.

Run

$ java -cp /path/to/idris2-boot-jvm/lib/runtime-1.0-SNAPSHOT.jar:build/exec/main_app Main
12502500
True
"1000000000"
5

The above example demonstrates tail recursion, mutual recursion, Java FFI instance and static method calls.

sum a tail recursive function, would be compiled into a loop. Here is the decompiled code for the nested go function inside sum:

    public static Object $nested1201$307$go(Object arg$0, int arg$1, int arg$2) {
        while(true) {
            switch(arg$2) {
            case 0:
                return arg$1;
            default:
                arg$1 = Prelude.++_Num__Int(arg$1, arg$2);
                arg$2 = Prelude.--_Neg__Int(arg$2, 1);
            }
        }
    }

As we can see here, the tail recursive function call is removed in the default block instead the arguments are updated for next iteration. The loop would continue to run until the base case is reached where the result is returned.

For isEven and isOdd, the tail calls would be trampolined using JVM’s invokedynamic. Here is the decompiled bytecode.

    public static Object isOdd(int arg$0) {
        switch(arg$0) {
        case 0:
            return 1;
        default:
            return () -> {
                return Runtime.createThunk(isEven(Prelude.--_Neg__Int(arg$0, 1)));
            };
        }
    }

    public static Object isEven(int arg$0) {
        switch(arg$0) {
        case 0:
            return 0;
        default:
            return () -> {
                return Runtime.createThunk(isOdd(Prelude.--_Neg__Int(arg$0, 1)));
            };
        }
    }

Here since the tail call is not to itself, function call is turned into a thunk which would be eventually unwrapped in a loop.

Now let’s look at FFI calls in the above example. jvmStringLength function is an example for Java FFI instance method call. It calls length function on Java’s java.lang.String instance. Similarly intToBinaryString calls toBinaryString static function on class java.lang.Integer. Function name starting with a dot denotes an instance method call differentiating it from a static method call. Precise types can also be passed explicitly as in the example below with argument types and return type (full code here).

%foreign jvm' fileClass "getLine" fileClass "String"
prim__readLine : FilePtr -> PrimIO (Ptr String)

Next steps

Next step would be to use this bootstrap version to compile current Idris 2 and then porting the JVM backend from here which is on Idris 1 to Idris 2 so there are some interesting things ahead to work on. Meanwhile, if anyone gets a chance to use this boostrap JVM version, please share any feedback or any issues here that can help while we try to compile mainstream Idris 2 for the JVM. Thank you for reading and happy coding!

Idris JVM: Automated FFI with null safety and exception handling

Background

Idris JVM backend has supported foreign function calls for some time now. For example, to invoke parseInt method on java.lang.Integer class,

invokeStatic (Class "java/lang/Integer") "parseInt" (String -> JVM_IO Int) "234" 

Here since the Idris compiler doesn’t know anything about Java’s Integer class or its parseInt method, we have to explicitly provide the function signature. The function call also has the explicit Class before java/lang/Integer and the type of invocation invokeStatic.

Since we are targeting JVM bytecode, JVM has to know whether a method call is a static method call or an interface method call or a virtual method call. It would be nice if we don’t have to worry about any of these things and just call a FFI function with a class name, method name and the arguments. This is the motivation behind this new feature along with some other nice things like null safety, construtor and method overloading resolution and exception handling.

Maybe and Either in foreign function calls

Maybe type and Either type can be used in foreign function calls for null safety and exception handling. Maybe type can be used for argument types and return types. Maybe type used in an argument position will pass null to the target foreign function if it is Nothing or the actual value if it is Just. Similarly, Maybe type used for return type will convert null returned from foreign function into Nothing and the non-null value into Just. At the bytecode level, Maybe wrapper doesn’t exist. It gets compiled down to null or the actual value.

Either type can only be used in return types to indicate whether the foreign function can throw exceptions. At runtime, if the foreign function throws exception, it will be captured in the “left” of type Throwable or if the foreign function completes normally, the result will be stored in the “right” of result type. There are functions try and catch to handle exceptions which we will see later in the post.

How it works

Before we look at some examples, first let’s declare some class names as we are going to use them in multiple places and we don’t want to duplicate.

stringClass: String
stringClass = "java/lang/String"

listInterface: String
listInterface = "java/util/List"

arrayListClass: String
arrayListClass = "java/util/ArrayList"

collectionInterface : String
collectionInterface = "java/util/Collection"

systemClass: String
systemClass = "java/lang/System"

comparatorClass : String
comparatorClass = "java/util/Comparator"

pointClass : String
pointClass = "java/awt/Point"

collectionsClass : String
collectionsClass = "java/util/Collections"

stringBuilderClass : String
stringBuilderClass = "java/lang/StringBuilder"

objectsClass : String
objectsClass = "java/util/Objects"

integerClass : String
integerClass = "java/lang/Integer"

And “import” some methods:

jdkimport [
    (systemClass, ["getProperty", "setProperty"]),
    (stringClass, ["substring", "CASE_INSENSITIVE_ORDER", "valueOf"]),
    (integerClass, ["parseInt"]),
    (comparatorClass, ["compare"]),
    (arrayListClass, ["<init>", "add"]),
    (listInterface, ["get"]),
    (collectionsClass, ["max"]),
    (stringBuilderClass, ["<init>", "toString"]),
    (objectsClass, ["toString"]),
    (pointClass, ["<init>", "x"])
  ]

Here jdkimport is just an additional syntax created using Idris syntax extensions. It just calls a type provider function written in Idris to know about these classes, methods and fields. Note that it imports fields such as CASE_INSENSITIVE_ORDER, x and also constructors in the name of <init> which is the JVM internal name for constructors. The jdkimport syntax launches a JVM during compilation without any classpath so it basically can import all the JDK classes and methods.

There is also another syntax called jvmimport that can take an additional argument, a command, which could be just the JVM with correct classpath or could be a build tool that properly sets up the classpath from your project dependencies so that we can “import” classes and methods from external foreign libraries.

Once the information about JVM classes and methods is collected using type provider, appropriate call site, Idris code similar to the one in the beginning of the post can be created using Idris elaborator reflection with just class name and member name from the user. As a user, we don’t have to know much about these internals, we just need to import classes and members and can use them without having to explicitly provide foreign types. Now let’s look at some examples on how we can actually make FFI calls in the new way.

Examples

1. Safe static method call

main : JVM_IO ()
main = do
  exceptionOrInt <- (integerClass <.> "parseInt") "1234"
  printLn $ either (const 0) id exceptionOrInt 

Here the type of (integerClass <.> "parseInt") is String -> JVM_IO (Either Throwable Int). Since the method can throw exceptions, it returns an Either. Here we return 0 in case of an exception. Later in the post, we will see a detailed example of exception handling. As the method returns an Int which is a primitive type in JVM, it cannot be null and the FFI call already knows that hence the result Int is not wrapped in a Maybe. We don’t provide any explicit type signature for the foreign function. If we try to pass anything other than String for this foreign function, it will be a compilation error!

2. Unsafe static method call

  do
    number <- (integerClass <.!> "parseInt") "23"
    printLn number

Here we use <.!> with an ! to indicate an unsafe method call instead of <.>. There is also javaUnsafe and java if you prefer names to operators. The type of (integerClass <.!> "parseInt") is String -> JVM_IO Int. Sometimes if we are sure that the foreign function would not return null or throw exceptions, we can use unsafe method calls but as the name indicates, it would fail at runtime if null is returned or an exception is thrown.

3. Overloading resolution

We can pick which overloaded variant we want to use by passing appropriate types to the foreign function and the FFI call will automatically have corresponding types.

printLn !((stringClass <.!> "valueOf(double)") 2.5)
printLn !((stringClass <.!> "valueOf(char)") 'H')

The first function takes an Idris Double and the second function takes Idris Char. The types passed to the foreign functions to resolve overloading are JVM types.

4. Safe instance method

  do
    s <- (stringClass <.> "substring(int)") "Foobar" 1
    putStrLn !(either throw (pure . show) s) 

Safe instance method calls are similar to static method calls except that the instance should be passed as the first argument. Here again, we don’t provide any explicit type signature or the type of method invocation whether it is static or instance method but it all works out automatically in a type safe way. Here also we pick a particular overloaded version.

The type of (stringClass <.> "substring(int)") is String -> Int -> JVM_IO (Either Throwable (Maybe String)). Since the return type is String and it can be null, it is in a Maybe and the method can throw exceptions so the overall type is in Either.

5. Exception handling

do
  propValue <- try ((systemClass <.> "getProperty(?java/lang/String)") Nothing) [
    ([catch IllegalArgumentExceptionClass, catch NullPointerExceptionClass], \t =>
      do
        printLn "property name is null or empty"
        pure Nothing
    ),
    ([catchNonFatal], \t =>
      do
        printLn "unable to get property value"
        pure Nothing
    )
  ]
  printLn propValue

This example shows how to handle exceptions with different handlers and also shows how to pass a null to a foreign function. If a FFI function argument type is prefixed with ?, then the idris type would be Maybe nativeTy and we can pass Nothing to pass a null to the foreign function. We can have handlers for single exception, multiple exceptions or for all non fatal errors similar to Scala’s NonFatal.

6. Constructors

do
  arrayList1 <- (arrayListClass <.> "<init>(int)") 10
  putStrLn !(either throw toString arrayList1)

  -- Unsafe constructor
  arrayList2 <- arrayListClass <.!> "<init>()"
  putStrLn !(toString arrayList2)

Similar to methods, constructors can be overloaded and we can select a particular overload variant by explicitly specifying the foreign type. Constructors can also be invoked in a safe or unsafe way. As constructors cannot return null, when invoked in a safe way, the result type will only be in Either and not wrapped in a Maybe.

7. Fields

do
  -- static field getter
  caseInsensitiveComparator <- stringClass <.#!> "CASE_INSENSITIVE_ORDER"
  printLn !((comparatorClass <.!> "compare") caseInsensitiveComparator "Bar" "august")

  point <- (pointClass <.!> "<init>(int,int)") 2 3

  -- instance field getter
  printLn !((pointClass <.#> "x") point)

  -- instance field setter
  (pointClass <.=> "x") point 34
  printLn !((pointClass <.#> "x") point)

Similar to methods and constructors, fields can also be accessed either in a safe or unsafe way using <.#> for safe getter, <.=> for safe setter, <.#!> for unsafe getter and <.=!> for unsafe setter. Since field access cannot throw a exception, the return type is automatically just Maybe nativeTy. The field types are automatically determined without the user having to provide the foreign types of the fields.

Summary

This post demonstrated how with Idris’ powerful features FFI, type provider and elaborator reflection, we can safely and easily access JVM foreign functions. We can access fields, methods and constructors without having to explicitly provide foreign types and we can access them in safe way without null getting into Idris code and handle exceptions thrown by foreign functions. It also showed how to call overloaded methods and constructors and how Maybe and Either types are used with foreign functions.

Idris JVM: Guarding against Java null using Maybe type

Idris JVM now helps avoiding nulls getting into Idris from FFI calls using Maybe type. FFI declarations can have Maybe type in any argument position or in the return type.

Handling null from FFI call

getProperty : String -> JVM_IO (Maybe String)
getProperty = invokeStatic SystemClass "getProperty" (String -> JVM_IO (Maybe String))

The above function is an FFI call to Java’s method static String getProperty(String key). The method returns a system property value if the property is set otherwise returns null. With Maybe type in the Idris function’s return type, the Idris function returns Nothing if the returned value is null otherwise the value is wrapped in Just.

Example

module Main

import IdrisJvm.IO
import Java.Lang

main : JVM_IO ()
main = printLn !(getProperty "foo")  

$ idris --portable-codegen jvm -p idrisjvmffi returningnull.idr -o target

$ java -cp target:/path/to/idris-jvm-runtime-1.0-SNAPSHOT.jar main.Main
Nothing

$ java -cp target:/path/to/idris-jvm-runtime-1.0-SNAPSHOT.jar -Dfoo=hello main.Main
Just "hello"

Passing Maybe values for nullable values in FFI calls

module Main

import IdrisJvm.IO
import Java.Lang

namespace Component
  Component : Type
  Component = JVM_Native $ Class "java/awt/Component"

namespace JOptionPane
  JOptionPaneClass : JVM_NativeTy
  JOptionPaneClass = Class "javax/swing/JOptionPane"

  showMessageDialog : Inherits Object messageTy => Maybe Component -> messageTy -> JVM_IO ()
  showMessageDialog parent message =
    invokeStatic JOptionPaneClass "showMessageDialog" (Maybe Component -> Object -> JVM_IO ()) parent (believe_me message)

main : JVM_IO ()
main = showMessageDialog Nothing "Hello Idris!"

In the above code, the Java method JOptionPane.showMessageDialog(parentComponent, message) takes a nullable parent component and a message. If the parent component is null then the message is displayed in a default frame.

$ idris --portable-codegen jvm -p idrisjvmffi passingnull.idr -o target

$ java -cp target:/path/to/idris-jvm-runtime-1.0-SNAPSHOT.jar main.Main

Idris code passes Nothing in the above code so null is passed for the Java method that displays the message in a default frame as shown below.

Introducing Idris on the JVM and an Idris Android example

Idris on the JVM! Yes, a dependently typed language on the JVM! I have been working on a JVM bytecode backend for Idris for the past few months and it is now at a point that we can even write Android programs with Idris without having to write a single line of Java. In this post, we will see how Idris works on the JVM and an example Android program written in Idris.

Hello World

module Main

main : IO ()
main = printLn "Hello World"

Compile:

$ idris --portable-codegen jvm -p idrisjvmffi helloworld.idr -o target

Dependencies are provided as Idris packages, not as Java dependencies like jar or class files. The overall process is that the compiler reads Idris files and converts them into an intermediate JSON representation and the JVM bytecode generator takes the JSON files and converts them into JVM bytecode class files directly. It is only when we run a Java class, we have to provide Java dependency jars. The output option -o represents a directory where the Java class files will be created.

Run:

$ java -cp target:/path/to/idris-jvm-runtime-1.0-SNAPSHOT.jar main.Main
"Hello World"

And the output folder contains,

$ tree target
target
├── Decidable
│   └── Equality.class
├── main
│   └── Main.class
└── Prelude
    ├── Basics.class
    ├── Bool.class
    ├── Chars.class
    ├── Interfaces.class
    ├── Show.class
    └── Strings.class

Why do we have all these classes? We only compiled Main module! This is because Idris performs whole program analysis/compilation and code generator generates bytecode for all the modules that are relevant for the result produced by the main program.

How does Idris JVM handle tail calls?

Idris JVM eliminates self-recursion with JVM GOTO and uses trampolines for other tail calls. Let’s look at the following examples.

self-recursion example

module Main

import IdrisJvm.IO

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 : JVM_IO ()
main = printLn (sum 50000)

This program would work just fine without blowing up the stack as it will be compiled down to a loop that uses JVM’s GOTO instruction. Here is the relevant section from bytecode:

$ javap -c -cp target:/path/to/idris-jvm-runtime-1.0-SNAPSHOT.jar main.Main

  public static java.lang.Object sum$whr$go$colon$0(java.lang.Object, java.lang.Object, java.lang.Object);
    Code:
       0: aconst_null
       1: astore        7
       3: aconst_null
       4: astore_3
       5: aconst_null
       6: astore        4
       8: aconst_null
       9: astore        5
      11: aconst_null
      12: astore        6
      14: iconst_1
      15: istore        8
      17: iload         8
      19: ifeq          130
      22: aload_2
      23: new           #80                 // class java/math/BigInteger
      26: dup
      27: ldc           #82                 // String 0
      29: invokespecial #85                 // Method java/math/BigInteger."<init>":(Ljava/lang/String;)V
      32: invokestatic  #333                // Method mmhelloworld/idrisjvmruntime/Util.equals:(Ljava/lang/Object;Ljava/lang/Object;)Z
      35: ifeq          47
      38: aload_1
      39: astore        7
      41: iconst_0
      42: istore        8
      44: goto          127
      47: new           #80                 // class java/math/BigInteger
      50: dup
      51: ldc_w         #335                // String 1
      54: invokespecial #85                 // Method java/math/BigInteger."<init>":(Ljava/lang/String;)V
      57: astore_3
      58: aload_2
      59: invokestatic  #103                // Method mmhelloworld/idrisjvmruntime/Util.asBigInt:(Ljava/lang/Object;)Ljava/math/BigInteger;
      62: aload_3
      63: invokestatic  #103                // Method mmhelloworld/idrisjvmruntime/Util.asBigInt:(Ljava/lang/Object;)Ljava/math/BigInteger;
      66: invokevirtual #338                // Method java/math/BigInteger.subtract:(Ljava/math/BigInteger;)Ljava/math/BigInteger;
      69: astore_3
      70: new           #80                 // class java/math/BigInteger
      73: dup
      74: ldc_w         #335                // String 1
      77: invokespecial #85                 // Method java/math/BigInteger."<init>":(Ljava/lang/String;)V
      80: astore        4
      82: aload_3
      83: invokestatic  #103                // Method mmhelloworld/idrisjvmruntime/Util.asBigInt:(Ljava/lang/Object;)Ljava/math/BigInteger;
      86: aload         4
      88: invokestatic  #103                // Method mmhelloworld/idrisjvmruntime/Util.asBigInt:(Ljava/lang/Object;)Ljava/math/BigInteger;
      91: invokevirtual #107                // Method java/math/BigInteger.add:(Ljava/math/BigInteger;)Ljava/math/BigInteger;
      94: astore        4
      96: iconst_0
      97: invokestatic  #41                 // Method java/lang/Integer.valueOf:(I)Ljava/lang/Integer;
     100: astore        5
     102: aload_1
     103: invokestatic  #103                // Method mmhelloworld/idrisjvmruntime/Util.asBigInt:(Ljava/lang/Object;)Ljava/math/BigInteger;
     106: aload         4
     108: invokestatic  #103                // Method mmhelloworld/idrisjvmruntime/Util.asBigInt:(Ljava/lang/Object;)Ljava/math/BigInteger;
     111: invokevirtual #107                // Method java/math/BigInteger.add:(Ljava/math/BigInteger;)Ljava/math/BigInteger;
     114: astore        6
     116: aload         5
     118: astore_0
     119: aload         6
     121: astore_1
     122: aload_3
     123: astore_2
     124: goto          127
     127: goto          17
     130: aload         7
     132: areturn

The third line from the last is the GOTO instruction that transfers the control back to the top of function instead of actually calling the function.

Mutual recursion example:

module Main

mutual
  evenT : Nat -> IO Bool
  evenT Z = pure True
  evenT (S k) = oddT k

  oddT : Nat -> IO Bool
  oddT Z = pure False
  oddT (S k) = evenT k

main : IO ()
main = printLn !(evenT 9999)

The above code also would work fine without killing the stack. Mutual recursion is handled using trampolines and the tail calls are delayed and compiled down to Java 8 lambdas. As the bytecode for this is bit long, here is the decompiled bytecode for the evenT function:

    public static Object evenT(Object var0) {
        Object var4 = null;
        Integer var1 = null;
        Integer var2 = null;
        IdrisObject var3 = null;
        if (Util.equals(var0, BigInteger.ZERO)) {
            var1 = Integer.valueOf(0);
            var2 = Integer.valueOf(0);
            var3 = new IdrisObject(1);
            var4 = new IdrisObject(65653, new Object[]{var1, var2, var3});
        } else {
            BigInteger var5 = BigInteger.ONE;
            var5 = Util.asBigInt(var0).subtract(Util.asBigInt(var5));
            var4 = () -> {
                return oddT(var5);
            };
        }

        return var4;
    }

As we can see from the decompiled output above, the oddT call is not performed on the same call stack but a thunk wrapping the function call is returned using lambda (which is compiled down to JVM’s invokedynamic instruction).

Here is the relevant bit from bytecode for those who are interested:

        68: getstatic     #64                 // Field java/math/BigInteger.ONE:Ljava/math/BigInteger;
        71: astore_1
        72: aload_0
        73: invokestatic  #68                 // Method io/github/mmhelloworld/idrisjvm/runtime/Util.asBigInt:(Ljava/lang/Object;)Ljava/math/BigInteger;
        76: aload_1
        77: invokestatic  #68                 // Method io/github/mmhelloworld/idrisjvm/runtime/Util.asBigInt:(Ljava/lang/Object;)Ljava/math/BigInteger;
        80: invokevirtual #72                 // Method java/math/BigInteger.subtract:(Ljava/math/BigInteger;)Ljava/math/BigInteger;
        83: astore_1
        84: aload_1
        85: invokedynamic #79,  0             // InvokeDynamic #1:call:(Ljava/lang/Object;)Lio/github/mmhelloworld/idrisjvm/runtime/Thunk;
        90: astore        4
        92: goto          95
        95: aload         4
        97: areturn

Java interoperability: Calling Java from Idris and calling Idris from Java

Idris JVM supports calling Java static methods, instance methods, constructors and also accessing static and instance fields from Idris. At the moment, except for Java arrays, all the Java types can be constructed from Idris and passed to Java methods. Support for handling nulls and exceptions is currently in progress and will soon be available. (Update 01/10/2017: We can now use Maybe type to avoid Java nulls in Idris code)

To use Idris functions from Java, Idris JVM supports exporting Idris functions as static methods, instance methods, constructors of an exported Java class. The exported class can also extend a Java class or implement interfaces with Idris functions.

To demonstrate these features, let’s create an Android application In Idris.

An Android application in Idris

module Main

import IdrisJvm.IO
import Java.Lang

pythag : Int -> List (Int, Int, Int)
pythag max = [(x, y, z) | z <- [1..max], y <- [1..z], x <- [1..y],
                          x * x + y * y == z * z]

IdrisAndroidActivity : Type
IdrisAndroidActivity = JVM_Native $ Class "hello/IdrisAndroidActivity"

Bundle : Type
Bundle = JVM_Native $ Class "android/os/Bundle"

Context : Type
Context = JVM_Native $ Class "android/content/Context"

View : Type
View = JVM_Native $ Class "android/view/View"

TextView : Type
TextView = JVM_Native $ Class "android/widget/TextView"

Inherits View TextView where {}

CharSequence : Type
CharSequence = JVM_Native $ Class "java/lang/CharSequence"

Inherits CharSequence String where {}

superOnCreate : IdrisAndroidActivity -> Bundle -> JVM_IO ()
superOnCreate = invokeInstance "superOnCreate" (IdrisAndroidActivity -> Bundle -> JVM_IO ())

getApplicationContext : IdrisAndroidActivity -> JVM_IO Context
getApplicationContext = invokeInstance "getApplicationContext" (IdrisAndroidActivity -> JVM_IO Context)

newTextView : Context -> JVM_IO TextView
newTextView = FFI.new (Context -> JVM_IO TextView)

setText : Inherits CharSequence charSequence => TextView -> charSequence -> JVM_IO ()
setText this text = invokeInstance "setText" (TextView -> CharSequence -> JVM_IO ()) this (believe_me text)

setContentView : Inherits View view => IdrisAndroidActivity -> view -> JVM_IO ()
setContentView this view = invokeInstance "setContentView" (IdrisAndroidActivity -> View -> JVM_IO ()) this (believe_me view)

onCreate : IdrisAndroidActivity -> Bundle -> JVM_IO ()
onCreate this bundle = do
  superOnCreate this bundle
  context <- getApplicationContext this
  textView <- newTextView context
  setText textView $ "Hello Android from Idris! pythag 50 is " ++ show (pythag 50)
  setContentView this textView

main : IO ()
main = pure ()

androidExport: FFI_Export FFI_JVM "hello/IdrisAndroidActivity extends android/support/v7/app/AppCompatActivity" []
androidExport =
  Fun superOnCreate (Super "onCreate") $
  Fun onCreate (ExportInstance "onCreate") $
  End

The above program demonstrates calling Java instance methods (setText for example) and constructors (newTextView).

It further demonstrates how to handle inheritance relationship when passing subclass instances to a parent class type. For example, function setContentView takes a View but we can pass a TextView as it is a subclass of View and we mention that to Idris via Inherits View TextView where {}.

It also demonstrates how we can create a Java class that extends another class and override methods with Idris functions. The last section androidExport creates a Java class named hello/IdrisAndroidActivity that extends android/support/v7/app/AppCompatActivity. The Java class also creates a wrapper method superOnCreate that just delegates to super.OnCreate and the class also overrides onCreate method with Idris’ onCreate function. The Java class can also implement one or more Java interfaces with something like,

hello/IdrisAndroidActivity extends android/support/v7/app/AppCompatActivity implements java/lang/Runnable, java/lang/Comparable

A module can have multiple exports so we can actually create multiple Java classes with Idris implementation functions from an Idris module.

We can compile this as usual,

idris --portable-codegen jvm -p idrisjvmffi idrisandroid.idr -o target

It would produce the following class files:

$ tree target/
target/
├── Decidable
│   └── Equality.class
├── hello
│   └── IdrisAndroidActivity.class
├── main
│   ├── Main.class
│   └── Prelude.class
└── Prelude
    ├── Algebra.class
    ├── Applicative.class
    ├── Bool.class
    ├── Foldable.class
    ├── Interfaces.class
    ├── List.class
    ├── Monad.class
    ├── Show.class
    └── Strings.class

Deploying to Android:

1. Create an android project using Android studio with Jack support for Java 8.
2. Then package the classes compiled above along with idris-jvm-runtime-1.0-SNAPSHOT.jar classes in a single jar and copy into an android project’s app/libs directory.
3. Change the activity class name in android manifest file to the Idris exported class name hello.IdrisAndroidActivity.
4. Then run ./gradlew installDebug from android project after starting an emulator or connected to an android device.
5. Finally we should see our Idris code running on Android! It should look something like this:

Happy coding!

Haskell on the JVM via GHCJS and Nashorn

Currently there are 2 ways we can write Haskell on the JVM:

1. Frege, a language that follows Haskell 2010 standard and compiles to Java.
2. Haskell itself by compiling it to JavaScript via GHCJS.

Frege is basically a Haskell for the JVM and infact conforms to Haskell 2010 with few inbuilt GHC extensions. Even with good Java interop, it doesn’t sacrifice its type guarantees and currently is the only pure language on the JVM.

In this post, I am going to explore another interesting option: Haskell itself on the JVM. Haskell can be compiled to JavaScript using GHCJS and Java has an inbuilt JavaScript engine, called Nashorn so it is actually possible to compile Haskell to JavaScript and run the resulting JavaScript on the JVM.

Here is a simple Haskell code that can be run on the JVM:

module Main where

-- Nashorn doesn't provide default console object. Haskell's putStrLn logs to the console.
foreign import javascript unsafe "console={ \
    \ log: function(s) { java.lang.System.out.print(s); },\
    \ info: function(s) { java.lang.System.out.print(s); },\
    \ warn: function(s) { java.lang.System.out.print(s); },\
    \ debug: function(s) { java.lang.System.out.print(s); },\
    \ error: function(s) { java.lang.System.err.print(s); }\
    \ }"
  setupConsole :: IO ()

foreign import javascript unsafe "java.lang.System.exit($1)"
  sysexit :: Int -> IO ()

main = do
  setupConsole
  putStrLn "Hello from Haskell!"
  sysexit 0

Nashorn doesn’t have an inbuilt console object and Haskell’s putStrLn prints to the console so we have to provide an implementation of console. The implementation, as can be seen from the code above, is actually backed by Java’s System.out.print. That is our first example of calling Java from Haskell. sysexit is another function calling Java. sysexit is needed here as otherwise the program just keeps on running which I think is because of JavaScript event loop or something similar that prevents the JVM from shutting down.

Compiling Haskell with GHCJS and running on JVM

$ ghcjs -o HelloJava HelloJava.hs
[1 of 1] Compiling Main             ( HelloJava.hs, HelloJava.js_o )
Linking HelloJava.jsexe (Main)

$ jjs HelloJava.jsexe/all.js 
Hello from Haskell!

jjs is a JVM laucher for JavaScript code similar to Node. It is also possible to run this as a regular Java program along with other Java classes without jjs. jjs is just a convenient way to run just JavaScript code on the JVM. Above GHCJS compiles the Haskell code to JavaScript in one file all.js and the JVM runs the JavaScript code from all.js.

Example 2

Now let’s look at another example that shows how to convert between Haskell and Java lists:

{-# LANGUAGE ForeignFunctionInterface #-}
{-# LANGUAGE JavaScriptFFI #-}
{-# LANGUAGE UnliftedFFITypes #-}
{-# LANGUAGE GHCForeignImportPrim #-}
{-# LANGUAGE TypeSynonymInstances #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE DeriveDataTypeable #-}
{-# LANGUAGE TypeFamilies #-}

module Main where

import Control.Monad.ST
import GHCJS.Types
import GHCJS.Foreign
import GHCJS.Prim
import Data.Typeable
import GHC.ST 

data MutabilityType s = Mutable
                      | Immutable
                      | STMutable s

data IsItMutable = IsImmutable
                 | IsMutable

-- Copied from GHCJS.Internal.Types. Not sure why this is not exposed.
type family Mutability (a :: MutabilityType s) :: IsItMutable where
  Mutability Immutable     = IsImmutable
  Mutability Mutable       = IsMutable
  Mutability (STMutable s) = IsMutable

{- java.util.ArrayList class and its methods -}
newtype SomeArrayList (a :: MutabilityType s) = SomeArrayList JSVal deriving Typeable
type ArrayList           = SomeArrayList Immutable
type MutableArrayList    = SomeArrayList Mutable
type STArrayList s      = SomeArrayList (STMutable s)

instance IsJSVal (SomeArrayList m)

-- ArrayList Constructor
foreign import javascript unsafe "new $1()"
  arrayList_new :: JType -> ST s (STArrayList s) 

-- Adds an element to ArrayList
foreign import javascript unsafe "$2.add($1)"
  arrayList_add :: JSVal ->  STArrayList s -> ST s ()

{- java.util.Iterator class and its methods -}
newtype SomeIterator (a :: MutabilityType s) = SomeIterator JSVal deriving Typeable
type Iterator            = SomeIterator Immutable
type MutableIterator     = SomeIterator Mutable
type STIterator s        = SomeIterator (STMutable s)

instance IsJSVal (SomeIterator m)

-- Create an Iterator from an ArrayList
foreign import javascript unsafe "$1.iterator()"
  iterator :: STArrayList s -> ST s (STIterator s)

foreign import javascript unsafe "$1.hasNext()"
  iterator_hasNext :: STIterator s -> ST s Bool

foreign import javascript unsafe "$1.next()"
  iterator_next :: STIterator s -> ST s JSVal

{- Other Nashorn imports -}

-- Represents a Java type
newtype JType = JType JSVal

foreign import javascript unsafe "java.lang.System.out.println($1)"
  jprintln :: JSVal -> IO ()

foreign import javascript unsafe "java.lang.System.exit($1)"
  sysexit :: Int -> IO ()

-- Imports a Java class
foreign import javascript unsafe "Java.type($1)"
  jimport :: JSVal -> JType 

{- Create an instance of Java's ArrayList from Haskell's list -}
listToArrayList :: [JSVal] -> ST s (STArrayList s)
listToArrayList xs = do
    let arrayListClass = jimport $ toJSString "java.util.ArrayList"
    arrList <- arrayList_new arrayListClass
    go xs arrList
  where
    go [] arrList = return arrList
    go (x:xs) arrList = do
      arrayList_add x arrList
      go xs arrList

{- Create Haskell's list from Java's Iterator -}
iteratorToList :: STIterator s -> ST s [JSVal]
iteratorToList itr = reverse <$> go [] where
  go acc = do
    hasNext <- iterator_hasNext itr
    if hasNext
      then do
        next <- iterator_next itr
        go (next: acc)
      else
        return acc

-- Nashorn doesn't provide default console object. Haskell's putStrLn logs to the console.
foreign import javascript unsafe "console={ \
    \ log: function(s) { java.lang.System.out.print(s); },\
    \ info: function(s) { java.lang.System.out.print(s); },\
    \ warn: function(s) { java.lang.System.out.print(s); },\
    \ debug: function(s) { java.lang.System.out.print(s); },\
    \ error: function(s) { java.lang.System.err.print(s); }\
    \ }"
  setupConsole :: IO ()

demo = runST $ do
  jlist <- listToArrayList . map toJSInt $ [1..5]
  iterator jlist >>= iteratorToList
 
main = do
  setupConsole
  mapM_ (putStrLn . show . fromJSInt) demo
  sysexit 0
 

In the code above, two Java types are used: java.util.ArrayList and java.util.Iterator.

Importing a Java class

A Java class can be imported with Java.type(className) Nashorn JavaScript code. Line 80 defines the corresponding Haskell FFI function:

-- Imports a Java class
foreign import javascript unsafe "Java.type($1)"
  jimport :: JSVal -> JType

Creating an instance of a Java class

An instance can be created by invoking the constructor on the Java class with new. Here is the corresponding FFI:

-- ArrayList Constructor
foreign import javascript unsafe "new $1()"
  arrayList_new :: JType -> ST s (STArrayList s)

It takes the ArrayList class and invokes the dafault ArrayList constructor to return an instance of it. In the same way, we can create FFI functions for ArrayList.add and ArrayList.iterator to return an Java Iterator instance.

The function listToArrayList takes a Haskell list and return an instance of Java ArrayList. As the java list is mutable, it is returned as STArrayList s inside ST. This function first creates an instance of ArrayList by invoking the Java constructor and then calls ArrayList.add to add items from Haskell list to the ArrayList.

In the similar way, the function iteratorToList takes a Java iterator and returns Haskell list by extracting items from the iterator by invoking corresponding FFI functions for Iterator.hasNext and Iterator.next.

Building with Stack

It is easy to setup a GHCJS project with Stack so that we can add other dependencies easily and build it for GHCJS. With the above code in a stack project “haskell-jvm-hello”, we can build it with stack build and run it with jjs:

$ stack build
haskell-jvm-hello-0.1.0.0: unregistering (local file changes: app/Main.hs)
haskell-jvm-hello-0.1.0.0: build
Preprocessing library haskell-jvm-hello-0.1.0.0...
In-place registering haskell-jvm-hello-0.1.0.0...
Preprocessing executable 'haskell-jvm-hello-exe' for
haskell-jvm-hello-0.1.0.0...
[1 of 1] Compiling Main             ( app/Main.hs, .stack-work/dist/x86_64-linux/Cabal-1.22.4.0_ghcjs/build/haskell-jvm-hello-exe/haskell-jvm-hello-exe-tmp/Main.js_o )
Linking .stack-work/dist/x86_64-linux/Cabal-1.22.4.0_ghcjs/build/haskell-jvm-hello-exe/haskell-jvm-hello-exe.jsexe (Main)
haskell-jvm-hello-0.1.0.0: copy/register
Installing library in
/workspace/haskell-jvm-hello/.stack-work/install/x86_64-linux/lts-3.12/ghcjs-0.2.0_ghc-7.10.3/lib/x86_64-linux-ghcjs-0.2.0-ghc7_10_3/haskell-jvm-hello-0.1.0.0-7MA0h74rERuEwiJY2TRuHx
Installing executable(s) in
/workspace/haskell-jvm-hello/.stack-work/install/x86_64-linux/lts-3.12/ghcjs-0.2.0_ghc-7.10.3/bin
Warning: the following files would be used as linker inputs, but linking is not being done: .stack-work/dist/x86_64-linux/Cabal-1.22.4.0_ghcjs/build/haskell-jvm-hello-exe/haskell-jvm-hello-exe
Registering haskell-jvm-hello-0.1.0.0...

$ jjs .stack-work/dist/x86_64-linux/Cabal-1.22.4.0_ghcjs/build/haskell-jvm-hello-exe/haskell-jvm-hello-exe.jsexe/all.js
1
2
3
4
5

Java’s Nashorn JavaScript engine opens up few more ways for the JVM to be polyglot and it is so good to have one of the best languages, Haskell, on the JVM. Actually it should also be possible to run PureScript as well in this way on the JVM but that is for another day. Happy Haskelling!

Frege: Record accessors and mutators

Frege has built-in mechanism to access and mutate (non-destructive) record fields.

Consider the following type in Frege:

frege> data Point = Point {x :: Int, y :: Int}
data type Point :: *

frege> derive Show Point
instance Show  Point

Now we can use the following functions to get and set record fields:

frege> Point.x
:: Point -> Int

frege> Point.{x = }
:: Point -> Int -> Point

frege> Point.{x <- }
:: Point -> (Int->Int) -> Point

For Field x,

1. The function Point.x is the getter.
2. The function Point.{x = } is a setter which sets the field x with a new value.
3. The function Point.{x <- } is also a setter but applies a function to update the current value.

We can use the functions like this:

frege> p = Point 3 4
value p :: Point

frege> p
Point 3 4

frege> Point.x p
3

frege> Point.{x =} p 13
Point 13 4

frege> Point.{x <-} p (+15)
Point 18 4

Frege also provides some shortcuts to apply these functions:

frege> p.x -- Same as `Point.x p`
3

frege> p.{x = 10} -- Same as `Point.{x = } p 10`
Point 10 4

frege> p.{x <-} -- Same as `Point.{x <-} p`
:: (Int->Int) -> Point

frege> p.{x <- (+10)} -- Same as `Point.{x <- } p (+10)`
Point 13 4

Multiple updates can be combined:

frege> p.{x <- (+8), y = 20} -- Increment x by 8 and set y to 20
Point 11 20

Accessors and updates can be at any level deep. Let’s create another type:

frege> :{
> data Circle = Circle {center :: Point, radius :: Int}
>
> derive Show Circle
> :}

data type Circle :: *
instance Show  Circle

frege>

Here we have an aggregate type Circle which composes another type Point for it’s field center. Now we can update and select fields at different levels:

frege> c = Circle {center = Point 4 5, radius = 10}
value c :: Circle

frege> c
Circle (Point 4 5) 10

frege> c.center.x
4

frege> c.{center <- Point.{x = 8}}
Circle (Point 8 5) 10

frege> c.{center <- Point.{y <- (+20)}, radius <- (*5)}
Circle (Point 4 25) 50

In the latest version, Frege provides syntactic sugar for lambdas using underscores. For example, T.foo can be written as _.foo if the type can be deduced from the context the lambda is applied. Hence the following two are equivalent.

frege> c.{center <- Point.{x = 25}}
Circle (Point 25 5) 10

frege> c.{center <- _.{x = 25}}
Circle (Point 25 5) 10

Frege provides another utility to check for a field’s existence. This would be useful if we have multiple constructors with different set of fields.

frege> :{
> data Point = Point2d {x :: Int, y :: Int}
>            | Point3d {x :: Int, y :: Int, z :: Int}
>
> derive Show Point
> :}

data type Point :: *
instance Show  Point

frege>

In the above code, we have two constructors Point2d and Point3d where the field z exists only for Point3d. We can check for the existence of field z like this:

frege> Point.{z?}
:: Point -> Bool

frege> hasZ = Point.{z?}

frege> hasZ $ Point3d 3 4 5
true

frege> hasZ $ Point2d 3 4
false

frege> p = Point3d 3 4 5
value p :: Point

frege> p.{z?}
true

For more details on how these field existence check, accessor and mutator functions are generated for a record type, here is the link to Frege language reference: http://www.frege-lang.org/doc/Language.pdf.

Happy coding!

Frege: Hello Java

Here is a small code demonstrating Java interoperability in Frege:

module hellojava.HelloJava where
 
data LinkedList a = native java.util.LinkedList where
    native add :: Mutable s (LinkedList a) -> a -> ST s Bool
    native get :: Mutable s (LinkedList a) -> Int -> ST s (Maybe a) throws
        IndexOutOfBoundsException
    native new :: () -> STMutable s (LinkedList a)
    
    fromFregeList :: [a] -> STMutable s (LinkedList a)
    fromFregeList xs = LinkedList.new () >>= loop xs where
        loop (x:xs) jlist = LinkedList.add jlist x >> loop xs jlist
        loop [] jlist = return jlist
        
plusTop :: Mutable s (LinkedList Int) -> ST s (Maybe Int)
plusTop xs = do
    a <- xs.get 0
    b <- xs.get 1
    return ((+) <$> a <*> b)
 
data IndexOutOfBoundsException = native java.lang.IndexOutOfBoundsException
derive Exceptional IndexOutOfBoundsException

data Exception = native java.lang.Exception
derive Exceptional Exception
 
data NullPointerException = native java.lang.NullPointerException
derive Exceptional NullPointerException
 
pure native showThrowable toString :: Throwable -> String
 
main _ = do
    javaList <- LinkedList.fromFregeList [1, 2, 3]
    try (\xs -> plusTop xs >>= (println . maybe "Got a null pointer" show)) javaList 
        `catch` (\(npe :: NullPointerException) -> println $ showThrowable npe)
        `catch` (\(exception :: Exception) -> println $ showThrowable exception)

We can observe the following things from the above code:

1. Making use of a Java class and its methods
2. Using a Java object in a Frege function
3. Using Java Exceptions in functions
4. Handling Java exceptions

1. Making use of a Java class and its methods:

If a Java class is pure then without much effort, we can use that class in Frege. For example,

data Integer = native java.math.BigInteger where
    pure  native abs                                  :: Integer -> Integer
    pure  native negate                               :: Integer -> Integer
    pure  native valueOf java.math.BigInteger.valueOf :: Long -> Integer

A Java class is declared with data declaration in Frege. The identifier after the data keyword is the corresponding type for the Java class in Frege and the qualified Java class is identified after the native keyword followed by the instance methods, static methods or even some Frege functions not defined in the original Java class.

An important point here is that the instance methods on BigInteger take Integer as their first argument which is the this reference on which the methods will be invoked.

Coming back to our original example, here we are trying to use the mutable Java class java.util.LinkedList. An obvious difference between this one and the BigInteger example is that the functions now do not have the pure keyword in front.

The next difference is that the instance methods now cannot take the simple type like LinkedList a as we did for Integer but the type is now Mutable s (LinkedList a) since it is not a pure function. If we don’t annotate a native function pure and we don’t use Mutable to consume or return a mutable Object, it will be a compilation error. Mutable objects can only be used in ST or IO actions so the return type must be in ST or IO monad.

The LinkedList.add() method returns a boolean. Since it is an impure function, it should be used in ST monad. Here the boolean itself is pure so it is just ST s Bool. Take a look at the third function new, LinkedList constructor. This function is impure and it returns a mutable object, a new LinkedList instance, so the return type is ST s (Mutable s (LinkedList a)) for which the shorthand is STMutable s (LinkedList a).

Here is an example for a native function not being part of a native data declaration. This is useful when a native class is already declared in Frege in some module but the function that we are looking for is missing in the data declaration.

pure native showThrowable toString :: Throwable -> String

Here showThrowable is the Frege function name for Throwable.toString(). Since it is an instance method on Throwable, the first argument is of type Throwable and then the formal arguments’ types (in this case, none) and return type.

2. Using a Java object in a Frege function

A native data declaration doesn’t have to just contain the native members, it can also have additional Frege functions. In our example, the function fromFregeList is not defined in the Java class but it has been added as an utility function to create a LinkedList from a frege list. Here again the same rule as in the previous section applies: To return a mutable Java object, we should use ST s (Mutable s TheJavaType) which is nothing but STMutable s TheJavaType.

In the same way, the plusTop function takes a mutable Java object so the parameter type is Mutable s (LinkedList Int). Also since it consumes a mutable type, it must be in ST monad hence the return type is ST s (Maybe Int) returning an Maybe Int in ST.

3. Using Java Exceptions in functions

To use a Java Exception class, it must be first defined in a Frege module. It is the same as declaring native declaration for a Java class but additionally we need to derive the Exceptional type class so that the exception can later be handled with catch.

data IndexOutOfBoundsException = native java.lang.IndexOutOfBoundsException

derive Exceptional IndexOutOfBoundsException

The exceptions can then be used in native declarations as in get function in our example:

native get :: Mutable s (LinkedList a) -> Int -> ST s (Maybe a) throws
    IndexOutOfBoundsException

4. Handling Java exceptions

In two ways, we can handle exceptions:

1. Using action `catch` handler1 `catch` handler2

   The type of catch is Exceptional β => ST γ α -> (β->ST γ α) -> ST γ α.

   Here the action is the code where an exception might be thrown and the handlers handler1 and handler2 take an exception and return another value in ST monad. The infix notation facilitates adding multiple handlers with better readability. Further here the handler1 must be more specific(in terms of the types of the exceptions being handled) than handler2. Also note that from Frege standard library with respect to catch:

   Note If action is of the form: doSomething arg then, depending on the strictness of doSomething the argument arg may be evaluated before the action is returned. Exceptions (i.e. undefined values) that occur in the construction of the action do not count as exceptions thrown during execution of it, and hence cannot be catched.

   Example: println (head []) `catch` ....

   will not catch the exception that will be thrown when println evaluates

   For a remedy, see try.

2. Using try

   First, the type: try :: Monad γ => (α-> γ β) -> α -> γ β

   Unlike catch, try takes a function that produces a monadic value. If the function can throw an exception, it must result in an ST monad which can then be passed to catch to handle those exceptions. In our example, \xs -> plusTop xs >>= (println . maybe "Got a null pointer" show) is the function which when applied to a java.util.LinkedList might throw a NullPointerException or IndexOutOfBoundsException:

   try (\xs -> plusTop xs >>= (println . maybe "Got a null pointer" show)) javaList
       catch` (\(npe :: NullPointerException) -> println $ showThrowable npe)
       catch` (\(exception :: Exception) -> println $ showThrowable exception)
   

Since the construction of action is deferred through a lambda here, try eliminates the issue with catch mentioned in the above note.

###Extending a class or implementing an interface in Frege:

One thing that is not shown in the example is extending a Java class or implementing an interface in Frege. Unfortunately both are not possible in Frege yet. There is a workaround though using a Java class which extends a class or implements an interface but instead of an implementation on its own, it just delegates to a Frege function. For example, see here for implementing java.lang.Runnable in Frege using a Java class frege.runtime.SwingSupport which takes a Frege function and then delegates to it in run method implementation.

This concludes our little experimentation calling Java from Frege. The other interesting side, calling Frege from Java, is for a future post.