273: Extensions to Data (Type-)Checking273: Extensions to Data (Type-)Checkingby Artyom Bologov
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-273@nospamsrfi.schemers.org. To subscribe to the list, follow these instructions. You can access previous messages via the mailing list archive.
The original SRFI 253 established a basis for type-checked (or otherwise checked) data handling.
But it lacked some quality-of-life features.
This SRFI extends SRFI 253 to match existing implementation practice and common sense.
Provided extensions are:
check aliasing with define-check;
pre- and post-declaration of type / check with declare-checked;
return value checks
in lambda-checked, case-lambda-checked, and define-checked;
the check-of
and procedure-check-of
procedures to derive a suitable check for a datum / procedure;
and some optimizable checking patterns suggested to implementors.
SRFI 253 was good in establishing a fundamental set of data-checking primitives. It enabled portable strongly typed programming on multiple implementations. However, there was some incompleteness and mismatch with implementation practice in it. In particular:
define-checked and the like did not allow return-value checking. This meant that compiled procedures lacked important metadata useful for optimization.
This SRFI extends SRFI 253 based on additional exposure to type systems in languages like Common Lisp, TypeScript, and Haskell. It closes the gaps left by SRFI 253, two years after its publication. Hopefully, there won’t be a need for a third SRFI in this series.
This SRFI extends SRFI 253 to match the practice / behavior of many implementations, and to add quality-of-life features that are not present in implementations but are nonetheless a logical extension of SRFI 253 ethos. Thus it makes Scheme code with 253’s primitives even more optimizable, correct, and compliant. Backwards compatibility with SRFI 253 is an explicit priority, so all code written with SRFI 253 continues to work in implementations including this SRFI.
Included features (painfully missing from SRFI 253) are:
lambda-checked, case-lambda-checked (whenever available), and define-checked in procedure case.
define-check.
declare-checked syntax for pre-definition / post-definition / declaration of checks for a given procedure/variable. Matches Chicken Scheme : syntax and Common Lisp declaim ftype macro.
define-values-checked to match the define-checked
and define duality.
check-of and procedure-check-of.
SRFI 253 included a way to specify argument checks for procedures via lambda-checked and the like.
However, what was missing was return-value checking.
Most implementations supporting type annotations also support return-type checks.
SRFI 253 not mentioning these and leaving return-value checking to
values-checked form
was an under-specification.
Thus this addition.
Implementations supporting this SRFI must support return-value checking via a => operator in procedure-creating checking forms.
lambda-checked, case-lambda-checked (whenever available), and define-checked procedure form, in particular.
This operator should be followed by a parenthesized list of predicates checking the return value(s).
(Note that parentheses are not optional, like in
SRFI-253 value-checked).
It is an error if any of these predicate checks returns false.
Use of => for this might be seen as an unnecessary overload of an
already overused symbol.
But this is the most minimal and recognizable choice of an operator.
It is also similar in syntax to e.g. JavaScript arrow functions.
This form, when used in either of SRFI 253 or this SRFI primitives, passes the datum to the implementation unaltered. The form itself is discarded as a non-predicate. This is useful to allow implementation-specific types and types not covered by standard predicates.
check-impl? is not guaranteed to work in check-arg, because check-arg might be implemented as a procedure.
check-impl? should be avoided in this case.
(values-checked ((check-impl? uint)) -1) ;; is an error (define-checked (ref (data (check-impl? pointer)) (idx integer?)) (implementation-specific-ffi-pointer-ref data idx))
This form defines a new name-d checking predicate based on the provided predicate (possibly evaluated).
In the simplest implementation form, it might be a mere define aliasing a predicate value to name.
In a more complex, type-based implementation, it may define a new type derived from predicate-matching type, whenever derivable.
Implementations — especially compiled and/or statically typed — may require define-check to happen in a separate module from its first use.
This is to make static type inference easier.
However, implementors must allow intra-module define-check, possibly falling back to dynamic predicate definition.
(define-check any? (constantly #t)) (define-check email? string?) (define-check positive-integer? (conjoin integer? positive?)) (check-arg email? "srfi-273@example.com") ;; terminates normally (check-arg positive-integer? -3) ;; is an error
This syntax declares checks for a given value (in the first form) before / after the value itself was bound to a name.
Or argument / return checks for a procedure defined separately.
In the case of the procedure check declaration, argument checks are specified as either (arg pred?) (list of 2 elements) or arg (a single symbol,) like in define-checked
Return value type checks, introduced by => symbol, are syntactically optional.
They specify the checks for procedure return value(s) when provided.
The return value is unspecified.
It is highly recommended that checked declaration be supported even for symbols from other libraries. This supports post-factum type hardening, similar to TypeScript type declaration files.
;; Declare checks for pre-existing standard functions (declare-checked (identity x) => ((constantly #t))) ;; Declare the contract for a function before it is defined (declare-checked (numbered-string (str string?) (idx integer?)) => (string?)) (define (numbered-string str idx) (string-append str (number->string idx)))
Previous version of SRFI document used declare-checked only listing types without argument names.
Argument names were added because there’s a descriptive function to declare-checked.
To make fellow programmer’s codebase exploration easier.
Without the need to consult procedure definition in addition to declare-checked signature.
Same as define-values, but makes sure the values returned by form abide by checks.
Further symbol value modifications may be checked too.
Returns a check the provided datum satisfies, as a quoted symbol or expression.
Returns #f if the check cannot be derived.
The returned value should be eval-uatable in the current (interaction-environment) to get the check procedure that the datum satisfies.
The precision to which the check is derived is not specified.
Conceptually similar to type-of and typeof of other languages
and type-fetching primitives of some Scheme implementations.
;; Any of these might return #f and still be compliant (check-of 3) ;; => integer? or number? or exact? or exact-integer? (define-checked x (cut = 3 <>) 3) (check-of x) ;; => (cut = 3 <>) or number checks as above
Accepts a procedure (as per procedure?)
Returns two values:
#f (if argument check cannot be determined.)
In case the procedure accepts rest arguments, the returned checks are only covering required arguments.
Checking for rest / optional argument presence is beyond this SRFI.
Either of lists can be #f.
Like in check-of,
each expression in either list should be eval-uatable in the current (interaction-environment).
;; Example numbered-string function from before (procedure-check-of numbered-string) ;; => (string? integer?), (string?) (procedure-check-of +) ;; Rest argument not included ;; => (), (number?) (procedure-check-of eval) ;; Rest argument is ignored, fetch it elsewhere ;; => ((constantly #t) (constantly #t)), ((constantly #t)) (procedure-check-of procedure-check-of) ;; (procedure?), ((disjoin boolean? symbol? pair?) (disjoin boolean? symbol? pair?))
While SRFI 253 established behaviors for primitive/built-in types, it didn’t specify something like union types of sequence types. This is an under-specification. The proposed solution is to optimize the most obvious patterns used for these. Say, as SRFI 235 combinators. Or SRFI 26 pseudo-currying.
While all of these are listed here as relying on existing SRFI primitives, code analysis that can prove the equivalence of the combinator used with these can safely optimize these patterns:
(lambda (x) (and (integer? x) (positive? x))) ;; === (conjoin integer? positive?) (lambda (x) (not (integer? x))) ;; === (complement integer?)
Note that none of these are required for this SRFI compliance, and will work even in the absence of any special treatment from the implementation. These are combinators working with functions, after all.
Effectively a union check/type.
Effectively an intersection check/type.
Not check/type.
Member check/type against constants.
memv is picked specifically, as it’s close to implementation-specific type systems,
unlike more involved and non-optimizable member.
Single-member check/type.
List-of check.
Vector-of check.
Top/any check/type; and bottom/none check/type respectively.
Find the sample implementation for return value checking in SRFI 253 repository. It is also contributed to most existing SRFI 253 implementations (Chicken, Chibi, Gauche, Kawa,), ETA unspecified.
As for (srfi 273) APIs, here’s the minimal implementation:
(define-syntax define-check
(syntax-rules ()
((_ name predicate)
(define name predicate))))
(define-syntax define-values-checked
(syntax-rules ()
((_ (vars ...) (checks ...) form)
(define-values (vars ...) form))))
(define (check-of datum)
#f)
(define (procedure-check-of proc)
(values #f #f))
(define-syntax declare-checked
(syntax-rules (=>)
((_ name predicate)
(when #f #f))
((_ (name . args))
(when #f #f))
((_ (name . args) => return)
(when #f #f))))
Thanks to Yukari Hafner for working on trivial-arguments Common Lisp library,
where the author of this SRFI have contributed function type inspection,
inspiring procedure-check-of.
Thanks also to Felix Winkelmann for working on CRUNCH compiler, during the use of which the need for type-checking macros manifested.
Thanks to John Cowan and Peter McGoron for the discussion on better
procedure-check-of
and check-of
(previously derive-check) design.
© 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.