Quote:

>You lose "expressive" power in a statically typed language.

>Consider the lambda calculus. In the usual (dynamically typed)

^^^^^^^^^^^^^^^^^

Sorry - the usual (pure) lambda calculus is untyped. I quote from [2]:

"In the lambda calculus, everything is (or is meant to represent) a

function. Numbers, data structures and even bit strings can be

represented by appropriate functions. Yet there is only one type: the

type of functions from values to values, where all the values are them-

selves functions of the same type."

In other words if a closed lambda expression has type X then it also has

type X->X. The only solution is to assign the type \mu x . x -> x to all

lambda expressions (as in [4]). The result is that everything has the same

type and by a traditional abuse of terminology whenever a language has only

one type we say it is untyped (or type-free as in [1], p5).

Quote:

>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.

This is certainly true. A good example of this is subtraction. In the first

order (or simply-typed) lambda calculus it is possible to represent numbers

and some operations on them such as successor and addition but it is not

possible to represent subtraction (see [3]). You need to step upto the

second-order system to be able to do subtraction. Most people regard

subtraction as desirable (and hence "good").

Quote:

>Theorem: No (decidable) static type system can only accept all the

>"good" programs in a "reasonable" language.

There are two main things to point out here. Firstly most functional

languages that I know (which are sematically based on lambda calculi) have

some sort of mechanism for specifying recursive types (such as Constructors

in SML etc). Typed lambda calculi normally don't allow recursive types and

this is why they're not as powerful as the untyped lambda calculus.

Secondly you're confusing languages with their underlying model.

Functional languages, such as SML or Miranda, are based on the *untyped*

lambda calculus - that is their underlying model - but are themselves

statically typed. Machine language, for example, is untyped (everything is

a bit pattern) but HL languages can have any type discipline they like.

An example may help convince you. The following two functions are

written in Miranda which is a *statically* typed functional language

whose underlying model is the lambda calculus. They deal with the

well-known 3*n+1 problem:

reduce n = 3*n+1 ,if n mod 2 = 1

= n div 2 ,otherwise

is_it_wondrous n = True ,if n = 1

= is_it_wondrous (reduce n) ,otherwise

The function 'reduce' takes a number and, if it is odd, triples it and

adds one. If the number is even it halves it. The compiler happily

deduces the type num->num for 'reduce'. The function 'is_it_wondrous'

returns True if the given number eventually reduces to one. It has type

num->bool. Both these functions are monomorphic, i.e. simply-typed. Now

does 'is_it_wondrous' always terminate? There are any number of

Journals that would be interested in publishing a proof either way.

Quote:

>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.

Nope. Most languages I know fail to make a type distinction between whole

numbers and natural numbers. In Miranda, for example, you don't need to

declare types - the compiler deduces them for you (like in SML). So

long as it can deduce that E has type 'num' then 1/E will type-check ok.

(MIranda only has one numeric type - 'num')

Quote:

>The bottom line is a statically typed programming language prevents

>you from writing some programs which are good programs (they

Nope. Not true. Miranda and SML are both statically typed and its

possible to simulate TM's or the full pure untyped lambda-calculus in both

of them. You can't get more powerful than that.

References:

[1] "The lambda calculus - its syntax and semantics" , H.P. Barendregt

[2] "On understanding Types, Data abstraction, and Polymorphism",

L. Cardelli,P. Wegener, Computing Surveys 17,4, (1985), pp471-522

[3] "The expressiveness of simple and second-order type structures",

S. Fortune, D. Leivant,, M. O'donnell, Journal of the ACM 30,1,

(1983), pp151-185.

[4] "An ideal model for recursive polymorphic types", D. MacQueen,

G. Plotkin, R. Sethi, Information and Control 71, (1986), pp 95-130

--

-----------------------------------------------------------------------

"Merely corrobarative detail, intended to give artistic verisimilitude

to an otherwise bald and unconvincing narrative"

-- W.S. Gilbert ("The Mikado")