{"action":"created","issue":{"url":"https://api.github.com/repos/josefs/Gradualizer/issues/122","repository_url":"https://api.github.com/repos/josefs/Gradualizer","labels_url":"https://api.github.com/repos/josefs/Gradualizer/issues/122/labels{/name}","comments_url":"https://api.github.com/repos/josefs/Gradualizer/issues/122/comments","events_url":"https://api.github.com/repos/josefs/Gradualizer/issues/122/events","html_url":"https://github.com/josefs/Gradualizer/issues/122","id":393774331,"node_id":"MDU6SXNzdWUzOTM3NzQzMzE=","number":122,"title":"Bounded quantification","user":{"login":"zuiderkwast","id":273886,"node_id":"MDQ6VXNlcjI3Mzg4Ng==","avatar_url":"https://avatars2.githubusercontent.com/u/273886?v=4","gravatar_id":"","url":"https://api.github.com/users/zuiderkwast","html_url":"https://github.com/zuiderkwast","followers_url":"https://api.github.com/users/zuiderkwast/followers","following_url":"https://api.github.com/users/zuiderkwast/following{/other_user}","gists_url":"https://api.github.com/users/zuiderkwast/gists{/gist_id}","starred_url":"https://api.github.com/users/zuiderkwast/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/zuiderkwast/subscriptions","organizations_url":"https://api.github.com/users/zuiderkwast/orgs","repos_url":"https://api.github.com/users/zuiderkwast/repos","events_url":"https://api.github.com/users/zuiderkwast/events{/privacy}","received_events_url":"https://api.github.com/users/zuiderkwast/received_events","type":"User","site_admin":false},"labels":[],"state":"open","locked":false,"assignee":null,"assignees":[],"milestone":null,"comments":3,"created_at":"2018-12-23T19:16:11Z","updated_at":"2018-12-28T15:41:44Z","closed_at":null,"author_association":"COLLABORATOR","body":"Picking up this topic from #93. I think we do already agree about these points:\r\n\r\n* Type variables are often used where the a type could just have been used directly.\r\n* For type variables appearing only once, bounded quantification doesn't make sense.\r\n* For type variables appearing only in the result, bounded quantification doesn't make sense.\r\n\r\nBut I think there are other cases where bounded quantification does make sense. I don't agree about this point:\r\n\r\n>>> [bounded quantification] is way too strict for variables occurring more than once\r\n\r\n>>  How so?\r\n\r\n> Would you really expect the function -spec foo([Y]) -> Y when Y :: number() to only type check when returning one of the numbers already in the list? No adding them up or multiplying them?\r\n\r\nYes, I do think it makes sense that `foo/1` above must return one of the elements in the list. For many of the lists functions, this is what you want. Here are some examples (with only-once used variables unfolded):\r\n\r\n```Erlang\r\n-spec lists:any(fun((T) -> boolean()), [T]) -> boolean().\r\n-spec lists:filter(fun((T) -> boolean()), [T]) -> [T].\r\n-spec lists:map(fun((A) -> B), [A]) -> [B].\r\n-spec lists:sort([T]) -> [T].\r\n```\r\n\r\nThese often have `when T :: term()` in the spec, which I think shouldn't make a difference.\r\n\r\nIf we just unfold, we get `[term()]` or `term()` as the return type of many of these functions, which gives rise to a type error where e.g. `integer()` is expected. Here are examples of applying these functions:\r\n\r\n```Erlang\r\n-spec integer_sort(integer()) -> integer().\r\ninteger_sort(Xs) -> lists:sort(Xs).\r\n\r\n-spec filter_even([integer()]) -> [integer()].\r\nfilter_even(Xs) -> lists:filter(fun (X) -> X rem 2 == 0 end, Xs).\r\n```\r\n\r\nI have a feeling that many of the remaining errors reported when gradualizing the gradualizer are from these, the errors involving `term()`. (Some specs are just wrong though, e.g. that of `lists:foldl/3` which always returns `term()`. These we can override.)\r\n\r\nSo, I suggest we go for bounded quantification where it makes sense, in a pragmatic way. What do you think?"},"comment":{"url":"https://api.github.com/repos/josefs/Gradualizer/issues/comments/450379049","html_url":"https://github.com/josefs/Gradualizer/issues/122#issuecomment-450379049","issue_url":"https://api.github.com/repos/josefs/Gradualizer/issues/122","id":450379049,"node_id":"MDEyOklzc3VlQ29tbWVudDQ1MDM3OTA0OQ==","user":{"login":"josefs","id":152020,"node_id":"MDQ6VXNlcjE1MjAyMA==","avatar_url":"https://avatars0.githubusercontent.com/u/152020?v=4","gravatar_id":"","url":"https://api.github.com/users/josefs","html_url":"https://github.com/josefs","followers_url":"https://api.github.com/users/josefs/followers","following_url":"https://api.github.com/users/josefs/following{/other_user}","gists_url":"https://api.github.com/users/josefs/gists{/gist_id}","starred_url":"https://api.github.com/users/josefs/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/josefs/subscriptions","organizations_url":"https://api.github.com/users/josefs/orgs","repos_url":"https://api.github.com/users/josefs/repos","events_url":"https://api.github.com/users/josefs/events{/privacy}","received_events_url":"https://api.github.com/users/josefs/received_events","type":"User","site_admin":false},"created_at":"2018-12-28T15:41:44Z","updated_at":"2018-12-28T15:41:44Z","author_association":"OWNER","body":"A few thoughts on handling flexible variables:\r\nI have already tried to pave the way for dealing with flexible variables.\r\n\r\n- The `constraints` module collects constraints on both rigid and flexible variables.\r\n- It also records all the flexible variables that have been generated.\r\n\r\nThe difficult part is to solve the constraints to eliminate the flexible variables. This has to be done after we've traversed the whole function.\r\n\r\nSolving the constraints would be simple if it wasn't for gradual types. Normally subtyping is transitive and if we have the case that `T1 <: A <: T2` (where `T1` and `T2` are concrete types and `A` is a flexible variable) then we can pick `A` to be a type between `T1` and `T2`. (There is sometimes a choice as to what type to pick but it's a solvable problem that's not relevant to the current discussion.)\r\n\r\nIn the presence of the `any()` then subtyping is not transitive anymore (because we don't want `integer() <: any()` and `any() <: boolean()` to imply `integer() <: boolean()`). So we cannot use transitivity anymore to solve constraints. That's a real bummer. What to do?\r\nI've been thinking that we should just go ahead and use transitivity anyway despite it not being correct. What would be the consequence of that? It would mean that we sometimes generate an error message when the code is actually well-typed. That is somewhat suboptimal but at least it is a way forward and I don't have any other suggestion how to do it. If you guys have a better idea I'm all ears."}}
{"actor":{"display_login":"josefs"}}