Path: utzoo!utgpu!news-server.csri.toronto.edu!rpi!zaphod.mps.ohio-state.edu!swrinde!cs.utexas.edu!rice!sabry
From: sabry@newsrice.edu (Amr Sabry)
Newsgroups: comp.lang.misc
Subject: Static typing and expressiveness
Message-ID: <1991Mar29.195840.14735@rice.edu>
Date: 29 Mar 91 19:58:40 GMT
References: <1211@optima.cs.arizona.edu> <3073:Mar2820:38:5191@kramden.acf.nyu.edu>
Sender: news@rice.edu (News)
Reply-To: sabry@newsrice.edu (Amr Sabry)
Organization: Rice University
Lines: 27
Originator: sabry@hedera.rice.edu


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.