Skip to content

Commit 53b993a

Browse files
btlachancebtlachance
committed
Clearer contract type names; Reexpose infer's meet/join
Typechecking or/c (in check-contract) uses infer/meet.
1 parent 76d0ef2 commit 53b993a

File tree

17 files changed

+220
-215
lines changed

17 files changed

+220
-215
lines changed

‎typed-racket-doc/typed-racket/scribblings/reference/typed-contracts.scrbl

Lines changed: 47 additions & 47 deletions
Original file line numberDiff line numberDiff line change
@@ -21,7 +21,7 @@ currently supported in Typed Racket.
2121
@section{Types}
2222

2323
@defform[#:kind "type"
24-
(Con [in type] [out type])]{
24+
(Contract [in type] [out type])]{
2525
A contract can only be attached to values that satisfy its @racket[in] type,
2626
just like how a function can only be applied to arguments that satisfy its
2727
domain type. Attaching a contract with output type @racket[out] to a value
@@ -32,72 +32,72 @@ currently supported in Typed Racket.
3232
to the precision order, which is like the subtype order. It differs in that it
3333
lacks contravariance in negative positions such as function domains.
3434

35-
@racket[Con] is the most general type for contracts.
35+
@racket[Contract] is the most general type for contracts.
3636
}
3737

3838
@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)].
39+
(FlatContract [in type] [out type])]{
40+
This type is like @racket[Contract] but corresponds to @tech{flat contracts}. All
41+
@racket[FlatCon] contracts have a corresponding @racket[Contract] type. For
42+
example, a @racket[(FlatContract Real Real)] is also a @racket[(Contract Real Real)].
4343

4444
A contract with @racket[FlatCon] type can be used as a function having domain
4545
type @racket[in].
4646

4747
Ordinary Racket @tech[#:key "contracts"]{values coercible to a contract}, such
4848
as integers, do not have this type. Coercing such values of type @racket[T] to
4949
a contract, as Racket's contract attachment forms automatically do, produces a
50-
value of type @racket[(FlatCon Any T)].
50+
value of type @racket[(FlatContract Any T)].
5151
}
5252

5353
@section{Data-structure Contracts}
5454

5555
@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)]
56+
[c (FlatContract a b)])
57+
(FlatContract a b)]
58+
@defthing[any/c (FlatContract Any Any)]
59+
@defthing[none/c (FlatContract Any Any)]
60+
@defproc[(not/c [c (FlatContract a b)])
61+
(FlatContract a b)]
62+
@defproc*[([(=/c [n Natural]) (FlatContract Any Natural)]
63+
[(=/c [z Integer]) (FlatContract Any Integer)]
64+
[(=/c [r Real]) (FlatContract Any Real)])]
65+
@defproc[(</c [r Real]) (FlatContract Any Real)]
66+
@defproc[(>/c [r Real]) (FlatContract Any Real)]
67+
@defproc[(<=/c [r Real]) (FlatContract Any Real)]
68+
@defproc[(>=/c [r Real]) (FlatContract Any Real)]
69+
@defproc[(between/c [lo Real] [hi Real]) (FlatContract Any Real)]
70+
@defproc[(real-in [lo Real] [hi Real]) (FlatContract Any Real)]
7171
@defproc*[([(integer-in [lo Positive-Integer] [hi Integer])
72-
(FlatCon Any Positive-Integer)]
72+
(FlatContract Any Positive-Integer)]
7373
[(integer-in [lo Natural] [hi Integer])
74-
(FlatCon Any Natural)]
74+
(FlatContract Any Natural)]
7575
[(integer-in [lo Integer] [hi Integer])
76-
(FlatCon Any Integer)])]
77-
@defthing[natural-number/c (FlatCon Any Natural)]
76+
(FlatContract Any Integer)])]
77+
@defthing[natural-number/c (FlatContract Any Natural)]
7878
@defproc[(string-len/c [len Real])
79-
(FlatCon Any String)]
80-
@defthing[false/c (Con Any False)]
81-
@defthing[printable/c (FlatCon Any Any)]
82-
@defproc[(listof [c (Con a b)])
83-
(Con (Listof a) (Listof b))]
84-
@defproc[(non-empty-listof [c (Con a b)])
85-
(Con (Listof a) (Pairof b (Listof b)))]
86-
@defproc[(list*of [c (Con a b)])
87-
(Con (Rec x (Pairof a (U a x)))
79+
(FlatContract Any String)]
80+
@defthing[false/c (Contract Any False)]
81+
@defthing[printable/c (FlatContract Any Any)]
82+
@defproc[(listof [c (Contract a b)])
83+
(Contract (Listof a) (Listof b))]
84+
@defproc[(non-empty-listof [c (Contract a b)])
85+
(Contract (Listof a) (Pairof b (Listof b)))]
86+
@defproc[(list*of [c (Contract a b)])
87+
(Contract (Rec x (Pairof a (U a x)))
8888
(Rec x (Pairof b (U b x))))]
89-
@defproc[(cons/c [car-c (Con a b)]
90-
[cdr-c (Con c d)])
91-
(Con Any (Pairof b d))]
92-
@defproc[(syntax/c [c (FlatCon a b)])
93-
(FlatCon (Syntaxof a) (Syntaxof b))]
94-
@defproc*[([(parameter/c [c (Con a b)])
95-
(Con (Parameter b) (Parameter b))]
96-
[(parameter/c [in-c (Con a b)]
97-
[out-c (Con c d)])
98-
(Con (Parameter b d) (Parameter b d))])]
89+
@defproc[(cons/c [car-c (Contract a b)]
90+
[cdr-c (Contract c d)])
91+
(Contract Any (Pairof b d))]
92+
@defproc[(syntax/c [c (FlatContract a b)])
93+
(FlatContract (Syntaxof a) (Syntaxof b))]
94+
@defproc*[([(parameter/c [c (Contract a b)])
95+
(Contract (Parameter b) (Parameter b))]
96+
[(parameter/c [in-c (Contract a b)]
97+
[out-c (Contract c d)])
98+
(Contract (Parameter b d) (Parameter b d))])]
9999
@defproc[(symbols [sym Symbol] ...+)
100-
(Con Any Symbol)])]{
100+
(Contract Any Symbol)])]{
101101
These forms are typed versions of those found in Racket. They are otherwise
102102
the same.
103103
}
@@ -153,5 +153,5 @@ library is a work in progress.
153153
@item{Contract types do not have any contract compilation/runtime enforcement.}
154154
@item{Racket's built-in combinators for vectors, boxes, hashes are unsupported.}
155155
@item{Values that pass @racket[flat-contract?] are not necessarily members of
156-
the @racket[FlatCon] type: members of that type can be used in function
156+
the @racket[FlatContract] type: members of that type can be used in function
157157
position, but @racket[flat-contract?] returns true for non-predicates.}]

