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

[address@hidden (Gregory T. Sullivan)]

The way I understood Howard's description of the Curl type
safety-related compiler directives was as a reasonable approach to the
inherent restrictions imposed by static type checking.

A quick restatement of a simple fact of type checking may be in order:

  A decidable type checking system, applied to a Turing-complete
  programming language, must conservatively reject some programs that
  will run without any runtime type-related errors.

Here's a trivial program that is type-correct but not provably so in
most type systems (in pseudo-code, with def'n of prime elided): 

  List l = {1, "hello", "world", 4, "goodbye", 6, "sweet", 8};
  for (int i = 0 to (length(l) - 1)) {
    if (prime?(i + 1)) {
       String s = (String) l[i];  // provably type-safe?
       println "String length is ", strlen(s);
    }
  }

or, in Scheme (w/o I/O): 

  (do ((l '(1 "hello" "world" 4 "goodbye" 6 "sweet" 8) (cdr l))
       (i 0 (+ i 1)))
      ((null? l) #t)
    (if (prime? (+ 1 i))
	(string-length (car l))))

Even the allegedly omniscient <wink> PLT Scheme flags the use of
string-length as potentially unsafe, even though it is clearly safe.

As I understand it, Curl's compiler directives allow you to state
whether you want to go ahead and run the above program or
conservatively reject it.

Put another way, all programs, for given a static analysis, fall into
one of three camps:

  (1) Statically safe - proven to be free of runtime errors.
  (2) Statically unsafe - proven to encounter an error at runtime, 
      for at least some legal inputs.
  (3) Not sure.

It is the 3rd class of programs that the programmer (or user) may want
to have some say in whether they run.

P.S. Standard partial evaluation techniques would allow you to
     prove the correctness of the above program, as the loop relies
     only on static data.

P.P.S.  Why to the two words "surge" and "curl" always make me think
      of "hurl"?

-- 
Greg      gregs@ai.mit.edu (617)253-5807
Sullivan  http://www.ai.mit.edu/~gregs/