7 ms·

Idris 2 0.6.0 is now available for the JVM

162 points by ska80 4y ago

pestatije 4y ago
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
- gnulinux 4y ago
  To slightly elaborate: when this comment say "first class types" they're referring to dependent types. For programmers who are not aware: think about functions in functional programming languages. They're "first class citizens" in the sense that there is no difference between functions and any other values, such as `3` or `"hello"`. In dependently types languages, there is no difference between types and other values. Types are just any other value. For example, normally `Int` would be a type, but in these kind of programming languages `x: Int, x > 5` would also be a type even though the type depends on the value `x`. In terms of software engineering, one bonus you get is being able to encode your unittests in your type system. For example, you can do (in Agda): _ : myFunction x y z == 33 _ = refl -- refl is of type `x == x` and compiler will run this test for you at compile-time while type-checking your program. Two popular "practical" dependently typed languages are Agda and Idris. Of these two, Idris is relatively designed for software engineers, whereas Agda also wants to be a state-of-the-art automated theorem proving tool. I would strongly recommend checking both if you want to explore this area of programming languages. I wrote practical programs in Agda (e.g. language parsers, JSON parser etc) and I think it can make a programmer extremely productive, if you like this kind of workflow. Correctness is very easy to reason in these languages, and although it may look daunting at first, writing practical programs are very approachable (about as hard, maybe ever-so-slightly harder than writing code in Haskell). Have fun!
  - satvikpendem 4y ago
    So I could also write all my code purely in the type system too, right?
    - gnulinux 4y ago
      Yes, all computation done at runtime can be done at compile time (within type system). This is a problem in some cases e.g. if you write an infinite loop, this would mean compilation will infinitely loop. Different languages deal with this problem differently. E.g. in Agda, there is a "safe" subset of language that is not Turing Complete such that all programs can be algorithmically proven to be halting. But you can work around this via pragmas. Speaking from experience, the safe subset of Agda is all you need to write useful programs. You just need a tiny shell (maybe only few lines of code) that will handle IO and Haskell FFI. The rest of the code will be purely functional, safe, Turing Incomplete Agda.
fidgewidge 4y ago
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.
- mmhelloworld 4y ago
  Hello, I am the author of Idris JVM. Thank you for your feedback. I will update the README to include a link for JVM interop. For now, this file https://github.com/mmhelloworld/idris-jvm/blob/main/libs/base/System/Concurrency.idr https://github.com/mmhelloworld/idris-jvm/blob/main/libs/bas... , demonstrates how the interop looks like currently. The %foreign directive takes an FFI descriptor to talk to the respective backends. Here you can see few scheme and JVM descriptors starting with "scheme:" and "jvm:" respectively. The JVM descriptors there also show constructor calls `<init>`, instance methods `.lock` and static methods `getThreadData`.
revskill 4y ago
One of most frequent usage of a type system is literal types. Haskell, Rust,... and modern programming languages fail to do it. The only exception is Typescript. For example, simple way to adding a extended boolean type: type MyBoolean = null | true | false. Or type MyRange = 3 | 4 | 5 Curious.
- freilanzer 4y ago
  Why would I ever want to extend a type with null? That's exactly the opposite of what I want of a type system in the first place.
  - evomassiny 4y ago
    the type `null | true | false` is different from `true | false`, a type checker can assert that you handle the `null` case before using a function that wants a boolean. This is how rust handles it (with the Option<T> type).
    - harperlee 4y ago
      In particular, you may want this to signify “I dont know” with NULL, just as in SQL. See the Wikipedia page for ternary logic for more info.
      - alexvoda 4y ago
        Note that 3VL (3 valued logic) is one of the more criticized aspects of SQL. 3VL is a gigantic leap of of complexity over 2VL (boolean). The number of possible operations is a lot higher and the choice of operations is not standardized. To quote wikipedia: "In two-valued logic there are 2 nullary operators (constants), 4 unary operators, 16 binary operators, 256 ternary operators" And we all agree which of those 16 is named what. "In three-valued logic there are 3 nullary operators (constants), 27 unary operators, 19683 binary operators, 7625597484987 ternary operators" There is no standard meaning of the 3'rd value and of the operations involving it. That is not to say that 3VL isn't useful. I believe the reason for the criticism of 3VL in SQL it that the system made those choices for you and those choices are not always intuitive. Therefore a null in one attribute in one relation might mean something very different from a null in another attribute in another relation. Also note that as opposed to digital signal processing (where binary and ternary refer to the number of possible values a bit/trit can have), when discussing logic arity (nullary, unary, binary, ternary, n-ary) refers to the number of arguments required by a function as opposed to the number of values the arguments can have (univalent, bivalent, trivalent, k-valent). This is confusing because the terms are used interchangeably.
