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.

(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 objects

In this section we will revisit the “Tree Object” example from lecture07

To simplify moving between different dialects of Racket, we will use a simplified version of the msg function that does not take any arguments other than the method selector. We also simplify things by returning a value rather than a lambda that must be called

(define (msg0 obj selector) (obj selector))

Here is the node definition, using the new msg0 function.

(define (node v l r)
  (lambda (m)
    (case m
      [(sum)  (+ (msg0 l 'sum) (msg0 r 'sum))])))

Observe that by itself, this function typechecks fine in plait.

Let’s try filling in a more complete set of methods. We can start by adding a method val to return the number stored at the root node.

(define (node v l r)
  (lambda (m)
    (case m
      [(value) v]
      [(sum) (+ v (+ (msg0 l 'sum) (msg0 r 'sum)))]
      [else (error 'node (symbol->string m))])))

Along with a definition for mt

(define (mt)
  (lambda (m)
    (case m
      [(sum) 0]
      [else (error 'mt (symbol->string m))])))

We can now typecheck and pass some simple tests

(define tree1 (node 1 (mt) (mt)))
(test (msg0 tree1 'sum) 1)
(test (msg0 tree1 'value) 1)

When we add methods to retrieve the left and right subtree, plait is no longer able to typecheck this function

(define (node v l r)
  (lambda (m)
    (case m
      [(value) v]
      [(left)  l]
      [(right) r]
      [(sum) (+ v (+ (msg0 l 'sum) (msg0 r 'sum)))]
      [else (error 'node (symbol->string m))])))

After adding an appropriate require for test see lecture07, verify that the following tests pass with #lang racket

(define tree2 (node 1 (node 2 (mt) (mt)) (mt)))
(test (msg0 tree2 'value) 1)
(test (msg0 (msg0 tree2 'left) 'value) 2)

Let’s start to convert to #lang typed/racket by using #lang typed/racket/nocheck (this turns off the type-checker) We need a different require for test (this version of test only reports errors, like (print-only-errors #t) in plait).

(require (rename-in typed/rackunit [check-equal? test])
         (only-in typed/rackunit check-exn))
(define-syntax-rule (test/exn expr msg)
  (check-exn exn:fail? (lambda () expr) msg))

What to hand in

Start with skeleton.rkt. In order to work in typed/racket, the functions msg0 node and mt have had their parameters annotated.

(define (msg0 [obj : Node] [selector : Symbol]) (obj selector))

(define (node [v : Number] [l : Node] [r : Node]) : Node
  (lambda (m)
    (case m
      [(value) v]
      [(left)  l]
      [(right) r]
      [(sum) (+ v (+ (msg-num l 'sum) (msg-num r 'sum)))]
      [else (error 'node (symbol->string m))])))

(define (mt)
  (lambda ([m : Symbol])
    (case m
      [(sum) 0]
      [else (error 'mt (symbol->string m))])))

Define a union-type Node (with define-type-alias) and functions msg-num and msg-node so that the following tests pass.

(module+ test
  (define tree1 (node 1 (mt) (mt)))
  (test (msg0 tree1 'sum) 1)
  (test (msg0 tree1 'value) 1)
  (define tree2 (node 1 (node 2 (mt) (mt)) (mt)))
  (test (msg0 tree2 'value) 1)
  (test (msg0 (msg-node tree2 'left) 'value) 2)
  (test (msg0 (msg-node tree2 'right) 'sum) 0)
  (test/exn (msg0 (mt) 'left) "left")
  (test/exn (msg0 tree2 'wrong) "wrong")
  (test/exn (msg-num tree2 'left) "number")
  (test/exn (msg-node tree2 'value) "node"))