sabry@newsrice.edu (Amr Sabry) (03/30/91)
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.
boehm@parc.xerox.com (Hans Boehm) (03/30/91)
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)
cs450a03@uc780.umd.edu (04/07/91)
chisnall@cosc.canterbury.ac.nz (whoever) > >... 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. ahem. It is quite possible to construct a functional language from a set of first principles different from those of lambda calculii. I have worked with more than one. > [halting problem example] Ignorant question: are you saying that in lambda calculus there is no way to model "function domains" other than to have a non-terminating procedure? I mean, in that model, if I divide by zero, or try and find which is the least of two complex numbers, the model would specify a computation that would go on forever? I've heard things about the inapplicability of lambda calculus to computing models, but this (if true) is somewhat worse than anything else I've encountered. If your example was just of an ill-defined function, well... that's different. >> ... 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') hmm... "type error" and "type distinction" ... I believe the point here is that for division, which is an inverse of multiplication (which is not one-to-one) there is no good reason to use a different static-domain (machine representation for number) than is used for other arithmetic functions, but it is useful to have a different dynamic-domain (numbers which the division function will accept as valid arguments) than for other arithmetic functions. If that looks like an involved concept, well, in this context it is. Another problem with typing division is that while addition, subtraction and multiplication all work nicely in integer domains, division opens up either rational numbers (usually approximated by floating point numbers), or other ordered pairs (such as quotient/remainder). Since it is useful to apply other arithmetic to the results of division, you can view division as the operation which moves arithmetic from an "untyped" or single-typed discipline to a multi-typed discipline. Finally note for the general case of x divided by y, it is undecidable whether the resulting value is an integer value or not. One solution is to declare that the general case never results in an integer value. Another solution is to declare that any function which needs an integer value will coerce to integer any non-integer argument. Both of these solutions allow static typing for the results of general division. On the other hand, if you don't mind a run-time check, neither of these "solutions" are necessary. This is especially useful if you weren't working with the general case, but with some limited domain where x divided by y always yields an integer. Ummm.... at the machine language level, you're probably going to have "quotient, remainder" semantics, or maybe "divide and branch" semantics. The statically typed high-level language implementation tends to throw away some of this information in the interests of speed, and the dynamic typing implementation tends to hang onto this kind information, at the expense of speed. These are short-term effects. >>The bottom line is a statically typed programming language prevents >>you from writing some programs which are good programs > >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. The issue, I believe, is not computability, but complexity (machine level, and project level). Raul Rockwell
chisnall@cosc.canterbury.ac.nz (The Technicolour Throw-up) (04/07/91)
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")
sabry@rice.edu (Amr Sabry) (04/08/91)
In article <Sun_Apr__7_22:35:04_1991@cosc.canterbury.ac.nz>, chisnall@cosc.canterbury.ac.nz (The Technicolour Throw-up) writes: |> |> >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. I think you are missing my point. Consider SML and Scheme. The first is statically typed and the second is dynamically typed and both can simulate a Turing Machine. However, the following programs will run in Scheme with no (type) errors, but will fail to type in SML. (cons 10 #t) (lambda (f) (cons (f 10) (f #t)))