Hi Jay,

I appreciate your pointers! However, I think either I didn’t make my question 
clear enough, or I misunderstand your explanation (or perhaps some of both).

What I am trying to model is, indeed, a form of delimited control. I have 
already written a model that supports a couple classic control operators, 
namely exception handling and nondeterminism, plus some of the simpler 
algebraic operations from the algebraic effects literature such as mutable 
state. However, this isn’t quite sufficient for what I’m trying to do, as 
effect systems allow the programmer to define those kinds of control operators 
using more general primitives in the host language.

Here’s an example of what an effect definition and an effect handler might look 
like in a hypothetical language that supports algebraic effect handlers:

  effect Error e where
    throw :: e -> a

  handleError :: (() ->{Error e} a) -> Either e a
  handleError f =
    handle Error where
      throw e _k = Left e
    in Right (f ())

You can reasonably think of `effect` and `handle` in terms of delimited 
control. Each `effect` declaration declares a new prompt tag, and each 
operation of the effect aborts, passing its current continuation to the prompt 
handler. Likewise, each `handle` declaration installs a new prompt with the 
appropriate tag and handler. (In the above example, `throw` discards the 
continuation and simply returns.)

This interpretation works well enough for algebraic effects, but this makes it 
impossible to support operations like `catch`, or `cut` (for some kind of 
backtracking effect) forcing them to be handlers instead. This turns out to 
cause trouble in practice., so some newer work handles so-called “scoped” 
effects as well, which support “scoping” operations like `catch` and `cut`. I 
have been working on an implementation of a scoped effect system in Haskell, 
but I have found many edge cases where the behavior of current systems produces 
nonsensical results given certain handler compositions.

Fortunately, I have found that it is possible to produce a significantly more 
predictable semantics for scoped effect handlers by viewing them as kind of 
like “first class reduction rules.” A handler for an Error effect supporting 
both `throw` and `catch` can be expressed using the following three reduction 
rules:

    E[handleError v] -> E[Right v]
    E_1[handleError E_2[throw v]] -> E_1[Left v]
    E_1[handleError E_2[catch e v]] ->
      E_1[handleError E_2[
        case handleError e of
          Right a -> a
          Left  b -> v b]]

However, doing this also requires extending the definition of E itself so that 
reduction may proceed into the appropriate locations:

    E ::= ... | throw E | catch e E | handleError E

Therefore, this encoding of scoped handlers requires that they operate at the 
level of the metalanguage, which is not enough — I want to come up with a model 
that pushes the above expressive power into the language by defining 
appropriately general-purpose `effect` and `handler` syntactic forms.

It is possible that what you are telling me is I should not bother, and instead 
I should try to define a translation from my higher-level language into 
something simpler to actually implement, such as some well-known model of 
delimited control. However, the reason I have been hoping to avoid doing that 
is I think the translation is not as straightforward as it seems, and the main 
reason I want to model the higher-level interface directly is to better 
understand how I think it ought to work before I try and define a translation 
into something else (probably delimited continuations or monads).

Does that help to give a little more context? I was trying not to drag too much 
of it in when writing my original email, but it’s possible that in doing so I 
omitted too much. :)

Alexis

> On Nov 9, 2019, at 04:53, Jay McCarthy <jay.mccar...@gmail.com> wrote:
> 
> First, any inductive definition could be defined with
> `define-judgment-form` (although derivations will only be discoverable
> if you can give a mode spec.) If the semantics you're talking about
> can't be written as an inductive definition, then it probably doesn't
> make any sense.
> 
> Second, 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. (The beginning of
> SEwPR explains this very well.) I feel like you'll get something from
> thinking about existing semantics that structure the context in
> different ways. For example, in "boring" lambda calculus, rules are
> always of the form "E [ e ] -> E [ e' ]". But, in the traditional way
> to explain exception-handling, you have a reduction rule like "E [ try
> F [ throw v_x ] with catch v_h ] => "E [ v_h v_x ]" where you've
> structured the context (F is "catch"-less contexts.) Chapter 8 of
> SEwPR [1] covers this kind of thing. The delimited control example has
> more complicated things like this too [2] but it might be too
> complicated to understand just this piece of it. Another example to
> look at is the context-based semantics of call-by-need. Stephen's ESOP
> 2012 paper [3] is a great place to look because it talks about a
> standard old way and a clever new way, and is very readable, the key
> is a rule like: "(\x. E[x]) v -> (\x. E[v]) v" where the terms in the
> reduction relation don't use contexts only on the outside.
> 
> I don't really understand what you're trying to do, but it may be
> possible to have a LHSes like
> 
> PhiContext [ GammaContext [ (gamma f v ExprContext [ (f e) ]) ] ]
> 
> to get what you want
> 
> Jay
> 
> 1. https://redex.racket-lang.org/sewpr-toc.html
> 2. 
> https://github.com/racket/redex/tree/master/redex-examples/redex/examples/delim-cont
> 3. http://www.ccs.neu.edu/home/stchang/pubs/Chang-Felleisen-ESOP2012.pdf
> 
> --
> Jay McCarthy
> Associate Professor @ CS @ UMass Lowell
> http://jeapostrophe.github.io
> Vincit qui se vincit.
> 
> 
> --
> Jay McCarthy
> Associate Professor @ CS @ UMass Lowell
> http://jeapostrophe.github.io
> Vincit qui se vincit.
> 
> 
> On Sat, Nov 9, 2019 at 4:10 AM Alexis King <lexi.lam...@gmail.com> wrote:
>> 
>> 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/1F0DAEA5-9BDD-40DA-BE95-08652781D9D8%40gmail.com.

Reply via email to