{"action":"created","issue":{"url":"https://api.github.com/repos/idris-lang/Idris-dev/issues/2234","repository_url":"https://api.github.com/repos/idris-lang/Idris-dev","labels_url":"https://api.github.com/repos/idris-lang/Idris-dev/issues/2234/labels{/name}","comments_url":"https://api.github.com/repos/idris-lang/Idris-dev/issues/2234/comments","events_url":"https://api.github.com/repos/idris-lang/Idris-dev/issues/2234/events","html_url":"https://github.com/idris-lang/Idris-dev/issues/2234","id":73500039,"number":2234,"title":"Is this expected behavior of the partial evaluator?","user":{"login":"osa1","id":448274,"avatar_url":"https://avatars.githubusercontent.com/u/448274?v=3","gravatar_id":"","url":"https://api.github.com/users/osa1","html_url":"https://github.com/osa1","followers_url":"https://api.github.com/users/osa1/followers","following_url":"https://api.github.com/users/osa1/following{/other_user}","gists_url":"https://api.github.com/users/osa1/gists{/gist_id}","starred_url":"https://api.github.com/users/osa1/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/osa1/subscriptions","organizations_url":"https://api.github.com/users/osa1/orgs","repos_url":"https://api.github.com/users/osa1/repos","events_url":"https://api.github.com/users/osa1/events{/privacy}","received_events_url":"https://api.github.com/users/osa1/received_events","type":"User","site_admin":false},"labels":[{"url":"https://api.github.com/repos/idris-lang/Idris-dev/labels/F-Question","name":"F-Question","color":"bebe00"}],"state":"closed","locked":false,"assignee":null,"milestone":null,"comments":2,"created_at":"2015-05-06T03:20:29Z","updated_at":"2016-04-16T18:11:28Z","closed_at":"2016-04-16T18:11:28Z","body":"I've been playing with the partial evaluator lately and I realized this:\r\n\r\n```idris\r\n-- This is partially evaluated just fine...\r\nmy_pow_sd : [static] Nat -> Nat -> Nat\r\nmy_pow_sd x Z     = 1\r\nmy_pow_sd x (S k) = mult x (my_pow_sd x k)\r\n\r\n-- But this one is not evaluated partially evaluated no matter what. See f' below.\r\nmy_pow_ss : [static] Nat -> [static] Nat -> Nat\r\nmy_pow_ss x Z     = 1\r\nmy_pow_ss x (S k) = mult x (my_pow_ss x k)\r\n\r\n-- This is also not partially evaluated at all. See f'' below.\r\nmy_pow_ds : Nat -> [static] Nat -> Nat\r\nmy_pow_ds x Z     = 1\r\nmy_pow_ds x (S k) = mult x (my_pow_ds x k)\r\n```\r\n\r\nAlso, we need eta-expansion for partial evaluation here:\r\nDoesn't work: `f   = my_pow_sd 10`\r\nWorks: `f x = my_pow_sd 10 x`\r\n\r\nExamples:\r\n\r\nOK:\r\n```\r\n-- *Unlambda> :printdef f\r\n-- f : Nat -> Nat\r\n-- f x = PE_my_pow_28a53c2b (fromInteger 20)\r\n-- *Unlambda> :printdef PE_my_pow_28a53c2b\r\n-- PE_my_pow_28a53c2b : Nat -> Nat\r\n-- PE_my_pow_28a53c2b 0 = fromInteger 1\r\n-- PE_my_pow_28a53c2b (S k) = mult (fromInteger 10)\r\n--                                 (PE_my_pow_28a53c2b k)\r\n--\r\nf : Nat -> Nat\r\nf x = my_pow_sd 10 20\r\n```\r\n\r\nOK:\r\n\r\n```\r\n-- *Unlambda> :printdef f_ss\r\n-- f_ss : Nat -> Nat\r\n-- f_ss x = PE_my_pow_sd_28a53c2b x\r\n--\r\nf_ss : Nat -> Nat\r\nf_ss x = my_pow_sd 10 x\r\n```\r\n\r\nIsn't partially evaluated:\r\n\r\n```\r\n-- *Unlambda> :printdef f_eta\r\n-- f_eta : Nat -> Nat\r\n-- f_eta = my_pow_sd (fromInteger 10)\r\n--\r\n-- Not partially evaluated...\r\n--\r\nf_eta : Nat -> Nat\r\nf_eta = my_pow_sd 10\r\n```\r\n\r\nIsn't partially evaluated:\r\n```\r\n-- *Unlambda> :printdef f'\r\n-- f' : Nat -> Nat\r\n-- f' x = my_pow_ss (fromInteger 10) (fromInteger 20)\r\nf' : Nat -> Nat\r\nf' x = my_pow_ss 10 20\r\n```\r\n\r\nAlso isn't partially evaluated:\r\n\r\n```\r\n-- *Unlambda> :printdef f''\r\n-- f'' : Nat -> Nat\r\n-- f'' x = my_pow_ds (fromInteger 10) (fromInteger 20)\r\nf'' : Nat -> Nat\r\nf'' x = my_pow_ds 10 20\r\n```"},"comment":{"url":"https://api.github.com/repos/idris-lang/Idris-dev/issues/comments/210867631","html_url":"https://github.com/idris-lang/Idris-dev/issues/2234#issuecomment-210867631","issue_url":"https://api.github.com/repos/idris-lang/Idris-dev/issues/2234","id":210867631,"user":{"login":"ahmadsalim","id":1647846,"avatar_url":"https://avatars.githubusercontent.com/u/1647846?v=3","gravatar_id":"","url":"https://api.github.com/users/ahmadsalim","html_url":"https://github.com/ahmadsalim","followers_url":"https://api.github.com/users/ahmadsalim/followers","following_url":"https://api.github.com/users/ahmadsalim/following{/other_user}","gists_url":"https://api.github.com/users/ahmadsalim/gists{/gist_id}","starred_url":"https://api.github.com/users/ahmadsalim/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/ahmadsalim/subscriptions","organizations_url":"https://api.github.com/users/ahmadsalim/orgs","repos_url":"https://api.github.com/users/ahmadsalim/repos","events_url":"https://api.github.com/users/ahmadsalim/events{/privacy}","received_events_url":"https://api.github.com/users/ahmadsalim/received_events","type":"User","site_admin":false},"created_at":"2016-04-16T18:11:28Z","updated_at":"2016-04-16T18:11:28Z","body":"I will close this issue since the question seems to have been answered and there is no further action points."}}