Path: utzoo!utgpu!news-server.csri.toronto.edu!rpi!zaphod.mps.ohio-state.edu!samsung!uunet!stanford.edu!snorkelwacker.mit.edu!ai-lab!life!tmb
From: tmb@ai.mit.edu (Thomas M. Breuel)
Newsgroups: comp.lang.misc
Subject: Re: definitions
Message-ID: <TMB.91Apr29182914@volterra.ai.mit.edu>
Date: 29 Apr 91 22:29:14 GMT
References: <2494@optima.cs.arizona.edu> <51984@nigel.ee.udel.edu>
	<333124@socrates.umd.edu> <11525@mentor.cc.purdue.edu>
	<TMB.91Apr29022852@volterra.ai.mit.edu>
	<ROCKWELL.91Apr29091355@socrates.socrates.umd.edu>
Sender: news@ai.mit.edu
Organization: MIT Artificial Intelligence Lab
Lines: 78
In-reply-to: rockwell@socrates.umd.edu's message of 29 Apr 91 14:13:55 GMT


   T[h]omas Breuel:
   >  Dynamically typed programs are also impossible to prove type-correct,
   >  and many trivial errors go unchecked.

   This is true when you are using a statically typed language (which
   does not provide support of dynamically typed programs).  This is not
   true in general, however.

Dynamic typing lets you write programs like the following:

  ;;; Scheme
  (define (fermat-conjecture-is-true?) ...)
  (define (f) (if (fermat-conjecture-is-true?) 9 #f))
  (define (g) (+ (f) 1))
  (g)

Now, you cannot determine statically whether this program is
type-correct (i.e., whether this program will never give you
a runtime type error).

A statically typed language will simply not allow you to
write such functions:

  (* SML *)
  fun f () = if fermat_conjecture_is_true_p() then 9 else false
  ---> type error

In order to express the same concept in a statically typed
language like SML, you have to use unions:

  (* SML *)
  datatype bool_or_int = BOOL of bool | INT of int;
  fun f () = if fermat_conjecture_is_true_p() then INT(9) else BOOL(false)
  ---> f: unit -> bool_or_int

In essence, you are introducing a little bit of dynamic typing into
the statically typed language.

   You can implement static typing in a dynamically typed language by
   introducing "functions" which do no processing but which have limited
   domains.  These functions are equivalent to type declarations.

You can write:

  ;;; Scheme
  (define (NUMBER-+ x y)
    (if (not (and (number? x) (number? y))) (error "number+")
        (+ x y)))

  (define (DOUBLE x) (NUMBER-+ 'a 'b))

However, this does not give you static typing, since the Scheme
compiler is not required to check statically whether all uses of
NUMBER-+ satisfy the type constraints. In fact, in most cases, it
cannot even determine the type correctness of your program statically
because of language semantics. For example, in the above example, the
compiler cannot flag a type error for the function DOUBLE because
NUMBER-+ could have been rebound by the time DOUBLE is called.

Static typing is added functionality in the compiler. If you want to,
you can use dynamic typing on top of a statically typed language, but
the converse is not true.

  In a well-written program, in a well-designed language, you should not
  _usually_ need such a function.  All primitive functions of the language
  should have such functionality built-in.

I disagree. It is very useful to be able to flag the type error in the
function DOUBLE shown above at compile time. DOUBLE may be called only
very rarely, so that it doesn't get detected on testing, but the
runtime type error might "make your airplane crash".

Trivial type errors like this occur even in well-written programs, and
cannot be caught by many well-designed dynamically typed languages
(like Scheme) at compile time.

						Thomas.