#lang plai-typed (require plai-typed/s-exp-match) ;; Start with "type-case.rkt" ;; Add a new test case to that ends ;; ;; {+ {toKelvin {F 32}} ;; {toKelvin {C 0}}} ;; ;; where `F` and `C` are constructors for a ;; `Degrees` type in the book language ;; (in Fahrenheit or Celsius, respotively). ;; ;; Recall that Celsius + 273.15 = Kelvin ;; and (Fahrenheit -32) * 5/9 = Celsius (module+ test (define degrees-example (parse '{let-type {Temperature {F num} {C num}} {let {[toKelvin : {Temperature -> num} {lambda {[T : Temperature]} {type-case Temperature T {F {n} {+ {* {+ n -32} 5/9} 273.15}} {C {n} {+ n 273.15}}}}]} {+ {toKelvin {F 32}} {toKelvin {C 0}}}}})) (test (typecheck degrees-example mt-env) (numT)) (test (interp degrees-example mt-env) (numV (+ 273.15 273.15)))) ;; ---------------------------------------- ;; Add `equal?`, which is implemented not using plai-type's `equal?` ;; ---------------------------------------- (define-type Value [numV (n : number)] [closV (arg : symbol) (body : ExprC) (env : Env)] [undefinedV] ; for letrec [variantV (tag : symbol) (val : Value)] [constructorV (tag : symbol)]) (define-type ExprC [numC (n : number)] [idC (s : symbol)] [plusC (l : ExprC) (r : ExprC)] [multC (l : ExprC) (r : ExprC)] [eqC (l : ExprC) (r : ExprC)] [lamC (n : symbol) (arg-type : Type) (body : ExprC)] [appC (fun : ExprC) (arg : ExprC)] [letrecC (n : symbol) (n-type : Type) (rhs : ExprC) (body : ExprC)] [let-typeC (type-name : symbol) (tag1 : symbol) (type1 : Type) (tag2 : symbol) (type2 : Type) (body : ExprC)] [type-caseC (type-name : symbol) (tst : ExprC) (tag1 : symbol) (n1 : symbol) (rhs1 : ExprC) (tag2 : symbol) (n2 : symbol) (rhs2 : ExprC)]) (define-type Type [numT] [boolT] [arrowT (arg : Type) (result : Type)] [definedT (name : symbol)]) (define-type Binding [bind (name : symbol) (val : (boxof Value))]) (define-type-alias Env (listof Binding)) (define-type TypeBinding [tbind (name : symbol) (type : Type)] [tdef (type-name : symbol) (tag1 : symbol) (type1 : Type) (tag2 : symbol) (type2 : Type)]) (define-type-alias TypeEnv (listof TypeBinding)) (define mt-env empty) (define extend-env cons) (module+ test (print-only-errors true)) ;; parse ---------------------------------------- (define (parse [s : s-expression]) : ExprC (cond [(s-exp-match? `NUMBER s) (numC (s-exp->number s))] [(s-exp-match? `SYMBOL s) (idC (s-exp->symbol s))] [(s-exp-match? '{+ ANY ANY} s) (plusC (parse (second (s-exp->list s))) (parse (third (s-exp->list s))))] [(s-exp-match? '{* ANY ANY} s) (multC (parse (second (s-exp->list s))) (parse (third (s-exp->list s))))] [(s-exp-match? '{equal? ANY ANY} s) (eqC (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)))))]) (appC (lamC (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)))))]) (letrecC (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)))))]) (lamC (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-typeC (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-caseC (s-exp->symbol (second (s-exp->list s))) (parse (third (s-exp->list s))) (s-exp->symbol (first case1)) (s-exp->symbol (first (s-exp->list (second case1)))) (parse (third case1)) (s-exp->symbol (first case2)) (s-exp->symbol (first (s-exp->list (second case2)))) (parse (third case2))))] [(s-exp-match? '{ANY ANY} s) (appC (parse (first (s-exp->list s))) (parse (second (s-exp->list s))))] [else (error 'parse "invalid input")])) (define (parse-type [s : s-expression]) : 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) (numC 2)) (test (parse `x) ; note: backquote instead of normal quote (idC 'x)) (test (parse '{+ 2 1}) (plusC (numC 2) (numC 1))) (test (parse '{* 3 4}) (multC (numC 3) (numC 4))) (test (parse '{+ {* 3 4} 8}) (plusC (multC (numC 3) (numC 4)) (numC 8))) (test (parse '{let {[x : num {+ 1 2}]} y}) (appC (lamC 'x (numT) (idC 'y)) (plusC (numC 1) (numC 2)))) (test (parse '{letrec {[x : num {+ 1 2}]} y}) (letrecC 'x (numT) (plusC (numC 1) (numC 2)) (idC 'y))) (test (parse '{lambda {[x : num]} 9}) (lamC 'x (numT) (numC 9))) (test (parse '{double 9}) (appC (idC 'double) (numC 9))) (test (parse '{let-type {Fruit [apple num] [banana (num -> num)]} 1}) (let-typeC 'Fruit 'apple (numT) 'banana (arrowT (numT) (numT)) (numC 1))) (test (parse '{type-case Fruit 1 [apple {a} 2] [banana {b} 3]}) (type-caseC 'Fruit (numC 1) 'apple 'a (numC 2) 'banana 'b (numC 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")) ;; interp ---------------------------------------- (define (interp [a : ExprC] [env : Env]) : Value (type-case ExprC a [numC (n) (numV n)] [idC (s) (lookup s env)] [plusC (l r) (num+ (interp l env) (interp r env))] [multC (l r) (num* (interp l env) (interp r env))] [eqC (l r) (let ([r-v (interp r env)] [l-v (interp l env)]) (if (undefinedV? r-v) (error 'interp "undefined value") (letrec ([eq-val? (lambda (l-v r-v) (type-case Value l-v [numV (n) (= n (numV-n r-v))] [closV (arg body env) (eq? l-v r-v)] [variantV (tag val) (and (eq? tag (variantV-tag r-v)) (eq-val? val (variantV-val r-v)))] [constructorV (tag) (and (constructorV? r-v) (eq? tag (constructorV-tag r-v)))] [undefinedV () (error 'interp "undefined value")]))]) (if (eq-val? l-v r-v) (numV 0) (numV 1)))))] [lamC (n t body) (closV n body env)] [appC (fun arg) (type-case Value (interp fun env) [closV (n body c-env) (interp body (extend-env (bind n (box (interp arg env))) c-env))] [constructorV (tag) (variantV tag (interp arg env))] [else (error 'interp "not a function")])] [letrecC (n t rhs body) (let ([b (box (undefinedV))]) (let ([new-env (extend-env (bind n b) env)]) (begin (set-box! b (interp rhs new-env)) (interp body new-env))))] [let-typeC (type-name tag1 type1 tag2 type2 body) (interp body (extend-env (bind tag1 (box (constructorV tag1))) (extend-env (bind tag2 (box (constructorV tag2))) env)))] [type-caseC (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 val)) env))] [(eq? tag tag2) (interp rhs2 (extend-env (bind n2 (box 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 (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 (plusC (idC 'x) (idC '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 (interp (parse '{letrec {[f : num f]} f}) mt-env) (undefinedV)) (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") (test (interp (parse '{equal? 1 1}) mt-env) (numV 0)) (test (interp (parse '{equal? 1 0}) mt-env) (numV 1)) (test (interp (parse '{let {[f : (num -> num) {lambda {[x : num]} x}]} {equal? f f}}) mt-env) (numV 0)) (test (interp (parse '{equal? {lambda {[x : num]} x} {lambda {[x : num]} 0}}) mt-env) (numV 1)) (test (interp (parse '{let-type {Animal [lion num] [bear num]} {equal? {lion 1} {lion 1}}}) mt-env) (numV 0)) (test (interp (parse '{let-type {Animal [lion num] [bear num]} {equal? {lion 1} {lion 0}}}) mt-env) (numV 1)) (test (interp (parse '{let-type {Animal [lion num] [bear num]} {equal? {lion 1} {bear 1}}}) mt-env) (numV 1)) (test (interp (parse '{let-type {Animal [lion num] [bear num]} {equal? lion lion}}) mt-env) (numV 0)) (test (interp (parse '{let-type {Animal [lion num] [bear num]} {equal? lion bear}}) mt-env) (numV 1)) (test/exn (interp (parse '{letrec {[x : num x]} {equal? x 1}}) mt-env) "undefined value") (test/exn (interp (parse '{letrec {[x : num x]} {equal? 1 x}}) mt-env) "undefined value")) ;; 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 (cond [(empty? vals) (error 'find "free variable")] [else (if (and (check? (first vals)) (equal? name (name-of (first vals)))) (val-of (first vals)) ((make-lookup check? name-of val-of) name (rest vals)))]))) (define lookup (make-lookup bind? bind-name (lambda (b) (unbox (bind-val b))))) (module+ test (test/exn (lookup 'x mt-env) "free variable") (test (lookup 'x (extend-env (bind 'x (box (numV 8))) mt-env)) (numV 8)) (test (lookup 'x (extend-env (bind 'x (box (numV 9))) (extend-env (bind 'x (box (numV 8))) mt-env))) (numV 9)) (test (lookup 'y (extend-env (bind 'x (box (numV 9))) (extend-env (bind 'y (box (numV 8))) mt-env))) (numV 8))) ;; typecheck ---------------------------------------- (define (typecheck [a : ExprC] [tenv : TypeEnv]) (type-case ExprC a [numC (n) (numT)] [plusC (l r) (typecheck-nums l r tenv)] [multC (l r) (typecheck-nums l r tenv)] [eqC (l r) (if (equal? (typecheck l tenv) (typecheck r tenv)) (numT) (type-error r "types are not the same"))] [idC (n) (type-lookup n tenv)] [lamC (n arg-type body) (begin (tvarcheck arg-type tenv) (arrowT arg-type (typecheck body (extend-env (tbind n arg-type) tenv))))] [appC (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")])] [letrecC (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-typeC (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-caseC (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") (test (typecheck (parse '{equal? 1 1}) mt-env) (numT)) (test (typecheck (parse '{equal? {lambda {[x : num]} x} {lambda {[x : num]} 1}}) mt-env) (numT)) (test/exn (typecheck (parse '{equal? 1 {lambda {[x : num]} 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))