16 Lab My Second Typed Language
Goals |
— |
We have created a language skeleton in the afternoon lecture. See the notes if you need a refresher. Now let’s finish implementing the rules for the type checker.
Exercise 27. Run the typed program (+ 1). It results in an error that says something about "incompatible ellipsis match counts". Obviously, that is an unacceptable message. Let’s fix that.
Here is the Turnstile implementation of a function application type checking rule.
(define-typerule (typed-app f e ...) ≫ [⊢ f ≫ f- ⇒ (~-> τin ... τout)] [⊢ e ≫ e- ⇐ τin] ... -------------------- [⊢ (#%app f- e- ...) ⇒ τout]) Improve typed-app so it emits a better "wrong arity" error message. Hint: define-typerule is compatible with syntax-parse pattern directives. In other words, you may use (almost) any syntax-parse pattern directive as a premise of the type rule. You may wish to consult the documentation to figure out what the various directives so, in particular for #:fail-unless.
(define-typerule typed-app [(_ f e ...) ≫ [⊢ f ≫ f- ⇒ (~-> τin ... τout)] [⊢ e ≫ e- ⇐ τin] ... -------------------- [⊢ (#%app f- e- ...) ⇒ τout]]) Add another clause that implements the "check" (<=) version of the rule.Hint, the clause will look like:
Exercise 30. Implement typed lambda. The syntax for an environment entry (to the left of the ) ⊢ is [x ≫ x- : τ].
Exercise 31. CHALLENGE 1: Implement a type rule for define-function.
You may or may not want to use your typed-lambda implementation to help out. If you do use typed-lambda, you’ll probably need the "check" (<=) version of typed-lambda.
Either way, you’ll need to use the "≻" Turnstile conclusion and define-typed-variable might come in handy to help define top-level definitions.
Be sure to write some tests to check your implementation. In particular, make sure that your implementation respects the annotations supplied by programmer. The typecheck-fail/toplvl testing form from turnstile/rackunit-typechecking may come in handy.
Exercise 32. CHALLENGE 2: Change our language to support subtyping.
(This exercise will let you practice writing functions that manipulate syntax objects.)
Turnstile includes overloadable hooks that change the behavior of all typing rules. For example, our type rules have been assuming type equality, but what if we want subtyping? It turns out, using the same rules we already wrote, we can add subtyping by modifying the current-typecheck-relation hook. (It’s implemented as a Racket parameter.)
Specifically, we have to write our own (compile-time) function that implements the subtyping relation. For example, it might start with something like:
(define-for-syntax (subtype? τ1 τ2) (syntax-parse (list τ1 τ2) clauses ...)) Complete this function.
Be careful because the type checking relation may no longer be symmetrical, depending on the behavior of our new function.
You may also want to add something like Nats, to better test the subtyping behavior.
After we implement such a function, we just need to install it as the type check relation (at the top of the file):
(begin-for-syntax (current-typecheck-relation subtype?))
Now (most of) our rules are automatically updated to utilize subtyping. Are there any rules that need to be manually updated?
Please fill out today’s post-day survey.