tag:blogger.com,1999:blog-6522986046288736604.post2011389356615639165..comments2024-03-19T03:39:24.263-07:00Comments on Everything in Context: Some classes of effectful programsChrishttp://www.blogger.com/profile/11607281981163980702noreply@blogger.comBlogger7125tag:blogger.com,1999:blog-6522986046288736604.post-66953610061995449412013-09-07T11:20:50.598-07:002013-09-07T11:20:50.598-07:00right - that one is non-monospace =right - that one is non-monospace =Chrishttps://www.blogger.com/profile/11607281981163980702noreply@blogger.comtag:blogger.com,1999:blog-6522986046288736604.post-16393461996399811082013-09-07T10:55:01.496-07:002013-09-07T10:55:01.496-07:00Oh, you _did_ mean `f(x) = x` to be the identity f...Oh, you _did_ mean `f(x) = x` to be the identity function. OK, I was confused because in the example following, you have `f(x) = (f(x); f(x))`, which looks like a meta-level equation.Lindsey Kuperhttps://www.blogger.com/profile/16008212366231583780noreply@blogger.comtag:blogger.com,1999:blog-6522986046288736604.post-13668590749831610322013-09-07T09:52:23.171-07:002013-09-07T09:52:23.171-07:00Oooh, that was maybe a bad notational choice on my...Oooh, that was maybe a bad notational choice on my part -- I was writing code in monospace font, which included some monospace "="s for function definition, and I was writing metalevel equations, in which bits of code were being related to other bits of code by /non/-monospace "=".<br /><br />For the specific example you mentioned, I did mean it to be the identity function, but also maybe should have made the point that "f(x) META-EQUALS x" no matter how many times we've called f(x) previously, which is what the term "referentially transparent" seems to emphasize. i didn't mean to suggest anything about the effects of evaluating the argument to the function in this case, though that's also an interesting line of inquiry.Chrishttps://www.blogger.com/profile/11607281981163980702noreply@blogger.comtag:blogger.com,1999:blog-6522986046288736604.post-63507504446365340732013-09-06T19:55:56.634-07:002013-09-06T19:55:56.634-07:00Thanks for this post, Chris! I understand the punc...Thanks for this post, Chris! I understand the punchline about what class 4 has to do with class 3, but I was confused by some of your notation. In your first example, you write `f(x) = x`. At first I thought that this was supposed to be a single effectless program (the identity function), but now I think that `=` is a meta-level thing and you're instead saying that `f(x)` and `x` are equal in the sense that a store `S` after `f(x)` is evaluated will be the same as store `S` is after `x` is evaluated. Is that right? If so, that definition is interesting because it allows for the possibility that the evaluation of `x` may perform effects, and so calling `f(x)` (which presumably would involve the evaluation of `x`) might too, but at least they are the same effects we'd get from merely evaluating `x`. But you have all this under the heading of "effectless programs", so am I misreading this?Lindsey Kuperhttps://www.blogger.com/profile/16008212366231583780noreply@blogger.comtag:blogger.com,1999:blog-6522986046288736604.post-72956556443832037482013-09-06T19:55:05.005-07:002013-09-06T19:55:05.005-07:00This comment has been removed by the author.Lindsey Kuperhttps://www.blogger.com/profile/16008212366231583780noreply@blogger.comtag:blogger.com,1999:blog-6522986046288736604.post-58791907867785766372013-09-06T19:35:47.964-07:002013-09-06T19:35:47.964-07:00Have you found the blog posts to be any more appro...Have you found the blog posts to be any more approachable than the papers? I recommend <a href="http://composition.al/blog/2013/01/18/a-ten-minute-talk-about-my-research/" rel="nofollow">this one</a>, followed by <a href="http://composition.al/blog/2013/05/25/how-to-read-from-an-lvar-an-illustrated-guide/" rel="nofollow">this one</a>!Lindsey Kuperhttps://www.blogger.com/profile/16008212366231583780noreply@blogger.comtag:blogger.com,1999:blog-6522986046288736604.post-72659294904113069942013-09-06T01:50:08.491-07:002013-09-06T01:50:08.491-07:00Hmm. A lot of the idea of "mapping out the e...Hmm. A lot of the idea of "mapping out the effects of state" seems strikingly similar to the work that Lindsey is doing. I confess that I have not read her papers yet (I heard of her work somewhat later than when her papers were in the introductory phase, which then resulted in me feeling hopelessly lost trying to understand it...), but your modeling of state transitions as linear implication makes me want to go back and reread that.<br /><br />Beyond that, interesting reading. Thanks for the insights!<br /><br />(Sigh. I can't comment as my livejournal self, because BlogSpot can't handle my account name having an underscore. Ugh.)Joshuahttps://www.blogger.com/profile/15663697470213886945noreply@blogger.com