[CakeML-dev] [CakeML-Dev] Exceptions in cakeML basis library

[Scott Owens]

In that case, we should definitely have a look at the Haskell standard Prelude for inspiration. I think that they tend to avoid exceptions.

Scott

> On 2016/11/28, at 06:19, Magnus Myreen <magnus.myreen at gmail.com> wrote:
> 
> I'm in favour of having as few preconditions / exceptions as possible
> for operations on lists, options, strings etc. -- Magnus
> 
> On 28 November 2016 at 15:11, Ramana Kumar <Ramana.Kumar at cl.cam.ac.uk> wrote:
>> I just realised it's probably possible to have the same HOL function both
>> produce translator preconditions and generate CakeML that raises exceptions,
>> once we have https://github.com/CakeML/cakeml/issues/181 completed.
>> 
>> So there's not really a choice to be made here. You should just write
>> functions that have preconditions where necessary, and eventually we can
>> make these translate to code that raises the correct exception. (If you want
>> to force the translator to produce a precondition, you can always use ARB in
>> your definition. It's usually better to avoid preconditions where possible,
>> though..)
>> 
>> On 28 November 2016 at 14:11, Connor Cashman <connorjcashman at gmail.com>
>> wrote:
>>> 
>>> Hi,
>>> 
>>> I’m working on creating the basis library for cakeML and Ramana told me to
>>> ask your opinions on the use of exceptions in its creation. I have initially
>>> based the library on definitions given in the standard ML basis library, but
>>> these have cases where exceptions need to be raised. My question is whether
>>> I should leave these to pre-conditions on HOL, or whether I should raise
>>> exceptions in my definitions. Usually, HOL gives pre-conditions which match
>>> the exceptions, but this is not always the case. For example, the take
>>> function, as defined in HOL’s TAKE_def, has no issue with using indexes
>>> outside of the length of the list, where SML raises an exception for this.
>>> This also often occurs in cases where SML raises exceptions for negative
>>> inputs. This could be fixed by writing new definitions for such functions
>>> but I am unsure if this is the best option.
>>> 
>>> Your opinions would be much appreciated.
>>> 
>>> Connor
>>> _______________________________________________
>>> Developers mailing list
>>> Developers at cakeml.org
>>> https://lists.cakeml.org/listinfo/developers
>> 
>> 
>> 
>> _______________________________________________
>> Developers mailing list
>> Developers at cakeml.org
>> https://lists.cakeml.org/listinfo/developers
>> 
> 
> _______________________________________________
> Developers mailing list
> Developers at cakeml.org
> https://lists.cakeml.org/listinfo/developers