Re: [racket-users] Redex compatible closure of mutually defined nonterminals

[William J. Bowman]

On Tue, May 07, 2019 at 03:55:09PM -0500, Robby Findler wrote:
> I can agree that the current definition isn't the best one, but this
> one doesn't seem right. I mean, this requires that both sides step? It
> is a kind of parallel reduction? That doesn't seem like something
> commonly wanted.
Yeah, that was a mistake, and not the only one I made in that email.
Let me try again.

In this model, I'm actually trying to define two reduction relations and take
the compatible-closure of these two mutually defined relations.
The first is of the form `t -> t'` and the second of the form `v -> v'`.
`v -> v'` is trivial (contains no reductions), but it's compatible closure
contains an the following interesting reduction rule.

  t -> t'
  
  thunk t -> thunk t'

It looks like the compatible-closure of `t -> t'` is doing the right thing: it
does apply the above rule, as long as I was reducing a `t` to begin with.
The real problem is that I can't access the `v -> v'` relation directly, so I
can't apply any reduction relation at all to `v`s.

This is particularly annoying, since Redex has computed that relation and can
use it internally.
I can't define a trivial reduction relation (all reduction relations need
rules), so I can't manually call `compatible-closure` on this trivial relation.
I also can't access `cross` in my surface language to define contexts, so I
can't take the context closure without writing out about 50 lines of contexts 
:(.

--
William J. Bowman

-- 
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/20190508021903.GW95917%40williamjbowman.com.
For more options, visit https://groups.google.com/d/optout.

Re: [racket-users] tilda - a threading macro full of itself

[Matthias Felleisen]

> On May 7, 2019, at 1:29 PM, zeRusski  wrote:
> 
> It just names the threaded value. Did I overlook anything?
> 
> That's right, nothing fancy. Think let-binding the threaded value at that 
> point. #:with id ~ would achieve the same thing, so as it is now #:as is 
> redundant. With #:do both #:with and #:as are redundant, really.
>  
> Let me point out that if ~> specified an identifier (as suggested in my first 
> response) you could co-mingle two threaded computations, keeping separate 
> concerns that don’t matter as opposed to bundling them up in structs or lists 
> or whatever you have to do if you have only one. At first I thought #:as 
> would you let you do so, but that’s not correct.
> 
> Ok, this one I don't quite understand. My first thought went as far as to 
> weave multiple computations where each #:as would capture continuations and 
> macro would keep these "threads" separate, but now I'm thinking you mean this:
> 
> (~> 1 #:as ~a
> ;; now ~a is being threaded
> (add1 ~a)   ;=> 2
> 2 #:as ~b
> ;; now ~b is being threaded
> (add1 ~b)   ;=> 3
> ;; simply use whatever ~a was last
> (+ ~a ~b)   ;=> 5
> #:as ~a
> ;; continue to thread ~a
> (add1 ~a)   ;=> 3
> (list ~a ~b))
> ;; => (list 3 5)

Think: 

(~> (x 0)
  (add1 x) 
  (sin 
(~> (y  1)
  (sub1 y] 
  (+ x y)))
  (* pi x))

This looks equally simple and is equally easy to read. If you wish to emphasize 
the “hole variable” make sure its name has a certain shape, say ~x. 
But now the threading has precise syntactic boundaries, and the implementation 
gets away without any assignments (which I assume #:as uses). 

— Matthias

-- 
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/227C9002-72D0-45DD-939A-9D55F4833403%40felleisen.org.
For more options, visit https://groups.google.com/d/optout.

Re: [racket-users] Redex compatible closure of mutually defined nonterminals

[Robby Findler]

On Mon, May 6, 2019 at 2:11 PM William J. Bowman  
wrote:
>
> I took a quick look at the implementation of `cross` and `compatible-closure`,
> and couldn't make sense of any of it.
> For now, I guess I'll manually write out the contexts, and discuss a feature
> request.
>
> I spoke to Max a bit about what a compatible closure "ought" to be for 
> mutually
> defined syntax.
> I think right now, Redex is doing the "wrong" thing.
> Suppose I have some relation "->" on my nonterminals `v` and `t`.
> Right now, `compatible-closure` is computing something like this:
>
>   t -> t'
>   v = v'
>   
>   t v -> t' v'
>
> That is, to compute the congruence rule for the `(t v)`, we lift the relation
> `->` to apply under `T`, but it appears to compute the simplest possible
> relation on `v`: syntactic identity.
> This is the reason I don't get reduction of `t`s under a `thunk`.
>
> Instead, it "ought" to compute these rules:
>
>   (extending t -> t to closure)
>   t -> t'
>   v -> v'
>   
>   t v -> t' v'

I can agree that the current definition isn't the best one, but this
one doesn't seem right. I mean, this requires that both sides step? It
is a kind of parallel reduction? That doesn't seem like something
commonly wanted.

>   ...
>
>   (generated definition of v -> v)
>
>   t -> t'
>   
>   λ x. t -> λx. t'
>
> This lifts `->` to `v` while computing the closure of `->`.
> I think this should be the default behavior of `compatible-closure` on 
> mutually
> defined nonterminals.
>
> I think in general, we actually want something more: for mutually defined
> syntax/judgments, I might want to define `->t` and `->v` (generally, `->ᵢ 
> ...`),
> and compute the closure of `->` w.r.t. `t` and the closure of `->v`.

This is basically what redex does, but perhaps not in the way you mean it.

What I'm saying is that when redex sees a language with n
non-terminals, it computes n^2 new non-terminals, one for each pair.
For the pair (x,y), it has a pattern that is internally `(cross x-y)`
(or something like that). This non-terminal corresponds with putting a
hole at each place in `x` where there is a reference to `y` (which
requires duplicating productions in general, repeating each production
once for each occurrence of `y` in a given production, allowing the
hole to be there).

In the earlier example when I wrote out the two non-terminals, TT was
`(cross t-t)` and TV was `(cross t-v)`. And when you do compatible
closure of `t`, redex uses `(cross t-t)`.

(I hope this makes a little bit more sense.)

Robby

-- 
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/CAL3TdONnd1j%3DDRrQOD6SqoP3doRQHhZb7ex8CxZ04fbz4MUgWw%40mail.gmail.com.
For more options, visit https://groups.google.com/d/optout.

[racket-users] Re: how do you read, manipulate, debug scope sets?

[Michael Ballantyne]

It's not an answer to your broader question, but I suspect what you 
actually want here is

#+begin_src racket
  ;; inside syntax-parse
  (datum->syntax this-syntax '<~)
#+end_src

Notice that the second argument to datum->syntax should be a symbol here, 
rather than a syntax object. If you provide a syntax object as you did in 
your original code, datum->syntax simply returns that syntax unchanged.

I don't expect using syntax-local-introduce will work reliably; before the 
change to the scope sets model of hygiene in Racket 6.3 it was another way 
to accomplish this purpose, but no longer.  For example, it breaks when the 
macro introducing the binding and its use are in different modules. Below, 
(m introduced) works in a but fails in b.

#+begin_src racket
#lang racket

(module a racket
  (define-syntax (m stx)
(syntax-case stx ()
  [(_ body)
   (with-syntax ([introduced (syntax-local-introduce #'introduced)])
 #'(let ([introduced 5])
 body))]))
  (m introduced)
  (provide m))

(module b racket
  (require (submod ".." a))
  (m introduced))
#+end_src

If you haven't read the papers describing Racket's hygiene algorithm and 
module system, you might find them helpful. The documentation isn't enough 
on its own, unfortunately.

For hygiene: http://www.cs.utah.edu/plt/scope-sets/
For phasing: https://www.cs.utah.edu/plt/publications/macromod.pdf 

On Monday, May 6, 2019 at 10:53:33 AM UTC-4, zeRusski wrote:
>
> I wrote a macro which introduced an implicit binding <~ so that it could 
> be used
> in expressions at the use-site. Initially did it with
>
> #+begin_src racket
>   ;; inside syntax-parse
>   (datum->syntax this-syntax #'<~)
> #+end_src
>
> followed by macro introduced expr that binds it, then the use-site 
> macro-input
> that uses it. Think (let/ec <~ macro-input-body).
>
> Worked just fine when tested at top-level or module begin or in expression
> position, but then suddenly broke when I wrote another define-like macro 
> whose
> body expanded into the macro above. Turns out scopes of <~ at use-site and 
> one I
> introduced in a macro didn't match, at least that's what I surmount from 
> the
> message below. I was originally going to ask if someone could teach me to 
> read
> these messages, but then I found ~syntax-debug-info~ in docs :) and IIUC 
> the
> message below tells me there are two identifier bindings where the error 
> occurs
> whose scope-sets share some scopes namely "common scopes ...", but neither 
> one's
> scope-set is a subset of the other hence the error. Am I reading it right?
>
> #+begin_src racket
> ; /Users/russki/Code/tilda/prelude/tilda.rkt:303:20: <~: unbound identifier
> ;   in: <~
> ;   context...:
> ;#(2212719 use-site) #(2212754 intdef) #(2212808 local)
> ;#(2212809 intdef) [common scopes]
> ;   other binding...:
> ;local
> ;#(2212718 macro) [common scopes]
> ;   common scopes...:
> ;#(2198084 module) #(2198091 module tilda) #(2212726 local)
> ;#(2212727 intdef) #(2212737 local) #(2212738 intdef) #(2212741 local)
> ;#(2212742 intdef) #(2212745 local) #(2212746 intdef) #(2212749 local)
> ;#(2212750 intdef) #(2212753 local)
> #+end_src
>
> I fixed the above with some guesswork that amounted to replacing 
> datum->syntax
> with
>
> #+begin_src racket
>   (syntax-local-introduce #'<~)
> #+end_src
>
> which IIUC simply flips the scopes so now <~ is use-site and may as well 
> be part
> of the macro input. Right?
>
> Suddenly I find myself playing games with hygiene and not really knowing 
> the
> rules.
>
> Are there any tutorials that show you how to use things documented in 
> Syntax
> Transformers chapter of the Reference?
>
> How do you debug these scope games?
>
> How do you introduce or capture identifier bindings (break hygiene)?
>
> Can you temporarily unbind an identifier (for the extent of some expr), so
> basically remove or trim some scopes from identifiers that occur in macro 
> input? I
> suppose there are several possible cases here: 
> - trim or replace scopes of ids whose sets match those at use-site, 
> guessing this
>   won't unbind "shadowing" identifiers (let or define introduced in your 
> macro
>   input) i.e. those with extra scopes in addition to use-site,
> - how do we deal with those, could we trim ids whose scope sets are 
> supersets of
>   use-site?
> - assuming I know how to do the above, do I walk the syntax tree and trim 
> those
>   scopes every time I find matching id or is there a better way?
>
> At this point I'd like to better understand how to manipulate sets of 
> scopes and
> verify the result. Could someone kindly teach me or point out good reads or
> examples?
>
> Thanks
>
>

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

Re: [racket-users] Re: tilda - a threading macro full of itself

[Greg Hendershott]

> I like this. Reminds me of `rackjure/threading`, but more involved.

A few years ago, after Alexis released

  https://github.com/lexi-lambda/threading

I updated rackjure to re-provide that.

Speaking of which, a couple issues there might be interesting for you,
Vlad.

For example, it's better if a threading macro expands using the `#%app`
bound at the macro use site. (Whereas by default, macros expand using
identifiers bound where the macro is defined.)

  https://github.com/lexi-lambda/threading/issues/3

