CSE 341, Spring 2011, Lecture 17 SummaryStandard Disclaimer: These comments may prove useful, but certainly are not a complete summary of allthe important stuff we did in class. They may make little sense if you missed class, but hopefully will helpyou organize and process what you have learned.One of the biggest differences between Scheme and ML is that ML has a type system that rejects manyprograms “before they run” meaning they are not ML programs at all. (Ruby and Java have an analogousdifference.) The purpose of this lecture is to give some perspective on what it means to have a type system,how one can judge a particular type system, and in general some of the advantages and disadvantages ofhaving a type system.Let’s first discuss the difference between strong typing and weak typing. In a language with weak typing,there exist programs that the implementation must accept as legal (i.e., it must run them) but that then cando anything including produce arbitrary output, corrupt data, delete files, or set the computer on fire. Cand C++ are the most common examples – if you have a type-cast that is incorrect (the result of evalutingan expression is not the type you claim), you don’t get an exception like in Java. Instead, anything canhappen, including things that make no sense from the programmer’s perspective. A strongly typed languagedoes not have this property: A value of a certain type (e.g., int) always behaves as it should (e.g., as aninteger), which prevents such arbitrary behavior. In this sense, both ML and Scheme are strongly typed.Even though Scheme does not reject ill-typed programs until they run, it is still well-behaved enough neverto treat a string as a procedure.In the past, strong typing was dismissed with the slogan, “strong types for weak minds” which meantthat programmers should be smarter than any particular type system so languages should have uncheckedtype casts for programmers who know what they are doing. You hear this view less these days since arbitrarybehavior sounds pretty bad for a society that relies on software for nearly everything, and experience showsthat programmers often make mistakes. The “advantage” of unchecked type casts is that they are moreefficient at run-time (i.e., zero cost), just like the “advantage” of unchecked array-indexing is more efficient.Yet this sort of undefined behavior costs the world economy billions of dollars a year. For the rest of thelecture, we will consider only strong typing.The relevant difference between ML and Scheme is that ML is statically typed and Scheme is dynam-ically typed. To understand the difference, consider that in ML "hi" - "mom" is an error and in Scheme(- "hi" "mom") is an error, but these errors arise at different times. An ML “program” containing stringsubtraction is not a program at all — the type-checker rejects it statically, i.e., “at compile-time”, i.e., beforeexecution begins. A Scheme program containing string subtraction is a perfect fine program, but if dynam-ically, i.e., “at run-time”, the subtraction is actually performed, an error will occur since - checks that itsarguments are numbers. Similarly, car and cdr check that their arguments are pairs whereas ML’s hd andtl do not need to check — the type-checker guarantees it.An example like "hi" - "mom" clearly demonstrates an advantage of static typing — such an expressionis always wrong so it’s helpful to know that before the program starts running since it can’t possibly beuseful. However, static type systems are always approximate. They also reject programs that are usefuljust to be sure that they don’t allow bad programs. Before we discuss exactly why and some importantterminology about this issue, here is an example:(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! *)The ML code will not type-check because y has to have type string in one place and type int in another.However, the function f is fine if callers use it correctly. In particular, they must pass an int for y wheneverg x will produce #f and a string for y otherwise.In general, one big advantage of a static type system is that it catches certain bugs without testing,i.e., earlier in the software-development cycle. However, it’s impossible for a static type system to reject1exactly all the buggy programs and accept exactly all the correct programs, so any type system is just anapproximation. Here are some reasons why:• For an arbitrary program, it’s impossible (in the sense of undecidable as studied in CSE 311) to knowat compile-time what code will execute, what values variables will have, etc. So a type system willgive false positives if it thinks for example that an expression might evaluate to a string when in factit will always evaluate to an int.• Just because a program “type-checks” does not mean it is correct. Algorithm bugs can remain sincesurely a type system cannot “know” you meant to write - where you wrote +.This is not meant to dismiss the advantages of static typing, but simply to emphasize that type systems arealways an approximation of what you actually want to check for. Approximations can be extraordinarilyuseful, especially when they are fast, automatic, and sound (see below, roughly, “always erring on the sideof caution”).So far we have been very informal about a key question for any type system: What is it checking, i.e.,what does it intend to prevent for any program that type-checks? This depends on the language, and yousimply cannot talk about whether static typing is “good” or “bad” without being clear about what is beingchecked. For example, here are several errors one can have in an ML program:1. Apply a primitive (e.g., +) to arguments of the wrong values (e.g., functions)2. Violate a module signature (e.g., access a private function)3. Have a redundant pattern in a case-expression4. Apply hd to the empty list5. Retrieve the 10th element of an array that has only 5 elementsIt turns out that the ML type system prevents 1–3 (they will never happen in a well-typed program) butnot 4–5. This division of what is checked is “pretty normal” — it’s about what one typically expects froma type system these days — but a different language might have a different list. As a programmer, it’sessential to know what the type-checker prevents and what it does not. When I program in ML, I am
View Full Document
Unlocking...