7.0.0.6
15 Building a Typed Language with Macros and Turnstile
Goals |
— |
Here is a link to the afternoon lecture slides (also available in PDF).
Here is the grammar for our typed language:
| Type | = | (-> Type ...) | ||
| | | Boolean | |||
| | | Number | |||
| | | String |
| Definition | = | (define-function (Variable [Variable : Type] ...) : Type Expression) | ||
| Expression | = | (function-application Variable Expression ...) | ||
| | | (λ ([x : Type] ...) Expression) | |||
| | | (if Expression Expression Expression) | |||
| | | (+ Expression Expression) | |||
| | | Variable | |||
| | | Boolean | |||
| | | Number | |||
| | | String |
Below is the skeleton we implemented together in lecture. In lab, we will complete the rest of our typed language.
| #lang turnstile/quicklang |
| ; e.g., save this to file "typed-lang.rkt" |
| (provide Int String -> |
| (rename-out [typed-app #%app] |
| [typed-+ +] |
| [typed-datum #%datum])) |
| (define-base-types Int String) |
| (define-type-constructor -> #:arity > 0) |
| (define-primop typed-+ + : (-> Int Int Int)) |
| (define-typerule (typed-app f e ...) ≫ |
| [⊢ f ≫ f- ⇒ (~-> τin ... τout)] |
| [⊢ e ≫ e- ⇐ τin] ... |
| -------------------- |
| [⊢ (#%plain-app f- e- ...) ⇒ τout]) |
| (define-typerule typed-datum |
| [(_ . n:integer) ≫ |
| ------------- |
| [⊢ (#%datum . n) ⇒ Int]] |
| [(_ . s:str) ≫ |
| ------------- |
| [⊢ (#%datum . s) ⇒ String]] |
| [(_ . x) ≫ |
| -------- |
| [#:error (type-error #:src #'x #:msg "Unsupported literal: ~v" #'x)]]) |
Below is an example program written in our typed language. The turnstile/rackunit-typechecking library will be useful for testing your typed language.
| #lang s-exp "typed-lang.rkt" |
| ; e.g., save this to file "typed-lang-prog.rkt" |
| (require turnstile/rackunit-typechecking) |
| (check-type 5 : Int) |
| (check-type "five" : String) |
| (typecheck-fail #f #:with-msg "Unsupported literal") |
| (typecheck-fail 1.1 #:with-msg "Unsupported literal") |
| (check-type + : (-> Int Int Int)) |
| (check-type (+ 1 2) : Int -> 3) |
| (typecheck-fail (+ 1)) |