Creating libraries for other languages

[Nathan Ringo]

Are there any examples of creating libraries in Idris2 for other
languages to call? A quick examination of the Idris2 source didn't leave
me with the impression that this was likely to be easy, since the
codegen interface looks like it's for compiling a single closed term.

Would the best approach be to make my application's entrypoint take a
record with all the Idris items I care about in it, and have the Idris
main function just call the application entrypoint with those items?

[Edwin Brady]

Hi Nathan,

Idris 2 doesn't yet have a way to do this - there doesn't seem to be
much demand I suppose, and I haven't had a use for it myself yet. But if
you'd like some possible ideas to proceed, there's a bit about it in
section 4.5 of this (rejected) paper from 2015:
https://eb.host.cs.st-andrews.ac.uk/drafts/compile-idris.pdf

I think it's plausible that a code generator could do this the same way,
but how it works will likely be very back end dependent. Your suggested
approach sounds like it's probably easier though, for the moment, if a
bit tedious to set up.

Edwin

[Nathan Ringo]

Okay, for posterity's sake (does this mailing list get indexed by search
engines?), I got this working; I build up a big record of exports and
set it into a JavaScript global [0], use QuickJS to build it to
bytecode [1], link to the interpreter from Rust and wrap the Idris
JavaScript ABI [2], then provide some wrappers [3].

A lot of this seemed mechanical enough to do through a Rust proc macro...
Maybe next time I have too much free time, I'll write something you can
just point at a set of Idris modules and get Rust bindings out.

> section 4.5

Thankfully, doing this in terms of JavaScript lets me express whatever
polymorphism I want (as far as I've been able to tell, at least), so I don't
have the monomorphism requirement here!

It is a little unfortunate to have to bundle a JavaScript runtime, but maybe
it'd be possible to partially-evaluate most of it away if I really wanted to
put my back into it?

[0]: https://git.sr.ht/~remexre/stahl/tree/c48c6283de770d971fc7d988149bdc09db918fbc/item/langbs/core/Stahl/Main.idr
[1]: https://git.sr.ht/~remexre/stahl/tree/c48c6283de770d971fc7d988149bdc09db918fbc/item/langbs/core/default.nix
[2]: https://git.sr.ht/~remexre/stahl/tree/c48c6283de770d971fc7d988149bdc09db918fbc/item/langbs/driver/src/core/ffi.rs#L139
[3]: https://git.sr.ht/~remexre/stahl/tree/c48c6283de770d971fc7d988149bdc09db918fbc/item/langbs/driver/src/core/mod.rs