diff --git a/rfcs/text/0000-basic-typed-contracts.md b/rfcs/text/0000-basic-typed-contracts.md new file mode 100644 index 000000000..1a1aaa133 --- /dev/null +++ b/rfcs/text/0000-basic-typed-contracts.md @@ -0,0 +1,275 @@ +- Feature Name: basic-typed-contracts +- Start Date: 2019-06-30 +- RFC PR: (leave this empty) +- Feature Commit(s): (leave this empty) + +# Summary + +Give TR typed analogues of the `racket/contract` module. This needs a +new type constructor, `Contract`, to support higher-order +contracts. And adding a `FlatContract` type constructor helps e.g. to +give a more precise type to combinators like `not/c`. + +(The MS thesis related to this work is on my personal page at Tufts +. I don't yet have +an arXiv link because I need to get my Scribble build working enough +to at least get the intermediate TeX out. + +Any mention of "the current implementation" refers to the pull request +at .) + +# Motivation + +Racket programmers use the contract forms provided by +`racket/contract` but there currently isn't a clear path for Typed +Racket programmers to do the same. Without those forms, enforcing +invariants outside of the type system's sweet spot is harder, and +migrating contract-using Racket programs to Typed Racket is harder. + +The current implementation supports most of the data structure +contracts in the contract documentation, and it also supports most of +`->i`, `->*`, and `contract-out`. (But the `struct/c` form isn't yet +supported, and things like the `struct` *contract-out-item* may need +special support from a TR version of `contract-out`). + +# Guide-level explanation + +## Basics/contracts over first-order types + +(Assumes a passing knowledge of Racket's contract library and TR's +propositions. In typed contracts, I write `->/c` for Racket's `->` +contract combinator.) + +Racket's contract system monitors how values flow through +contracts. Using those same contracts in Typed Racket means we'll need +to give typed values to the contract system, and so the type system +will have to ensure that those values are used appropriately. + +We can use typed functions as contracts. To properly use a typed +function, the type system has to ensure that the contract is only ever +used to monitor values that agree with the function's type. Being a +predicate on `Integer`s, we can use `even?` to monitor integers: + +`(contract even? -6 'pos 'neg)` +`(contract even? 6 'pos 'neg)` + +We can also combine typed functions using contract combinators like +`and/c`: + +`(contract (and/c even? positive?) 10 'pos 'neg)` + +When we combine contracts, we need to be careful that the combination +makes sense. But first we need to talk about the types of the +contracts *being* combined. We've already seen that we need to make +sure a function is only used as a contract to monitor values of the +right type. But one idiom in Racket is to write contracts like `(and/c +exact-integer? even?)`: Here, a (Racket) contract programmer uses the +`exact-integer?` test to guard that `even?` in their contract is only +applied to integers. Without the guard, `even?` might raise a runtime +error (its own contract violation) unrelated to the contract the +programmer wrote. To give types to these contracts, then, we need to +know that whatever comes out of the `exact-integer?` contract is safe +to flow into the `even?` contract. So in addition to needing to know +the types of values a contract can be used on, we also need to know +that what comes out of a contract is safe for some subsequent +contract, like in `and/c`. Typed Racket's propositions help us uncover +this last part. + +The two parts of a contract's type explain what the contract can be +used on and what comes out of the contract. For `exact-integer?`, its +function type says it can be used on `Any` and that it has a positive +proposition for `Integer`, thus it has contract type `(Contract Any +Integer)`. The type of `even?` is `(-> Integer Boolean)`, with no +propositions, and so it has contract type `(Contract Integer +Integer)`. We say that the first part of a contract's type is its +*input type* and that the second part of a contract's type is its +*output type*. For example, the input type of `exact-integer?` is +`Any` and its output type is `Integer`. + +Back to type checking the combined contract, `(and/c exact-integer? +even?)`. From the types above, we know that what comes out of +`exact-integer?` can safely go in to `even?`. And since everything +lines up, we take the the input type of the first contract type +(`Integer`) and the output type of the last contract (`Integer`) and +give the whole contract type `(Contract Any Integer)`. + +--- + +As another example, this is a contract for lists of positive numbers: + + (listof positive?) + +Since `positive?` has type `(-> Real Boolean : #:+ Positive-Real)`, +this list contract has type `(Contract (Listof Real) (Listof +Positive-Real))`. + +The `listof` combinator itself has type `(-> (Contract a b) (Contract +(Listof a) (Listof b)))`. (Maybe we could give it a more specific type +with `case->` so that when applied to a `FlatContract`, `listof` +returns a `FlatContract`.) + +## Contracts on higher-order types + +If a function only consumes and produces positive reals, a Racket +programmer might express that information using the contract `(->/c +positive? positive?)`. In Typed Racket, that same information could be +expressed with the type `(-> Positive-Real Positive-Real)`. So +although that exact contract might not make sense in a Typed Racket +program, we still want to give it a type---the path from Racket to +Typed Racket isn't always smooth so we might be able to help the +Racket programmer if we give a meaningful type to that contract. + +Starting with the function `positive?`, its type is `(-> Real +Boolean)` and it has a positive proposition for `Positive-Real`. So +based on what we saw in the previous section, it has the contract type +`(Contract Real Positive-Real)`. + +The function contract combinator `->/c` wraps whatever function it is +applied to, ensuring that a caller provides arguments that satisfy the +domain contract and that the function returns a result that satisfies +the range contract; Values flow from the caller through the domain +contract into the function, and out of the function and through the +range contract. + +This value flow is reflected in the type of a function contract. For +our `(->/c positive? positive?)` the type is + + (Contract (-> #|2|#Positive-Real #|3|#Real) + (-> #|1|#Real #|4|#Positive-Real)) + +In the output type of the contract, here a function type, the domain +type is `Real` (marked `#|1|#`). This is because after applying the +contract to a function, calling the result with a value will apply the +domain contract (with input type `Real`) to that value. If the value +passes the domain contract, we know it is a `Positive-Real` by the +domain contract's output type, which is reflected in the input type's +domain contract (marked `#|2|#`). This means that a function we apply +this contract to has to accept `Positive-Real` values. + +In the input type of the contract, the range of the type is `Real` +(marked `#|3|#`) because applying the contract to a function is only +allowed if that function returns a value that can flow through the +range contract (whose input type is `Real`). Finally, in the output +type of the contract the range type is `Positive-Real` (marked `#|4|#`) +because that's the output type of the range contract. This means that +if we apply this contract to a function, then the resuling function +returns at least a `Positive-Real` if it returns at all. + +# Reference-level explanation + +## Interaction with other features + +As far as I can tell contracts are mostly self-contained. Some +exceptions: + + - Predicates are subtypes of the `FlatContract` type. + + - Values of `FlatContract` type are not functions (`FlatContract` + currently corresponds to Racket's `flat-contract?` which is `#t` + for e.g. numbers) + + - Applying a function contract (with the current type rule for + contract application) combines the range type of the function + contract's output type with the range type of the function that + will be monitored. In the code this is called "pairwise + intersection" and in the thesis this is the `comb` operator. + +As far as subtyping goes, `(Contract S T)` and `(FlatContract S T)` is +contravariant in `S` and covariant in `T`. And a `FlatContract` type +is a subtype of a `Contract` type according to the same variance +conditions. + +## How the feature would be implemented + +The MS thesis linked up top gives type rules formalizing what I walked +through in the guide-level explanation. It also discuss some of the +implementation techniques used for macro-based combinators like `->i`. + +Adding the *types* to TR is just like adding other types: define new +type constructors with the proper variance, define aliases +(e.g. `FlatContract` as a union type), extend the parser/pretty +printer, and add cases to the subtyping procedure. + +## Corner cases + +Because I haven't worked out how to compile a contract type to a +contract for typed/untyped interaction, typed code can't let untyped +code use a value of contract type. At the moment I believe the current +implementation raises an error (maybe an internal one?) when providing +a value of contract type because I haven't defined a way to compile +those types to contracts. + +I haven't properly looked at how these contract types interact with +polymorphic types. I'll update the PR to reject polymorphic types that +appear in contracts and to reject functions like `null?` (which has a +polymorphic type) from being used like contracts. (This sounds tricky: +we want combinators like `listof` to have a function type where +possible, which currently relies on polymorphism, but we want to +reject attempts to construct a contract over polymorphic types. At any +rate, I'll try to reject this polymorphism corner case with a useful +error message.) + +# Drawbacks and Alternatives + +[drawbacks]: #drawbacks + +I don't see drawbacks in adding typed contracts themselves to Typed +Racket; I see a potential drawback to the type system I've proposed. + +The rule for contract application is complicated by the two-argument +`Contract` type, and it may not be worth the cognitive overhead. One +reason for the two type arguments is so that the type computed by the +`and/c` rule is not far from what you get from a sequence of contract +applications (i.e. the `and/c` rule is privileged, but with the two +type arguments it's not as privileged). But this may not be worth the +complexity. + +Using a unary type constructor would remove the whole notion of input +and output types, which could make for an easier type rule for the +`and/c` combinator and for the other combinators, too. + +# Prior art +[prior-art]: #prior-art + +I haven't seen a language that combines typed, higher-order contracts +and subtyping---the combination seems to be unique to bringing +Racket's contracts to Typed Racket. The current design is written up +in the MS thesis linked up top. + +The original higher-oder contract paper [ff-icfp2002] uses contract +types in a simply typed language, and that type system was also used +in some work around higher-oder assertions and Haskell +[hjl-flp2006]. The Haskell work supports polymorphism but doesn't have +subtyping. + +- [ff-icfp2002] Robert Bruce Findler and Matthias Felleisen. Contracts +for Higher-Order Functions. ICFP 2002 +- [hjl-flp2006] Ralf Hinze, Johan Jeuring, and Andres Löh. Typed +Contracts for Functional Programming. Functional and Logic +Programming, 2006. + +# Unresolved questions +[unresolved]: #unresolved-questions + +> What parts of the design do you expect to resolve through the RFC +> process before this gets merged? + +Whether the two-argument `Contract` type constructor and the +corresponding contract application rule is too complex + +> What parts of the design do you expect to resolve through the +> implementation of this feature before stabilization? + +Giving better error messages, simplifying tricky parts of the +implementation (assuming that's in scope for "parts of the design"; +e.g. recovering the dependency identifiers in a ->i contract from a +fully expanded program) + +> What related issues do you consider out of scope for this RFC that +> could be addressed in the future independently of the solution that +> comes out of this RFC? + +- Types for object contracts, unit contracts, parametric contracts + (i.e. `racket/contract/parametric`) + +- Typed/untyped interaction at contract types