> For #2 it is important to widen the notion of a type.  A type is theoretically a set of possible values.  This means that a range of values, like 0..9, and even a singleton, like 42, are types.  With this point of view on types, type analysis subsumes constant folding so that the type of (* x y) is the singleton type 42 when x has the singleton type 6 and y has the singleton type 7.  Moreover, if x and y are known to have type 0..9 then the overflow check on (* x y) can be eliminated because the result is of type 0..81, something that is important for performance.

> It would be more correct to say that the length of a vector is part of its type, but most languages’ static type systems are not powerful enough to express that type (so that in reality any “type error” on the index must be detected at run time).

Yes, you could put all static invariants into the type system. As far as
I can tell this is the main idea behind dependent types.

It's less clear what to do about things like a resizable vector. In
Smalltalk and CLOS you can even change the class of an object at
runtime. Common Lisp has a (satisfies p) type where p is a predicate
function, so you can do runtime checks. That aspect is more expressive
than what can be done in a static type system.

> It would be more correct to say that the length of a vector is part of its type, but most languages’ static type systems are not powerful enough to express that type (so that in reality any “type error” on the index must be detected at run time).

The cognoscenti make a distinction between "types" and "classes" for
these kinds of debates. I can't tell whether it's a legitimate point or
a misdirection to conceal the downsides of their favorite type systems.

> A statically typed Scheme will probably impose lots of constraints on what can be expressed, to the point of hampering the typical Scheme programming style.  Take lists for example.  Some say that lists are the “universal data structure” because all kinds of information can be represented in them:
>
> ;; lists of primes… should be fairly easy to statically type (but is it a list of integers, or a list of numbers, or a list of positive exact integers?):
> '(2 3 5 7 11 13)
>
> ;; poker hand… not so easy to statically type (mixes symbols and integers):
> '((spades king) (clubs 7) (hearts ace) (hearts 7) (clubs queen))

A ML or Haskell coder would replace the inner lists with tuples (or use
records, which are essentially named tuples). We don't have tuples in
Scheme and Lisp since we don't really need them. A tuple is like
first-class multiple values; SRFI 195 (Multiple-value boxes) comes close.

Python is a dynamic language which has an explicit tuple type but it's
hard to demonstrate the importance of the type to dynamic programmers.
It looks a bit out of place. "Why does Python have two list types, one
that is a normal list and one that is weirdly inconvenient?"

> ;; an s-expression to pass to eval:
> '(if (< x 0) (abs x) (string-length "hello!"))
>
> I could go on and on with other examples of this idiom we take for granted in Lisp/Scheme programming (representing complex data with lists).

The major failing of static types is that everything must be known in
advance. You'd need to enumerate every possible kind of Scheme datum in
a union type at compile time.

This is alleviated by bolting on an extra layer to the type system
(typeclasses, modules, traits, interfaces, etc.) at the cost of
increased complexity and slower compilation.

> Of course you could design a Scheme subset where these things would no longer be allowed, but I think it would be so crippling that it would be of little use for practical use in Scheme code.

> Could you explain how this issue could be addressed?

Static typing is more of a burden than a help without type inference and
correctness and exhaustiveness checking. If you make the type system
more permissive and expressive, it can do less of all these good things.

No one seems to have resolved this fundamental tension satisfactorily.
Racket, Common Lisp, and Python opted to use "gradual typing".
Everything is dynamic by default and you can add type hints, but
"well-typed" code is not enforced.

In Scheme we have a similar tension in macros. `define-macro` lets you
use everything in normal Scheme but does not help with safety. Hygienic
macros offer varying levels of help, but the easier it is to be safe,
the more the macro language deviates from normal Scheme. Syntax-rules is
safest, but it's a completely different language. Type systems are
similar: Hindley-Milner without any add-ons is rock solid, fast, and
simple, but it's like coding in a straitjacket. Like syntax-rules, you
have to unlearn old habits and it can't express everything.

I expect that the most satisfying solution is to have a separate dynamic
and static language (the latter H-M based) with similar surface syntax
and good interop. Many Lispers will probably think gradual typing is the
only acceptable option. We should try both.