RFC for initial implementation of types for untyped contracts

[btlachance]

I'd appreciate any feedback you all have on the RFC.

As an FYI: When I read "guide-level explanation" in the RFC template, for some reason I thought the audience of the RFC might not just be other TR developers. So what I wrote might be more than what was actually wanted...

(The section "Reference-level explanation" is probably not detailed enough, but I'm having trouble figuring out what more needs to be said or what should be excerpted from another source.)

[samth]

This is great. I hope that @capfredf @pnwamk @bennn can offer thoughts as well.

[samth]

A few initial thoughts:

1. Can you given an example with a function contract and say what the result type is?
2. Can you say more about the status of dependent contracts?
3. Can you say how the FlatContract type is handled?

[btlachance]

(Should these go in the RFC?)

1. Can you given an example with a function contract and say what the result type is?

Sure, the contract (->/c positive-real? positive-real?) has type

(Contract (-> Positive-Real Real)
          (-> Real Positive-Real))

Another: (->/c (>/c 9) (between/c 0 99)) has type

(Contract (-> Real Any)
          (-> Any Real))

The type I'm using for >/c is (-> Real Real (FlatContract Any Real))

2. Can you say more about the status of dependent contracts?

The only dependent contract I have is ->i, and as far as I can tell the current implementation supports:

• mandatory and optional domain contracts, both the named and keyword variants
• #:rest contracts
• all variants of the pre- and post-condition contracts
• named single- and multi-value range contracts (i.e. the id+ctc variants in the contract docs)

Big things missing:

• The any range contract
• Thethe-unsupplied-arg and unsupplied-arg? values. Giving types to those shouldn't be hard, but it does make me question how unions and contract types should interact (needed to support conditionals that produce contracts, like in the ->i example that uses unsupplied-arg?).

And type-system wise: dependent function contracts just have a contract type with ordinary function types in the input and output positions.

3. Can you say how the FlatContract type is handled?

Single-argument function types are a subtype of FlatContract (which makes them a subtype of Contract). And a couple contract combinators (e.g. not/c) only allow FlatContract arguments. The domain of the predicate is the contract's input type, and the contract's output type is the predicate's positive proposition or the predicate's domain type if the proposition was trivial.

In the current implementation the function application code (tc-funapp.rkt) allows a FlatContract in operator position. This maybe isn't the right design choice since flat-contract? is true for things that aren't usable as functions; If more of the atomic types should be subtypes of FlatContract, then the funapp code should change.

[samth]

Adding the first two answers to the RFC would be good.

For the FlatContract type, I'm somewhat worried. Could we represent FlatContract as just a union of various types? And also add a specific type for the result of coerce-contract when it produces a flat contract, so that those can be applied?

[bennn]

Can the RFC explain why there aren't types for chaperone & impersonator contracts?

I like the 2-arg contract type. But why not use TR's prop syntax and have (Contract Any #:+ Integer)? Because it's a chore to write #:+ everywhere?

Allowing FlatContract as an operator sounds good. Maybe the error message can suggest adding contract-first-order-passes? for the edge cases.

[bennn]

This notation is a little confusing. How about (Contract (-> #|2|#Positive-Real #|3|#Real) ....) so that:

1. it's valid TR syntax
2. the labels always come first
3. the labels touch the names they belong to

[btlachance]

Good idea. Will update the RFC

[bennn]

Add quick examples for lists, structs, and/or vectors?

I'm guessing: functions are a great example because a function type has input & output. Other contract-types should be simpler, but it'd be nice to have that confirmed.

[btlachance]

I'll add a list example.

As far as structs go: No support yet for struct/c, and I might need to provide a variant of contract-out that does some additional checks; At the moment the PR just reprovides Racket's contract-out. I updated the RFC with notes about that.

For vectors, are you interested in mutable vectors specifically? or just any vector contract?

[bennn]

Mutable specifically

[btlachance]

Could we represent FlatContract as just a union of various types?

This is a great idea! I've only thought about this a little but I think using a union type for FlatContract is doable. Edit My first thought is that there would be a type definition (without Ben's syntax suggestion) like:

(define-type (FlatContract A B) (U Integer String (-> A Boolean : #:+ B)))

But it's not clear how to admit Integer as a subtype of (FlatContract Integer Integer) with just this definition. I guess this means I still need to extend the subtype rules with some of the atomic cases?

And also add a specific type for the result of coerce-contract when it produces a flat contract, so that those can be applied?

Is your thought that the "specific type" for the result should be a subtype of the FlatContract (union) type? Or does the specific type use some new type constructor?

[btlachance]

(I'll add these to the RFC too. But replying here first.)

Can the RFC explain why there aren't types for chaperone & impersonator contracts?

AFAIK there's no reason to not have them, it just wasn't part of the initial work. It was something we talked about eventually wanting though. After adding them, I think the Contract type could then just be defined as a union of flat, chaperone, and impersonator types.

I like the 2-arg contract type. But why not use TR's prop syntax and have (Contract Any #:+ Integer)? Because it's a chore to write #:+ everywhere?

No complaints here about the proposition syntax, but I haven't used it often enough in TR to have formed much of an opinion; We just never thought of it. But I like this idea a lot since the output type seems analagous to a proposition.

Since there is a default proposition for a function type, using the proposition syntax for contract types suggests I might need to figure out a sensible default there, too.

Allowing FlatContract as an operator sounds good. Maybe the error message can suggest adding contract-first-order-passes? for the edge cases.

I'm not sure how contract-first-order-passes? fits here---did you mean contract-first-order? I had forgotten about that operator, so at the very least I should get my head around how contract-first-order and coerce-contract differ at first-order types.

[bennn]

(btlachance) Since there is a default proposition for a function type, using the proposition syntax for contract types suggests I might need to figure out a sensible default there, too.

I wouldn't worry about the default for now, and just require #:+ everywhere.

(bennn) Allowing FlatContract as an operator sounds good. Maybe the error message can suggest adding contract-first-order-passes? for the edge cases.

(btlachance) I'm not sure how contract-first-order-passes? fits here---did you mean contract-first-order? I had forgotten about that operator, so at the very least I should get my head around how contract-first-order and coerce-contract differ at first-order types.

Either one:

> (contract-first-order-passes? 4 4)
#t
> ((contract-first-order 4) 4)
#t