I’m currently using the Racket wrapped library for C library Raylib and one problem that I’m running into is that when I pass the wrong types to a function the whole program crashes. I’ve never used them before, but it seems to me like contracts would solve this problem. I could create a function with a contract, that then calls the wrapped c function in its body if the parameters check out, preventing me from accidentally crashing my program. But then I realized that’s basically like Typed Racket, so I could just make a Typed Racket Library that does the same thing, and if I decide to convert the rest of my code over to Typed Racket later, I won’t have to annotate the functions saving me work. Also my understanding is that if I used Typed Racket code in an untyped Racket program the annotated types are converted into contracts anyway.
But now I’ve confused myself. Why would you use contracts over Typed Racket? Is there any situation where one is preferred over the other? And what should I do in my case?
Typed Racket is a static check of a specification, i.e. the types of the values are checked at compile time, before your code ever runs. Contracts are dynamic checks: they are verified when the program is running. Here are some important implications of this difference:
With static type checking you offload the checks to compile time, allowing your final program to run faster.
With dynamic contract checking you can verify some finer-grained conditions on your values more easily. Note that advanced typed systems (e.g. dependent types) allow this to some degree as well.
I have no experience with foreign interfaces in Racket, but from my understanding I'd say that contracts should be able to prevent your program from crashing just as well as types, since the checks happen before the actual function is called.
Maybe you should check whether your contract catches all edge case, and especially whether it is positioned on the correct boundary. For example, if you attach a contract on a function via contract-out, the contract will not be checked if the function is called from the same module in which it is defined (7.1 Contracts and Boundaries).
Now if you are interested in Typed Racket, please do use it
In a way I like to think as types as tools to help me prove something. What is it that you are trying to prove? As an example many typed systems are about proving that you cannot have X (memory errors, data races, undefined behavior ...).
So let's say that you are sold and you want to prove something, use typed racket! If you are not trying to prove something then contracts are quite nice to catch those crash the world annoyances.
With dynamic contract checking you can verify some finer-grained conditions on your values more easily. Note that advanced typed systems (e.g. dependent types) allow this to some degree as well.
I guess that is my answer. I don’t need to dynamically check a parameter for some complicated condition, therefore Typed Racket is fine in my case. Thanks!
It doesn't look like anyone has mentioned the obvious advantage of contracts: it's very simple to add just one or two contracts. Adding contracts won't prevent your code from running. Changing to TR, though, is generally a much more time-intensive exercise.
To be clear, TR is incredibly good at interfacing with untyped code (though values that cross the typed/untyped interface frequently may wind up causing problems), but you have to choose your boundaries carefully, and (speaking from personal experience), translating to TR is kind of addictive, and can wind up eating a lot more time than you expect it to....
That's completely right! Typed Racket has progressively become richer and easier to use, but it may still be quite challenging to properly add types to some code.