‎typed-racket-lib/typed-racket/base-env/base-types.rkt

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -199,5 +199,5 @@
199199

200200
[Continuation-Mark-Keyof (-poly (a) (make-Continuation-Mark-Keyof a))]
201201
[Prompt-Tagof (-poly (a b) (make-Prompt-Tagof a b))]
202-
[Con (-poly (a b) (make-Con a b))]
203-
[FlatCon (-poly (a b) (make-FlatCon a b))]
202+
[Contract (-poly (a b) (make-Contract a b))]
203+
[FlatContract (-poly (a b) (make-FlatContract a b))]

‎typed-racket-lib/typed-racket/base-env/contract-prims.rkt

Lines changed: 36 additions & 31 deletions
Original file line numberDiff line numberDiff line change
@@ -21,7 +21,12 @@
2121
;; syntax objects for surface-level types (e.g. Real instead of -Real)
2222
(base-env base-types base-types-extra)
2323
(prefix-in untyped: racket/contract/base))
24-
(provide ;; TODO: we don't support all of the p/c-item forms
24+
(provide and/c
25+
or/c
26+
list/c
27+
->/c
28+
->i
29+
;; TODO: we don't support all of the p/c-item forms
2530
;; (exists, struct, etc.), we really should provide our own
2631
;; versions of provide/contract and contract-out that give
2732
;; good "x is unsupported" messages
@@ -43,48 +48,48 @@
4348
untyped-ctc))) ...)]))
4449

