Not a Racket user, but I know that Typed Racket is gradually typed. You can mix typed and untyped code. If an untyped value is passed as an argument to a typed function, then a “blame” system will accurately report a type error at the point of call if the untyped value turns out to have the wrong type, even if this doesn’t become apparent until later on, in which case you have to “rewind history” to report the type error at the correct location. I don’t know if accurate stack traces are reported when history is rewound (anybody know?). It’s especially tricky for functions, since in general you don’t know if an untyped function has the wrong type until you call it.
Most of what Typed Racket (the default, “deep” variant) does is indeed a comprehensive “rewind system” called “chaperons”. If you pass a function from untyped code to typed code, the function gets wrapped with contracts that will correctly assigns the blame if the output value is not the advertised type.
Chaperons for higher-order types are the main source of overheads in Typed Racket.
Hack together something that mostly works, then fix the bugs as they are found. The 2020 slides described a number of misfeatures/bugs, but these aren’t mentioned again in the 2022 slides, so I guess they are fixed.
Those “bugs” are that (deep) Typed Racket is too strict and rejects some programs with correct runtime behavior.
A decidable static type systems cannot be both sound (rejects all programs with runtime type errors) and complete (accepts all programs without runtime type errors). Typed Racket is sound, so it is not complete.
The Racket community doesn’t yet have a clean design with good semantics and good performance, just a bunch of hacks with different tradeoffs.
Aside from the “hack” verbiage, I find that mostly a fair description of what Racket people do, they do research and offer different options with different tradeoffs, but they don’t really seem to spend a lot of time forming opinions on which tradeoffs work the best in practice.
Hopefully a sound and performant design for gradual typing will eventually be implemented.
To be fair, no such gradual typing system actually exists today. The gradual typing systems of mainstream dynamic languages (TypeScript, Python’s typecheckers) are not sound, because they simply don’t inject runtime checks. They are equivalent to the “optional” variant of Typed Racket.
Hmm, there’s actually an updated slide deck: https://cs.brown.edu/people/bgreenma/resources/talks/gt-rcon-2022.pdf
And recording: https://youtu.be/OEocbRO8ua0
[Comment removed by author]
Most of what Typed Racket (the default, “deep” variant) does is indeed a comprehensive “rewind system” called “chaperons”. If you pass a function from untyped code to typed code, the function gets wrapped with contracts that will correctly assigns the blame if the output value is not the advertised type.
Chaperons for higher-order types are the main source of overheads in Typed Racket.
Those “bugs” are that (deep) Typed Racket is too strict and rejects some programs with correct runtime behavior.
A decidable static type systems cannot be both sound (rejects all programs with runtime type errors) and complete (accepts all programs without runtime type errors). Typed Racket is sound, so it is not complete.
Aside from the “hack” verbiage, I find that mostly a fair description of what Racket people do, they do research and offer different options with different tradeoffs, but they don’t really seem to spend a lot of time forming opinions on which tradeoffs work the best in practice.
To be fair, no such gradual typing system actually exists today. The gradual typing systems of mainstream dynamic languages (TypeScript, Python’s typecheckers) are not sound, because they simply don’t inject runtime checks. They are equivalent to the “optional” variant of Typed Racket.