Redex: call for alpha-equivalence beta testers

[Robby Findler]

Paul Stansifer has been implementing the ideas from his dissertation
work in Redex and is now ready to share them with the world.

Thanks to Paul, Redex languages now understand binding structure,
meaning that if you write a substitution function that just blindly
substitutes, it will actually properly do alpha conversion to avoid
name collisions. In general, pattern matching now has alpha
equivalence smarts (see the docs for more).

The new features include the #:binding keyword in define-language and
extend-language, and the alpha-equivalent? and substitute functions.

The plan is to let it stay only in Paul's repo until the next release
goes out and then push it to the main Redex repo to be included in the
release after this one. If you'd like to give it a try, some
instructions are below. Please let us know how it goes!

Robby


--------------------------------

To try it out, first download a snapshot build:

http://pre.racket-lang.org/installers/

and then create a parent directory to hold the git repo for Redex:

cd PLTDIR; mkdir extra-pkgs; cd extra-pkgs

run this command to get the git version of Redex:

raco pkg update --clone redex \
"git://github.com/racket/redex?path=redex" \
"git://github.com/racket/redex?path=redex-benchmark" \
"git://github.com/racket/redex?path=redex-doc" \
"git://github.com/racket/redex?path=redex-examples" \
"git://github.com/racket/redex?path=redex-gui-lib" \
"git://github.com/racket/redex?path=redex-lib" \
"git://github.com/racket/redex?path=redex-pict-lib" \
"git://github.com/racket/redex?path=redex-test"

and then get Paul's version:

cd redex
git remote add paul https://github.com/paulstansifer/redex-1.git
git checkout public
raco setup

[Daniel Feltey]

> and then get Paul's version:
>
>   cd redex
>   git remote add paul https://github.com/paulstansifer/redex-1.git
>   git checkout public
>   raco setup

This didn't quite work for me the first time I tried it, I needed to run `git fetch paul` before the checkout to make it work.

Looking forward to trying this out!

Dan

--
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...@googlegroups.com.
For more options, visit https://groups.google.com/d/optout.

[William J. Bowman]

I get this error several times during the final `raco setup`:

redex-examples/redex/examples/lazy-with-binding.rkt:30:38: define-language: expected a shadow, nothing, or nonterminal
in: (rib x ...)
compilation context...:
/home/bluephoenix47/workspace/racket/racket/share/extra-pkgs/redex/redex-examples/redex/examples/lazy-with-binding.rkt
context...:
/home/bluephoenix47/workspace/racket/racket/share/extra-pkgs/redex/redex-lib/redex/private/binding-forms-compiler.rkt:190:12: process-under
/home/bluephoenix47/workspace/racket/racket/share/extra-pkgs/redex/redex-lib/redex/private/binding-forms-compiler.rkt:169:1: surface-bspec->pat&bspec
/home/bluephoenix47/workspace/racket/racket/share/extra-pkgs/redex/redex-lib/redex/private/binding-forms-compiler.rkt:19:1: compile-binding-forms
/home/bluephoenix47/workspace/racket/racket/share/extra-pkgs/redex/redex-lib/redex/private/reduction-semantics.rkt:1885:0
/home/bluephoenix47/workspace/racket/racket/collects/syntax/wrap-modbeg.rkt:46:4
/home/bluephoenix47/workspace/racket/racket/collects/compiler/cm.rkt:346:0: compile-zo*
/home/bluephoenix47/workspace/racket/racket/collects/compiler/cm.rkt:561:26
/home/bluephoenix47/workspace/racket/racket/collects/compiler/cm.rkt:553:42
/home/bluephoenix47/workspace/racket/racket/collects/compiler/cm.rkt:518:0: maybe-compile-zo
/home/bluephoenix47/workspace/racket/racket/collects/compiler/cm.rkt:633:2: do-check
/home/bluephoenix47/workspace/racket/racket/collects/compiler/cm.rkt:713:4
/home/bluephoenix47/workspace/racket/racket/collects/setup/..:261:28
/home/bluephoenix47/workspace/racket/racket/collects/setup/..:261:28
/home/bluephoenix47/workspace/racket/racket/collects/setup/parallel-do.rkt:435:20: loop


