morrison@thucydides.cs.uiuc.edu (08/03/90)
Hello, The question has been raised on why type checking is always done at compile time (even conceptually). I believe this question deserves a simple answer (and it is NOT because of efficiency). A type system is basically a very simple and specialized type of program verifyer. If the type system is 'type-safe' (a VERY desirable property of a type system) and a program passes the type checker, then the programmer is GUARENTEED that there will be no type conflicts at run time. Run time type checking does NOT do this. It simply allows the programmer to do something 'exceptional' when such a 'error' occurs. Run as many test cases on the code as you like, you will never get the guarentee of type safety that the compile time type system gives you. Thus a type system is simply the first modest step in program verification (that is determining run time behavior by analysing the program text). Vance Morrison Univ of Il.
gudeman@cs.arizona.edu (David Gudeman) (08/06/90)
In article <1990Aug3.144312.3157@ux1.cso.uiuc.edu> morrison@thucydides.cs.uiuc.edu writes: > >Hello, > >The question has been raised on why type checking is always >done at compile time (even conceptually). I believe this >question deserves a simple answer (and it is NOT because of >efficiency). > >A type system is basically a very simple and specialized >type of program verifyer. This is a common misconception among people from the Pascal/Ada world. It is true that a type system _can_ be used as a program verifier. And this observation is arguably one of the benefits that came out of early research in that programming language tradition. But this is not the only use of types. It is also the case that a compile time system allows for more efficient programs, and this was the original motivation for them. (Although, coming from assembly language, the first langauge designers may never have considered an alternative). However, type systems are used in mathematics where neither motivation applies, so it seems that if there is a _true_ purpose for types, it is the purpose used by mathematicians. The purpose of types is simply to group values with similar characteristics so that their behavior may be easily described, and so that signatures may be given for operations. These motivations also clearly apply to programming. >Thus a type system is simply the first modest step in program >verification (that is determining run time behavior by analysing >the program text). Of course, this is only useful if your program happens to fall into that class of programs that has a strict enough type structure that it is useful to to compile-time analysis. For many programs this is not true. -- David Gudeman Department of Computer Science The University of Arizona gudeman@cs.arizona.edu Tucson, AZ 85721 noao!arizona!gudeman
db@cs.ed.ac.uk (Dave Berry) (08/11/90)
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? -- Dave Berry, LFCS, Edinburgh Uni. db%lfcs.ed.ac.uk@nsfnet-relay.ac.uk Snuffsaidbutgorblimeyguvstonemeifhedidn'tthrowawobblerchachachachachacha chachachachachayou'regoinghomeinacosmicambience.
gudeman@cs.arizona.edu (David Gudeman) (08/12/90)
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
morrison@thucydides.cs.uiuc.edu (Vance Morrison) (08/13/90)
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