Path: utzoo!utgpu!news-server.csri.toronto.edu!rpi!zaphod.mps.ohio-state.edu!wuarchive!uwm.edu!bionet!parc!boehm From: boehm@parc.xerox.com (Hans Boehm) Newsgroups: comp.lang.misc Subject: Re: Static typing and expressiveness Message-ID: Date: 30 Mar 91 00:18:51 GMT References: <1211@optima.cs.arizona.edu> <3073:Mar2820:38:5191@kramden.acf.nyu.edu> <1991Mar29.195840.14735@rice.edu> Sender: news@parc.xerox.com Organization: Xerox PARC Lines: 51 sabry@newsrice.edu (Amr Sabry) writes: >You lose "expressive" power in a statically typed language. >Consider the lambda calculus. In the usual (dynamically typed) >setting the language can express all computable functions and >hence equality of terms is undecidable. However, in the simply >typed frame, equality becomes decidable. The simple minded >type system rules out so many programs that you can longer >write non-terminating programs [1]. Moreover, no matter how >"smart" your type system is, it will still rule out some >perfectly good programs. >Theorem: No (decidable) static type system can only accept all the >"good" programs in a "reasonable" language. >Proof: Let E be a good expression in the language, consider the >program x = 1/E; the program gives a type error iff E=0 which >is undecidable. >The bottom line is a statically typed programming language prevents >you from writing some programs which are good programs (they >will not give any type errors when executed). Now whether >you care about such a loss is debatable but there IS a loss. >Amr >[1] H. Friedman 1975, Equality between functionals. Some interpretation of the "bottom line" is no doubt correct, but I have some trouble with this reasoning. The arguments about expressiveness of the typed lambda calculus assume a pure lambda calculus with no explicit recursion. They don't hold for anything I would consider a real programming language. It's easy to embed the untyped lambda calculus in some statically typed languages that allow recursive types. (I believe this is true for ML. It's definitely true for Russell.) The "theorem" seems reasonable, but the "proof" assumes that 1/0 is a type error rather than, say, a diverging computation that might be detectable at runtime. (I know of at least one mechanical calculator that implemented it that way, without the run-time check.) I view a type system (static or dynamic) as a mechanism for ensuring that abstractions are preserved and that no bits are misinterpreted as something other than what they represent. With this interpretation it's not clear that 1/0 is a type error either. It's certainly true that no static type system can accept only terminating programs, and all "good" terminating programs. But none claims to, either. Hans (boehm@xerox.com)