> Yes, typing becomes undecidable in the more general type systems. You
> have to supply proof that your program is well-typed. This, however,
> limits the expressibility of your language because you can no longer
> write non-halting programs. :)

:) I can't find a definition of well-typedness. Does it mean the types
can be known completely at compile time, which in a turing-complete type
system means you can prove the type specification terminates?

> Well, you can easily switch from some implementation to the other in your code:
>
> (define-syntax frobnicate
>    (syntax-rules ()
>      ((_ :type arg* ...)
>       (begin
>         (map :type arg* ...)
>         (unfold :type ...)
>         (improve :type ...)))))
>
> Then you can do
>
> (frobnicate :vector ...)
>
> when you want to frob vectors, or you can do (frobnicate :list ...)
> when you have to frob lists.
>
> (Of course, we need some syntax to make this easy and so that an
> identifier reference of frobnicate returns a proper procedure.)
>
> Think of
>
> (matrix* :gaussian-integers m1 m2).
>
> We only want to write matrix multiplication once but we mustn't have
> any runtime-type dispatching overhead in some numerical code.

OK, that makes sense. So you can re-use the implementation of an
algorithm to work on multiple data types, or write higher-order
collection procedures that pass the expand-time type information to
lower-level collection procedures.

Thanks for taking the time to write the example elsewhere in the thread;
it clarifies things a lot. Is this akin to Haskell type classes?

>> 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
>
> Rust is not bad, not at all, in my opinion. But that's not relevant here.

It seems like a vast improvement over C++. I meant to note that
languages like Rust, Haskell, and Common Lisp embrace complexity,
whereas Scheme (like Smalltalk and Lua) is noted for its simple core and
has been sitting on the fence regarding complexity. R7RS-large should
arrive at a consensus on how complex a core language is desired since
that consensus will have ripple effects on a lot of specific decisions.

> The macros I mentioned are not to be written by an everyday user but
> by a library writer. For the consumer, things can nevertheless become
> simpler.

Writing (generator-fold ...) is slightly simpler than (fold :generator)
IMHO since it looks roughly the same but involves fewer concepts.

However, (fold T ...) is indeed simpler if T is a type variable (in your
proposed scheme, an identifier with an expand-time property).

> I didn't mention static types initially. :) I am more interested in
> the reification of runtime-time types in expand-time (or vice versa)
> to make efficient compilation possible.

True, that was my fault :)

I would still prefer real static typing and type inference, but I may be
a one-person minority. I'd be happy to simply agree that a generics are
a bit slower in dynamically typed code, and if you want speed, drop into
static types which also permit additional optimizations like unboxing.
However, it's not clear how to efficiently pass data over the
static-dynamic boundary. IIRC John said Racket solved that problem by
gradually moving most of their standard library into Typed Racket.