OK, now I *finally* understand where you're coming from :)

So you'd basically like to write ML/Haskell/Idris-style static type
definitions for everything defined in the SRFIs (as far as Scheme's
dynamic nature permits). And those would drive a Dialyzer workalike to
bring static type checking to a big percentage of Scheme code.

The reason I didn't understand what you meant, is I thought we were just
transcribing the argument signatures as written in the SRFIs into a
machine-readable form. But you would also like to formalize things that
are implied but not explicitly written (or are written in prose or
mathematical symbols, but could be converted to a formal definition for
a type checker with some manual work). So this is a *lot* more of a far
reaching project than the rest of us were pondering and I think a lot of
the confusion came from the fact that we didn't understand this.

I think the static checker is a very nice idea but this brings a bit of
an impedance mismatch - it's basically an open research problem, whereas
the rest of our project is just run-of-the-mill editorial and tools
work. For starters, is there a generally agreed-upon way to write the
types? Type systems are an active field of research and enthusiasts are
constantly debating which kind (no pun intended :D) is best.

Transcribing the definitions written in the SRFI as-is is quite
straightforward, but once you get into things that could be inferred
from that information, it becomes less clear how much information to
include. It's basically an open-ended research/development project. As
such, I wonder if whether the SRFI repositories are the right place to
house something that's so researchy/actively developed.

I sympathize with your concern in that storing the type definitions
right in each SRFI's own Git repository would make them more likely to
stay in sync. At the same time, this might necessitate quite a lot of
edits to the definitions as the type checker is figured out over the
years. The SRFI repos were originally made to track the documents; they
would now track both the documents and the exploratory type checking
work based on them.

What does Arthur as the editor think about this?

My personal motivation would be just to transcribe the simple things
written in the SRFIs into a machine-readable form, preferably quite soon
:) All the other work proposed here is awesome too, but I'm ambivalent
about how its the timeline and scope fit with the simpler and more
immediate goals originally proposed.

> (BTW, do you know of such a introspection tool?)

Nope. I thought you might have used one to obtain your definitions :)