🚀 go-pugleaf

sabry@newsrice.edu (Amr Sabry) writes:

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

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

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

>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')

>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")