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

1. I will screw up, losing between 30 seconds and 5 minutes to fix things
2. I will forget how to do some step
3. I may take far too long writing some of the boilerplate, such as (require/typed ...)

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

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
#:wrap-body? #t
#:xexpr (div (h1 "Home Page")
(h3 "Time left: " ,(number->string (time-left)) " minutes")

(a ((class "btn btn-default")
(href "/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.

### Cleaning up

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.

#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 (require "subset-gregor-typed.rkt"):

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

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

1. I took the idea of using a typed module and slowly moving code there from Ben Greenman’s Tutorial: Zero to Sixty in Racket, which has lots of goodies.

##### Marc Kaufmann
###### Assistant Professor in Economics and Business

I do applied theory in behavioral economics, currently focusing on projection bias and narrow bracketing. On the applied side, I measure these biases experimentally. On the theory side, I explore how they affect work and study decisions, with a focus on implications for education and personnel management.