Hi Wolfgang,

> > I don't know - those SRFIs seem overly dynamic, using things like
> > predicates and disjoin/union.  The CHICKEN type system is a lot simpler.

> I may be wrong, but I believe in Scheme it’s necessary to check types
> dynamically, as in Artyom’s SRFIs, unless either (a) you have a way
> to express gnarly types, or (b) you’re willing to ignore a variety
> of possibilities.

Yeah, that, basically. That’s why predicates and Clojure specs work
while Common Lisp type system not always does. It’s good, I was a
Common Lisper for like 5 years. Just that things like parametric and
dependent types are not easy to express even there. Too much
variability.

> (I don’t mean to bash CHICKEN’s type system, which I’ve used in most
> of my CHICKEN libraries.  But I’ve had to resort to the ‘*’ result
> type more often than I’d like.)
>
> Whatever their runtime cost, contracts at least have the flexibility
> to cover some of what Scheme offers.  First-class contracts can be
> dynamically constructed and passed, which can allow checking of argument
> procedures of higher-order functions.  (I don’t think Artyom’s SRFIs
> support this yet, but it is possible.)  Continuations are harder —
> I don’t know how much checking it’s possible to do (especially with
> undelimited ‘call/cc’ continuations), but contracts using continuation
> marks and barriers might be plausible.

Some things cannot really be checked. I mean, Java documents which
exceptions a method might throw, but it stops at that, because there’s
no idea what this exception throw might mean. Practically speaking,
some cases are better off ignored for the sake of project
implementability.

> For example, procedures can return various numbers
> of various types of values depending on their arguments, something
> that makes static typing of higher-order procedures a pain at best.
> For another, static typing of procedures that juggle control requires
> a type system which expresses Scheme’s first-class continuations.
>
> > 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.

CHICKEN has `forall' and `procedure' types, but these are not enough,
for sure. Early versions of SRFI 273 actually included a set of type
patterns, like check-procedure-of? (checking whether a procedure has a
certain argument contract) and check-list-of? (homogeneous list) which
were intended to be optimized by the implementations that wish to do
so. These were removed for the sake of minimalism and ease of
implementation, but they were part of the original design.

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

Yeah, they, in the current state, are not able to express every
possible type, but I consider that a good starting point anyways, for
the lack of better portable notation. Perhaps getting the removed
check-of-* predicates back purely for the purpose of bridging the gap
might be a good idea. Not fully sufficient, but good enough.

(Ignoring the fact that default type systems in most Schemes nowadays
don’t proceed much further than numeric types and one type per
Disjointness of Types
<https://standards.scheme.org/r7rs-html5/index.html#3.2> maybe.)

(SRFI 273 also mentions dependent types et al. as a further research &
standardization direction.)

Anyway, I consider this project of documenting types useful even with
the current state of 253/273. index.scheme.org has a simple enough
type system backing the index, but it’s quite useful already!

Useful enough also to allow kickstarting type systems in new Scheme
implementations almost for free. Writing a compiled and statically typed
implementation (TBA) I all too painfully realize the need for explicit
typing of SRFIs. Inferring types for them is a royal pain, and I dare
not think of implementing that.

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

Yeah, the best SRFI 253/273 can express, even with the removed
extensions, is:

(check-procedure-of? (list mapping? check-any? (check-procedure-of? (list procedure? procedure?)) procedure?) (list mapping? check-any?))

Which is wordy and incomplete, but better than just a

“(mapping-search mapping key failure success)”

that SRFI 146 itself says. More machine-readable too. So, for me, it’s a
question of maximizing usefulness per effort spent. And having SRFI
253/273 declarations is quite high on that scale.

Best of luck,
--
Artyom Bologov
https://aartaka.me