Path: utzoo!attcan!uunet!tut.cis.ohio-state.edu!purdue!iuvax!ux1.cso.uiuc.edu!thucydides.cs.uiuc.edu!morrison
From: morrison@thucydides.cs.uiuc.edu (Vance Morrison)
Newsgroups: comp.lang.functional
Subject: Re: Why type checking is done at compile time
Message-ID: <1990Aug13.142021.26786@ux1.cso.uiuc.edu>
Date: 13 Aug 90 14:20:21 GMT
References: <24152@megaron.cs.arizona.edu>
Sender: usenet@ux1.cso.uiuc.edu (News)
Reply-To: morrison@thucydides.cs.uiuc.edu.UUCP (Vance Morrison)
Organization: University of Illinois, Urbana-Champaign
Lines: 99

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