Web Adventures in Typed Racket

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.

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 formlets.rkt.

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 module called this-is-typed inside 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

to this:

#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.¹

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 Request and Response types, conveniently defined in the typed version of web-server/http, called 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 response/wrap-xexpr from 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)))
  )

While 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 req to 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.

#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. 

#lang typed/racket

(require "subset-gregor-typed.rkt")

...

#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)

Conclusion

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.