Thanks for commenting!

> 1) expressing the type signatures of library procedures succinctly to get precise error messages and to avoid convoluted manually written code to check that the arguments are of the correct type and shape

Unclear error messages are one of the pain points of Scheme. Research on
improving them isn't glamorous, and I don't know if it's possible to get
grant money for it, but it would be a big help in practice.

> 2) optimized compilation by specialization of the code to the types that are used by the program

Yes. And type tagging can be avoided in many cases. This is one of ML's
advantages, and I bet this is important when people (once again) start
writing web browser scale software in Lisp.

A web browser written in Lisp could have a layout engine using static
types and a JavaScript implementation using dynamic types.

The ML family should be folded into the Lisp family, anyway. We have
more commonalities than differences. I hope a really good structural
editor can eventually convince them to drop the complicated syntax and
adopt S-expressions, which would also give them our macros.

> So the first parameter must be a vector, and the second parameter must be an exact integer in the range 0 to the length of the vector.

AFAIK this is usually called dependent typing (the type of the integer
depends on the vector). A full dependent type system seems to get quite
complicated; in most languages, the length is not part of the type.

> If some typing system is designed for Scheme, my wish is that it will be powerful enough to express easily the type signatures of all the predefined R7RS Scheme procedures, and most of the SRFIs.  That way it can be included in the RnRS itself and be used to automatically generate dynamic type checks and good error messages with low programmer effort.

There's a fundamental split between "gradual typing" and systems that
enforce "well-typed" programs from the ground up. Hence there probably
can't be only one type system for Scheme. We should try making at least
one of each type of system, and find out how much surface syntax they
can share. Maybe the common parts could go into RnRS.