@leafac : the rules for the single step overlap with the rule that breaks out the and.

And then the rules don’t work because there are no contexts.

I’m getting build errors during making for <pkgs>/racket-benchmarks/tests/racket/benchmarks/shootout/typed – and it looks like the Utah snapshot build failed for that reason, too. Known problem?

@robby:

> the rules for the single step overlap with the rule that breaks out the and.

You mean that and and concat are resolved by the same reduction relation? In fact, if I were to write that, I would define a concat meta-function. Because the meta-function execution would not take one node in the reduction graph.

> And then the rules don’t work because there are no contexts.

What do you mean by “contexts?” I still don’t see where it would break. Can you please explain some more? Or at least point me what I need to learn?

Thank you so much for your time :slightly_smiling_face:

@leafac mostly what I’m saying is that you should give a try. Redex will be your guide! Plus, there are more interesting things to discover if you want to work up to actually making add work.

That said, let me try to at least explain what I meant with those specific comments.

(give me a sec to write some code)

With this definition (the one I was hinting at above):

#lang racket
(require redex)
(define-language L
  (e ::=
     (b ...)
     (and e e)
     (concat e ...))
  (b ::= 0 1))

(define red
  (reduction-relation
   L
   (--> (and (b_1 ...) (b_2 ...))
        (concat (and (b_1) (b_2)) ...))
   (--> (concat (b ...) ...)
        (b ... ...))
   (--> (and (0) (b)) (0))
   (--> (and (b) (0)) (0))
   (--> (and (1) (1)) (1))))

(traces
 red
 (term (and (1 0 1 0) (0 0 1 1))))

you get only one step; the last three rules don’t fire because they don’t have a context around them.

Now we can fix that by introducing and using E:

#lang racket
(require redex)
(define-language L
  (e ::=
     (b ...)
     (and e e)
     (concat e ...))
  (b ::= 0 1)
  (v ::= (b ...))
  (E ::= hole
     (and v E)
     (and E e)
     (concat v ... E e ...)))

(define red
  (reduction-relation
   L
   (--> (in-hole E (and (b_1 ...) (b_2 ...)))
        (in-hole E (concat (and (b_1) (b_2)) ...)))
   (--> (in-hole E (concat (b ...) ...))
        (in-hole E (b ... ...)))
   (--> (in-hole E (and (0) (b))) (in-hole E (0)))
   (--> (in-hole E (and (b) (0))) (in-hole E (0)))
   (--> (in-hole E (and (1) (1))) (in-hole E (1)))))


(traces
 red
 (term (and (1 0 1 0) (0 0 1 1))))

but now things go crazy.

indeed, there are infinite reduction sequences there that probably we don’t want.

I’ll let you try to fix that one, but the main hint is already there, namely that there is an overlap in the rules. Find the overlap and figure out which part you don’t really want.

Feel free to ask if you have more questions on this! I found it fun to work through this the first time I did it. :slightly_smiling_face:

@mflatt: Haven’t seen that. Will try it today.

http://classicprogrammerpaintings.com/post/158510621362/lightly-tested-hotfix-just-deployed-to-production

nice, reminds me of Jakob Rehof’s POPL 2017 slides http://www-seal.cs.tu-dortmund.de/seal/downloads/rehof/research_papers/POPL2017.pdf

“it took me a while to find a picture to describe ‘subject reduction’, but I think this one by Andy Warhol does the trick”

for anyone reading this down the road — should be fixed by https://github.com/racket/typed-racket/pull/514

@pnwamk: Thanks!

@robby: Thank you for your answer. I try to solve this and get back to you :slightly_smiling_face:

I had a lot of fund with that one :slightly_smiling_face:

@robby: I think I get it. I changed the first rule in the reduction relation to only fire if the input lists are larger than 1. One way is to use a side-condition, or use more variables, like I did here:

(--> (in-hole E (and (b_1 b_2 b_3 ...) (b_4 b_5 b_6 ...)))
        (in-hole E (concat (and (b_1) (b_4)) (and (b_2) (b_5)) (and (b_3) (b_6)) ...)))

right

(Ideally, Redex would support …+ patterns, like syntax-parse. But it doesn’t.)

Well, now is the time when I point out the design constraints on Redex.

Namely that it match the way people write stuff in papers.

And …+ is not a common notation in the PL research papers, I would say.

Or, maybe it is, in which case I’d add it.

I suggest you try some random testing.

write somethign that translates arrays of booleans to numbers and then throw it at racket

(turn and into bitwise-and or whatever that function is called)

(turn and into bitwise-...... ….)

:+1: I understand the design decision. It’s a good one :slightly_smiling_face: And there are always side-conditions.

you will find one bug that, I think.

Yes, a common thing in papers is something like

\|(b…)\| > 1 or something

And that’s just one typesetting rewrite away from a side-condition implmented via length.

(via racket’s length function)

Sure :slightly_smiling_face:

@robby:

> write somethign that translates arrays of booleans to numbers and then throw it at racket > (turn and into bitwise-and or whatever that function is called)

I understand you proposed something like the following:

(define-metafunction L
  reverse : (b ...) -> (b ...)
  [(reverse ()) ()]
  [(reverse (b_1 b_2 ...)) (b_3 ... b_1) (where (b_3 ...) (reverse (b_2 ...)))])

(define-metafunction L
  bs->integer : (b ...) -> integer
  [(bs->integer (b ...)) (bs->integer* (reverse (b ...)) 0)])

(define-metafunction L
  bs->integer* : (b ...) integer -> integer
  [(bs->integer* () integer) 0]
  [(bs->integer* (b_1 b_2 ...) integer)
   ,(+ (* (expt 2 (term integer)) (term b_1))
       (term (bs->integer* (b_2 ...) ,(add1 (term integer)))))])

(define red
  (reduction-relation
   L
   (--> (and (b_1 ...) (b_2 ...))
        ,(bitwise-and (term (bs->integer (b_1 ...))) (term (bs->integer (b_2 ...)))))))

But I believe my understanding is wrong. Can you clarify?