Starting by trying to describe types for what's already in Scheme
sounds like a good idea.  I would start with the basics:

Be creative and try to think of what should be the types of the
following expressions:

+

0

#i0

(<operator> <operand> ...)

(<keyword> <datum> ...)

call/cc

(lambda (x)
  "converts seconds to minutes"
  (/ x 60))

(raise (make-assertion-violation))

(case-lambda
  [() 42]
  [(x) (when (symbol=? 'x 'german) "zweiundvierzig"])

(let* ()
  (define-record-type pair (fields x y))
  make-pair)

(values 1 2 3)

values

"string"

(string-copy "string")

Am Mi., 9. Nov. 2022 um 23:54 Uhr schrieb Lassi Kortela <xxxxxx@lassi.io>:
>
> 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.