An option to omit type checks

[joskoot]

Hi,

The type checking in Racket is a big help in debugging programs and to prevent crashes that shut down the whole of the computer (as far as seen my the current user). I don't know how the most recent version of Fortran nowadays handles type-checking, but in the sixties and seventies it did not any type-checking, and programmers usually did not either. This is a big burden on debugging programs, but eventually produced fast programs. Now for Racket we have typed/racket and unsafe libraries. Typed racket remains type-checking when passing module borders. Unsafe libraries require the use of for example 'unsafe-fx+' for addition of integer numbers instead of a simple symbol '+' and may crash too, I think. (Nevertheless, with the debug option disabled, error messages point to to point of detection without references to the point of the problem proper. In that case, if it is not clear where the bug is located, I enable the debug option and run again, which usually can use me to find the cause of the problem rather than the point of its detection. )

I wonder: would it be possible to include a racket language option that omits all type checking? Probably much work, I think. I think that an option to omit all type checking can be useful for the preparation of fast racket programs. For debugging, it should be possible to disable this option, of course. That is, type checking is to be included or omitted in the expansion phase. Complicated, because expansion phases can be nested.

I know, without type checking a program may crash. In the early days we looked at a dump to see where the crash was caused (not easy). Nevertheless, how do you think about an option that allows omission of all type checks? In case of a crash enable type checking and run the program again to see where the crash came from? (Well, probably some checks should be maintained)

I look forward to your opion about this.

Jos Koot

[jbclements]

I think I'd like to suggest some alternate language here. It sounds like your main goal here is to eliminate dynamic checks, in order to make code run as quickly as possible. In fact, if I'm reading you correctly, you'd probably be in support of (what I would call) type checking insofar as it can (in some situations and in some languages) lead to the elimination of dynamic checks.

I would also like to ask a related question: you say that you're willing to tolerate crashes. Are you also willing to tolerate silently wrong answers? Suppose that you store a value at index 1000 of an index with only 900 slots; in the best case you'll get a halt, but you might instead just get silent data corruption. I think that most people would not be very happy about such a language.

(Except of course for the millions of people using C and C++ who obviously either disagree or haven't thought about it or don't have a choice.)

[samth]

For Typed Racket, you can omit checking by using typed/racket/unsafe and the unsafe-require/typed and unsafe-provide forms.

