WIP: Initial support for racket/contract in TR #420

btlachance · 2016-08-23T20:35:39Z

This pull request implements initial support for using racket/contract in TR.

Type system from a high-level

Contracts in TR have two type arguments and are written as (Con S T).

The first argument is the contract's input type, which specifies what it can
monitor. For example, using the function positive? as a contract would have
input type Real. You can think of the input type like the function's domain.

The second argument is the contract's output type, which indicates extra
information we can conclude if the contract does not fail. For positive?, its
output type is Positive-Real. As you may have guessed, this information comes
from the function type's propositions.

The entire contract type of positive? is (Con Real Positive-Real).

A function contract like (->/c positive? positive?) has a slightly more
complicated type. By the domain contract's output type, we know the function
contract will only allow Positive-Reals to get through to the function.
Because the range contract can only monitor Reals, we know the function must
produce a Real. Thus, we say that the input type of the function contract is
(-> Positive-Real Real). We construct the output type of the function contract
with similar reasoning, and get that the entire type of the function contract is
(Con (-> Positive-Real Real) (-> Real Positive-Real)).

What's supported?

I mostly focused on the combinators found in the "Data Structure Contracts"
section of the docs, the function contract combinators -> and ->i,
provide/contract, and contract-out.

Notable missing forms:

->*
unsupplied-arg? and the-unsupplied-arg from ->i
struct/c
struct, exists, and forall contract-out sub-forms
combinators for vectors, boxes, hashes
any range contract

Brief implementation details

Typed contract forms are provided by contract-prims.rkt (a name that is
annoyingly close to prims-contract.rkt). Most forms can be directly given a
type, e.g. >/c can be given a function type.

Other combinator forms are a little more complicated. TR provides its own
version of these that annotate the surface syntax before delegating to the
racket/contract's version of the form. After expansion, TR recovers the
annotated pieces, typechecks those pieces, and uses that to calculate the type
of the contract.

One particularly tricky part of the implementatation is that contract-out and
provide/contract generate transformers for the provided, contracted, bindings.
We want typed code with contracts on it to be able to go to untyped code.
However, macros defined in TR are generally forbidden from doing so. These
bindings are special-cased in tc-toplevel. I don't know what implications this
has on TR's invariants.

Any sort of feedback is welcome---type system, implementation, comment prefix
syntax, etc.

btlachance · 2016-08-23T20:36:03Z