Also you might want to treat `quote` forms specially, and not "thread
into" them.

  https://github.com/lexi-lambda/threading/issues/2

-- 
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/87r29axhzq.fsf%40greghendershott.com.
For more options, visit https://groups.google.com/d/optout.

Re: [racket-users] tilda - a threading macro full of itself

[zeRusski]

>
> It just names the threaded value. Did I overlook anything?


That's right, nothing fancy. Think let-binding the threaded value at that 
point. #:with id ~ would achieve the same thing, so as it is now #:as is 
redundant. With #:do both #:with and #:as are redundant, really.
 

> Let me point out that if ~> specified an identifier (as suggested in my 
> first response) you could co-mingle two threaded computations, keeping 
> separate concerns that don’t matter as opposed to bundling them up in 
> structs or lists or whatever you have to do if you have only one. At first 
> I thought #:as would you let you do so, but that’s not correct.


Ok, this one I don't quite understand. My first thought went as far as to 
weave multiple computations where each #:as would capture continuations and 
macro would keep these "threads" separate, but now I'm thinking you mean 
this:

(~> 1 #:as ~a
;; now ~a is being threaded
(add1 ~a)   ;=> 2
2 #:as ~b
;; now ~b is being threaded
(add1 ~b)   ;=> 3
;; simply use whatever ~a was last
(+ ~a ~b)   ;=> 5
#:as ~a
;; continue to thread ~a
(add1 ~a)   ;=> 3
(list ~a ~b))
;; => (list 3 5)

