Path: utzoo!utgpu!news-server.csri.toronto.edu!rpi!zaphod.mps.ohio-state.edu!sdd.hp.com!decwrl!deccrl!news.crl.dec.com!shlump.nac.dec.com!decuac!haven!ni.umd.edu!uc780.umd.edu!cs450a03
From: cs450a03@uc780.umd.edu
Newsgroups: comp.lang.misc
Subject: RE: Static typing and expressiveness
Message-ID: <7APR91.10353617@uc780.umd.edu>
Date: 7 Apr 91 10:35:36 GMT
References: <Sun_Apr__7_22:35:04_1991@cosc.canterbury.ac.nz>
Sender: usenet@ni.umd.edu (USENET News System)
Organization: The University of Maryland University College
Lines: 88
Nntp-Posting-Host: uc780.umd.edu

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