Hi,

On Wed, Aug 5, 2026, at 2:56 PM, Artyom Bologov wrote:
> 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.

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). For a starting point (and almost everything I know), see §7, “Related Work,” in “The Design and Implementation of Typed Scheme” (Tobin-Hochstadt & Felleisen, 2008): https://doi.org/10.1145/1328897.132848

>
>> (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?))
>

Below I've written a toy implementation of `mapping-search` in Typed Racket (where the implementation is only there to confirm that it really does typecheck).

The most interesting part is is the type of the `type-test` argument to `make-comparitor`, `(-> Any Any : #:+ α)`. The part at the end is a “positive proposition” saying that, when the result is non-false, the argument has the type `α` (a polymorphic type variable). The “positive” part means the proposition doesn't imply anything when the result is `#f`, so you can still use predicates like `string-containing-x?` that are more specific than a corresponding static type like `String`. This is part of “occurrence typing,” one of the innovative contributions of Typed Racket's type system. When a predicate with a proposition controls a conditional, Typed Racket can use the information from the to refine the types of constants. There's an introduction to “occurrence typing” here: https://docs.racket-lang.org/ts-guide/occurrence-typing.html

Of course, this does not contradict the point that:

>> (a) you have a way to express gnarly types

In some ways the type of `mapping-search` is simpler than the type of `+`, which pretty-prints at 413 lines! It uses a `case->` form to cover e.g. `(-> One Negative-Fixnum Nonpositive-Fixnum)`, not just `(-> Number Number * Number)`.

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

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.

With that, here’s the code:

#lang typed/racket

(struct (α) comparator
  ([type-test-predicate : (-> Any Any : #:+ α)]
   [equality-predicate : (-> α α Any)]
   [ordering-predicate : (-> α α Any)]
   [hash-function : (-> α Exact-Nonnegative-Integer)]
   [ordered? : Boolean]
   [hashable? : Boolean]))

(: make-comparator (∀ (α)
                      (-> (-> Any Any : #:+ α)
                          (-> α α Any)
                          (U #f (-> α α Any))
                          (U #f (-> α Exact-Nonnegative-Integer))
                          (comparator α))))
(define (make-comparator type-test equality ordering hash)
  (comparator
   type-test
   equality
   (or ordering (λ (x y)
                  (error "ordering not supported")))
   (or hash (λ (x)
              (error "hashing not supported")))
   (and ordering #t)
   (and hash #t)))

(struct (K V) mapping
  ([comparator :  (comparator K)]
   ;; To simplify the presentation,
   ;; I'm just using an alist for the internal implementation,
   ;; which is very inefficient and totally ignores ordering.
   ;; But note that `Listof` and `Pairof` do not leak into
   ;; the type of `mapping-search`, so you can replace it with
   ;; a better data structure without changing the interface.
   [alist : (Listof (Pairof K V))]))

(define-type (Insert K V Obj)
  (-> V Obj (Values (mapping K V) Obj)))
(define-type (Ignore K V Obj)
  (-> Obj (Values (mapping K V) Obj)))
(define-type (Update K V Obj)
  (-> K V Obj (Values (mapping K V) Obj)))
(define-type (Remove K V Obj)
  (-> Obj (Values (mapping K V) Obj)))

(: mapping-search (∀ (K V Obj)
                     (-> (mapping K V)
                         K
                         (-> (Insert K V Obj)
                             (Ignore K V Obj)
                             (Values (mapping K V) Obj))
                         (-> K
                             V
                             (Update K V Obj)
                             (Remove K V Obj)
                             (Values (mapping K V) Obj))
                         (Values (mapping K V) Obj))))
(define (mapping-search m k failure success)
  (match-define (mapping cmp alist) m)
  (define same?
    (comparator-equality-predicate cmp))
  (let loop ([prefix : (Listof (Pairof K V)) '()]
             [alist alist])
    (cond
      [(null? alist)
       (: insert (Insert K V Obj))
       (define (insert v obj)
         (values (mapping cmp (append prefix
                                      (list (cons k v))))
                 obj))
       (: ignore (Ignore K V Obj))
       (define (ignore obj)
         (values m obj))
       (failure insert ignore)]
      [(same? k (caar alist))
       (define tail (cdr alist))
       (: update (Update K V Obj))
       (define (update k v obj)
         (values (mapping cmp `(,@prefix ,(cons k v) ,@tail))
                 obj))
       (: remove (Remove K V Obj))
       (define (remove obj)
         (values (mapping cmp (append prefix tail))
                 obj))
       (success (caar alist) (cdar alist) update remove)]
      [else
       (loop (cons (car alist) prefix)
             (cdr alist))])))