chickadee » srfi-253

SRFI-253: Data (Type-)Checking

Overview

Many Scheme programs, while dynamically typed, will have some degree of optional or non-optional checks on pre/post-conditions to procedures. A cynical view of this might be that users of Scheme really want a statically typed system, or believe that type checks are necessary in whole or in part to guarantee a correctness as a property of our programs.

Putting correctness aside, types can be leveraged by CHICKEN's compiler to make code faster, perform better inlining, etc. There is in fact a whole page on the wiki dedicated to the discussion of how CHICKEN uses types. This can result in faster code, and when compiling said code into some binary artefact, the compiler can even provide helpful hints as to when one might be making an error related to the types being passed into a procedure, or the types of objects being returned from a procedure.

Less cynically, it is helpful to be able to insert as well as inspect pre- and post-conditions on a procedure to produce more correct and more performant code. Whether this constitutes static-typing lipstick on a dynamic pig is not our problem; the kinds of checks that are provided by SRFI-253 come in the form of checking arguments and data, and yet are not limited strictly to the definition of a single or even related set of "types" in the typical way that one might understand a static type system in C or even Haskell.

Precedent for SRFI-253

Broadly, there are many systems that Schemers use today in order to perform said checks. In CHICKEN alone, we have:

SRFI-253 exists to coalesce the many ways in which this is done today and try to provide a single set of interfaces that provide the same functionality, but more portably and with a more compact syntax. This is not to say that SRFI-253 does anything distinctly different — it in fact mostly just standardizes existing practice with some forethought to how an API like this might be used across R7RS implementations.

For more information on "why SRFI-253?", you should see the SRFI document.

Does this do multiple-dispatch like COOPS?

The answer here is it depends; but generally no, not really. COOPS' multiple dispatch based on types has a much more complex resolution mechanism than SRFI-253 provides. Even if you were to use check-case to try and simulate this somehow, you would very quickly find that the left-to-right resolution of the syntax forms produces a much different kind of type resolution, and one that only works on a single parameter at a time (i.e. no multiple dispatch, only single dispatch).

