283: (Type-)Check Introspection

by Artyom Bologov

Status

This SRFI is currently in draft status. Here is an explanation of each status that a SRFI can hold. To provide input on this SRFI, please send email to srfi-283@nospamsrfi.schemers.org. To subscribe to the list, follow these instructions. You can access previous messages via the mailing list archive.

Table of Contents

Abstract

This SRFI focuses on the introspection and type inference sides of typing / checking. It provides several useful procedures deriving types / checks for arbitrary data. procedure-check-of and check-of work with checks, as in SRFI 253. procedure-type-of and type-of work with implementation-specific types. check->sexp provides a way to serialize opaque checks from above into more readable s-expressions.

Issues

Rationale

Types / checks / contracts / assertions are useful. (The claim is debatable.) They might help ensure program correctness and prevent basic programming errors. But yet another function of these is explanatory. They help in setting the expectations, e.g., for what the procedure accepts and what it returns. Or understanding what the implementation-specific effective type for a value is. Having a way to infer / deduce / fetch types et al. for a procedure or a value is an important introspection mechanism. Thus this SRFI: to augment the declarative side of SRFI 253 and SRFI 273 with more explanatory power, and to allow peeking behind the implementation scaffolds for types.

The idea of checks and check-level introspection is (un)fortunately inherited from SRFI 253. The idea of type-level introspection was always on the surface in most Scheme implementations. Overall, this SRFI does nothing revolutionary (unless one is a static typing enthusiast thinking of types as a non-introspectable, purely compile-time artifact.)

Specification

There are two main concepts / levels in this specification: check-level and type-level. Check level focuses on checks, as per SRFI 253 and SRFI-273, while type level is based on an (inherently) implementation-specific notion of types, whatever they might mean.

Check-level API #

Checks, using the terminology of SRFI 253, might be the wrong basis for program checking. Types might be the right one. (One has yet to prove either.) However, checks capture the inherent dynamicity of Scheme values and are flexible enough for useful contract declaration. Introspecting the checks attached to the value / symbol / procedure is as useful as defining them. This section defines two procedures providing a complete set of introspection operations on procedures and values.

Given that SRFI 253 et al. serve as a portable façade for implementation-specific types, implementors are encouraged to infer checks even for things only having implementation-specific types. Thus making APIs in this section a superset of the next one.

There’s a peculiar choice of returning procedures instead of more introspectable s-expressions. It is motivated by the fact that s-expressions may be interpreted (eval-uated) in different ways depending on the context / environment. Returning procedures, on the other hand, ensures that there are no ambiguous interpretations. Thanks to Peter McGoron for bringing this up on the SRFI 273 mailing list. In case one does direly need s-expressions, one can use the check->sexp procedure to turn checks into parseable s-expressions.

(srfi 283) procedure-check-of proc ⟹ #f | [procedure | #f], #f | [procedure | #f] #

Procedure check introspection API. Accepts a procedure, possibly defined with SRFI 253 syntax or otherwise checked / typed. Returns two values:

Either of the returned values may be #f in case the implementation cannot provide the checks for arguments and / or returned values. For whatever reason and at any time. Including: always.

Rationale: this procedure is needed because it is necessary to get checks for both arguments and return values. Fitting all of these into a single returned procedure is nigh impossible. Earlier drafts of SRFI-273 included such a procedure / syntax, check-procedure-of?, but it was removed for reasons. Thus this particular operation and its return values.
(procedure-check-of procedure?)
;; => (#f) ;; No check due to “any” type
;; => (#<procedure boolean?>)
(procedure-check-of map)
;; Notice the lack of optional arguments checks
;; => (#<procedure procedure?> #<procedure list?>)
;; => (#<procedure list?>)
(procedure-check-of +)
;; => () ;; + has no required arguments
;; => (#<procedure number?>)
(procedure-check-of procedure-check-of)
;; => (#<procedure procedure?>)
;; => (#<procedure (disjoin list? boolean?)> #<procedure (disjoin list? boolean?)>)

(srfi 283) check-of obj ⟹ procedure | #f #

Returns the most exact check matching the value, as a procedure that this value must satisfy. Interpretation of “the most exact check” is left to the implementor. (It might overlap with Common Lisp’s concept of “actual type”.) The implementation can also return #f in case the check cannot be introspected — or at any time really.

(check-of 3)
;; => #<procedure exact-integer?>
(check-of check-of)
;; => #<procedure procedure?>

Type-level API

While checks might be a useful and portable way to reason about values, a more concrete and close-to-the-metal / implementation-specific introspection might be needed. Like… types. This section details on the forms working with types instead of checks.

(srfi 283) procedure-type-of proc ⟹ implementation-specific #

Returns an implementation-specific number of implementation-specific values characterizing the given procedure. It is recommended to follow the format of procedure-check-of—two pairs / booleans of types. Unlike procedure-check-of, returning a dotted list for arguments is possible, as some implementations type the rest argument too. Returning a single type object for procedures (like +) that accept a single rest argument is possible, too.

(srfi 283) type-of obj ⟹ implementation-specific #

Returns an implementation-specific object representing the type of obj. This is included by some implementations already.

Utilities #

(srfi 283) check->sexp proc ⟹ list | symbol | #f #

Working with checking procedures is not entirely worry-free. Given that Scheme has no procedure introspection facilities in the standard, even getting a procedure name is an adventure in itself. Thus the need for a helper that translates the opaque procedures into something printable and graspable.

check->sexp converts the passed-in check procedure into a symbol (in case of simple predicates, like integer?), list (for more complex ones, like (cut eqv? <> 3)), or returns #f (in case the conversion is unsuccessful).

Symbol Type Introspection

Early drafts of this SRFI included symbol-check-of and symbol-type-of procedures. The check / type metadata was attached to the symbol. These were supposed to be useful in case the domain of the symbol was wider than the domain of the value currently bound to it, say with a symbol restricted to reals, while its value is an exact integer. Both procedures were removed because interpretation of a symbol involves questions of environment management and evaluation. These are too expansive for a simple SRFI like this one, thus the removal.

Implementations might add these procedures if they wish to. But the complicated questions have to be answered for these.

Implementation

There is not yet a sample implementation.

Acknowledgements

Thanks to Peter McGoron for the discussion of an earlier design of this SRFI, then part of SRFI 273.

Thanks to Arthur Gleckler for shepherding the SRFI process all these years.

© 2026 Artyom Bologov.

Permission is hereby granted, free of charge, to any person obtaining a copy of this software and associated documentation files (the "Software"), to deal in the Software without restriction, including without limitation the rights to use, copy, modify, merge, publish, distribute, sublicense, and/or sell copies of the Software, and to permit persons to whom the Software is furnished to do so, subject to the following conditions:

The above copyright notice and this permission notice (including the next paragraph) shall be included in all copies or substantial portions of the Software.

THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.


Editor: Arthur A. Gleckler