tag:blogger.com,1999:blog-7068528325708136131.post7804041610439237362..comments2024-03-01T21:25:21.218-08:00Comments on Structural insight: The trouble with monadsJohn Shutthttp://www.blogger.com/profile/00041398073010099077noreply@blogger.comBlogger15125tag:blogger.com,1999:blog-7068528325708136131.post-23018588779661111082016-10-25T16:12:13.647-07:002016-10-25T16:12:13.647-07:00'Fraid I don't follow that analogy.
It se...'Fraid I don't follow that analogy.<br /><br />It seems the tree we're discussing is that of dynamic extents; in Kernel some of its nodes are protected by guarded continuations.John Shutthttps://www.blogger.com/profile/00041398073010099077noreply@blogger.comtag:blogger.com,1999:blog-7068528325708136131.post-90340995827483886372016-10-20T06:27:02.086-07:002016-10-20T06:27:02.086-07:00If I imagine a program to be a tree...then, given ...If I imagine a program to be a tree...then, given my amateur understanding of this, operatives would correspond to xylem and applicatives to phloem. Photosynthesis would correspond to the wrapping and unwrapping of applicatives; the "wood" in the interior of the tree, to operatives that operate like macros or special forms; the bark and the buds, to that part of the program generated by $lambda. <br /><br />How am I doing? :D Unknownhttps://www.blogger.com/profile/17416989034140981385noreply@blogger.comtag:blogger.com,1999:blog-7068528325708136131.post-14625508890177389032016-10-19T09:44:28.470-07:002016-10-19T09:44:28.470-07:00I generally avoided the words "function"...I generally avoided the words "function" and "procedure" for Kernel and vau-calculus, because they get used in different ways. The alternative word was "combiner". Combiners are either "applicative" or "operative"; an applicative is a wrapper around some other combiner, and applying an applicative causes its operands to be evaluated to arguments, and the arguments are then passed to whatever combiner underlies the applicative (most often, an operative). Hence the title of my dissertation "Fexprs as the basis of Lisp function application". Ordinary Scheme procedures are applicatives whose underlying combiners are operatives.John Shutthttps://www.blogger.com/profile/00041398073010099077noreply@blogger.comtag:blogger.com,1999:blog-7068528325708136131.post-31095442190608516772016-10-18T19:46:22.569-07:002016-10-18T19:46:22.569-07:00So, anything derived--directly or indirectly--from...So, anything derived--directly or indirectly--from $vau is a fexpr...<br /><br />You won't just be inheriting from function definitions, you'll be inheriting from individual function calls. <br /><br />That is very interesting.Unknownhttps://www.blogger.com/profile/17416989034140981385noreply@blogger.comtag:blogger.com,1999:blog-7068528325708136131.post-7431551569399593162016-10-18T19:34:55.897-07:002016-10-18T19:34:55.897-07:00Point blank: Are all functions fexprs in vau calc...Point blank: Are all functions fexprs in vau calculus? <br /><br />* If so, why is the fact so obscure, even among your blog readers? <br />* If not, which functions are truly plain old Scheme procedures and nothing more?<br /><br /><br /><br />Unknownhttps://www.blogger.com/profile/17416989034140981385noreply@blogger.comtag:blogger.com,1999:blog-7068528325708136131.post-4562359024697978542016-10-18T18:54:25.935-07:002016-10-18T18:54:25.935-07:00Point blank: Are all functions fexprs in vau calc...Point blank: Are all functions fexprs in vau calculus? <br /><br />* If so, why is the fact so obscure, even among your blog readers? <br />* If not, which functions are truly plain old Scheme procedures and nothing more?<br /><br /><br /><br />Unknownhttps://www.blogger.com/profile/17416989034140981385noreply@blogger.comtag:blogger.com,1999:blog-7068528325708136131.post-90331323778263583422016-10-18T18:34:34.148-07:002016-10-18T18:34:34.148-07:00Inheritance/synthesis here is the same sort of ide...Inheritance/synthesis here is the same sort of idea as in RAGs, yes. Inheritance is where stuff is passed into a called function, so yes, that would be the point in vau-calculus where beta-substitution occurs.John Shutthttps://www.blogger.com/profile/00041398073010099077noreply@blogger.comtag:blogger.com,1999:blog-7068528325708136131.post-72672286708049388762016-10-18T16:26:58.611-07:002016-10-18T16:26:58.611-07:00When you talk about synthesis and inheritance, tow...When you talk about synthesis and inheritance, toward the end of this post, are you referring back to the use of these terms in your master's thesis (i.e., RAGs)? If you used this with Kernel--with fexprs--would the inheritance occur at the point in function call where beta substitution is taking place (after evaluation of all arguments has occurred? I'm still trying to wrap my head around the fexprs-as-abstractions-in-lambda-calculus idea. I haven't found anything much like it outside of your writings.<br /><br /> Unknownhttps://www.blogger.com/profile/17416989034140981385noreply@blogger.comtag:blogger.com,1999:blog-7068528325708136131.post-89918622564164690502011-12-26T09:23:02.646-08:002011-12-26T09:23:02.646-08:00It does not 'break abstractions' to contro...It does not 'break abstractions' to control effects as part of abstraction. I disagree with your argument that preventing easy addition of a diagnostic message is `what goes wrong`. But I do have <a href="http://lambda-the-ultimate.org/node/4357#comment-67178" rel="nofollow">my own objections</a> to purity due to concerns with composition. <br /><br />Functions can be defined independently of a monad by generic programming techniques. I.e. instead of writing a program for monad Foo, we can write a function for typeclass (FooFeature m). This seems to undermine your complaint of `hardcoded` type signatures. It also fits a role for inheritance.<br /><br />I prefer a capability-secure but effectful model. Inheritance and synthesis can both be modeled by representing records of capabilities. <a href="http://lambda-the-ultimate.org/node/2993" rel="nofollow">Purity can be modeled</a> by isolation.Anonymousnoreply@blogger.comtag:blogger.com,1999:blog-7068528325708136131.post-17397021127425520712011-12-18T15:37:54.564-08:002011-12-18T15:37:54.564-08:00I looked at monads years ago and concluded that un...I looked at monads years ago and concluded that uniqueness types were a better way of handling I/O and other stateful behaviors; more natural and straightforward.<br /><br />But uniqueness types still require that intermediate functions (or predicates or combiners) adapt to the state being passed around, though in a more natural way.<br /><br />Nowadays I have hopes for a model that combines immutability with signals that fake mutability in a controllable way (Conceptually. Under the hood the relation is reversed for optimization; mutability is used to fake signals when possible). Signals don't need the co-operation of intermediate code, they are between objects. They should be blockable, though. I blogged a bit about that, http://tehom-blog.blogspot.com/2011/10/mutability-and-signals.html and http://tehom-blog.blogspot.com/2011/12/signals-continuations-and-constraint.htmlTehomhttps://www.blogger.com/profile/14836581076251384864noreply@blogger.comtag:blogger.com,1999:blog-7068528325708136131.post-8918030275038325872011-12-09T20:13:48.761-08:002011-12-09T20:13:48.761-08:00The grammatical structure must be harder to follow...The grammatical structure must be harder to follow than I'd hoped. I did mean to write it that way. The tail of the sentence is meant to distribute over both: 'domain category from which, and codomain category to which, the heterogeneous morphisms of the adjunction go'.John Shutthttps://www.blogger.com/profile/00041398073010099077noreply@blogger.comtag:blogger.com,1999:blog-7068528325708136131.post-20043528365494564942011-12-09T15:00:14.387-08:002011-12-09T15:00:14.387-08:00Minor note - looks like there's a couple words...Minor note - looks like there's a couple words missing in the 4th paragraph under Bigness:<br /><br /> >called the domain category *(from which)* and codomain category (to which the heterogeneous morphisms of the adjunction go).Nick Knowlsonhttps://www.blogger.com/profile/06096511832465887288noreply@blogger.comtag:blogger.com,1999:blog-7068528325708136131.post-10868887424776974932011-12-09T14:34:48.449-08:002011-12-09T14:34:48.449-08:00gasche — It's interesting you say the example ...gasche — It's interesting you say the example has to do with the programmer's understanding of doesn't-matter versus the language's. Because that 'programmer's understanding' is the God's eye view. Whether it's acceptable from the language interpreter's perspective to use unsafe IO ("just do it") rather depends on what the language interpreter is using the information for. Note, it's an illustration of the problem, not a claimed example of practicality; I tend to go for demonstrating a principle without worrying about demonstrations of how often it'll come up in practice, perhaps because I assume that if a system has a theoretical hole in it, sooner or later someone would be sure to step right in the hole, therefore showing the hole is there is sufficient to establish the situation needs fixing for the long run (and I plan for the long run, because that's all that will matter — in the long run).<br /><br />DAY — I mean adjunctions, the highest-level of the basic categorical structures — categories, functors, natural transformations, adjunctions.John Shutthttps://www.blogger.com/profile/00041398073010099077noreply@blogger.comtag:blogger.com,1999:blog-7068528325708136131.post-22312568173426638002011-12-09T13:52:47.675-08:002011-12-09T13:52:47.675-08:00It seems to me what you call "adjunctions&quo...It seems to me what you call "adjunctions" are actually "functors", or I did not get it?Anonymoushttps://www.blogger.com/profile/14359320866411018319noreply@blogger.comtag:blogger.com,1999:blog-7068528325708136131.post-78557771371265725962011-12-09T12:33:40.241-08:002011-12-09T12:33:40.241-08:00I think types should capture the interface of a va...I think types should capture the interface of a value. In your example, when you wish to add some effect to the function f, but are sure that it `makes no difference to the operation of the program`, you should use unsafePerformIO or equivalent: if an effect does not change the interface, it can be cast away.<br /><br />This is by the way a perfectly fine way to do debugging logging, and I believe it is accepted by Haskell programmers. Of course, you have to restrict yourself to operationrs that "make no difference"; if you suddenly realize that it actually makes a difference because, for example, you then need to control the "order of evaluation" of different parts of the program, then it changes the mode of use, hence the interface, and it is natural that it "breaks abstraction".<br /><br />Note that this case is a bit particular; it doesn't feel good to "hack away" the effect by using an unsafe feature. But this is actually necessary here because the notion of "making no difference" you use is different from the one of your programming language, which is observational equivalence. By saying that "oh, this logging does not matter", you have a notion of equivalence that is more lenient than the observational equivalence -- you quotient over some things that are actually observable. There is no way the type system is ever to admit that your change is safe (because from what he knows, it isn't), you have to force him to accept it.<br /><br />In the more common case where you want to use an effect inside (say, a mutable reference for optimization purposes) but it *really* is not observable, you can try to get your type system to admit it and keep the type effect-less by itself. That is, for example, what the ST monad does in Haskell, in a specific case where a parametricity/genericity based argument allows the type system to prove that some use of effects are unobservable.<br /><br /><br />This is only a comment on your example. I think that, the way it is presented, it is not actually convincing (for the reason that I said: you should just use unsafePerformIO). Might be it could be turned into a good example by changing the setting; but I'm afraid you will end up with "changing the type is inevitable and the right thing to do, the only problem is to propagate that change through the calls, the hughe code changes required are boring"; this is a valid engineering problem, but I'm not quite sure it stands at the fundamental level you describe.<br /><br />I'm sorry I don't have much to say on your presentation of monad coming from adjunctions. It reminds me of the work on algebraic effects, which tend to compose more easily than general monads.gaschehttps://www.blogger.com/profile/06100241581708586136noreply@blogger.com