Hello,
I am trying to model a (not quite algebraic) effect system in PLT Redex, but
I’m struggling to encode my evaluation contexts into Redex’s pattern language.
My question is best explained via example, so I’ll start with a bog-standard
call-by-value lambda calculus:
(define-language lam
[v ::= boolean (λ x e)]
[e ::= x v (e e) (if e e e)]
[E ::= hole (E e) (v E) (if E e e)]
[x ::= variable-not-otherwise-mentioned]
#:binding-forms
(λ x e #:refers-to x))
My reduction relation for lam is the usual one. Next, I define an extended
language:
(define-extended-language eff lam
[e ::= .... (ψ x e) (γ (x p ...) e) (x e ...)]
[E ::= .... (ψ x E) (γ (x p ...) E)]
[p ::= :v :e :E]
#:binding-forms
(ψ x e #:refers-to x))
This is a severe simplification of the actual language I’m trying to model, but
it’s enough to illustrate my problem: the definition for E I’ve given above is
inadequate. What I actually want is to have some kind of
“dynamic”/“context-sensitive” evaluation context, where γ can introduce scoped
evaluation rules for identifiers bound by ψ.
To give an example, if I have the expression
(ψ f
(γ (f :E :e)
(f (if #t #f #t) (if #t #f #t))))
I would like it to reduce to
(ψ f
(γ (f :E :e)
(f #f (if #t #f #t))))
because (γ (f :E :e) e_1) effectively extends E with a new production rule (f E
e) inside e_1, allowing reduction to recur into the first argument to f, but
not the second.
If I were to define these rules on pen and paper, without using Redex, my
instinct would be to create some kind of “parameterized” evaluation context.
That is, I would define something like this:
r ::= (x p ...)
(E r ...) ::=
hole ((E r ...) e) (v (E r ...)) (if (E r ...) e e)
(ψ x (E r ...)) (γ r_0 (E r_0 r ...))
(E-r r r ...) ...
(E-r (x p ...) r ...) ::= (x (E-p p r ...) ...)
(E-p :v _ ...) ::= v
(E-p :e _ ...) ::= e
(E-p :E r ...) ::= (E r ...)
Though a little complicated to define, I think decomposition using these
evaluation contexts is still entirely syntax-directed (assuming the r arguments
are only used as inputs; i.e. E, E-r, and E-p are “metapatterns”). Proving
anything in this system seems like it could be a massive headache, but it’s
much too soon for me to be worrying about that — I just want a super-flexible
model I can throw some examples at to see what it does. Redex seems like it
would be ideal for that, but I have no idea how to encode this kind of
complicated decomposition into Redex’s pattern language.
I suspect that doing it directly is completely impossible, so I was wondering
if there are any tricks or techniques I might use to encode it indirectly. Is
there something clever I can do with a judgment form? I’ve been thinking about
ways I might define my reduction relation inductively or something like that,
but I really want to have access to the evaluation context (actually multiple
evaluation contexts) in my reduction rules, since I’m using the language to
define complicated control operators.
Thanks,
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/E7A24480-1E87-42AB-A580-33FB3A2B3C04%40gmail.com.
