<html><head><style type='text/css'>p { margin: 0; }</style></head><body><div style='font-family: Times New Roman; font-size: 12pt; color: #000000'>For the benefit of the wider list, I am copying Robby's feedback below, as taken from the private list.<br><br><br><div><br></div>Here's the list, interspersed with my comments.<div> <br></div> <ul style="margin-top:15px;margin-right:0px;margin-left:0px;padding:0px 0px 0px 30px;border:0px;margin-bottom:0px!important"><li style="margin:0px;padding:0px;border:0px">multi-hole evaluation contexts</li><ul style="margin:0px;padding:0px 0px 0px 30px;border:0px"><li style="margin:0px;padding:0px;border:0px">being able to write up the pi-calculus in a natural way, with multi-hole contexts acting as congruence rules, could be a good goal here</li></ul></ul><div><br></div><div style="">This one is, unless I'm missing something (which is entirely possible), tricky. It is a fundamental change to the matcher (which is the heart of redex). I think the right thing here would be to start with this paper: <a href="http://www.eecs.northwestern.edu/%7Erobby/plug/" target="_blank">http://www.eecs.northwestern.edu/~robby/plug/</a> and work out the new semantics. Only after you know exactly how it works should you tackle implementing it. IMO.</div> <ul style="margin-top:15px;margin-right:0px;margin-left:0px;padding:0px 0px 0px 30px;border:0px;margin-bottom:0px!important"><li style="margin:0px;padding:0px;border:0px">`traces' analogue for judgment-holds</li></ul> <div><br></div><div style="">Are you looking for show-derivations?</div><ul style="margin-top:15px;margin-right:0px;margin-left:0px;padding:0px 0px 0px 30px;border:0px;margin-bottom:0px!important"><li style="margin:0px;padding:0px;border:0px"> allow unquoting in judgment premise side-conditions</li></ul><div><br></div><div style="">This is already allowed.</div><ul style="margin-top:15px;margin-right:0px;margin-left:0px;padding:0px 0px 0px 30px;border:0px;margin-bottom:0px!important"><li style="margin:0px;padding:0px;border:0px">cross-language metafunctions</li></ul><div><br></div><div style="">This one is tricky. Here's the simple example that suggests what needs to be thought out:</div><div style=""><br> </div><div style="">(define-language L1</div><div style="">  (e ::= 1))</div><div style=""><br></div><div style="">(define-language L2</div><div style="">  (e ::= 2))</div><div style=""><br></div><div style="">(define-metafunction domain-as-L1-codomain-as-L2</div> <div style="">  [(M e) e])</div><div style=""><br></div><div style="">What does this do? Always <span style="line-height:1.7">signal an error? If so, does that mean that the right-hand sides of metafunctions are now doing matching (to handle the case when M is called with 1 as the input? If so, then I think we'd probably want to start with the paper I pointed you to above first and figure things out at that level. If not, maybe there's another way to do this?</span></div> <div style=""><br></div><ul style="margin-top:15px;margin-right:0px;margin-left:0px;padding:0px 0px 0px 30px;border:0px;margin-bottom:0px!important"><li style="margin:0px;padding:0px;border:0px">don't-bind-don't-care construct</li></ul><div><br></div><div style="">We could add underscore for this. It should be easy.</div><div><br></div><ul style="margin-top:15px;margin-right:0px;margin-left:0px;padding:0px 0px 0px 30px;border:0px;margin-bottom:0px!important"><li style="margin:0px;padding:0px;border:0px">matching on more than just sexprs: structs, sets, hashes</li></ul><div><br></div><div style="">Redex really needs this. The place I've struggled thinking about it is the concrete syntax. Writing "#hash(x . 1)" or something like that in a redex pattern is unacceptable! So I think the place to start here is to add something to the pattern language and working at the leve of that paper I've now pointed out twice before.<br>Oh, one more comment on the hashes-and-sets additions to the pattern language: we should really study Maude and co. for this one. They do this well already.<br></div> <div><br></div><ul style="margin-top:15px;margin-right:0px;margin-left:0px;padding:0px 0px 0px 30px;border:0px;margin-bottom:0px!important"><li style="margin:0px;padding:0px;border:0px">general "debugging" friendliness</li><ul style="margin:0px;padding:0px 0px 0px 30px;border:0px"><li style="margin:0px;padding:0px;border:0px">e.g. a "reasonable" means of introspecting the state of a reduction so that we don't have to e.g. put in nasty printing side-conditions</li></ul></ul><div><br></div><div style="">This sounds promising. But what do you have in mind? </div><div style=""><br></div><div style="">I'd given some thought to somehow instrumenting the matcher so that when it fails to match something you can get feedback about the parts that did match to go quickly to the unmatched part. Is that what you have in mind? Or do you imagine something at a coarser granularity?</div> <div style=""><br></div><ul style="margin-top:15px;margin-right:0px;margin-left:0px;padding:0px 0px 0px 30px;border:0px;margin-bottom:0px!important"><li style="margin:0px;padding:0px;border:0px">disable caching for individual metafunctions (but not the metafunctions they call)</li></ul><div><br></div><div style="">Eminently doable.</div><div><br></div><ul style="margin-top:15px;margin-right:0px;margin-left:0px;padding:0px 0px 0px 30px;border:0px;margin-bottom:0px!important"><li style="margin:0px;padding:0px;border:0px"> "type-checking"-like thing for metafunctions: at the very least, every clause's pattern should have the same arity as the contract</li><ul style="margin:0px;padding:0px 0px 0px 30px;border:0px"><li style="margin:0px;padding:0px;border:0px"> even better: check that the clause's pattern is a refined version of the pattern from the contract (this may be hard)</li></ul></ul><div><br></div><div style="">Very. That's why there are contracts for now.</div><ul style="margin-top:15px;margin-right:0px;margin-left:0px;padding:0px 0px 0px 30px;border:0px;margin-bottom:0px!important"><ul style="margin:0px;padding:0px 0px 0px 30px;border:0px"><li style="margin:0px;padding:0px;border:0px">"has some overlap with pattern contract" might be a more useful check</li></ul></ul><div><br></div><div style=""> This is pattern language inclusion. It should be decidable, but it is tricky and almost certainly super-duper exponential (yes, that's a technical term (okay no, not really)). Working out the algorithm would be a research contribution.</div> <div><br></div><ul style="margin-top:15px;margin-right:0px;margin-left:0px;padding:0px 0px 0px 30px;border:0px;margin-bottom:0px!important"><li style="margin:0px;padding:0px;border:0px">shortcut arrows that are actually useful</li><ul style="margin:0px;padding:0px 0px 0px 30px;border:0px"><li style="margin:0px;padding:0px;border:0px">(There's already a macro hack by Ian for this; should be in redex-proper)</li></ul></ul><div><br></div><div style=""> This sounds promising. I like useful things, anyway.</div><div><br></div><ul style="margin-top:15px;margin-right:0px;margin-left:0px;padding:0px 0px 0px 30px;border:0px;margin-bottom:0px!important"><li style="margin:0px;padding:0px;border:0px"> a distinction between introducing a new variable and matching on that variable: would prevent trying to bind to that variable twice.</li></ul><div><br></div><div style="">Can you say more what you have in mind here?</div><ul style="margin-top:15px;margin-right:0px;margin-left:0px;padding:0px 0px 0px 30px;border:0px;margin-bottom:0px!important"><li style="margin:0px;padding:0px;border:0px">'traces' support for user-defined reduction relation applications (e.g. apply-reduction-relation*/random)</li></ul><div><br></div><div style="">I'm not getting this. But I think it sounds like one in the doable category.<br></div><br>----- Original Message -----<br>From: "Alex Marquez" <nam@ccs.neu.edu><br>To: "users" <users@racket-lang.org><br>Cc: "ejs" <ejs@ccs.neu.edu>, "Casey Klein" <clklein@racket-lang.org>, "Phil Nguyen" <pnguyen@ccs.neu.edu>, "matthias" <matthias@ccs.neu.edu>, pauls@ccs.neu.edu, "Daniel King" <danking@ccs.neu.edu>, "Claire Alvis" <calvis@ccs.neu.edu>, "Phillip Mates" <mates@ccs.neu.edu><br>Sent: Thursday, May 23, 2013 1:43:18 PM GMT -05:00 US/Canada Eastern<br>Subject: [racket] Redex hackfest<br><br>Several of us at the NEU Programming Research Laboratory are interested in improving Redex and will be having a hackfest to do so, scheduled for sometime in the first week of June.<br><br>We invite whomever would like to join to express their interest and availability, as that will influence the exact schedule.  It is not required to be physically at NEU; rather, one may simply take the opportunity to hack remotely and communicate via e-mail or IRC, taking advantage of the collective focus on Redex for the time.<br><br>Our high-level, provisional "wishlist" for changes to Redex is available at:<br>https://github.com/plt/racket/wiki/Redex-Features<br><br>Please feel free to comment on these features or add to them as you see fit.  Until the hackfest, we will be using this thread to discuss logistics and these features.<br><br><br>Alex Marquez<br>NEU PRL<br>____________________<br>  Racket Users list:<br>  http://lists.racket-lang.org/users<br></div></body></html>