{"action":"created","issue":{"url":"https://api.github.com/repos/racket/typed-racket/issues/138","labels_url":"https://api.github.com/repos/racket/typed-racket/issues/138/labels{/name}","comments_url":"https://api.github.com/repos/racket/typed-racket/issues/138/comments","events_url":"https://api.github.com/repos/racket/typed-racket/issues/138/events","html_url":"https://github.com/racket/typed-racket/issues/138","id":78194677,"number":138,"title":"Strengthen type for partition","user":{"login":"bennn","id":1731829,"avatar_url":"https://avatars.githubusercontent.com/u/1731829?v=3","gravatar_id":"","url":"https://api.github.com/users/bennn","html_url":"https://github.com/bennn","followers_url":"https://api.github.com/users/bennn/followers","following_url":"https://api.github.com/users/bennn/following{/other_user}","gists_url":"https://api.github.com/users/bennn/gists{/gist_id}","starred_url":"https://api.github.com/users/bennn/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/bennn/subscriptions","organizations_url":"https://api.github.com/users/bennn/orgs","repos_url":"https://api.github.com/users/bennn/repos","events_url":"https://api.github.com/users/bennn/events{/privacy}","received_events_url":"https://api.github.com/users/bennn/received_events","type":"User","site_admin":false},"labels":[],"state":"open","locked":false,"assignee":null,"milestone":null,"comments":1,"created_at":"2015-05-19T18:11:19Z","updated_at":"2015-05-19T18:52:50Z","closed_at":null,"body":"The current types for partition are:\r\n```\r\n(-> a Any) (Listof a) -> (values (Listof a) (Listof a))\r\n(-> Any Boolean : a) (Listof b) -> (values (Listof a) (Listof b))\r\n```\r\nThis second type is too weak. The type of the second list returned should express that the filter failed on all its elements. For example, I'd like this example to typecheck:\r\n\r\n```\r\n#lang typed/racket/base\r\n\r\n(require (only-in racket/list partition))\r\n\r\n(: xs (Listof (U Boolean Char)))\r\n(define xs '())\r\n\r\n(let-values: ([([bools : (Listof Boolean)]\r\n                [chars : (Listof Char)])\r\n               (partition boolean? xs)])\r\n  (void))\r\n```\r\n\r\n---\r\n\r\nI was hoping to make this change myself, but I don't know how to express the filter. The closest I've come up with is to change the type of partition to use a `not-filter`.\r\n```\r\n[partition                                                                      \r\n  (-poly (a b) (cl->* (-> (-> a Univ) (-lst a) (-values (list (-lst a) (-lst a))))\r\n               (-> (make-pred-ty a) (-lst b) (-values (list (-lst a) (-lst (-not-filter a (make-Path null (list 0 0)))))))))]\r\n```\r\nBut I doubt this compiles, and the `not-filter` should mention `b`.\r\n\r\nCan someone with more experience help me?\r\n"},"comment":{"url":"https://api.github.com/repos/racket/typed-racket/issues/comments/103630588","html_url":"https://github.com/racket/typed-racket/issues/138#issuecomment-103630588","issue_url":"https://api.github.com/repos/racket/typed-racket/issues/138","id":103630588,"user":{"login":"samth","id":244723,"avatar_url":"https://avatars.githubusercontent.com/u/244723?v=3","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},"created_at":"2015-05-19T18:52:50Z","updated_at":"2015-05-19T18:52:50Z","body":"I don't think we can do this currently, but it will be possible when @andmkent lands #45."}}