Home

Refinement types allow you to make expressive type declarations like “any number greater than 3 but less than 33” or “any integer that is prime”. Essentially, they are the intersection of a base type and a predicate. Breaking the type descriptions down to their requisite parts, you get something like:

Base Type: Integer Predicate: (3 < x < 33) Refinement Type: Integer and (3 < Integer < 33)

In Typed Racket, this can be translated fairly literally.

(: (Refine [n : Integer] (and (> n 3) (< n 33)))

In practice, this type would be used like so:

(define-type A (Refine [n : Integer] (and [> n 3] [< n 33])))

(: add-one (-> A Integer))
(define (add-one n)
  (+ n 1))
  
> (add-one 4)
- : Integer
5

> (add-one 55)
; main.rkt::2469: Type Checker: type mismatch
;   expected: A

Refinement types are cool, and type-theoretically interesting, but they’re also really useful.

For example, I’ve recently been working on Gemengine, a small Gemini application server. Like HTTP, Gemini has a “Redirect” response. Gemengine supports this response with a simple API:

(redirect "/home")

If, instead of specifying a "/home" redirect, you allow dynamic, user-controllable input, you’ve inadvertently introduced a vulnerability: an Open Redirect. Although minor, especially in Gemini-land, we’d rather have no vulnerabilities at all.

As a library author, it would be great to prevent this issue for Gemengine’s users. However, the obvious solution - validating or sanitizing input on the dev’s behalf - is not ideal. If we take that approach, we’re taking control away from the developer. Even worse, they may not realize we’ve done so until the application is already in production and they start getting errors.

A friendlier approach would be to type-enforce secure usage of the redirect function. This way, developers aren’t surprised, because they must consciously make the secure choice, but they also aren’t left vulnerable.

What would type enforcement look like? Well, essentially what we’re looking for is a URL path. Or, put another way, a string that, when parsed as a URL, doesn’t have a host component. This type description maps cleanly to our notion of a Refinement type.

You might expect we could define a type like this:

(Refine [n : String] (not [url-host (string->url n)]))

Unfortunately, Racket doesn’t support such arbitrary refinement definitions. However, there is a workaround.

Typed Racket allows you to integrate with untyped Racket, and provides a mechanism to specify types for your untyped code. We can take advantage of this functionality to create types defined by an arbitrary predicate.

To do so, first we need to define our untyped predicate.

; gemini-path.rkt

#lang racket

(require net/url)
(provide gemini-path?)

(define (gemini-path? url)
  (false? (url-host (string->url url))))

Then, we can require it in Typed Racket.

; types.rkt

#lang typed/racket

(require/typed "gemini-path.rkt"
  [#:opaque Internal-Gemini-Path gemini-path?])

The require/typed function above allows us to specify an opaque type name along with a predicate that returns true for some input.

The only problem with the type as defined is that it has no notion that it is also a String. That means if we have some function that returns an Internal-Gemini-Path, we can’t use it in places we ought to be able to. To get around this issue, we can add one more line and complete our type definition.

(define-type Gemini-Path (Refine [s : String] (: s Internal-Gemini-Path)))

We don’t actually need a Refinement here, we could just as well define Gemini-Path to be (Intersection String Internal-Gemini-Path), but it (subjectively) clarifies the intent to declare it via Refine.

Finally, we can update the type of redirect:

(: redirect (-> Gemini-Path response))

Now, developers will get a type error for attempting to use the API insecurely.

(define input : String (get-insecure-input))
(redirect input)

But, with the help of Racket’s occurrence typing, they have a simple path towards secure usage.

(define input : String (get-insecure-input))

(if (gemini-path? input)
    (redirect input)
    (error "Error!"))

Faking Useful Refinement Types in Racket