{"action":"created","issue":{"url":"https://api.github.com/repos/racket/typed-racket/issues/420","repository_url":"https://api.github.com/repos/racket/typed-racket","labels_url":"https://api.github.com/repos/racket/typed-racket/issues/420/labels{/name}","comments_url":"https://api.github.com/repos/racket/typed-racket/issues/420/comments","events_url":"https://api.github.com/repos/racket/typed-racket/issues/420/events","html_url":"https://github.com/racket/typed-racket/pull/420","id":172800104,"number":420,"title":"WIP: Initial support for racket/contract in TR","user":{"login":"btlachance","id":1145862,"avatar_url":"https://avatars3.githubusercontent.com/u/1145862?v=4","gravatar_id":"","url":"https://api.github.com/users/btlachance","html_url":"https://github.com/btlachance","followers_url":"https://api.github.com/users/btlachance/followers","following_url":"https://api.github.com/users/btlachance/following{/other_user}","gists_url":"https://api.github.com/users/btlachance/gists{/gist_id}","starred_url":"https://api.github.com/users/btlachance/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/btlachance/subscriptions","organizations_url":"https://api.github.com/users/btlachance/orgs","repos_url":"https://api.github.com/users/btlachance/repos","events_url":"https://api.github.com/users/btlachance/events{/privacy}","received_events_url":"https://api.github.com/users/btlachance/received_events","type":"User","site_admin":false},"labels":[],"state":"open","locked":false,"assignee":{"login":"samth","id":244723,"avatar_url":"https://avatars1.githubusercontent.com/u/244723?v=4","gravatar_id":"","url":"https://api.github.com/users/samth","html_url":"https://github.com/samth","followers_url":"https://api.github.com/users/samth/followers","following_url":"https://api.github.com/users/samth/following{/other_user}","gists_url":"https://api.github.com/users/samth/gists{/gist_id}","starred_url":"https://api.github.com/users/samth/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/samth/subscriptions","organizations_url":"https://api.github.com/users/samth/orgs","repos_url":"https://api.github.com/users/samth/repos","events_url":"https://api.github.com/users/samth/events{/privacy}","received_events_url":"https://api.github.com/users/samth/received_events","type":"User","site_admin":false},"assignees":[{"login":"samth","id":244723,"avatar_url":"https://avatars1.githubusercontent.com/u/244723?v=4","gravatar_id":"","url":"https://api.github.com/users/samth","html_url":"https://github.com/samth","followers_url":"https://api.github.com/users/samth/followers","following_url":"https://api.github.com/users/samth/following{/other_user}","gists_url":"https://api.github.com/users/samth/gists{/gist_id}","starred_url":"https://api.github.com/users/samth/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/samth/subscriptions","organizations_url":"https://api.github.com/users/samth/orgs","repos_url":"https://api.github.com/users/samth/repos","events_url":"https://api.github.com/users/samth/events{/privacy}","received_events_url":"https://api.github.com/users/samth/received_events","type":"User","site_admin":false},{"login":"btlachance","id":1145862,"avatar_url":"https://avatars3.githubusercontent.com/u/1145862?v=4","gravatar_id":"","url":"https://api.github.com/users/btlachance","html_url":"https://github.com/btlachance","followers_url":"https://api.github.com/users/btlachance/followers","following_url":"https://api.github.com/users/btlachance/following{/other_user}","gists_url":"https://api.github.com/users/btlachance/gists{/gist_id}","starred_url":"https://api.github.com/users/btlachance/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/btlachance/subscriptions","organizations_url":"https://api.github.com/users/btlachance/orgs","repos_url":"https://api.github.com/users/btlachance/repos","events_url":"https://api.github.com/users/btlachance/events{/privacy}","received_events_url":"https://api.github.com/users/btlachance/received_events","type":"User","site_admin":false}],"milestone":null,"comments":5,"created_at":"2016-08-23T20:35:39Z","updated_at":"2017-12-06T18:38:29Z","closed_at":null,"author_association":"CONTRIBUTOR","pull_request":{"url":"https://api.github.com/repos/racket/typed-racket/pulls/420","html_url":"https://github.com/racket/typed-racket/pull/420","diff_url":"https://github.com/racket/typed-racket/pull/420.diff","patch_url":"https://github.com/racket/typed-racket/pull/420.patch"},"body":"This pull request implements initial support for using racket/contract in TR.\n## Type system from a high-level\n\nContracts in TR have two type arguments and are written as `(Con S T)`.\n\nThe first argument is the contract's input type, which specifies what it can\nmonitor. For example, using the function `positive?` as a contract would have\ninput type Real. You can think of the input type like the function's domain.\n\nThe second argument is the contract's output type, which indicates extra\ninformation we can conclude if the contract does not fail. For `positive?`, its\noutput type is `Positive-Real`. As you may have guessed, this information comes\nfrom the function type's propositions.\n\nThe entire contract type of `positive?` is `(Con Real Positive-Real)`.\n\nA function contract like `(->/c positive? positive?)` has a slightly more\ncomplicated type. By the domain contract's output type, we know the function\ncontract will only allow `Positive-Real`s to get through to the function.\nBecause the range contract can only monitor `Real`s, we know the function must\nproduce a `Real`. Thus, we say that the input type of the function contract is\n`(-> Positive-Real Real)`. We construct the output type of the function contract\nwith similar reasoning, and get that the entire type of the function contract is\n`(Con (-> Positive-Real Real) (-> Real Positive-Real))`.\n## What's supported?\n\nI mostly focused on the combinators found in the \"Data Structure Contracts\"\nsection of the docs, the function contract combinators `->` and `->i`,\n`provide/contract`, and `contract-out`.\n\nNotable missing forms:\n- `->*`\n- `unsupplied-arg?` and `the-unsupplied-arg` from `->i`\n- `struct/c`\n- struct, exists, and forall contract-out sub-forms\n- combinators for vectors, boxes, hashes\n- `any` range contract\n## Brief implementation details\n\nTyped contract forms are provided by contract-prims.rkt (a name that is\nannoyingly close to prims-contract.rkt). Most forms can be directly given a\ntype, e.g. `>/c` can be given a function type.\n\nOther combinator forms are a little more complicated. TR provides its own\nversion of these that annotate the surface syntax before delegating to the\nracket/contract's version of the form. After expansion, TR recovers the\nannotated pieces, typechecks those pieces, and uses that to calculate the type\nof the contract.\n\nOne particularly tricky part of the implementatation is that contract-out and\nprovide/contract generate transformers for the provided, contracted, bindings.\nWe want typed code with contracts on it to be able to go to untyped code.\nHowever, macros defined in TR are generally forbidden from doing so. These\nbindings are special-cased in tc-toplevel. I don't know what implications this\nhas on TR's invariants.\n\nAny sort of feedback is welcome---type system, implementation, comment prefix\nsyntax, etc.\n"},"comment":{"url":"https://api.github.com/repos/racket/typed-racket/issues/comments/349734125","html_url":"https://github.com/racket/typed-racket/pull/420#issuecomment-349734125","issue_url":"https://api.github.com/repos/racket/typed-racket/issues/420","id":349734125,"user":{"login":"mfelleisen","id":1571323,"avatar_url":"https://avatars2.githubusercontent.com/u/1571323?v=4","gravatar_id":"","url":"https://api.github.com/users/mfelleisen","html_url":"https://github.com/mfelleisen","followers_url":"https://api.github.com/users/mfelleisen/followers","following_url":"https://api.github.com/users/mfelleisen/following{/other_user}","gists_url":"https://api.github.com/users/mfelleisen/gists{/gist_id}","starred_url":"https://api.github.com/users/mfelleisen/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/mfelleisen/subscriptions","organizations_url":"https://api.github.com/users/mfelleisen/orgs","repos_url":"https://api.github.com/users/mfelleisen/repos","events_url":"https://api.github.com/users/mfelleisen/events{/privacy}","received_events_url":"https://api.github.com/users/mfelleisen/received_events","type":"User","site_admin":false},"created_at":"2017-12-06T18:38:29Z","updated_at":"2017-12-06T18:38:29Z","author_association":"NONE","body":"\nThat would be so cool. \n\n\n> On Dec 6, 2017, at 1:29 PM, Sam Tobin-Hochstadt <notifications@github.com> wrote:\n> \n> That sounds great, thanks!\n> \n> —\n> You are receiving this because you are subscribed to this thread.\n> Reply to this email directly, view it on GitHub, or mute the thread.\n> \n\n"}}
{"actor":{"display_login":"mfelleisen"}}