Static typing and expressiveness 
Author Message
 Static typing and expressiveness

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



Thu, 23 Sep 1993 18:40:35 GMT  
 Static typing and expressiveness

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

Quote:
> [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.

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

Quote:
>>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



Thu, 23 Sep 1993 18:35:36 GMT  
 Static typing and expressiveness


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



Fri, 24 Sep 1993 23:09:35 GMT  
 
 [ 3 post ] 

 Relevant Pages 

1. expressiveness and strong type system?

2. Types, types: static vs. dynamic -- classification

3. Types, types: static vs. dynamic --

4. Types, types: static vs. dynamic -- classification

5. x/0 as a type error [Extremely static typing]

6. opacity and static typing (Re: Type checkers for scheme)

7. Types, types: static vs. dynamic -- classification

8. Provide an option: static typing + type inference ?

9. Flying With Python (Strong versus Weak Typing) [actually, Static vs Dynamic typing]

10. Static vs Dynamic Typing: Effects on Productivity?

11. Static typing is needed when..

 

 
Powered by phpBB® Forum Software