ANN: idris-cil - A Common Intermediate Language backend for Idris

[Rodrigo B. de Oliveira]

Hi,

"Cross-platform compilers for functional languages" inspired me to write a CIL backend for Idris and it's been a lot of fun so far:

  https://github.com/bamboo/idris-cil

It very early stage but it can already compile HelloWorld and the generated CIL code is not too bad:

  https://gist.github.com/bamboo/4da42e1627e6e35a5620#file-helloworld-il

The ultimate goal is to be able to use Idris together with the Unity game engine.

Let me take this opportunity to thank and congratulate everyone involved with Idris, and Edwin Brady in particular for such inspiring work. I'm learning a lot.

Best wishes,

Rodrigo

  

[Echo Nolan]

Cool! Keep us updated when/if you get Unity integration working.

--
You received this message because you are subscribed to the Google Groups "Idris Programming Language" group.
To unsubscribe from this group and stop receiving emails from it, send an email to idris-lang+...@googlegroups.com.
For more options, visit https://groups.google.com/d/optout.

[David Raymond Christiansen]

Rodrigo,

This sounds really cool! Thanks so much for the pointer!

How does the FFI work? Are you planning on representing inheritance in
the FFI types?

/David

[Rodrigo B. de Oliveira]

Sure thing.

[Rodrigo B. de Oliveira]

Hi David,

FFI is the next big TODO but I haven't give it much thought yet.

First milestone will be importing/exporting static methods accepting primitive type arguments which looks easy enough and should allow for some more interesting applications. 

"Are you planning on representing inheritance in the FFI types?"

I'm still learning Idris so I'd be very curious to understand how something like that could be achieved idiomatically.

Thanks for the enthusiasm! 

Rodrigo

[Rodrigo B. de Oliveira]

I'm happy to report that Unity integration is taking shape:

  https://vimeo.com/139207756

The FFI is still a bit rough around the edges as witnessed by the amount of believing required in the source but it will get better.

Excelsior!

[David Christiansen]

This is exceedingly cool. Thanks for sending the link!

As a matter of style, when I'm dealing with foreign objects, I usually
make some wrapper datatype that doesn't export its constructor, and keep
the raw Ptr in there. Like:

abstract
data GameState = MkGameState Ptr

rather than casting Ptrs using believe_me.

/David

> --
> You received this message because you are subscribed to the Google
> Groups "Idris Programming Language" group.
> To unsubscribe from this group and stop receiving emails from it, send
> an email to idris-lang+...@googlegroups.com

> <mailto:idris-lang+...@googlegroups.com>.

[Rodrigo B. de Oliveira]

Thanks for the feedback, David!

Soon it will be possible to have the record type as part of the exported function signature effectively removing the need for those Ptr casts.

To unsubscribe from this group and stop receiving emails from it, send an email to idris-lang+...@googlegroups.com.

[Rodrigo B. de Oliveira]

The source code for that first Unity integration experiment is now online at https://github.com/bamboo/IdrisUnityPlayground in case anyone wants to play with it. 

Notice that Ptr and believe_me are no longer required when exporting data types:

https://github.com/bamboo/IdrisUnityPlayground/blob/master/Assets/Idris/src/GameOfLifeBehaviour.idr#L25

The declaration of exports is still a bit verbose at this point but I'm hoping it can be simplified with some %runElab magic in the future:

  exports : FFI_Export FFI_CIL "GameOfLifeBehaviour" []
  exports =
    Data Game "Game" $
    Fun start CILDefault $ 
    Fun update CILDefault
    End

https://github.com/bamboo/IdrisUnityPlayground/blob/master/Assets/Idris/src/GameOfLifeBehaviour.idr#L33

Your comments and suggestions are appreciated. 

[Jeremy Shaw]

Oh nice! Very excited. In fact, I was in the middle of watching Unity tutorials in another tab when I first read this announcement.

- jeremy

--