Artyom,

On 2026-08-05 16:13 +0400, Artyom Bologov wrote:
> How would you look at a project rigorously documenting types of all (or
> most) SRFIs? This might allow statically typed implementations like
> CRUNCH to easier infer types. Also helps to write more performant
> code. And allows to understand the shape of args for a given procedure.

Useful, but difficult and perhaps even impossible for some SRFIs.  As
you no doubt know from working on two type-checking SRFIs, there is a
*lot* of variety in Scheme types.  This is especially true in the realm
of higher-order procedures, which often have quantified types.  (For
example, the type of the value returned by ‘map’.)  Adding to the
difficulty is the fact that most SRFIs either give types informally or
don’t give them at all.

> The format I suggest is SRFI 273 declare-checked
> with a set of combinators from SRFI 235
> to have union
> (disjoin) and complement types.

I’m sorry I’m not more familiar with SRFIs 253 & 273, but do you think
they are up to defining types (perhaps we should say contracts) for
higher-order procedures?  I don’t see those mentioned in either SRFI.
If it’s possible to handle such standard patterns as folds and unfolds,
excellent; if not, I think the toolkit will have to be expanded
(perhaps with something like Findler & Felleisen’s higher-order
contracts[1]) before a SRFI type dictionary is possible.

(For an especially nasty stress test, try writing a type for SRFI 146’s
‘mapping-search’!)

[1]: https://www2.ccs.neu.edu/racket/pubs/icfp2002-ff.pdf

--
Wolfgang Corcoran-Mathe  <xxxxxx@sigwinch.xyz>