I'm currently writing an Erlang backend for the Idris compiler. Right now I've got to the internally "primitive" operations, and would like to see an increased reliance on compiling to these primitives in the Prelude rather than using the foreign function calls that are currently used.
This would probably be a breaking change for lots of backends, so I thought I'd propose it before making any major code changes.
I'm willing to do all these changes to the C and conventional backends, I'd just like to run the idea of them past a few set of eyes before I start.
The list of current primitives (over 70) is in Lang.hs below. They cover a wide variety of functionality, most of which is mathematical operations, but there's some more important stuff about I/O: LPrintNum
, LPrintStr
, LReadStr
, LStdIn
, LStdOut
, LStdErr
.
However, if you look in the Prelude (both Prelude.idr
and IO.idr
), you'll see that these aren't really used. At the idris-level, a primitive invocation by convention is a function beginning with prim__
. Instead, in lots of places in Prelude.idr
, Idris just directly uses an FFI call to some C. These are below in Prelude.idr
(there is a single FFI call in IO.idr
, we'll ignore it for now).
It's not a massive problem, but it would be easier for code-generators to not have to special-case all the foreign functions in the Prelude. Instead, it would be easier if all these foreign calls were primitives. That way, a code generator can completely ignore foreign functions, and still know they have a system that will compile any Idris program that relies only on the prelude and basic libraries.
How do we chose what should be a primitive, and what is fine to be a FFI Call? In my opinion, anything in the prelude should just be a primitive. There are a lot of networking functions in libs/base/networking
which also use FFIs, but I think that they probably shouldn't be primitives, to keep the number of primitives as low as possible.
I propose this short list below (categorised). Where a type is intbool
that just means an integer, with 0 representing false, and non-zero representing success.
Files:
LReadChr
(args: file handle; return: char) - Read a character from that fileLFileOpen
(args: name, mode; return: file handle) - Open a file, with a given modeLFileClose
(args: file handle; return: unit) - Close an opened fileLFileFlush
(args: file handle; return: unit) - Flush a file to diskLFileEOF
(args: file handle; return: intbool) - Has the file reached EOF?LFileError
(args: file handle; return: intbool) - Have any errors occured in the stream?LFilePoll
(args: file handle; return: intbool) - Poll the file, is it ready for reading?
Processes:
LPOpen
(args: command, mode; return: file handle) - Open a process, with a given modeLPClose
(args: file handle; return: unit) - Close an opened process
Pointers:
LPtrNull
(args: pointer; return: intbool) - Is the pointer null?LStrNull
(args: string; return: intbool) - Is this the null string?LPtrEq
(args: pointer a, pointer b; return intbool) - are the supplied pointers equal?
VM:
LForceGC
(args: vm pointer; return: unit) - Force the VM to perform GC
This short list should cover all uses. Some places where symmetry is expected (LPrintChar
for LReadChar
for example), aren't needed as they can be implemented in terms of other primitives (in this case, LPrintStr
).
In an effort to improve the reusability of the current primitives, I propose that we also make the following breaking changes:
Files:
LPrintStr
- it currently only takes a string to print to stdout. Instead, I think it should also take the file handle to print to, so that this can be used for files as well as stdout/stderr.LPrintNum
- this can be removed, I think, as not only is it not currently used, but the same behaviour can be achieved through combinations ofLPrintStr
andLIntStr a
.