On 6/14/26 17:46, Artyom Bologov wrote:
> I don’t see how environment becomes irrelevant here. Care to expand?

check-of/procedure-check-of (which is what derive-check became) operate
on datums, which are interpreted as programs in some environment. As I
understand it, the use for this would be in a macro, where one could
derive the check for a section of code, and place that check in a place
that expects a check, such as the predicate position of `check-arg`.

By using a datum, the code is used without any reference to its scope,
so any identifiers in it would have to be declared in the corresponding
environment. This would include identifiers that library code has
imported. In the current specification (which specifies the interaction
environment), this means that unless a check was imported into the REPL,
it would not be available for check-of/procedure-check-of.

In addition, if one uses this in a library, then the returned datum
whose interpretation is based on the interaction environment may not be
interpretable correctly in the library environment. (Example: a library
implementing SRFI 101, which uses `null?`, `pair?`, etc. internally as
something different than `null?` and `pair?` it the interaction
environment.) You generally can't `eval` the returned value and splice
in the check value as output from the macro.

Operation on expressions would allow the implementation to understand
the type information in context with other expressions. I don't know
about how type inference works on most implementations (Typed Racket is
probably very weird), but CRUNCH does all type inference after macro
expansion. Implementations that do that would then be able to replace

     (let ((x 10))
       (check-of (* x 1/2)))

is integer? (and not rational?) in the type-inference stage of a
compiler. Then if I import, say, SRFI 144 and write

     (let ((x (flonum 2.0))
       (check-of x))

it can return `flonum?` even if the flonum library is not imported into
the interaction environment.

As a macro, one could implement a very simple version in syntax-case:

``scheme
(define-syntax check-of
   (lambda (x)
     (syntax-case x ()
       ((_ (%lambda . rest))
        (if (free-identifier=? #'%lambda #'lambda)
            #'procedure?
            #f))
       ((_ y)
        (let ((y (syntax->datum #'y)))
        (cond
          ((integer? y) #'integer?)
          ((string? y) #'string?)
          ((boolean? y) #'boolean?)
          ;; etc.
          (else #f)))))))

(check-of (lambda (x) x)) ⇒ #<procedure procedure?>
(check-of 5) ⇒ #<procedure integer?>
```

Here it uses syntax objects and not datums, which preserve information
about the local environment, so that this can check for an expression
that is creating a lambda. (One could specify check-of to be a procedure
on syntax objects, but that would restrict its usefulness to only
R6RS-style expanders.)

A particularly high-powered implementation of SRFI 273 would instead
defer checking until the type-checking stage of the compiler, where it
could then use inferred type information to make a decision or to return #f.

-- Peter McGoron