It is clear that static typing can help in the process of developing reliable software and libraries.  Recently my interest in typing has been motivated by other related concerns:

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

2) optimized compilation by specialization of the code to the types that are used by the program

For this the Gambit standard libraries are gradually being refactored to use a define-procedure macro that allows specifying the parameter types. Here is an example with the SRFI 1 list-tabulate procedure:

> (list-tabulate 10 square)
(0 1 4 9 16 25 36 49 64 81)
> (list-tabulate -10 square)
*** ERROR IN (stdin)@2.1 -- (Argument 1, n) Out of range
(list-tabulate -10 '#<procedure #2 square>)
1>
> (list-tabulate 10 'not-a-procedure)
*** ERROR IN (stdin)@3.1 -- (Argument 2, init-proc) PROCEDURE expected
(list-tabulate 10 'not-a-procedure)
1>

Note that the error messages are precise, giving the faulty argument number and name (when it is known), and the kind of error.

For list-tabulate it is not sufficient to say that the first parameter is an exact integer, it must also be non-negative (this type is called an “index”).  With define-procedure list-tabulate and all its dynamic type checking can be generated like this:

 (define-procedure (list-tabulate (n index) (init-proc procedure))
   (let loop ((i n) (result '()))
     (if (fx> i 0)
         (let ((i (fx- i 1)))
           (loop i (cons (init-proc i) result)))
         result)))

For procedures that do indexing in a sequence the type of the index (the allowed values) will depend on the length of the sequence.  For example vector-ref can be defined like this:

 (define-procedure (vector-ref (vector vector)
                               (k (index-range 0 (vector-length vector))))
   ...)

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.

The “index-range” type could also be used to give the type signature of number->string where the radix must be between 2 and 16:

 (define-procedure (number->string (number number) (radix (index-range 2 17) 10))
   ...)

Note that a default value of 10 is specified for the radix.

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.

Marc

> On Nov 9, 2022, at 5:54 PM, Lassi Kortela <xxxxxx@lassi.io> wrote:
>
> Scheme is a dynamically typed language and should stay that way.
>
> Nevertheless, static types are irresistible in some of the application areas that are of the greatest personal interest to me.
>
> The most important one is code sharing. Useful software systems involve a lot of unimaginative work implementing well known algorithms, formats, and protocols. Language enthusiasts often act like there are good reasons to have 100 slightly different variations of this stuff but I don't buy any of those reasons. I want less variety and more re-use.
>
> When thinking of code re-use, we should think first about execution models. A dynamic language can support virtually the same execution model as a static language. I think this should be exploited by writing most of the unexciting code in the static language, then translating to the dynamic one by throwing away the type restrictions. (Likewise code can be written in a language with macros, and the expanded code translated into a language without macros that has a similar execution model.)
>
> Observe that the converse does not work: translating a dynamic language into a static one is a scruffy Artificial Intelligence problem. Any formalism you could invent to solve it would itself be a type system.
>
> The reason I didn't quit Scheme after a few months as I initially expected is that it's still the best core for algorithmic programming. You get the lambda calculus with an arbitrarily extensible syntax that can be used to add types, constraints, and whatever else you need on the side. For as long as we'll represent programs as trees and not as more general graphs, this is where it's at.
>
> So if we add types to Scheme, that gives a language which translates easily enough into any language with a lambda calculus based execution model and either dynamic types or compatible static types.
>
> This ties into a big and evolving web I have in my mind about how to organize the social and technical aspects of programming for maximum productivity in the next decade or two. There's much more to be said on that later. For now, I'd like to remark that no one has the moral authority to step up and say "this is the kind of type system that Statically Typed Scheme (TM) should have". A standardized, dynamically typed language has dynamic types, and any static complement is just someone's opinion.
>
> That being said, it would be a tragedy if different groups of people go off and over time make 3 or 5 different type systems for Scheme with no possibility of code re-use between them.
>
> I'd like to make an attempt to avoid that fate early by surveying the kinds of type systems available, with a view to finding equivalences and automatic conversions between them. We should find ways to express algorithms and interfaces that solve practical problems in Scheme, such that the same surface syntax can automatically be turned into the dynamically type Scheme we have now as well as any nascent typed flavors. Ideally the surface syntax will be something as similar as possible to dynamic Scheme, which would make it painless to copy/paste code between them. Type inference the gateway.
>
> Personally I like my type systems the way I like my memory management: invisible. To that end, I'll pursue simplicity with maximum inference. If others are inspired to look into something heavier like effects or dependent types, that's fine. We should find ways to interface our work. There still is the https://github.com/pre-srfi/static-scheme repo which I kind of bowed out of since the proposed system got too complex for me. Maybe some of you will want to run with that and see where it goes.
>
> But I didn't fully realize back when we started the repo that "Typed Scheme" should intrinsically be a network of type systems with translation pathways between them, sharing as much surface syntax and nomenclature as possible. If memory serves, we started a kind of rivalry about what kind of type system would "win", but there should be no winner.
>
> The way to start the long trek toward types is bottom up: Find practical problems, then say "here's how I would express this using my favorite type system". Compare solutions. As the first order of business, we should write types for the procedures in RnRS and the most popular SRFIs.
>
> While these "Typed Schemes" will take a decade to mature into something canonical, I think the problem is urgent because it may guide the evolution of dynamic Scheme. My ideal is not the "gradual typing" found in Common Lisp and Racket, but "twin typing" where there are separate dynamic and static languages, and the surface syntax is as compatible as possible to the point that you hardly have to care which one you're using at any given time.
>
> Comments are welcome, but above all, please help me write down type signatures for the Scheme canon. There are bound to be many surprises, both pleasant and vexing.
>