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" <n...@ccs.neu.edu>
To: "users" <users@racket-lang.org>
Cc: "ejs" <e...@ccs.neu.edu>, "Casey Klein" <clkl...@racket-lang.org>, "Phil
Nguyen" <pngu...@ccs.neu.edu>, "matthias" <matth...@ccs.neu.edu>,
pa...@ccs.neu.edu, "Daniel King" <dank...@ccs.neu.edu>, "Claire Alvis"
<cal...@ccs.neu.edu>, "Phillip Mates" <ma...@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
____________________
Racket Users list:
http://lists.racket-lang.org/users