(Initially submitted as #417)

btlachance · 2016-08-24T23:49:22Z

Apart from the changes mentioned in #417, I don't think there's much blocking this on my end. (There's always cleanup to do, of course.)

Thoughts @samth @asumu?

samth · 2017-12-06T03:17:36Z

@btlachance My apologies for not reviewing this earlier. Do you have cycles to make it mergeable again? (if not, I'll take a look).

btlachance · 2017-12-06T18:25:05Z

@samth No worries, long ago I did say I would ping you more about this.

Anyhow, I can likely take a look this week but much more likely I can take a look this weekend. So as long as making it mergeable doesn't require dramatic effort, all that should be wrapped up by this time next week. How's that sound?

samth · 2017-12-06T18:29:36Z

That sounds great, thanks!

mfelleisen · 2017-12-06T18:38:29Z

That would be so cool.

…

On Dec 6, 2017, at 1:29 PM, Sam Tobin-Hochstadt ***@***.***> wrote: That sounds great, thanks! — You are receiving this because you are subscribed to this thread. Reply to this email directly, view it on GitHub, or mute the thread.

btlachance · 2017-12-14T05:18:09Z

So, where I'm currently at (480a676) merges cleanly but there are some lingering problems that my untrained eye can see. The biggest one though is typed contract tests that error like

--------------------
basic combinators > contract typechecking tests > 50 (listof string?)
ERROR

mask-accessor: contract violation
  expected: mask?
  given: '()
--------------------

when I raco test typed-racket-test/unit-tests/typed-contract-tests.rkt

My only guess is that I have something wrong in my type reps. Apart from that I have no clue.

@samth Any ideas?

Edit Pushed something new that should at least compile in the Travis build.

bennn · 2017-12-14T06:46:55Z

The reps look okay to me. I think if you added a #:mask (mask:unknown or anything else) you'd get the same error.

I have no idea where mask-accessor is defined. :(

samth · 2017-12-14T13:06:42Z

I think @pnwamk is the best person to answer that question, but I'll also take a look today.

btlachance · 2017-12-16T02:47:42Z

The tests that fail involving mask-accessor seem to have this in common: they involve combinators defined in in typed-racket/base-env/contract-prims.rkt with a function type.

But only some tests involving those combinators fail. The test with (=/c 13) passes but the one with (not/c even?) doesn't. (Focusing on the combinators, the test with (syntax/c (->/c any/c any/c)) is odd at least because it passes; but maybe it has to do with ->/c being a macro.) I'm still lost, but maybe somehow this can narrow the search.

pnwamk · 2017-12-22T19:10:26Z

I'll look into this (and hopefully report back with a solution) in the next day or so. Sorry for the delay.

pnwamk · 2017-12-22T19:26:48Z

typed-racket-lib/typed-racket/types/subtype.rkt

+   (match t2
+     [(Con: t2-pre t2-post)
+      (subtype-seq A
+                   (subtype* A t2-pre t1-pre obj)


During its expansion, subtype-seq adds an argument to the head of each operand list after the first expression (i.e. after the initial A), so you're passing two A values to subtype* here (and in other places).

Take a gander at other usages of subtype-seq in this file and you'll see they seem to mysteriously omit the first argument to subtype* usages in the body of the subtype-seq (because subtype-seq provides it).

I haven't built and tested this hypothesis, but it's almost certainly what is causing the mask-accessor issue you noticed.

The mask error says basically it expected a type (i.e. something with a mask struct property field -- defined here), but I got '() (i.e. an empty A argument in the incorrect subtype-seq usage).

i.e. it should read (assuming all the other details are correct):

(subtype-seq A (subtype* t2-pre t1-pre obj) (subtype* t1-post t2-post obj))

pnwamk · 2017-12-22T19:35:21Z

I'll give this PR a proper review sometime over the next couple days.

pnwamk · 2017-12-23T19:10:11Z

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

+         (base-env base-types base-types-extra)
+         (prefix-in untyped: racket/contract/base))
+(provide (except-out (all-defined-out)
+                     define-contract)


It might be nice to not use (all-defined-out), and instead make define-contract export each form, and then just manually export the other forms.

pnwamk · 2017-12-23T19:11:23Z

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

@@ -588,6 +588,24 @@
        [((Distinction: _ _ S) T)
         (cg S T obj)]

+        ;; XXX only barely noticed that cg takes an obj parameter
+        ;; halfway through the rebase


Does this "XXX ..." comment still need addressed? Removed?

pnwamk · 2017-12-23T19:16:00Z

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

+        [((Fun: (list (Arrow: (list S-pre) _ _ _)))
+          (Con*: T-pre T-post))
+         (% cset-meet (cg T-pre S-pre obj) (cg S-pre T-post obj))]
+


The obj parameter should only stay the same for recursive calls if the thing we're generating constraints for is the same.

i.e. when passing under a set-theoretic type constructor like U, we're still talking about the same value, so obj stays the same. However, if we're looking at some structural sub-compotent of the original thing (i.e. a field of a struct, the domain/range of a function, etc) then we're no longer looking at that same obj and so the argument should be #f (or just left off, since that's its default value).

I don't fully understand the Con types yet, but my suspicion at the moment is we're no longer generating constraints for obj when we're looking in the sub-components of a Con (though like I said, I don't "just get" them yet).

At any rate, the conservative (i.e. sound but not complete) thing to do is leave off the objs in these new cases, so maybe that's best for now?

pnwamk · 2017-12-23T19:18:16Z

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


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



I don't see any uses of meet or join in a quick search of this github diff page -- do we need to provide them?

Yup. They're used to check or/c in check-contract.rkt.

pnwamk · 2017-12-23T19:21:28Z

typed-racket-lib/typed-racket/types/pairwise-intersect.rkt

+(provide pairwise-intersect)
+
+(define (pairwise-intersect/arr s t)
+  (match* (s t)


We've moved away from arr as an abbreviation in TR's implementation due to some common ambiguities with what it stands for/implies/etc.

Would pairwise-intersect/arrow work?

pnwamk · 2017-12-23T19:22:34Z

typed-racket-lib/typed-racket/types/pairwise-intersect.rkt

+                 (pairwise-intersect s-rng t-rng))]
+    [(_ _)
+     (raise-arguments-error
+      'pairwise-intersect/arr


int-err raises internal TR errors (we usually use that or just omit an "else" match case.

pnwamk · 2017-12-23T19:22:54Z

typed-racket-lib/typed-racket/types/pairwise-intersect.rkt

+     (make-Keyword ks (pairwise-intersect ts tt) rs)]
+    [(_ _)
+     (raise-arguments-error
+      'pairwise-intersect/kw


same as above w.r.t. error raising

pnwamk · 2017-12-23T19:25:04Z

typed-racket-lib/typed-racket/types/pairwise-intersect.rkt

+     (make-NotTypeProp o (pairwise-intersect s t))]
+    [(_ _)
+     (raise-arguments-error
+      'pairwise-intersect/prop


This is a pretty limited set of props we support intersecting... is raising an error here the right thing? (i.e. won't this error be raised often? For example if one of the props is FalseProp, or an And or an Or, etc)

The errors probably aren't the right thing.

But here's some context: I initially implemented pairwise-intersect just to get a few examples working, and I thought raising an error might help me debug the cases I missed as I added more examples.

pnwamk · 2017-12-23T19:26:46Z

typed-racket-lib/typed-racket/types/pairwise-intersect.rkt

+;; Computes a lower bound of the two types w.r.t. the "precision order." The
+;; precision order is like the subtype order except that it does not account for
+;; variance. Effectively, this amounts to a fold over the two types in a uniform
+;; way. For base types (and, as a default, for unimplemented cases) this


Is there a brief thing we can insert here why we want to ignore variance? Why it's sound? etc (it seems a little concerning to just read that we're ignoring variance w/o knowing why)

I think the comment about ignoring variance shouldn't be there. I unfortunately don't have the theory worked out really well here, but I'll try to describe why I think the remark was misleading.

(First, maybe pairwise is the wrong modifier.. but bear with me) If we use p to refer to pairwise intersecting, then (a -> b) p (c -> d) is (a pc) -> (bp d). I've been assuming p is commutative, so for the domains a p c should be the same as c p a, and so it seems like variance shouldn't even be brought up.

pnwamk · 2017-12-23T19:27:15Z

typed-racket-lib/typed-racket/types/pairwise-intersect.rkt

+    [(u (Univ:)) u]
+    [((Fun: arr1s) (Fun: arr2s))
+     #:when (= (length arr1s) (length arr2s))
+     (make-Fun (map pairwise-intersect/arr arr1s arr2s))]


arr --> arrow

pnwamk · 2017-12-23T19:29:43Z

typed-racket-lib/typed-racket/types/pairwise-intersect.rkt

@@ -0,0 +1,121 @@
+#lang racket
+
+;; This module provides a function pairwise-intersect for calculating a lower


This file seems to raise a lot of errors instead of returning default results. Can you help me understand why?

There's no good reason why it explicitly raises errors, so I can change it to either return default results or I can drop the catch-all cases.

Repeating what I put in one of the other comments: I initially implemented pairwise-intersect just to get a few examples working, and I thought raising an error might help me debug the cases I missed as I added more examples.

pnwamk · 2017-12-23T19:30:06Z

typed-racket-lib/typed-racket/types/pairwise-intersect.rkt

+                    [(o1 (Empty:)) o1]
+                    [(o o) o]
+                    [(_ _)
+                     (raise-arguments-error


same -- is an error here the right thing?

pnwamk · 2017-12-23T19:33:05Z

typed-racket-lib/typed-racket/types/subtype.rkt

+      (subtype-seq A
+                   (subtype* A t2-pre t1-pre obj)
+                   (subtype* A t1-post t2-post obj))]
+     [_ (continue<: A t1 t2 obj)])]


The recursive calls to subtype* pass obj... but are we still talking about the same obj? If this is like recursively checking the domain and range of a function, those should not be obj but #f (or -empty-obj... I forget what the default "no object" value in this file is at the moment).

actually you can just leave off obj it looks like (it's an optional arg)

pnwamk · 2017-12-23T19:33:44Z

typed-racket-lib/typed-racket/types/subtype.rkt

+     [(FlatCon: t2-pre t2-post)
+      (subtype-seq A
+                   (subtype* A t2-pre t1-pre)
+                   (subtype* A t1-post t2-post))]


same issues w/ subtype-seq (i.e. erase the A's after each subtype* in the subtype-seq

pnwamk · 2017-12-23T19:33:49Z

typed-racket-lib/typed-racket/types/subtype.rkt

+     [(Con: t2-pre t2-post)
+      (subtype-seq A
+                   (subtype* A t2-pre t1-pre)
+                   (subtype* A t1-post t2-post))]


pnwamk · 2017-12-23T19:34:01Z

typed-racket-lib/typed-racket/types/subtype.rkt

+        [(ConFn*: t1-pre t1-post)
+         (subtype-seq A
+                      (subtype* A t2-pre t1-pre)
+                      (subtype* A t1-post t2-post))])]


pnwamk · 2017-12-23T19:34:41Z

typed-racket-lib/typed-racket/types/subtype.rkt

+           (Con: t2-pre t2-post))
+       _)
+      ;; XXX hacks
+      (match t1


XXX hacks, oh my! Um... either get rid of the hacks, or document the hacks? I don't know what this means, what the consequences are, etc.

pnwamk · 2017-12-23T19:36:25Z

typed-racket-lib/typed-racket/utils/contract-utils.rkt

+(define (confn-out ty) (cadr (confn-type-components ty)))
+;; confn-type-components : Type? -> #f or ConFnInfo
+;; Note: only gets components for functions with a single unary arr
+(define (confn-type-components ty)


arr -> arrow

pnwamk · 2017-12-23T19:37:17Z

typed-racket-lib/typed/racket/contract.rkt

+         ;; (except-out (all-from-out racket/contract) case-> ->* ->)
+         ;; (rename-out [case-> case->/c]
+         ;;             [->* ->*/c])
+         )


is this commented out code here for a reason?

pnwamk · 2017-12-23T19:39:12Z

Typed Racket seems to choose painfully verbose and clear in favor of cuteness and brevity in most cases. In light of that, would Contract be better than Con?

pnwamk · 2017-12-23T19:43:05Z

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

@@ -0,0 +1,156 @@
+#lang scribble/manual
+


I read the docs - I don't really understand how the new Con and FlatCon types are used, when they appear, etc. They don't seem to be in any of the examples explicitly.

pnwamk · 2017-12-23T19:46:12Z

It would be nice if there was a description (in this PR for sure, maybe also somewhere in the implementation) of why we need Con and FlatCon and why Racket's rich functions do not suffice. i.e. we can already write a pretty rich type for positive? (-> Real Boolean : Positive-Real) which seems to capture everything we might care about, so what is (Con Real Positive-Real) buying us?

pnwamk · 2017-12-23T19:47:08Z

I've reviewed and made comments. I'd still appreciate it if @samth took a detailed look at it at some point since he'll be able to better comment on some aspects.

btlachance · 2018-03-11T00:44:58Z

Thank you so much for taking a look, @pnwamk. I've been slowly making changes to address your feedback and I think the commits I just pushed to the PR address most of your remarks.

I might be misunderstanding how you imagine using TR's function types/propositions. So, if you have an idea in mind then I could try to respond. But without that, here's an attempt to justify why TR's function types/propositions aren't enough:

Contract application isn't the same thing as function application (and contract introduction isn't the same as function introduction).
If there were only first-order checks then reusing the function types might be kind of OK (though, not all of Racket's first-order contracts are functions). But since there are higher-order contracts, we need to make sure that contracts like (-> even? odd?) only get applied to functions that return Integer (because the return value flows through odd?). Similarly we need to make sure the result from applying that -> contract is only called with Integer arguments (because the argument flows through even?).

I added some examples to the documentation that at least give a drive-by for why contracts need their own type. (I adapted the examples from the intro of the ICFP 2002 paper on higher-order contracts.)

I'll respond to the inline remarks that I don't think the new commits address that well. If it helps in terms of the review process I'd be happy to respond to all of them, too.

Typechecking or/c (in check-contract) uses infer/meet.

Still missing good examples for the binary contract types

- Updated the signature for apply-contract (context-limit is a new arg); Made the pattern names consistent with the definition in racket/contract/private/base. - Updated the type for do-partial-app (it and source-location-source appear in contract-out's expansion)

btlachance · 2018-08-06T02:43:01Z

I believe I've now addressed all of the suggestions from Andrew's review, and everything should merge cleanly.

@samth @pnwamk Any further suggestions? Sorry for the extra round-trip if I did miss something---just let me know and I'll get on it.

pnwamk

I added a few more comments. Sorry if they're duplicates from previous discussions (I tried to search previous comments, but I could have missed some).

Also, this PR is based on some work that is summarized in a master's thesis... is that right?

Would it be useful to put a pointer to a semi-permanent URL with that thesis (e.g. https://arxiv.org/)?

pnwamk · 2018-08-07T13:40:03Z

typed-racket-lib/typed-racket/types/pairwise-intersect.rkt

+    [((TypeProp: o s) (TypeProp: o t))
+     (make-TypeProp o (pairwise-intersect s t))]
+    [((NotTypeProp: o s) (NotTypeProp: o t))
+     (make-NotTypeProp o (pairwise-intersect s t))]))


Is there an invariant that ensures pairwise-intersect/prop isn't called with a TypeProp and a NotTypeProp? Or that it's never called with a LeqProp and some other prop?

I ask because there's no case for handling these combinations. If those combinations arise... is that actually an internal error? Or... does that mean we need to return some conservative, sound default result?

pnwamk · 2018-08-07T13:45:10Z

typed-racket-lib/typed-racket/types/pairwise-intersect.rkt

+    [((Fun: arr1s) (Fun: arr2s))
+     #:when (= (length arr1s) (length arr2s))
+     (make-Fun (map pairwise-intersect/arrow arr1s arr2s))]
+    [((Result: ss pset-s o1) (Result: ts pset-t o2))


I can't help but be a little skeptical this is the right thing to do for functions in general (although I have not spent a lot of time thinking about this issue specifically, so maybe there's some obvious things I'm missing).

Why do two functions need the same number of arrows to be pairwise intersected? And why are we pairwise intersecting their arrows only in a pointwise fashion?

If this is right, maybe a comment as to why would be helpful for posterity's sake? If we're less confident, perhaps for now only support pairwise intersecting functions with a single arrow? Just a thought.

pnwamk · 2018-08-07T13:48:22Z

typed-racket-lib/typed-racket/types/pairwise-intersect.rkt

+                      dbound)]
+    [((Poly: vs b) _)
+     #:when (or (subtype s t) (subtype t s))
+     s]


It's neat that we can just check subtyping here. That makes me wonder, should pairwise-intersect start out with a subtype/subval/implies-atomic?/etc check up front before beginning to examine and recur into the specific types/propositions?

samth · 2019-12-17T22:40:52Z

See #833 as well.

samth self-assigned this Dec 6, 2017

samth assigned btlachance Dec 6, 2017

btlachance force-pushed the conTRacts' branch 2 times, most recently from fc7eb80 to d0b686c Compare December 14, 2017 05:14

bennn requested review from pnwamk and removed request for pnwamk December 14, 2017 06:47

btlachance force-pushed the conTRacts' branch from d0b686c to 480a676 Compare December 14, 2017 17:47

pnwamk reviewed Dec 22, 2017

View reviewed changes

pnwamk self-requested a review December 22, 2017 19:34

pnwamk reviewed Dec 23, 2017

View reviewed changes

samth added the in-progress label May 3, 2018

btlachance force-pushed the conTRacts' branch from addf780 to f1bcb3f Compare July 29, 2018 20:39

btlachance added 4 commits July 29, 2018 17:01

Initial support for racket/contract in TR

4cb2468

First pass of changes from PR review

945fb34

Clearer contract type names; Reexpose infer's meet/join

24252cf

Typechecking or/c (in check-contract) uses infer/meet.

Scribble example w/migrating contracts and contract types

8cc55e1

Still missing good examples for the binary contract types

btlachance force-pushed the conTRacts' branch from f1bcb3f to 8cc55e1 Compare July 29, 2018 21:15

btlachance added 2 commits July 30, 2018 08:45

Remove catch-all cases from pairwise-intersect

be055bd

pnwamk reviewed Aug 7, 2018

View reviewed changes


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

		@@ -0,0 +1,121 @@
		#lang racket

		;; This module provides a function pairwise-intersect for calculating a lower

WIP: Initial support for racket/contract in TR #420

Are you sure you want to change the base?

WIP: Initial support for racket/contract in TR #420

Conversation

btlachance commented Aug 23, 2016

Type system from a high-level

What's supported?

Brief implementation details

btlachance commented Aug 23, 2016

btlachance commented Aug 24, 2016

samth commented Dec 6, 2017

btlachance commented Dec 6, 2017

samth commented Dec 6, 2017

mfelleisen commented Dec 6, 2017 via email

btlachance commented Dec 14, 2017 • edited Loading

bennn commented Dec 14, 2017

samth commented Dec 14, 2017

btlachance commented Dec 16, 2017 • edited Loading

pnwamk commented Dec 22, 2017

pnwamk Dec 22, 2017 • edited Loading

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

pnwamk commented Dec 22, 2017

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

pnwamk Dec 23, 2017 • edited Loading

Choose a reason for hiding this comment

Choose a reason for hiding this comment

pnwamk commented Dec 23, 2017

Choose a reason for hiding this comment

pnwamk commented Dec 23, 2017

pnwamk commented Dec 23, 2017

btlachance commented Mar 11, 2018 • edited Loading

btlachance commented Aug 6, 2018 • edited Loading

pnwamk left a comment • edited Loading

Choose a reason for hiding this comment

Choose a reason for hiding this comment

pnwamk Aug 7, 2018 • edited Loading

Choose a reason for hiding this comment

Choose a reason for hiding this comment

samth commented Dec 17, 2019

btlachance commented Dec 14, 2017 •

edited

Loading

btlachance commented Dec 16, 2017 •

edited

Loading

pnwamk Dec 22, 2017 •

edited

Loading

pnwamk Dec 23, 2017 •

edited

Loading

btlachance commented Mar 11, 2018 •

edited

Loading

btlachance commented Aug 6, 2018 •

edited

Loading

pnwamk left a comment •

edited

Loading

pnwamk Aug 7, 2018 •

edited

Loading