🚀 go-pugleaf

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