[Top][All Lists]

[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

Re: [Axiom-developer] Catching up on internals

From: Eugene Surowtz
Subject: Re: [Axiom-developer] Catching up on internals
Date: Sat, 25 Nov 2017 12:43:47 -0500
User-agent: Mozilla/5.0 (Windows NT 5.1; rv:52.0) Gecko/20100101 Thunderbird/52.4.0

OK somehow it never arrived here.


On 11/21/2017 12:07 PM, Martin Baker wrote:

Yes, Tim posted the following reply, I think saying ML-related languages also have some knowledge of partial functions.

I think I am coming around to the view that the easiest way to to prove axiom correct and get better type system, parallel code, etc. would be to put the Axiom library on top of a more modern language such as Idris but I think Tim has made it very clear he is not interested in going in that direction.


-------- Forwarded Message --------

Subject:     Re: [Axiom-developer] Catching up on internals
Date:     Wed, 8 Nov 2017 08:13:00 -0500
From:     Tim Daly <address@hidden>
To:     Martin Baker <address@hidden>
CC:     axiom-dev <address@hidden>, Tim Daly <address@hidden>

Partial function checking happens in ML-fathered languages also. It complains
when I fail to fill out a pattern match with all the cases, for example.

Proving partial functions implies a set of provisos (checks on the input).
These checks could be inserted as an 'assert' on the calling arguments
automatically. In addition, or as an alternative in a closed system, you
could prove that every caller respects the preconditions and will not ever
make a call with an invalid argument.

This is problematic in cases where the user chooses the input rather
than calls between internal functions. In that case, adding 'assert'
statements would provide a place to insert your user-level error message.


On 21/11/17 15:37, Eugene Surowtz wrote:

Did you get any response from Tim on these notes?


On 11/7/2017 10:34 AM, Martin Baker wrote:
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.


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

Axiom-developer mailing list

reply via email to

[Prev in Thread] Current Thread [Next in Thread]