but then I think you can achieve this with current #:as semantics since a 
clause without a hole simply starts computation from that clause yet 
preserves any #:as bound vars in scope, so I'm guessing I'm way off. Could 
you expand please? 

-- 
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/c580880e-6551-44c0-b144-79c32faaefe8%40googlegroups.com.
For more options, visit https://groups.google.com/d/optout.

[racket-users] Re: tilda - a threading macro full of itself

[Lehi Toskin]

I like this. Reminds me of `rackjure/threading`, but more involved.

-- 
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/7b1ae615-3398-4620-96b9-ecc9cdd2603a%40googlegroups.com.
For more options, visit https://groups.google.com/d/optout.

Re: [racket-users] tilda - a threading macro full of itself

[zeRusski]

>
> It just names the threaded value. Did I overlook anything?


That's right, nothing fancy. Think let-binding the threaded value at that 
point. #:with id ~ would achieve the same thing, so as it is now #:as is 
redundant. With #:do both #:with and #:as are redundant, really.
 

> Let me point out that if ~> specified an identifier (as suggested in my 
> first response) you could co-mingle two threaded computations, keeping 
> separate concerns that don’t matter as opposed to bundling them up in 
> structs or lists or whatever you have to do if you have only one. At first 
> I thought #:as would you let you do so, but that’s not correct.