ghostwriter 4y ago
How does it interop with the existing Java libraries?
- nerdponx 4y ago
  I can't speak for the JVM backend specifically, but in general Idris 2 code can call arbitrary functions in the backend with the "%foreign" pragma. So hopefully that would be supported for Java, although I don't know how it would work with classes.
- mmhelloworld 4y ago
  This file https://github.com/mmhelloworld/idris-jvm/blob/main/libs/base/System/Concurrency.idr https://github.com/mmhelloworld/idris-jvm/blob/main/libs/bas... demonstrates how the interop looks like currently. The `%foreign` directive takes an FFI descriptor to talk to the respective backends. Here you can see few scheme and JVM descriptors starting with "scheme:" and "jvm:" respectively. The JVM descriptors there show constructor calls `<init>`, instance methods `.lock` and static methods `getThreadData`.
bsaul 4y ago
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 ?
- nerdponx 4y ago
  Idris 2 does compile to C, but it uses its own reference-counting garbage collector and cannot currently be used to generate libraries. I believe this limitation is true for all of the compiler targets right now, except maybe Javascript (some work was actively in progress on this when I last checked).
zelphirkalt 4y ago
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"?
- pjmlp 4y ago
  Naturally it doesn't have TCO on JVM, at least not natively as bytecode representation for it. The only possibility is to rewrite the code in similar way as clojure and Scala do it.
  - catiopatio 4y ago
    Which, to be clear, is not a zero-cost mechanical translation, and can be tricky and annoying when you start talking about things like generic monad transformer stacks.
- otto-edgar 4y ago
  I think TCO and JVM are orthogonal discussions -- by the time the bytecode is generated, the TCO may have already been performed.
  - nerdponx 4y ago
    I'm actually not sure about that. I think the Javascript compiler target also lacks full TCO. The Idris 2 compiler itself I think does not perform this optimization, because the Scheme reference backend does it already. I might be wrong about that, but I remember several active unresolved discussions on this topic in the community last year. I haven't been involved actively in it for several months, so my memory might be wrong.
    - dunham 4y ago
      The javascript back end handles mutually recursive tail calls. It finds connected components and rewrites them to use a trampoline-like thing. There is a nice explanation of how it works at the top of the file: https://github.com/idris-lang/Idris2/blob/main/src/Compiler/ES/TailRec.idr https://github.com/idris-lang/Idris2/blob/main/src/Compiler/... One could argue that it's not "full" TCO, but it does cover a lot of use-cases. That rewrites to NamedCExp, so it could be reused by other backends. The Java backend seems to be doing its own thing. There aren't a lot of comments or documentation in that repository, but I do see evidence that it's doing something interesting in src/Compiler/Jvm/Optimizer.idr: Pure $ if shouldTrampoline && hasNonSelfTailCall tailCallCategory then trampolineExpression True inlinedAndTailRecursionMarkedExpr else inlinedAndTailRecursionMarkedExpr
IncRnd 4y ago
This link to the latest readme.md may be helpful. https://github.com/mmhelloworld/idris-jvm/blob/latest/README.md https://github.com/mmhelloworld/idris-jvm/blob/latest/README...
exabrial 4y ago
Never seen this language before, but I can say I _really_ like the syntax. Just looking at it it's pretty easy to figure out what they were trying to do.
- saghm 4y ago
  Have you used Haskell before? It seems almost identical syntactically at a glance, so I'm curious if that's what you mean by "what they were trying to do" or if it's your first time seeing syntax like this at all.

