Re: Why type checking is done at compile time

Thread View: comp.lang.functional

2 messages

[T] Back to Threads [V] Tree View [G] Group Articles

2 total messages Started by David Gudeman Sat, 11 Aug 1990 21:59

#434

Author: David Gudeman
Date: Sat, 11 Aug 1990 21:59

38 lines
1956 bytes

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

Re: Why type checking is done at compile time

#435

Author: Vance Morrison
Date: Mon, 13 Aug 1990 14:20

99 lines
4628 bytes

In article <24152@megaron.cs.arizona.edu> gudeman@cs.arizona.edu (David Gudeman) writes:

>(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)

I think we are splitting hairs here.  I agree with you completely
that organization is the primary use of types.   This is why even
in mathematics type are a very useful concept.  However, what makes
type systems a more organizational tool than say naming schemes,
or indentation, etc, is that there are very specific syntatic 
(compile-time, decidable) rules that can be checked.  Thus the 
programmer can be SURE that the organization the typeing struture
places on his program is consistant.  This is what makes type
systmes powerful.

Note that if typing was done at run time (or the type system was
so complex that checking consistancy is undecidable), much of the
value of a typeing system is lost.  Sure, I can still use types to
orgainize my code, but I will never know for sure that it is correct 
(type consistant).

>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.
>-- 

I did not mean to imply that verification was the only purpose of
type systems.  Notice that I was merely trying to answer the question
of why it is that checking type consistancey is usually thought of as 
'compiie-time' operation.  Notice that the orgainizational aspects
of typeing does not require typeing to be compile-time.  However,
verification does by its very nature require this.

Vance
Univ of lllinois, Urbana

Newsgroups: comp.lang.functional
Subject: Re: Why type checking is done at compile time
Summary: 
Expires: 
References: <24152@megaron.cs.arizona.edu>
Sender: 
Reply-To: morrison@thucydides.cs.uiuc.edu.UUCP (Vance Morrison)
Followup-To: 
Distribution: 
Organization: University of Illinois, Urbana-Champaign
Keywords: 

In article <24152@megaron.cs.arizona.edu> gudeman@cs.arizona.edu (David Gudeman) writes:

>(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)

I think we are splitting hairs here.  I agree with you completely
that organization is the primary use of types.   This is why even
in mathematics type are a very useful concept.  However, what makes
type systems a more organizational tool than say naming schemes,
or indentation, etc, is that there are very specific syntatic 
(compile-time, decidable) rules that can be checked.  Thus the 
programmer can be SURE that the organization the typeing struture
places on his program is consistant.  This is what makes type
systmes powerful.

Note that if typing was done at run time (or the type system was
so complex that checking consistancy is undecidable), much of the
value of a typeing system is lost.  Sure, I can still use types to
orgainize my code, but I will never know for sure that it is correct 
(type consistant).

>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.
>-- 

I did not mean to imply that verification was the only purpose of
type systems.  Notice that I was merely trying to answer the question
of why it is that checking type consistancey is usually thought of as 
'compiie-time' operation.  Notice that the orgainizational aspects
of typeing does not require typeing to be compile-time.  However,
verification does by its very nature require this.

Vance
Univ of lllinois, Urbana

Thread Navigation

This is a paginated view of messages in the thread with full content displayed inline.

Messages are displayed in chronological order, with the original post highlighted in green.

Use pagination controls to navigate through all messages in large threads.

Back to All Threads