3 ms·

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

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
mmhelloworld 4y ago
In the JVM backend, recursive calls are eliminated with loop. There is an option to enable trampoline for functions but I am currently working on replacing mutual recursion with loops so with that the trampoline option might be removed. As for data structures, there are Idris data structures like `List`, `SortedSet`, `SortedMap` etc. but only Idris `List` currently implements Java `List` interface.

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

mmhelloworld 4y ago

In the JVM backend, recursive calls are eliminated with loop. There is an option to enable trampoline for functions but I am currently working on replacing mutual recursion with loops so with that the trampoline option might be removed. As for data structures, there are Idris data structures like `List`, `SortedSet`, `SortedMap` etc. but only Idris `List` currently implements Java `List` interface.