tag:blogger.com,1999:blog-11295132.post3930070047200672636..comments2024-02-24T01:46:31.188-08:00Comments on A Neighborhood of Infinity: The Three Projections of Doctor Futamurasigfpehttp://www.blogger.com/profile/08096190433222340957noreply@blogger.comBlogger25125tag:blogger.com,1999:blog-11295132.post-4923495644330397802011-02-02T19:22:04.687-08:002011-02-02T19:22:04.687-08:00I'm sorry to say but I believe I'm one of ...I'm sorry to say but I believe I'm one of those non-programmers whom you failed to explain the three projections to a level of understanding to. It did make my brain hurt a bit but I'll have to give you props for the effort.<br /><br />I do understand the GIGO (Garbage In Garbage Out) process but any internal processes prior to output is still a bit of a blur for me. Even trying to picture it out as a scene in the game incredible machines didn't do the trick.<br /><br />In any case, I will keep reading your blog for further comment exchange and resources until I get this. Thanks.Sonny O.http://www.sanyo-lcd.com/whats-new-my-z4000-sanyo-lcd-projector-reviewnoreply@blogger.comtag:blogger.com,1999:blog-11295132.post-7910263778112826602010-08-07T00:31:07.990-07:002010-08-07T00:31:07.990-07:00It looks like you guys are building some type of s...It looks like you guys are building some type of slot machine or something. I'm not sure I understand, is that what it is, a slot machine???Bobby Jamesonhttp://www.slotmachinesecretsrevealed.comnoreply@blogger.comtag:blogger.com,1999:blog-11295132.post-18477699413039832622010-07-14T11:38:29.788-07:002010-07-14T11:38:29.788-07:00The Google Books link to "Vicious Circles&quo...The Google Books link to "Vicious Circles" is broken. Could you post the title and author info? Thanks.solrizenoreply@blogger.comtag:blogger.com,1999:blog-11295132.post-64514926996160109742010-02-09T19:38:24.687-08:002010-02-09T19:38:24.687-08:00Dear Guy,
In the second diagram, under the heading...Dear Guy,<br />In the second diagram, under the heading "The First Projection", the type is still<br />type Specialiser a b c = (Pic ((a,b) -> c), a) -> Pic (b -> c)<br />where a = Pic(d). If you look at the top, you'll see the original machine takes a picture of a coin, which makes sense for coins but has no "program as data" connotation, possibly the source of your confusion. The diagrams are quite consistent.Zachary Vancehttps://www.blogger.com/profile/06055515765180704709noreply@blogger.comtag:blogger.com,1999:blog-11295132.post-80522319089069794322009-05-10T12:03:00.000-07:002009-05-10T12:03:00.000-07:00I had to follow to the Wikipedia link before I rea...I had to follow to the Wikipedia link before I read it properly and noticed it was Doctor <I>Futamura</I> rather than Doctor <I>Futurama.</I>I feel somewhat disappointed.Anonymousnoreply@blogger.comtag:blogger.com,1999:blog-11295132.post-25258189881900002942009-05-07T19:47:00.000-07:002009-05-07T19:47:00.000-07:00Peter Berry,
Thanks for your nice type analysis, ...Peter Berry,<br /><br />Thanks for your nice type analysis, and I think it illuminates the problem. In the sigfpe essay, the diagram under the heading "Specialisation" indeed corresponds to your type<br /><br />type Specialiser a b c = (Pic ((a,b) -> c), a) -> Pic (b -> c)<br /><br />But the next diagram, under the heading "The FIrst Projection", has a different type:<br /><br />type Specialiser a b c = (Pic ((a,b) -> c), Pic(a)) -> Pic (b -> c)<br /><br />and this is the type that I relied on when making my original criticism. So the best I can say now is that there does seem to be a slight type inconsistency somewhere.Guy Steelenoreply@blogger.comtag:blogger.com,1999:blog-11295132.post-45748601432146599572009-05-07T09:08:00.000-07:002009-05-07T09:08:00.000-07:00Peter,
If Pic were a comonad we'd have a func...Peter,<br /><br />If Pic were a comonad we'd have a function<br /><br />(a -> b) -> Pic a -> Pic b<br /><br />but we only have<br /><br />Pic (a -> b) -> Pic a -> Pic b<br /><br />The latter corresponds to the fact that we can draw a diagram for constructing a b by showing first how to make an a and then showing how to make a machine to transform an a into a b.sigfpehttps://www.blogger.com/profile/08096190433222340957noreply@blogger.comtag:blogger.com,1999:blog-11295132.post-30198425095453719712009-05-06T21:31:00.000-07:002009-05-06T21:31:00.000-07:00Guy, I see now I misread your criticism. But it's ...Guy, I see now I misread your criticism. But it's still a picture of a machine, not a picture of a picture of one, as you can see from the type.<br /><br />Dan, that's pretty interesting. Somehow I'd never thought of applying Curry-Howard to modal logic before. By 'very close to a comonad' do you mean 'looks like a comonad but I haven't proved it yet' or 'actually isn't a comonad'? Not that I have much of a grasp on just what a comonad is, mind.Peter Berryhttps://www.blogger.com/profile/08770230331776974807noreply@blogger.comtag:blogger.com,1999:blog-11295132.post-3623946464123389332009-05-06T15:51:00.000-07:002009-05-06T15:51:00.000-07:00Peter,
We can have a bit of fun with Pic. If we h...Peter,<br /><br />We can have a bit of fun with Pic. If we have a picture of an a, it tells us how to make an a. So we have a map<br /><br />Pic a -> a<br /><br />Now if we have an a, it's hard to make a picture of it, because it involves reverse engineering all of its internals. In fact, the machine might be booby trapped. So we have no map, in general, a -> Pic a. But we do have a map<br /><br />Pic a -> Pic (Pic a)<br /><br />because if you have a complete picture of an a there's nothing hidden that prevents you fully describing that in a higher order picture.<br /><br />So Pic is very close to a comonad. In fact, it's the modal operator from the S4 logic: http://www.cs.cmu.edu/~fp/talks/scottfest02.pdf (see p.16)<br /><br />So if I wasn't feeling so stupid I could probably turn the Futamura projection into something interesting in S4.sigfpehttps://www.blogger.com/profile/08096190433222340957noreply@blogger.comtag:blogger.com,1999:blog-11295132.post-10250579809674440722009-05-06T14:45:00.000-07:002009-05-06T14:45:00.000-07:00> {-# LANGUAGE EmptyDataDecls #-}
> data Pic...> {-# LANGUAGE EmptyDataDecls #-}<br />> data Pic a<br />> type Specialiser a b c = (Pic ((a,b) -> c), a) -> Pic (b -> c)<br />> <br />> specialise :: Specialiser a b c<br />> specialise = undefined<br />> <br />> spec_pic :: Pic (Specialiser a b c)<br />> spec_pic = undefined<br />> <br />> test = specialise (spec_pic, spec_pic)<br /><br />*Main> :t test<br />test :: Pic (Pic ((a, b) -> c) -> Pic (a -> Pic (b -> c)))<br /><br />test is the picture of X that you get by feeding the specialiser with two pictures of itself. So X is a machine that takes a picture of a machine - _not_ a picture of a picture of a machine.Peter Berryhttps://www.blogger.com/profile/08770230331776974807noreply@blogger.comtag:blogger.com,1999:blog-11295132.post-27210742107446077642009-05-06T09:29:00.000-07:002009-05-06T09:29:00.000-07:00Very nice! This blog entry is a delightful metaph...Very nice! This blog entry is a delightful metaphorical introduction to the concepts---I love the drawings---and seems to be technically sound. One very slight glitch: in the last two drawings, I believe that the right-hand input to the specializer should be not a picture of a machine, but a picture of a picture of a machine. This is a subtlety that is all too easy to gloss over.Guy Steelehttp://research.sun.com/people/noreply@blogger.comtag:blogger.com,1999:blog-11295132.post-52009898447024711202009-05-05T21:37:00.000-07:002009-05-05T21:37:00.000-07:00Partial evaluators that are not to be self applied...Partial evaluators that are not to be self applied are very useful too, but they don't tickle the imagination in the same way.<br /><br />In fact, I would almost claim that most of the commercial Haskell code I've written have been partial evaluators of one kind or another. But only one actually went by that name.augustsshttps://www.blogger.com/profile/07327620522294658036noreply@blogger.comtag:blogger.com,1999:blog-11295132.post-43232646757395847702009-05-05T11:23:00.000-07:002009-05-05T11:23:00.000-07:00augustss,
I'd expect it to be really hard. I can ...augustss,<br /><br />I'd expect it to be really hard. I can see that it'd be easy to specialise many kinds of purely numerical code, say, because you're just simplifying mathematical expressions. But specialising a piece of code that takes source code as input, and hence specialising all of the decisions made during the process of, say, parsing and interpreting that code, seems pretty scary to me.sigfpehttps://www.blogger.com/profile/08096190433222340957noreply@blogger.comtag:blogger.com,1999:blog-11295132.post-41930548718362138002009-05-05T10:34:00.000-07:002009-05-05T10:34:00.000-07:00Writing a specializer that actually does something...Writing a specializer that actually does something interesting when applied to itself is a really tricky. It took the DIKU group something like 10 years to figure out how.<br /><br />You can bypass some of the problems by writing cogen (the 3rd Futamura projection) by hand.augustsshttps://www.blogger.com/profile/07327620522294658036noreply@blogger.comtag:blogger.com,1999:blog-11295132.post-87696381625962861892009-05-05T07:21:00.000-07:002009-05-05T07:21:00.000-07:00Handwaving wildly, it seems like there ought to be...Handwaving wildly, it seems like there ought to be a topological problem here: if one curries f(stat,dyn) to f(stat)(dyn), then a specializer ought to produce f_stat(dyn). This is like saying that one can, instead of traversing two sides of a triangle, wind up at the same place by traversing the third. In some cases we can smoothly map a path from the first two sides to the third, in other cases -- particularly when the implementation is hardware based -- we run into an exponential blowup. Could it be useful to classify these situations into the presence or absence of the triangle "face"?Davenoreply@blogger.comtag:blogger.com,1999:blog-11295132.post-56217670567750323192009-05-05T02:45:00.000-07:002009-05-05T02:45:00.000-07:00FYI, I'm been working writing RenderMan Shader Lan...FYI, I'm been working writing RenderMan Shader Language compiler in Haskell with specialization facility.<br /><br />I believe shader specialization is killer application of Futamura projection.<br /><br />See my demo if you are interested in this field.<br /><br />http://vimeo.com/3294472syoyohttps://www.blogger.com/profile/15167076070732369617noreply@blogger.comtag:blogger.com,1999:blog-11295132.post-16637331899432075642009-05-04T19:36:00.000-07:002009-05-04T19:36:00.000-07:00It seems to me that there is a clear connection wi...It seems to me that there is a clear connection with reflective towers, e.g. as discussed in extraordinary detail in Lisp in Small Pieces, but I don't recall whether the latter (or anything else) examines the connection.<br /><br />As with reflective towers, mathematically it seems clear that the most natural theory actually does have not just a fourth projection, but actually an infinite number of projections (although one could axiomatically chop it short to suit one's tastes), but the connection of each level to some understandable concrete concepts seems questionable -- perhaps not unlike the general theory of N-Categories?<br /><br />That thought is not identical to Martijn's, but is similar in flavor.Doug Merrittnoreply@blogger.comtag:blogger.com,1999:blog-11295132.post-58957888482529130082009-05-04T09:40:00.000-07:002009-05-04T09:40:00.000-07:00Arnar,
I tried to avoid talking about multiple la...Arnar,<br /><br />I tried to avoid talking about multiple languages to make things easier to understand.<br /><br />But any individual specialiser is typically written in language A, takes an input to specialise written in language B, and outputs something in language C. (Or directly outputs executables rather than source.) It's now kinda fun to work out schemes for using combinations of specialisers to bootstrap specialisers from one language to another.<br /><br />You can also consider specialisers that only work with a subset of a language - for example a subset just big enough to write a specialiser. Or specialisers good enough to specialise an embedded DSL if not the full host language.sigfpehttps://www.blogger.com/profile/08096190433222340957noreply@blogger.comtag:blogger.com,1999:blog-11295132.post-60357771846849885912009-05-04T09:27:00.000-07:002009-05-04T09:27:00.000-07:00Sorry for a second comment, but what does the spec...Sorry for a second comment, but what does the specializer depend on? I.e. when we build a specializer (a partial evaluator) for a programming language, I imagine it depends on the programming language in question, right? Does it also depend on the target language?Arnar Birgissonhttps://www.blogger.com/profile/12073820949049315334noreply@blogger.comtag:blogger.com,1999:blog-11295132.post-71100936033101554432009-05-04T09:23:00.000-07:002009-05-04T09:23:00.000-07:00Excellent article, as usual. Although I do have a ...Excellent article, as usual. Although I do have a tiny bit of feeling that there is a even better analogy out there somewhere.Arnar Birgissonhttps://www.blogger.com/profile/12073820949049315334noreply@blogger.comtag:blogger.com,1999:blog-11295132.post-48932696368510508222009-05-04T09:19:00.000-07:002009-05-04T09:19:00.000-07:00Ah, yes, of course.
Anyhow, it's still the case t...Ah, yes, of course.<br /><br />Anyhow, it's still the case that your pedagogy breaks down in the particular case for machine language, when the description and the actual program is the same. It's a shame, because I think it's very clear otherwise.Josefhttps://www.blogger.com/profile/13272830598221833253noreply@blogger.comtag:blogger.com,1999:blog-11295132.post-48214946189423019402009-05-04T09:14:00.000-07:002009-05-04T09:14:00.000-07:00I wonder how many others read that as Futurama and...I wonder how many others read that as Futurama and thought of Dr. Zoidberg.Anonymousnoreply@blogger.comtag:blogger.com,1999:blog-11295132.post-1960384896269996532009-05-04T06:27:00.000-07:002009-05-04T06:27:00.000-07:00Josef,
Or you use one of the language changing sp...Josef,<br /><br />Or you use one of the language changing specialisers I mentioned - In particular one that targets assembly language.sigfpehttps://www.blogger.com/profile/08096190433222340957noreply@blogger.comtag:blogger.com,1999:blog-11295132.post-76123104491140149712009-05-04T05:16:00.000-07:002009-05-04T05:16:00.000-07:00Thanks for the post, I really like it.
I think it...Thanks for the post, I really like it.<br /><br />I think it's worth clarifying one thing though. You say "If we have a specialiser we never need to make a compiler again". Although it's technically correct it might be read as if we will never ever need a compiler as long as we have specialisers. But that's not true. A compiler is the only machine which turns a description of a machine into an actual machine. So it's not specialisers all the way down, we need a compiler at the bottom.Josefhttps://www.blogger.com/profile/13272830598221833253noreply@blogger.comtag:blogger.com,1999:blog-11295132.post-8842119535069021652009-05-04T00:20:00.000-07:002009-05-04T00:20:00.000-07:00That's really interesting.
I bet the higher proje...That's really interesting.<br /><br />I bet the higher projections are progressively harder to implement. Could it be that they are so hard to implement that they are not worth implementing anymore?Martijnhttps://www.blogger.com/profile/03420202886083056827noreply@blogger.com