Re: in defense of types

[Matthias Felleisen <address@hidden>]

Paul, 

At 29 May 2002 17:29:58 -0000, Paul Graham wrote:
> I admit that type declarations will help turn up bugs that 
> might not have been found till later, if at all.
> 
> However, type declarations are only one of many assertions
> you might choose to make in the source of a program to
> catch bugs.  Why not let it be up to the programmer to
> decide which such assertions to make, and when?  What's
> special about variables' types that makes it a good idea to
> make assertions about them mandatory, at compile time?

It turns out that the reason is very simple. A syntax is an algebra. 
For literal constants (flat and function space) you know the types. 
For variables, you don't know them. So you declare them. 
For all other forms of syntax, you take a constructor and build
a term. So, their type can be synthesized from the pieces. No need
to declare them. 

;; --- 

Otherwise I agree with you that types are just one form of assertion
and that we should pay attention to more general forms of assertions. 

Robby Findler and I have a paper at ICFP that talks about general 
contracts for languages with higher-order functions, and yes, I 
believe that this kind of research/language extension is necessary 
to discover useful static classes of assertions. (Hint to Michael: 
that's an "academic" criticism of type research.)

-- Matthias

P.S. Paul is correct that the >>>other<<< tradition of types is just 
about declaring how many bits you allocate. C makes no secret of that. 
But that is TWO different traditions.