Ok, this one I don't quite understand. My first thought went as far as to 
weave multiple computations where each #:as would capture continuations and 
macro would keep these "threads" separate, but now I'm thinking you mean 
this:

(~> 1 #:as ~a
;; now ~a is being threaded
(add1 ~a)   ;=> 2
2 #:as ~b
;; now ~b is being threaded
(add1 ~b)   ;=> 3
;; simply use whatever ~a was last
(+ ~a ~b)   ;=> 5
#:as ~a
;; continue to thread ~a
(add1 ~a)   ;=> 3
(list ~a ~b))
;; => (list 3 5)

but then I think you can achieve this with current #:as semantics since a 
clause without a hole simply starts computation from that clause yet 
preserves any #:as bound vars in scope, so I'm guessing I'm way off. Could 
you expand please? 

-- 
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/ad4b7d46-5b3f-42b4-b50d-019c786de63e%40googlegroups.com.
For more options, visit https://groups.google.com/d/optout.

Re: [racket-users] https://lists.racket-lang.org/ is throwing a security exception

[David Storrs]

No worries, just figured I'd pass it along.  Thanks for the rapid fix.

On Mon, May 6, 2019 at 12:59 PM Stephen Chang  wrote:

> https for lists.racket-lang is not working at the moment. Sorry for
> the inconvenience. The server hosting lists.racket-lang went down
> recently. A partial temporary non-https version is up but https hasnt
> been enabled yet.
>
> On Mon, May 6, 2019 at 12:48 PM David Storrs 
> wrote:
> >
> > I'm not sure if this is relevant or not, but figured I'd mention it.  Is
> that supposed to be working, or is it obsolete?  It does turn up in Google
> searches, so maybe worth thinking about.
> >
> > --
> > 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.
> > For more options, visit https://groups.google.com/d/optout.
>

