> On Nov 9, 2019, at 09:18, Jay McCarthy <jay.mccar...@gmail.com> wrote: > > "remember that an evaluation context is just a way of describing more > succinctly what you could otherwise define by hand as a big, > complicated relation on individual terms."
Yes, that makes sense — I wasn’t really considering what it would look like to define these rules without evaluation contexts until you mentioned that in your first email. They’re a very nice way of thinking about these things, though! I’m not sure if it is worth it to me right now to go to the effort to define the “big, complicated relation” in this particular case just to get an executable version of the rules I’ve written down with pen and paper, but maybe it would be a good exercise; I don’t know. > There is nothing special about evaluation contexts. I think they are > beautiful, but they don't, for example, automatically come with a set > of free theorems, like monads. The best thing they have going for them > is that they decouple the specification of evaluation rules and where > those rules occur (i.e. there are no "congruence" rules in the > reduction relation.) But, a reduction system can always have extra > rules that don't use them, so you don't get anything "for free". It is > possible that the thing you want can't be done using contexts, but > that doesn't mean redex or even redex's reduction-relation is wrong > tool to use. > > That said, I don't think the idea of a "first-class" context or > evaluation rule makes sense, because the whole point of a proof theory > is to have a fixed set of proof schemas which you can reason about. If > you want to take term data and turn that into new rule cases, then > you'll have to have a more general rule that inspects the term data > and acts on it. For example, if you wanted your term data to be able > to cause evaluation anywhere, then one technique would be to by > default have evaluation happen everywhere, but then the evaluation > rule will inspect the context to see if evaluation is enabled in any > specific case. I think that makes sense from an implementation > perspective too. I should be clear: the main reason I decided to think about this in terms of reduction rules defined using evaluation contexts in the first place is because I didn’t even know what I thought the system I was trying to build ought to do in the edge cases. Writing down rules in terms of evaluation contexts has been an exercise in figuring out what I think the system I’m building means, and specifically, it is an attempt to find a system that reflects the equational reasoning rules I already intuitively believe ought to hold. From that perspective, the “expressive power” of evaluation contexts is precisely what appeals to me — it makes it easier to sketch out variations on the rules I have and see how they interact with one another. I don’t think the set of rules I have is directly useful for either proving things about my effect system or actually practically implementing it. I just don’t know how to express some of the more complicated interactions I’m thinking about (such as, for example, distributivity of the continuation over nondeterministic choice) more clearly and simply than with evaluation contexts. If the takeaway here is that I am better served doing that with pen and paper, and maybe putting something in Redex once I have a firmer grasp on what I actually want to model, that’s fine; it’s helpful to know. > Maybe not useful, but I believe that delimited control was really made > by Matthias to solve the same problem as algebraic effects are solving > today. Read his papers again in that light and it may be helpful. Thanks, I will certainly do so. I read a couple of them several years ago when I was first learning about delimited control, but I think you’re right I would benefit from looking at them again. (Algebraic effects are appealing to me not because of their expressive power necessarily but because of certain implementation advantages, especially in a typed setting, but it is quite clear that they have an intimate relationship with delimited control. I could do to be more familiar with that literature.) Alexis -- You received this message because you are subscribed to the Google Groups "Racket Users" group. To unsubscribe from this group and stop receiving emails from it, send an email to racket-users+unsubscr...@googlegroups.com. To view this discussion on the web visit https://groups.google.com/d/msgid/racket-users/D19B5D53-7D2B-4513-820C-989F57B0727C%40gmail.com.
