Re: [racket-dev] Announcing Soft Contract Verification tool
On Jan 15, 2015, at 11:13 AM, David Van Horn dvanh...@cs.umd.edu wrote: On 1/15/15, 11:04 AM, Matthias Felleisen wrote: Well that got me all excited. So I tried to get the sample module to pass the verification step -- until I realized how restricted the grammar is! (module f racket (provide (contract-out [f (real? . - . integer?)])) (define (f n) (/ 1 (- 100 n I would love to be able to use at least (and/c real? (/c 0)) for the domain so I can get the example done. Or am I overlooking a way to make this work here? The /c contract is there, but missing from the grammar (we'll fix that). But (/c 0) will not make this program verify. You want this contract: ((and/c real? (lambda (x) (not (= x 100 . - . real?) Using this contract, the program verifies. My contract is stronger than yours. So why will it not go through? _ Racket Developers list: http://lists.racket-lang.org/dev
Re: [racket-dev] Announcing Soft Contract Verification tool
On 1/15/15, 11:27 AM, Matthias Felleisen wrote: Argh, I wanted the other way (negative). I always get the directions confused. Sorry. Right -- using (and/c real? (/c 0)) will also make this verify. Thanks for trying it out! David On Jan 15, 2015, at 11:26 AM, David Van Horn dvanh...@cs.umd.edu wrote: On 1/15/15, 11:17 AM, Matthias Felleisen wrote: On Jan 15, 2015, at 11:13 AM, David Van Horn dvanh...@cs.umd.edu wrote: On 1/15/15, 11:04 AM, Matthias Felleisen wrote: Well that got me all excited. So I tried to get the sample module to pass the verification step -- until I realized how restricted the grammar is! (module f racket (provide (contract-out [f (real? . - . integer?)])) (define (f n) (/ 1 (- 100 n I would love to be able to use at least (and/c real? (/c 0)) for the domain so I can get the example done. Or am I overlooking a way to make this work here? The /c contract is there, but missing from the grammar (we'll fix that). But (/c 0) will not make this program verify. You want this contract: ((and/c real? (lambda (x) (not (= x 100 . - . real?) Using this contract, the program verifies. My contract is stronger than yours. So why will it not go through? 100 is (/c 0) but (f 100) divides by zero. David _ Racket Developers list: http://lists.racket-lang.org/dev
Re: [racket-dev] Announcing Soft Contract Verification tool
FWIW, (/c 0) already implies real?. Robby On Thu, Jan 15, 2015 at 10:30 AM, David Van Horn dvanh...@cs.umd.edu wrote: On 1/15/15, 11:27 AM, Matthias Felleisen wrote: Argh, I wanted the other way (negative). I always get the directions confused. Sorry. Right -- using (and/c real? (/c 0)) will also make this verify. Thanks for trying it out! David On Jan 15, 2015, at 11:26 AM, David Van Horn dvanh...@cs.umd.edu wrote: On 1/15/15, 11:17 AM, Matthias Felleisen wrote: On Jan 15, 2015, at 11:13 AM, David Van Horn dvanh...@cs.umd.edu wrote: On 1/15/15, 11:04 AM, Matthias Felleisen wrote: Well that got me all excited. So I tried to get the sample module to pass the verification step -- until I realized how restricted the grammar is! (module f racket (provide (contract-out [f (real? . - . integer?)])) (define (f n) (/ 1 (- 100 n I would love to be able to use at least (and/c real? (/c 0)) for the domain so I can get the example done. Or am I overlooking a way to make this work here? The /c contract is there, but missing from the grammar (we'll fix that). But (/c 0) will not make this program verify. You want this contract: ((and/c real? (lambda (x) (not (= x 100 . - . real?) Using this contract, the program verifies. My contract is stronger than yours. So why will it not go through? 100 is (/c 0) but (f 100) divides by zero. David _ Racket Developers list: http://lists.racket-lang.org/dev _ Racket Developers list: http://lists.racket-lang.org/dev
Re: [racket-dev] Announcing Soft Contract Verification tool
On 1/15/15, 11:04 AM, Matthias Felleisen wrote: Well that got me all excited. So I tried to get the sample module to pass the verification step -- until I realized how restricted the grammar is! (module f racket (provide (contract-out [f (real? . - . integer?)])) (define (f n) (/ 1 (- 100 n I would love to be able to use at least (and/c real? (/c 0)) for the domain so I can get the example done. Or am I overlooking a way to make this work here? The /c contract is there, but missing from the grammar (we'll fix that). But (/c 0) will not make this program verify. You want this contract: ((and/c real? (lambda (x) (not (= x 100 . - . real?) Using this contract, the program verifies. David _ Racket Developers list: http://lists.racket-lang.org/dev
Re: [racket-dev] Announcing Soft Contract Verification tool
On 1/15/15, 11:17 AM, Matthias Felleisen wrote: On Jan 15, 2015, at 11:13 AM, David Van Horn dvanh...@cs.umd.edu wrote: On 1/15/15, 11:04 AM, Matthias Felleisen wrote: Well that got me all excited. So I tried to get the sample module to pass the verification step -- until I realized how restricted the grammar is! (module f racket (provide (contract-out [f (real? . - . integer?)])) (define (f n) (/ 1 (- 100 n I would love to be able to use at least (and/c real? (/c 0)) for the domain so I can get the example done. Or am I overlooking a way to make this work here? The /c contract is there, but missing from the grammar (we'll fix that). But (/c 0) will not make this program verify. You want this contract: ((and/c real? (lambda (x) (not (= x 100 . - . real?) Using this contract, the program verifies. My contract is stronger than yours. So why will it not go through? 100 is (/c 0) but (f 100) divides by zero. David _ Racket Developers list: http://lists.racket-lang.org/dev
Re: [racket-dev] Announcing Soft Contract Verification tool
On 2015-01-15 14:13:02 -0500, Asumu Takikawa wrote: Contract violation: 'fact' violates '='. Value 0.105 violates predicate real? An example module that breaks it: (module user racket (require (submod .. fact)) (factorial 0.105)) (Verification takes 0.05s) Hmm, actually I should've looked at this more carefully. Is this a case where the tool is telling me that the function is non-terminating on this input? Cheers, Asumu _ Racket Developers list: http://lists.racket-lang.org/dev
Re: [racket-dev] Announcing Soft Contract Verification tool
I think this is saying that the result is going to be negative. (But it won't, since it doesn't terminate.) Robby On Thu, Jan 15, 2015 at 1:13 PM, Asumu Takikawa as...@ccs.neu.edu wrote: On 2015-01-14 19:11:59 -0500, David Van Horn wrote: If you have questions, comments, bugs, or any other feedback, let us know, or just file bug reports on the GitHub source code. Nice tool! I like the web interface too. I was confused by this interaction though. Clicking verify on this: (module fact racket (define (factorial x) (if (zero? x) 1 (* x (factorial (sub1 x) (provide (contract-out [factorial (- (=/c 0) (=/c 0))]))) gives me: Contract violation: 'fact' violates '='. Value 0.105 violates predicate real? An example module that breaks it: (module user racket (require (submod .. fact)) (factorial 0.105)) (Verification takes 0.05s) but the value 0.105 shouldn't violate the predicate real? I think. Cheers, Asumu _ Racket Developers list: http://lists.racket-lang.org/dev _ Racket Developers list: http://lists.racket-lang.org/dev
Re: [racket-dev] Announcing Soft Contract Verification tool
On 2015-01-14 19:11:59 -0500, David Van Horn wrote: If you have questions, comments, bugs, or any other feedback, let us know, or just file bug reports on the GitHub source code. Nice tool! I like the web interface too. I was confused by this interaction though. Clicking verify on this: (module fact racket (define (factorial x) (if (zero? x) 1 (* x (factorial (sub1 x) (provide (contract-out [factorial (- (=/c 0) (=/c 0))]))) gives me: Contract violation: 'fact' violates '='. Value 0.105 violates predicate real? An example module that breaks it: (module user racket (require (submod .. fact)) (factorial 0.105)) (Verification takes 0.05s) but the value 0.105 shouldn't violate the predicate real? I think. Cheers, Asumu _ Racket Developers list: http://lists.racket-lang.org/dev
Re: [racket-dev] Announcing Soft Contract Verification tool
Can you randomly make up programs from your grammar, get example errors from the tool, and then run those programs to see if you find bugs in the analysis like that one? That said, I don't see how the bug in =/c is coming in here. Can you explain more? Robby On Thu, Jan 15, 2015 at 1:42 PM, David Van Horn dvanh...@cs.umd.edu wrote: On 1/15/15, 2:13 PM, Asumu Takikawa wrote: On 2015-01-14 19:11:59 -0500, David Van Horn wrote: If you have questions, comments, bugs, or any other feedback, let us know, or just file bug reports on the GitHub source code. Nice tool! I like the web interface too. I was confused by this interaction though. Clicking verify on this: (module fact racket (define (factorial x) (if (zero? x) 1 (* x (factorial (sub1 x) (provide (contract-out [factorial (- (=/c 0) (=/c 0))]))) gives me: Contract violation: 'fact' violates '='. Value 0.105 violates predicate real? An example module that breaks it: (module user racket (require (submod .. fact)) (factorial 0.105)) (Verification takes 0.05s) but the value 0.105 shouldn't violate the predicate real? I think. This is reporting that the fact module can break the contract on = when it uses =/c; that's a bug in our modelling of =/c, which we currently have as: (define (=/c n) (lambda (m) (= m n))) But should be: (define (=/c n) (lambda (m) (and (real? m) (= m n That said, if you change it to (and/c real? (=/c 0)), it says there's a counterexample of 2.0, but that's because we check contracts on recursive calls (and should not). Thanks! David _ Racket Developers list: http://lists.racket-lang.org/dev _ Racket Developers list: http://lists.racket-lang.org/dev
Re: [racket-dev] Implementing contracts for async channels
As an update, I’ve made a bit more progress on this. I’ve implemented an impersonate-async-channel function, and I’ve actually included this in the exports from racket/contract. I also realized the blame information is correct, it works fine. Most of the other issues remain, as well as a few new questions: There is no impersonate-evt function, so I’m not sure that my implementation will work. What should I do about this? I’d assume this needs to be documented/tested as well. Where should those things be located? On Jan 14, 2015, at 23:44, Alexis King lexi.lam...@gmail.com wrote: Currently, async channels do not have contracts to check their contents. This is a problem for Typed Racket, and it prevents typed code from interacting with code that produces async channels. I started looking into how to add contracts to the language, and it seems to use the chaperones/impersonator system, as I suspected. However, async channels obviously cannot be impersonated, so I needed to implement that as well. I modified the async-channel struct to use generics to allow it to be impersonated or chaperoned, which I have exposed by implementing chaperone-async-channel. I then tried implementing async-channel/c. The internals of the contract system are a little beyond me, but I got a working solution by following the example of the box contracts. My work thus far can be found here: https://github.com/lexi-lambda/racket/commit/84b9f3604891f3f2061fb28ed4800af8afa4751b https://github.com/lexi-lambda/racket/commit/84b9f3604891f3f2061fb28ed4800af8afa4751b First of all, is this a correct approach? Have I done anything wrong, or should I have done anything differently? I didn’t find much documentation on the internals of either of these systems, so I mostly went about things as I found them. Second, obviously, not everything is implemented here. Among the additional necessary changes are: I need to implement support for impersonators and impersonator contracts (right now I’ve only bothered to do chaperones). I need to implement async-channel/c-first-order and async-channel/c-stronger. I can probably figure out the latter, but I’m not even sure what the former is supposed to do. I need to implement a wrap-async-channel/c macro for the export. I’m not sure how this works, either. From looking at wrap-box/c, it seems to add some syntax properties, but I’m not sure what they do or how they work. Somehow, the blame information has to be correct. Is that what the wrap function does? Or do the async-channel functions need to be updated to assign blame? I’d really like to get this working, and I think I’m close, but I’m a little inexperienced. I’d appreciate any help, even if it’s just pointing me in the right direction. Thanks! _ Racket Developers list: http://lists.racket-lang.org/dev
Re: [racket-dev] Implementing contracts for async channels
Sorry, I wasn’t clear. The chaperone/impersonate-async-channel functions are exported from racket/async-channel. The async-channel contracts, however, are exported from racket/contract. On Jan 15, 2015, at 14:41, Robby Findler ro...@eecs.northwestern.edu wrote: Just a small nit: why export that function from racket/contract and not an async-channel library? Robby On Thu, Jan 15, 2015 at 3:33 PM, Alexis King lexi.lam...@gmail.com wrote: As an update, I’ve made a bit more progress on this. I’ve implemented an impersonate-async-channel function, and I’ve actually included this in the exports from racket/contract. I also realized the blame information is correct, it works fine. Most of the other issues remain, as well as a few new questions: There is no impersonate-evt function, so I’m not sure that my implementation will work. What should I do about this? I’d assume this needs to be documented/tested as well. Where should those things be located? On Jan 14, 2015, at 23:44, Alexis King lexi.lam...@gmail.com wrote: Currently, async channels do not have contracts to check their contents. This is a problem for Typed Racket, and it prevents typed code from interacting with code that produces async channels. I started looking into how to add contracts to the language, and it seems to use the chaperones/impersonator system, as I suspected. However, async channels obviously cannot be impersonated, so I needed to implement that as well. I modified the async-channel struct to use generics to allow it to be impersonated or chaperoned, which I have exposed by implementing chaperone-async-channel. I then tried implementing async-channel/c. The internals of the contract system are a little beyond me, but I got a working solution by following the example of the box contracts. My work thus far can be found here: https://github.com/lexi-lambda/racket/commit/84b9f3604891f3f2061fb28ed4800af8afa4751b First of all, is this a correct approach? Have I done anything wrong, or should I have done anything differently? I didn’t find much documentation on the internals of either of these systems, so I mostly went about things as I found them. Second, obviously, not everything is implemented here. Among the additional necessary changes are: I need to implement support for impersonators and impersonator contracts (right now I’ve only bothered to do chaperones). I need to implement async-channel/c-first-order and async-channel/c-stronger. I can probably figure out the latter, but I’m not even sure what the former is supposed to do. I need to implement a wrap-async-channel/c macro for the export. I’m not sure how this works, either. From looking at wrap-box/c, it seems to add some syntax properties, but I’m not sure what they do or how they work. Somehow, the blame information has to be correct. Is that what the wrap function does? Or do the async-channel functions need to be updated to assign blame? I’d really like to get this working, and I think I’m close, but I’m a little inexperienced. I’d appreciate any help, even if it’s just pointing me in the right direction. Thanks! _ Racket Developers list: http://lists.racket-lang.org/dev _ Racket Developers list: http://lists.racket-lang.org/dev
Re: [racket-dev] Implementing contracts for async channels
I think they should probably all be exported from racket/async-channel. Unless there is some reason to modify the internals of racket/contract to support them? Robby On Thu, Jan 15, 2015 at 4:50 PM, Alexis King lexi.lam...@gmail.com wrote: Sorry, I wasn’t clear. The chaperone/impersonate-async-channel functions are exported from racket/async-channel. The async-channel contracts, however, are exported from racket/contract. On Jan 15, 2015, at 14:41, Robby Findler ro...@eecs.northwestern.edu wrote: Just a small nit: why export that function from racket/contract and not an async-channel library? Robby On Thu, Jan 15, 2015 at 3:33 PM, Alexis King lexi.lam...@gmail.com wrote: As an update, I’ve made a bit more progress on this. I’ve implemented an impersonate-async-channel function, and I’ve actually included this in the exports from racket/contract. I also realized the blame information is correct, it works fine. Most of the other issues remain, as well as a few new questions: There is no impersonate-evt function, so I’m not sure that my implementation will work. What should I do about this? I’d assume this needs to be documented/tested as well. Where should those things be located? On Jan 14, 2015, at 23:44, Alexis King lexi.lam...@gmail.com wrote: Currently, async channels do not have contracts to check their contents. This is a problem for Typed Racket, and it prevents typed code from interacting with code that produces async channels. I started looking into how to add contracts to the language, and it seems to use the chaperones/impersonator system, as I suspected. However, async channels obviously cannot be impersonated, so I needed to implement that as well. I modified the async-channel struct to use generics to allow it to be impersonated or chaperoned, which I have exposed by implementing chaperone-async-channel. I then tried implementing async-channel/c. The internals of the contract system are a little beyond me, but I got a working solution by following the example of the box contracts. My work thus far can be found here: https://github.com/lexi-lambda/racket/commit/84b9f3604891f3f2061fb28ed4800af8afa4751b First of all, is this a correct approach? Have I done anything wrong, or should I have done anything differently? I didn’t find much documentation on the internals of either of these systems, so I mostly went about things as I found them. Second, obviously, not everything is implemented here. Among the additional necessary changes are: I need to implement support for impersonators and impersonator contracts (right now I’ve only bothered to do chaperones). I need to implement async-channel/c-first-order and async-channel/c-stronger. I can probably figure out the latter, but I’m not even sure what the former is supposed to do. I need to implement a wrap-async-channel/c macro for the export. I’m not sure how this works, either. From looking at wrap-box/c, it seems to add some syntax properties, but I’m not sure what they do or how they work. Somehow, the blame information has to be correct. Is that what the wrap function does? Or do the async-channel functions need to be updated to assign blame? I’d really like to get this working, and I think I’m close, but I’m a little inexperienced. I’d appreciate any help, even if it’s just pointing me in the right direction. Thanks! _ Racket Developers list: http://lists.racket-lang.org/dev _ Racket Developers list: http://lists.racket-lang.org/dev
Re: [racket-dev] Implementing contracts for async channels
Just a small nit: why export that function from racket/contract and not an async-channel library? Robby On Thu, Jan 15, 2015 at 3:33 PM, Alexis King lexi.lam...@gmail.com wrote: As an update, I’ve made a bit more progress on this. I’ve implemented an impersonate-async-channel function, and I’ve actually included this in the exports from racket/contract. I also realized the blame information is correct, it works fine. Most of the other issues remain, as well as a few new questions: There is no impersonate-evt function, so I’m not sure that my implementation will work. What should I do about this? I’d assume this needs to be documented/tested as well. Where should those things be located? On Jan 14, 2015, at 23:44, Alexis King lexi.lam...@gmail.com wrote: Currently, async channels do not have contracts to check their contents. This is a problem for Typed Racket, and it prevents typed code from interacting with code that produces async channels. I started looking into how to add contracts to the language, and it seems to use the chaperones/impersonator system, as I suspected. However, async channels obviously cannot be impersonated, so I needed to implement that as well. I modified the async-channel struct to use generics to allow it to be impersonated or chaperoned, which I have exposed by implementing chaperone-async-channel. I then tried implementing async-channel/c. The internals of the contract system are a little beyond me, but I got a working solution by following the example of the box contracts. My work thus far can be found here: https://github.com/lexi-lambda/racket/commit/84b9f3604891f3f2061fb28ed4800af8afa4751b First of all, is this a correct approach? Have I done anything wrong, or should I have done anything differently? I didn’t find much documentation on the internals of either of these systems, so I mostly went about things as I found them. Second, obviously, not everything is implemented here. Among the additional necessary changes are: I need to implement support for impersonators and impersonator contracts (right now I’ve only bothered to do chaperones). I need to implement async-channel/c-first-order and async-channel/c-stronger. I can probably figure out the latter, but I’m not even sure what the former is supposed to do. I need to implement a wrap-async-channel/c macro for the export. I’m not sure how this works, either. From looking at wrap-box/c, it seems to add some syntax properties, but I’m not sure what they do or how they work. Somehow, the blame information has to be correct. Is that what the wrap function does? Or do the async-channel functions need to be updated to assign blame? I’d really like to get this working, and I think I’m close, but I’m a little inexperienced. I’d appreciate any help, even if it’s just pointing me in the right direction. Thanks! _ Racket Developers list: http://lists.racket-lang.org/dev _ Racket Developers list: http://lists.racket-lang.org/dev
Re: [racket-dev] Implementing contracts for async channels
On Thu, Jan 15, 2015 at 4:33 PM, Alexis King lexi.lam...@gmail.com wrote: As an update, I’ve made a bit more progress on this. I’ve implemented an impersonate-async-channel function, and I’ve actually included this in the exports from racket/contract. I also realized the blame information is correct, it works fine. Most of the other issues remain, as well as a few new questions: There is no impersonate-evt function, so I’m not sure that my implementation will work. What should I do about this? I’d assume this needs to be documented/tested as well. Where should those things be located? Documentation for contracts is here: https://github.com/plt/racket/blob/master/pkgs/racket-doc/scribblings/reference/contracts.scrbl and in the dependent files. Tests for contracts are here: https://github.com/plt/racket/tree/master/pkgs/racket-test/tests/racket/contract Sam On Jan 14, 2015, at 23:44, Alexis King lexi.lam...@gmail.com wrote: Currently, async channels do not have contracts to check their contents. This is a problem for Typed Racket, and it prevents typed code from interacting with code that produces async channels. I started looking into how to add contracts to the language, and it seems to use the chaperones/impersonator system, as I suspected. However, async channels obviously cannot be impersonated, so I needed to implement that as well. I modified the async-channel struct to use generics to allow it to be impersonated or chaperoned, which I have exposed by implementing chaperone-async-channel. I then tried implementing async-channel/c. The internals of the contract system are a little beyond me, but I got a working solution by following the example of the box contracts. My work thus far can be found here: https://github.com/lexi-lambda/racket/commit/84b9f3604891f3f2061fb28ed4800af8afa4751b First of all, is this a correct approach? Have I done anything wrong, or should I have done anything differently? I didn’t find much documentation on the internals of either of these systems, so I mostly went about things as I found them. Second, obviously, not everything is implemented here. Among the additional necessary changes are: I need to implement support for impersonators and impersonator contracts (right now I’ve only bothered to do chaperones). I need to implement async-channel/c-first-order and async-channel/c-stronger. I can probably figure out the latter, but I’m not even sure what the former is supposed to do. I need to implement a wrap-async-channel/c macro for the export. I’m not sure how this works, either. From looking at wrap-box/c, it seems to add some syntax properties, but I’m not sure what they do or how they work. Somehow, the blame information has to be correct. Is that what the wrap function does? Or do the async-channel functions need to be updated to assign blame? I’d really like to get this working, and I think I’m close, but I’m a little inexperienced. I’d appreciate any help, even if it’s just pointing me in the right direction. Thanks! _ Racket Developers list: http://lists.racket-lang.org/dev _ Racket Developers list: http://lists.racket-lang.org/dev
Re: [racket-dev] question, issue(?) with the scope of identifiers passed into define-syntax-rule
Yes, I see some of this at the bottom of the chapter 16 in the guide, and the recursion supported with (require http://docs.racket-lang.org/reference/require.html#%28form._%28%28lib._racket%2Fprivate%2Fbase..rkt%29._require%29%29 (for-meta http://docs.racket-lang.org/reference/require.html#%28form._%28%28lib._racket%2Fprivate%2Fbase..rkt%29._for-meta%29%29 n racket/base)). On Fri, Jan 16, 2015 at 11:21 AM, Thomas Lynch thomas.ly...@reasoningtechnology.com wrote: Thank you for that nice explanation. I'm reminded of the scope variables carried in Ruby. In Mathematica the renaming of module variables is explicit. There do not appear to be run phases there. Also thanks for the working example using syntax parse. Thus far I have working examples using define-syntax via datum and define-syntax with case (thanks to Matthais). The following questions might best be answered by pointing me to some other docs, haven't run across yet: Are there more than two phases? There is the syntax phase, i.e. compile time phase, and then a run phase. Lexical scope at the syntax phase would be static based textual layout of the program - i.e. lexical scope. Then the macros (syntax transformers) are gone (as the syntax has been transformed) after the syntax phase. At run time then, we have no access to the syntax object information? Academic question, but can syntax information, or other values be shared across phases? As an example, could one store the file name, line, and column number for an identifier, the make use of that later? How is it that we do work inside of a macro, for example by making use of require-for-syntax? Does that imply that the routines that we make use of in the macro for doing work had their own syntax phase, and now they are in run time phase during the macro's syntax phase? .. then if those worker routines make use of macros ... seems this recursion could be arbitrarily deep. Can the syntax analysis be explicitly invoked? Sort of like (apply ...) or (eval ..) ? Come to think of it, eval must do the syntax phase, then the run phase, so perhaps it is calls to that which causes the recursion. On Fri, Jan 16, 2015 at 11:01 AM, Alexander D. Knauth alexan...@knauth.org wrote: But I think it’s important that it doesn’t use gensym or something like that, it uses syntax-marks, which means you can break these lexical scoping rules if you want/need to by using either syntax-local-introduce or datum-syntax: #lang racket (require syntax/parse/define) (define-simple-macro (with-tables stem body ...) #:with table-author-id (syntax-local-introduce #'table-author) (let([table-publication (string-append stem _publication)] [table-author-id (string-append stem _author)] [table-bridge-publication-author (string-append stem _bridge_publication_author)] [table-unique-counters (string-append stem _unique_counters)] ) body ... )) (with-tables x table-author) ;”x_author On Jan 15, 2015, at 9:23 PM, Alexander McLin alex.mc...@gmail.com wrote: Warning I am still a Racket intermediate user but I've been studying syntactic extensions a lot the past several months. The problem here is macros in Racket have lexical scope just like procedures, they are hygienic macros. The identifiers you introduced in the with-tables macro only exist or refer to other bindings in the same lexical scope as where you originally wrote the macro. When you invoke the macro and pass in table-author, even though it is spelled the same as the identifier you wrote in the macro definition, they are not the same. When the macro expands, hygiene is implemented by renaming all identifiers in the macro to unique non-clashing symbols that don't conflict with others existing in the scope the macro is expanding in. The table-author identifier in the macro in the let form is renamed to something different like g6271 or something along those lines. Furthermore, you need to be careful about what you mean by evaluation. In the presence of macros, you have the concept of syntax phase(or compile-time or expand-time) evaluation versus run-time evaluation. When the macro is expanding, it does it thing, processing the original syntax into the new piece of syntax that replaces what was there previously such as (with-tables x table-author) which is then finally evaluated during run-time. (with-tables x table-author) will expand into something looking similar to the following, just to give you an idea of what macro expansion looks like: (let ((g6191 (string-append x _publication)) (g6271 (string-append x _author)) (g6369 (string-append x _bridge_publication_author)) (g6445 (string-append x _unique_counters))) table-author) Note that the original table-author identifier has been replaced by a different identifier that still has the same binding you originally defined. The table-author identifier
Re: [racket-dev] Implementing contracts for async channels
Sure thing, done. I’ve moved everything into racket/async-channel, added the missing functions, and added some tests. I squashed my commits into one, and the result is here: https://github.com/lexi-lambda/racket/commit/0074ba13b712a87c9d05948ae075bcd74c7651e7 https://github.com/lexi-lambda/racket/commit/0074ba13b712a87c9d05948ae075bcd74c7651e7 Two simple points remain: Where should the documentation go? Should it be under contracts or async-channels? I’d prefer the latter, but I’m not sure. Since there is no impersonate-evt function, I don’t think my impersonate-async-channel function will actually work. Is that an accurate concern? How could I fix it? Otherwise, I think this works fine and is probably ready to go. On Jan 15, 2015, at 15:09, Robby Findler ro...@eecs.northwestern.edu wrote: I think they should probably all be exported from racket/async-channel. Unless there is some reason to modify the internals of racket/contract to support them? Robby On Thu, Jan 15, 2015 at 4:50 PM, Alexis King lexi.lam...@gmail.com wrote: Sorry, I wasn’t clear. The chaperone/impersonate-async-channel functions are exported from racket/async-channel. The async-channel contracts, however, are exported from racket/contract. On Jan 15, 2015, at 14:41, Robby Findler ro...@eecs.northwestern.edu wrote: Just a small nit: why export that function from racket/contract and not an async-channel library? Robby On Thu, Jan 15, 2015 at 3:33 PM, Alexis King lexi.lam...@gmail.com wrote: As an update, I’ve made a bit more progress on this. I’ve implemented an impersonate-async-channel function, and I’ve actually included this in the exports from racket/contract. I also realized the blame information is correct, it works fine. Most of the other issues remain, as well as a few new questions: There is no impersonate-evt function, so I’m not sure that my implementation will work. What should I do about this? I’d assume this needs to be documented/tested as well. Where should those things be located? On Jan 14, 2015, at 23:44, Alexis King lexi.lam...@gmail.com wrote: Currently, async channels do not have contracts to check their contents. This is a problem for Typed Racket, and it prevents typed code from interacting with code that produces async channels. I started looking into how to add contracts to the language, and it seems to use the chaperones/impersonator system, as I suspected. However, async channels obviously cannot be impersonated, so I needed to implement that as well. I modified the async-channel struct to use generics to allow it to be impersonated or chaperoned, which I have exposed by implementing chaperone-async-channel. I then tried implementing async-channel/c. The internals of the contract system are a little beyond me, but I got a working solution by following the example of the box contracts. My work thus far can be found here: https://github.com/lexi-lambda/racket/commit/84b9f3604891f3f2061fb28ed4800af8afa4751b First of all, is this a correct approach? Have I done anything wrong, or should I have done anything differently? I didn’t find much documentation on the internals of either of these systems, so I mostly went about things as I found them. Second, obviously, not everything is implemented here. Among the additional necessary changes are: I need to implement support for impersonators and impersonator contracts (right now I’ve only bothered to do chaperones). I need to implement async-channel/c-first-order and async-channel/c-stronger. I can probably figure out the latter, but I’m not even sure what the former is supposed to do. I need to implement a wrap-async-channel/c macro for the export. I’m not sure how this works, either. From looking at wrap-box/c, it seems to add some syntax properties, but I’m not sure what they do or how they work. Somehow, the blame information has to be correct. Is that what the wrap function does? Or do the async-channel functions need to be updated to assign blame? I’d really like to get this working, and I think I’m close, but I’m a little inexperienced. I’d appreciate any help, even if it’s just pointing me in the right direction. Thanks! _ Racket Developers list: http://lists.racket-lang.org/dev _ Racket Developers list: http://lists.racket-lang.org/dev
Re: [racket-dev] question, issue(?) with the scope of identifiers passed into define-syntax-rule
Warning I am still a Racket intermediate user but I've been studying syntactic extensions a lot the past several months. The problem here is macros in Racket have lexical scope just like procedures, they are hygienic macros. The identifiers you introduced in the with-tables macro only exist or refer to other bindings in the same lexical scope as where you originally wrote the macro. When you invoke the macro and pass in table-author, even though it is spelled the same as the identifier you wrote in the macro definition, they are not the same. When the macro expands, hygiene is implemented by renaming all identifiers in the macro to unique non-clashing symbols that don't conflict with others existing in the scope the macro is expanding in. The table-author identifier in the macro in the let form is renamed to something different like g6271 or something along those lines. Furthermore, you need to be careful about what you mean by evaluation. In the presence of macros, you have the concept of syntax phase(or compile-time or expand-time) evaluation versus run-time evaluation. When the macro is expanding, it does it thing, processing the original syntax into the new piece of syntax that replaces what was there previously such as (with-tables x table-author) which is then finally evaluated during run-time. (with-tables x table-author) will expand into something looking similar to the following, just to give you an idea of what macro expansion looks like: (let ((g6191 (string-append x _publication)) (g6271 (string-append x _author)) (g6369 (string-append x _bridge_publication_author)) (g6445 (string-append x _unique_counters))) table-author) Note that the original table-author identifier has been replaced by a different identifier that still has the same binding you originally defined. The table-author identifier you passed to the macro gets inserted in the body position and then the expanded code is evaluated at run-time and of course gives you a run-time error since table-author does not refer to anything and thus when it's evaluated, it is recognized as an undefined identifier. (with-tables x hello) works because what you get in return is: (let ((g6191 (string-append x _publication)) (g6271 (string-append x _author)) (g6369 (string-append x _bridge_publication_author)) (g6445 (string-append x _unique_counters))) hello) hello is just a self-evaluating string giving you back hello from within the let form. On Thu, Jan 15, 2015 at 12:12 AM, Thomas Lynch thomas.ly...@reasoningtechnology.com wrote: I have a simple syntax rule: Welcome to Racket v5.2.1. racket@ (define-syntax-rule (with-tables stem body ...) (let( [table-publication (string-append stem _publication)] [table-author (string-append stem _author)] [table-bridge-publication-author (string-append stem _bridge_publication_author)] [table-unique-counters (string-append stem _unique_counters)] ) body ... )) Which works fine when I don't reference the environment defined by the let: racket@ racket@ (with-tables x hello) hello However when I pass it an identifier corresponding to one of the variables defined in the let: racket@ (with-tables x table-author) reference to undefined identifier: table-author stdin::1167: table-author The identifier passed in doesn't seem to be part of the local let context, but carried in a different context, or perhaps it was evaluated as an operand. I didn't expect either of those. Can someone point me at a description of the expected behavior, or give me a tip here on what is happening and why. ... in Wolfram language there is a 'Hold' operator for situations like this. Apparently inside the macro we have to do some evaluation to handle the work of the macro, is that why the operand is evaluated? Thanks in advance for explaining the evaluation/context model here. Thomas _ Racket Developers list: http://lists.racket-lang.org/dev _ Racket Developers list: http://lists.racket-lang.org/dev
Re: [racket-dev] question, issue(?) with the scope of identifiers passed into define-syntax-rule
But I think it’s important that it doesn’t use gensym or something like that, it uses syntax-marks, which means you can break these lexical scoping rules if you want/need to by using either syntax-local-introduce or datum-syntax: #lang racket (require syntax/parse/define) (define-simple-macro (with-tables stem body ...) #:with table-author-id (syntax-local-introduce #'table-author) (let([table-publication (string-append stem _publication)] [table-author-id (string-append stem _author)] [table-bridge-publication-author (string-append stem _bridge_publication_author)] [table-unique-counters (string-append stem _unique_counters)] ) body ... )) (with-tables x table-author) ;”x_author On Jan 15, 2015, at 9:23 PM, Alexander McLin alex.mc...@gmail.com wrote: Warning I am still a Racket intermediate user but I've been studying syntactic extensions a lot the past several months. The problem here is macros in Racket have lexical scope just like procedures, they are hygienic macros. The identifiers you introduced in the with-tables macro only exist or refer to other bindings in the same lexical scope as where you originally wrote the macro. When you invoke the macro and pass in table-author, even though it is spelled the same as the identifier you wrote in the macro definition, they are not the same. When the macro expands, hygiene is implemented by renaming all identifiers in the macro to unique non-clashing symbols that don't conflict with others existing in the scope the macro is expanding in. The table-author identifier in the macro in the let form is renamed to something different like g6271 or something along those lines. Furthermore, you need to be careful about what you mean by evaluation. In the presence of macros, you have the concept of syntax phase(or compile-time or expand-time) evaluation versus run-time evaluation. When the macro is expanding, it does it thing, processing the original syntax into the new piece of syntax that replaces what was there previously such as (with-tables x table-author) which is then finally evaluated during run-time. (with-tables x table-author) will expand into something looking similar to the following, just to give you an idea of what macro expansion looks like: (let ((g6191 (string-append x _publication)) (g6271 (string-append x _author)) (g6369 (string-append x _bridge_publication_author)) (g6445 (string-append x _unique_counters))) table-author) Note that the original table-author identifier has been replaced by a different identifier that still has the same binding you originally defined. The table-author identifier you passed to the macro gets inserted in the body position and then the expanded code is evaluated at run-time and of course gives you a run-time error since table-author does not refer to anything and thus when it's evaluated, it is recognized as an undefined identifier. (with-tables x hello) works because what you get in return is: (let ((g6191 (string-append x _publication)) (g6271 (string-append x _author)) (g6369 (string-append x _bridge_publication_author)) (g6445 (string-append x _unique_counters))) hello) hello is just a self-evaluating string giving you back hello from within the let form. On Thu, Jan 15, 2015 at 12:12 AM, Thomas Lynch thomas.ly...@reasoningtechnology.com wrote: I have a simple syntax rule: Welcome to Racket v5.2.1. racket@ (define-syntax-rule (with-tables stem body ...) (let( [table-publication (string-append stem _publication)] [table-author (string-append stem _author)] [table-bridge-publication-author (string-append stem _bridge_publication_author)] [table-unique-counters (string-append stem _unique_counters)] ) body ... )) Which works fine when I don't reference the environment defined by the let: racket@ racket@ (with-tables x hello) hello However when I pass it an identifier corresponding to one of the variables defined in the let: racket@ (with-tables x table-author) reference to undefined identifier: table-author stdin::1167: table-author The identifier passed in doesn't seem to be part of the local let context, but carried in a different context, or perhaps it was evaluated as an operand. I didn't expect either of those. Can someone point me at a description of the expected behavior, or give me a tip here on what is happening and why. ... in Wolfram language there is a 'Hold' operator for situations like this. Apparently inside the macro we have to do some evaluation to handle the work of the macro, is that why the operand is evaluated? Thanks in advance for explaining the evaluation/context model here. Thomas _ Racket Developers list:
Re: [racket-dev] Announcing Soft Contract Verification tool
On 1/15/15, 2:13 PM, Asumu Takikawa wrote: On 2015-01-14 19:11:59 -0500, David Van Horn wrote: If you have questions, comments, bugs, or any other feedback, let us know, or just file bug reports on the GitHub source code. Nice tool! I like the web interface too. I was confused by this interaction though. Clicking verify on this: (module fact racket (define (factorial x) (if (zero? x) 1 (* x (factorial (sub1 x) (provide (contract-out [factorial (- (=/c 0) (=/c 0))]))) gives me: Contract violation: 'fact' violates '='. Value 0.105 violates predicate real? An example module that breaks it: (module user racket (require (submod .. fact)) (factorial 0.105)) (Verification takes 0.05s) but the value 0.105 shouldn't violate the predicate real? I think. This is reporting that the fact module can break the contract on = when it uses =/c; that's a bug in our modelling of =/c, which we currently have as: (define (=/c n) (lambda (m) (= m n))) But should be: (define (=/c n) (lambda (m) (and (real? m) (= m n That said, if you change it to (and/c real? (=/c 0)), it says there's a counterexample of 2.0, but that's because we check contracts on recursive calls (and should not). Thanks! David _ Racket Developers list: http://lists.racket-lang.org/dev
Re: [racket-dev] Announcing Soft Contract Verification tool
On 1/15/15, 2:48 PM, Robby Findler wrote: Can you randomly make up programs from your grammar, get example errors from the tool, and then run those programs to see if you find bugs in the analysis like that one? Yes, we're planning to do this. That said, I don't see how the bug in =/c is coming in here. Can you explain more? On further inspection, the counterexample is wrong. (There are counterexamples due to the model of =/c, but the one that reported is not an actual one.) This will be fixed shortly. David _ Racket Developers list: http://lists.racket-lang.org/dev
Re: [racket-dev] question, issue(?) with the scope of identifiers passed into define-syntax-rule
Thank you for that nice explanation. I'm reminded of the scope variables carried in Ruby. In Mathematica the renaming of module variables is explicit. There do not appear to be run phases there. Also thanks for the working example using syntax parse. Thus far I have working examples using define-syntax via datum and define-syntax with case (thanks to Matthais). The following questions might best be answered by pointing me to some other docs, haven't run across yet: Are there more than two phases? There is the syntax phase, i.e. compile time phase, and then a run phase. Lexical scope at the syntax phase would be static based textual layout of the program - i.e. lexical scope. Then the macros (syntax transformers) are gone (as the syntax has been transformed) after the syntax phase. At run time then, we have no access to the syntax object information? Academic question, but can syntax information, or other values be shared across phases? As an example, could one store the file name, line, and column number for an identifier, the make use of that later? How is it that we do work inside of a macro, for example by making use of require-for-syntax? Does that imply that the routines that we make use of in the macro for doing work had their own syntax phase, and now they are in run time phase during the macro's syntax phase? .. then if those worker routines make use of macros ... seems this recursion could be arbitrarily deep. Can the syntax analysis be explicitly invoked? Sort of like (apply ...) or (eval ..) ? Come to think of it, eval must do the syntax phase, then the run phase, so perhaps it is calls to that which causes the recursion. On Fri, Jan 16, 2015 at 11:01 AM, Alexander D. Knauth alexan...@knauth.org wrote: But I think it’s important that it doesn’t use gensym or something like that, it uses syntax-marks, which means you can break these lexical scoping rules if you want/need to by using either syntax-local-introduce or datum-syntax: #lang racket (require syntax/parse/define) (define-simple-macro (with-tables stem body ...) #:with table-author-id (syntax-local-introduce #'table-author) (let([table-publication (string-append stem _publication)] [table-author-id (string-append stem _author)] [table-bridge-publication-author (string-append stem _bridge_publication_author)] [table-unique-counters (string-append stem _unique_counters)] ) body ... )) (with-tables x table-author) ;”x_author On Jan 15, 2015, at 9:23 PM, Alexander McLin alex.mc...@gmail.com wrote: Warning I am still a Racket intermediate user but I've been studying syntactic extensions a lot the past several months. The problem here is macros in Racket have lexical scope just like procedures, they are hygienic macros. The identifiers you introduced in the with-tables macro only exist or refer to other bindings in the same lexical scope as where you originally wrote the macro. When you invoke the macro and pass in table-author, even though it is spelled the same as the identifier you wrote in the macro definition, they are not the same. When the macro expands, hygiene is implemented by renaming all identifiers in the macro to unique non-clashing symbols that don't conflict with others existing in the scope the macro is expanding in. The table-author identifier in the macro in the let form is renamed to something different like g6271 or something along those lines. Furthermore, you need to be careful about what you mean by evaluation. In the presence of macros, you have the concept of syntax phase(or compile-time or expand-time) evaluation versus run-time evaluation. When the macro is expanding, it does it thing, processing the original syntax into the new piece of syntax that replaces what was there previously such as (with-tables x table-author) which is then finally evaluated during run-time. (with-tables x table-author) will expand into something looking similar to the following, just to give you an idea of what macro expansion looks like: (let ((g6191 (string-append x _publication)) (g6271 (string-append x _author)) (g6369 (string-append x _bridge_publication_author)) (g6445 (string-append x _unique_counters))) table-author) Note that the original table-author identifier has been replaced by a different identifier that still has the same binding you originally defined. The table-author identifier you passed to the macro gets inserted in the body position and then the expanded code is evaluated at run-time and of course gives you a run-time error since table-author does not refer to anything and thus when it's evaluated, it is recognized as an undefined identifier. (with-tables x hello) works because what you get in return is: (let ((g6191 (string-append x _publication)) (g6271 (string-append x _author)) (g6369 (string-append x _bridge_publication_author))
Re: [racket-dev] Announcing Soft Contract Verification tool
I tried writing a small program, but got stuck pretty early on. When I try verifying the divides? function below, the tool times out. What's happening? (module div racket (provide (contract-out [divides? (- positive? positive? boolean?)])) (define (positive? x) (and (integer? x) (= 0 x))) (define (divides? a b) (cond [(= 0 b) #t] [( b a) #f] [else (divides? a (- b a))])) ) On Thu, Jan 15, 2015 at 3:14 PM, David Van Horn dvanh...@cs.umd.edu wrote: On 1/15/15, 2:48 PM, Robby Findler wrote: Can you randomly make up programs from your grammar, get example errors from the tool, and then run those programs to see if you find bugs in the analysis like that one? Yes, we're planning to do this. That said, I don't see how the bug in =/c is coming in here. Can you explain more? On further inspection, the counterexample is wrong. (There are counterexamples due to the model of =/c, but the one that reported is not an actual one.) This will be fixed shortly. David _ Racket Developers list: http://lists.racket-lang.org/dev _ Racket Developers list: http://lists.racket-lang.org/dev