4550
(define-contract
46-
[flat-named-contract (All (a b) (-> Any (FlatCon a b) (FlatCon a b)))]
47-
[any/c (FlatCon Any Any)]
48-
[none/c (FlatCon Any Any)]
49-
[not/c (All (a b) (-> (FlatCon a b) (FlatCon a a)))]
50-
[=/c (case-> (-> Natural (FlatCon Any Natural))
51-
(-> Integer (FlatCon Any Integer))
52-
(-> Real (FlatCon Any Real)))]
53-
[</c (-> Real (FlatCon Any Real))]
54-
[>/c (-> Real (FlatCon Any Real))]
55-
[<=/c (-> Real (FlatCon Any Real))]
56-
[>=/c (-> Real (FlatCon Any Real))]
57-
[between/c (-> Real Real (FlatCon Any Real))]
58-
[real-in (-> Real Real (FlatCon Any Real))]
51+
[flat-named-contract (All (a b) (-> Any (FlatContract a b) (FlatContract a b)))]
52+
[any/c (FlatContract Any Any)]
53+
[none/c (FlatContract Any Any)]
54+
[not/c (All (a b) (-> (FlatContract a b) (FlatContract a a)))]
55+
[=/c (case-> (-> Natural (FlatContract Any Natural))
56+
(-> Integer (FlatContract Any Integer))
57+
(-> Real (FlatContract Any Real)))]
58+
[</c (-> Real (FlatContract Any Real))]
59+
[>/c (-> Real (FlatContract Any Real))]
60+
[<=/c (-> Real (FlatContract Any Real))]
61+
[>=/c (-> Real (FlatContract Any Real))]
62+
[between/c (-> Real Real (FlatContract Any Real))]
63+
[real-in (-> Real Real (FlatContract Any Real))]
5964
[integer-in
60-
(case-> (-> Positive-Integer Integer (FlatCon Any Positive-Integer))
61-
(-> Natural Integer (FlatCon Any Natural))
62-
(-> Integer Integer (FlatCon Any Integer)))]
63-
[natural-number/c (FlatCon Any Natural)]
64-
[string-len/c (-> Real (FlatCon Any String))]
65-
[false/c (Con Any False)]
66-
[printable/c (FlatCon Any Any)]
65+
(case-> (-> Positive-Integer Integer (FlatContract Any Positive-Integer))
66+
(-> Natural Integer (FlatContract Any Natural))
67+
(-> Integer Integer (FlatContract Any Integer)))]
68+
[natural-number/c (FlatContract Any Natural)]
69+
[string-len/c (-> Real (FlatContract Any String))]
70+
[false/c (Contract Any False)]
71+
[printable/c (FlatContract Any Any)]
6772
;; one-of/c
6873
;; vectorof
6974
;; vector-immutableof (tricky, TR doesn't have immutable vectors)
7075
;; vector/c
7176
;; vector-immutable/c
7277
;; box/c
7378
;; box-immutable/c
74-
[listof (All (a b) (-> (Con a b) (Con (Listof a) (Listof b))))]
79+
[listof (All (a b) (-> (Contract a b) (Contract (Listof a) (Listof b))))]
7580
[non-empty-listof
76-
(All (a b) (-> (Con a b) (Con (Listof a) (Pairof b (Listof b)))))]
81+
(All (a b) (-> (Contract a b) (Contract (Listof a) (Pairof b (Listof b)))))]
7782
[list*of
78-
(All (a b) (-> (Con a b) (Con (Rec x (Pairof a (U a x)))
83+
(All (a b) (-> (Contract a b) (Contract (Rec x (Pairof a (U a x)))
7984
(Rec x (Pairof b (U b x))))))]
80-
[cons/c (All (a b c d) (-> (Con a b) (Con c d) (Con Any (Pairof b d))))]
85+
[cons/c (All (a b c d) (-> (Contract a b) (Contract c d) (Contract Any (Pairof b d))))]
8186
;; cons/dc
82-
[syntax/c (All (a b) (-> (FlatCon a b) (FlatCon (Syntaxof a) (Syntaxof b))))]
87+
[syntax/c (All (a b) (-> (FlatContract a b) (FlatContract (Syntaxof a) (Syntaxof b))))]
8388
;; struct/c
8489
;; struct/dc
8590
[parameter/c
86-
(All (a b c d) (case-> (-> (Con a b) (Con (Parameter b) (Parameter b)))
87-
(-> (Con a b) (Con c d) (Con (Parameter b d)
91+
(All (a b c d) (case-> (-> (Contract a b) (Contract (Parameter b) (Parameter b)))
92+
(-> (Contract a b) (Contract c d) (Contract (Parameter b d)
8893
(Parameter b d)))))]
8994
;; procedure-arity-includes/c
9095
;; hash/c
@@ -99,7 +104,7 @@
99104
;; promise/c
100105
;; flat-contract
101106
;; flat-contract-predicate
102-
[symbols (-> Symbol Symbol * (Con Any Symbol))])
107+
[symbols (-> Symbol Symbol * (Contract Any Symbol))])
103108

104109
(define-syntax (and/c stx)
105110
(syntax-parse stx
@@ -125,9 +130,9 @@
125130

126131
;; list/c needs its own type rule because giving it a function type outright
127132
;; wouldn't allow us to give e.g. (list/c exact-integer? positive?) a type like
128-
;; (Con (List Any Real) (List Integer Positive-Real)). The form is polyvariadic
133+
;; (Contract (List Any Real) (List Integer Positive-Real)). The form is polyvariadic
129134
;; but polydots is currently too weak, it won't let us give list/c a type like
130-
;; (All ((a b) ...) (-> (Con a b) ... (Con (List a ...) (List b ...)))).
135+
;; (All ((a b) ...) (-> (Contract a b) ... (Contract (List a ...) (List b ...)))).
131136
(define-syntax (list/c stx)
132137
(syntax-parse stx
133138
#:literals (list/c)

‎typed-racket-lib/typed-racket/env/init-envs.rkt

Lines changed: 4 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -331,10 +331,10 @@
331331
`(make-Distinction (quote ,nm)
332332
(quote ,id)
333333
,(type->sexp ty))]
334-
[(FlatCon: t1 t2)
335-
`(make-FlatCon ,(type->sexp t1) ,(type->sexp t2))]
336-
[(Con: t1 t2)
337-
`(make-Con ,(type->sexp t1) ,(type->sexp t2))]
334+
[(FlatContract: t1 t2)
335+
`(make-FlatContract ,(type->sexp t1) ,(type->sexp t2))]
336+
[(Contract: t1 t2)
337+
`(make-Contract ,(type->sexp t1) ,(type->sexp t2))]
338338
[(Value: v) `(make-Value (quote ,v))]
339339
;; Most Top types are in the predefined table, the ones here
340340
;; are not

‎typed-racket-lib/typed-racket/infer/infer-unit.rkt

Lines changed: 5 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -588,20 +588,20 @@
588588
[((Distinction: _ _ S) T)
589589
(cg S T obj)]
590590

591-
[((Con: S-pre S-post) (Con: T-pre T-post))
591+
[((Contract: S-pre S-post) (Contract: T-pre T-post))
592592
(% cset-meet (cg T-pre S-pre) (cg S-post T-post))]
593-
[((FlatCon: S-pre S-post) (FlatCon: T-pre T-post))
593+
[((FlatContract: S-pre S-post) (FlatContract: T-pre T-post))
594594
(% cset-meet (cg T-pre S-pre) (cg S-post T-post))]
595-
[((FlatCon: S-pre S-post) (Con: T-pre T-post))
595+
[((FlatContract: S-pre S-post) (Contract: T-pre T-post))
596596
(% cset-meet (cg T-pre S-pre) (cg S-post T-post))]
597597
[((and (PredicateProp: (PropSet: (TypeProp: _ S-post) _))
598598
(Fun: (list (Arrow: (list S-pre) _ _ _))))
599599
;; Apparently I can't just have the FlatCon case -- is the inference
600600
;; not aware of the subtyping relation?
601-
(Con*: T-pre T-post))
601+
(Contract*: T-pre T-post))
602602
(% cset-meet (cg T-pre S-pre) (cg S-post T-post))]
603603
[((Fun: (list (Arrow: (list S-pre) _ _ _)))
604-
(Con*: T-pre T-post))
604+
(Contract*: T-pre T-post))
605605
(% cset-meet (cg T-pre S-pre) (cg S-pre T-post))]
606606

607607
;; two structs with the same name

‎typed-racket-lib/typed-racket/infer/infer.rkt

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -6,7 +6,7 @@
66
define-values/invoke-unit/infer link
77
only))
88

9-
(provide-signature-elements intersect^ infer^)
9+
(provide-signature-elements intersect^ infer^ (only constraints^ meet join))
1010

1111
(define-values/invoke-unit/infer
1212
(link infer@ constraints@ dmap@ intersect@))

‎typed-racket-lib/typed-racket/rep/type-rep.rkt

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -1175,8 +1175,8 @@
11751175
(make-Distinction nm id ty))])
11761176

11771177
;; Contract type
1178-
(def-structural Con ([in-ty #:contravariant] [out-ty #:covariant]))
1179-
(def-structural FlatCon ([in-ty #:contravariant] [out-ty #:covariant]))
1178+
(def-structural Contract ([in-ty #:contravariant] [out-ty #:covariant]))
1179+
(def-structural FlatContract ([in-ty #:contravariant] [out-ty #:covariant]))
11801180

11811181
;;************************************************************
11821182
;; Type Variable tools (i.e. Abstraction/Instantiation)

0 commit comments

Comments
 (0)