CSE341: Programming Languages Lecture 18 Static vs. Dynamic Typing Dan Grossman Fall 2011Static vs. dynamic typing • A big, juicy, essential, topic about how to think about PLs – Conversation usually overrun with half-informed opinions – Will consider reasonable arguments “for” and “against” last • First need to understand: – What static checking (e.g., with a type system) means – What static checking intends to do (details depend on PL) – Why static checking must be approximate – The standard features of a type system – A more general view of how eager should error detection be Fall 2011 2 CSE341: Programming LanguagesStatic checking • Static checking is anything done to reject a program after it (successfully) parses but before it runs • What static checking is performed is part of the PL definition – A “helpful tool” could do more • Most common way to define a PL’s static checking is via a type system – Approach is to give each variable, expression, etc. a type – Purposes include preventing misuse of primitives (e.g., 4/"hi") and avoiding dynamic checking (dynamic means at run-time) • Dynamically typed PLs (Racket, Ruby) do much less static checking – Maybe none but the line is fuzzy Fall 2011 3 CSE341: Programming LanguagesExample: ML, what types prevent In ML, type-checking ensures a program (when run) will never: • Use a primitive operation on a value of the wrong type – Use arithmetic on a non-number – Have e1 e2 where e1 does not evaluate to a function – Have a non-boolean between if and then • Use a variable that is not in the environment • Have a pattern-match with a redundant pattern • Have code outside a module directly call a function not in the module’s signature • … The first two are “standard” for type systems Fall 2011 4 CSE341: Programming LanguagesExample: ML, what types don’t prevent In ML, type-checking does not prevent any of these errors – Instead, detected at run-time • Calling functions such that exceptions occur, e.g., hd [] • An array-bounds error • Division-by-zero And in general no type system prevents logic / algorithmic errors: • Reversing the branches of a conditional • Calling f instead of g Fall 2011 5 CSE341: Programming LanguagesThe purpose is to prevent something Have discussed facts about what the ML type system does and does not prevent – Without discussing how (e.g., one type for each variable) though we already studied many of ML’s typing rules Part of language design is deciding what is checked and how – Hard part is making sure the type system does it correctly – Definition of correctness on next slide A different language can prevent different things, e.g., – Java: Checks no casts unless supertype or subtype – OCaml: Lets you use = on any two types (not just eqtypes) Fall 2011 6 CSE341: Programming LanguagesCorrectness Suppose a type system is supposed to prevent X for some X • A type system is sound if it never accepts a program that, when run with some input, does X – No false negatives • A type system is complete if it never rejects a program that, no matter what input it is run with, will not do X – No false positives The goal is usually for a PL type system to be sound (so you can rely on it) but not complete – “Fancy features” like generics aimed at “less incomplete” Notice soundness/completeness is with respect to X Fall 2011 7 CSE341: Programming LanguagesIncompleteness A few functions ML rejects even though they do not divide by a string Fall 2011 8 CSE341: Programming Languages fun f1 x = 4 div "hi" (* but f1 never called *) fun f2 x = if true then 0 else 4 div "hi" fun f3 x = if x then 0 else 4 div "hi" val x = f3 true fun f4 x = if x <= abs x then 0 else 4 div "hi" fun f5 x = 4 div x val y = f5 if true then 1 else "hi"Why incompleteness • Almost anything you might like to check statically is undecidable: – Any static checker that always terminates cannot be sound and complete • Examples: – Will this function terminate on some input? On any input? – Will this function ever use a variable not in the environment? – Will this function treat a string as a function? – Will this function divide by zero? • Undecidability is discussed in CSE 311 – The inherent approximation of static checking is probably its most important ramification Fall 2011 9 CSE341: Programming LanguagesWhat about unsoundness? Suppose a type system were unsound. What could the PL do? – Other than fix it with an updated language definition • Insert dynamic checks as needed to prevent X from happening • Allow X or anything else to happen, including deleting your files, emailing your credit card number, or setting the computer on fire PLs where the latter is allowed/expected are called weakly typed as opposed to strongly typed – We’re looking at you C and C++ Fall 2011 10 CSE341: Programming LanguagesWhy weak typing Why define a language where there exist programs that, by definition, must pass static checking but then when run can set the computer on fire? – Dynamic checking is optional and in practice not done – Why might anything happen? (See CSE351/333/451/484) • Ease of language implementation: Checks left to the programmer • Performance: Dynamic checks take time • Lower level: Compiler does not insert information like array sizes, so it cannot do the checks Weak typing is a poor name: Really about doing neither static nor dynamic checks – A big problem is array bounds, which most PLs check dynamically Fall 2011 11 CSE341: Programming LanguagesWhat weak typing has caused • Old now-much-rarer saying: “strong types for weak minds” – Idea was humans will always be smarter than a type system (cf. undecidability), so need to let them say “trust me” • Reality: humans are really bad at avoiding bugs – We need all the help we can get! – And type systems have gotten much more expressive (less incomplete) • 1 bug in a 30-million line OS written in C can make the whole OS vulnerable – An important bug like this was probably announced this week (because there is one almost every week) Fall 2011 12 CSE341: Programming LanguagesExample: Racket • Racket is not weakly typed – It just checks most things dynamically* – Dynamic checking is the definition – if the implementation can analyze the code to ensure some checks aren’t needed, then
View Full Document
Unlocking...