UNB/ CS/ David Bremner/ teaching/ cs3613/ tutorials/ CS3613 Tutorial 5: Union Types


We have mainly been using the racket dialect plait this term. This dialect uses a typed system modelled on that of ML. This has some advantages, including allowing quite good type inference. Unfortunately it is unable to type several constructs that are fairly natural in dynamically typed languages. One interesting and practical idea in programming languagues is so called Gradual typing. In a gradually typed language some expressions have static types checked at compiled time while others are checked at run time. In this tutorial we will explore the idea of union types used by the gradually typed language typed/racket.

Type inference versus gradual typing

One subtlety to understand right away is that lack of type annotations is much different from gradual typing.

Conside the following function.

#lang plait

(define (fun arg)
    (if arg
(define (bar)
  (fun "hello"))

Notice that the "bad" code is never run, but we still get a typecheck error.

(define (fun arg)
    (if arg

Typing "Lambda Lists"

Let's look back at our example from implimenting data structures with functions.

#lang plait #:untyped
(define (_cons x y) (lambda (s) (s x y)))
(define (_first x) (x (lambda (x y) x)))
(define (_rest x) (x (lambda (x y) y)))
(define a (_cons 1 'alpha))
(define b (_cons 'beta 4))
(test (_first a) 1)
(test (_rest b) 4)
(test (_rest a) 'alpha)

It turns out that the test form is not available in typed/racket, but similar functionality is available from rackunit.

Let's convert our example to typed/racket and rackunit. Notice we leave the type-checker off at first.

#lang typed/racket/no-check
(define (_cons x y)
  (lambda (s)
    (s x y)))
(define (_first x) (x (lambda (x y) x)))
(define (_rest x) (x (lambda (x y) y)))

(module+ test
  (require rackunit)
  (define a (_cons 1 'alpha))
  (define b (_cons 'beta 4))
  (check-equal? (_first a) 1 "furst")
  (check-equal? (_rest b) 4 "rust")
  (check-equal? (_rest a) 'alpha))
(define (_first [x : _Pair]) (x (lambda (x y) x)))
(define (_rest [x : _Pair]) (x (lambda (x y) y)))