> On Nov 11, 2022, at 2:17 PM, Lassi Kortela <xxxxxx@lassi.io> wrote:
>
> 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.

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.

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

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

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

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

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

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?

Marc