Path: utzoo!attcan!uunet!cs.utexas.edu!uwm.edu!ux1.cso.uiuc.edu!thucydides.cs.uiuc.edu!morrison
From: morrison@thucydides.cs.uiuc.edu
Newsgroups: comp.lang.functional
Subject: Why type checking is done at compile time
Message-ID: <1990Aug3.144312.3157@ux1.cso.uiuc.edu>
Date: 3 Aug 90 14:43:12 GMT
Sender: usenet@ux1.cso.uiuc.edu (News)
Reply-To: morrison@thucydides.cs.uiuc.edu ()
Organization: University of Illinois, Urbana-Champaign
Lines: 26


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.