Re: cheerful static typing (was: Any and Every... (was: Eval))

[Matthias Felleisen <address@hidden>]

> We have had a "type system" like that in CL for years. 

"we" ~= "the world" and "like that" ~= "like Curl's". 

Please show me for a small essential core model of Curl
what typing means. The more I see about Curl's type system
the more I am confused. Let me point to two examples 
that most people on the list should know and understand. 

When the Java type checker performs its task, we know exactly what the
 underlying type language is (the specified interface and class hierarchy,
 including the imported Java libs, plus the basic types specified in the
 Java report. When it reports an error, it's pretty easy to see what I need
 to fix, because the typing rules are published and the explanations make
 sense. Finally, when the Java program runs, I am guaranteed that what the
 type checker proved holds during an evaluation. For example, the type
 checker proved that the machine will never attempt to add the bit
 representation of 10998 to the bit representation of "hello world". 
 That's called type safety. If you discover that your particular
 compiler/rt system violates this last part, you can go to the vendor and
 complain. 

Compare this to the C++ type checker: 
 1. Yes, the types are specified in the same way. 
 2. Yes, the typing rules are specified alright for plain classes. 
    If you get into parametric polymorphism, things don't look that easy 
    anymore when we get to type errors and fixing type errors. 
 3. When you run a C++ program, you have absolutely no guarantee that it
    doesn't add the bit representation of some integer to the bit
    representation of some string. That's called "lack of type safety". 
    
When you add a type system to a language, you should investigate these
three aspects. That's what research on type systems over the past 25 years
points to and when we invent new languages we should  understand
that. Otherwise our interpreters and compilers look like those that
undergraduates write as Simon Cozen argued during LL1. 

-- Matthias