Typed Racket v7.0 Prefab Changes/Fixes

Typed Racket v7.0 Prefab Changes

For some time now, Typed Racket has unsoundly type checked prefab structs. This bug been fixed for the Racket v7.0 release (for more info, see the relevant Typed Racket RFC and the illustrative examples in the Prefab section of the docs). If you suspect your prefab-utilizing Typed Racket code no longer type checks because of this fix, we hope the below instructions help make any necessary changes as painless as possible. We apologize for any inconvenience. If you believe there are issues/fixes that should be added to this list, please do let us know.

Typed Racket HEAD w/ a Snapshot Build

How to run Typed Racket HEAD (or perhaps a fork) on a Racket snapshot build? Try the following steps:

1. download and set up a racket snapshot (https://pre.racket-lang.org/)
2. cd to the root folder for that snapshot install
3. mkdir extra-pkgs && cd extra-pkgs
4. git clone https://github.com/racket/typed-racket.git
5. cd typed-racket
6. raco pkg install --auto -i --no-setup --skip-installed typed-racket-test
7. raco pkg update -i --auto --no-setup source-syntax/ \
                                        typed-racket-lib/ \
                                        typed-racket-more/ \
                                        typed-racket-compatibility/ \
                                        typed-racket-doc/ \
                                        typed-racket/ \
                                        typed-racket-test/
8. raco setup typed typed-racket typed-racket-test typed-scheme

Voila.

Set-theoretic Types: Brief Intro and Some Base Types

Summary:

• Semantic subtyping allows for a more complete treatment of subtyping.
• Keeping types in DNF can be convenient for checking emptiness.
• The base type portion of a DNF type is either $\top$, $\bot$, $(b_0 \vee ... \vee b_n)$ or $\neg(b_0 \vee ... \vee b_n)$.

Set-theoretic Types

Here is a simple grammar for types with set-theoretic constructors:

\begin{array}{l c l l} \tau , \sigma & ::= & b & Base \, type \, (e.g. \, Int,\, Str,\, etc) \\ & \mid & \tau \times \tau & Product \\ & \mid & \tau \rightarrow \tau & Function \\ & \mid & \tau \vee \tau & Union \\ & \mid & \tau \wedge \tau & Intersection \\ & \mid & \neg \tau & Negation \\ & \mid & \top & Anything \end{array}

In other words, it includes some simple types as well as set-theoretic operators that allow us to express logical "or" (union), "and" (intersection), and "not" (negation) along with top and bottom types $\top$ and $\bot$ (which is short for $\neg \top$).