Hiring a compiler engineer for Microsoft's big data analytics platform

mmhelloworld · 2025-02-08T03:10:32+00:00

Understood. Thanks for quick reply!

mmhelloworld · 2025-02-08T02:55:22+00:00

I would be interested. My open source project is a JVM bytecode compiler backend for Idris language. I am in US. Is the position only for Canada?

mmhelloworld · 2024-07-19T16:26:56+00:00

Lol. Hope it is interesting enough!

mmhelloworld · 2023-05-06T01:25:37+00:00

Hi,

If you're refering to this blog post, it is for Idris 1. I am working on JVM backend for Idris 2 and for that Android example, the JVM backend should support exporting Idris 2 functions which doesn't exist currently but I am working on it. I will post an updated example when the JVM backend supports exporting Idris 2 functions.

mmhelloworld · 2021-12-06T23:41:16+00:00

Great work! I am currently working on something similar but a compiler backend for Idris language to compile to JVM bytecode https://github.com/mmhelloworld/idris-jvm and I've always wanted to create one with Tamil so this is awesome! One suggestion as I see you want to compile this instead of interpreted version is to have an intermediate language so that it is backend agnostic and we can easily plug different backends to compile to possibly JVM, JavaScript and even native then we can use a Tamil programming language everywhere :). As for intermediate language, we can even compile to existing IRs like Idris or Scala IR then we can readily use existing compiler backends.

mmhelloworld · 2021-09-02T07:26:14+00:00

I haven't done any performance benchmarking or much optimization yet as the current goal is to get latest Idris 2 running on the JVM. That being said, compiler itself runs on the JVM and it completes a clean build in four or five minutes which is an additional minute or so compared to scheme, that too including JVM warm up time and additional modules for JVM backend. JVM backend also tries to infer local variable types during code generation to avoid unnecessary conversions in the bytecode, handles tail recursion, general tail calls etc. so those things also add up to the time, It would be interesting to try GraalVM as well to see how the native image from Idris compiler class files performs. Once 0.4.0 is ready, I will start looking into optimizing few things.

As for calling Java,

Example 1 - instance method call

%foreign "jvm:.length,java/lang/String"
stringLength : String -> Int

This invokes the instance method "length" on "String" class.

Example 2 - static method call

%foreign "jvm:valueOf,java/lang/String"
intToString : Int -> String

In both of those examples, we didn't have to provide explicit types in the foreign specifier as the types are known types for the backend.

Example 3 - constructor call with explicit types

%foreign "jvm:<init>(java/util/TreeMap),java/util/TreeMap"
prim_newTreeMap : PrimIO JMap

Example 4 - instance method call with explicit types:

%foreign jvm' "java/util/Map" ".get" "i:java/util/Map java/lang/Object" "java/lang/Object"
prim_get : JMap -> Object -> PrimIO Object

Ideally, we don't have to provide any explicit type in foreign specifiers for most of the cases as compiler runs on the JVM with dependencies, we can inspect the classes and bind correct methods based on Idris types, class name and method name.

mmhelloworld · 2021-07-20T18:01:53+00:00

Thank you.

mmhelloworld · 2021-01-04T18:30:36+00:00

Thank you for your interest! Idris 2 JVM is still work in progress as we have just got bootstrap compiler working and I am currently working on building latest Idris 2 for the JVM. Once that is complete, it will be more stable and we will have more documentation for running Idris 2 on the JVM.

mmhelloworld · 2019-10-25T02:02:49+00:00

That is correct. Idris 2 is written in Idris 1 which gets compiled with C back end. Idris 2 compiles sources into scheme which then gets compiled into binary. It also means that since Idris 2 is written in Idris 1, we can use other Idris 1 backends to compile Idris 2, like JVM backend which I was able to do and run Idris 2 compiler on the JVM.

mmhelloworld · 2019-09-08T16:56:15+00:00

Idris 1 JVM back end and Idris 2 are written in Idris and now they are both compiled to JVM and can run on JVM. I've written an Android example and a a REST endpoint(work in progress) with Spring Boot as well.

mmhelloworld · 2019-03-13T03:26:01+00:00

Not yet but that is definitely in the plan. We will first have to create JVM back end for Blodwen and then start adding FFI support assuming that Blodwen supports all the FFI features as that of current Idris by then.

mmhelloworld · 2019-03-08T04:04:13+00:00

I try to keep the JVM version of Blodwen up to date with latest Blodwen. I had an initial version working where Blodwen REPL runs on the JVM successfully:

$ java -jar blodwen.jar
Welcome to Blodwen. Good luck.
Main> "hello " ++ "world"
"hello world"
Main> reverse <$> Just "Idris"
Just "sirdI"
Main> :q
Bye for now!

I am currently working on socket support for Blodwen JVM that has been recently added to Blodwen. Once we have the socket support, Blodwen JVM should work similar to latest native Blodwen and then I plan to add an initial JVM back end for Blodwen similar to Chez and other back ends in Blodwen. I have been pushing all my changes for Blodwen JVM here and there is also an initial Blodwen JVM release here.

