@robby I’m starting a lang from scratch and not looking at my previous code to see how much I’m getting… I spent way too long last night trying to debug “can’t find a hole in this expr”, which blows out compilation and thus prevents any exploration in the repl. Are there strategies for this (besides “get more sleep”). Something more to the effect of “I can’t even see v” vs “can’t find a hole” would help, but are there hints or tips?

I’m not familiar with that error message

Are you seeing something like the error message this program produces?

#lang racket
(require redex)

(define-language Q
  (E ::=
     (+ e e)
     hole))

(define r
  (reduction-relation
   Q
   (--> (in-hole E (+ 1 2))
        (in-hole E 3))))

Dinner at 6:00pm this evening, here’s a map https://goo.gl/maps/xo8BXvjfAPJ2 – expect to spend about 30 minutes to get from the TRAX station near the dorm to the restaurant, and we’ll end a little early today

I think that’s M expressing some strong opinions re types

https://www.youtube.com/watch?v=JBmIQIZPaHY

extracurricular things to do : music and mountains

Thursday July 13 8pm – 11pm Alan Michael Band (jazz saxophonist from New York, my wife plays in this band) The Garage on Beck http://www.garageonbeck.com/directions

Saturday July 15 NOON–6pm Cirque Series Race (mountain race — or hike) Alta, Utah https://www.facebook.com/events/688612277988942/

Saturday July 15 6:30pm – 8:30pm Better Off With The Blue (blues band - I play bass in this band) Feldman’s Deli http://www.feldmansdeli.com/home

Saturday July 15 9:30pm – 12:30am Alan Michael Band (I will be subbing on bass) https://www.utahbayou.com/location

If this talk interests you: http://www.greghendershott.com/fear-of-macros/

Isn’t this a kind of antisyntactic thing, like was mentioned in the talk yesterday afternoon? You can’t even tell what define or quote are until you’re about to run them

(No value judgment here, just observation)

well, when we compile them (in Racket), I guess

that happens when ‘compiler’ runs the compile-time function at least at runtime that .. we know them

@joergen7 here:

(define-syntax (hello stx)
  (syntax-parse stx
    [(_ id:id) #'(define id 'world)]
    [(_ (quote id:id)) #'(hello id)]))
(hello 'y)
y

@twisol A difference is that the scope of redefinitions is well-defined, so while quote may be redefined within a module, there’s no way to change the meaning of quote in any existing module (without changing that module or something that it imports)

Ahh, that makes sense. Thanks!

at some point I need to really understand the full power of the modules (esp submodules)… instantiation for example seems like voodoo and I have yet to find good doco for it

@mflatt eg… this required a lot of help from you to dynamically create and instantiate a module: https://gist.github.com/zenspider/6c4e50cdea9925f706ac1ff0019e3105

I don’t know if that implies missing (or confusing) doco or a missing function/macro

“It’s hard, unlike types!” :smile:

so will the canonical solutions to all the exercises be made available somewhere?

Hello @robby

In the language I am modeling, recusive function definitions are stated:

 (rec x (λ (x) e))

and reduced via:

(—> (prog Π (in-hole E ((rec x_1 (λ (x_2) e_1)) v_1))) (prog Π (in-hole E ((λ (x_2) e_2) v_1))) (where e_2 (subst [((rec x_1 (λ (x_2) e_1)) x_1)] e_1))

QUESTION: Is it possible to state that the body e refers to both x_1 and x_2?

#:binding-forms (rec x_1 (λ (x_2) e #:refers-to x_2)) ;; AND e #:refers-to x_1

@haroldcarr use shadow

#:refers-to (shadow x_1 x_2)

(or maybe in the other order; try it out to see which one should count as the inner binding)

the intuition I get from the name shadow does not match what I am trying to do. I want e to refer to BOTH x_1 and x_2 — and those two vars should be unique.

I looked up the redex doc for shadow - does not give any info.

Spoke too soon - I see more info on shadow - but still not clear.

@haroldcarr look up at yesterday’s convo… there was a code sample (inline) that may help

my understanding now is: e #:refers-to (shadow x_1 x_2) says e should refer to ALL the variables mentions in shadow - and if any of the variables have the same name, pick the leftmost one. Right?

@haroldcarr : correct

debug metalanguage: https://github.com/AlexKnauth/debug

Re: syntax-parse and literals http://macrologist.blogspot.com/2011/09/syntax-parse-and-literals.html?m=1

could anyone send me a map location? Lost u near the temple

redex-match says “The procedure accepts a single term and returns #f or a list of match structures describing the matches.” but that seems false:

    (test-equal (redex-match Lambda (if #f e_1 e_2) e13)
                (term (list (match (list (bind 'e_1 1) (bind 'e_2 2))))))

produces:

  actual: (list (match (list (bind 'e_1 1) (bind 'e_2 2))))
expected: '(list (match (list (bind 'e_1 1) (bind 'e_2 2))))

?? how to write a test using test-equal and test-equal? Or what’s the proper alternative? I basically want to do the part Robby suggested where you start up at e and go down in pattern or remove part of the term until it matches the way you think it should.