#lang plait ;; Start with "type-case.rkt" ;; Add a new test case that ends ;; ;; {+ {toKelvin {F 32}} ;; {toKelvin {C 0}}} ;; ;; where `F` and `C` are constructors for a `Degrees` type in Curly ;; (in Fahrenheit or Celsius, respotively). ;; ;; Recall that Celsius + 273.15 = Kelvin ;; and (Fahrenheit - 32) * 5/9 = Celsius (module+ test (define expr (parse `{let-type [Degrees {F num} {C num}] {letrec {[toKelvin : (Degrees -> num) {lambda {[arg : Degrees]} {type-case Degrees arg [{F n} {toKelvin {C {* 5/9 {+ n -32}}}}] [{C n} {+ n 273.15}]}}]} {+ {toKelvin {F 32}} {toKelvin {C 0}}}}})) (test (typecheck expr mt-env) (numT)) (test (interp expr mt-env) (numV (* 2 273.15)))) ;; ---------------------------------------- ;; Add an `equal?` operator that is like Plait's: ;; it works on any two values, as long as the values ;; have the same type. (module+ test (test (typecheck (parse `{equal? 1 2}) mt-env) (numT)) (test (typecheck (parse `{let-type [Degrees {F num} {C num}] {equal? {F 0} {F 0}}}) mt-env) (numT)) (test (typecheck (parse `{let-type [Degrees {F num} {C num}] {equal? {F 0} {C 0}}}) mt-env) (numT)) (test/exn (typecheck (parse `{let-type [Degrees {F num} {C num}] {equal? 0 {F 0}}}) mt-env) "no type") (test (interp (parse `{equal? 1 2}) mt-env) (numV 1)) (test (interp (parse `{equal? 1 1}) mt-env) (numV 0)) (test (interp (parse `{let-type [Degrees {F num} {C num}] {equal? {F 0} {F 0}}}) mt-env) (numV 0)) (test (interp (parse `{let-type [Degrees {F num} {C num}] {equal? {F 0} {C 0}}}) mt-env) (numV 1)) (test (interp (parse `{let-type [Degrees {F num} {C num}] {equal? {F 0} {F 1}}}) mt-env) (numV 1))) ;; ---------------------------------------- (define-type Value (numV [n : Number]) (closV [arg : Symbol] [body : Exp] [env : Env]) (variantV [tag : Symbol] [val : Value]) (constructorV [tag : Symbol])) (define-type Exp (numE [n : Number]) (idE [s : Symbol]) (plusE [l : Exp] [r : Exp]) (multE [l : Exp] [r : Exp]) (equalE [l : Exp] [r : Exp]) (lamE [n : Symbol] [arg-type : Type] [body : Exp]) (appE [fun : Exp] [arg : Exp]) (letrecE [n : Symbol] [n-type : Type] [rhs : Exp] [body : Exp]) (let-typeE [type-name : Symbol] [tag1 : Symbol] [type1 : Type] [tag2 : Symbol] [type2 : Type] [body : Exp]) (type-caseE [type-name : Symbol] [tst : Exp] [tag1 : Symbol] [n1 : Symbol] [rhs1 : Exp] [tag2 : Symbol] [n2 : Symbol] [rhs2 : Exp])) (define-type Type (numT) (boolT) (arrowT [arg : Type] [result : Type]) (definedT [name : Symbol])) (define-type Binding (bind [name : Symbol] [val : (Boxof (Optionof Value))])) (define-type-alias Env (Listof Binding)) (define-type Type-Binding (tbind [name : Symbol] [type : Type]) (tdef [type-name : Symbol] [tag1 : Symbol] [type1 : Type] [tag2 : Symbol] [type2 : Type])) (define-type-alias Type-Env (Listof Type-Binding)) (define mt-env empty) (define extend-env cons) (module+ test (print-only-errors #t)) ;; parse ---------------------------------------- (define (parse [s : S-Exp]) : Exp (cond [(s-exp-match? `NUMBER s) (numE (s-exp->number s))] [(s-exp-match? `SYMBOL s) (idE (s-exp->symbol s))] [(s-exp-match? `{+ ANY ANY} s) (plusE (parse (second (s-exp->list s))) (parse (third (s-exp->list s))))] [(s-exp-match? `{* ANY ANY} s) (multE (parse (second (s-exp->list s))) (parse (third (s-exp->list s))))] [(s-exp-match? `{equal? ANY ANY} s) (equalE (parse (second (s-exp->list s))) (parse (third (s-exp->list s))))] [(s-exp-match? `{let {[SYMBOL : ANY ANY]} ANY} s) (let ([bs (s-exp->list (first (s-exp->list (second (s-exp->list s)))))]) (appE (lamE (s-exp->symbol (first bs)) (parse-type (third bs)) (parse (third (s-exp->list s)))) (parse (fourth bs))))] [(s-exp-match? `{letrec {[SYMBOL : ANY ANY]} ANY} s) (let ([bs (s-exp->list (first (s-exp->list (second (s-exp->list s)))))]) (letrecE (s-exp->symbol (first bs)) (parse-type (third bs)) (parse (fourth bs)) (parse (third (s-exp->list s)))))] [(s-exp-match? `{lambda {[SYMBOL : ANY]} ANY} s) (let ([arg (s-exp->list (first (s-exp->list (second (s-exp->list s)))))]) (lamE (s-exp->symbol (first arg)) (parse-type (third arg)) (parse (third (s-exp->list s)))))] [(s-exp-match? `{let-type [SYMBOL {SYMBOL ANY} {SYMBOL ANY}] ANY} s) (let ([rec (s-exp->list (second (s-exp->list s)))]) (let-typeE (s-exp->symbol (first rec)) (s-exp->symbol (first (s-exp->list (second rec)))) (parse-type (second (s-exp->list (second rec)))) (s-exp->symbol (first (s-exp->list (third rec)))) (parse-type (second (s-exp->list (third rec)))) (parse (third (s-exp->list s)))))] [(s-exp-match? `{type-case SYMBOL ANY [{SYMBOL SYMBOL} ANY] [{SYMBOL SYMBOL} ANY]} s) (let ([case1 (s-exp->list (fourth (s-exp->list s)))] [case2 (s-exp->list (fourth (rest (s-exp->list s))))]) (type-caseE (s-exp->symbol (second (s-exp->list s))) (parse (third (s-exp->list s))) (s-exp->symbol (first (s-exp->list (first case1)))) (s-exp->symbol (second (s-exp->list (first case1)))) (parse (second case1)) (s-exp->symbol (first (s-exp->list (first case2)))) (s-exp->symbol (second (s-exp->list (first case2)))) (parse (second case2))))] [(s-exp-match? `{ANY ANY} s) (appE (parse (first (s-exp->list s))) (parse (second (s-exp->list s))))] [else (error 'parse "invalid input")])) (define (parse-type [s : S-Exp]) : Type (cond [(s-exp-match? `num s) (numT)] [(s-exp-match? `bool s) (boolT)] [(s-exp-match? `(ANY -> ANY) s) (arrowT (parse-type (first (s-exp->list s))) (parse-type (third (s-exp->list s))))] [(s-exp-match? `SYMBOL s) (definedT (s-exp->symbol s))] [else (error 'parse-type "invalid input")])) (module+ test (test (parse `2) (numE 2)) (test (parse `x) ; note: backquote instead of normal quote (idE 'x)) (test (parse `{+ 2 1}) (plusE (numE 2) (numE 1))) (test (parse `{* 3 4}) (multE (numE 3) (numE 4))) (test (parse `{+ {* 3 4} 8}) (plusE (multE (numE 3) (numE 4)) (numE 8))) (test (parse `{let {[x : num {+ 1 2}]} y}) (appE (lamE 'x (numT) (idE 'y)) (plusE (numE 1) (numE 2)))) (test (parse `{letrec {[x : num {+ 1 2}]} y}) (letrecE 'x (numT) (plusE (numE 1) (numE 2)) (idE 'y))) (test (parse `{lambda {[x : num]} 9}) (lamE 'x (numT) (numE 9))) (test (parse `{double 9}) (appE (idE 'double) (numE 9))) (test (parse `{let-type [Fruit {apple num} {banana (num -> num)}] 1}) (let-typeE 'Fruit 'apple (numT) 'banana (arrowT (numT) (numT)) (numE 1))) (test (parse `{type-case Fruit 1 [{apple a} 2] [{banana b} 3]}) (type-caseE 'Fruit (numE 1) 'apple 'a (numE 2) 'banana 'b (numE 3))) (test/exn (parse `{{+ 1 2}}) "invalid input") (test (parse-type `num) (numT)) (test (parse-type `bool) (boolT)) (test (parse-type `(num -> bool)) (arrowT (numT) (boolT))) (test/exn (parse-type `1) "invalid input")) (define (my-equal? [l : Value] [r : Value]) : Boolean (type-case Value l [(numV n) (type-case Value r [(numV r-n) (= n r-n)] [else #f])] [(closV arg body env) #f] [(variantV tag val) (type-case Value r [(variantV r-tag r-val) (if (symbol=? tag r-tag) (my-equal? val r-val) #f)] [else #f])] [(constructorV tag) (type-case Value r [(constructorV r-tag) (symbol=? tag r-tag)] [else #f])])) ;; interp ---------------------------------------- (define (interp [a : Exp] [env : Env]) : Value (type-case Exp a [(numE n) (numV n)] [(idE s) (lookup s env)] [(plusE l r) (num+ (interp l env) (interp r env))] [(multE l r) (num* (interp l env) (interp r env))] [(equalE l r) (if (my-equal? (interp l env) (interp r env)) (numV 0) (numV 1))] [(lamE n t body) (closV n body env)] [(appE fun arg) (type-case Value (interp fun env) [(closV n body c-env) (interp body (extend-env (bind n (box (some (interp arg env)))) c-env))] [(constructorV tag) (variantV tag (interp arg env))] [else (error 'interp "not a function")])] [(letrecE n t rhs body) (let ([b (box (none))]) (let ([new-env (extend-env (bind n b) env)]) (begin (set-box! b (some (interp rhs new-env))) (interp body new-env))))] [(let-typeE type-name tag1 type1 tag2 type2 body) (interp body (extend-env (bind tag1 (box (some (constructorV tag1)))) (extend-env (bind tag2 (box (some (constructorV tag2)))) env)))] [(type-caseE ty tst tag1 n1 rhs1 tag2 n2 rhs2) (type-case Value (interp tst env) [(variantV tag val) (cond [(eq? tag tag1) (interp rhs1 (extend-env (bind n1 (box (some val))) env))] [(eq? tag tag2) (interp rhs2 (extend-env (bind n2 (box (some val))) env))] [else (error 'interp "wrong tag")])] [else (error 'interp "not a variant")])])) (module+ test (test (interp (parse `2) mt-env) (numV 2)) (test/exn (interp (parse `x) mt-env) "free variable") (test (interp (parse `x) (extend-env (bind 'x (box (some (numV 9)))) mt-env)) (numV 9)) (test (interp (parse `{+ 2 1}) mt-env) (numV 3)) (test (interp (parse `{* 2 1}) mt-env) (numV 2)) (test (interp (parse `{+ {* 2 3} {+ 5 8}}) mt-env) (numV 19)) (test (interp (parse `{lambda {[x : num]} {+ x x}}) mt-env) (closV 'x (plusE (idE 'x) (idE 'x)) mt-env)) (test (interp (parse `{let {[x : num 5]} {+ x x}}) mt-env) (numV 10)) (test (interp (parse `{let {[x : num 5]} {let {[x : num {+ 1 x}]} {+ x x}}}) mt-env) (numV 12)) (test (interp (parse `{let {[x : num 5]} {let {[y : num 6]} x}}) mt-env) (numV 5)) (test (interp (parse `{{lambda {[x : num]} {+ x x}} 8}) mt-env) (numV 16)) (test/exn (interp (parse `{letrec {[f : num f]} f}) mt-env) "use before initialization") (test (interp (parse `{letrec {[f : (num -> num) {lambda {[x : num]} {+ x x}}]} {f 8}}) mt-env) (numV 16)) (test (interp (parse `{letrec {[f : (((num -> num) -> ((num -> num) -> (num -> num))) -> (num -> num)) {lambda {[sel : ((num -> num) -> ((num -> num) -> (num -> num)))]} {{sel {lambda {[x : num]} {{f {lambda {[f : (num -> num)]} {lambda {[g : (num -> num)]} g}}} 3}}} {lambda {[x : num]} x}}}]} {{f {lambda {[f : (num -> num)]} {lambda {[g : (num -> num)]} f}}} 9}}) mt-env) (numV 3)) (test (interp (parse `{let-type [Fruit {apple num} {banana (num -> num)}] {apple 1}}) mt-env) (variantV 'apple (numV 1))) (test (interp (parse `{let-type [Fruit {banana (num -> num)} {apple num}] {apple 1}}) mt-env) (variantV 'apple (numV 1))) (test (interp (parse `{let-type [Fruit {apple num} {banana (num -> num)}] {let {[f : (Fruit -> num) {lambda {[f : Fruit]} {type-case Fruit f [{apple a} a] [{banana g} {g 2}]}}]} {+ {f {apple 1}} {f {banana {lambda {[n : num]} {+ n 3}}}}}}}) mt-env) (numV 6)) (test/exn (interp (parse `{type-case Fruit 1 [{apple a} 1] [{banana b} 1]}) mt-env) "not a variant") (test/exn (interp (parse `{let-type [Animal {lion num} {bear num}] {type-case Fruit {lion 1} [{apple a} 1] [{banana b} 1]}}) mt-env) "wrong tag") (test/exn (interp (parse `{1 2}) mt-env) "not a function") (test/exn (interp (parse `{+ 1 {lambda {[x : num]} x}}) mt-env) "not a number") (test/exn (interp (parse `{let {[bad : (num -> num) {lambda {[x : num]} {+ x y}}]} {let {[y : num 5]} {bad 2}}}) mt-env) "free variable")) ;; num+ and num* ---------------------------------------- (define (num-op [op : (Number Number -> Number)] [l : Value] [r : Value]) : Value (cond [(and (numV? l) (numV? r)) (numV (op (numV-n l) (numV-n r)))] [else (error 'interp "not a number")])) (define (num+ [l : Value] [r : Value]) : Value (num-op + l r)) (define (num* [l : Value] [r : Value]) : Value (num-op * l r)) (module+ test (test (num+ (numV 1) (numV 2)) (numV 3)) (test (num* (numV 2) (numV 3)) (numV 6))) ;; lookup ---------------------------------------- (define (make-lookup [check? : ('a -> Boolean)] [name-of : ('a -> Symbol)] [val-of : ('a -> 'b)]) (lambda ([name : Symbol] [vals : (Listof 'a)]) : 'b (type-case (Listof 'a) vals [empty (error 'find "free variable")] [(cons val rst-vals) (if (and (check? val) (equal? name (name-of val))) (val-of (first vals)) ((make-lookup check? name-of val-of) name rst-vals))]))) (define lookup (make-lookup bind? bind-name (lambda (b) (type-case (Optionof Value) (unbox (bind-val b)) [(none) (error 'lookup "use before initialization")] [(some v) v])))) (module+ test (test/exn (lookup 'x mt-env) "free variable") (test (lookup 'x (extend-env (bind 'x (box (some (numV 8)))) mt-env)) (numV 8)) (test (lookup 'x (extend-env (bind 'x (box (some (numV 9)))) (extend-env (bind 'x (box (some (numV 8)))) mt-env))) (numV 9)) (test (lookup 'y (extend-env (bind 'x (box (some (numV 9)))) (extend-env (bind 'y (box (some (numV 8)))) mt-env))) (numV 8))) ;; typecheck ---------------------------------------- (define (typecheck [a : Exp] [tenv : Type-Env]) (type-case Exp a [(numE n) (numT)] [(plusE l r) (typecheck-nums l r tenv)] [(multE l r) (typecheck-nums l r tenv)] [(equalE l r) (if (equal? (typecheck l tenv) (typecheck r tenv)) (numT) (type-error l "same type"))] [(idE n) (type-lookup n tenv)] [(lamE n arg-type body) (begin (tvarcheck arg-type tenv) (arrowT arg-type (typecheck body (extend-env (tbind n arg-type) tenv))))] [(appE fun arg) (type-case Type (typecheck fun tenv) [(arrowT arg-type result-type) (if (equal? arg-type (typecheck arg tenv)) result-type (type-error arg (to-string arg-type)))] [else (type-error fun "function")])] [(letrecE n t rhs body) (begin (tvarcheck t tenv) (let ([new-tenv (extend-env (tbind n t) tenv)]) (if (equal? t (typecheck rhs new-tenv)) (typecheck body new-tenv) (type-error rhs (to-string t)))))] [(let-typeE type-name tag1 type1 tag2 type2 body) (let ([new-tenv (extend-env (tdef type-name tag1 type1 tag2 type2) tenv)]) (begin (tvarcheck type1 new-tenv) (tvarcheck type2 new-tenv) (let ([result-type (typecheck body (extend-env (tbind tag1 (arrowT type1 (definedT type-name))) (extend-env (tbind tag2 (arrowT type2 (definedT type-name))) new-tenv)))]) (if (contains-type? (definedT type-name) result-type) (type-error body (string-append "type without " (to-string type-name))) result-type))))] [(type-caseE type-name tst tag1 n1 rhs1 tag2 n2 rhs2) (let ([def (defined-type-lookup type-name tenv)]) (if (not (and (equal? tag1 (tdef-tag1 def)) (equal? tag2 (tdef-tag2 def)))) (type-error a "matching variant names") (type-case Type (typecheck tst tenv) [(definedT name) (if (not (equal? name type-name)) (type-error tst (to-string type-name)) (let ([rhs1-t (typecheck rhs1 (extend-env (tbind n1 (tdef-type1 def)) tenv))] [rhs2-t (typecheck rhs2 (extend-env (tbind n2 (tdef-type2 def)) tenv))]) (if (equal? rhs1-t rhs2-t) rhs1-t (type-error rhs2 (to-string rhs1-t)))))] [else (type-error tst (to-string type-name))])))])) (define (typecheck-nums l r tenv) (type-case Type (typecheck l tenv) [(numT) (type-case Type (typecheck r tenv) [(numT) (numT)] [else (type-error r "num")])] [else (type-error l "num")])) (define (type-error a msg) (error 'typecheck (string-append "no type: " (string-append (to-string a) (string-append " not " msg))))) (define type-lookup (make-lookup tbind? tbind-name tbind-type)) (define defined-type-lookup (make-lookup tdef? tdef-type-name (lambda (d) d))) (module+ test (test (typecheck (parse `10) mt-env) (numT)) (test (typecheck (parse `{+ 10 17}) mt-env) (numT)) (test (typecheck (parse `{* 10 17}) mt-env) (numT)) (test (typecheck (parse `{lambda {[x : num]} 12}) mt-env) (arrowT (numT) (numT))) (test (typecheck (parse `{lambda {[x : num]} {lambda {[y : bool]} x}}) mt-env) (arrowT (numT) (arrowT (boolT) (numT)))) (test (typecheck (parse `{{lambda {[x : num]} 12} {+ 1 17}}) mt-env) (numT)) (test (typecheck (parse `{let {[x : num 4]} {let {[f : (num -> num) {lambda {[y : num]} {+ x y}}]} {f x}}}) mt-env) (numT)) (test (typecheck (parse `{letrec {[f : bool f]} f}) mt-env) (boolT)) (test (typecheck (parse `{letrec {[f : (num -> num) {lambda {[x : num]} {+ x x}}]} {f 8}}) mt-env) (numT)) (test (typecheck (parse `{letrec {[f : (((num -> num) -> ((num -> num) -> (num -> num))) -> (num -> num)) {lambda {[sel : ((num -> num) -> ((num -> num) -> (num -> num)))]} {{sel {lambda {[x : num]} {{f {lambda {[f : (num -> num)]} {lambda {[g : (num -> num)]} g}}} 3}}} {lambda {[x : num]} x}}}]} {{f {lambda {[f : (num -> num)]} {lambda {[g : (num -> num)]} f}}} 9}}) mt-env) (numT)) (test/exn (typecheck (parse `{letrec {[x : (num -> num) 5]} x}) mt-env) "no type") ;; This example would typecheck if `let-type` allowed the result to ;; mention the defined type: (test/exn (typecheck (parse `{let-type [Fruit {apple num} {banana (num -> num)}] {apple 1}}) mt-env) "no type") ; instead of (definedT 'Fruit) (test (typecheck (parse `{let-type [Fruit {apple num} {banana (num -> num)}] {let {[a : Fruit {apple 1}]} 5}}) mt-env) (numT)) (test (typecheck (parse `{let-type [Fruit {apple num} {banana (num -> num)}] {let {[b : Fruit {banana {lambda {[x : num]} 3}}]} 5}}) mt-env) (numT)) (test (typecheck (parse `{let-type [Fruit {apple num} {banana (num -> num)}] {let {[f : (Fruit -> num) {lambda {[f : Fruit]} {type-case Fruit f [{apple a} a] [{banana g} {g 2}]}}]} {+ {f {apple 1}} {f {banana {lambda {[n : num]} {+ n 3}}}}}}}) mt-env) (numT)) (test/exn (typecheck (parse `{type-case Fruit 1 [{apple a} 1] [{banana b} 1]}) mt-env) "free variable") (test/exn (typecheck (parse `{let-type [Fruit {apple num} {banana (num -> num)}] {+ apple 1}}) mt-env) "no type") (test/exn (typecheck (parse `{let-type [Fruit {apple num} {banana (num -> num)}] {banana 1}}) mt-env) "no type") (test/exn (typecheck (parse `{let-type [Fruit {apple num} {banana (num -> num)}] {type-case Fruit {apple 1} [{lion a} 1] [{bear b} 1]}}) mt-env) "no type") (test/exn (typecheck (parse `{let-type [Fruit {apple num} {banana (num -> num)}] {type-case Fruit 1 [{apple a} 1] [{banana b} 1]}}) mt-env) "no type") (test/exn (typecheck (parse `{let-type [Fruit {apple num} {banana (num -> num)}] {let-type [Animal {lion num} {bear num}] {type-case Fruit {lion 1} [{apple a} 1] [{banana b} 1]}}}) mt-env) "no type") (test/exn (typecheck (parse `{let-type [Fruit {apple num} {banana (num -> num)}] {type-case Fruit {apple 1} [{apple a} a] [{banana b} b]}}) mt-env) "no type") (test/exn (typecheck (parse `{1 2}) mt-env) "no type") (test/exn (typecheck (parse `{{lambda {[x : bool]} x} 2}) mt-env) "no type") (test/exn (typecheck (parse `{+ 1 {lambda {[x : num]} x}}) mt-env) "no type") (test/exn (typecheck (parse `{* {lambda {[x : num]} x} 1}) mt-env) "no type")) ;; ---------------------------------------- (define (tvarcheck ty tenv) (type-case Type ty [(numT) (values)] [(boolT) (values)] [(arrowT a b) (begin (tvarcheck a tenv) (tvarcheck b tenv))] [(definedT id) (begin (defined-type-lookup id tenv) (values))])) (module+ test (test (tvarcheck (numT) mt-env) (values)) (test (tvarcheck (boolT) mt-env) (values)) (test (tvarcheck (arrowT (numT) (boolT)) mt-env) (values)) (test (tvarcheck (definedT 'Fruit) (extend-env (tdef 'Fruit 'apple (numT) 'banana (arrowT (numT) (numT))) mt-env)) (values)) (test/exn (tvarcheck (definedT 'Fruit) mt-env) "free variable")) ;; ---------------------------------------- (define (contains-type? find-ty ty) (or (equal? find-ty ty) (type-case Type ty [(numT) #f] [(boolT) #f] [(arrowT a b) (or (contains-type? find-ty a) (contains-type? find-ty b))] [(definedT id) #f]))) (module+ test (test (contains-type? (definedT 'Fruit) (numT)) #f) (test (contains-type? (definedT 'Fruit) (boolT)) #f) (test (contains-type? (definedT 'Fruit) (arrowT (boolT) (numT))) #f) (test (contains-type? (definedT 'Fruit) (definedT 'Animal)) #f) (test (contains-type? (definedT 'Fruit) (definedT 'Fruit)) #t) (test (contains-type? (definedT 'Fruit) (arrowT (numT) (definedT 'Fruit))) #t))