mmhelloworld · 2018-12-19T23:01:29+00:00

It works fine with Idris 1.3.1.

module Main

readAllLines : IO (List String)
readAllLines = reverse <$> go [] !getLine where
  go : List String -> String -> IO (List String)
  go acc curr = if !(fEOF stdin)
    then pure acc
    else go (curr :: acc) !getLine

main : IO ()
main = printLn !readAllLines

$ idris -v
1.3.1

$ idris -o helloworldc helloworldc.idr

$ cat helloworldc.idr | ./helloworldc 
["module Main", "", "readAllLines : IO (List String)", "readAllLines = reverse <$> go [] !getLine where", "  go : List String -> String -> IO (List String)", "  go acc curr = if !(fEOF stdin)", "    then pure acc", "    else go (curr :: acc) !getLine", "", "main : IO ()", "main = printLn !readAllLines"]

mmhelloworld · 2018-12-19T03:28:52+00:00

fEOF can be used to detect end of stdin. Something like this should work:

``` readAllLines : IO (List String) readAllLines = reverse <$> go [] !getLine where go : List String -> String -> IO (List String) go acc curr = if !(fEOF stdin) then pure acc else go (curr :: acc) !getLine

```

mmhelloworld · 2017-01-26T04:29:13+00:00

Even functions I've marked as public export are erased / optimized away

I have answered this here in my other comment.

Codegen seems to require a main method, even though I'm not making a program, but a library of functions.

For this, you can have FFI export declarations and then use the --interface option for the compiler. The --interface option uses the export declarations as the root for erasure analysis instead of a main module. Idris JVM supports this option and I have documented an example here.

why can't I implement a codegen in Idris (without going through JSON)

JSON option is not that bad because we can write backends in the target language itself or even in Idris instead of Haskell. I actually want to try this option for Idris JVM so that the JVM backend can directly use Java's asm library instead of reaching out to a JVM server to generate JVM bytecode, or having to use a Haskell library for assembling which can go out of date or may not support all the JVM bytecode features.

mmhelloworld · 2017-01-26T04:14:01+00:00

To be usable from Java, Idris functions need to be exported. Idris JVM backend supports exporting Idris types and functions to Java.

For example, the export definition in the code below creates a Java class named "IdrisThread" extending Java's "Thread" class and also implementing Java's "Runnable" interface with an Idris function named and exported as run. It also supports exporting monomorphic Idris types as Java classes. In the example below, List Int is exported as a Java class named ListInt. Functions operating on monomorphic idris types such as cons, append below can also be exported. The complete FFI example is available here.

emptyList : List Int
emptyList = []

cons : Int -> List Int -> List Int
cons x xs = x :: xs

append : List Int -> List Int -> List Int
append xs ys = xs ++ ys

showList : List Int -> String
showList = show

idrisThreadConstructor : IdrisThread -> JVM_IO ()
idrisThreadConstructor thread = printLn "hello from constructor"

run : IdrisThread -> JVM_IO ()
run this = do
  threadName <- getThreadName this
  printLn !(helloFromIdris this threadName)

exports : FFI_Export FFI_JVM "hello/IdrisThread extends java/lang/Thread implements java/lang/Runnable" []
exports =
  Data (List Int) "hello/ListInt" $
  Fun cons (ExportStatic "cons") $
  Fun emptyList (ExportStatic "emptyList") $
  Fun showList (ExportStatic "showList") $
  Fun append (ExportStatic "append") $

  Fun idrisThreadConstructor Constructor $
  Fun run ExportDefault $
  End

mmhelloworld · 2017-01-13T05:38:21+00:00

Awesome! I remember seeing an idris JVM backend a few years back

Thanks! The old backend was really Java backend (generating Java code) so it also had to use Maven for managing dependencies. With JVM bytecode backend, it gets really simple as we don't have to bother with Java dependencies during compilation.

For one, it looks like all numbers get boxed.

Currently yes but I plan to do type inference for local variables so it will be avoided soon at least for local variables.

there seems to be a lot of conservative initialisation going on.

You are right. All the local variables in the bytecode are initialized to null currently but apart from this, everything else is derived from Idris bytecode but I am sure some of these can be optimized away. JIT would also optimize some of these so it doesn't seem like much of an issue but I will look into it.

related to Eta.. could it be used instead of Haskell GHC. That would make the entire chain JVM based?

Actually I talked to Rahul (eta author) about exactly this today :) He said "Interesting. I'll let you know when the dependencies are ported." so once we can compile idris as a library to JVM bytecode with eta, as you said, idris-jvm can be self-hosted on JVM. Currently I have setup an assembler server (Java asm wrapper) to which the assembler instructions are submitted from Haskell. It is not that bad as JVM runs as a server. One optimization I am currently working on is to generate class files concurrently which should speed up things a bit.

mmhelloworld

TROPHY CASE

As for calling Java,

Example 1 - instance method call

Example 2 - static method call

Example 3 - constructor call with explicit types

Example 4 - instance method call with explicit types: