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!)
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.
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.
Including appropriate casts, and Num/Eq/Ord/Show implementations.
Also includes new primitives in Data.Buffer, and calls to foreign
functions in C as 'unsigned'.
This means it abstracts over the value syntactically, rather than by
value, and can significantly speed up elaboration where large types are
involved, at a cost of being less general. Try it if "with" is slow.
There are more flags we want on with (well, at least one: "proof")
The required totality of interface methods is now only affected if
there's an explicit modifier on the method. This allows us to set
%default total on the Prelude, which is a good thing to do anyway,
without also requiring that every implementation of the interface in the
prelude has to be total, which would potentially be a pain.
Another good affect is that it speeds up totality checking elsewhere
because totality checking is done lazily, and so with the total flag set
we know in advance that prelude functions are total.
If we're going to use assert_total. we might as well not have the
distinction between empty and non empty results, which only makes the
code harder to follow.
Also there's some kind of issue which seems to mean the token list can't
be erased if we do that. I will investigate if I can make a smaller
example.
Still a couple of things to resolve in coverage and totality checking
before we can switch on %default, so don't expect quite the right
behaviour just yet. More progress though!
Also working on this has caught a few totality errors in the Idris 2
code base that Idris 1 missed... so these are fixed on the way.
This means temporarily removing some '%default total' from the libraries
and tests, since the input for codata checking isn't right yet (it needs
appropriate use of inlining)
