Idris 2 0.6.0 is now available for the JVM

It would be nice if this linked to the README rather than a dump of the commit log, which makes it hard to know what's new or interesting in this release. It would be double nice if the readme talked about JVM language interop or performance, as that's presumably the main selling points of running Idris on the 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 2 compiler and Idris 2 programs can run on the JVM

I am wondering what kind of implications there are for Idris 2 to run on the JVM. For example: Does it still have TCO on the JVM? What about data structures? Does it have a set of functional data structures implemented, on top of Java ones? Or is it all implemented on top of Idris 2 "primitives"?

This link to the latest readme.md may be helpful.<p><a href="https:&#x2F;&#x2F;github.com&#x2F;mmhelloworld&#x2F;idris-jvm&#x2F;blob&#x2F;latest&#x2F;README.md">https:&#x2F;&#x2F;github.com&#x2F;mmhelloworld&#x2F;idris-jvm&#x2F;blob&#x2F;latest&#x2F;README...</a>

Never seen this language before, but I can say I _really_ like the syntax. Just looking at it it&#x27;s pretty easy to figure out what they were trying to do.

How does it interop with the existing Java libraries?

saw that idris compiled to C . How realistic is it to build a small core library in idris that would then have hooks to external components in other PL using C as a bridging layer ?

One of most frequent usage of a type system is literal types.<p>Haskell, Rust,... and modern programming languages fail to do it. The only exception is Typescript.<p>For example, simple way to adding a extended boolean type:<p>type MyBoolean = null | true | false.<p>Or<p>type MyRange = 3 | 4 | 5<p>Curious.