[racket] Redex hackfest

For the benefit of the wider list, I am copying Robby's feedback below, as taken from the private list. 




Here's the list, interspersed with my comments. 



    • multi-hole evaluation contexts 


        • 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 



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: http://www.eecs.northwestern.edu/~robby/plug/ and work out the new semantics. Only after you know exactly how it works should you tackle implementing it. IMO. 

    • `traces' analogue for judgment-holds 



Are you looking for show-derivations? 

    • allow unquoting in judgment premise side-conditions 



This is already allowed. 

    • cross-language metafunctions 



This one is tricky. Here's the simple example that suggests what needs to be thought out: 


(define-language L1 
(e ::= 1)) 


(define-language L2 
(e ::= 2)) 


(define-metafunction domain-as-L1-codomain-as-L2 
[(M e) e]) 


What does this do? Always 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? 



    • don't-bind-don't-care construct 



We could add underscore for this. It should be easy. 



    • matching on more than just sexprs: structs, sets, hashes 



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. 
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. 




    • general "debugging" friendliness 


        • 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 



This sounds promising. But what do you have in mind? 


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? 



    • disable caching for individual metafunctions (but not the metafunctions they call) 



Eminently doable. 



    • "type-checking"-like thing for metafunctions: at the very least, every clause's pattern should have the same arity as the contract 


        • even better: check that the clause's pattern is a refined version of the pattern from the contract (this may be hard) 



Very. That's why there are contracts for now. 



        • "has some overlap with pattern contract" might be a more useful check 



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. 



    • shortcut arrows that are actually useful 


        • (There's already a macro hack by Ian for this; should be in redex-proper) 



This sounds promising. I like useful things, anyway. 



    • a distinction between introducing a new variable and matching on that variable: would prevent trying to bind to that variable twice. 



Can you say more what you have in mind here? 

    • 'traces' support for user-defined reduction relation applications (e.g. apply-reduction-relation*/random) 



I'm not getting this. But I think it sounds like one in the doable category. 

----- Original Message ----- 
From: "Alex Marquez" <nam at ccs.neu.edu> 
To: "users" <users at racket-lang.org> 
Cc: "ejs" <ejs at ccs.neu.edu>, "Casey Klein" <clklein at racket-lang.org>, "Phil Nguyen" <pnguyen at ccs.neu.edu>, "matthias" <matthias at ccs.neu.edu>, pauls at ccs.neu.edu, "Daniel King" <danking at ccs.neu.edu>, "Claire Alvis" <calvis at ccs.neu.edu>, "Phillip Mates" <mates at ccs.neu.edu> 
Sent: Thursday, May 23, 2013 1:43:18 PM GMT -05:00 US/Canada Eastern 
Subject: [racket] Redex hackfest 

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. 

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. 

Our high-level, provisional "wishlist" for changes to Redex is available at: 
https://github.com/plt/racket/wiki/Redex-Features 

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. 


Alex Marquez 
NEU PRL 
____________________ 
Racket Users list: 
http://lists.racket-lang.org/users 
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.racket-lang.org/users/archive/attachments/20130528/77643d6f/attachment.html>