> (And in fact, I am not very much in favor of
> a static type system because only with dependent typing you can
> express all types.)

What is "all types"? For example, Common Lisp has a `satisfies` type
(http://www.lispworks.com/documentation/HyperSpec/Body/t_satisf.htm)
that checks whether the value satisfies a predicate. The predicate can
in principle be side-effecting, though it probably should not be.

Finding a definition for all types sounds like a problem that would
arrive at a fundamental paradox or ambiguity. Something similar in
spirit to the halting problem or Gödel's incompleteness theorem. (Aren't
some type systems Turing-complete? In that case we're already at the
former.) On top of the technical difficulties with logic there is the
philosophical problem of what a program means, which I assume is
indefinable as well.

> As I said, we should do some research first.

Warmly agreed - a lot of it :)

> For example, one objection against the many exported identifiers of
> the form TYPE-OPERATION (like vector-unfold or generator-map) is the
> duplication of similar identifiers. It would be enough to have general
> "procedures" unfold, map, etc., which takes as their first argument an
> expand-time value that selects the type (at expand-time). E.g.
>
> (map :vector PROC ARG)
>
> or
>
> (unfold :generator STOP? ...)
>
> One would implement (given that R7RS (large) becomes at least as
> expressive as R6RS) map, unfold, etc. as a macro, which checks whether
> the first argument carries a certain SRFI 213 property indicating that
> it specifies a type. If this is the case, the correct procedure is
> selected at expand-time.

The idea is interesting, but aren't these essentially more complex ways
to write vector-map and generator-unfold? Without type inference the
user doesn't save keystrokes.

I fear that if we normalize the use of macros to do something akin to
static analysis or generics, Scheme will cease to be a simple language
and will become something like Rust. When I started finding out about
R7RS-large I got the impression it was meant to be a large language in
the sense of a small core with a large library. If the core language
itself gets very complex, it will be something different in spirit from
classic Scheme. (As we know, many argue R6RS is already a step too far
in that direction; I'm neutral on that.)

(I'm using a layman's definition of simplicity, i.e. things are simple
when they look and feel simple. I strongly believe this is the right one
-- language design is first and foremost design, i.e. making things that
are good to use. Most of the time something is good to use when it's
among the simplest known ways to solve a given problem.)

My personal preference for static analysis would be a real type system
copied from the ML family, with full type inference so one doesn't need
type annotations. It would have to be an opt-in sublanguage; I think
having it opt-in is also the right thing.

The Common Lisp type system is another option. Personally I don't really
like that part of the language. I think bolting on static typing to a
dynamic language will inevitably end up with an inelegant result that is
hard to reason about.

Sorry about the heated tone; it's hard to talk about static types and
complexity on a Scheme list and stay neutral :)