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

["Christopher Barber" <address@hidden>]

> 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);
>     }
>   }

> 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.

Yes.  Here it is in Curl, without type annotations:

  let l = {Array 1, "hello", "world", 4, "goodbye", 6, "sweet", 8}
  {for s key i in l do
     {if {prime? i + 1} then
        {output "String length is ", s.size}
     }
  }

This will compile and run just fine (assuming that you have actually defined
'prime?').

If you wrap this with:

   {with-compiler-directives stringent? = true do ...}

then you will be required to add a type annotation for 'l' and add an
explicit cast in order for this to compile:

  {with-compiler-directives stringent? = true do
     let l:Array = {Array 1, "hello", "world", 4, "goodbye", 6, "sweet", 8}
     {for s key i in l do
        {if {prime? i + 1} then
           {output "String length is ", (s asa String).size}
        }
     }
   }

Static typers should like this because it makes it clear where the potential
runtime type error could occur.

- Christopher