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

Background

We have mainly been using the racket dialect plai-typed 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 plai-typed

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

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

(define (fun arg)
    (if arg
        'foo
        "bar"))
- comment out the type annotation
- verify this no longer typechecks in `plai-typed` (comment out the type annotation)
- verify that it _does_ typecheck in `typed/racket`, and put back
  a "human friendly" type annotation.

Typing "Lambda Lists"

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

#lang plai
(define (kons x y)
  (lambda (s)
    (s x y)))
(define (furst x) (x (lambda (x y) x)))
(define (rust x) (x (lambda (x y) y)))
(define a (kons 1 'alpha))
(define b (kons 'beta 4))
;
(test (furst a) 1)
(test (rust b) 4)
(test (rust 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 rackunit

#lang plai
(define (kons x y)
  (lambda (s)
    (s x y)))
(define (furst x) (x (lambda (x y) x)))
(define (rust x) (x (lambda (x y) y)))

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