For regular Racket see (#%declare #:unsafe): 3.1 Modules: module, module*, ...

[joskoot]

To jbclements.

Thanks very much for your opinions. Very much appreciated. As far as I am concerned there is no alternative language after Racket. One important factor is that it provides very good debugging tools while developing a program. After COMPASS of CDC (unfortunately died) I never have seen such a rich system of making macros and making macros that make macros. My wish is that after debugging and testing, dynamic checks may be eliminated. Static checks at compilation time should be maintained, of course. Aye, this probably slacks up JIT. Silent errors always remain a danger, even with extensive dynamic checks. Extensive dynamic type checking does not detect all other types of errors. The second concern always remains a correct algorithm. The first concern is that you have to know what your program should implement. When programming for a third party the first concern is to find out what your customer wants. Usually the customer it/his/herself does not yet know what is wanted. That’s why I advocate starting with user documentation (and feasibility studies) before writing one single line of code.

To Sam Tobin-Hochstadt

I’ll look into (#%declare #:unsafe) Thanks for this suggestion. Never has seen it before, but it may be an option, may be also to avoid locks when running places on a multi-processor platform. I’ll try this, for it may be that just commenting in/out such declaration may include/exclude dynamic checks. I am not advocating a system that limits dynamic checks during development. In the past, many years ago, I always started writing testing programs before writing the first line of the program proper. I’m retired and nowadays program for pleasure only, but even for my own toys I usually start with a declaration of what I want and a design of data and program structure., sometimes explicitly written, other times just in my head. (In earlier discussions some people declared that a full design is not possible before starting the programming proper. I disagree strongly with them. Knowing what to program and having a proper design beforehand eliminates many problems, even simple bugs, although not all of them, of course. But a proper design beforehand avoids more essential errors.)

Thanks to you both.

Jos

[jbclements]

Ha! That was funny, I'm sorry I wasn't clear. When I said "alternate language", I was absolutely not suggesting an alternate programming language. I was instead suggesting that you describe your desire using different technical terms: specifically, that you talk about eliminating dynamic checks, rather than eliminating type checking.

More to the point, I suppose, I believe that Sam has given you most of the tools for unsafe programming that you might want.

[joskoot]

Surely I’ll look into Sam’s advice. I am not sure what is the difference between type checking and dynamic checks. I do know the difference between static checks at compile time and dynamic checks at run time. I also know the difference between explicit code for dynamic checks and checks included in the expansion and primitives behind the wall. For explicit checks in the code itself: it is easy to enclose them in macros that include or ignore the checks depending on a simple parameter, may be a few parameters when distinct levels of dynamic checks are desired. And, of course, it would be stupid to omit checks on data imported from elsewhere, for example in data read from a file, but such checks normally are needed once only and do not slow down compared to the transfer rate of input.

Thanks again, Jos

[gus-massa]

I interpreted omitting "type checks" as disabling the checks in Typed Racket, and omitting "dynamic checks" as omitting the invisible checks in (Untyped) Racket. I think it's not an official difference,

Another trick is

(require  (filtered-in (λ (name) (regexp-replace #rx"unsafe-" name ""))
                       racket/unsafe/ops))

to shadow some of the safe operations with the unsafe ones.

[joskoot]

filtered-in
I now about prefix-in and looked for a unfix-in and now you gave it. Thanks Sam.
Jos

[LiberalArtist]

Conceptually, I think it would be hard to say what operations constitute dynamic "type checking" that could be omitted, as opposed to behavior that can be relied upon. For example, you might want arithmetic operations that don't check that their arguments are number?s (and racket/unsafe/ops provides some such operations), but imagine a function like this:

(define (strange-reciprocal x)
  (with-handlers ([exn:fail:contract:divide-by-zero? (λ (e) 9)]
                  [exn:fail? (λ (e) 12)])
    (/ 1 x)))

The value of (strange-reciprocal "hello, world") is perfectly well defined to be 12, but replacing / with an unsafe variant might produce some different answer, perhaps by interpreting the address of "hello, world" as a number.

Maybe your code doesn't do anything this strange, but it seems hard to know that libraries you use, even if they are totally correct, would give the right answers if the functions they call were replaced without their knowledge with variants that never raised exceptions.

Division by zero is especially interesting because the "type checking" might be done by your CPU!

[hendrikboom3]

There is some confusion about this point.

There are two ways o running a program:
(1) with thorough checking
(2) without thorough checking.

With the second way, there is of course the possibiity that an erroneous program will behave erroneously without warning.

But history shows that this situation has oftern been tolerated in the field when the cost of run-time checks is too great for the appication workload.

This is usually provided in compilers as an option to shut off run-time checks.
Some compilers never provide such run-time checks, some optionally provide an incomplete set of run-time checks, some offer them by default, and some always perform them, For some applications, the possibility of shutting down run-time checks is a criterion for selecting the programmint language.

Independent of this is the possibility of compile-time checks, usually called static type checking. These compile-time checks are usualy not sufficient to prove that the program satisfies its specifications, but do substantially reduce teh time needed to debug the program, because each test run of the program can find many errors at compile time, but usually only one at run-time, and tracking down the cause of a run-time failure can be time-consuming.

But by using compile-time and run-time checks you can get some of the benefits of both worlds; eficient debugging or all error the compiler can catch, wne reliiable execution -- reliable in the sense that if the program fails some language-defined restriction you can be assured it will be caught, and when not caught you can use the fact that this set of problems did not occur in reasoning about any failures that did occur.

Now compile-time type checks make it possible to eliminate a lot of run-time checks -- those that have become redundant. So this is a run-time speed-up.

But thorough debugging also can make it reasonably safe to suppress run-time checks. It is a trade-off between the cost of debugging and the cost of execution. in production. This is a decision that has to be made with the risk tolerance of the application in mind.

There is a role for stringent compile-time checking and complete abandonment of run-time checking.

There is also a role for having complete compile- and run-time checking while developing and debugging a program and abandoning run-time checking in production.

I'd prefer to get all the checking I cen get on my code, and yes, I've done research on formal program verification, but I recognise that this is often not be practical.

-- hendrik

[LiberalArtist]

@hendrikboom3

There is a role for stringent compile-time checking and complete abandonment of run-time checking.

There is also a role for having complete compile- and run-time checking while developing and debugging a program and abandoning run-time checking in production.

I'd prefer to get all the checking I cen get on my code, and yes, I've done research on formal program verification, but I recognise that this is often not be practical.

I don't disagree. My point was that I think you need to be able to predict which checks might be turned off.

For example, the documentation for fx+ and unsafe-fx+ documents that both require that their arguments be fixnums and that their result would fit in a fixnum, but the unsafe version will not raise an exception if those requirements are violated. If you know those facts, you know you can not write a function like my strange-reciprocal that relies on such an exception if you are writing in a language where fx+ might be compiled to unsafe-fx+ in certain compilation modes.

Otherwise, it's not only as you said that:

@hendrikboom3

With the second way, there is of course the possibiity that an erroneous program will behave erroneously without warning.

In my strange-reciprocal example, omitting the checks from / would cause correct programs to produce erroneous results without warning.

[joskoot]

To HendrikBoom and liberalartist:

I agree with your comments. Full checking a program always is important. Failure handlers that do not reraise an exception are dangerous, of course. I am strongly in favor of checking a program as much as possible, but after checks have passed, many of them can be eliminated, I think. In the sixties and seventies interleaved writes where used. CPU detection of errors was the ultimate tool but required laborious study on dumps. A love the extensive error detection of Racket, but in some cases, after all checks passed, it would be nice to omit a lot of them. MHO. And if a crash occurs, well just run the program again with all checks enabled. Of course trying to omit checks requires testing again in a protected environment , for example in a separate account, that protects all stuff of other users, yourself included. Even better, do all the development and testing of a program in a protected environment before making it available for all users.

Thanks, Jos

[joskoot]

Oh I forgot to say that there also is a decision to be made between the costs of development and maintenance and the costs of using the program. Many years ago I made a system for random access on rotating memory including rather complicated data structures. The code of testing it was was a multiple of the code proper. Only once an error occurred after unnecessary checks were eliminated. It took me a few seconds to find the bug. This was about 1970 and all code was in Fortran IV and the most essential parts in COMPASS (comprehensive assembler). In fact I only did the documentation and design and the COMPASS programming, but almost all Fortran IV code was prepared by another person, who still is a close friend of mine.

During my studies I was a few months at work in Orsay (France) where I had to find energy levels of Erbium I and Erbium II given a spectrum of the light radiated when exciting the atoms. A program was available to do this, but it could run about an hour and then end with the message that the problem was to big. It took me 24 hours to make a much faster program without any additional run time checks other than checking the input and that could take problems as long as fitting within memory and responded within a few seconds. This program has been used by others for at least two decades after, until there no longer a computer with a compiler was available accepting my source-code. I wrote the program quickly because I needed it quickly. This may illustrate that sometimes it is possible to omit run time checks. Good design before starting coding is the best way to avoid problems. And indeed, I had a very clear idea how to structure the program. Always MHO.

[joskoot]

Notice, this was in the early seventies, writing program on hollertit cards.

[joskoot]

Even with the most extensive checking, both static and dynamic, incorrect programs may run without noticing. Especially when simply the algorithm is incorrect. Detailed design of data , program structure, algorithms and feasibility studies before writing the first line of code can help. The most important issue is that you have to know well what your program will be used for. It can occur that a student does not quite understand an exercise. In that case she/he cannot do the exercise. We have to know what to program before starting. MHO and my MHE (my humble experience). I am not advocating to omit checks, I am advocating tools to parameterize the code such as to omit check after testing and to include them again after a bug or more severe error, such as a crash, has been encountered. Jos

[sschwarzer]

@joskoot

I don't know how the most recent version of Fortran nowadays handles type-checking, but in the sixties and seventies it did not any type-checking, and programmers usually did not either.

FWIW, Fortran has gotten modules since Fortran 90 and in that case checks for matching types between caller and callee.