162 points by ska80 4y ago

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

gnulinux 4y ago
To slightly elaborate: when this comment say "first class types" they're referring to dependent types. For programmers who are not aware: think about functions in functional programming languages. They're "first class citizens" in the sense that there is no difference between functions and any other values, such as `3` or `"hello"`. In dependently types languages, there is no difference between types and other values. Types are just any other value. For example, normally `Int` would be a type, but in these kind of programming languages `x: Int, x > 5` would also be a type even though the type depends on the value `x`. In terms of software engineering, one bonus you get is being able to encode your unittests in your type system. For example, you can do (in Agda): _ : myFunction x y z == 33 _ = refl -- refl is of type `x == x` and compiler will run this test for you at compile-time while type-checking your program. Two popular "practical" dependently typed languages are Agda and Idris. Of these two, Idris is relatively designed for software engineers, whereas Agda also wants to be a state-of-the-art automated theorem proving tool. I would strongly recommend checking both if you want to explore this area of programming languages. I wrote practical programs in Agda (e.g. language parsers, JSON parser etc) and I think it can make a programmer extremely productive, if you like this kind of workflow. Correctness is very easy to reason in these languages, and although it may look daunting at first, writing practical programs are very approachable (about as hard, maybe ever-so-slightly harder than writing code in Haskell). Have fun!
- satvikpendem 4y ago
  So I could also write all my code purely in the type system too, right?
  - gnulinux 4y ago
    Yes, all computation done at runtime can be done at compile time (within type system). This is a problem in some cases e.g. if you write an infinite loop, this would mean compilation will infinitely loop. Different languages deal with this problem differently. E.g. in Agda, there is a "safe" subset of language that is not Turing Complete such that all programs can be algorithmically proven to be halting. But you can work around this via pragmas. Speaking from experience, the safe subset of Agda is all you need to write useful programs. You just need a tiny shell (maybe only few lines of code) that will handle IO and Haskell FFI. The rest of the code will be purely functional, safe, Turing Incomplete Agda.

fidgewidge 4y ago

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.

mmhelloworld 4y ago
Hello, I am the author of Idris JVM. Thank you for your feedback. I will update the README to include a link for JVM interop. For now, this file https://github.com/mmhelloworld/idris-jvm/blob/main/libs/base/System/Concurrency.idr https://github.com/mmhelloworld/idris-jvm/blob/main/libs/bas... , demonstrates how the interop looks like currently. The %foreign directive takes an FFI descriptor to talk to the respective backends. Here you can see few scheme and JVM descriptors starting with "scheme:" and "jvm:" respectively. The JVM descriptors there also show constructor calls `<init>`, instance methods `.lock` and static methods `getThreadData`.

revskill 4y ago

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

freilanzer 4y ago
Why would I ever want to extend a type with null? That's exactly the opposite of what I want of a type system in the first place.
- evomassiny 4y ago
  the type `null | true | false` is different from `true | false`, a type checker can assert that you handle the `null` case before using a function that wants a boolean. This is how rust handles it (with the Option<T> type).
  - harperlee 4y ago
    In particular, you may want this to signify “I dont know” with NULL, just as in SQL. See the Wikipedia page for ternary logic for more info.
    - alexvoda 4y ago
      Note that 3VL (3 valued logic) is one of the more criticized aspects of SQL. 3VL is a gigantic leap of of complexity over 2VL (boolean). The number of possible operations is a lot higher and the choice of operations is not standardized. To quote wikipedia: "In two-valued logic there are 2 nullary operators (constants), 4 unary operators, 16 binary operators, 256 ternary operators" And we all agree which of those 16 is named what. "In three-valued logic there are 3 nullary operators (constants), 27 unary operators, 19683 binary operators, 7625597484987 ternary operators" There is no standard meaning of the 3'rd value and of the operations involving it. That is not to say that 3VL isn't useful. I believe the reason for the criticism of 3VL in SQL it that the system made those choices for you and those choices are not always intuitive. Therefore a null in one attribute in one relation might mean something very different from a null in another attribute in another relation. Also note that as opposed to digital signal processing (where binary and ternary refer to the number of possible values a bit/trit can have), when discussing logic arity (nullary, unary, binary, ternary, n-ary) refers to the number of arguments required by a function as opposed to the number of values the arguments can have (univalent, bivalent, trivalent, k-valent). This is confusing because the terms are used interchangeably.

