Relay-Version: version B 2.10 5/3/83; site utzoo.UUCP
Posting-Version: version B 2.10.1 6/24/83; site csd1.UUCP
Path: utzoo!linus!decvax!harpo!floyd!cmcl2!csd1!condict
From: condict@csd1.UUCP (Michael Condict)
Newsgroups: net.lang
Subject: Re: Strong Typing and Ignorance
Message-ID: <137@csd1.UUCP>
Date: Tue, 6-Dec-83 13:12:50 EST
Article-I.D.: csd1.137
Posted: Tue Dec  6 13:12:50 1983
Date-Received: Fri, 9-Dec-83 02:30:58 EST
References: <2892@utcsrgv.UUCP>
Organization: New York University
Lines: 54

I agree with Don's comment about the vagueness of the phrase "strong typing".
Consequently, when I want to distinguish between the kind of typing done in
LISP and that found in Pascal, I call the former "static typing" and the
latter "dynamic typing".  These phrases can be precisely defined, although
most languages will fall somewhere between the two extremes.  Here are my
definitions:

static typing - the language has a set of type expressions one of which is
required to be associated with each variable at the point of its declaration.
The type expression specifies the set of values (not bit patterns, but values
in an abstract mathematical world) that the declared variable may take on.
Different type expressions may denote the same set of values, but the question
of equality between types is decidable (computable).
Furthermore, a program is invalid if it contains a comparison between
two variables of unequal type or if it contains an assignment (explicit or
implicit) of an expression of type tau to a variable of type sigma and tau is
not a subset of sigma.

dynamic typing - a language is dynamically typed if variables are not associ-
ated with a type expression when declared, and any variable may be assigned
any value.

The purpose of the restrictions on types in the definition of static typing
is so that it is possible to ensure at compile time that no variable ever
takes on, or is compared to, a value that is outside of its declared type.
Of course, most staticly typed languages allow some sort of type coersion, at
least between integers and floating point.  Also, Pascal allows a value of
type integer to be assigned to a variable of type m..n, which violates the
subset rule given above -- this is exactly why Pascal needs run-time type
checking at the point of such assignments.

I find these definitions to be quite useful in categorizing languages and
discussing the benefits of various typing strategies.  I hope others agree
and that they will lend some precision to this discussion.

One more point.  Many people want to distinguish between languages that they
view as being "weakly typed" (by which they usually include LISP) and those
that are "untyped".  I always find it impossible to discover exactly what they
mean by untyped.  For any programming language I know, including the formal
untyped lambda-calculus, there are many possible mathematical domains that
can equally well be viewed as the collection of objects which are computable
within the programming language.  Furthermore, it is always possible to
partition this domain into subsets and to call each subset a different type.
Apparently, when one says a language is untyped, one is saying that no such
partition is reasonable.  This may be, but I do not know of any such cases.
Even in the lambda-calculus, one constructs certain expressions that are to
denote integer constants and others that are to denote arithmetic operations
on these integers, and thereby sets up a type system -- expressions that
denote integers are of a different type from expressions that do.  The lesson
is just that the question of whether or not a language has types, and what
those types are, depends on the intended usage of the language.

M. Condict    ...cmcl2!csd1!condict
New York Univ.