Idris 2 for JVM

Idris 2 is a purely functional programming language with first class types. This repository provides Idris 2 compiler targeting JVM bytecode so that Idris can run on the JVM.

Install

• Download the latest Idris 2 JVM release from Github releases. If you prefer Maven, Idris compiler is available in Maven central from here.
• Extract the archive and add idris2 launcher script directory <EXTRACTED_DIRECTORY_ROOT>/exec to PATH.
• Create an environment variable IDRIS2_PREFIX pointing to <EXTRACTED_DIRECTORY_ROOT>/env

IDE Support

The Idris 2 (JVM) plugin for IntelliJ IDEA provides editor support backed by this compiler, including syntax highlighting, code completion, interactive editing (case split, add clause, proof search, generate definition, holes), go-to-definition, and documentation lookup. It also surfaces the JVM FFI: completing on a Java class offers its full set of callable members and generates the binding on demand.

Install it from the link above, or from within the IDE via Settings → Plugins → Marketplace and searching for "Idris 2 JVM". The plugin drives the idris2 executable from this repository, so make sure it is installed (see Install above).

Example

helloworld.idr

    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"]

Documentation

• Idris JVM documentation
• Idris 2 documentation
• Idris 2 (JVM) IntelliJ plugin

License

This repository extends idris-lang/Idris2 repository with JVM backend. Files from idris-lang/Idris2 are covered by that repository's license. All other files from this repository are covered by BSD-3-Clause License. See LICENSE.