{"action":"created","issue":{"url":"https://api.github.com/repos/idris-lang/Idris-dev/issues/3479","repository_url":"https://api.github.com/repos/idris-lang/Idris-dev","labels_url":"https://api.github.com/repos/idris-lang/Idris-dev/issues/3479/labels{/name}","comments_url":"https://api.github.com/repos/idris-lang/Idris-dev/issues/3479/comments","events_url":"https://api.github.com/repos/idris-lang/Idris-dev/issues/3479/events","html_url":"https://github.com/idris-lang/Idris-dev/issues/3479","id":181542229,"number":3479,"title":"No defined implementation Cast ty ty","user":{"login":"Termina1","id":815848,"avatar_url":"https://avatars.githubusercontent.com/u/815848?v=3","gravatar_id":"","url":"https://api.github.com/users/Termina1","html_url":"https://github.com/Termina1","followers_url":"https://api.github.com/users/Termina1/followers","following_url":"https://api.github.com/users/Termina1/following{/other_user}","gists_url":"https://api.github.com/users/Termina1/gists{/gist_id}","starred_url":"https://api.github.com/users/Termina1/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/Termina1/subscriptions","organizations_url":"https://api.github.com/users/Termina1/orgs","repos_url":"https://api.github.com/users/Termina1/repos","events_url":"https://api.github.com/users/Termina1/events{/privacy}","received_events_url":"https://api.github.com/users/Termina1/received_events","type":"User","site_admin":false},"labels":[],"state":"open","locked":false,"assignee":null,"assignees":[],"milestone":null,"comments":10,"created_at":"2016-10-06T22:32:50Z","updated_at":"2016-10-17T11:56:57Z","closed_at":null,"body":"For example, there is a code that does something like:\r\n```idris\r\nlet x : Integer = 10 in the Integer (cast x)\r\n```\r\nAnd I get error like:\r\n\r\n```\r\nCan't cast from Integer to Integer \r\n```\r\n\r\nWhich is strange, but we could solve this with this implementation:\r\n```idris\r\nCast ty ty where\r\n    cast = id \r\n```\r\nI encountered this problem while doing exercise for the book Type Driven Development with Idris.\r\nI need to implement Cast interface for some custom type.\r\n```idris\r\ndata Expr num = Val num\r\n              | Add (Expr num) (Expr num)\r\n              | Sub (Expr num) (Expr num)\r\n              | Mul (Expr num) (Expr num)\r\n              | Div (Expr num) (Expr num)\r\n              | Abs (Expr num)\r\neval : (Neg num, Integral num) => Expr num -> num\r\neval (Val x) = x\r\neval (Add x y) = eval x + eval y\r\neval (Sub x y) = eval x - eval y\r\neval (Mul x y) = eval x * eval y\r\neval (Div x y) = eval x `div` eval y\r\neval (Abs x) = abs (eval x)\r\n```\r\n\r\nI defined it as follows:\r\n\r\n```idris\r\n(Integral ty, Neg ty, Cast ty num) => Cast (Expr ty) num where\r\n    cast orig = cast (eval orig) \r\n```\r\nBut the test example from the book failed because of the reason I described earlier:\r\n\r\n```idris\r\nlet x : Expr Integer = 6 * 3 + 12 in the Integer (cast x) \r\n```\r\n\r\nAm I getting something wrong? Why casting from type ty to ty haven't been implemented as a part of standard library for idris?"},"comment":{"url":"https://api.github.com/repos/idris-lang/Idris-dev/issues/comments/254187237","html_url":"https://github.com/idris-lang/Idris-dev/issues/3479#issuecomment-254187237","issue_url":"https://api.github.com/repos/idris-lang/Idris-dev/issues/3479","id":254187237,"user":{"login":"melted","id":219997,"avatar_url":"https://avatars.githubusercontent.com/u/219997?v=3","gravatar_id":"","url":"https://api.github.com/users/melted","html_url":"https://github.com/melted","followers_url":"https://api.github.com/users/melted/followers","following_url":"https://api.github.com/users/melted/following{/other_user}","gists_url":"https://api.github.com/users/melted/gists{/gist_id}","starred_url":"https://api.github.com/users/melted/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/melted/subscriptions","organizations_url":"https://api.github.com/users/melted/orgs","repos_url":"https://api.github.com/users/melted/repos","events_url":"https://api.github.com/users/melted/events{/privacy}","received_events_url":"https://api.github.com/users/melted/received_events","type":"User","site_admin":false},"created_at":"2016-10-17T11:56:57Z","updated_at":"2016-10-17T11:56:57Z","body":"I think it makes sense to add it, there is only sensible way to do it and while it is a degenerate case those have tendency to be needed when one writes generic code. \n\n> 15 okt. 2016 kl. 20:30 skrev Melvar Chen <notifications@github.com>:\n> \n> That’s not what Cast is for; you’d use a dedicated IsString class. Just because you can cast from String to ty doesn’t make ty semantically a string type. (For example, Integer and Double.)\n> \n> To the best of my understanding, the only reason for Cast is to centralize conversion functions so you don’t need to remember a zillion names for conversion functions.\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"}}
{"actor":{"display_login":"melted"}}