check-contract on functions that may error?

[dbp]

Some functions might have cases that are unrecoverable. e.g., eval on arithmetic, division by zero.

How should we handle this? erroring should be an acceptable possible result (at least, certain errors)...

[camoy]

I think the general approach is to strengthen pre-conditions such that the contract covers all error cases. So for division the contract would be (-> Number NonZero Number) where the generator for NonZero does not generate zero. There might be cases where this isn't feasible, but I'm not sure if that'll come up in the course. Did you have a specific one in mind?

[dbp]

Hmm. So I think the issue is that sometimes we want to express a partial specification essentially, and expressing the right precondition will amount to doing a lot of work.

I noticed this first when trying to write some things using an “eval” function on an expression language with arithmetic. I wanted to express, for example, that “eval (add e1 e2) = eval e1 + eval e2”.

Maybe it would be enough to provide a helper to catch (certain) errors? So I could write “if eval e1 does not error, and eval e2 does not error, then eval (add e1 e2) is the sum of the former”

On Fri, Dec 29, 2023, at 6:48 PM, Cameron Moy wrote:

I think the general approach is to strengthen pre-conditions such that the contract covers all error cases. So for division the contract would be (-> Number NonZero Number) where the generator for NonZero does not generate zero. There might be cases where this isn't feasible, but I'm not sure if that'll come up in the course. Did you have a specific one in mind?

— Reply to this email directly, view it on GitHub https://github.com/logiccomp/lsl/issues/12#issuecomment-1872423043, or unsubscribe https://github.com/notifications/unsubscribe-auth/AAELBJOABRD4LRW6DEJIM73YL5XGXAVCNFSM6AAAAABBG2IE7CVHI2DSMVQWIX3LMV43OSLTON2WKQ3PNVWWK3TUHMYTQNZSGQZDGMBUGM. You are receiving this because you authored the thread.Message ID: @.***>

[dbp]

To expand on this, if we had a (MayError T) contract, perhaps with a variant (MayErrorWith "message" T) (the former could be (MayErrorWith "" T), we could put that on the output. It's not a Flat contract, so would probably have to be handled specially.

[camoy]

I'm thinking the right way to go is to put an extra clause on the Function contract that lists possible exceptions. And then instead of error we have raise with an exception. I'm wondering then if exceptions should have a separate define- form or if we should just reuse ordinary structs. Thoughts?

[dbp]

Hmm. So idea is that you match exception by struct tag? I think normal structs are probably fine...

[camoy]

So it would look something like:

(define-struct div-by-zero ())

(: eval (Function (arguments [_ Expr]) (result Integer) (raises div-by-zero)))
(define (eval e)
  ... (raise (make-div-by-zero)) ...)

The syntax for Function will have to change to accommodate the extra clause.

My thought is that (MayError T) only makes sense when T is a function contract anyway, so we can avoid adding a new primitive contract form by extending Function, if that makes sense.

[dbp]

Yeah, I think this makes perfect sense.