-- 
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/CAE8gKodUNBG7za7iGaV1ut7i9y8SEuYtmPGNtKyJPsBbZMVfqw%40mail.gmail.com.
For more options, visit https://groups.google.com/d/optout.

Re: [racket-users] tilda - a threading macro full of itself

[Matthias Felleisen]

> On May 7, 2019, at 9:39 AM, zeRusski  wrote:
> 
> I asked in a separate thread how one debugs set of scopes in Racket macros. I 
> appreciate the question may read a bit hand-wavy and abstract, so I split out 
> the piece of code I had in mind into a separate package so that interested 
> Racketeers could have a look and their time permitting maybe even suggest 
> improvements.
> 
> Tilda is nothing but an opinionated threading macro. Even though "threading" 
> macros punctuate all of my Clojure code I've been mostly making do without 
> them in Racket. I was just being lazy tbh. I finally caved but instead of 
> using off the shelf implementation I turned this into a nice exercise in 
> macrology.
> 
> https://github.com/vkz/tilda
> 
> README shows off its capabilities with silly but hopefully sufficient 
> examples.
> 
> If you have 5-10min on your hands and would like to help me learn, I'd 
> appreciate PRs that improve or critique my code. Obviously, feel free to 
> write here, but Github may provide a nicer interface to discuss code.
> 
> Also, see if you can break it:
> - break scoping rules,
> - hit an error that doesn't point to correct location with errortrace on etc.


Let me point out that if ~> specified an identifier (as suggested in my first 
response) you could co-mingle two threaded computations, keeping separate 
concerns that don’t matter as opposed to bundling them up in structs or lists 
or whatever you have to do if you have only one. At first I thought #:as would 
you let you do so, but that’s not correct. It just names the threaded value. 
Did I overlook anything? 

— Matthias

-- 
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/9E6E2826-4DF8-419F-8321-3E4D432F3D5F%40felleisen.org.
For more options, visit https://groups.google.com/d/optout.

[racket-users] tilda - a threading macro full of itself

[zeRusski]

I asked in a separate thread how one debugs set of scopes 
 in 
Racket macros. I appreciate the question may read a bit hand-wavy and 
abstract, so I split out the piece of code I had in mind into a separate 
package so that interested Racketeers could have a look and their time 
permitting maybe even suggest improvements.

Tilda is nothing but an opinionated threading macro. Even though 
"threading" macros punctuate all of my Clojure code I've been mostly making 
do without them in Racket. I was just being lazy tbh. I finally caved but 
instead of using off the shelf implementation I turned this into a nice 
exercise in macrology.

https://github.com/vkz/tilda

README shows off its capabilities with silly but hopefully sufficient 
examples.

If you have 5-10min on your hands and would like to help me learn, I'd 
appreciate PRs that improve or critique my code. Obviously, feel free to 
write here, but Github may provide a nicer interface to discuss code.

Also, see if you can break it:
- break scoping rules,
- hit an error that doesn't point to correct location with errortrace on 
etc.

Thanks


-- 
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/4f36682c-f2f4-44a2-89f7-55ee00b1151b%40googlegroups.com.
For more options, visit https://groups.google.com/d/optout.

Re: [racket-users] how do you read, manipulate, debug scope sets?

[zeRusski]

Thanks Matthew I'll have a look
>
>
All:
I published a link to the code I had in mind in a separate thread 
, so if 
interested check it out. I don't want to pollute this one if someone takes 
on the challenge of answering in more general terms.

-- 
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/43bf4832-e649-4e08-9151-7a02277ee4ce%40googlegroups.com.
For more options, visit https://groups.google.com/d/optout.