Background

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
        'foo
        'bar))

• Type fun in the REPL to see what the infered type of this function is.

• To convince yourself that this checking happens at compile time, add the following

(define (bar)
  (fun "hello"))

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

• Try changing

    #lang plait
  

  to

    #lang plait #:untyped
  

  Not only does it quiet the typechecker, but you can run the function (bar). Why is this?

• Try changing the #lang to typed/racket. What is the inferred type of fun?

  • To help understand this, note that typed/racket reports function type A B -> C as (-> A B C). This is no loss of information because the arrow is always in the same place in our usual form.

  • the (U … ) form defines a union type, which here looks a bit like dodging the question, by listing all possible return values.

  • the Any marks a dynamically typed identifier

• Write a type annotation for the function fun by copying the inferred type.

• Modify your type annotation to look more like the familar (A -> B) form

• Modify your type annotation to avoid the use union types. Note that your new type will be less precise than before, but possibly more meaningful for humans. You may want to drop or modify the function bar so you can get rid of the Any.

• Modify the actual function definition to

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

• comment out the type annotation
• verify this no longer typechecks in plait (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 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 "_first")
  (check-equal? (_rest b) 4 "_rest")
  (check-equal? (_rest a) 'alpha))

• Try switching to #lang typed/racket. Unlike our previous example, this one doesn't typecheck without annotations.

  • The main point of the remaining error messages seems to be that typed/racket can't seem to infer when things are functions. Although plait can't typecheck some things, it is actually better at inferring what is a function.

• Comment out everything but the definition of _cons, and try to find an annotation for parameter s that lets typed/racket typecheck it. Be as vague as you can get away with. You'll need to replace lambda with lambda:

• Define a type alias using (define-type-alias BinOp (Any Any -> Any))

• Use this type alias to give a type-annotation (using (: … )) for _cons. Can you get rid of your previous type annotation on s? Why or why not?
• Define a second type alias _Pair for the return type of _cons, and use this in your type annotation. Also use _pair to annotate _first and _rest, as follows:

(define (_first [x : _Pair]) (x (lambda (x y) x)))
(define (_rest [x : _Pair]) (x (lambda (x y) y)))

• At this point, you should be able to change (require rackunit) to (require typed/rackunit) and have all tests pass.

• You might think we're not using union types at all, except that Any is really the biggest union type of all. Define a third type alias Thing and replace the use of Any with Thing. Make your definition of Thing general enough, but less general than Any. Your final set of type-aliases will be mutually recursive.