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. Tim On Tue, Nov 7, 2017 at 10:34 AM, Martin Baker <ax87...@martinb.com> 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. >> > > 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 > > >
_______________________________________________ Axiom-developer mailing list Axiom-developer@nongnu.org https://lists.nongnu.org/mailman/listinfo/axiom-developer
