{"action":"created","issue":{"url":"https://api.github.com/repos/stchang/typed-rosette/issues/10","repository_url":"https://api.github.com/repos/stchang/typed-rosette","labels_url":"https://api.github.com/repos/stchang/typed-rosette/issues/10/labels{/name}","comments_url":"https://api.github.com/repos/stchang/typed-rosette/issues/10/comments","events_url":"https://api.github.com/repos/stchang/typed-rosette/issues/10/events","html_url":"https://github.com/stchang/typed-rosette/issues/10","id":220002630,"number":10,"title":"Types for lifted functions that preserve concrete-ness","user":{"login":"AlexKnauth","id":6600123,"avatar_url":"https://avatars0.githubusercontent.com/u/6600123?v=4","gravatar_id":"","url":"https://api.github.com/users/AlexKnauth","html_url":"https://github.com/AlexKnauth","followers_url":"https://api.github.com/users/AlexKnauth/followers","following_url":"https://api.github.com/users/AlexKnauth/following{/other_user}","gists_url":"https://api.github.com/users/AlexKnauth/gists{/gist_id}","starred_url":"https://api.github.com/users/AlexKnauth/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/AlexKnauth/subscriptions","organizations_url":"https://api.github.com/users/AlexKnauth/orgs","repos_url":"https://api.github.com/users/AlexKnauth/repos","events_url":"https://api.github.com/users/AlexKnauth/events{/privacy}","received_events_url":"https://api.github.com/users/AlexKnauth/received_events","type":"User","site_admin":false},"labels":[],"state":"closed","locked":false,"assignee":null,"assignees":[],"milestone":null,"comments":6,"created_at":"2017-04-06T19:13:17Z","updated_at":"2018-02-08T20:25:27Z","closed_at":"2018-02-08T20:25:27Z","author_association":"COLLABORATOR","body":"Right now these types have to be represented as `Ccase->` types, and there is no way for the user to construct a new function with a `Ccase->` type. So there are two issues.\r\n\r\n* Should we stick with just `Ccase->` and accept that there are going to be a bunch of types which look like `(Ccase-> (C-> CA ... CB) (C-> A ... B))`, or should we implement some kind of \"concreteness polymorphism\" like `(∀/Symbolicness/Concreteness (X) (C-> (X A) ... (X B)))`?\r\n\r\n* We need to allow users to construct functions with these types. Adding `case-lambda` doesn't solve this. Most of these are cases where the same `body` needs to be type checked multiple times against different environments with different expected types:\r\n```racket\r\n[[a : CA] ... ⊢ body ⇐ CB]\r\n[[a : A] ... ⊢ body ⇐ B]\r\n```\r\n\r\nWe would probably end up doing something similar to this anyway for other `Ccase->` purposes, using a rule similar to what we already do for `#%app` of union functions. \r\n\r\nWould this be easier or harder with some notion of concreteness polymorphism? Or are we better off reusing the `Ccase->` rules?"},"comment":{"url":"https://api.github.com/repos/stchang/typed-rosette/issues/comments/364237533","html_url":"https://github.com/stchang/typed-rosette/issues/10#issuecomment-364237533","issue_url":"https://api.github.com/repos/stchang/typed-rosette/issues/10","id":364237533,"user":{"login":"stchang","id":28650,"avatar_url":"https://avatars0.githubusercontent.com/u/28650?v=4","gravatar_id":"","url":"https://api.github.com/users/stchang","html_url":"https://github.com/stchang","followers_url":"https://api.github.com/users/stchang/followers","following_url":"https://api.github.com/users/stchang/following{/other_user}","gists_url":"https://api.github.com/users/stchang/gists{/gist_id}","starred_url":"https://api.github.com/users/stchang/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/stchang/subscriptions","organizations_url":"https://api.github.com/users/stchang/orgs","repos_url":"https://api.github.com/users/stchang/repos","events_url":"https://api.github.com/users/stchang/events{/privacy}","received_events_url":"https://api.github.com/users/stchang/received_events","type":"User","site_admin":false},"created_at":"2018-02-08T20:25:27Z","updated_at":"2018-02-08T20:25:27Z","author_association":"OWNER","body":"https://github.com/stchang/typed-rosette/commit/ec6dc496890866267c83d09dfac1e1844d9df994"}}
{"actor":{"display_login":"stchang"}}