-
Notifications
You must be signed in to change notification settings - Fork 4
/
srfi-253.html
650 lines (549 loc) · 28.2 KB
/
srfi-253.html
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
382
383
384
385
386
387
388
389
390
391
392
393
394
395
396
397
398
399
400
401
402
403
404
405
406
407
408
409
410
411
412
413
414
415
416
417
418
419
420
421
422
423
424
425
426
427
428
429
430
431
432
433
434
435
436
437
438
439
440
441
442
443
444
445
446
447
448
449
450
451
452
453
454
455
456
457
458
459
460
461
462
463
464
465
466
467
468
469
470
471
472
473
474
475
476
477
478
479
480
481
482
483
484
485
486
487
488
489
490
491
492
493
494
495
496
497
498
499
500
501
502
503
504
505
506
507
508
509
510
511
512
513
514
515
516
517
518
519
520
521
522
523
524
525
526
527
528
529
530
531
532
533
534
535
536
537
538
539
540
541
542
543
544
545
546
547
548
549
550
551
552
553
554
555
556
557
558
559
560
561
562
563
564
565
566
567
568
569
570
571
572
573
574
575
576
577
578
579
580
581
582
583
584
585
586
587
588
589
590
591
592
593
594
595
596
597
598
599
600
601
602
603
604
605
606
607
608
609
610
611
612
613
614
615
616
617
618
619
620
621
622
623
624
625
626
627
628
629
630
631
632
633
634
635
636
637
638
639
640
641
642
643
644
645
646
647
648
649
650
<!DOCTYPE html>
<html lang="en">
<!--
SPDX-FileCopyrightText: 2024 Artyom Bologov
SPDX-License-Identifier: MIT
-->
<head>
<meta charset="utf-8">
<title>SRFI 253: Data (Type-)Checking</title>
<link href="/favicon.png" rel="icon" sizes="192x192" type="image/png">
<link rel="stylesheet" href="https://srfi.schemers.org/srfi.css" type="text/css">
<meta name="viewport" content="width=device-width, initial-scale=1"></head>
<body>
<h1><a href="https://srfi.schemers.org/"><img class="srfi-logo" src="https://srfi.schemers.org/srfi-logo.svg" alt="SRFI surfboard logo" /></a>253: Data (Type-)Checking</h1>
<p>by Artyom Bologov</p>
<h2 id="status">Status</h2>
<p>This SRFI is currently in <em>final</em> status. Here is <a href="https://srfi.schemers.org/srfi-process.html">an explanation</a> of each status that a SRFI can hold. To provide input on this SRFI, please send email to <code><a href="mailto:srfi+minus+253+at+srfi+dotschemers+dot+org">srfi-253@<span class="antispam">nospam</span>srfi.schemers.org</a></code>. To subscribe to the list, follow <a href="https://srfi.schemers.org/srfi-list-subscribe.html">these instructions</a>. You can access previous messages via the mailing list <a href="https://srfi-email.schemers.org/srfi-253/">archive</a>.</p>
<ul>
<li>Received: 2024-08-08</li>
<li>Draft #1 published: 2024-08-13</li>
<li>Draft #2 published: 2024-08-27</li>
<li>Draft #3 published: 2024-09-01</li>
<li>Draft #4 published: 2024-09-23</li>
<li>Draft #5 published: 2024-10-07</li>
<li>Draft #6 published: 2024-10-10</li>
<li>Draft #7 published: 2024-10-24</li>
<li>Draft #8 published: 2024-10-28</li>
<li>Finalized: 2024-11-15</li>
</ul>
<h2 id="toc">Table of contents</h2>
<ol>
<li><a href="#abstract">Abstract</a>
<li><a href="#rationale">Rationale</a>
<li><a href="#specification">Specification</a>
<ol>
<li><a href="#spec--check-arg">(check-arg predicate arg [caller])</a>
<li><a href="#spec--values-checked">(values-checked (predicates ...) values ...)</a>
<li><a href="#spec--check-case">(check-case value (predicate body ...) ... [(else else-body ...)])</a>
<li><a href="#spec--lambda-checked">(lambda-checked (args ...) body ...)</a>
<li><a href="#spec--case-lambda-checked">(case-lambda-checked ((args ...) body ...) ...)</a>
<li><a href="#spec--define-checked">(define-checked (name args ...) body ...) | (define-checked name predicate value)</a>
<li><a href="#spec--define-record-type-checked">(define-record-type-checked type-name (constructor arg-name ...) predicate field ...)</a>
</ol>
</li>
<li><a href="#implementation">Implementation</a>
<ol>
<li><a href="#implementation--caveat-rest-arg">Caveat: Rest Argument Support Is Uneven</a>
<li><a href="#implementation--check-arg-macro">check-arg—procedure or macro?</a>
</ol>
</li>
<li><a href="#prior">Prior Art</a>
<ol>
<li><a href="#prior--conditionals">Guarding conditionals</a>
<li><a href="#prior--check-x">Ad hoc checks: check-*</a>
<li><a href="#prior--coercion-ensure">Coercion: ensure-*</a>
<li><a href="#prior--assume-assert">SRFI-145 (assume) and R6RS (assert)</a>
<li><a href="#prior--implementations">Implementation-specific (typing) primitives</a>
<li><a href="#prior--other-lisps">Other Lisps: Common Lisp, Clojure</a>
</ol>
</li>
<li><a href="#acknowledgements">Acknowledgements</a>
<li><a href="#copyright">Copyright</a>
</ol>
<h2 id="abstract">Abstract</h2>
<p>
Data validation and type checking (supposedly) make for more correct code.
And faster code too, sometimes.
And, in rare cases, code that's easier to follow than un-checked code.
Unfortunately, Scheme does not have many (type-)checking primitives out of the box.
This SRFI provides some, with the aim of allowing more performant and correct code with minimum effort on the user side.
Both (manual) argument checking/validation (<a href="#spec--check-arg"><code>check-arg</code></a>)
and return value(s) (<a href="#spec--values-checked"><code>values-checked</code></a>) checking/coercion are provided.
Syntax sugar like <a href="#spec--define-checked"><code>define-checked</code></a>
and <a href="#spec--define-record-type-checked"><code>define-record-type-checked</code></a> is added on top.
</p>
<h2 id="rationale">Rationale</h2>
<p>
Many Scheme code bases grow to a certain point—a point where entropy creates too diverse of an input set to ignore.
That's the moment most programmers turn to contracts (in a loose sense of the word) and data validation.
Other languages have type systems, object-orientation, type polymorphism, and other systems establishing code contracts.
Scheme doesn't.
</p>
<p>
Scheme programmers and projects often compile a set of validation utilities.
Be it for correctness (reliable data structure libraries, foreign function interfaces.)
Or for speed (game engines, numeric libraries.)
These utilities come in many shapes and implementations, but they can be split into several groups:
</p>
<ol>
<li id="use-case-1"> Argument/data validation.
<li id="use-case-2"> Value coercion.
<li id="use-case-3"> Function/value/record type declaration.
<li id="use-case-4"> Type/property/predicate dispatching.
</ol>
<p>
Implementations cater to these needs and cases, providing special forms/macros, usually for type declaration.
The syntax and semantics of these differ wildly, though.
If one wants to write correct, strongly typed, or performant code,
one is stuck with non-portable APIs and implementation-specific hacks.
Thus the need for standardization—one needs portable ways to ensure code validity/strictness.
</p>
<p>
The SRFIs most closely related to this one (and their differences) are:
</p>
<dl>
<dt><a href="https://srfi.schemers.org/srfi-145/">SRFI-145 (assume)</a></dt>
<dd>
One of the cited reasons for <code>assume</code> is performance gains.
Which is consistent with this SRFI.
The difference is the scope—this SRFI provides primitives covering most categories above.
While <code>assume</code> is exclusively restricted to generic condition checking <a href="#use-case-1">(1)</a>.
And practical use of <code>assume</code> is too wordy, a more inlined syntax (like <a href="#spec--lambda-checked"><code>lambda-checked</code></a>) never hurts.
</dd>
<dt><a href="https://srfi.schemers.org/srfi-187/">SRFI-187 (alambda)</a> and the like</dt>
<dd>
A withdrawn family of SRFIs, the only ones bearing the "Type Checking" category.
They fully cover the case of data validation and are good at establishing contracts in general.
A few (minor) flaws: they're withdrawn; and the scope of the alambda SRFI is explicitly wider than type checking, mostly focusing on procedure arguments <a href="#use-case-3">(3)</a> in general.
</dd>
<dt><a href="https://srfi.schemers.org/srfi-143/">SRFI-143 (Fixnums)</a>
and <a href="https://srfi.schemers.org/srfi-144/">SRFI-144 (Flonums)</a></dt>
<dd>
SRFIs defining two types of numbers that are "close to the metal" in being size and functionality restricted.
These SRFIs are already used by multiple implementations (Guile and PreScheme, notably) in code optimization.
And the notion of types is permeating both SRFIs.
The downside of both flonum and fixnum SRFIs is that they don't generalize to more types.
Which is a virtue in their particular context, but loss in terms of general (type-)checking.
This SRFI fills the gap for more types.
</dd>
</dl>
<p>
See the <a href="#prior">Prior art</a> section for more references and context.
</p>
<p>
This SRFI is novel in that it introduces a set of primitives explicitly geared for predicate/type checking.
It is designed so that implementations can turn these primitives into cheap and strong type checks if need be.
(The sample implementation already includes multiple implementation-specific optimizations, which proves the point.)
No other goal is pursued but allowing more correct, strict, and optimized Scheme code.
</p>
<h2 id="specification">Specification</h2>
<p>
Provided APIs can conceptually be split into two parts: basic and derived.
(The distinction won't be reflected in this section structure, but should be trivial to guess.)
Derived APIs are merely a syntactic sugar over basic primitives, but they are too useful for everyday programming to be left out.
Derived operations also mirror the way some implementations handle typing/contracts at the procedure/record level.
This solidifies existing practice, making it convenient to reproduce.
</p>
<p id="it-is-an-error">
It is recommended that implementations actually throw checking errors in all the "it is an error" cases below.
At least in debug mode.
The possible type of error might be <code>&assertion</code>.
Implementations are free to follow the original permissive "it is an error" behavior whenever deemed necessary, though.
</p>
<h3 id="spec--check-arg">(check-arg predicate arg [caller])</h3>
<p>
Guarantees that the <code>arg</code> (evaluated) conforms to the <code>predicate</code> (evaluated).
Implementations can enforce the predicate check in all the code that follows, but are not required to.
<a href="#it-is-an-error">It is an error</a> if <code>predicate</code> returns <code>#f</code> when called on <code>arg</code>.
Otherwise, return value is unspecified.
Implementations may use optional <code>caller</code> (evaluated) argument as the error who/origin if/when signaling a checking error.
</p>
<p>
One possible implementation, as found in SRFI-1, might be:
</p>
<pre>
(define (check-arg pred val caller)
(let lp ((val val))
(if (pred val) val (lp (error "Bad argument" val pred caller)))))
</pre>
<p>
Inspired by Common Lisp <code>check-type</code> special form.
</p>
<h3 id="spec--values-checked">(values-checked (predicates ...) values ...)</h3>
<p>
Guarantees that the <code>values</code> (evaluated) abide by the given <code>predicates</code> (evaluated)
(the number of values and predicates should match) and returns them as multiple values.
<a href="#it-is-an-error">It is an error</a> if any of the <code>predicates</code> returns false.
Implementations may choose to coerce the values when the types are compatible (e.g. integer -> inexact).
Supports multiple values:
</p>
<pre>
(values-checked (integer?) 9) ;; Single value
(values-checked (integer? string?) 9 "hello") ;; Multiple values
(values-checked (integer? real? char?) 9 83.12 #\a) ;; More values
(values-checked (integer?) 9.0) ;; 9 or 9.0
(values-checked (string?) 9) ;; => unspecified, is an error
</pre>
<p>
Notice that single value form still has the parentheses around the only predicate.
This is to avoid ambiguity.
Implementations must not omit parentheses.
If presence of parentheses was a marker for multiple values, then more complex predicate would break it:
</p>
<pre>
(values-checked (cut = <> 3) 9)
</pre>
<p>
<code>values-checked</code> is inspired by Common Lisp <code>the</code> special form
(one can already see the author comes from Common Lisp world),
declaring the unambiguous type for the return value.
The same inspiration can be traced in some Scheme implementations, like Chicken
(see <a href="#prior--implementations">(Prior Art) Implementations</a>).
</p>
<h3 id="spec--check-case">(check-case value (predicate body ...) ... [(else else-body ...)])</h3>
<p>
<code>check-case</code> checks whether the <code>value</code> satisfies one of the <code>predicate</code>s.
If any of the <code>predicate</code>s is satisfied, it evaluates the <code>body</code> corresponding to the first one that is satisfied.
If none of the <code>predicate</code>s is satisfied:
</p>
<ul>
<li> If there's a last <code>else</code> clause, it evaluates the respective <code>else-body</code>.
<li> Otherwise, <a href="#it-is-an-error">it is an error</a>.
</ul>
<p>
The return value is that of the satisfied clause <code>body</code>, <code>else-body</code> (when <code>else</code> clause is provided and no other clause matches), or unspecified.
</p>
<pre>
(check-case x
(integer? (+ 1 x)) ;; Return x + 1 if x is an integer.
(string? (+ 1 (string->number x)))) ;; Return x' + 1 where x' is read from x.
;; Otherwise (x is neither integer? nor string?), <a href="#it-is-an-error">it is an error</a>.
</pre>
<p>
Inspired by Common Lisp's <a href="https://www.lispworks.com/documentation/HyperSpec/Body/m_tpcase.htm">typecase</a> family of macros.
And Chicken's <a href="https://wiki.call-cc.org/man/5/Types#compiler-typecase">compiler-typecase</a> (already used/optimized in the sample implementation.)
</p>
<h3 id="spec--lambda-checked">(lambda-checked (args ...) body ...)</h3>
<p>
A regular lambda, but with any argument (except the rest argument) optionally having the form <code>(name predicate)</code>
(as compared to default single-symbol form).
Arguments of this extended form are guaranteed to satisfy the respective (evaluated) <code>predicate</code>.
At least on procedure application time.
This guarantee might be extended for all the procedure body, including for any modification and shadowing, at implementors' will.
<a href="#it-is-an-error">It is an error</a> if either of the arguments does not satisfy the predicate.
</p>
<pre>
;; See <a href="#implementation--caveat-rest-arg">(Implementation) Caveat: Rest Argument Support Is Uneven</a> for the caveats of using . rest pattern.
(define error
(lambda-checked ((who symbol?) (message string?) . irritants)
...))
</pre>
<h3 id="spec--case-lambda-checked">(case-lambda-checked ((args ...) body ...) ...)</h3>
<p>
Same as <code>case-lambda</code>, but with any argument taking a form of <code>(name predicate)</code> to be checked.
See <a href="#spec--lambda-checked">lambda-checked</a> section for other details.
</p>
<p>
Important note: <code>case-lambda</code> does not dispatch over its argument types <a href="#use-case-4">(4)</a>,
it only checks them <a href="#use-case-3">(3)</a>.
The only dispatching that happens is argument number dispatching.
</p>
<h3 id="spec--define-checked">(define-checked (name args ...) body ...) | (define-checked name predicate value)</h3>
<p>
Defines a procedure or variable satisfying the given predicates.
For procedures, effectively equal to <code>define+lambda-checked</code>:
</p>
<pre>
(define-checked (error (who symbol?) (message string?) . irritants)
...)
</pre>
<p>
For variables, checks the <code>value</code> (and, if implementation supports that, all the subsequent modifications) for the <code>predicate</code> match.
</p>
<pre>
(define-checked message string? "Hi!")
</pre>
<h3 id="spec--define-record-type-checked">(define-record-type-checked type-name (constructor arg-name ...) predicate field ...)</h3>
<p>
Defines a record type with checked constructor and field accessors/modifiers.
<code>type-name</code>, <code>constructor</code>, and <code>predicate</code> are the same as R<sup>7</sup>RS <code>define-record-type</code>'s
(note especially the constructor—checks are not allowed in it, only <code>arg-name</code> symbols!)
Fields are either of the form <code>(field-name predicate accessor-name)</code> or <code>(field-name predicate accessor-name modifier-name)</code>.
These ensure that accessor and modifier return checked data and check new data respectively.
<a href="#it-is-an-error">It is an error</a> if any of the checks are not successful.
</p>
<p>
<code>define-record-type-checked</code> also guarantees that initial values passed to constructor are satisfying the predicates provided in field specification.
</p>
<p>
<code>define-record-type-checked</code> is modeled after PreScheme's <code>define-record-type</code>.
</p>
<h2 id="implementation">Implementation</h2>
<p>
Sample implementation is done in standard syntax-rules, which makes it fairly portable and minimalist.
Chicken, Kawa, STklos, and Gauche-specific definitions with stronger typing/checking are also provided as <code>cond-expand</code>s.
</p>
<p>
<a href="srfi/impl.scm">Source for the portable sample implementation.</a>
See the <a href="https://github.com/scheme-requests-for-implementation/srfi-253">SRFI repository</a>
for other useful files.
</p>
<p>
Tested at least on
</p>
<ul>
<li> Guile: full support
<li> Kawa: full support:
<ul>
<li> <code>values-checked</code> coerces values whenever possible
<li> <code>check-arg</code> is not allowed in top-level context, only in wrapping block/procedure.
Which is not much of a hindrance, given that the main use-case is checking procedure arguments.
This divergence enables block-level optimizations.
</ul>
<li> STklos: full support
<li> Chicken: partial support, with type checking only working in compile-time and rest argument support missing.
<li> Gauche: partial support:
<ul>
<li> Rest arguments are not supported.
<li> <code>check-arg</code> shadows the syntax provided by <code>(gauche base)</code>...
<li>... and makes additional type checks with Gauche object system.
</ul>
<li> Gambit and Gerbil: broken, undebugged due to insufficient understanding of the implementation
</ul>
<h3 id="implementation--caveat-rest-arg">Caveat: Rest Argument Support Is Uneven</h3>
<p>
Significant limitation: sample implementation does not support rest arguments in <code>lambda-checked</code> and other lambda macros <em>on some implementations</em>.
Notably Chicken and Gauche, because these don't allow rest pattern in macros.
Sample implementation should seamlessly support rest arguments on implementations allowing them.
</p>
<h3 id="implementation--check-arg-macro">check-arg—procedure or macro?</h3>
<p>
Most SRFIs that use <code>check-arg</code> (1, 13, 44, 152) define it as a procedure.
Sample implementation defines it as a macro,
mostly to reuse more optimizable <code>assert</code>/<code>assume</code> underneath.
Implementations are free to make it a procedure, and it should work like one.
</p>
<h2 id="prior">Prior Art</h2>
<p>
This section is not normative.
It is mostly a result of review of all the accessible SRFIs.
(At the moment of writing, 0-252.)
And, occasionally, implementation manuals and (mostly Guile-based) real-world programs.
There are emergent patterns worth optimizing, and that's what this SRFI does.
</p>
<h3 id="prior--conditionals">Guarding conditionals</h3>
<p>
One's code only accepts certain types of things.
The simplest way to ensure that the arguments are the right type of things is to check, which is what <code>cond</code> is for:
</p>
<pre>
(cond
((integer? x) (+ 1 x))
((string? x) (+ 1 (string->number x)))
(else ???))
</pre>
<p>
This pattern has two problems:
</p>
<ul>
<li> One needs to list out all the conditions and potentially duplicate code.
<li> It's not clear what to do when none of the conditions is satisfied.
</ul>
<h3 id="prior--check-x">Ad hoc checks: check-*</h3>
<p>
One obvious action on data mismatch is to raise an error.
That's what the conventional <code>check-*</code> procedures tend to do.
Check that conditions are satisfied and error out if they don't <a href="#use-case-1">(1)</a>.
Something like what SRFI-144 does:
</p>
<pre>
(define (check-flonum! name x)
(if (not (flonum? x))
(error (string-append "non-flonum argument passed to "
(symbol->string name))
x)))
</pre>
<p>
The benefit of this pattern is that one can put a single <code>check-*</code> form at the start of the procedure and be done with it (SRFI-144 again):
</p>
<pre>
(define (flop1 name op)
(lambda (x)
(check-flonum! name x)
(let ((result (op x)))
(if (not (flonum? result))
(error (string-append "non-flonum result from "
(symbol->string name))
result))
result)))
</pre>
<p>
The most prevalent example of this strategy is the <code>check-arg</code>, giving the name to one of the primitives in this SRFI.
It's present in SRFI-1, SRFI-13, SRFI-44, SRFI-152, and likely some others.
The canonical implementation (as found in SRFI-1) is
</p>
<pre>
(define (check-arg pred val caller)
(let lp ((val val))
(if (pred val) val (lp (error "Bad argument" val pred caller)))))
</pre>
<h3 id="prior--coercion-ensure">Coercion: ensure-*</h3>
<p>
Another strategy of dealing with malformed data is trying to coerce/fix it <a href="#use-case-2">(2)</a>.
That's what conventional <code>ensure-*</code> procedure do:
</p>
<pre>
;; SRFI-175
(define (ensure-int x) (if (char? x) (char->integer x) x))
</pre>
<p>
The benefit of the approach is that one is always certain the data is well-formed (to a certain extent.)
Some data is too broken to be coerced, which raises a need for checking and erroring out.
</p>
<h3 id="prior--assume-assert">SRFI-145 (assume) and R6RS (assert)</h3>
<p>
Another way to check that things are in order <a href="#use-case-1">(1)</a> is using the R<sup>6</sup>RS <code>assert</code> or SRFI-145 <code>assume</code>.
These are primitives allowing to check whether the given expression is true and error out if it isn't.
Same as <code>check-*</code> procedures, but more generic.
</p>
<p>
<code>assume</code>, in particular, is used in at least 9 SRFIs, mostly to do simple predicate checks.
This use pattern highlights the need for predicate-checking primitive.
A new primitive that might be tuned for performance, because performance is one of the motivations behind <code>assume</code> SRFI.
</p>
<p>
One problem with <code>assume</code> is that it gets too verbose at times.
To the point of being longer than the actual procedure body.
Take this example from SRFI-214:
</p>
<pre>
(define (flexvector-ref fv index)
(assume (flexvector? fv))
(assume (integer? index))
(assume (< -1 index (flexvector-length fv)))
(vector-ref (vec fv) index))
</pre>
<p>
One needs a shorter (likely inlined in the procedure definition) way to provide types/predicates.
Otherwise it's too much visual clutter.
</p>
<h3 id="prior--implementations">Implementation-specific (typing) primitives</h3>
<p>
Most big implementations caring for performance or correctness provide typing/checking APIs.
The problem of <code>assume</code> verbosity from the previous section is solved at least by Bigloo, Chicken, Gambit/Gerbil, Kawa, and Typed Racket.
Either through inline types in procedure definition
</p>
<pre>
;; Kawa/Bigloo
(define (a x::integer)
x)
;; Gambit
(define-procedure (a (x integer))
x)
;; Typed Racket
(define a (lambda ([x : Integer]) x))
</pre>
<p>
or through the separate declaration forms
</p>
<pre>
;; Chicken
(: a (integer -> integer))
;; Typed Racket
(: a (-> Integer Integer))
</pre>
<p>
With these ways to check procedures <a href="#use-case-3">(3)</a> for types (and sometimes predicates, with custom types some implementations provide) one gets 90% there.
Procedures are almost all there is to Scheme, after all.
</p>
<p>
But some implementations aim for more, rivaling systems like Common Lisp or even statically typed languages.
Chicken provides <code>the</code> for return type checking <a href="#use-case-2">(2)</a>, and Kawa provides <code>as</code>, which additionally coerces the values whenever possible.
Chicken also has the <code>assume</code> form (not to be confused with SRFI-145), which pins the variables to types for the duration of the body <a href="#use-case-1">(1)</a>.
Chicken even has <code>compiler-typecase</code> to cover type dispatch <a href="#use-case-4">(4)</a>.
<a href="https://wiki.call-cc.org/man/5/Types">Chicken has a whole assortment of checking tools.</a>
</p>
<h3 id="prior--other-lisps">Other Lisps: Common Lisp, Clojure</h3>
<p>
Most of these things won't be a surprise after talking about how advanced Scheme implementations get.
Still, doesn't hurt highlighting things that likely were an inspiration (from Common Lisp) and that enhance the state of the art (in Clojure) of type/predicate checks.
</p>
<p>
The main departure point for this library is Common Lisp.
Having <a href="https://www.lispworks.com/documentation/HyperSpec/Body/m_assert.htm"><code>assert</code></a>
and <a href="https://www.lispworks.com/documentation/HyperSpec/Body/m_check_.htm"><code>check-type</code></a>
for <a href="#use-case-1">(1)</a>;
<a href="https://www.lispworks.com/documentation/HyperSpec/Body/s_the.htm"><code>the</code></a>
and <a href="https://www.lispworks.com/documentation/HyperSpec/Body/f_coerce.htm"><code>coerce</code></a> for <a href="#use-case-2">(2)</a>;
<a href="https://www.lispworks.com/documentation/HyperSpec/Body/s_declar.htm"><code>declare</code></a>
for <a href="#use-case-3">(3)</a>;
and <a href="https://www.lispworks.com/documentation/HyperSpec/Body/m_tpcase.htm"><code>(e|c|)typecase</code></a>
(not even mentioning the object system and type-dispatched methods) for <a href="#use-case-4">(4)</a>,
it's covering most of what one needs with types/predicates.
Thanks to gradual strong typing system integrated into the language.
</p>
<p>
Clojure, while being restricted by JVM and functional design, has type annotations, conveniently allowing one to attach types to values <a href="#use-case-2">(2)</a>.
It also has <a href="https://clojure.org/reference/special_forms#_fn_name_param_condition_map_expr_2">pre/post conditions</a>
for functions, allowing to check the argument validity <a href="#use-case-3">(3)</a>.
And, finally, there's <a href="https://clojure.org/news/2016/05/23/introducing-clojure-spec"><code>clojure.spec</code></a> that allows to define arbitrarily complex checks for data and match things to the contracts <a href="#use-case-1">(1)</a>.
</p>
<h2 id="acknowledgements">Acknowledgements</h2>
<p>
Thanks to Pjotr Prins for the project where the necessity for this SRFI emerged.
And for financing parts of this SRFI work.
</p>
<p>
Thanks to Arthur A. Gleckler for shepherding the whole process.
And for accommodating and being patient about some of my chaotic changes.
</p>
<p>
Thanks goes to all the people on SRFI mailing list. In chronological order:
</p>
<dl>
<dt>Marc Nieper-Wißkirchen</dt>
<dd>For mentioning <code>&assert</code> and suggesting stronger error behavior in this SRFI constructs</dd>
<dt>Antero Mejr</dt>
<dd>For multiple comments leading to significant clarifications of the text and for <code>define-record-type-checked</code> suggestion.</dd>
<dt>Wolfgang Corcoran-Mathe</dt>
<dd>For reiterations on stronger erroring behavior and input on <code>check-case</code>.</dd>
<dt>Juliana Sims</dt>
<dd>For:
<ul>
<li>check-arg clarifications and mandating caller argument.
<li>Suggesting removal/repurposing of relatively unnecessary "Design Decisions" section.
<li>Suggesting rewrite of opt-lambda-checked that ended up with its removal.
<li>Multiple wording and formalities comments.
</ul>
</dd>
<dt>Daphne Preston-Kendal</dt>
<dd>For convincing arguments in favor of <code>check-case</code> and other input.</dd>
<dt>Retropikzel, Amirouche, Lassi Kortela, and Yuval Langer</dt>
<dd>For multiple comments, especially regarding practical matters and implementation.</dd>
</dl>
<h2 id="copyright">Copyright</h2>
<p>© 2024 Artyom Bologov.</p>
<p>
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:</p>
<p>
The above copyright notice and this permission notice (including the
next paragraph) shall be included in all copies or substantial
portions of the Software.</p>
<p>
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.</p>
<hr>
<address>Editor: <a href="mailto:srfi-editors+at+srfi+dot+schemers+dot+org">Arthur A. Gleckler</a></address></body></html>