|
| 1 | +#lang scribble/manual |
| 2 | + |
| 3 | +@begin[(require "../utils.rkt" scribble/example racket/sandbox racket/require |
| 4 | + (for-label (only-meta-in 0 typed/racket) |
| 5 | + (only-in racket/contract flat-contract?)))] |
| 6 | +@(define the-top-eval (make-base-eval)) |
| 7 | +@(the-top-eval '(require (except-in typed/racket #%module-begin))) |
| 8 | + |
| 9 | +@(define-syntax-rule (ex . args) |
| 10 | + (examples #:eval the-top-eval . args)) |
| 11 | + |
| 12 | +@title{Typed Contracts} |
| 13 | + |
| 14 | +@defmodule[typed/racket/contract] |
| 15 | + |
| 16 | +Typed Racket supports contract programming using the |
| 17 | +@racketmodname[racket/contract] library. This section covers the |
| 18 | +contract-specific features of the type system as well as the functionality |
| 19 | +currently supported in Typed Racket. |
| 20 | + |
| 21 | +@section{Types} |
| 22 | + |
| 23 | +@defform[#:kind "type" |
| 24 | + (Con [in type] [out type])]{ |
| 25 | + A contract can only be attached to values that satisfy its @racket[in] type, |
| 26 | + just like how a function can only be applied to arguments that satisfy its |
| 27 | + domain type. Attaching a contract with output type @racket[out] to a value |
| 28 | + with type @racket[t] either raises blame or results in a value with a more |
| 29 | + precise type. |
| 30 | + |
| 31 | + The result's type is a lower-bound of @racket[out] and @racket[t] with respect |
| 32 | + to the precision order, which is like the subtype order. It differs in that it |
| 33 | + lacks contravariance in negative positions such as function domains. |
| 34 | + |
| 35 | + @racket[Con] is the most general type for contracts. |
| 36 | +} |
| 37 | + |
| 38 | +@defform[#:kind "type" |
| 39 | + (FlatCon [in type] [out type])]{ |
| 40 | + This type is like @racket[Con] but corresponds to @tech{flat contracts}. All |
| 41 | + @racket[FlatCon] contracts have a corresponding @racket[Con] type. For |
| 42 | + example, a @racket[(FlatCon Real Real)] is also a @racket[(Con Real Real)]. |
| 43 | + |
| 44 | + A contract with @racket[FlatCon] type can be used as a function having domain |
| 45 | + type @racket[in]. |
| 46 | + |
| 47 | + Ordinary Racket @tech[#:key "contracts"]{values coercible to a contract}, such |
| 48 | + as integers, do not have this type. Coercing such values of type @racket[T] to |
| 49 | + a contract, as Racket's contract attachment forms automatically do, produces a |
| 50 | + value of type @racket[(FlatCon Any T)]. |
| 51 | +} |
| 52 | + |
| 53 | +@section{Data-structure Contracts} |
| 54 | + |
| 55 | +@deftogether[(@defproc[(flat-named-contract [name Any] |
| 56 | + [c (FlatCon a b)]) |
| 57 | + (FlatCon a b)] |
| 58 | + @defthing[any/c (FlatCon Any Any)] |
| 59 | + @defthing[none/c (FlatCon Any Any)] |
| 60 | + @defproc[(not/c [c (FlatCon a b)]) |
| 61 | + (FlatCon a b)] |
| 62 | + @defproc*[([(=/c [n Natural]) (FlatCon Any Natural)] |
| 63 | + [(=/c [z Integer]) (FlatCon Any Integer)] |
| 64 | + [(=/c [r Real]) (FlatCon Any Real)])] |
| 65 | + @defproc[(</c [r Real]) (FlatCon Any Real)] |
| 66 | + @defproc[(>/c [r Real]) (FlatCon Any Real)] |
| 67 | + @defproc[(<=/c [r Real]) (FlatCon Any Real)] |
| 68 | + @defproc[(>=/c [r Real]) (FlatCon Any Real)] |
| 69 | + @defproc[(between/c [lo Real] [hi Real]) (FlatCon Any Real)] |
| 70 | + @defproc[(real-in [lo Real] [hi Real]) (FlatCon Any Real)] |
| 71 | + @defproc*[([(integer-in [lo Positive-Integer] [hi Integer]) |
| 72 | + (FlatCon Any Positive-Integer)] |
| 73 | + [(integer-in [lo Natural] [hi Integer]) |
| 74 | + (FlatCon Any Natural)] |
| 75 | + [(integer-in [lo Integer] [hi Integer]) |
| 76 | + (FlatCon Any Integer)])] |
| 77 | + @defthing[natural-number/c (FlatCon Any Natural)] |
| 78 | + @defproc[(string-len/c [len Real]) |
| 79 | + (FlatCon Any String)] |
| 80 | + @defthing[printable/c (FlatCon Any Any)] |
| 81 | + @defproc[(listof [c (Con a b)]) |
| 82 | + (Con (Listof a) (Listof b))] |
| 83 | + @defproc[(non-empty-listof [c (Con a b)]) |
| 84 | + (Con (Listof a) (Pairof b (Listof b)))] |
| 85 | + @defproc[(list*of [c (Con a b)]) |
| 86 | + (Con (Rec x (Pairof a (U a x))) |
| 87 | + (Rec x (Pairof b (U b x))))] |
| 88 | + @defproc[(cons/c [car-c (Con a b)] |
| 89 | + [cdr-c (Con c d)]) |
| 90 | + (Con Any (Pairof b d))] |
| 91 | + @defproc[(syntax/c [c (FlatCon a b)]) |
| 92 | + (FlatCon (Syntaxof a) (Syntaxof b))] |
| 93 | + @defproc*[([(parameter/c [c (Con a b)]) |
| 94 | + (Con (Parameter b) (Parameter b))] |
| 95 | + [(parameter/c [in-c (Con a b)] |
| 96 | + [out-c (Con c d)]) |
| 97 | + (Con (Parameter b d) (Parameter b d))])] |
| 98 | + @defproc[(symbols [sym Symbol] ...+) |
| 99 | + (Con Any Symbol)])]{ |
| 100 | + These forms are typed versions of those found in Racket. They are otherwise |
| 101 | + the same. |
| 102 | +} |
| 103 | + |
| 104 | +@section{Function Contracts} |
| 105 | + |
| 106 | +Typed Racket supports two of Racket's function contract forms: @racket[->/c], a |
| 107 | +renamed version of the contract library's function combinator, and @racket[->i]. |
| 108 | +The grammar for each form is the same in Typed Racket as it is in Racket. |
| 109 | + |
| 110 | +For @racket[->/c], the ellipsis form is unsupported in Typed Racket. |
| 111 | +Additionally, both forms do not support the @racket[any] range. |
| 112 | + |
| 113 | +@section{Attaching Contracts to Values} |
| 114 | + |
| 115 | +Typed Racket supports two of Racket's contract attachment forms: |
| 116 | +@racket[contract-out] for attaching contracts to values that flow between server |
| 117 | +and client modules, in addition to the primitive contract attachment form |
| 118 | +@racket[contract] for directly attaching a contract to a value. Of course, |
| 119 | +@racket[provide/contract] is also supported. |
| 120 | + |
| 121 | +@; XXX: I wish I knew how to use the typechecker to get the input type. Also, |
| 122 | +@; is talking about the value's type before the contract's type the correct |
| 123 | +@; order? or should it be reversed? |
| 124 | + |
| 125 | +Currently, attaching a contract to a value requires the value's type to be a |
| 126 | +subtype of the contract's input type. The example below uses |
| 127 | +@racket[contract-out] to attach a function contract with input type @racket[(-> |
| 128 | +Integer Real)] to a function with type @racket[(-> Integer Integer)]. Because |
| 129 | +the latter is a subtype of the former, this program is well-typed. |
| 130 | + |
| 131 | +@ex[(module game typed/racket |
| 132 | + (provide |
| 133 | + (contract-out |
| 134 | + [number-game (->/c even? positive?)])) |
| 135 | + (: number-game (-> Integer Integer)) |
| 136 | + (define (number-game x) |
| 137 | + (+ 2 x))) |
| 138 | + (require 'game) |
| 139 | + (number-game 6)] |
| 140 | + |
| 141 | +If attaching a contract to a value does not satisfy this requirement, as in the |
| 142 | +following example, the typechecker rejects the program. |
| 143 | + |
| 144 | +@ex[(eval:error (contract odd? "11" 'pos 'neg))] |
| 145 | + |
| 146 | +Providing better error messages for Typed Racket's support of the contract |
| 147 | +library is a work in progress. |
| 148 | + |
| 149 | +@section{Limitations} |
| 150 | + |
| 151 | +@itemlist[ |
| 152 | + @item{Contract types do not have any contract compilation/runtime enforcement.} |
| 153 | + @item{Racket's built-in combinators for vectors, boxes, hashes are unsupported.} |
| 154 | + @item{Values that pass @racket[flat-contract?] are not necessarily members of |
| 155 | + the @racket[FlatCon] type: members of that type can be used in function |
| 156 | + position, but @racket[flat-contract?] returns true for non-predicates.}] |
0 commit comments