Abstract over FFI

[nightscape]

Nothing to see here yet, but I'd like to use this PR as a starting point for discussion.
@mmhelloworld has achieved the amazing feat of getting Blodwen to compile on idris-jvm:
mmhelloworld/idris-jvm#79
In order to do this, he had to make some changes to Blodwen itself:
mmhelloworld@1de49a9
These changes modify the code to work with idris-jvm, but take away the possibility to compile using native Idris.
I've been reading up on how one could make this compatible with both C and JVM FFI. The recommended way seems to be algebraic effect types (see section 4.4 here and the corresponding section in the official documentation).
I think I understand the basic principles, so this might be something where I could contribute.

@edwinb do you agree this is the right approach?
If so, I would give this a shot and start introducing algebras like FileSystem that can then be implemented by both C and JVM FFIs.

[edwinb]

We should be supporting multiple back ends, and dealing with multiple FFIs, though I'm no longer convinced that the type based approach from Idris 1 is the best way especially since it doesn't do anything about primitives which only work on a subset of the targets. And I think @mmhelloworld's patches illustrate the problem nicely - ideally there shouldn't be any need to do anything clever, but rather it should be a backend's job to say "sorry I can't do this", possibly with some source annotations to direct compilation on different back ends.

If it was only about FFI calls I think this would be fine. But having some primitives which only work on some backends (e.g. forking, or different primitive values being supported on different hardware) complicates things some more.

[nightscape]

So would you change the Idris 1 implementation of FFIs or do your comments refer to how you would do it in Blodwen/Idris 2?
If the latter, then until Blodwen is self-hosting, the algebraic effects would still be the way to go, right?

[edwinb]

Ah, you mean for the Idris implementation in Blodwen, I see. This is going to get confusing ;).

I think the simplest way to go here would be to find the smallest set of IO operations which the Core type needs to support, and have an interface which could be implemented for both IO and JVM_IO. This is something that needs tidying up anyway (Core really shouldn't allow arbitrary IO, it only needs console and file IO, and even then only in some very specific places). I'm trying to use the minimum number of libraries for Blodwen (mostly to make self-hosting easier in the end) and I'd rather avoid using things like algebraic effects where we really don't know the right way to do it yet.

One challenge is that Core is the fundamental structure throughout Blodwen, and it's hand specialised for efficiency (the Idris compiler isn't very good at doing this itself) so supporting JVM_IO in some nice neat abstract way runs the risk of slowing everything down. It's still worth a try, but we'd need to see the effect on performance.

I had an earlier version using ST (kind of similar to Effects) but that was about 3 times slower than the current implementation, which is too much of an overhead to bear, hence the current hand specialised version.

Given all that, maybe the simplest solution to supporting JVM for Blodwen (rather than a patch which changes IO to JVM_IO everywhere) would be some kind of configuration module which exports either

BIO : Type -> Type
BIO = IO

or

BIO : Type -> Type
BIO = JVM_IO

depending on which version you want.

[nightscape]

@edwinb something like this (ignoring the tampering of the build files which I yet have to make more generic)?

[nightscape]

@edwinb @mmhelloworld this is taking some form.
Now would be a good time to veto or make proposals if I'm running in the wrong direction 😉

[edwinb]

Hi, sorry to keep you.

I think this is fine especially if it helps keep the JVM build going, as long as the default in this repo remains the C version. The main thing I'd say as a thing to beware of is that I'm unlikely to maintain the JVM version myself, so if I ever do anything that makes it stop working then someone else will need to fix it.

Also, I doubt this'll be an issue, but I'd also like to check that there's no signficant reduction in performance of the C version before I merge it in. It seems really unlikely that'll happen, but always good to check.

[nightscape]

Here's a quick performance comparison using

time bash -c "make ; make clean ; make ; make clean ; make ; make clean"`

master:

2459,44s user 46,04s system 108% cpu 38:25,52 total

abstract_over_ffi:

2442,95s user 46,50s system 108% cpu 38:07,56 total

From first glance, it looks like it doesn't have a negative impact.
Regarding the maintenance of the JVM version: I could make simpler adaptations to the CompilerRuntime, but for advanced stuff @mmhelloworld would have to chime in.
I think having an automated CI build for both platforms would be immensely helpful to see when stuff breaks.

[mmhelloworld]

Thank you @nightscape and @edwinb . As for maintaining the JVM version, I would be happy to help there wherever possible.

[nightscape]

I fixed the incorrect JVM chmod implementation and rebased on the latest master.
@edwinb from my side this is good to merge 😃

[zaoqi]

This branch has conflicts that must be resolved

[nightscape]

Yes, I'd need to rebase my branch in order to make it mergeable again.
@edwinb from your Twitter feed it looks like you are investigating a different approach.
If successful, would that make Blodwen obsolete?
If not, would you mind having a look at this PR and tell me if you'd be willing to merge it once updated to master?

[zaoqi]

@nightscape

@edwinb from your Twitter feed it looks like you are investigating a different approach.
If successful, would that make Blodwen obsolete?

where?

[clayrat]

@zaoqi probably here: https://twitter.com/edwinbrady/status/1119675651181699072

[edwinb]

I'm trying something a bit different in the core for representation of metavariables, which I'll make public soonish, and while I'm at it I'm taking the chance to fix some of the mistakes in Blodwen (e.g. not propagating source code locations into the core representation, slow representation of names, needlessly complicated implicit name handling, ...). It was mostly something I did as a distraction from teaching this last semester. I haven't said this publically before now, but I now think it's the right way to implement Idris 2, so I probably won't do much with Blodwen except as a (very useful) source of how to implement things. I was thinking that once I'd worked it out, I'd edit the changes back into Blodwen, but I think the elaborator is just a bit too different now for that to be worth it.

Since most of the support code is from Blodwen and more or less unchanged (but for some small simplifications), this approach to abstracting over FFI will work the same way.

It's probably best to think of Blodwen as an experiment in learning how to write a dependently typed language in the type-driven style. It's got a bit further than I intended at first, but there's lots of valuable lessons learned (for me at least) and a lot of the higher level code is reusable (as long as you count copy, paste and edit as some kind of reuse).