Path: utzoo!utgpu!news-server.csri.toronto.edu!rpi!zaphod.mps.ohio-state.edu!samsung!munnari.oz.au!comp.vuw.ac.nz!waikato.ac.nz!canterbury!cosc.canterbury.ac.nz!chisnall From: chisnall@cosc.canterbury.ac.nz (The Technicolour Throw-up) Newsgroups: comp.lang.misc Subject: Re: Static typing and expressiveness Message-ID: Date: 7 Apr 91 10:40:35 GMT Organization: Computer Science,University of Canterbury,New Zealand Lines: 104 Nntp-Posting-Host: cantua.canterbury.ac.nz 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")