Week 13 Set b
Due Date Thursday 11/29 at 9:00pm (Week 13)
Purpose Extend the type checker.
Graded Exercises
We are starting from code used in class:
; SIMPLE TYPED LANGUAGE ; An Expression is a: ; - Number ; - Boolean ; - (list AopName Expression Expression) ; - (list BopName Expression Expression) ; - (list CmpopName Expression Expression) ; - (list 'if Expression Expression Expression) ; - (list 'var Symbol) ; - (list 'lam Symbol Type Expression) ; - (list 'app Expression Expression) (define AOPS '(+ -)) ; An AopName is a member of AOPS, all of which have type: Number Number -> Number (define BOPS '(and or)) ; An BopName is a member of BOPS, all of which have type: Boolean Boolean -> Boolean (define CmpOPS '(> < =)) ; An CmpopName is a member of CmpOPS, all of which have type: Number Number -> Boolean ; A Type is one of: ; - 'Number ; - 'Boolean (define-struct funty [arg ret]) ; - (make-funty Type Type) ; ensuretype : Environment Expression Type -> Type ; Check that expression e has type t, error if e's type does not match t (define (ensuretype env e t) (local ((define ty-e (typecheck-env env e))) (if (equal? ty-e t) t (error "Expression " e " has type " ty-e " but was expected to have type " t)))) (define-struct var:ty [var ty]) ; An Environment is a [List of (make-var:ty Symbol Type)] ; Interp: A mapping from variables to types ; typecheck-env : Environment Expresssion -> Type ; return the type of the expression e or error if the expression is not well typed ; Accumulator: env represents... (define (typecheck-env env e) (cond [(number? e) 'Number] [(boolean? e) 'Boolean] [(member? (first e) AOPS) (local ((define t-1 (ensuretype env (second e) 'Number)) (define t-2 (ensuretype env (third e) 'Number))) 'Number)] [(member? (first e) BOPS) (local ((define t-1 (ensuretype env (second e) 'Boolean)) (define t-2 (ensuretype env (third e) 'Boolean))) 'Boolean)] [(member? (first e) CmpOPS) (local ((define t-1 (ensuretype env (second e) 'Number)) (define t-2 (ensuretype env (third e) 'Number))) 'Boolean)] [(symbol=? (first e) 'if) (local ((define t-0 (ensuretype env (second e) 'Boolean)) (define ty-e1 (typecheck-env env (third e))) (define ty-e2 (typecheck-env env (fourth e)))) (if (equal? ty-e1 ty-e2) ty-e1 (error "Branches of if expression " e "have different types")))])) ; typecheck : Expression -> Type ; return the type of the expression e or error if the expression is not well typed (define (typecheck e) (typecheck-env ? e)) (check-expect (typecheck 1) 'Number) (check-expect (typecheck #false) 'Boolean) (check-expect (typecheck (list '+ 1 2)) 'Number) (check-expect (typecheck (list '- (list '+ 1 2) 5)) 'Number) (check-error (typecheck (list '+ #false 2))) (check-error (typecheck (list 'if 1 #true #false))) (check-error (typecheck '(if (> 3 9) 1 #true))) (check-expect (typecheck '(if (> 3 9) 1 4)) 'Number) (check-expect (typecheck '(and #false (> 2 2))) 'Boolean) (check-error (typecheck '(and #false (+ 2 2))))
Exercise 1 Your first task is to complete the code that handles typechecking of lambdas, variables, and application. We showed on the board how to handle typechecking these, with the following typing rules:
x:t ∈ Γ --------- Var Γ ⊢ x : t Γ,x:t1 ⊢ e : t2 --------------------- Lam Γ ⊢ λx:t1.e : t1 → t2 Γ ⊢ e1 : t1 → t2 Γ ⊢ e2 : t1 ------------------------------ App Γ ⊢ e1 e2 : t2 Implement these typing rules in the typechecker given above.
Exercise 2 A pair can be represented in our expression language as (e1, e2). where we can get the two components (first and second, respectively) with fst and snd. Pairs should have the pair type t1 x t2.
t ::= ... | t1 x t2 e ::= ... | (e1, e2) | fst e | snd e We can write typing rules for all three expressions as follows:
Γ ⊢ e1 : t1 Γ ⊢ e2 : t2 ------------------------- Pair Γ ⊢ (e1,e2) : t1 x t2 Γ ⊢ e : t1 x t2 --------------- Fst Γ ⊢ fst e : t1 Γ ⊢ e : t1 x t2 --------------- Snd Γ ⊢ snd e : t2 Please extend the expression data definition, type data definition, and typechecker to handle pairs, fst, and snd.
A common type that we use in our signatures is an enumeration, e.g.,
; A Pet is one of ; - Dog ; - Cat
If Dog and Cat were themselves types, we said we could represent Pet as [Union Dog Cat]. This is an example of an "untagged" union, because there is no value (or tag) that allows us to distinguish that a given Dog is indeed a Pet. A more disciplined approach results in tagged unions (which we will call Sum types and write t1 + t2), which we will add in a restricted form to our language. We will add:
t ::= ... | t1 + t2 e ::= ... | inleft(t1,t2) e | inright(t1,t2) e | case e of inleft x => e1, inright y => e2
Where inleft and inright are how we construct values of our sum type, and case is how we use a value that has type t1 + t2. When evaluating a case expression, if the expression e evaluates to an inleft(t1,t2) v, we will bind v to x and evaluate e1, whereas if e evaluates to an inright v, we will bind v to y and evaluate e2, and the resulting types of e1 and e2 must be the same (though they can depend on values of different types: t1 and t2 respectively). Note that x and y here are placeholders for any variable, which can then we used in the corresponding branch.
NOTE: Since when you have inleft e (same for inright), you don’t know what the other type is, we explicitly annotate with both types (that’s what we write in the parentheses). In a language with type inference, writing these would not be necessary, but that would require a more complicated type checker.
The typing rules for inleft, inright, and case are as follows:
Γ ⊢ e : t1 ---------------------- Inleft Γ ⊢ inleft(t1,t2) e : t1 + t2 Γ ⊢ e : t2 ----------------------- Inright Γ ⊢ inright(t1,t2) e : t1 + t2 Γ ⊢ e : t1 + t2 Γ,x:t1 ⊢ e1 : t Γ,y:t2 ⊢ e2 : t ----------------------------------------------------- Case Γ ⊢ case e of inleft x => e1, inright y => e2 : t
Here in an example of how case evaluates:
case (inleft(Num,Bool) 10) of inleft x => x + 2, inright y => if y 3 4 ====> x=10 in x + 2 (this is a fake step just to show the substitution of x) ====> 10 + 2 ====> 12
case (inright(Num,Bool) true) of inleft x => x + 2, inright y => if y 3 4 ====> y=true in if y 3 4 (this is a fake step just to show the substitution of y) ====> if true 3 4 ====> 3
Exercise 3 Extend the expression data definition and the type-checker to handle sum types.
You may have noticed that handling sum types shares some aspects with how if was handled. In fact, you can implement booleans in terms of a sum type where the actual values are ignored (as the important part is whether the boolean is an inleft or an inright, not the values that are carried). A helpful value to introduce in this case is the so-called "unit" value, which is called void in some languages. This value has the type Unit, and it is the only value of that type. In that sense, it carries no interesting information.
We can write the unit value as unit and its type as Unit, as follows:
t ::= ... | Unit e ::= ... | unit
And the typing rule is similarly uninteresting:
--------------- Γ ⊢ unit : Unit
Exercise 4 Extend the source language with cases for unit, and extend the typechecker to handle unit.
Exercise 5 Show how booleans can be translated into values of type Unit + Unit, and how an if expression can be translated into a case expression. Please write an expression for each of the following cases that does not use booleans or if, but captures the same meaning:
true false if e0 then e1 else e2