[Agda] IO design dangers

[Tristan Wibberley]

On Mon, 2008-03-24 at 17:58 +0000, Nils Anders Danielsson wrote:
> On Mon, Mar 24, 2008 at 4:18 AM, Tristan Wibberley
> <tristan at wibberley.org> wrote:
> >
> >  I think, for the proofs in a program to hold, the requirements of the
> >  platform and language implementation must be encoded throughout said
> >  program. So if a program is written to assume a computation will
> >  complete the implementation must allocate all necessary memory (/and
> >  ensure the operating system has not overcommitted/) or, alternatively,
> >  fail to compile.
> 
> This would be very nice, but there are two problems:
> 
> 1) The amount of memory available to the program is typically not
> known at compile time. Some properties are inherently dynamic.

That's not a problem because it doesn't need to be known at compile
time, it needs to be known at input time :) And needed memory can be
calculated and allocated at that time -- a computation just needs to
have an error case for not being able to get the necessary memory. If
you write your program without allowing for said error condition then it
would be okay if the platform specification guaranteed that system
memory would be available but not okay if you tried to compile said
program for a general purpose computer.

This would be great for both systems programming and embedded systems.
If necessary you could "lie" to the compiler in the platform spec and
say that allocations always succeed and document that a device fails in
a certain situation (this would be the C/C++ recursion/stack-overflow
problem) or tell the truth and the compiler ensures you'll never fail.

> 2) I expect that keeping track of memory consumption all over the
> program will be rather heavyweight, especially if we are talking about
> real memory usage and not some abstraction.

You mean a heavyweight task for the compiler? I don't think that's such
a big job. It knows the pathways and conditions, it knows the possible
input data format, so it can write an algorithm to determine the future
memory requirements instead of combining all those bits of the algorithm
lazily as Haskell implementations do.

Obviously, it couldn't compile a computation that uses potentially
unbound natural numbers but that is quite right... you can't compile
such a program - you always have to compile a subtly different program
and lie to the programmer, saying "Great! I just compiled what you asked
me to... (sucker)".

The programmer just has to prove (I say "just"... I seem to be having
difficulty proving anything at all) that the naturals are bounded and
the programmer's proof will direct the memory calculation algorithm.

The computation abstraction just lets you prove things about the
compiler's attempt to compile your program (and can thus direct
parameters of the compilation) and what the target platform will do,
when. This would offer very great flexibility. Imagine targeting an
image processing routine at a particular hardware configuration,
programming the performance characteristics of it, and proving that you
can process a particular sized video stream in real-time regardless of
the contents of the stream.

> Having said that, there are some domains, like embedded systems, where
> doing something like this might still be worthwhile because of the
> inherent constraints of the domain. Quite a lot of research has gone
> into systems keeping track of memory usage, for instance.

Not on observational systems I'd bet. They'll just use heuristics to
examine some of the search space such that the compilation process will
terminate instead of providing a way for the programmer to prove things.
This is why agda2 and epigram excite me - I should be able to give the
implementation something to assume and have it fail until I've given it
a suitable proof.

-- 
Tristan Wibberley

Any opinion expressed is mine (or else I'm playing devils advocate for
the sake of a good argument). My employer had nothing to do with this
communication.