Assertions and irrecoverable runtime errors #158

ppolesiuk · 2024-11-22T20:53:25Z

This commit introduces three functions to the standard library:

runtimeError for raising fatal errors in impossible cases or in case of gross violation of function preconditions.
assertImpossible for indicating impossible branches
regular assert function

All these function are pure, so they should not be called at runtime of a correct program.

Resolves #157

This commit introduces three functions to the standard library: - `runtimeError` for raising fatal errors in impossible cases or in case of gross violation of function preconditions. - `assertImpossible` for indicating impossible branches - regular `assert` function All these function are pure, so they should not be called at runtime of a correct program.

Foxinio

Marked two minor changes i would prefer, but aside from that all seems good. Maybe if we decide to add reflection (like macros evaluating to filename, line number, etc) this module could be revisited.

Foxinio · 2024-11-24T18:49:01Z

src/Eval/External.ml

@@ -55,8 +55,12 @@ let int64_cmpop op = int64_fun2 (fun x y -> of_bool (op x y))

 let str_cmpop op = str_fun (fun s1 -> str_fun (fun s2 -> of_bool (op s1 s2)))

+let runtime_error msg =
+  failwith ("Runtime error: " ^ msg)


I don't think this should be implemented using failwith. Triggering this function will result in output:

Fatal error: exception Failure("Runtime error: Assertion failed")

Personally i think it should be Just Runtime error: Assertion failed, so this code should be changed to eprintf + exit 1

I would add possibility to add custom error code/number on exit.

I agree that this error should not be implemented with failwith. Maybe a custom exception that is handled in the main file would be better? The REPL implementation could catch this exception and recover with a prompt for an another command, instead of aborting the interpreter.

Actually that would probably be best

I don't know and possible I am wrong but this sounds like an error implementation which we would make in standard library.

Do you mean the issue #130? I think these two are two different things. In this PR we talk about errors that should never occur in correct programs (but unfortunately, most of programs are incorrect), so the effect of such error is pure ([]). In #130 the error has some effect visible in types. However, after merging this PR, we may rethink if we still want to implement #130.

However, I realized that catching runtime error in REPL is not as trivial as I thought. It is not just adding extra match clasue in Eval.ml, because the exception are catch before the evaluation. I think it is still possible to handle it correctly, because the evaluator is in CPS, but it would be a more complex change, and should be done in a separate issue.

lib/Base/Assert.fram

Foxinio · 2024-11-27T17:08:15Z

I think we should have default ~onError in prelude that just calls runtimeError. After that it's all good to go.

Foxinio

One thing to fix, and in my opinion PR is ready to merge

src/Eval/External.ml

forell · 2024-12-13T13:16:56Z

I brought this PR up to date with master and made some small changes based on the discussion we had.

I got rid of the program-ending version of Int64.toInt and made the Option variant the default. The failing version could be reintroduced as toIntUnsafe or something, but I think it's nicer to minimize the number of such "unsafe" functions, so...
I added Base.Option to the standard library, with two methods to unwrap optionals: unwrap (unsafe, uses runtimeError) and unwrapOr (takes a default value as an argument). I'm open to other names for these methods, I just went with what Rust uses. Also, unwrapOr is similar to the various implicit-based *Err functions that exist in the standard library, except the argument is not named and not a function. The proposed version is convenient for short expressions like n.toInt.unwrapOr 0, though.
The get method for strings remains unsafe. Littering code using indexing with unwraps or long method names would be too noisy when it's normally used in a context where the bounds have already been checked by the programmer. Safe variants that allow for recovery could be introduced.

ppolesiuk

I agree with the changes, and generally, I approve this PR (this PR is created be me, so GitHub forbids me from approving it formally). I have some minor comments (below), that I would like to have discussed, but not necessarily implemented.

ppolesiuk · 2024-12-13T20:42:47Z

lib/Base/Int.fram

-  else (extern dbl_divInt : Int -> Int -> Int) self n
+pub method div (n : Int) =
+  assert {msg="Division by zero"} (n != 0);
+  (extern dbl_divInt : Int -> Int -> Int) self n


I have a philosophical question: is the type of this extern correct? Or should it be Int -> Int ->[] Int? The decision will to influence the overall type of this method (because it uses assert), but in the potential optimizing compiler can we assume that this function always terminates correctly?

The same question applies for some other function modified in this PR.

Well the effect in this case doesn't come from the extern, but from assertion, so in my opinion it works both ways.

