'&$%CSE 341:Programming LanguagesDan GrossmanSpring 2008Lecture 18— Static vs. dynamic typingDan Grossman CSE341 Spring 2008, Lecture 18 1'&$%TodayConsider one of the biggest differences between Scheme and ML:• ML is statically typed (many errors when compiled)• Scheme is dynamically typed (many errors when run)More generally:• Why is static typing good/bad?• How do you judge a type system?Dan Grossman CSE341 Spring 2008, Lecture 18 2'&$%Strong typing vs. Weak typingIn languages with weak typing, there exist programs thatimplementations must accept at compile-time, but at run-time theprogram can do anything, including blow-up your computer.• Examples: C, C++Old wisdom: Strong types for we ak mindsNew wisdom: Weak typing endangers society & costs > $1e10/yearWhy weak typing? For efficiency and low-level implementation(important for small parts of low- leve l syst ems )My view: Programming is hard enough withoutimplementation-defined behavior. This has little to do with types:• ML, Scheme, Java, Ruby all “strongly typed” in this senseDan Grossman CSE341 Spring 2008, Lecture 18 3'&$%Static Typing vs. D ynamic TypingIn ML and Scheme "hi" - "mom" or (- "hi" "mom") are errors.• In ML it’s “at compile-time” (static)• In Scheme it’s “at run-time” (dynamic)(define (f) (- "hi" "mom")) fine until you call it, but nevertype-checks in ML.This also never type-checks in ML, but may never fail if calledappropriately:(define (f g x y) fun f (g,x,y) =(if (g x) if g x(string-length y) then String.size y(+ y 1))) else y + 1 (* type-error! *)Dan Grossman CSE341 Spring 2008, Lecture 18 4'&$%Basic benefits/limitationsIndisputable facts:• A language with static checks catches certain bugs without testing(earlier in the software-development cycle)• It’s impossible to catch exactly the buggy programs atcompile-time– Impossible (undecidable) to know what code will execute inwhat environments, so may give false positives– Impossible to know exactly what types a function argumentmight have without running the program, so may give falsepositives– Algorithm bugs remain (e.g., using + where you meant -)Dan Grossman CSE341 Spring 2008, Lecture 18 5'&$%Static CheckingKey questions for a compile-time check (e.g., ML type-checking):1. What is it checking? Examples (and not):• Yes: Primitives (e.g., +) aren’t applied to inappropriate values• Yes: Module interfaces are respected(e.g., don’t use private functions)• Yes: Patterns are not redundant• No: hd is never applied to the empty list• No: Array indices are in boundsKnowing what is caught for me affects how I program.2. Is it sound? (Does it ever accept a program that at run-time doeswhat we claimed it could not? “false negative”)3. Is it complete? (Does it ever reject a program that could not dothe “bad thing” at run-time? “false positive”)Dan Grossman CSE341 Spring 2008, Lecture 18 6'&$%Unfortunately...All non-trivial static analyses are either unsound or incomplete.• Direct corollary to CSE322 concept of undecidabilityGood design leads to “useful subsets” of all programs, typically (butnot always) ensuring soundness and sacrificing completeness.• Forbid all programs that do some “bad” things(like pass a function to +)• Also forbid some programs that don’t do the bad things becausewe can’t tellTo judge a type system:• Is it sound (or is it “broken”)?• Is it “expressive enough” (is the incompleteness palatable)?Dan Grossman CSE341 Spring 2008, Lecture 18 7'&$%A Question of EagernessAgain, eve ry static type system provides certain guarantees. Somethings we might want to check statically (soundly but incompletely),but ML and Java’s type system don’t: no null-pointer exce ptions, nodivision-by-zero, no data races, ...There is also more than “compile-time” or “run-time”.Consider 3 / 0.• Compile-time: reject if code is “reachable” (maybe dead branch)• Link-time: reject if code is “reachable” (maybe unused function)• Run-time: reject if code executes (maybe branch never taken)• Even later: maybe delay error until “bad number” is used to indexinto an array or something.– Crazy? Floating-point allows 3.0 / 0.0; gives you +inf.0.Dan Grossman CSE341 Spring 2008, Lecture 18 8'&$%Explorin g Some Argumen ts1a. Dynamic typing is more convenient(define (f x) (if (> x 0) (* 2 x) #f))(let ([ans (f y)]) (if ans e1 e2))datatype intOrBool = Int of int | Bool of boolfun f x = if x > 0 then Int (2*x) else Bool falsecase f y ofInt ans => e1| Bool _ => e2Just return what you want; no need to define datatype s (usethe-one-big-datatype)Dan Grossman CSE341 Spring 2008, Lecture 18 9'&$%Explorin g Some Argumen ts1b. Static typing is more convenient(define (cube x) (if (not (number? x))(error "bad arguments")(* x x x)))(cube 7)fun cube x = x * x * xcube 7With dynamic-typing, assuming things about arguments can lead toerrors far from the logical mistake(“expected foo got bar” deep in some library)Dan Grossman CSE341 Spring 2008, Lecture 18 10'&$%Explorin g Some Argumen ts2. Static typing prevents / doesn’t preve nt useful programs• Overly restrictive type s yste ms certainly can (e.g., withoutpolymorphism a new list library for each list-element type )• datatype gives you as much or as little flexibility as you want –can embed Scheme in ML:datatype SchemeVal = Int of int | String of string| Fun of SchemeVal -> SchemeVal| Cons of SchemeVal * SchemeValif e1then Fun (fn x => case x of Int i => Int (i * i * i))else Cons (Int 7, String "hi")Viewed this way, Scheme is “unityped” with “implicittag-checking” which is “just” a matter of convenience.Dan Grossman CSE341 Spring 2008, Lecture 18 11'&$%Explorin g Some Argumen ts3. Static/dynamic typing better for code evolutionChange:fun f x = x * 2 (define (f x) (* x 2))to:datatype t = I of int| S of stringfun f x = (define (f x)case x of (if (number? x)I i => I (i * 2) (* x 2)| S s => S (s ^ s) (string-append x x)))• Good example for dynamic: In ML, all callers must change• But: If we change the return type of f, ML type-checker will giveus a full t o-do list of what to c hange.Dan Grossman CSE341 Spring 2008, Lecture 18 12'&$%Another evolution exampleSuppose I add a new constructor to an ML datatype(like a Mult for arithmetic expressions)• Most existing patterns over the type will now give a warning– Good reason not to use _ patterns• But if I “know” some expressions will not be
View Full Document
Unlocking...