Hi Philip,

Thanks for your detailed reply, and for tackling ‘mapping-search’!

On 2026-08-05 20:55 -0400, Philip McGrath wrote:
> Can I encourage you to look further into not only Typed Racket
> itself, but the history of attempts at type systems for Scheme that
> preceded it?  I’m not intimately familiar with the details myself,
> but my impression is that many of the ideas you discussed have been
> tried, particularly in the “soft typing” line of research from the
> ’90s (distinct from the “gradual typing” associated with Typed
> Racket).

Shortly after I replied to Artyom & Peter Bex, I realized that
I’d forgotten about the _éminence grise_ of gradually-typed Lisps,
Typed Racket.  I didn’t mean to write off gradual typing, by any
means.  There is, of course, an inherent difficulty in using it here,
in implementation-agnostic SRFI land: getting Scheme implementers to
accept a gradual-typing system is a rather distant hope.  Artyom’s
type-check system and runtime contracts have the merit of being
portable in current Scheme.

> Of course, this does not contradict the point that:
>
> >> (a) you have a way to express gnarly types

Apropos “gnarly types”, one thing I notice about the TR implementation
of ‘mapping-search’ is that the types don’t express the procedure’s
continuation semantics.  *insert* is a continuation, not a vanilla
(-> V Obj (Values (mapping K V) Obj)) function; it has to be tail-called
(just once) to continue ‘mapping-search’s search-and-build loop.
(The exposure of loop continuations is something I dislike about
‘mapping-search’, but the same idea shows up in many other places.)
I don’t know if TR has a way to express such things.

> >> (b) you’re willing to ignore a variety of possibilities.
>
> I'm less sure what exactly this means.
>
> It follows from Gödel that, for any static type system, there will be
> some correct programs that its axioms can't prove.

No kidding.  But I had in mind something less abstruse.  There is a
tradition of programming-language type systems covering enough to be
useful, without capturing the more difficult features of a language.
The types might just get too complicated for anyone to understand, or
the feature might be on the very edge of current type-theory research.
(I think David Herman is one of the few people to try to come up with a
type system including hygienic macros, for example.[1]  It’s hairy, to
say the least.)

I’ve become a bit disillusioned with static type systems in the past
few years, in part because of the truly intimidating complexity of
(Haskell) types in practical programs.  There seems to be an unavoidable
trade-off (at this point in programming-language design, at least)
between using a mind-boggling type to fully describe a program, or
to use a type comprehensible to mortals which only describes some
of the program’s characteristics.  Our ability to come up with crazy
programs far outstrips our ability to understand their types.

But I digress.

> But there are also different notions of soundness (see e.g.  Ben
> Greenman's work), and, in the (very different!) dynamic world of
> contracts, it is ultimately a pragmatic judgement what properties are
> worth checking, as contracts can express so much more than (at least
> mainstream) static types (There’s example here:
> <https://docs.racket-lang.org/guide/contracts-first.html>).  Mostly,
> I would encourage anyone to clarify their thinking on such questions
> before diving into implementation.

I agree, and I very much appreciate the references and food for
thought.  We should definitely review the possibility of gradual-typed
Scheme, as well as the contract-based alternatives.

Regards,

Wolfgang

[1]: https://dl.acm.org/doi/10.5555/1925552

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