If you really need an object-model or some meta-object protocol for method resolution using multiple dispatch, it is advised that you stick to COOPS and avoid SRFI 253. If single dispatch according to a single argument is all you need (i.e. you're doing something akin to the datatype or record-variants eggs), then SRFI-253 may be sufficient for your needs.

Installation

Installation happens through chicken-install. You should be able to do the following:

 
chicken-install -s -test srfi-253

Module Structure

There is exactly one module in this egg: (srfi 253). You can import it as follows:

 
(import (srfi 253))

Note: everything in this egg is syntax of some kind, and thus can be imported via import-syntax as well as import:

 
(import-syntax (srfi 253))

This way, CHICKEN does not attempt to link to the egg directly, but instead just imports the syntax itself. You may need to import (chicken base) in order to get access to import-syntax.

Reporting issues

Please report issues in the repository or on the CHICKEN bug tracker.

Known Bugs & Limitations

This egg more or less packages the sample implementation of the SRFI with some caveats. These are:

Also note that this egg intentionally uses assert internally to check any conditions or predicates in its syntax forms. This means that if you compile with -unsafe on, these assertions will be compiled out and removed. This is intentional so that unnecessary checks can be removed if you find that constant precondition checking is a drag on performance. This allows one to test with a lower optimization threshold (-O3 and lower) and test for correctness, but switch to a higher optimization threshold (-O4 and higher) and skip all the extra checks after the program has been verified.

Repository

https://gitlab.com/ThatGeoGuy/srfi-253/

Tutorial

Checking arguments in procedure definitions

The simplest use of this egg is to merely check the types of arguments in your procedures:

 
(define (my-proc a b c)
  (check-arg procedure? a 'my-proc)
  (check-arg string? b 'my-proc)
  (check-arg list? c 'my-proc)
  ; ...
  )

This mostly mirrors what the check-errors egg does; however, this is a bit verbose and tiresome. You can go a step further by checking the arguments in one call to values-checked instead:

 
(define (my-proc a b c)
  (values-checked (procedure? string? list?)
    a b c)
  ; ...
  )

This is the primary basis for most of this SRFI: checking arguments via pre-conditions with check-arg or checking multiple arguments with values-checked.

Taking this a step further, we can define my-proc using define-checked to pair these arguments right off the bat:

 
(define-checked (my-proc (a procedure?) (b string?) (c list?))
  ; ...
  )

Which is a syntactic way of performing the very same checks in-place. Note though, that define-checked does not support "rest" args:

 
(define-checked (foo (a integer?) . rest)
  ; ...
  )

The above code results in an error! This is an implementation restriction in CHICKEN specifically. If you need to use "rest" arguments whatsoever, it is recommended to use regular define with either values-checked or check-arg explicitly.

Single-Dispatch based on Predicates

SRFI-253 also provides a simple form of predicate-based single-dispatch via check-case. This is similar to variant record dispatch via datatype, record-variants, or SRFI-99. You might wish to write a procedure that is recursive on certain structures, or roots its base-case on some other predicate check. For example, this is how one might vector-ify a tree of cons-pairs:

 
;; Assume that our tree of pairs is either a single
;; number (a leaf node), or consists of a pair.
(define tree '((33 . 44) . 55))

(define (vectorify x)
  (check-case x
    (number? x)
    (pair? (vector (flatten (car x))
                   (flatten (cdr x))))))

(vectorify tree) ;=> #(#(33 44) 55)

check-case is a bit more general than Scheme's default case syntax; notably, any predicate can be used to check equality rather than how case uses eqv? for each datum.

Note that check-case evaluates the expression in left-to-right order. This can matter if you are using multiple predicates that may evaluate to #t for the same value. E.g.:

 
(check-case 4
  (number? (print "I am a number"))
  (integer? (print "I am an integer"))
  (else
    (print "I don't know what I am")))

;=> "I am a number"

By changing the order, we might get:

 
(check-case 4
  (integer? (print "I am an integer"))
  (number? (print "I am a number"))
  (else
    (print "I don't know what I am")))

;=> "I am an integer"

Be careful that you always pick your predicates in the correct order, so as not to evaluate the wrong body branch!

API Reference

(check-arg predicate? expr [caller])syntax

Guarantees that the expression expr satisfies the procedure predicate?. Implementations can enforce the predicate check in all the code that follows, but are not required to. An error is raised if the predicate returns #f when called on the value that expr evaluates to. Otherwise, return value is unspecified.

Note that check-arg will do nothing if you compile your program with the -unsafe flag, as this macro expands to call CHICKEN's assert internally.

(values-checked (predicate? ...) expr ...)syntax

Guarantees that the evaluated expressions expr ... satisfy the given predicate? ... in order and returns them as multiple values. The number of values and predicates should match exactly. An error is raised if any of the predicates returns #f.

(check-case expr (predicate? body ...) ... [(else else-body ...)])syntax

Checks whether the expression expr satisfies one of the predicates. If any of the predicates is satisfied, it evaluates the body corresponding to the first one that is satisfied, in left-to-right order. If none of the predicates is satisfied, one of two things may happen:

  1. If an else clause is present, the body of that else clause is evaluated.
  2. If an else clause is not present, an error is instead raised.

While this is similar to something like compiler-typecase, this form specifically guarantees that a missing else block won't result in a syntax-expansion error if run in the interpreter or with -specialization disabled at compile time.

(lambda-checked ((arg-name predicate?) args ...) body ...)syntax
(define-checked (name ((arg-name predicate?) args ...) body ...))syntax
(define-checked name predicate? value)syntax

A regular lambda, but where any argument checks (akin to calling check-arg directly) can be specified by writing (arg-name predicate?) in where a regular lambda would only allow arg-name.

Example:

 
(import (srfi 253))

(define foo (lambda-checked ((x number?)) (+ x 1)))

(foo 2)             ;=> 3
(foo "hello world") ;=> An error is raised

define-checked relates to lambda-checked the same way that define relates to lambda. The second form of define-checked validates that the value bound to name satisfies predicate?, or else an error is raised. define-checked also produces CHICKEN type declarations (see types) that match the defined function as well.

IMPORTANT NOTE: "rest" args such as ((arg1 pred?) args . rest) are not supported by this implementation, and will produce an compilation error if used.

(case-lambda-checked (((arg-name predicate?) args ...) body ...) ...)syntax

Similar to [[|case-lambda]], but allows for each argument to be specified as an (arg-name predicate?) pair which only succeeds if the argument matches the provided predicate.

IMPORTANT NOTE: like lambda-checked, case-lambda-checked does not support "rest" args such as ((arg2 pred?) args . rest). Attempts to use this syntax will result in a compilation error.

(define-record-type-checked type-name (constructor arg-name ...) type-predicate? field ...)syntax

Defines a record type with checked constructor and field accessors/modifiers. type-name, constructor, and type-predicate? are the same as R7RS define-record-type's (note especially the constructor— checks are not allowed in it, only arg-name symbols!). Fields are either of the form (field-name field-predicate? accessor-name) or (field-name field-predicate? accessor-name modifier-name). These ensure that accessor and modifier return checked data and check new data respectively. It is an error if any of the checks are not successful.

define-record-type-checked also guarantees that initial values passed to constructor satisfy the predicates provided in field specification.

License

The code is licensed under the MIT license:

 
MIT License

Copyright (c) 2024 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 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.

Contents »