ppolesiuk · 2024-12-13T21:00:25Z

lib/Base/Option.fram

I agree with these two methods, and proposed names are fine. I think, the unwrapErr function is missing. As a use case, consider that we have some polymorphic ~onError implicit in the context, so we can write a code optimistically using *Err functions without explicit error handling, but we still can recover from an error in some handler.

Moreover, other methods and functions for manipulating Option type, like map, fold, iter, etc. are missing, but the can be added as a separate issue.

ppolesiuk · 2024-12-13T21:03:36Z

lib/Base/Option.fram

+
+{## For `Some x` returns `x`, otherwise the provided argument is returned.
+ #}
+pub method unwrapOr default =


I was wondering, if the default parameter should be named, because in almost all cases it will be provided. But I think, the proposed interface is good: the name of this method suggests what is the meaning of its first parameter, and writing code like x.unwrapOr {default = 42} would make some unnecessary noise.

Yeah, I had the same dilemma here and came to the same conclusion.

Alternative (although I don't know how good) would be for unwrap to take optional argument default.

Functions unwrap with optional parameter and unwrapOr have different effects. The latter is more pure (-> instead of ->[]).

MinionJakub

It looks good.

Foxinio

I agree that more Option functionality should be added, and can be done in separate PR. And beside that, all changes look good and should be merged.

ppolesiuk added 2 commits November 22, 2024 21:46

Merge branch 'master' into 157-irrecoverable-errors

f43a86e

ppolesiuk requested review from MinionJakub and Foxinio November 24, 2024 18:36

Foxinio reviewed Nov 24, 2024

View reviewed changes

Runtime error as a special exception

46453dc

ppolesiuk requested a review from Foxinio November 25, 2024 15:34

Foxinio reviewed Nov 28, 2024

View reviewed changes

src/Eval/External.ml Outdated Show resolved Hide resolved

ppolesiuk assigned forell Dec 10, 2024

forell added 3 commits December 12, 2024 16:46

Merge branch 'master' into 157-irrecoverable-errors

cef6ac9

Use new comment syntax in Assert

18b0324

Add unwrap* methods for Option and some tweaks

01ac2d7

forell requested a review from Foxinio December 13, 2024 13:17

ppolesiuk commented Dec 13, 2024

View reviewed changes

MinionJakub approved these changes Dec 13, 2024

View reviewed changes

Foxinio approved these changes Dec 14, 2024

View reviewed changes

Foxinio mentioned this pull request Dec 14, 2024

Ordered Map and Ordered Set #136

Open

forell added 3 commits December 15, 2024 21:16

Merge branch 'master' into 157-irrecoverable-errors

81ce2c5

Add unwrapErr method to Option

7aacb27

Rename test

ff8cb6a

ppolesiuk merged commit b88e893 into master Dec 15, 2024
2 checks passed

ppolesiuk deleted the 157-irrecoverable-errors branch December 15, 2024 20:42

ppolesiuk mentioned this pull request Dec 17, 2024

Runtime error ( ~re ) in Prelude is unusable #131

Closed

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Assertions and irrecoverable runtime errors #158

Assertions and irrecoverable runtime errors #158

ppolesiuk commented Nov 22, 2024

Foxinio left a comment

Foxinio Nov 24, 2024

MinionJakub Nov 24, 2024

ppolesiuk Nov 24, 2024

Foxinio Nov 24, 2024

MinionJakub Nov 24, 2024

ppolesiuk Nov 25, 2024

ppolesiuk Nov 25, 2024

Foxinio commented Nov 27, 2024

Foxinio left a comment

forell commented Dec 13, 2024

ppolesiuk left a comment

ppolesiuk Dec 13, 2024

Foxinio Dec 14, 2024

ppolesiuk Dec 13, 2024

ppolesiuk Dec 13, 2024

forell Dec 14, 2024

Foxinio Dec 14, 2024

ppolesiuk Dec 15, 2024

MinionJakub left a comment

Foxinio left a comment

Assertions and irrecoverable runtime errors #158

Assertions and irrecoverable runtime errors #158

Conversation

ppolesiuk commented Nov 22, 2024

Foxinio left a comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Foxinio commented Nov 27, 2024

Foxinio left a comment

Choose a reason for hiding this comment

forell commented Dec 13, 2024

ppolesiuk left a comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

MinionJakub left a comment

Choose a reason for hiding this comment

Foxinio left a comment

Choose a reason for hiding this comment