Types, Type Checking
- A language is latently or dynamically typed if it is possible to determine the type of a value at runtime.
Scheme is latently typed -- every value has a tag which indicates its type, and there are predicates for recognizing each type (number?, symbol?, string?, vector?, null?, pair?, boolean?, procedure?).
- A language is statically typed if it is possible to determine the type of each expression from the text of the program. Each variable and procedure is explicitly typed, or it is possible to infer their types.
- In a a strongly statically typed language, a type checker can determine whether there is an attempt in a program to
Java is strongly statically typed. Compilation errors are reported if there are any type errors.
- apply a non-procedure.
- apply a procedure to the wrong number of arguments,
- apply a procedure to an argument of the wrong type,
- use a non-boolean as the test in a conditional.
- Static type checking
- We will associate a type expression with each expression.
- The type of an integer is
int.- The type of a boolean is
bool.- The type of a procedure with parameter
t1and value of typetis(t1 -> t)- The type of a procedure with parameters
t1,t2,... and value of typetis((t1 * t2 * ...) -> t)- Examples (in DL)
Type Expression (int -> bool) zero? (int -> int) add1 ((int * int) -> int) + (int -> (int -> int) proc (x) proc (y) +(x, y) ((int -> int) * int -> bool proc (f, x) zero?((f add1(x)))- We introduce type expressions
with abstract syntax[type-exp] ::= int [type-exp] ::= bool [type-exp] ::= ( -> [type-exp]) | ([type-exp] {* [type-exp]}* -> [type-exp])int-type-exp () bool-type-exp () proc-type-exp (argument-type-exps result-type-exp)- And we modify our grammar with concrete syntax (to obtain STDK?)
with abstract syntax[expression] ::= proc () [expression] | proc ([type-exp] [id] {, [type-exp] [id]}*) [expression] | letrec {[type-exp] [id] ({[type-id] [id]}*(,) ) = [expression]}* in [expression] | true | falseproc-exp (argument-type-exps ids body) letrec-exp (result-type-exps proc-names argument-type-expss idss bodies letrec-body) true-exp false-exp- Example programs with this syntax:
proc (int x) add1(x) letrec int fact (int x) = if zero(x) then 1 else *(x, (fact sub1(x))) in fact proc ((int -> bool) p, int x) (p x) proc (int x) proc (int y) +(x, y) proc ((int -> int) f, int x) zero?((f add1(x)))- We can type any expression in a type environment -- an environment in which each variable is bound to its type -- with the following rules. ([[exp]] denotes abstract syntax.)
- Type rules for integer, boolean values:
If the equations above the line hold, then the equation below the line holds.(type-of-expression [[b]] tenv) = bool (type-of-expression [[id]] tenv) = (apply-env tenv id)
- Type rule for applications:
(type-of-expression [[rator]] tenv) = (t1 * t2 * ... * tn) -> t (type-of-expression [[rand1]] tenv) = t1 (type-of-expression [[rand2]] tenv) = t2 ... (type-of-expression [[randn]] tenv) = tn ---------------------------------------------------------------- (type-of-expression [[(rator rand1 rand2 ... randn)]] tenv) = t- Type rule for if:
(type-of-expression [[test-exp]] tenv) = bool (type-of-expression [[true-exp]] tenv) = t (type-of-expression [[false-exp]] tenv) = t ---------------------------------------------------------------- (type-of-expression [[if test-exp then true-exp else false-exp]] tenv) = t- Type rule for procedures: (Recall notation for extended envs)
(type-of-expression [[exp]] [x1 = t1,..., xn = tn]tenv) = t ---------------------------------------------------------------- (type-of-expression [[proc (x1,..., xn) exp]] tenv) = (t1 * t2 * ... * tn) -> t
- A
typedata type is introduced for analysis-time representation of types. There are two kinds of types, atomic and procedure.Type expressions are converted to types by
expand-type-expression.The primitive types:(define-datatype type type? (atomic-type (name symbol?)) (proc-type (arg-types (list-of type?)) (result-type type?))) (define expand-type-expression (lambda (texp) (cases type-exp texp (int-type-exp () int-type) (bool-type-exp () bool-type) (proc-type-exp (arg-texps result-texp) (proc-type (expand-type-expressions arg-texps) (expand-type-expression result-texp)))))) (define expand-type-expressions (lambda (texps) (map expand-type-expression texps)))(define int-type (atomic-type 'int)) (define bool-type (atomic-type 'bool)) (define type-of-primitive (lambda (prim) (cases primitive prim (add-prim () (proc-type (list int-type int-type) int-type)) (subtract-prim () (proc-type (list int-type int-type) int-type)) (mult-prim () (proc-type (list int-type int-type) int-type)) (incr-prim () (proc-type (list int-type) int-type)) (decr-prim () (proc-type (list int-type) int-type)) (zero-test-prim () (proc-type (list int-type) bool-type)))))- Type environments.
(define-datatype type-environment type-environment? (empty-tenv-record) (extended-tenv-record (syms (list-of symbol?)) (vals (list-of type?)) (tenv type-environment?))) (define empty-tenv empty-tenv-record) (define extend-tenv extended-tenv-record) (define apply-tenv (lambda (tenv sym) (cases type-environment tenv (empty-tenv-record () (eopl:error 'apply-tenv "unbound variable ~s" sym)) (extended-tenv-record (syms vals env) (let ((position (list-find-position sym syms))) (if (number? position) (list-ref vals position) (apply-tenv env sym)))))))type-of-expressionhas abstract syntax and type environmen parameters, and returns a type expression or signals an error.type-to-external-formconverts a type expression to external form.(define type-to-external-form (lambda (ty) (cases type ty (atomic-type (name) name) (proc-type (arg-types result-type) (append (arg-types-to-external-form arg-types) '(->) (list (type-to-external-form result-type))))))) (define arg-types-to-external-form (lambda (types) (if (null? types) '() (if (null? (cdr types)) (list (type-to-external-form (car types))) (cons (type-to-external-form (car types)) (cons '* (arg-types-to-external-form (cdr types))))))))- Interface to the type checker in 7.2.scm.
(define type-check (lambda (string) (type-to-external-form (type-of-program (scan&parse string))))) (define run (lambda (string) (eval-program (scan&parse string)))) (define run-all (lambda () (run-list all-tests))) (define check-all (lambda () (check-list all-tests)))- The type checker (from 7.2.scm)
(define type-of-program (lambda (pgm) (cases program pgm (a-program (exp) (type-of-expression exp (empty-tenv)))))) (define type-of-expression (lambda (exp tenv) (cases expression exp (lit-exp (number) int-type) (true-exp () bool-type) (false-exp () bool-type) (var-exp (id) (apply-tenv tenv id)) (if-exp (test-exp true-exp false-exp) (let ((test-type (type-of-expression test-exp tenv)) (true-type (type-of-expression true-exp tenv)) (false-type (type-of-expression false-exp tenv))) ;; these tests either succeed or raise an error (check-equal-type! test-type bool-type test-exp) (check-equal-type! true-type false-type exp) true-type)) (proc-exp (texps ids body) (type-of-proc-exp texps ids body tenv)) (primapp-exp (prim rands) (type-of-application (type-of-primitive prim) (types-of-expressions rands tenv) prim rands exp)) (app-exp (rator rands) (type-of-application (type-of-expression rator tenv) (types-of-expressions rands tenv) rator rands exp)) (let-exp (ids rands body) (type-of-let-exp ids rands body tenv)) (letrec-exp (result-texps proc-names texpss idss bodies letrec-body) (type-of-letrec-exp result-texps proc-names texpss idss bodies letrec-body tenv))))) (define check-equal-type! (lambda (t1 t2 exp) (or (equal? t1 t2) (eopl:error 'type-of-expression "types didn't match: ~s != ~s in~%~s" (type-to-external-form t1) (type-to-external-form t2) exp)))) (define type-of-proc-exp (lambda (texps ids body tenv) (let ((arg-types (expand-type-expressions texps))) (let ((result-type (type-of-expression body (extend-tenv ids arg-types tenv)))) (proc-type arg-types result-type))))) (define type-of-application (lambda (rator-type rand-types rator rands exp) (cases type rator-type (proc-type (arg-types result-type) (if (= (length arg-types) (length rand-types)) (begin (for-each (lambda (arg-type rator-type rand) (check-equal-type! rator-type arg-type rand)) arg-types rand-types rands) result-type) (eopl:error 'type-of-expression "wrong number of arguments in expression ~s:~%expected ~s~%got ~s" exp (map type-to-external-form arg-types) (map type-to-external-form rand-types)))) (else (eopl:error 'type-of-expression "rator not a proc type:~%~s~%had rator type ~s" rator (type-to-external-form rator-type)))))) (define types-of-expressions (lambda (rands tenv) (map (lambda (exp) (type-of-expression exp tenv)) rands))) (define type-of-let-exp (lambda (ids rands body tenv) (let ((new-tenv (extend-tenv ids (types-of-expressions rands tenv) tenv))) (type-of-expression body new-tenv)))) (define type-of-letrec-exp (lambda (result-texps proc-names texpss idss bodies letrec-body tenv) (let ((arg-typess (map (lambda (texps) (expand-type-expressions texps)) texpss)) (result-types (expand-type-expressions result-texps))) (let ((the-proc-types (map proc-type arg-typess result-types))) (let ((tenv-for-body ; type env for all proc-bodies (extend-tenv proc-names the-proc-types tenv))) (for-each (lambda (ids arg-types body result-type) (check-equal-type! (type-of-expression body (extend-tenv ids arg-types tenv-for-body)) result-type body)) idss arg-typess bodies result-types) (type-of-expression letrec-body tenv-for-body))))))- To use 7-2.scm, first load
Search for "add-test" to see the tests, with types and values.
(check-all)-- to check types
(run-all)-- to check values