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

On Mon, Dec 22, 2008 at 09:29:17AM -0500, Matthias Felleisen wrote:
> 
> My original response was meant to express "historical development" in  
> a concise manner:
> 
> 1. Scheme was started in 1974 (someone correct me if I am off by a year)
> 
> 2. Since then, dozens of implementations have revised, extended,  
> changed the nature of the language. Thousands of programmers have  
> written useful code, including in PLT Scheme.
> 
> 3. So how in the world could Sam and I think of building Scheme on  
> top of Typed Scheme? The idea of Typed Scheme is quite simple:
> 
>  * there is useful code out there
>  * maintaining with 'types' is easier than without
>  * we should provide a smooth path from where we are (Scheme as given)
>    to where people may want to be (Scheme with a sound type system)
>    without imposing any cost on those who don't wish to come along
> 
> This is indeed how research should always work. Researchers discover  
> paradise and keep making it more perfect than it always is (Haskell,  
> ML). They don't care how ordinary people can get from hell to heaven.  
> We (PLT) have decided to build an exemplary bridge on which others  
> can follow or which others can mimic and build in different ways.
> 
> In general, if you think about how computing evolved this is just a  
> small universe that completely mirrors the large evolution. The world  
> was untyped. Decades later, people discovered unsound compiler  
> pragmas (C), naive type systems (Pascal, Algol) and then went on to  
> fancy stuff, including inference (PAL, ML). Two decades later they  
> finally realized how fancy types can be interpreted as compiler  
> pragmas but to this day, we don't have a completely typed hierarchy.  
> Sooner or later you descend from heaven to hell (Led Zeppelin has it  
> backwards) and at that point hell breaks loose. You move from simple  
> type theorems to full-fledged theorem proving, you yell abracadabra  
> and nothing helps. Why would we want to do all this? We haven't even  
> gotten the bridge complete or right yet?

That's right.  And until we have a practical way to formalize 
everything, we won't.  But there's no shame in having a language that 
can handle 99.9% of programming in a typed manner, and having a few 
unsafe loopholes for the rest.  And an untyped language can perfectly 
well be built on top of that, should anyone desire it.

The efficiency and reliability one can get from static typing will be 
there.  The alleged convenience (and its cost) will be there if anyone 
needs it, too.  But building a typed system on top of an untyped system 
means one pays the cost of the untyped system whether one needs it or 
not.

-- hendrik