#lang plaitypus (print-only-errors #t) ; DIFFERENT! (define-type Type [numberT] [arrowT (param : Type) (result : Type)]) (define-type TypeEnv [mtEnv] [aBind (name : symbol) (type : Type) (rest : TypeEnv)]) (define-type TFAE [num (n : number)] [add (lhs : TFAE) (rhs : TFAE)] [sub (lhs : TFAE) (rhs : TFAE)] [id (name : symbol)] [fun (param-name : symbol) (param-type : Type) (body : TFAE)] [app (fun-expr : TFAE) (arg-expr : TFAE)]) ;; ---------------------------------------------------------------------- ;; Now that we have a typechecker, we have to be a lot more explicit about ;; what types of data we're using, and how we're converting between them. ;; Otherwise, the typechecker can't prove that what we're doing is ok. ;; We lose flexibility, but gain safety. (define parse : (s-expression -> TFAE) (lambda (s-exp) (cond [(s-exp-number? s-exp) (num (s-exp->number s-exp))] [(s-exp-symbol? s-exp) (id (s-exp->symbol s-exp))] [(s-exp-list? s-exp) (define as-list (s-exp->list s-exp)) (cond [(empty? as-list) (error 'parse "the empty list is not a valid FAE")] [(s-exp-symbol? (first as-list)) (case (s-exp->symbol (first as-list)) [(+) (check-pieces as-list "add" 3) (add (parse (second as-list)) (parse (third as-list)))] [(-) (check-pieces as-list "sub" 3) (sub (parse (second as-list)) (parse (third as-list)))] [(fun) (check-pieces as-list "fun" 3) (unless (s-exp-list? (second as-list)) (error 'parse "expected parameter list")) (define param-list (s-exp->list (second as-list))) (check-pieces param-list "parameter list" 3) (unless (s-exp-symbol? (first param-list)) (error 'parse "expected symbol as parameter name")) (unless (and (s-exp-symbol? (second param-list)) (equal? ': (s-exp->symbol (second param-list)))) (error 'parse "expected `:`")) (fun (s-exp->symbol (first param-list)) (parse-type (third param-list)) (parse (third as-list)))] [else (parse-app as-list)])] [else (parse-app as-list)])] [else (error 'parse "wat")]))) (define parse-app : ((listof s-expression) -> TFAE) (lambda (s-exps) (check-pieces s-exps "app" 2) (app (parse (first s-exps)) (parse (second s-exps))))) (define parse-type : (s-expression -> Type) (lambda (s-exp) (cond [(and (s-exp-symbol? s-exp) (equal? 'number (s-exp->symbol s-exp))) (numberT)] [(s-exp-list? s-exp) (define as-list (s-exp->list s-exp)) (check-pieces as-list "function type" 3) (if (and (s-exp-symbol? (second as-list)) (equal? '-> (s-exp->symbol (second as-list)))) (arrowT (parse-type (first as-list)) (parse-type (third as-list))) (error 'parse "expected `->`"))]))) (define check-pieces : ((listof s-expression) string number -> void) (lambda (s-exps expected n-pieces) (unless (= n-pieces (length s-exps)) ;; With a typechecker, niceties like `error` taking 2 *or more* arguments ;; are gone. Hard for a typechecker to prove it's ok! (error 'parse (string-append (string-append "expected " expected) (string-append " got " (to-string s-exps))))))) ;; ---------------------------------------------------------------------- (define typecheck : (TFAE TypeEnv -> Type) (lambda (a-tfae gamma) ...)) ;; ---------------------------------------------------------------------- (test (typecheck (parse `5) (mtEnv)) (numberT)) (test (typecheck (parse `{+ 4 5}) (mtEnv)) (numberT)) (test (typecheck (parse `{- 4 5}) (mtEnv)) (numberT)) (test/exn (typecheck (parse `{+ 4 {fun {x : number} x}}) (mtEnv)) "expected number") (test (typecheck (parse `{fun {x : number} x}) (mtEnv)) (parse-type `(number -> number))) (test (typecheck (parse `{fun {x : number} {+ x 5}}) (mtEnv)) (parse-type `(number -> number))) (test (typecheck (parse `{fun {f : (number -> number)} {f 5}}) (mtEnv)) (parse-type `((number -> number) -> number))) (test (typecheck (parse `{{fun {x : number} x} 5}) (mtEnv)) (numberT)) (test (typecheck (parse `{{fun {f : (number -> number)} {f 5}} {fun {x : number} x}}) (mtEnv)) (numberT)) (test/exn (typecheck (parse `{4 5}) (mtEnv)) "expected function") (test/exn (typecheck (parse `{{fun {f : (number -> number)} {f 5}} 4}) (mtEnv)) "wrong argument type")