I'd add an issue in the repo, but Paul's fork seems to have issues
disabled.

--
William J Bowman

[William J. Bowman]

Paul asked me to forward this as racket-users is currently rejecting him:

On Sep 24, 2015, at 14:36, Paul Stansifer <pa...@ccs.neu.edu> wrote:

Sorry about that; it looks like I forgot to check the examples after disabling 'rib'. The fix is to change all instances of 'rib' to 'shadow'. I'll try to push a fix soon, but I won't get a chance to do it today. 

Paul

[William J. Bowman]

I just ported Cur to use this version of Redex
(https://github.com/wilbowma/cur/tree/redex-with-binding), and was able
to delete and simplify many lines of code and get all tests passing in
minutes. Hurrah! Although, I do not have interesting binding structure.

A few comments

0. Was very easy; kudos. The new Redex build was completely backwards
compatible, and all changes to my code were simplifications, such
as deleting my hand-rolled α-equivalence relation, and deleting
substitution.

1. It was not obvious to me that /binding-pattern/ was not just a
grammar but a pattern. I tried to specify binding with:

#:binding-forms (Π (x : t) t #:refers-to x),

but this caused problems until I changed it to:

#:binding-forms (Π (x : t_0) t_1 #:refers-to x)

2. default-lang was not properly linked in at least one place in the
documentation (in the explanation of default-equiv).

3. I'm getting some seriously long names, making output rather unreadable. The output of some of my tests:

'(λ (x159160161162 : Bool) x159160161162)
'(λ (x168169170171172 : Bool) x168169170171172)
'(λ (x178179180181182183 : Bool) x178179180181182183)
'(λ (x189190191192193194195 : Bool) x189190191192193194195)

Previously, this output was

'(λ (x2 : Bool) x2)
'(λ (x1 : Bool) x1)
'(λ (x2 : Bool) x2)
'(λ (x1 : Bool) x1)

--
William J. Bowman

On Sat, Sep 19, 2015 at 12:21:17PM -0500, Robby Findler wrote:

[Paul Stansifer]

Thanks for trying it out! It's exciting to have a user! The broken example is now fixed on GitHub.

On Thursday, September 24, 2015 at 5:07:22 PM UTC-4, William J. Bowman wrote:
> ...

>
> 1. It was not obvious to me that /binding-pattern/ was not just a
> grammar but a pattern. I tried to specify binding with:
>
> #:binding-forms (Π (x : t) t #:refers-to x),
>
> but this caused problems until I changed it to:
>
> #:binding-forms (Π (x : t_0) t_1 #:refers-to x)

That should probably be emphasized more in the documentation. A problem that I have encountered in general is that bugs caused by /binding-pattern/s failing to match are hard to track down.

> 2. default-lang was not properly linked in at least one place in the
> documentation (in the explanation of default-equiv).

Odd. I think that it might be the case that parameter definitions are handled differently by Scribble.

>
> 3. I'm getting some seriously long names, making output rather unreadable. The output of some of my tests:
>
> '(λ (x159160161162 : Bool) x159160161162)
> '(λ (x168169170171172 : Bool) x168169170171172)
> '(λ (x178179180181182183 : Bool) x178179180181182183)
> '(λ (x189190191192193194195 : Bool) x189190191192193194195)
>
> Previously, this output was
>
> '(λ (x2 : Bool) x2)
> '(λ (x1 : Bool) x1)
> '(λ (x2 : Bool) x2)
> '(λ (x1 : Bool) x1)

This would be easy to fix by generating totally fresh names, instead of keeping around the original. But maybe it would be worth it to make it look like we did `(gensym original-name)` rather than `(gensym (gensym (gensym (gensym original-name))))` in cases where names are repeatedly freshened?

Thanks,
Paul

[Robby Findler]

On Friday, September 25, 2015, Paul Stansifer <paul.st...@gmail.com> wrote:

Thanks for trying it out! It's exciting to have a user! The broken example is now fixed on GitHub.

On Thursday, September 24, 2015 at 5:07:22 PM UTC-4, William J. Bowman wrote:
> ...
>
> 1. It was not obvious to me that /binding-pattern/ was not just a
> grammar but a pattern. I tried to specify binding with:
>
>    #:binding-forms (Π (x : t) t #:refers-to x),
>
> but this caused problems until I changed it to:
>
>   #:binding-forms (Π (x : t_0) t_1 #:refers-to x)

That should probably be emphasized more in the documentation. A problem that I have encountered in general is that bugs caused by /binding-pattern/s failing to match are hard to track down.

Could one formulate a reliable test case for binding via a pattern matching form somehow? And then maybe provide some convenience from the redex testing library?

 

> 2. default-lang was not properly linked in at least one place in the
> documentation (in the explanation of default-equiv).

Odd. I think that it might be the case that parameter definitions are handled differently by Scribble.

There may be a missing for-label require. Where is the specific problem?

 

>
> 3. I'm getting some seriously long names, making output rather unreadable. The output of some of my tests:
>
>   '(λ (x159160161162 : Bool) x159160161162)
>   '(λ (x168169170171172 : Bool) x168169170171172)
>   '(λ (x178179180181182183 : Bool) x178179180181182183)
>   '(λ (x189190191192193194195 : Bool) x189190191192193194195)
>
> Previously, this output was
>
>   '(λ (x2 : Bool) x2)
>   '(λ (x1 : Bool) x1)
>   '(λ (x2 : Bool) x2)
>   '(λ (x1 : Bool) x1)

This would be easy to fix by generating totally fresh names, instead of keeping around the original. But maybe it would be worth it to make it look like we did `(gensym original-name)` rather than `(gensym (gensym (gensym (gensym original-name))))` in cases where names are repeatedly freshened?

I think so. 

 

Thanks,
Paul

[William J. Bowman]

On Fri, Sep 25, 2015 at 02:36:30PM -0500, Robby Findler wrote:
> > > 2. default-lang was not properly linked in at least one place in the
> > > documentation (in the explanation of default-equiv).
> >
> > Odd. I think that it might be the case that parameter definitions are
> > handled differently by Scribble.
>
>
> There may be a missing for-label require. Where is the specific problem?

In the documentation for `default-equiv`.

--
William J. Bowman

[William J. Bowman]

On Fri, Sep 25, 2015 at 11:01:55AM -0700, Paul Stansifer wrote:
> >
> > 3. I'm getting some seriously long names, making output rather unreadable. The output of some of my tests:
> >
> > '(λ (x159160161162 : Bool) x159160161162)
> > '(λ (x168169170171172 : Bool) x168169170171172)
> > '(λ (x178179180181182183 : Bool) x178179180181182183)
> > '(λ (x189190191192193194195 : Bool) x189190191192193194195)
> >
> > Previously, this output was
> >
> > '(λ (x2 : Bool) x2)
> > '(λ (x1 : Bool) x1)
> > '(λ (x2 : Bool) x2)
> > '(λ (x1 : Bool) x1)
>
> This would be easy to fix by generating totally fresh names, instead of keeping around the original. But maybe it would be worth it to make it look like we did `(gensym original-name)` rather than `(gensym (gensym (gensym (gensym original-name))))` in cases where names are repeatedly freshened?

If possible it would be great to maintain the original name as much as
possible. For example, there is only one binder in all the previous
expands so it's strange that they all got changed.

But, if not, yes `(gensym original-name)` would be preferable.

--
William J. Bowman

[Andrew Kent]

First, just want to say I'm loving this feature so far! Thank you.

One quick question---I have something failing to work, and I'm not sure if it's a bug, or a feature/capability that's not supported (yet?):

[;; other details ...
--------------- "S-Refine"
(subtype Δ (Refine [x : S] Q) (Refine [x : T] P))]

I was hoping that sort of case in a judgment would (1) auto-magically perform substitution such that any two refinements would be made in terms of the same variable, and (2) that variable x would be fresh with respect to the other arguments (i.e. Δ).

It seems like (2) holds, but (1) does not. For example, this test case does not even successfully match on this judgment rule:

(test-equal
(term (subtype (Env ([y : Int]) ())
(Refine [x : Int] (≤ x y))
(Refine [z : Int] (≤ z y))))
#t)

Thanks,
Andrew

[Andrew Kent]

Oh! And I was also curious if a 'free-identifiers' function (similar to 'alpha-equivalent?' and 'substitute') is on a list of future features, perhaps? That would be another nice piece of boilerplate to throw away once binding info is specified for a language...

Thanks again for the awesome new features! =)

[Paul Stansifer]

Thanks!

Regarding feature (1), that might be hard to implement because of the internal design of the freshener. But could you send me the Redex model in question so I can poke at it anyways?

`free-identifiers` should be pretty easy to make. What does it tend to be useful for?

Paul

--
You received this message because you are subscribed to a topic in the Google Groups "Racket Users" group.
To unsubscribe from this topic, visit https://groups.google.com/d/topic/racket-users/CjFIFEhTEj8/unsubscribe.
To unsubscribe from this group and all its topics, send an email to racket-users...@googlegroups.com.

[Andrew Kent]

- I'll send the model I'm toying with your way.

- I was using free-identifiers/free-vars to define the wellformedness of environments and types. I've seen it used in other formalisms, but I'm not sure just how widely used it is relative to other potential features.

[William J. Bowman]

Recently after upgrading from Paul's fork, substitute stopped working
inside my reduction relation. I get the following error:

> compiled-lang-binding-table: contract violation
> expected: compiled-lang?
> given: #f
> context...:
> /home/bluephoenix47/workspace/racket/extra-pkgs/redex/redex-lib/redex/private/reduction-semantics.rkt:1425:42
> /home/bluephoenix47/workspace/racket/racket/collects/racket/private/map.rkt:21:13: map
> /home/bluephoenix47/workspace/racket/extra-pkgs/redex/redex-lib/redex/private/reduction-semantics.rkt:1724:24: loop
> /home/bluephoenix47/workspace/racket/extra-pkgs/redex/redex-lib/redex/private/reduction-semantics.rkt:840:15
> /home/bluephoenix47/workspace/racket/extra-pkgs/redex/redex-lib/redex/private/reduction-semantics.rkt:973:9
> /home/bluephoenix47/workspace/racket/extra-pkgs/redex/redex-lib/redex/private/reduction-semantics.rkt:1047:7
> /home/bluephoenix47/workspace/racket/extra-pkgs/redex/redex-lib/redex/private/reduction-semantics.rkt:250:0: apply-reduction-relation/tagged
> /home/bluephoenix47/workspace/racket/extra-pkgs/redex/redex-lib/redex/private/reduction-semantics.rkt:2464:2
> /home/bluephoenix47/workspace/racket/extra-pkgs/redex/redex-lib/redex/private/reduction-semantics.rkt:2442:0: apply-reduction-relation*15
> /home/bluephoenix47/workspace/racket/racket/collects/racket/contract/private/arrow-val-first.rkt:324:3

I notice that substitute recently changed to a metafunction--which is
handy--and requires (default-language) be set. According to the
documentation, (default-language) is only set inside metafunction and
judgment-forms, *not* reduction-relations. Perhaps this is the cause of
the error?

--
William J. Bowman

On Sat, Sep 19, 2015 at 12:21:17PM -0500, Robby Findler wrote:

> --

> 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...@googlegroups.com.

[Robby Findler]

I believe I've pushed a fix for this. Thanks for the report!

Robby

[William J. Bowman]

Did Paul's work just get merged into the main Redex package, or did this
just get pushed to the wrong place?

--
William J. Bowman

[Robby Findler]

It was merged.

Robby

On Wed, Oct 28, 2015 at 10:55 AM, William J. Bowman