Am Do., 8. Okt. 2020 um 22:09 Uhr schrieb Lassi Kortela <xxxxxx@lassi.io>:
>
> > (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.

That can truly model all (decidable) types and thus all dependent
types. But you can hardly reason with it (think of a static analyzer).

> 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.

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. :)

> > 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.

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.

> 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.

> 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.)

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.

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

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.