From f0499ffd11e14ffd1c5e350a430854414c6e39e6 Mon Sep 17 00:00:00 2001 From: Andrew Kent Date: Mon, 17 Apr 2017 00:27:34 -0400 Subject: [PATCH] move refine and linear integer stuff in docs (#533) --- .../scribblings/reference/experimental.scrbl | 90 +++++++++++++++++++ .../scribblings/reference/types.scrbl | 82 ++--------------- 2 files changed, 98 insertions(+), 74 deletions(-) diff --git a/typed-racket-doc/typed-racket/scribblings/reference/experimental.scrbl b/typed-racket-doc/typed-racket/scribblings/reference/experimental.scrbl index b520db5c..7f508ac8 100644 --- a/typed-racket-doc/typed-racket/scribblings/reference/experimental.scrbl +++ b/typed-racket-doc/typed-racket/scribblings/reference/experimental.scrbl @@ -44,3 +44,93 @@ you want, so you shouldn't use @racket[make-predicate] with these types. (radians 0) (f (radians 0))] } + + + +@section{Refinements and Linear Integer Reasoning} + +Refinement types have been added to Typed Racket's core, but +Typed Racket does not yet have function types which allow +dependencies between argument types, limiting how useful +refinements are for now. Allowing argument dependencies +is on our `to do' list. + +@defform[#:literals (Refine : Top Bot ! and or when + unless if < <= = > >= car cdr + vector-length + *) + (Refine [id : type] proposition) + #:grammar + ([proposition Top + Bot + (: symbolic-object type) + (! symbolic-object type) + (and proposition ...) + (or proposition ...) + (when proposition proposition) + (unless proposition proposition) + (if proposition proposition proposition) + (linear-comp symbolic-object symbolic-object)] + [linear-comp < <= = >= >] + [symbolic-object exact-integer + linear-term + (+ linear-term linear-term ...)] + [linear-term symbolic-path + (* exact-integer symbolic-path)] + [symbolic-path id + (path-elem symbolic-path)] + [path-elem car + cdr + vector-length])]{@racket[(Refine [v : t] p)] is a + refinement of type @racket[t] with logical proposition + @racket[p], or in other words it describes any value + @racket[v] of type @racket[t] for which the logical + proposition @racket[p] holds. + + @ex[(ann 42 (Refine [n : Integer] (= n 42)))] + + Note: The identifier in a refinement type is in scope + inside the proposition, but not the type. + +} + + +@racket[(: o t)] used as a proposition holds when symbolic object @racket[o] +is of type @racket[t.] + +@defform[(! sym-obj type)]{This is the dual of @racket[(: o t)], holding +when @racket[o] is not of type @racket[t].} + +Propositions can also describe linear inequalities (e.g. @racket[(<= x 42)] +holds when @racket[x] is less than or equal to @racket[42]), using any +of the following relations: @racket[<=], @racket[<], @racket[=], +@racket[>=], @racket[>]. + +The following logical combinators hold as one would expect +depending on which of their subcomponents hold hold: +@racket[and], @racket[or], @racket[if], @racket[not]. + +@racket[(when p q)] is equivalent to @racket[(or (not p) (and p q))]. + +@racket[(unless p q)] is equivalent to @racket[(or p q)]. + +Typed Racket's linear integer reasoning is turned off by +default. If you want to activate it, you must add the +@racket[#:with-linear-integer-arithmetic] keyword when +specifying the language of your program: + + +@racketmod[typed/racket #:with-linear-integer-arithmetic] + + +With this language option on, code such as the following +will type check: + +@racketblock[(if (< 5 4) + (+ "Luke," "I am your father") + "that's impossible!")] + +i.e. with linear integer reasoning enabled, Typed Racket +detects that the comparison is guaranteed to produce +@racket[#f], and thus the clearly ill-typed `then'-branch is +ignored by the type checker since it is guaranteed to be +dead code. diff --git a/typed-racket-doc/typed-racket/scribblings/reference/types.scrbl b/typed-racket-doc/typed-racket/scribblings/reference/types.scrbl index 0ddba37e..895a71c3 100644 --- a/typed-racket-doc/typed-racket/scribblings/reference/types.scrbl +++ b/typed-racket-doc/typed-racket/scribblings/reference/types.scrbl @@ -717,6 +717,13 @@ functions and continuation mark functions. contract combinator, but with types instead of contracts. } +@deftogether[( +@defidform[Top] +@defidform[Bot])]{ These are propositions that can be used with @racket[->]. + @racket[Top] is the propositions with no information. + @racket[Bot] is the propositions which means the result cannot happen. +} + @defidform[Procedure]{is the supertype of all function types. The @racket[Procedure] type corresponds to values that satisfy the @racket[procedure?] predicate. @@ -816,89 +823,16 @@ this top type. #s((salad food 1) "quinoa" "EVOO" salad))] } - @defalias[Union U] @defalias[Intersection ∩] @defalias[→ ->] @defalias[case→ case->] @defalias[∀ All] - -@section{Logical Refinements and Propositions} - - -@defform[#:literals (Refine : Top Bot ! and or when - unless if < <= = > >= car cdr - vector-length + *) - (Refine [id : type] proposition) - #:grammar - ([proposition Top - Bot - (: symbolic-object type) - (! symbolic-object type) - (and proposition ...) - (or proposition ...) - (when proposition proposition) - (unless proposition proposition) - (if proposition proposition proposition) - (linear-comp symbolic-object symbolic-object)] - [linear-comp < <= = >= >] - [symbolic-object exact-integer - linear-term - (+ linear-term linear-term ...)] - [linear-term symbolic-path - (* exact-integer symbolic-path)] - [symbolic-path id - (path-elem symbolic-path)] - [path-elem car - cdr - vector-length])]{@racket[(Refine [v : t] p)] is a - refinement of type @racket[t] with logical proposition - @racket[p], or in other words it describes any value - @racket[v] of type @racket[t] for which the logical - proposition @racket[p] holds. - - @ex[(ann 42 (Refine [n : Integer] (= n 42)))] - - Note: The identifier in a refinement type is in scope - inside the proposition, but not the type. - -} - -@deftogether[( -@defidform[Top] -@defidform[Bot])]{ These are propositions that can be used with - @racket[->] and @racket[Refine]. - @racket[Top] is the proposition with no information (i.e. the trivially true - proposition). - @racket[Bot] is the propositions which means the result cannot happen - (i.e. the impossible proposition). -} - -@racket[(: o t)] used as a proposition holds when symbolic object @racket[o] -is of type @racket[t.] - -@defform[(! sym-obj type)]{This is the dual of @racket[(: o t)], holding -when @racket[o] is not of type @racket[t].} - -Propositions can also describe linear inequalities (e.g. @racket[(<= x 42)] -holds when @racket[x] is less than or equal to @racket[42]), using any -of the following relations: @racket[<=], @racket[<], @racket[=], -@racket[>=], @racket[>]. - -The following logical combinators hold as one would expect -depending on which of their subcomponents hold hold: -@racket[and], @racket[or], @racket[if], @racket[not]. - -@racket[(when p q)] is equivalent to @racket[(or (not p) (and p q))]. - -@racket[(unless p q)] is equivalent to @racket[(or p q)]. - - @section{Other Types} @defform[(Option t)]{Either @racket[t] or @racket[#f]} @defform[(Opaque t)]{A type constructed using the @racket[#:opaque] clause of @racket[require/typed].} -@(close-eval the-eval) +@(close-eval the-eval) \ No newline at end of file