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

[Guillaume Marceau <address@hidden>]

On Thu, 10 Jan 2002, Christopher Barber wrote:

>
> {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}
>       }
>    }
>  }



I understand goodness of type system come from their redundancy. Not
unlike CRC-based transfer-error detection, type systems detect 'thinking
errors'.

Within a typed language, the program is coded in two interweaving
languages : The core language, it is very precise and as thus, heavy of
details on the programmer's mind. The type language, it is more sketchy,
but also more intuitive. The compiler act as a peer-reviewer, detecting
inconsistencies between the two purposed expressions of the same program.


In that sense, the runtime guarantees given by the type system, although
often wildly useful, are not essential.

Maybe we could reach better performance/correctness trade-offs by
thinking of type systems less as automated/interactive proof tools, and
more as redundant programming.

As I ex-robot programmer, whose software involve complex algorithms
running in real-time, I found Java too slow and C++ too jello.



I like the Curl line "{with-compiler-directives stringent? = true do ... }".

It stands as a short sentence for both programmer-compiler communication
and programmer-programmer communication. In the first case, it means "I
claim this section is deterministic. Can you check up on me?", In the
second, "Hello fellow programmer! Behold that this is good code! For it
has been mechanically checked for deterministic behavior!"

All you proponent of literate programming in the audience will recognize
themselves.


In that vein, you could have more syntaxes of the form :

       (<checked property>, ...) { <code> }

as in

       (deterministic, exception-less) { i = i + 1 }

or, thinking of Java :

  (may or may not throw ClassCastException,  // compiler can't prove
   throws InvalidArgumentException,
   never throws IndexOutOfBoundsException) // proved by partialy evaluation?
         { <code> }




(nota: IHBILM, I have a bac, I am looking for a master. ask for references)


-- 

A la mer nous avons trempé crûment quelques gentilles allemandes stupidement bouleversées.

 - an oddly monotonic verse by Bens.

 Guillaume