Untyped Scheme should be built on Typed Scheme? WAS: Re: [plt-scheme] macro question
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?
End of communication. -- Matthias