Apparently the concrete syntax is controversial ("{apples}"
vs. "$oranges"), so I'm just adding a simple DYI version until we
agree on a concrete syntax
This involves updating the bootstrap code since it needs a fix in
interface resolution. It shouldn't affect the Idris2-boot build though,
since it's in the libraries not the Idris2 source.
It's worth delaying in case doing some more work (and some more
interface resolution) can make the type more concrete. This makes
test linear011 work more smoothly, and will help with this sort of
program in general.
A better way, later, would be to try elaborating and delay only if the
type is not yet known. We have the facilities, but it's too fiddly for
me to want to implement it right now...
We need to check below top level too, since there could be holes that
we're happy to resolve by searching. The linearity test added
illustrates a place where this is needed.
Doing this is awkward, for a number of reasons, including 'pure' not
being linear in its argument - there's no guarantee it'll be used
linearly after all - and lack of multiplicity polymorphism. Fortunately
the user doesn't have to know about the ugliness underneath!
We can look at ways to make it less horrible later :). For now, this is
starting to look like something that allows us to write linear protocols
without too much extra machinery on top of IO.
Conditional variables with timeout in Chez didn't work, so changed to a
consistent meaning of the timeout (microseconds). Also fix linearity of
unsafePerformIO.
Following a fairly detailed discussion on slack, the feeling is
generally that it's better to have a single interface. While precision
is nice, it doesn't appear to buy us anything here. If that turns out to
be wrong, or limiting somehow, we can revisit it later. Also:
- it's easier for backend authors if the type of IO operations is
slightly less restrictive. For example, if it's in HasIO, that limits
alternative implementations, which might be awkward for some
alternative back ends.
- it's one less extra detail to learn. This is minor, but there needs to
be a clear advantage if there's more detail to learn.
- It is difficult to think of an underlying type that can't have a Monad
instance (I have personally never encountered one - if they turns out
to exist, again, we can revisit!)
Backed by Data.IOArray. Also moved the array external primitives to a
separate module Data.IOArray.Prims, since the next step is to add a
linear bounded array type where the bounds checks are done at compile
time, so we'll want to read and write without bounds likes.
Having unsolved holes in a 'core' library unneccessarily pollutes the list of holes shown to the user.
Thus, having unfilled holes in a 'core' library is not right.
These constructs can be re-added once the holes have been filled in.
I'm playing with some linear structures and finding these useful a lot,
so good to have a consistent syntax for it. '#' is chosen because it's
short, looks a bit like a cross if you look at it from the right angle
(!) and so as not to clash with '@@' in preorder reasoning syntax.
Meaning that the FFI is aware of it, so you can send arbitrary byte data
to foreign calls. Fixes#209
This means that we no longer need the hacky way of reading and writing
binary data via scheme, so can have a more general interface for reading
and writing buffer data in files.
It will also enable more interesting high level interfaces to binary
data, with C calls being used where necessary.
Note that the Buffer primitive are unsafe! They always have been, of
course... so perhaps (later) they should have 'unsafe' as part of their
name and better high level safe interfaces on top.
This requires updating the scheme to support Buffer as an FFI primitive,
but shouldn't affect Idris2-boot which loads buffers its own way.
This involves new primitives GCPtr and GCAnyPtr which are pointer types
that have finalisers attached. The finalisers are run when the
associated pointer goes out of scope.
In the test, I am assuming that the GC will only be called once, right
at the end. Otherwise, the output isn't guaranteed to be deterministic!
Let's see how this assumption holds...
This is currently Chez only. I think it'll be easy enough to add to
the Racket and Gambit back ends too.
