Simple Function Specifications

8.12

Simple Function Specifications🔗ℹ

This package provides a few simple forms for creating definitions with specifications. These macros are much simpler and not as expressive as those provided by Racket’s contract library, but error messages for same-module violations of specifications will provide details about where the violation occurred that the standard racket/contract checks will not.

1 Definitions with Specifications🔗ℹ

syntax
(define/spec (name arg ...)
(-> spec ... spec)
body ...)

spec = any
| #t
| #f
| symbol
| predicate
| (cons spec spec)
| (list spec ...)
| (listof spec)
| (either spec ...)
| (both spec ...)
| (except spec)

Defines a function name equivalent to (define (name arg ...) body ...) but at each place where name is used, each provided argument is checked to ensure it passes its associated spec, and the return result is checked to ensure it passes the final spec.

Examples:

> (define/spec (plus x y)
    (-> integer? integer? integer?)
    (+ x y))
> (plus 40 2)
42
> (plus 40 "2")
plus: eval:4:0
2nd argument to plus failed predicate!
Expected: integer?
Given: "2"
> (map plus '(1 2 3) '(4 5 6))
'(5 7 9)
> (map plus '(1 2 3) '(4 5 "6"))
plus: eval:6:0
2nd argument to plus failed predicate!
Expected: integer?
Given: "6"
> (define/spec (sum-all xs ys)
    (-> (listof integer?)
        (listof integer?)
        integer?)
    (foldl (λ (x y total) (plus (plus x y) total))
           0
           xs
           ys))
> (sum-all '(1 2 3) '(4 5 6))
21
> (sum-all '(1 2 3) '(4 "5" 6))
sum-all: eval:9:0
2nd argument to sum-all failed predicate!
Expected: (listof integer?)
Given: '(4 "5" 6)
> (define/spec (sum-cars xs ys)
    (-> (listof (cons integer? any))
        (listof (cons integer? any))
        integer?)
    (foldl (λ (p1 p2 total) (plus (plus (car p1) (car p2)) total))
           0
           xs
           ys))
> (sum-cars '((1 "1") (2 "2") (3 "3"))
            '((4 "4") (5 "5") (6 "6")))
21
> (define/spec (bad-plus x y)
    (-> integer? integer? integer?)
    (number->string (+ x y)))
> (bad-plus 40 2)
bad-plus: eval:13:0
bad-plus returned invalid result!
Promised: integer?
Returned: "42"
Argument list: '(40 2)

syntax
(struct/spec name ([fld spec] ...))

A struct/spec form defines a structure data type name with a constructor that enforces the given specification for each field. In other words, it defines the following procedures:

name, a constructor which takes as many arguments as there are flds in order to create a name struct; each argument is checked against the associated fld’s spec. This identifier can also be used as a match-expander.
name?, a predicate (i.e. a procedure of one argument) that returns #t when given an instance of the structure type, otherwise it returns #f.
name-fld, for each fld; an accessor that takes an instance of the structure type and extracts the value for the corresponding field.

Examples:

> (struct/spec posn ([x number?] [y number?]))
> (define origin (posn 0 0))
> (define p (posn 3 4))
> (posn "3" "4")
posn: eval:17:0
1st argument to posn failed predicate!
Expected: number?
Given: "3"
> (define/spec (distance p1 p2)
    (-> posn? posn? number?)
    (match* (p1 p2)
      [((posn x1 y1) (posn x2 y2))
       (sqrt (+ (expt (- x2 x1) 2)
                (expt (- y2 y1) 2)))]))
> (distance origin p)
5

2 Specification Constructors🔗ℹ

The following forms are used to construct specs:

syntax
(-> spec ... spec)

Used to describe the argument and result specifications for a procedure that is being defined (i.e. only valid within a define/spec).

A function with n arguments would require an initial sequence of n spec that describe the arguments followed by a final spec that describes the result.

spec
any

A specification that allows any value.

spec
symbol

A literal symbol (e.g. 'apple) can be given to mean exactly that symbol value is permitted.

spec
predicate

Any identifier which is bound to a procedure that accepts 1 argument and returns a boolean can be used as a spec.

This can be a function defined by racket (e.g. symbol?, exact-nonnegative-integer?, etc), or any user defined procedure.

spec
(both spec ...)

Defines a spec that only allows values that pass all of the provided specs (they are checked in order, left-to-right).

e.g. (both integer? positive?) is a spec that only allows positive integers.

spec
(either spec ...)

Defines a spec that only allows values that pass at least one of the provided specs (they are checked in order, left-to-right).

e.g. (either (both integer? positive?) string?) is a spec that allows positive integers or strings.

spec
(listof spec)

Used to described a list where each element passes the spec.

e.g. (listof symbol?) allows a list of symbols.

spec
(cons spec spec)

Used to describe a pair where the car passes the first spec and the cdr passes the second spec.

e.g. (cons integer? string?) will allow values that are a pair where the car is an integer and the cdr is a string.

spec
(list spec ...)

Used to describe a list of fixed length where each positional spec describes what kinds of values are permitted in that position.

e.g. (list integer? string? (either string? #f)) allows lists of length three where the first element is an integer, the second a string, and the third is either a string or #f.

spec
(except spec)

Used to negate a spec.

e.g. (both integer? (except negative?)) allows non-negative integers.

3 Disabling Checks🔗ℹ

parameter
(define-with-spec-enforcement) → boolean?
(define-with-spec-enforcement status) → void?
status : boolean?
= #t

Specification checking can be disabled in a module by setting the define-with-spec-enforcement parameter (provided for-syntax by define-with-spec) to #f at phase level 1.

1	Definitions with Specifications
2	Specification Constructors
3	Disabling Checks