Re: [Axiom-developer] Catching up on internals

[Martin Baker]

On 04/11/17 00:42, Tim Daly wrote:
> How would you model handling errors in Spad?
>
> I do think that there might be an interesting research question of how to
> handle classes of errors in computational mathematics. I had proposed
> using Provisos to handle side-conditions on formulas. Hoon Hong and
> Chris Brown have done a lot of work on QEPCAD for handling these.
> Manuel Bronstein and I had long discussions about a SUCHTHAT domain
> for encapsulating Provisos but little code resulted as the QEPCAD work
> was still in the future at the time.

Tim,

Since you asked this question I've been thinking about it (although I 
don't claim any expert knowledge).

It seems to me that there are at least 2 types of errors:
1) An error where the programmer just does something wrong.
2) An error where a partial function is called with an invalid value.

If the program is proved correct then I assume type 1 can't happen so we 
are mainly concerned with type 2 errors.

I have been looking at a programming language called 'Idris'. This 
language classifies each function as being either 'total' or 'partial', 
if it is partial then perhaps we can say something about which inputs 
are invalid.

Of course the compiler can't always determine that a function is total 
(because of the halting problem). However, for most simple functions 
(without recursion, dependent types, etc.) it is possible (at least it 
is in 'Idris') and perhaps the other functions could be classified manually.

Of course any function could be made 'total' by returning Maybe % or 
Union(%,"Fail") but that just pushes the problem upto the next level. 
The advantage of the above ideas is that the error might be explained to 
the user in much more appropriate detail, for example:
"function x called with value y which caused division by 0"
Also it could avoid lots of error handling boilerplate code.

Martin B