Extract a type from a Typed Racket union

Question

I have a function which, sort of like assoc, searches a symbol in list and returns either #f or the position in the list.

The return type for this function should be a union of #f and Natural, (U #f Natural).

But when I want to use the value as a number, it will always type mismatch because the value is not just a Natural but in fact a union.

How can I pull the Natural value out and avoid the type-mismatch error?

Answer 1

Typed Racket has a feature called Occurrence Typing, which allows you to filter a value's type using predicates and assertions. The basic idea is that predicates, such as string?, empty?, and number? can filter types based on a program's control flow.

To illustrate this, see this example:

(: nat/#f->nat ((U Natural False) -> Natural))
(define (nat/#f->nat n)
  (if n n
      (error "Expected a number, given " n)))

This will typecheck because, if the first branch is taken, then n cannot be #f, so it must be a Natural. In the second case, the function just errors and doesn't return, so the type still holds.

In most cases, you won't just simply error on the failure case, but you'll provide some sort of alternate behavior. This still allows you to refine the type within a body itself.

(define n : (Option Natural) #f)

(cond
  [n
   ; do something with n as a number
   (+ n 1)]
  [else
   ; do something else
   (void)])

Within the body of the first case, the type of n is refined to be Natural, so it can be used as such.

In the case that you actually do want to just throw an error when a type doesn't match, you can use assert or cast. The former is effectively a derived concept, which basically performs the same sort of check as the first example above. You use it like this:

(assert n number?) ; now n is a number, and if it isn't, an error is thrown
(+ n 1)

The cast form is a little bit different, since it specifies types instead of predicates. That means you can use it like this:

(+ (cast n Natural) 1)

This also throws an error if it turns out that n isn't actually a Natural, but otherwise, the overall expression becomes of type Natural.