Re: Catching up on internals

OK somehow it never arrived here.

Gene

On 11/21/2017 12:07 PM, Martin Baker wrote:
> Gene,
> 
> 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.
> 
> Martin
> 
> -------- Forwarded Message --------
> 
> Subject:     Re: [Axiom-developer] Catching up on internals
> Date:     Wed, 8 Nov 2017 08:13:00 -0500
> From:     Tim Daly <[email protected]>
> To:     Martin Baker <[email protected]>
> CC:     axiom-dev <[email protected]>, Tim Daly <[email protected]>
> 
> 
> 
> 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 21/11/17 15:37, Eugene Surowtz wrote:
>> Martin:
>>
>> Did you get any response from Tim on these notes?
>>
>> Gene
>>
>> 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.
>>>
>>> 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
>>> [email protected]
>>> https://lists.nongnu.org/mailman/listinfo/axiom-developer
>>>
>>>
>>
>>
> 
> 
> 


_______________________________________________
Axiom-developer mailing list
[email protected]
https://lists.nongnu.org/mailman/listinfo/axiom-developer