Web Adventures in Typed Racket
Jesse Alama organized the latest installment of Racketfest in February 2020 – and for some reason that eludes me he asked me if I wanted to give a talk. I decided to talk about Typed Racket, since I had started to move one of my online experiments in economics from plain Racket to Typed Racket code. This blog post is based on that presentation and describes the issues in more detail.
To illustrate the issues I had with gradual typing – gradually moving from untyped to typed code – I created a toy website:
- It shows the time left until (or since) the end of the talk,
- has a button to add questions,
- and stores those questions on the filesystem.
The code for this website, and the patches for typing it, is available on my github repo. The code on the master branch is untyped, and the branch typed-racket has the commits that gradually type parts of the website.
Gradual typing, one commit at a time
During my talk, I moved forward one commit at a time, explaining the code changes. Initially I had wanted to live code, but I was certain that I’d screw something up, so I decided for this workflow instead. I followed this blog post to set a git alias to move quickly to the next commit. If you want to follow along one patch at a time, clone the git repository and define a git alias
git config --global alias.next '!git checkout `git rev-list HEAD..demo-end | tail -1`'
Then when you type
git next at the command line, you will check out the next commit.
Aside on git slides instead of live coding
Initially I wanted to live code, but decided against it for three reasons:
- I will screw up, losing between 30 seconds and 5 minutes to fix things
- I will forget how to do some step
- I may take far too long writing some of the boilerplate, such as
On the other hand, slides are as bad for presenting code as they are for presenting maths: one zips through way too fast, trivial parts get too much attention, hard parts get none, and because the slide appears fully formed on the screen, the audience has no idea where to focus their attention. By using small commits, I was hoping to have a similar dynamism and gradual explanation as if I coded live, while guaranteeing that I wouldn’t screw up the code – as long as I tested it before.
I should have asked for feedback, but my own impression was that it worked OK in these respects. However, I ended up rushing through the code – because I wanted to ‘cover’ too much material – and for some of the commits it wasn’t clear what had changed. Some feature that highlights what has changed might be useful. Yes, I know about diff, but it is –pleasant on the eyes– ++a horrible eyesore++. Besides, it hides the context so much that it’s again hard to figure out what’s going on.
Next time, I will try a mixture of live coding, with the git repository as a fallback and a way to fast-forward through boilerplate.
Let’s get Typing!
The website consists of several files
server.rkt which deals with the requests and passes them on to the handlers (
handlers.rkt). That one in turn requires the glorious database
db.rkt, as well as the
We’ll start typing
handlers.rkt, and we will do this one function at a time. The way we do this is that we define a
handlers.rkt and move a function that we want to type into this module. Thus our first step consists in going from this code:
#lang racket (provide home question question-post) (require "db.rkt" "tools.rkt" "formlets.rkt" gregor ... ) (define talk-end-time (datetime 2020 02 27 12 0 0)) ;;; MORE BELOW
#lang racket (provide home question question-post) (require "db.rkt" "tools.rkt" "formlets.rkt" gregor ... ) (module this-is-typed typed/racket ; TODO: Type annotations needed (define talk-end-time (datetime 2020 02 27 12 0 0)) (provide-all-out)) (require 'this-is-typed) ;;; MORE BELOW
The first argument to
module is the module name, the second is the module’s language – here
typed/racket. We then
provide-all-out and then require this typed module via
(require 'this-is-typed). By running
raco make server.rkt, we compile and thus also type check our website. If you run
raco make server.rkt at this point, it will fail to type check, since Racket can’t figure out what type
talk-end-time is created with
datetime imported from the untyped
gregor library. After some digging around, I found out that
gregor defines a
datetime struct, and it is straightforward to define types based on structs if the whole struct is provided. But
gregor doesn’t provide the full structure, but only the constructor
datetime and structure predicate
datetime?. In this case, we need to use (opaque types)[https://docs.racket-lang.org/ts-guide/typed-untyped-interaction.html#%28part._.Opaque_.Types%29] via the
#:opaque clause of
require/typed, used as follows:
(module typed typed/racket (require/typed gregor [#:opaque Datetime datetime?] [datetime (-> Integer Integer Integer Integer Integer Integer Datetime)]) (define talk-end-time (datetime 2020 02 27 12 0 0)) (provide (all-defined-out)))
This defines a new type Datetime, with
x being of type Datetime if
(datetime? x) returns
#true. Moreover, it defines
datetime as a function that takes 6 values of type Integer and returns a value of type Datetime. Following this small change, I check that the code works by running
raco make servers.rkt – mapped to
<leader>m in my .vimrc.
Next I move the definition of
time-left into the typed bubble, and in order to make it work, we need to
require/typed the definition of
now and of
minutes-between. We end up with
(module typed typed/racket (require/typed gregor [#:opaque Datetime datetime?] [datetime (-> Integer Integer Integer Integer Integer Integer Datetime)] [minutes-between (-> Datetime Datetime Integer)] [now (->*  [#:tz String] Datetime)] ) ...)
Next up, we move the definition of
home into the typed bubble, for which we need to define some
Response types, conveniently defined in the typed version of
typed/web-server/http. It’s worth checking out whether a given library has a typed equivalent in the Typed Racket repo
(module typed typed/racket (require typed/web-server/http) ; Provides Response, Request, etc (require/typed "tools.rkt" [response/wrap-xexpr (->* [#:xexpr Any #:title String] [#:wrap-body? Boolean] Response)]) (require/typed "db.rkt" [time-and-question-string (-> Integer String)] [db-keys (-> (Listof Integer))]) (: home (-> Request Response)) (define (home req) (response/wrap-xexpr #:title "Home Page" #:wrap-body? #t #:xexpr `(div (h1 "Home Page") (p "This is the home page.") (h3 "Time left: " ,(number->string (time-left)) " minutes") (a ((class "btn btn-default") (href "/question")) "Add question") (h3 "Previous questions") (ul ,@(for/list ([k (db-keys)]) `(li ,(time-and-question-string k)))) ))) ...)
In addition, I require
tools.rkt, which is a simple helper function that uses
response-xexpr by wrapping some boilerplate CSS that I add to almost all my pages. The
(->* ...) notation defines a function type that can have optional arguments, keyword arguments, or some forms of rest arguments.
However, at this point the code doesn’t typecheck. Instead we get the following error:
Type Checker: Error in macro expansion – insufficient type information to typecheck. please add more type annotations in: (for/list ((k (db-keys)))
This is an interesting error message, for a few reasons. Racket’s type checker apparently can’t figure out what type
for/list is, even though its body should make it clear that it returns S-expressions, and that
response/wrap-xexpr is happy to consume things of any type. So as long as
for/list returns a list, it should be fine - yet the Racket type checker complains. This is quickly resolved by annotating the
for/list as follows:
,@(for/list : (Listof Any) ([k (db-keys)])....
As a rule of thumb, I recommend you always annotate for loops and the like. Given that they are macros, they seem to be more prone to throwing weird type errors. In fact, at this point I annotate almost everything by default, because it avoids weird error messages and serves as decent documentation.
Next, we add the
question handler, which type checks without a hitch, followed by
question-post, the handler displaying the form to enter a question and submit it.
(module typed typed/racket ... (require/typed "formlets.rkt" [display-question (-> Any)]) (define (question req) (response/wrap-xexpr #:title "Question Page" #:wrap-body? #t #:xexpr `(div (h1 "Question Page") ,(display-question)))) (require/typed "db.rkt" ; Not entirely obvious. It is the return value of `(close-output-port...)`, which is Void [save-time-and-question (-> Datetime String Void)]) (require/typed "formlets.rkt" [get-question (-> Request String)]) (require/typed web-server/servlet [redirect/get (-> Request)]) (define (question-post req) (save-time-and-question (now #:tz "Europe/Berlin") (get-question req)) (home (redirect/get))) )
question type checks,
question-post does not and throws an error:
Type Checker: type mismatch expected: request given: Any in: req
This is because we pass on the variable
get-question, and the type checker has no way of knowing that it is of type
Request. We quickly fix this
(module typed typed/racket ;... (: question-post (-> Request Response)) (define (question-post req) (save-time-and-question (now #:tz "Europe/Berlin") (get-question req)) (home (redirect/get))) )
and we have completely typed the file.
Now that the whole file is typed, we can get rid of the
typed module, and instead switch from
#lang racket to
#lang typed/racket (provide home question question-post) (require/typed gregor [#:opaque Datetime datetime?] [datetime (-> Integer Integer Integer Integer Integer Integer Datetime)] [minutes-between (-> Datetime Datetime Integer)] [now (->*  [#:tz String] Datetime)] ) ;; etc etc.
Finally, since we might need to import
datetime more often, it makes sense to define our own typed file called
subset-gregor-typed.rkt that does all the
require/typed business. That way, we can replace all the
require/typed gregor ... clauses by a simple
#lang typed/racket (require "subset-gregor-typed.rkt") ...
and “subset-gregor-typed.rkt” looks as follows:
#lang typed/racket (require/typed gregor [#:opaque Datetime datetime?] [datetime (-> Integer Integer Integer Integer Integer Integer Datetime)] [minutes-between (-> Datetime Datetime Integer)] [now (->*  [#:tz String] Datetime)] [datetime->iso8601 (-> Datetime String)] ) (provide Datetime datetime? datetime minutes-between now datetime->iso8601)
This workflow can be continued until all the files that you want to move to typed code are ported, but it doesn’t require you to do it all in one huge and bug-prone port.
All in all, the above workflow is rather nice and I am planning on using it more moving forward. What is not clear in the above is how much easier it gets to use typed/racket, the more of your libraries are already in typed code, since then a simple
require is all you need to do.