Untyped Scheme should be built on Typed Scheme? WAS: Re:[plt-scheme] macro question

On Mon, Dec 22, 2008 at 06:29:30PM +0100, Jos Koot wrote:
> In a truly functional language, there are procedures (or functions) that 
> cannot even be proven to halt, let alone to halt with what kind of value. 
> Although rather expensive in terms of processor cycles, PLT's contract 
> system provides an acceptible compromise  (at least in theory). I guess 
> that a typed scheme (whether being the root or the target of an untyped 
> scheme does not concern me) I think a typed scheme should be implemented 
> such as to admit that it cannot in all cases infer the types of the values 
> produced by functions/procedures. I am not an expert in this area, but I 
> guess that building a fully safe typed functional language is like 
> bypassing the halting problem.
> Jos 

Yes, you are part right about the unsolvability issues.  It's easy to 
make a fully safe functional language.  What's hard is to make one that 
allows you to write all the programs you want to write.

You need to build in ways to escape the type system when necessary.

The way to do this neatly is to include some unsafe operations 
and types.  And some safe ways to generalize over safe types.

An unchecked type assertion is one way to include an unsafe type.  The 
implementation doesn't check it, and just hopes the prpgrammer is right.
This kind of thing is typically used in foreign-language interfaces.

A type for values whose details are not known at compile time, but 
will be sufficiently self-identifying at run time (like just about 
anything PLT Scheme currently provides) handles a lot of cases quite 
safely.  You can use type test predicates to inquire as to the actual 
values at run time, and use the (static) presence of those type tests to 
statically infer the types of those values through particular areas of 
the code.  THis is safe.

There should be an easy way to administratively prohinbit the 
use of unsafe things when that is desired.  Or, conversely, a clearly 
visible way to permit the use of unsafe things when needed (perhaps in 
a module header, or a #lang declaration or something).  This is to make 
it easy to find the places unsafe code exists.

Statically checking for termination cannot be done without restricting 
the class of functions that can be expressed in the language.  You can't 
even express all total, computable functions in a langauge that 
statically check for termination.  That is the import of the 
unsolvability results.

It is worth trying as a research project.  Certainly there are 
languages for restricted application domains where termination is easily 
achievable (trigger systems for warcraft, for example) but I don't 
think such restrictive systems are ready for day-to-day 
gerneral-purpose application coding yet.
 
Complete formal verification is still a hard problem.

But, as I said, the limited verification one can get with a static type 
system can deliver a lot at low cost.

-- hendrik