14 Lab My First Typed Language

Exercise 20. Review the type rule for function application. Then come up with type rules for if and +.

Exercise 21. Write down bidirectional rules for our language. Make sure to come up with both "check" (<=) and "compute" (=>) rules for each language construct. These bidirectional rules will help when implementing a type checker for our language.

Exercise 22. Use the rules you developed to create a basic type checker. Specifically, implement a compute function with this signature:

; compute : ExprStx -> TyStx

; Computes the type of the given expression. Raises an error if a type cannot be computed.

This compute function is simplified because it does not deal with type environments and only works with expressions.

In other words, your function should implement all your "compute" type rules for expressions except variables and lambda.

This functions assumes syntax object representations of both types and expressions.

Below is some code that starts the compute function for you. In addition, it embeds compute as the type checker in a basic language, so you can write tests easily. Be sure to write valid and invalid programs to test your type checker.

This exercise will also give you practice writing code that manipulates syntax objects. In particular, the starter code uses many features of syntax-parse, including syntax patterns and syntax classes. Consult the documentation or ask the TAs if anything is unclear.

A few more notes about the code:

• To get to a full language as quickly as possible, we start with a check function implemented in terms of compute. In other words, our implementation will only use one, general "check" rule. (See if you can write this rule down. Look at the given implementation as a hint.) If you have time at the end, try to implement check using the type rules you developed. It should have a structure similar to the compute function you wrote.

• Also, this deals with type checking expressions only. The next exercise will ask you to think about how to add define-function.

• For type checking of addition (+) terms, can you think of more than one way to implement it? How does it affect your language?

• The code only type checks a program, and then discards it, so nothing happens at runtime.

#lang racket

; e.g., save this to file "morn-typed-lang.rkt"

(require (for-syntax syntax/parse syntax/stx))

(provide (rename-out [typechecking-mb #%module-begin])

+ if)

; A TyStx is a syntax object representing a type.

; A ExprStx is a syntax object representing an expression.

; A IdStx is an identifier syntax object.

(begin-for-syntax

; TODO: complete this function

; compute: ExprStx -> TyStx

; computes the type of the given term

(define (compute e)

(syntax-parse e

[:integer #'Int]

[:string #'String]

[:boolean #'Bool]

[((~literal if) e1 e2 e3)

#:when (check #'e1 #'Bool)

#'???]

[((~literal +) e1 e2)

#'???]

; TODO: fill in above cases, and other cases ...

[e (raise-syntax-error

'compute

(format "could not compute type for term: ~a" (syntax->datum #'e)))]))

; check : ExprStx TyStx -> Bool

; checks that the given term has the given type

(define (check e t-expected)

(define t (compute e))

(or (type=? t t-expected)

(raise-syntax-error

'check

(format "error while checking term ~a: expected ~a; got ~a"

(syntax->datum e)

(syntax->datum t-expected)

(syntax->datum t)))))

; type=? : TyStx TyStx -> Bool

; type equality here is is stx equality

(define (type=? t1 t2)

(or (and (identifier? t1) (identifier? t2) (free-identifier=? t1 t2))

(and (stx-pair? t1) (stx-pair? t2)

(= (length (syntax->list t1))

(length (syntax->list t2)))

(andmap type=? (syntax->list t1) (syntax->list t2))))))

(define-syntax typechecking-mb

(syntax-parser

[(_ e ...)

; prints out each term e and its type, it if has one;

; otherwise raises type error

#:do[(stx-map

(λ (e)

(printf "~a : ~a\n"

(syntax->datum e)

(syntax->datum (compute e))))

#'(e ...))]

; this language only checks types,

; it doesn't run anything

#'(#%module-begin (void))]))

And here is an example program to try with your typed language.

#lang s-exp "morn-typed-lang.rkt"

; e.g., save this to file "morn-typed-prog.rkt"

5

#f

"five"

; 1.1 ;; err

; (if 1 2 3) ;; err

(if #f 2 3)

+

(+ 1 2)

; (+ #f 1) ;; err

; Running the program prints:

; 5 : Int

; #f : Bool

; five : String

; (if #f 2 3) : Int

; + : (-> Int Int Int)

; (+ 1 2) : Int

Exercise 23. Implement an API for a type environment. More specifically, implement the following three functions:

; A TyEnv is a [ImmutableFreeIdTableOf IdStx -> TyStx]

; mk-empty-env : -> TyEnv

; Returns a new type environment with no bindings.

; add-to-env : TyEnv IdStx TyStx -> TyEnv

; Returns a new type environment that extends the given env with the given binding.

; lookup-env : TyEnv IdStx -> TyStx or #f

; Looks up the given id in the given env and returns corresponding type. Returns false if the id is not in the env.

We define a TyEnv as a free identifier table, which is just a hash table where the keys are syntax identifiers. Consult the docs for make-immutable-free-id-table to figure out how to use them.

Exercise 24. Use your type environment API to extend your compute function with an environment argument. Then complete compute by implementing type checking for variables and lambda.

Exercise 25. Think about what a type rule for define-function might look like. What about if functions are to be mutually recursive? How would it differ from the other rules we’ve seen?

Exercise 26. CHALLENGE: Try to add define-function to your type checker.

If you finish early, in preparation for the afternoon, make sure the Turnstile package is installed from the Racket package server. Install from DrRacket or type raco pkg install --auto turnstile from the command line.