Path: utzoo!utgpu!news-server.csri.toronto.edu!clyde.concordia.ca!uunet!mailrus!ncar!noao!arizona!gudeman
From: gudeman@cs.arizona.edu (David Gudeman)
Newsgroups: comp.lang.functional
Subject: Re: Why type checking is done at compile time
Message-ID: <24152@megaron.cs.arizona.edu>
Date: 11 Aug 90 21:59:48 GMT
Organization: U of Arizona CS Dept, Tucson
Lines: 38

In article  <162@skye.cs.ed.ac.uk> db@cs.ed.ac.uk (Dave Berry) writes:
>In article <23896@megaron.cs.arizona.edu> gudeman@cs.arizona.edu (David Gudeman) writes:
>>However, type systems are used in mathematics where neither [verification nor
>>efficiency] applies, so it seems that if there is a _true_ purpose for types,
>>it is the purpose used by mathematicians.
>
>Why should mathematics be any more "true" than computer science?

I didn't say mathematics is more true than C.S.  I think the reasoning
was clear in the original article, but here it is in expanded form:

(a) the three most common uses for type systems are
    (1) verification,
    (2) efficiency and
    (3) organization.

(b) Purposes (1) and (2) are used in a small minority of applications
of types systems (a few programming languages), while (3) is used in
almost all applications of types systems.  (I know of only one
exception)

(c) type systems were invented for purpose (3).

(d) even in the application where (1) and/or (2) are important (that
is, in paternalistic and/or low-level languages) the use evolved from
(3). 

(e) there are a lot of people who think (1) and/or (2) is an
inapropriate use for a type system, but almost no one denies the
importance of (3).

Given the primacy and universality of (3), it seems a little silly to
say that either (1) or (2) is _the_ purpose of type systems.
-- 
					David Gudeman
Department of Computer Science
The University of Arizona        gudeman@cs.arizona.edu
Tucson, AZ 85721                 noao!arizona!gudeman