Re: Strong Typing, Dynamic Languages, What to do?

[Matthias Felleisen <matthias@ccs.neu.edu>]

The problem is that CL types have little meaning (see CL TL2). Furthermore,
I would like a tool that helps programmers infer and confirm such type
conjectures.

Remember types play two roles in this context: 

 1. they are conjectures about the flow of values in your program. 
    If so, they should be confirmed. If the tool fails to confirm, 
    they must explain why your conjecture failed. 

    For example, when you write down (car x), you "conjecture" that x is a
    pair. Your static debugger should try to prove that this is true, and
    if not display a non-pair that may flow into the x and even better a
    flow path along which it flows. That's a witness. 

 2. they introduce abstraction barriers for functions, modules, objects,
    etc. A static debugger must take those new barriers into account as it
    checks your conjectures about code. 

    For example, if you declare a function type such as 

	 f : pair[X,Y] -> X

    then you are demanding that all potential uses (we don't know all uses)
    of f must only be applied to one argument and that this argument is
    always a pair. If your static debugger finds an application site where
    this doesn't work, then it must exhibit a path on which f flows into
    the function position and a path for a non-pair that flows into the
    argument position.

In both cases, the static inference must hold at run-time so that when
something does go wrong, you know that you don't have to check such things
and can focus on other problems. That's where C and C++'s type system
totally fail; and, from what I understand about CL, its type system fails,
too. 

-- Matthias