Scheme is a dynamically typed language and should stay that way.

Nevertheless, static types are irresistible in some of the application
areas that are of the greatest personal interest to me.

The most important one is code sharing. Useful software systems involve
a lot of unimaginative work implementing well known algorithms, formats,
and protocols. Language enthusiasts often act like there are good
reasons to have 100 slightly different variations of this stuff but I
don't buy any of those reasons. I want less variety and more re-use.

When thinking of code re-use, we should think first about execution
models. A dynamic language can support virtually the same execution
model as a static language. I think this should be exploited by writing
most of the unexciting code in the static language, then translating to
the dynamic one by throwing away the type restrictions. (Likewise code
can be written in a language with macros, and the expanded code
translated into a language without macros that has a similar execution
model.)

Observe that the converse does not work: translating a dynamic language
into a static one is a scruffy Artificial Intelligence problem. Any
formalism you could invent to solve it would itself be a type system.

The reason I didn't quit Scheme after a few months as I initially
expected is that it's still the best core for algorithmic programming.
You get the lambda calculus with an arbitrarily extensible syntax that
can be used to add types, constraints, and whatever else you need on the
side. For as long as we'll represent programs as trees and not as more
general graphs, this is where it's at.

So if we add types to Scheme, that gives a language which translates
easily enough into any language with a lambda calculus based execution
model and either dynamic types or compatible static types.

This ties into a big and evolving web I have in my mind about how to
organize the social and technical aspects of programming for maximum
productivity in the next decade or two. There's much more to be said on
that later. For now, I'd like to remark that no one has the moral
authority to step up and say "this is the kind of type system that
Statically Typed Scheme (TM) should have". A standardized, dynamically
typed language has dynamic types, and any static complement is just
someone's opinion.

That being said, it would be a tragedy if different groups of people go
off and over time make 3 or 5 different type systems for Scheme with no
possibility of code re-use between them.

I'd like to make an attempt to avoid that fate early by surveying the
kinds of type systems available, with a view to finding equivalences and
automatic conversions between them. We should find ways to express
algorithms and interfaces that solve practical problems in Scheme, such
that the same surface syntax can automatically be turned into the
dynamically type Scheme we have now as well as any nascent typed
flavors. Ideally the surface syntax will be something as similar as
possible to dynamic Scheme, which would make it painless to copy/paste
code between them. Type inference the gateway.

Personally I like my type systems the way I like my memory management:
invisible. To that end, I'll pursue simplicity with maximum inference.
If others are inspired to look into something heavier like effects or
dependent types, that's fine. We should find ways to interface our work.
There still is the https://github.com/pre-srfi/static-scheme repo which
I kind of bowed out of since the proposed system got too complex for me.
Maybe some of you will want to run with that and see where it goes.

But I didn't fully realize back when we started the repo that "Typed
Scheme" should intrinsically be a network of type systems with
translation pathways between them, sharing as much surface syntax and
nomenclature as possible. If memory serves, we started a kind of rivalry
about what kind of type system would "win", but there should be no winner.

The way to start the long trek toward types is bottom up: Find practical
problems, then say "here's how I would express this using my favorite
type system". Compare solutions. As the first order of business, we
should write types for the procedures in RnRS and the most popular SRFIs.

While these "Typed Schemes" will take a decade to mature into something
canonical, I think the problem is urgent because it may guide the
evolution of dynamic Scheme. My ideal is not the "gradual typing" found
in Common Lisp and Racket, but "twin typing" where there are separate
dynamic and static languages, and the surface syntax is as compatible as
possible to the point that you hardly have to care which one you're
using at any given time.

Comments are welcome, but above all, please help me write down type
signatures for the Scheme canon. There are bound to be many surprises,
both pleasant and vexing.