Hi Peter,

> check-of/procedure-check-of (which is what derive-check became)
> operate on datums, which are interpreted as programs in some
> environment.

I think there’s a confusion here: check-of interprets its arguments as
data, while procedure-check-of only accepts procedures (not as
expressions, but as procedure? objects.) See
https://srfi.schemers.org/srfi-273/srfi-273.html#spec--procedure-check-of

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

Yes, that’s the intended use.

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

That’s a good case, which indeed is problematic. Returning an actual
procedure solves that, as it needs to additional interpretation in the
invoking environment. However, I opt for returning quoted expressions
instead of procedures because I really care about read/write
invariance—procedures are not write-able! Is there any solution to that
so that we both have context-aware (procedure-)check-of and read-write
invariance?

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

Hmmmmm, but this differs from check-of specification, which behaves like
a procedure and acts on evaluated data, i.e.

(check-of (+ 1 1)) ;; === (check-of 2)

So the implementation you listed is not compliant with the SRFI as
written now.

Another problem with this implementation is that it only works with
constant-ish data, so e.g. (check-of '5) returns #f. But that’s minor
and can probably be fixed if there’s will for that.

Whether the SRFI should be rewritten to work like that is another
question, and a good one! I personally feel that having the “The
returned value should be eval-uatable in the current
(interaction-environment)” language is just enough for the
specification, because the (interaction-environment) should be derivable
from the program / library as a whole at the compilations stage. But I
realize this is quite a requirement for the implementation!

Making environment explicit in the return value of (procedure-)check-of
is a possible solution. This can work either as:

• Last return value of (procedure-)check-of being an environment the
  other return values should be interpreted in.

• Environment being (again) passed explicitly into (procedure-)check-of
  and (procedure-)check-of guaranteeing that the returned check belongs
  to the provided environment.

• Restricting the return values to R7RS and (maybe) SRFI 235 + SRFI 26,
  to be safe in always having the necessary checks available.

Neither of these (and the last option in particular) is good. Currently,
it seems to me that designing (procedure-)check-of perfectly is almost
impossible. I want to settle on a version that does at least something
useful, and the current one seems to be just that.

Adding a clause specifying that the returned checks should be relevant
to the current library might be a good thing, though.

I am, of course, open to other options, because I’m at a stalemate right
now.

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

Oh, now I see where we have a misunderstanding. You seem to perceive
(procedure-)check-of as typeof in e.g. C
<https://en.cppreference.com/c/language/typeof>, while I perceive it as
type-of in e.g. Common Lisp
<https://www.lispworks.com/documentation/HyperSpec/Body/f_tp_of.htm> and
argtypes in trivial-arguments
<https://codeberg.org/shinmera/trivial-arguments/src/commit/f77147f1b92acef16ca5fee7a020814d0894bc28/arguments.lisp#L109>. Thus
your syntax and constant orientation, and my datum orientation. These
are indeed different types of operators, and both are too significant to
ignore!

Maybe it should be split into two sets of APIs:

• The current (procedure-)check-of

• And new (compile-time-check-of /constant/)

However, I wonder now whether they should be a separate SRFI, as the
complexity seems to be quite high for something (SRFI 273) intended as a
simple and portable extension to SRFI 253. It’s a whole type inference
territory now, and it’s much more diverse than I expected!

What do you think?

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