ghostwriter 4y ago

How does it interop with the existing Java libraries?

nerdponx 4y ago
I can't speak for the JVM backend specifically, but in general Idris 2 code can call arbitrary functions in the backend with the "%foreign" pragma. So hopefully that would be supported for Java, although I don't know how it would work with classes.
mmhelloworld 4y ago
This file https://github.com/mmhelloworld/idris-jvm/blob/main/libs/base/System/Concurrency.idr https://github.com/mmhelloworld/idris-jvm/blob/main/libs/bas... demonstrates how the interop looks like currently. The `%foreign` directive takes an FFI descriptor to talk to the respective backends. Here you can see few scheme and JVM descriptors starting with "scheme:" and "jvm:" respectively. The JVM descriptors there show constructor calls `<init>`, instance methods `.lock` and static methods `getThreadData`.

bsaul 4y ago

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 ?

nerdponx 4y ago
Idris 2 does compile to C, but it uses its own reference-counting garbage collector and cannot currently be used to generate libraries. I believe this limitation is true for all of the compiler targets right now, except maybe Javascript (some work was actively in progress on this when I last checked).

zelphirkalt 4y ago

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

pjmlp 4y ago
Naturally it doesn't have TCO on JVM, at least not natively as bytecode representation for it. The only possibility is to rewrite the code in similar way as clojure and Scala do it.
- catiopatio 4y ago
  Which, to be clear, is not a zero-cost mechanical translation, and can be tricky and annoying when you start talking about things like generic monad transformer stacks.
otto-edgar 4y ago
I think TCO and JVM are orthogonal discussions -- by the time the bytecode is generated, the TCO may have already been performed.
- nerdponx 4y ago
  I'm actually not sure about that. I think the Javascript compiler target also lacks full TCO. The Idris 2 compiler itself I think does not perform this optimization, because the Scheme reference backend does it already. I might be wrong about that, but I remember several active unresolved discussions on this topic in the community last year. I haven't been involved actively in it for several months, so my memory might be wrong.
  - dunham 4y ago
    The javascript back end handles mutually recursive tail calls. It finds connected components and rewrites them to use a trampoline-like thing. There is a nice explanation of how it works at the top of the file: https://github.com/idris-lang/Idris2/blob/main/src/Compiler/ES/TailRec.idr https://github.com/idris-lang/Idris2/blob/main/src/Compiler/... One could argue that it's not "full" TCO, but it does cover a lot of use-cases. That rewrites to NamedCExp, so it could be reused by other backends. The Java backend seems to be doing its own thing. There aren't a lot of comments or documentation in that repository, but I do see evidence that it's doing something interesting in src/Compiler/Jvm/Optimizer.idr: Pure $ if shouldTrampoline && hasNonSelfTailCall tailCallCategory then trampolineExpression True inlinedAndTailRecursionMarkedExpr else inlinedAndTailRecursionMarkedExpr

IncRnd 4y ago

This link to the latest readme.md may be helpful. https://github.com/mmhelloworld/idris-jvm/blob/latest/README.md https://github.com/mmhelloworld/idris-jvm/blob/latest/README...

exabrial 4y ago

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

saghm 4y ago
Have you used Haskell before? It seems almost identical syntactically at a glance, so I'm curious if that's what you mean by "what they were trying to do" or if it's your first time seeing syntax like this at all.