15 Lab My First Turnstile Language
15.1 Starter Code
Your primary goal for this lab is to implement the remaining typing rules using turnstile. Before getting started, you’ll want to download the starter file, which includes the code we saw in the lecture and one additional definition, which provides a definition form for our typed language:
"stlc.rkt" [download]
77 (define-typed-syntax def 78 [(_ x:id e:expr) 79 ≫ 80 ---- 81 [≻ (define-typed-variable x e)]] 82 83 [(_ x:id τ:type e:expr) 84 ≫ 85 [⊢ e ≫ e- ⇐ τ.norm] 86 ---- 87 [≻ (define-typed-variable x e- ⇐ τ.norm)]])
The turnstile library’s define-typed-variable can be used several ways. The first form above, given just an identifier and an expression, expands the expression in check mode. The second form expands the expression in check mode with the given expected type.
Notice that the conclusions of both cases use syntax we haven’t seen before: ≻ instead of ⊢. This means that the result of the expansion does not itself have a type, which is appropriate when we’re defining definition forms, which don’t evaluate to values. When you use def in module context then the context doesn’t demand a type, so it works. If you use a definition where an expression is expected then it should and will fail to type.
At this point, you should be able to both compute and check the type of a λ, though you can’t do anything useful in the body. Before moving on, try it out to make sure your setup is correct:
"stlc-test1.rkt" [download]
#lang s-exp "stlc.rkt" ; Compute type of annotated λ: (def fst (λ ([x Int] [y Bool]) x)) (check-type fst : (-> Int Bool Int)) ; Cannot compute type of unannotated λ: (typecheck-fail (λ (x y) y)) ; Check expected type of unannotated λ: (def snd (ann (λ (x y) y) (-> Int Bool Bool))) (check-type snd : (-> Int Bool Bool)) ; Expected type doesn't match λ arity: (typecheck-fail (ann (λ (x y z) z) (-> Int Bool Int))) ; No literals yet: (typecheck-fail 5) (typecheck-fail #f)
No output is good output.
15.2 Exercises
In order to type a turnstile rule (using your keyboard), you need to be able to enter the special characters that turnstile uses. DrRacket has a mechanism for entering special characters by typing a particular sequence starting with \ and ending with Control-\. Here are the sequences you’ll need:
≫
\gg
⇐
\Leftarrow
⇒
\Rightarrow
≻
\succ
⊢
\vdash
(Alternatively, see turnstile/no-unicode.)
Exercise 42. To use literals in your language, it needs a definition of #%datum to compute their types. Define #%datum so that it handles integer and Boolean literals.
You should now be able to use integer and Boolean literals in your language, but other kinds of literals should be a syntax error:
> 5 5
> #f #f
> "hello" TYPE-ERROR: unsupported literal
Hints: 1) Recall that is applied to a literal as a dotted pair, like (#%datum . literal). 2) Match literal forms using syntax classes, such as boolean. 3) Expand to a use of #%datum- to avoid an infinite loop.
Exercise 43. Here’s the type inference rule for application:
Implement the rule as #%app.
Hints: 1) Be careful about which premiss is computed and which are checked. 2) Like λ, implementing #%app with turnstile requires an arity check.
Once you’ve completed exercise 42 and exercise 43, you should be able to apply both built-in and user-defined functions:
"stlc-test2.rkt" [download]
#lang s-exp "stlc.rkt" (check-type 5 : Int -> 5) (check-type (+ 4 5) : Int -> 9) (check-type (+ 4 (+ 5 6)) : Int -> 15) (typecheck-fail (+ 5 #t)) (typecheck-fail (+ 5)) (def - (-> Int Int Int) (λ (x y) (+ x (* y -1)))) (check-type - : (-> Int Int Int)) (check-type (- 12 7) : Int -> 5) (typecheck-fail (- #t #f))
Exercise 44. Here are the type inference rules for if:
Implement the rules.
Hint: turnstile provides a function type=? for checking whether two types are the same.
Exercise 45. Recall the
expression from exercise 38. Suppose we want our typed language to provided it in two forms, as we did for
: The type-annotated form,
, works in both compute mode and check mode, whereas the unannotated form,
, works only in check mode.
Here are the type inference rules for
:
Implement the rules.
Hint: To expand typed rec to untyped rec-, you may need a definition of rec-, like this:
(define-syntax (rec- stx) (syntax-parse stx [(_ x:id e:expr) #'(letrec- ([x e]) x)]))
Exercise 46. Now that you have if and rec, you can write recursive functions. Implement fib to compute the nth Fibonacci number, in your typed language.
Exercise 47. The model language we saw this morning had a let that binds only one variable: (let ([x e]) e). Here are the type inference rules for that single-binding let:
Can you extend the rules to handle multiple bindings? Like Racket’s let, the bindings should be scoped in “parallel.”
You should again confirm that your implementation is correct. Here are some tests that should help (and you should write some more):
"stlc-test3.rkt" [download]
#lang s-exp "stlc.rkt" ;; Subtracts two integers. (def - (λ ([x Int] [y Int]) (+ x (* -1 y)))) (check-type - : (-> Int Int Int)) ; correct type for - (check-type (- 3 8) : Int -> -5) ; correct type and result (typecheck-fail (- 3 #t)) ; bad argument type (typecheck-fail (- 3 8 12)) ; too many arguments (typecheck-fail (- 3)) ; too few arguments ;; Finds the factorial of an integer, weirdly. (def fact (rec self (-> Int Int) (λ (n) (let ([condition (<= n 1)] [n (- n 1)]) (* (+ n 1) (if condition 1 (self n))))))) (check-type (fact 5) : Int -> 120) ;; (iter n f x) applies `f` to `x`, `n` times. (def iter (-> Int (-> Int Int) Int Int) (rec self (λ (n f x) (if (<= n 0) x (self (- n 1) f (f x)))))) ;; Integer exponentiation using `iter`. (def expt (-> Int Int Int) (λ (n m) (iter m (λ (acc) (* n acc)) 1))) (check-type (expt 2 10) : Int -> 1024)
In the unlikely case that you need more exercises, you can find some here.
Survey link: https://forms.gle/C1QnfXarBxZDQAyq6