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 derive-check form to derive a suitable check for an expression; type-matching syntax check? and check-impl? in syntax-rules, and some checking utilities.
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.
Some of the features in this SRFI are beyond the existing practice, and are marked as optional.
These are hidden behind cond-expand features for portability.
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.
derive-check primitive to derive a suitable check for a given expression. Expressions might be as complex as necessary, but there are no guarantees for check inference succeeding.
check-or? for union checks/types,
check-and? for intersection checks/types,
check-not? for negation checks/types,
check-memv? for member types,
check-eqv? for constant types,
check-list-of?, check-vector-of? for sequences with checked elements,
check-pair-of? for pairs with checked car/cdr,
check-procedure-of? for checking procedures against argument / return checks,
check-any? to accept any value.
syntax-rules extension with (check? predicate pattern) and (check-impl? datum pattern) match patterns to restrict rule matching to arguments of a certain type.
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? check-any?) (define-check email? string?) (define-check positive-integer? (check-and? 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, all of the args should be checks applied to the given positional argument.
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 check-any?) => (check-any?)) ;; Beware of using the rest argument with checks, see below (declare-checked (+ number? . number?) => (number?)) ;; Declare the contract for a function before it is defined (declare-checked (numbered-string string? integer?) => (string?)) (define (numbered-string str idx) (string-append str (number->string idx)))
Much like in the original SRFI 253, it is not recommended that rest argument check specifiers be used. This is because implementations unevenly support rest specifiers in macros and types. This is an unfortunate limitation that’s not resolvable without extensive cooperation between implementations. In other words, it's nearly unfixable.
This primitive should return the check matching the expression (implied to be a piece of code), or false, as an eval-uatable datum (quoted symbol or list),
possibly inferring the expression type.
Implementations may return false for any expression,
including in all cases.
This relaxed requirement is to support implementations that never check / infer / retain types of values.
It is not recommended that implementations eval the expression or any of its parts.
But, if they do so, they must manage mutable state, lexical/dynamic environment, and other implications of expression evaluation
so as to avoid surprising the programmer using derive-check.
derive-check is probably most useful in syntax-case (and other non-hygienic / procedural) macros because it
allows one to dispatch the behavior based on the type of macro arguments.
While SRFI 253 check-case might be used for simple cases of constant arguments, it’s insufficient for arbitrary forms.
Thus derive-check.
The behavior of derive-check on certain types needs further deliberation:
check-procedure-of? or procedure?, depending on sophistication of check inference in the implementation check-vector-of? predicate or vector? for vectors check-list-of?! derive-check is intended for deriving the check for expression-representing code, not for the type of expression itself. It just so happens that it returns the respective predicate for more primitive data above, because they usually represent themselves (automatically quoted) in the code. ;; Any of these might return #f and still be compliant (derive-check 3) ;; => integer? or number? or exact? or exact-integer? (derive-check '(+ 1 1.333)) ;; => number? or inexact? ;; Example numbered-string function from before (derive-check '(numbered-string "a" 1)) ;; => string? (derive-check 'numbered-string) ;; => (check-procedure-of? (list string?) (list number?)) (derive-check +) ;; or (derive-check '+) ;; Note that rest pattern in check-procedure-of? is not entirely portable ;; => (check-procedure-of? (list* number? number?) (list number?)) (derive-check '(let ((a 3)) a)) ;; integer? or possibly bailout #f due to expression complexity (derive-check derive-check) ;; => (check-procedure-of? (list check-any?) (list (check-or? symbol? pair?)))
Implementations—especially compiled and/or statically typed—may restrict check return guarantees to previously compiled / loaded libraries / files and not the current library / file.
These extensions allow using special forms check? and check-impl? in syntax-rules patterns.
For check?, provided predicate should match the part of the expression matching the pattern.
In case predicate returns false for a given expression, rule matching is considered unsuccessful.
And should proceed to matching other syntax-rules clauses.
It is not an error if predicate returns false.
While inconsistent with the rest of this SRFI and SRFI 253, this behavior is more useful in type-dispatching macros.
Type-guarding can be achieved by providing only one check? rule
because, in this case, syntax expansion would fail due to lack of matching patterns.
check-impl? is a fallthrough to implementation-specific type/predicate checking.
datum can be anything the implementation considers a valid check.
In case the check of the pattern-matched expression for datum does not succeed, syntax matching should proceed to matching other clauses.
Much like check? pattern.
check? and check-impl? are optional extensions.
While recommended for implementation, they change the logic of syntax-rules to essentially do arbitrary computation at macro expansion time.
This is not realistic in many cases.
Due to optionality, these should be hidden behind an srfi-273-syntax-check feature identifier.
The main motivation for check? is smart behavior for embedded Scheme-s with manual memory management.
For example, a simplified version of automatic memory management let/free macro could be defined like this:
(define-syntax let/free
(syntax-rules ()
((_ () body)
(begin body))
;; pointer? is implementation-provided predicate for machine pointer objects
((_ ((symbol (check? pointer? value)) other-bindings ...) body ...)
((lambda (symbol)
(dynamic-wind
(lambda () #f)
(lambda () (let/free (other-bindings ...) body ...))
;; "free" here is an implementation-provided memory-freeing form
(lambda () (free symbol))))
value))
((_ ((symbol value) other-bindings ...) body ...)
((lambda (symbol)
(let/free (other-bindings ...) body ...))
value))))
The motivation of check-impl? is that many implementations provide type specifiers beyond what SRFI 253 covers,
such as pointer types and container types.
It is not realistic to map all the implementation types to predicates,
in part because some types might not have matching predicates.
check-impl? allows one to pass an implementation-specific type specifier (or something else altogether) without the need for predicate matching.
This is a grab-bag of useful utilities, inspired by functional combinators and TypeScript + Common Lisp types. Implementations might provide more utilities, in particular for typed sequences and other container / collection types.
In the simplest form, all of these are procedures. However, implementations might turn these into macros for increased optimization and smartness.
Disjoint / union check, accepting any number of predicates and returning a checking predicate that succeeds if any of them succeeds on the provided data. On implementations with types, may be optimized into union type.
Similar to check-or?, but implements conjoin / intersection logic.
Returns a new predicate that succeeds if all of the provided predicates succeeds on the provided data.
May be optimized into an intersection type.
((check-and? integer? positive?) 3) ;; => #t ((check-and? integer? positive?) -3) ;; => #f ((check-and? integer? positive?) 4.3) ;; => #f ((check-and? integer? positive?) "hello") ;; => #f
Return a new predicate that tests whether the provided value is not satisfying the predicate.
Return a new predicate testing the argument for being equal to constant,
compared with eqv?, like in case.
Additional utils using other equality predicates are beyond this SRFI,
in part because they are harder to optimize (-equal?) or useless (eq?).
Return a new predicate checking the argument for being one of members,
compared with eqv?, like in case and memv.
Additional utils using other equality predicates are beyond this SRFI.
Returns a new predicate.
This predicate tests a given object for being a list or vector (respectively), with each element satisfying predicate.
In case of list with tail-predicate, it checks the list's tail, too.
On implementations supporting that, it may be optimized to e.g. (vector-of TYPE) type.
A matching check-bytevector-of? utility for bytevectors is not provided, because bytevectors are unambiguously typed already and only need bytevector?.
Returns a new predicate.
This predicate tests a given object for being a cons pair.
With its car satisfying car-predicate and its cdr cdr-predicate.
Returns a new predicate. This predicate tests the provided object for being a procedure with args satisfying arg-predicates, and return values satisfying return-predicates-conforming values. Both arg-predicates and return-predicates are lists of predicate procedures.
Notice that this utility lacks a => auxiliary syntax.
This is because check-procedure-of? might be implemented as a procedure and not a macro.
;;; These examples might return #f ;;; if the implementation has different domains / requirements / data for procedure arguments ;; Regular functions with required arguments ((check-procedure-of (list integer?) (list boolean?)) even?) ;; #t ;; Rest argument as a single predicate (remember the note on rest arg non-portability) ((check-procedure-of number? (list number?)) +) ;; #t ;; Rest args following the positional args as dotted tail ((check-procedure-of (list* real? real? real?) (list boolean?)) <) ;; #t
Predicate that returns #t for any argument value.
While extremely simple implementation-wise, it is included for completeness and consistency of the utility set.
Another benefit is that implementations may be able to optimize it to a top type easily.
Sample implementation to be done.
Thanks to Yukari Hafner for working on trivial-arguments Common Lisp library,
where the author of this SRFI have contributed function type inspection,
inspiring derive-check.
Thanks also to Felix Winkelmann for working on CRUNCH compiler, during the use of which the need for type-checking macros manifested.
© 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.