subject:"Re\: \[racket\-dev\] =\?"

I think you’re reading too far into what I’m proposing, though I admit I 
probably didn’t give enough context. I’ve been talking with Sam about this 
issue on IRC, so he knows what I’m talking about, but I’ll try and clarify here.

This entire thing is just a fix for the problem described in Section 2 
http://lexi-lambda.github.io/racket-parametric-opaque-types/#(part._.Extending_parametricity_to_opaque_types).
 When using require/typed to import “opaque” types from untyped code, the 
imported types cannot be polymorphic. This entire proposal is simply a way to 
make that possible.

In Section 2.1, A is used in a number of places, but it is just a type 
parameter. See the typed struct definition in Section 1. A does not refer to a 
specific type but any type. Posn essentially becomes a new type combinator than 
can make new types by supplying it with any other type.

The other functions imported in Section 2.1 simply make use of Typed Racket’s 
polymorphic type utilities to make use of the fact that Posn is now a 
polymorphic type. The concepts here are simple. No semantics are being changed, 
it’s just extending parameterization to opaque types.

Sections 2.3 and 2.2, in contrast, are simply describing mechanisms for 
implementing the functionality outlined in 2.1.

Now to answer your points.

 - Should an A only be a base type like String or Symbol

A can by any type. It’s a type parameter. (Posn A) is like (Boxof A).

 - Do you mean to infer the type of the first thing put into the struct as the 
 exact type for everything else?

No, not really. Remember that Posn is an opaque type. TR has no idea it’s 
actually implemented as a struct. Perhaps the JSExpr example given in Section 3 
will help to illustrate that generality. This will just leverage the existing 
polymorphic type inference mechanisms TR already provides.

 - Would first class members prevent me from filling a struct with members 
 of (define-type (Option A) (U 'None (Some A))), where Some is a struct with 
 one field?

No, as I said, you can supply any type for A. By “first class member” of the 
type system, I simply meant that these types would have to be built-in to TR as 
a special case—they cannot be derived from the existing type constructs 
provided by TR. This is similar to how structure types are “first class” in 
TR—the struct form is “magical” and cannot be reimplemented in terms of other 
TR primitives.

I hope that helps to make things a little more clear.

 On Jan 29, 2015, at 19:44, Benjamin Greenman bl...@cornell.edu wrote:
 
 This has bothered me too, but I've realized that I was on the wrong track.
 
 The string a and symbol 'b are not different types. A struct (Foo a 'b), 
 or (list a 'b), is a homogeneous data structure of type (U String Symbol) 
 just like Alexander said. This really upsets me -- I like the Hindley Milner 
 world where the compiler warns me if I make a list [1, two] and forces me 
 to wrap the int and string into a new datatype. But Typed Racket is not HM.
 
 About the proposal, I'm confused about what the syntax in Section 2.1 should 
 do -- what is a first class member of Typed Racket's type system?
 - Should an A only be a base type like String or Symbol
 - Do you mean to infer the type of the first thing put into the struct as the 
 exact type for everything else?
 - Would first class members prevent me from filling a struct with members 
 of (define-type (Option A) (U 'None (Some A))), where Some is a struct with 
 one field?
 
 I totally agree that something needs fixing, but I'm not sure what.
 
 
 
 On Thu, Jan 29, 2015 at 10:13 PM, Alexis King lexi.lam...@gmail.com 
 mailto:lexi.lam...@gmail.com wrote:
 Or Any for that matter. I know. The fact that it could be literally anything 
 was sort of the point.
 
 On Jan 29, 2015, at 19:10, Alexander D. Knauth alexan...@knauth.org 
 mailto:alexan...@knauth.org wrote:
 
 Um, for this:
 (module 
 http://docs.racket-lang.org/reference/module.html#%28form._%28%28quote._~23~25kernel%29._module%29%29
  typed typed/racket/base
 (provide 
 http://docs.racket-lang.org/reference/require.html#%28form._%28%28lib._racket%2Fprivate%2Fbase..rkt%29._provide%29%29
  (struct-out 
 http://docs.racket-lang.org/reference/require.html#%28form._%28%28lib._racket%2Fprivate%2Fbase..rkt%29._struct-out%29%29
  Foo))
 (struct 
 http://docs.racket-lang.org/ts-reference/special-forms.html#%28form._%28%28lib._typed-racket%2Fbase-env%2Fprims..rkt%29._struct%29%29
  [A] Foo ([x : 
 http://docs.racket-lang.org/ts-reference/special-forms.html#%28form._%28%28lib._typed-racket%2Fbase-env%2Fprims..rkt%29._~3a%29%29
  A] [y : 
 http://docs.racket-lang.org/ts-reference/special-forms.html#%28form._%28%28lib._typed-racket%2Fbase-env%2Fprims..rkt%29._~3a%29%29
  A]) #:transparent))
 
 (Foo a 'b)
 Should be fine because Foo could be instantiated at the type (U String 
 Symbol).
 
 On Jan 29, 2015, at 9:25 PM, Alexis King lexi.lam...@gmail.com 
 mailto:lexi.lam...@gmail.com wrote:
 
 I

Re: [racket-dev] A proposal for parametric opaque types in Typed Racket

2015-01-29 Thread Alexander D. Knauth


On Jan 29, 2015, at 11:34 PM, Alexis King lexi.lam...@gmail.com wrote:

 But the problem is that if it’s an opaque type then it can’t unwrap it once 
 the value is returned from make-posn.
 
 Yes, that’s precisely the problem. Your point about implementing everything 
 as single-valued structs on the typed side is an interesting one, though I 
 don’t think it ultimately solves any problems. The fact that the typed side 
 knows nothing about the contents of the value is what makes this such a 
 tricky problem.
 
 As for this:
 
 But then you couldn’t do any operations on it except those that you use 
 import with require/typed, right?
 
 That’s completely correct. That’s why it’s “opaque.”
 
 And what happens if you use cast on one of these things?
 
 That’s a little more interesting. Using cast on an object of this type would 
 never fail (unless, of course, it didn’t actually satisfy the basic posn? 
 predicate), but it would possibly introduce failures in the future since it 
 would affect the contracts generated for posn-x and posn-y, for example.
 
 To make that more clear, casting a (Posn Real) to a (Posn String) would work 
 fine until you tried to call posn-x on the instance, in which case it would 
 raise a contract error. Note that this isn’t really any different from 
 casting mutable data types.

But if it were wrapped in an opaque structure, then that structure wouldn’t 
satisfy the posn? predicate, unless of course the posn? predicate has a 
contract that unwraps it.  So all of the operations on it would have to have 
contracts that would unwrap it.  This might actually make sense if the type is 
meant to be actually opaque, but if it’s an opaque type that represents a 
normal non-opaque value, then it will still work as an opaque type, but it 
won’t be a normal non-opaque value anymore on the typed side.  

But the reason I asked about cast was because normally I can use cast with a 
value that has an opaque type, but it’s wrapped on the typed side in this 
opaque structure, then the contracts on the cast would see this opaque 
structure instead of the actual value.  

I’m thinking of an opaque typed representing a string with length 1, which I 
can use as long as I use either (cast x String) or (assert x string?) whenever 
I pass it to a string operation.  But if it were an opaque type, I don’t think 
I could do that.  There could be a 1string-string function that could take one 
of these 1strings and convert it to a string, but that seems like it should be 
unnecessary, but made necessary by this opaque structure thing.  

And for “this isn’t really any different from casting mutable data types,” look 
at this:
#lang typed/racket
(: b : (Boxof Number))
(define b (box 1))
(set-box! (cast b (Boxof (U Number String))) I am a string)
(ann (unbox b) Number) ;I am a string” ; not a contract error


 
 On Jan 29, 2015, at 20:20, Alexander D. Knauth alexan...@knauth.org wrote:
 
 Furthermore, even if the wrappers were shared between functions, untyped 
 code would recieved wrapped values, which would render them quite useless.
 
 If it’s not an opaque type, but something like a list, then this works, and 
 the untyped code receiving wrapped values isn’t a problem here:
 #lang typed/racket
 ; make Posn parametric
 (define-type (Posn A) (List A A))
 (provide Posn)
 (require/typed/provide
  untyped.rkt
  [make-posn (All (A) A A - (Posn A))]
  [posn-x (All (A) (Posn A) - A)]
  [posn-y (All (A) (Posn A) - A)]
  [real-posn? [(Posn Any) - Boolean]])
  (define p (make-posn 1 2))
 (make-posn #A6 #A6) ; a printf that I put in make-posn from “untyped.rkt
  p
 - : (Listof Positive-Byte) [more precisely: (List Positive-Byte 
 Positive-Byte)]
 '(1 2) ; unwrapped
  (posn-x p)
 - : Integer [more precisely: Positive-Byte]
 1
  (posn-y p)
 - : Integer [more precisely: Positive-Byte]
 2
  (real-posn? p)
 - : Boolean
 #t
 
 Even though for a short time it's wrapped, it’s unwrapped as soon as 
 make-posn returns, and then after that if it flows into untyped code again 
 it’s not wrapped and functions like real-posn? work fine.  
 
 But the problem is that if it’s an opaque type then it can’t unwrap it once 
 the value is returned from make-posn.
 
 And I don’t think parametric opaque types could solve this unless all posns 
 themselves were wrapped with an opaque struct on the typed side, which I 
 guess does make sense now that I think about it.  But then you couldn’t do 
 any operations on it except those that you use import with require/typed, 
 right?  Or not?  And what happens if you use cast on one of these things?
 
 
 On Jan 29, 2015, at 9:25 PM, Alexis King lexi.lam...@gmail.com wrote:
 
 I recently ran into a problem in which opaque types (types imported from 
 untyped code) cannot by parameterized by Typed Racket. I initially 
 encountered this problem in my attempt to port 2htdp/image to TR.
 
 After some further consideration, I’m interested in adding support to make 
 something like this possible, which

Re: [racket-dev] A proposal for parametric opaque types in Typed Racket

2015-01-29 Thread Alexander D. Knauth

Um, for this:
(module typed typed/racket/base
(provide (struct-out Foo))
(struct [A] Foo ([x : A] [y : A]) #:transparent))

(Foo a 'b)
Should be fine because Foo could be instantiated at the type (U String Symbol).

On Jan 29, 2015, at 9:25 PM, Alexis King lexi.lam...@gmail.com wrote:

 I recently ran into a problem in which opaque types (types imported from 
 untyped code) cannot by parameterized by Typed Racket. I initially 
 encountered this problem in my attempt to port 2htdp/image to TR.
 
 After some further consideration, I’m interested in adding support to make 
 something like this possible, which would certainly have additional benefits 
 beyond this specific use-case. I’ve outlined my proposal here:
 http://lexi-lambda.github.io/racket-parametric-opaque-types/
 
 Any feedback, suggestions, or advice would be appreciated, especially from 
 those who are familiar with Typed Racket’s internals.
 
 Thank you,
 Alexis
 _
  Racket Developers list:
  http://lists.racket-lang.org/dev

_
  Racket Developers list:
  http://lists.racket-lang.org/dev

Re: [racket-dev] build memory use (was: internal error during gc)

2015-01-29 Thread Philippe Meunier

Matthew Flatt wrote:
We've so far cut the peak memory use of a build by about 1/4 compared
to a v6.1.1 build.

Yes, peak memory use for me has now dropped from about 900MB to just
below 700MB.  Veeery nice :-)

Philippe


_
  Racket Developers list:
  http://lists.racket-lang.org/dev

Re: [racket-dev] A proposal for parametric opaque types in Typed Racket

 But the problem is that if it’s an opaque type then it can’t unwrap it once 
 the value is returned from make-posn.

Yes, that’s precisely the problem. Your point about implementing everything as 
single-valued structs on the typed side is an interesting one, though I don’t 
think it ultimately solves any problems. The fact that the typed side knows 
nothing about the contents of the value is what makes this such a tricky 
problem.

As for this:

 But then you couldn’t do any operations on it except those that you use 
 import with require/typed, right?

That’s completely correct. That’s why it’s “opaque.”

 And what happens if you use cast on one of these things?

That’s a little more interesting. Using cast on an object of this type would 
never fail (unless, of course, it didn’t actually satisfy the basic posn? 
predicate), but it would possibly introduce failures in the future since it 
would affect the contracts generated for posn-x and posn-y, for example.

To make that more clear, casting a (Posn Real) to a (Posn String) would work 
fine until you tried to call posn-x on the instance, in which case it would 
raise a contract error. Note that this isn’t really any different from casting 
mutable data types.

 On Jan 29, 2015, at 20:20, Alexander D. Knauth alexan...@knauth.org wrote:
 
 Furthermore, even if the wrappers were shared between functions, untyped code 
 would recieved wrapped values, which would render them quite useless.
 
 If it’s not an opaque type, but something like a list, then this works, and 
 the untyped code receiving wrapped values isn’t a problem here:
 #lang typed/racket
 ; make Posn parametric
 (define-type (Posn A) (List A A))
 (provide Posn)
 (require/typed/provide
  untyped.rkt
  [make-posn (All (A) A A - (Posn A))]
  [posn-x (All (A) (Posn A) - A)]
  [posn-y (All (A) (Posn A) - A)]
  [real-posn? [(Posn Any) - Boolean]])
  (define p (make-posn 1 2))
 (make-posn #A6 #A6) ; a printf that I put in make-posn from “untyped.rkt
  p
 - : (Listof Positive-Byte) [more precisely: (List Positive-Byte 
 Positive-Byte)]
 '(1 2) ; unwrapped
  (posn-x p)
 - : Integer [more precisely: Positive-Byte]
 1
  (posn-y p)
 - : Integer [more precisely: Positive-Byte]
 2
  (real-posn? p)
 - : Boolean
 #t
 
 Even though for a short time it's wrapped, it’s unwrapped as soon as 
 make-posn returns, and then after that if it flows into untyped code again 
 it’s not wrapped and functions like real-posn? work fine.  
 
 But the problem is that if it’s an opaque type then it can’t unwrap it once 
 the value is returned from make-posn.
 
 And I don’t think parametric opaque types could solve this unless all posns 
 themselves were wrapped with an opaque struct on the typed side, which I 
 guess does make sense now that I think about it.  But then you couldn’t do 
 any operations on it except those that you use import with require/typed, 
 right?  Or not?  And what happens if you use cast on one of these things?
 
 
 On Jan 29, 2015, at 9:25 PM, Alexis King lexi.lam...@gmail.com 
 mailto:lexi.lam...@gmail.com wrote:
 
 I recently ran into a problem in which opaque types (types imported from 
 untyped code) cannot by parameterized by Typed Racket. I initially 
 encountered this problem in my attempt to port 2htdp/image to TR 
 https://github.com/lexi-lambda/racket-2htdp-typed/issues/1.
 
 After some further consideration, I’m interested in adding support to make 
 something like this possible, which would certainly have additional benefits 
 beyond this specific use-case. I’ve outlined my proposal here:
 http://lexi-lambda.github.io/racket-parametric-opaque-types/ 
 http://lexi-lambda.github.io/racket-parametric-opaque-types/
 
 Any feedback, suggestions, or advice would be appreciated, especially from 
 those who are familiar with Typed Racket’s internals.
 
 Thank you,
 Alexis
 _
  Racket Developers list:
  http://lists.racket-lang.org/dev http://lists.racket-lang.org/dev
 

_
  Racket Developers list:
  http://lists.racket-lang.org/dev

Re: [racket-dev] A proposal for parametric opaque types in Typed Racket

2015-01-29 Thread Benjamin Greenman

This has bothered me too, but I've realized that I was on the wrong track.

The string a and symbol 'b are not different types. A struct (Foo a
'b), or (list a 'b), is a homogeneous data structure of type (U String
Symbol) just like Alexander said. This really upsets me -- I like the
Hindley Milner world where the compiler warns me if I make a list [1,
two] and forces me to wrap the int and string into a new datatype. But
Typed Racket is not HM.

About the proposal, I'm confused about what the syntax in Section 2.1
should do -- what is a first class member of Typed Racket's type system?
- Should an A only be a base type like String or Symbol
- Do you mean to infer the type of the first thing put into the struct as
the exact type for everything else?
- Would first class members prevent me from filling a struct with members
of (define-type (Option A) (U 'None (Some A))), where Some is a struct
with one field?

I totally agree that something needs fixing, but I'm not sure what.



On Thu, Jan 29, 2015 at 10:13 PM, Alexis King lexi.lam...@gmail.com wrote:

 Or Any for that matter. I know. The fact that it could be literally
 anything was sort of the point.

 On Jan 29, 2015, at 19:10, Alexander D. Knauth alexan...@knauth.org
 wrote:

 Um, for this:
 (module
 http://docs.racket-lang.org/reference/module.html#%28form._%28%28quote._~23~25kernel%29._module%29%29
  typed typed/racket/base(provide
 http://docs.racket-lang.org/reference/require.html#%28form._%28%28lib._racket%2Fprivate%2Fbase..rkt%29._provide%29%29
  (struct-out
 http://docs.racket-lang.org/reference/require.html#%28form._%28%28lib._racket%2Fprivate%2Fbase..rkt%29._struct-out%29%29
  Foo))(struct
 http://docs.racket-lang.org/ts-reference/special-forms.html#%28form._%28%28lib._typed-racket%2Fbase-env%2Fprims..rkt%29._struct%29%29
  [A] Foo ([x :
 http://docs.racket-lang.org/ts-reference/special-forms.html#%28form._%28%28lib._typed-racket%2Fbase-env%2Fprims..rkt%29._~3a%29%29
  A] [y :
 http://docs.racket-lang.org/ts-reference/special-forms.html#%28form._%28%28lib._typed-racket%2Fbase-env%2Fprims..rkt%29._~3a%29%29
  A]) #:transparent))

 (Foo a 'b)
 Should be fine because Foo could be instantiated at the type (U String
 Symbol).

 On Jan 29, 2015, at 9:25 PM, Alexis King lexi.lam...@gmail.com wrote:

 I recently ran into a problem in which opaque types (types imported from
 untyped code) cannot by parameterized by Typed Racket. I initially
 encountered this problem in my attempt to port 2htdp/image to TR
 https://github.com/lexi-lambda/racket-2htdp-typed/issues/1.

 After some further consideration, I’m interested in adding support to make
 something like this possible, which would certainly have additional
 benefits beyond this specific use-case. I’ve outlined my proposal here:
 http://lexi-lambda.github.io/racket-parametric-opaque-types/

 Any feedback, suggestions, or advice would be appreciated, especially from
 those who are familiar with Typed Racket’s internals.

 Thank you,
 Alexis
 _
  Racket Developers list:
  http://lists.racket-lang.org/dev




 _
   Racket Developers list:
   http://lists.racket-lang.org/dev


_
  Racket Developers list:
  http://lists.racket-lang.org/dev

Re: [racket-dev] A proposal for parametric opaque types in Typed Racket

2015-01-29 Thread Alexander D. Knauth

Furthermore, even if the wrappers were shared between functions, untyped code 
would recieved wrapped values, which would render them quite useless.

If it’s not an opaque type, but something like a list, then this works, and the 
untyped code receiving wrapped values isn’t a problem here:
#lang typed/racket
; make Posn parametric
(define-type (Posn A) (List A A))
(provide Posn)
(require/typed/provide
 untyped.rkt
 [make-posn (All (A) A A - (Posn A))]
 [posn-x (All (A) (Posn A) - A)]
 [posn-y (All (A) (Posn A) - A)]
 [real-posn? [(Posn Any) - Boolean]])
 (define p (make-posn 1 2))
(make-posn #A6 #A6) ; a printf that I put in make-posn from “untyped.rkt
 p
- : (Listof Positive-Byte) [more precisely: (List Positive-Byte Positive-Byte)]
'(1 2) ; unwrapped
 (posn-x p)
- : Integer [more precisely: Positive-Byte]
1
 (posn-y p)
- : Integer [more precisely: Positive-Byte]
2
 (real-posn? p)
- : Boolean
#t

Even though for a short time it's wrapped, it’s unwrapped as soon as make-posn 
returns, and then after that if it flows into untyped code again it’s not 
wrapped and functions like real-posn? work fine.  

But the problem is that if it’s an opaque type then it can’t unwrap it once the 
value is returned from make-posn.

And I don’t think parametric opaque types could solve this unless all posns 
themselves were wrapped with an opaque struct on the typed side, which I guess 
does make sense now that I think about it.  But then you couldn’t do any 
operations on it except those that you use import with require/typed, right?  
Or not?  And what happens if you use cast on one of these things?


On Jan 29, 2015, at 9:25 PM, Alexis King lexi.lam...@gmail.com wrote:

 I recently ran into a problem in which opaque types (types imported from 
 untyped code) cannot by parameterized by Typed Racket. I initially 
 encountered this problem in my attempt to port 2htdp/image to TR.
 
 After some further consideration, I’m interested in adding support to make 
 something like this possible, which would certainly have additional benefits 
 beyond this specific use-case. I’ve outlined my proposal here:
 http://lexi-lambda.github.io/racket-parametric-opaque-types/
 
 Any feedback, suggestions, or advice would be appreciated, especially from 
 those who are familiar with Typed Racket’s internals.
 
 Thank you,
 Alexis
 _
  Racket Developers list:
  http://lists.racket-lang.org/dev

_
  Racket Developers list:
  http://lists.racket-lang.org/dev

Re: [racket-dev] A proposal for parametric opaque types in Typed Racket

Or Any for that matter. I know. The fact that it could be literally anything 
was sort of the point.

 On Jan 29, 2015, at 19:10, Alexander D. Knauth alexan...@knauth.org wrote:
 
 Um, for this:
 (module 
 http://docs.racket-lang.org/reference/module.html#%28form._%28%28quote._~23~25kernel%29._module%29%29
  typed typed/racket/base
 (provide 
 http://docs.racket-lang.org/reference/require.html#%28form._%28%28lib._racket%2Fprivate%2Fbase..rkt%29._provide%29%29
  (struct-out 
 http://docs.racket-lang.org/reference/require.html#%28form._%28%28lib._racket%2Fprivate%2Fbase..rkt%29._struct-out%29%29
  Foo))
 (struct 
 http://docs.racket-lang.org/ts-reference/special-forms.html#%28form._%28%28lib._typed-racket%2Fbase-env%2Fprims..rkt%29._struct%29%29
  [A] Foo ([x : 
 http://docs.racket-lang.org/ts-reference/special-forms.html#%28form._%28%28lib._typed-racket%2Fbase-env%2Fprims..rkt%29._~3a%29%29
  A] [y : 
 http://docs.racket-lang.org/ts-reference/special-forms.html#%28form._%28%28lib._typed-racket%2Fbase-env%2Fprims..rkt%29._~3a%29%29
  A]) #:transparent))
 
 (Foo a 'b)
 Should be fine because Foo could be instantiated at the type (U String 
 Symbol).
 
 On Jan 29, 2015, at 9:25 PM, Alexis King lexi.lam...@gmail.com 
 mailto:lexi.lam...@gmail.com wrote:
 
 I recently ran into a problem in which opaque types (types imported from 
 untyped code) cannot by parameterized by Typed Racket. I initially 
 encountered this problem in my attempt to port 2htdp/image to TR 
 https://github.com/lexi-lambda/racket-2htdp-typed/issues/1.
 
 After some further consideration, I’m interested in adding support to make 
 something like this possible, which would certainly have additional benefits 
 beyond this specific use-case. I’ve outlined my proposal here:
 http://lexi-lambda.github.io/racket-parametric-opaque-types/ 
 http://lexi-lambda.github.io/racket-parametric-opaque-types/
 
 Any feedback, suggestions, or advice would be appreciated, especially from 
 those who are familiar with Typed Racket’s internals.
 
 Thank you,
 Alexis
 _
  Racket Developers list:
  http://lists.racket-lang.org/dev http://lists.racket-lang.org/dev
 

_
  Racket Developers list:
  http://lists.racket-lang.org/dev

Re: [racket-dev] A proposal for parametric opaque types in Typed Racket

It isn’t wrapped in an opaque structure. That wasn’t a part of my proposal, and 
while I didn’t think of it until you brought it up, I still think it’s 
unnecessary and doesn’t add any convenience.

Perhaps I’m not understanding you properly, but your “one-length string” idea 
sounds like it has little to do with this opaque type problem and more to do 
with the fact that you want refinement types in Typed Racket. I do, too! But I 
don’t think hacking the opaque type system is going to help you with that.

(Also, as for the box example, I’m actually a little surprised that doesn’t 
contract error. Seems like a bug to me, but perhaps I’m missing some 
idiosyncrasies of the type system. Either way, it’s precisely that kind of 
craziness I was referring to when I compared casting parametric opaque types to 
casting mutable types.)

 On Jan 29, 2015, at 20:50, Alexander D. Knauth alexan...@knauth.org wrote:
 
 
 On Jan 29, 2015, at 11:34 PM, Alexis King lexi.lam...@gmail.com 
 mailto:lexi.lam...@gmail.com wrote:
 
 But the problem is that if it’s an opaque type then it can’t unwrap it once 
 the value is returned from make-posn.
 
 Yes, that’s precisely the problem. Your point about implementing everything 
 as single-valued structs on the typed side is an interesting one, though I 
 don’t think it ultimately solves any problems. The fact that the typed side 
 knows nothing about the contents of the value is what makes this such a 
 tricky problem.
 
 As for this:
 
 But then you couldn’t do any operations on it except those that you use 
 import with require/typed, right?
 
 That’s completely correct. That’s why it’s “opaque.”
 
 And what happens if you use cast on one of these things?
 
 That’s a little more interesting. Using cast on an object of this type would 
 never fail (unless, of course, it didn’t actually satisfy the basic posn? 
 predicate), but it would possibly introduce failures in the future since it 
 would affect the contracts generated for posn-x and posn-y, for example.
 
 To make that more clear, casting a (Posn Real) to a (Posn String) would work 
 fine until you tried to call posn-x on the instance, in which case it would 
 raise a contract error. Note that this isn’t really any different from 
 casting mutable data types.
 
 But if it were wrapped in an opaque structure, then that structure wouldn’t 
 satisfy the posn? predicate, unless of course the posn? predicate has a 
 contract that unwraps it.  So all of the operations on it would have to have 
 contracts that would unwrap it.  This might actually make sense if the type 
 is meant to be actually opaque, but if it’s an opaque type that represents a 
 normal non-opaque value, then it will still work as an opaque type, but it 
 won’t be a normal non-opaque value anymore on the typed side.  
 
 But the reason I asked about cast was because normally I can use cast with a 
 value that has an opaque type, but it’s wrapped on the typed side in this 
 opaque structure, then the contracts on the cast would see this opaque 
 structure instead of the actual value.  
 
 I’m thinking of an opaque typed representing a string with length 1, which I 
 can use as long as I use either (cast x String) or (assert x string?) 
 whenever I pass it to a string operation.  But if it were an opaque type, I 
 don’t think I could do that.  There could be a 1string-string function that 
 could take one of these 1strings and convert it to a string, but that seems 
 like it should be unnecessary, but made necessary by this opaque structure 
 thing.  
 
 And for “this isn’t really any different from casting mutable data types,” 
 look at this:
 #lang typed/racket
 (: b : (Boxof Number))
 (define b (box 1))
 (set-box! (cast b (Boxof (U Number String))) I am a string)
 (ann (unbox b) Number) ;I am a string” ; not a contract error
 
 
 
 On Jan 29, 2015, at 20:20, Alexander D. Knauth alexan...@knauth.org 
 mailto:alexan...@knauth.org wrote:
 
 Furthermore, even if the wrappers were shared between functions, untyped 
 code would recieved wrapped values, which would render them quite useless.
 
 If it’s not an opaque type, but something like a list, then this works, and 
 the untyped code receiving wrapped values isn’t a problem here:
 #lang typed/racket
 ; make Posn parametric
 (define-type (Posn A) (List A A))
 (provide Posn)
 (require/typed/provide
  untyped.rkt
  [make-posn (All (A) A A - (Posn A))]
  [posn-x (All (A) (Posn A) - A)]
  [posn-y (All (A) (Posn A) - A)]
  [real-posn? [(Posn Any) - Boolean]])
  (define p (make-posn 1 2))
 (make-posn #A6 #A6) ; a printf that I put in make-posn from 
 “untyped.rkt
  p
 - : (Listof Positive-Byte) [more precisely: (List Positive-Byte 
 Positive-Byte)]
 '(1 2) ; unwrapped
  (posn-x p)
 - : Integer [more precisely: Positive-Byte]
 1
  (posn-y p)
 - : Integer [more precisely: Positive-Byte]
 2
  (real-posn? p)
 - : Boolean
 #t
 
 Even though for a short time it's wrapped, it’s unwrapped as soon as 
 make-posn returns, and

Re: [racket-dev] feature request: thread-safe memoize-evt

2015-01-29 Thread Jan Dvořák

On Thu, 2015-01-29 at 16:41 -0600, Robby Findler wrote:
 That is, I thought you could just create a separate thread that sync's
 on E_b and then whenever you get a value from it, then the E_m would
 just continue to produce that all the time. But I think you're saying
 that wouldn't work?

The problem is that the auxiliary thread would always wait for the E_b,
even when nobody is interested in the result anymore. Moreover, putting
the wait in another thread would require the E_b to be thread safe.

_
  Racket Developers list:
  http://lists.racket-lang.org/dev

Re: [racket-dev] dev Digest, Vol 72, Issue 31

2015-01-28 Thread Byron Davies

My apologies, especially to Matt, for letting this thread go cold.  I was
busy preparing a Racket-based demo for this morning -- and it went very
well.  As mentioned, I'm working on weakest precondition analysis for
finding latent faults in programs. Our goal is to do this for all kinds of
software, including machine language, but for proof of concept I'm doing it
*in* Racket *on* Racket programs.  Racket's language building tools,
including syntax and the syntax browser, have been very useful for this
problem.

Regarding transparency, thank you, Matt, for suggesting an alternative
approach.  I've played with your examples a bit, trying to see how I could
use this during debugging.  I have also read the Reflection and Security
chapter in the reference to learn more about inspectors in general.

Your code, commented:

(define orig-i (current-inspector))  ; saves the original inspector
(define sub-i (make-inspector orig-i))  ;make a new inspector whose parent
is the original inspector

(current-inspector sub-i)  ;makes the new inspector the current inspector
(struct a (x))  ; creates a structure using the new inspector as the
default inspector
(define v (a 1))  ; creates an instance of the new structure
(current-inspector orig-i) ;reverts the inspector to the original (the
parent of the new inspector)

I see how this works, but I'm a little confused about why it works.  I see
that the new inspector is a child of the old one, and I read in the
reference chapter that access is determined not by the inspector in force
at creation time, but by the parent of that inspector, i.e., the old
inspector. I can't find any description of the power of an inspector,
except that the parent is more powerful.

Are there degrees of power? Or if you have access to the parent do you have
all the power you can have? I see that the inspector gives you access to
the data in a structure instance, but does it also give you access to
meta-data, so that I know that the name of the first field in struct a is x?

I also don't understand how the root inspector works.  I have found that
setting (current-inspector root-inspector) delivers endless left parens for
the (a 1) example, presumably because the display function recursively
tries to inspect the components of the struct, all the way down.

Finally, does this also work for classes?

Date: Thu, 22 Jan 2015 05:36:18 -0700
From: Matthew Flatt mfl...@cs.utah.edu
To: Byron Davies byrondav...@starshine.us
Cc: dev@racket-lang.org
Subject: Re: [racket-dev] Full transparency
Message-ID: 20150122123620.2daa1650...@mail-svr1.cs.utah.edu
Content-Type: text/plain; charset=UTF-8

I don't think you want to do anything with the compiler or macros.
Instead, it's a matter of having a sufficiently powerful inspector
(which is the concept of inspectability turned into a language
construct).

If you have just

 (struct a (x))
 (a 1)

then the result will print as `#a`. But if you use

 (define orig-i (current-inspector))
 (define sub-i (make-inspector orig-i))

 (current-inspector sub-i)
 (struct a (x))
 (define v (a 1))
 (current-inspector orig-i)

 v

Then, the result will print as `(a 1)`. That's because the structure
declaration is creates under an inspector `sub-i` (which is the current
inspector at the time) that is subordinate to the inspector `orig-i`
that is in place when the structure instance is printed.

The current inspector is determined dynamically, which means that if
you're loading some code, you can set the inspector while loading the
code. For example, if a.rkt is

 #lang racket/base
 (provide v)

 (struct a (x))
 (define v (a 1))

then

 (define v
   (parameterize ([current-inspector (make-inspector)])
 (dynamic-require a.rkt 'v)))
 v

will print the `a` instance transparently.


To protect libraries, there's no safe way to access a root inspector
that controls all structure types when you start Racket. Nothing is
safe from unsafe code, though, and here's an unsafe way to access the
root inspector:

 #lang racket/base
 (require ffi/unsafe)

 (define-cstruct _Scheme_Inspector
   ([stag _short]
[keyex _short]
[depth _int]
[superior _racket]))

 (define root-inspector
   (Scheme_Inspector-superior
((get-ffi-obj 'scheme_get_initial_inspector
  #f
  (_fun - (_gcable _Scheme_Inspector-pointer))

Using `root-inspector`, you can inspect any structure instance.

At Wed, 21 Jan 2015 23:46:10 -0700, Byron Davies wrote:
 Nice parry!  What may be straightforward to you may not be so obvious to
 me.  But I'll take a look.

 I'm deep into a project using Racket for weakest precondition analysis.
 Every time I'm debugging it seems like I have to write another
 special-purpose accessor, or export some existing accessor up through
 multiple levels in order to get at the data I need at the top-level.  I
 remember how easy it was with the Lisp Machine to navigate through data no
 matter what it was.

 The Lisp Machine offered total transparency

Re: [racket-dev] Switching to Google Groups

2015-01-28 Thread Vincent St-Amour

In case anyone would like to use a non-gmail address for sign up, you
can sign up from this URL:
https://groups.google.com/forum/#!forum/racket-dev/join

The regular sign up button wouldn't let me.

Vincent


At Wed, 28 Jan 2015 16:47:58 -0800,
John Clements wrote:
 
 
 Dear developers,
 
 PLT would like to get out of the mailing-list administration game.
 
 Accordingly, we’re planning to switch to Google Groups. Rather than
 starting with our largest list, the Racket Users list, we’ve chosen to
 begin with the dev list, because … well, you’re probably more tolerant,
 if^H^H when something goes wrong.
 
 We would like the transition to be as smooth as possible, and we can use
 your help with this. Specifically, Google has a daily cap on the number
 of e-mail addresses that can be bulk-added to a mailing list. For this
 reason, it would speed the transition greatly if you could take a moment
 to sign up for the new group yourself, using this URL:
 
 https://groups.google.com/forum/#!forum/racket-dev
 
 We plan to disable signup for the old group now, and to halt delivery of
 mail to the existing group address tomorrow. You can post to the new
 group (after signing up) by sending mail to
 
 racket-...@googlegroups.com
 
 We plan to manually add or invite the members who do not add themselves,
 but the daily cap will mean that these users are likely to miss one or
 more days of postings to this list. Naturally, those posts will be
 archived, as part of the group.
 
 The archive of the existing list will continue to exist, though new
 messages will not be added to it.
 
 Let us know if you run into problems!
 
 Many thanks,
 
 John Clements  PLT
 _
   Racket Developers list:
   http://lists.racket-lang.org/dev
_
  Racket Developers list:
  http://lists.racket-lang.org/dev

Re: [racket-dev] Fwd: Sandbox evaluation problem - files with comment boxes

2015-01-27 Thread Matthew Flatt

Yes, it's a bug in v6.1.1. I've just pushed a repair for the next
build.

Do you need a workaround for v6.1.1? Your variant that sets
`sandbox-namespace-specs` is what I would have tried; unfortunately,
that runs into a second bug in v6.1.1 that I recently fixed. If you
need a workaround other than using the next snapshot, I can look harder
for one.

Thanks for the report!

At Mon, 26 Jan 2015 21:27:31 -0500, Nadeem Abdul Hamid wrote:
 Ah, I am still struggling with this sandbox problem! (previous message to
 'users' below) I'm starting to feel like maybe there's a bug in 6.1.1, or
 else something changed in recent versions that I'm missing. The following
 screenshots show the entire contents of the BSL file that I'm trying to
 load using make-module-evaluator, with gracket v6.1.1 failing the second
 time you try to load the file (or another one) that contains a comment box,
 while racket v6.1.1 and gracket 6.0 don't have this behavior:
 
 http://cs.berry.edu/~nhamid/temp/foo.png
 http://cs.berry.edu/~nhamid/temp/foo60.png
 
 ???
 
 --- nadeem
 
 
 
 -- Forwarded message --
 From: Nadeem Abdul Hamid nad...@acm.org
 Date: Sun, Jan 25, 2015 at 10:35 PM
 Subject: Sandbox evaluation problem - files with comment boxes
 To: users us...@racket-lang.org
 
 
 
 I'm trying to create a simple sandbox evaluator (to load in programs in
 *SL). I have the following code:
 
 #lang racket
 (require racket/sandbox)
 (define E
   (parameterize ([sandbox-path-permissions
   '([write /var/folders]
 [exists /]
 [read /])]
  )
 (make-module-evaluator (string-path test-file.rkt
 
 
 This works fine as long as test-file.rkt does *not* contain a comment box.
 If the file contains a comment box, then the following error occurs:
 
 /Applications/Racket
 v6.1.1/share/pkgs/snip-lib/racket/snip/private/load-one.rkt:21:2:
 dynamic-require: unknown module
   module name: #resolved-module-path:/Applications/Racket
 v6.1.1/share/pkgs/gui-lib/framework/main.rkt
 
 
 
 I thought maybe parameterizing sandbox-namespace-specs with 'framework
 might do something:
 
 (require racket/sandbox racket/gui)
 (define E
   (parameterize ([sandbox-path-permissions
   '([write /var/folders]
 [exists /]
 [read /])]
  [sandbox-namespace-specs
   (list make-gui-namespace 'framework)]
  )
 (make-module-evaluator (string-path lab01-insulin.rkt
 
 But it results in:
namespace-attach-module: a different instance of the same module is
 already in the destination namespace
   module name: /Applications/Racket
 v6.1.1/collects/racket/stxparam-exptime.rkt
 
 
 Any suggestions?
 
 Thanks!
 
 --- nadeem
 _
   Racket Developers list:
   http://lists.racket-lang.org/dev
_
  Racket Developers list:
  http://lists.racket-lang.org/dev

Re: [racket-dev] Sandbox evaluation problem - files with comment boxes

2015-01-27 Thread Nadeem Abdul Hamid

Ok, thank you! I can use the latest build.
--- nadeem

On Tuesday, January 27, 2015, Matthew Flatt mfl...@cs.utah.edu wrote:

 Yes, it's a bug in v6.1.1. I've just pushed a repair for the next
 build.

 Do you need a workaround for v6.1.1? Your variant that sets
 `sandbox-namespace-specs` is what I would have tried; unfortunately,
 that runs into a second bug in v6.1.1 that I recently fixed. If you
 need a workaround other than using the next snapshot, I can look harder
 for one.

 Thanks for the report!

 At Mon, 26 Jan 2015 21:27:31 -0500, Nadeem Abdul Hamid wrote:
  Ah, I am still struggling with this sandbox problem! (previous message to
  'users' below) I'm starting to feel like maybe there's a bug in 6.1.1, or
  else something changed in recent versions that I'm missing. The following
  screenshots show the entire contents of the BSL file that I'm trying to
  load using make-module-evaluator, with gracket v6.1.1 failing the second
  time you try to load the file (or another one) that contains a comment
 box,
  while racket v6.1.1 and gracket 6.0 don't have this behavior:
 
  http://cs.berry.edu/~nhamid/temp/foo.png
  http://cs.berry.edu/~nhamid/temp/foo60.png
 
  ???
 
  --- nadeem
 
 
 
  -- Forwarded message --
  From: Nadeem Abdul Hamid nad...@acm.org javascript:;
  Date: Sun, Jan 25, 2015 at 10:35 PM
  Subject: Sandbox evaluation problem - files with comment boxes
  To: users us...@racket-lang.org javascript:;
 
 
 
  I'm trying to create a simple sandbox evaluator (to load in programs in
  *SL). I have the following code:
 
  #lang racket
  (require racket/sandbox)
  (define E
(parameterize ([sandbox-path-permissions
'([write /var/folders]
  [exists /]
  [read /])]
   )
  (make-module-evaluator (string-path test-file.rkt
 
 
  This works fine as long as test-file.rkt does *not* contain a comment
 box.
  If the file contains a comment box, then the following error occurs:
 
  /Applications/Racket
  v6.1.1/share/pkgs/snip-lib/racket/snip/private/load-one.rkt:21:2:
  dynamic-require: unknown module
module name: #resolved-module-path:/Applications/Racket
  v6.1.1/share/pkgs/gui-lib/framework/main.rkt
 
 
 
  I thought maybe parameterizing sandbox-namespace-specs with 'framework
  might do something:
 
  (require racket/sandbox racket/gui)
  (define E
(parameterize ([sandbox-path-permissions
'([write /var/folders]
  [exists /]
  [read /])]
   [sandbox-namespace-specs
(list make-gui-namespace 'framework)]
   )
  (make-module-evaluator (string-path lab01-insulin.rkt
 
  But it results in:
 namespace-attach-module: a different instance of the same module is
  already in the destination namespace
module name: /Applications/Racket
  v6.1.1/collects/racket/stxparam-exptime.rkt
 
 
  Any suggestions?
 
  Thanks!
 
  --- nadeem
  _
Racket Developers list:
http://lists.racket-lang.org/dev



-- 

--
Nadeem Abdul Hamid
Associate Professor, Computer Science
Berry College, Mount Berry, GA 30149
http://cs.berry.edu/~nhamid/
_
  Racket Developers list:
  http://lists.racket-lang.org/dev

Re: [racket-dev] Release process for split repos

2015-01-27 Thread Vincent St-Amour

That sounds good to me.

One concern, though: it looks like recreating old releases requires that
all the participating repos (1) still exist, (2) have the same
name/location, and (3) still have the release tags. I'm not too worried
about (1) and (3), but I could see (2) happening if, e.g., a package
changes maintainer (and therefore location), or if we have to move away
from github at some point.

IIUC, archiving snapshots of the participating repos when the release is
finalized may solve that problem. Does that sound reasonable?

Vincent



At Fri, 23 Jan 2015 15:31:21 -0500,
Ryan Culpepper wrote:
 
 I’ve added a draft of a new release process that takes the repository split 
 into account. The main difference is that there is no longer a single release 
 branch under central management; instead, there is a release branch for each 
 repository, and management responsibilities for package release branches is 
 distributed.
 
 The wiki page is here:
 
   https://github.com/plt/racket/wiki/Release-process
 
 Please review, ask questions, and point out ambiguities and potential 
 problems.
 
 Ryan
 
 
 _
   Racket Developers list:
   http://lists.racket-lang.org/dev

_
  Racket Developers list:
  http://lists.racket-lang.org/dev

Re: [racket-dev] Release process for split repos

2015-01-26 Thread Neil Toronto

I like the general idea. I especially like that you've included 
instructions for repo managers like me who will likely forget everything 
about git branch management and cherry picking between releases.


In the past, you've played the part of central reviewer for requests to 
merge to the release branch. Are we going to try for the same kind of 
consistency now, or leave it up to repo managers?


Neil ⊥

On 01/23/2015 03:31 PM, Ryan Culpepper wrote:

I’ve added a draft of a new release process that takes the repository split 
into account. The main difference is that there is no longer a single release 
branch under central management; instead, there is a release branch for each 
repository, and management responsibilities for package release branches is 
distributed.

The wiki page is here:

   https://github.com/plt/racket/wiki/Release-process

Please review, ask questions, and point out ambiguities and potential problems.

Ryan


_
   Racket Developers list:
   http://lists.racket-lang.org/dev


_
 Racket Developers list:
 http://lists.racket-lang.org/dev

Re: [racket-dev] In Typed Racket, struct declarations do not work in an internal definition context

2015-01-24 Thread Alexis King

Yes, I’d considered that point, and yes, it makes sense. Anyway, the situation 
in which I was trying to do something like this ended up being unnecessary, so 
I don’t even have a valid use-case anymore. I think it’s probably okay to leave 
it as-is unless someone can come up with a useful reason to care.

 On Jan 24, 2015, at 09:24, Sam Tobin-Hochstadt sa...@cs.indiana.edu wrote:
 
 On Thu, Jan 22, 2015 at 3:57 PM, Alexis King lexi.lam...@gmail.com wrote:
 
 I can work around this in a variety of ways—I can extract this into an
 untyped module and use require/typed, I can use vectors to “fake” structs
 and provide an appropriate interface, etc. Still, I wonder if there are any
 plans to resolve this type of problem? Since it seems to be an issue with
 how TR handles types at its core, I’m not even sure how feasible it would
 be.
 
 
 I don't currently have plans to work on this problem. The big issue is
 that Racket structs are what's called generative, meaning that each
 time you execute a struct declaration, you get a different struct
 type. Thus it's not at all clear what the right type should be for
 your `make-me-a-struct` function, and type systems that do allow this
 sort of thing (such as ML) would reject this particular use.
 
 Can you say more about the specific issue you're having? There might
 be a different way around it.
 
 Sam


_
  Racket Developers list:
  http://lists.racket-lang.org/dev

Re: [racket-dev] In Typed Racket, struct declarations do not work in an internal definition context

2015-01-24 Thread Alexis King

I haven’t dug deep enough into the TR code to know for sure, but I think the 
difference is that structs declare fundamentally new types, whereas inline type 
definitions only declare type aliases. Whether or not this is actually the 
problem is unclear—I don’t know TR well enough to answer that.

 On Jan 23, 2015, at 21:23, Alexander D. Knauth alexan...@knauth.org wrote:
 
 There’s a bug report about this here:
 http://bugs.racket-lang.org/query/?cmd=viewpr=14524 
 http://bugs.racket-lang.org/query/?cmd=viewpr=14524
 Though I notice it gives a different error message now.
 But why should structure type declarations being a module-wide construct?
 Internal function definitions work, and internal type definitions work, so 
 why shouldn’t internal structure definitions?
 
 
 On Jan 22, 2015, at 3:57 PM, Alexis King lexi.lam...@gmail.com 
 mailto:lexi.lam...@gmail.com wrote:
 
 Simple enough. This works:
 
 #lang racket
 
 (define (make-me-a-struct)
   (struct foo ())
   (foo))
 
 (make-me-a-struct) ; = #foo
 
 This does not:
 
 #lang typed/racket
 
 (define (make-me-a-struct)
   (struct foo ())
   (foo)) ; error: cannot apply a function with unknown arity
 
 (make-me-a-struct)
 
 This problem makes sense. Type declarations seem to be a module-wide 
 construct, so a type that should be scoped to a single function doesn’t 
 work. I’m running into this issue when trying to create an executable struct 
 using define-struct/exec from within a macro, which doesn’t work due to this 
 particular problem.
 
 I can work around this in a variety of ways—I can extract this into an 
 untyped module and use require/typed, I can use vectors to “fake” structs 
 and provide an appropriate interface, etc. Still, I wonder if there are any 
 plans to resolve this type of problem? Since it seems to be an issue with 
 how TR handles types at its core, I’m not even sure how feasible it would be.
 _
  Racket Developers list:
  http://lists.racket-lang.org/dev http://lists.racket-lang.org/dev
 

_
  Racket Developers list:
  http://lists.racket-lang.org/dev

Re: [racket-dev] In Typed Racket, struct declarations do not work in an internal definition context

2015-01-24 Thread Sam Tobin-Hochstadt

On Thu, Jan 22, 2015 at 3:57 PM, Alexis King lexi.lam...@gmail.com wrote:

 I can work around this in a variety of ways—I can extract this into an
 untyped module and use require/typed, I can use vectors to “fake” structs
 and provide an appropriate interface, etc. Still, I wonder if there are any
 plans to resolve this type of problem? Since it seems to be an issue with
 how TR handles types at its core, I’m not even sure how feasible it would
 be.


I don't currently have plans to work on this problem. The big issue is
that Racket structs are what's called generative, meaning that each
time you execute a struct declaration, you get a different struct
type. Thus it's not at all clear what the right type should be for
your `make-me-a-struct` function, and type systems that do allow this
sort of thing (such as ML) would reject this particular use.

Can you say more about the specific issue you're having? There might
be a different way around it.

Sam

_
  Racket Developers list:
  http://lists.racket-lang.org/dev

Re: [racket-dev] In Typed Racket, struct declarations do not work in an internal definition context

2015-01-23 Thread Alexander D. Knauth

There’s a bug report about this here:
http://bugs.racket-lang.org/query/?cmd=viewpr=14524
Though I notice it gives a different error message now.
But why should structure type declarations being a module-wide construct?
Internal function definitions work, and internal type definitions work, so why 
shouldn’t internal structure definitions?


On Jan 22, 2015, at 3:57 PM, Alexis King lexi.lam...@gmail.com wrote:

 Simple enough. This works:
 
 #lang racket
 
 (define (make-me-a-struct)
   (struct foo ())
   (foo))
 
 (make-me-a-struct) ; = #foo
 
 This does not:
 
 #lang typed/racket
 
 (define (make-me-a-struct)
   (struct foo ())
   (foo)) ; error: cannot apply a function with unknown arity
 
 (make-me-a-struct)
 
 This problem makes sense. Type declarations seem to be a module-wide 
 construct, so a type that should be scoped to a single function doesn’t work. 
 I’m running into this issue when trying to create an executable struct using 
 define-struct/exec from within a macro, which doesn’t work due to this 
 particular problem.
 
 I can work around this in a variety of ways—I can extract this into an 
 untyped module and use require/typed, I can use vectors to “fake” structs and 
 provide an appropriate interface, etc. Still, I wonder if there are any plans 
 to resolve this type of problem? Since it seems to be an issue with how TR 
 handles types at its core, I’m not even sure how feasible it would be.
 _
  Racket Developers list:
  http://lists.racket-lang.org/dev

_
  Racket Developers list:
  http://lists.racket-lang.org/dev

Re: [racket-dev] (reposted from users) Noisy compiler at PLTSTDERR=info

2015-01-22 Thread Matthew Flatt

At Wed, 21 Jan 2015 11:22:38 -0500, Tony Garnock-Jones wrote:
 Over the past few months, more and more subsystems have started logging
 at info level as part of regular compilation.
 
 I prefer having PLTSTDERR=info in order to catch log-info that happens
 at runtime, and find the compile-time log output quite distracting.
 
 My current workaround is to set
 
 PLTSTDERR=info warning@cm warning@compiler/cm warning@module-prefetch
 warning@setup/parallel-build warning@cm-accomplice
 warning@online-check-syntax
 
 but this is quite verbose, and as subsystem log messages come and go
 I'll need to keep updating it.
 
 Could one of the following ideas be worth exploring?
 
  1. Have a superlogger for these (and other?) compile-time-ish loggers,
 so that I could write info warning@compilation, excluding the
 noise in one fell swoop
 
  2. Have a phase number associated with logging, so I could say
 info@0 warning@1, or similar

I have a suggestion below, but it's based on a guess of what you really
want, and it might be a bad guess.


Here's my train of thought:

On 1 above: I've been uncertain of the best way to organize logging
from the start, but the idea of grouping topics hierarchically (such as
a compilation topic group) doesn't sound promising. The original
implementation had a notion of hierarchy that I thought might play out
this way, but it didn't. Overall, it seems to be difficult to fit
topics into a hierarchy a priori, in much the same way that it has been
difficult or awkward to group exceptions hierarchically (and few Racket
libraries attempt to extend the exception hierarchy). I guess there's
often a mismatch between the producer's original idea of organization
the and consumer's eventual idea.

On 2 above: I'm not sure why compilation or phase 1 is special. As more
and more libraries use logging, it seems like they will generate noise
(from your perspective) at run time, too.


More generally:

The most successful step in the logging system's evolution was the move
toward level@topic specifications that include specific topics
of interest. In a growing sea of information, knowing which pieces you
want and specifying those pieces makes sense. Trying to exclude a
category of information is much harder, because it's hard to know all
the information that will be available to exclude.

At the same time, it makes sense to have error messages visible all
the time for all topics, because users should see errors that they
didn't anticipate. Similarly, it makes sense for a user to request
extra unanticipated information at the warning level.

In this sense, the info label is ambiguous. The info level could be
like warning: information that a human consumer might be interested
in without anticipating it, but (unlike warning) not a suggestion of
a problem. Or info could be more like debug: details that are only
useful when you're looking closely at a specific subsystem. A potential
distinction between info and debug is that the former makes sense
to the consumer of the subsystem as opposed to the producer.

My only idea, then, is that we're missing a level somewhere between
debug and warning. My guess is that you're getting too much
information from info, because you wanted a human-volume level of
status information; sometimes info is used for that. Other uses of
info are more like debug --- not really human-volume --- and that's
the part you don't want to see. It happens that many of the current
debug-like uses of info are in compilation subsystems.

If I'm guessing right, then we could introduce a new level and sort out
existing uses:

 * fatal - last-ditch communication channel before termination
 * error - errors
 * warning - info for humans that alerts a potential mistake
 * info - info for humans on status and progress
 * detail - info for subsystem consumers, not necessarily human-volume
 * debug - info for subsystem implementers, not necessarily human-volume

The idea is that most of the compilation messages could move to
detail. (Or maybe it makes sense to add the level between info and
warning; it becomes a transition and compatibility question as much
as anything.)

In retrospect, I realize that I've often struggled with choosing info
vs. debug levels precisely because I haven't been clear on which is
meant as human-volume --- or even that it makes sense to consider a
human-volume vs. machine-volume distinction. Other times, I've
struggled with info vs. debug because of a internal vs. external
distinction.


Does any of that connect to your actual situation and goals?

_
  Racket Developers list:
  http://lists.racket-lang.org/dev

Re: [racket-dev] Full transparency

2015-01-22 Thread Matthew Flatt

I don't think you want to do anything with the compiler or macros.
Instead, it's a matter of having a sufficiently powerful inspector
(which is the concept of inspectability turned into a language
construct).

If you have just

 (struct a (x))
 (a 1)

then the result will print as `#a`. But if you use

 (define orig-i (current-inspector))
 (define sub-i (make-inspector orig-i))

 (current-inspector sub-i)
 (struct a (x))
 (define v (a 1))
 (current-inspector orig-i)

 v

Then, the result will print as `(a 1)`. That's because the structure
declaration is creates under an inspector `sub-i` (which is the current
inspector at the time) that is subordinate to the inspector `orig-i`
that is in place when the structure instance is printed.

The current inspector is determined dynamically, which means that if
you're loading some code, you can set the inspector while loading the
code. For example, if a.rkt is

 #lang racket/base
 (provide v)

 (struct a (x))
 (define v (a 1))

then

 (define v
   (parameterize ([current-inspector (make-inspector)])
 (dynamic-require a.rkt 'v)))
 v

will print the `a` instance transparently.


To protect libraries, there's no safe way to access a root inspector
that controls all structure types when you start Racket. Nothing is
safe from unsafe code, though, and here's an unsafe way to access the
root inspector:

 #lang racket/base
 (require ffi/unsafe)

 (define-cstruct _Scheme_Inspector
   ([stag _short]
[keyex _short]
[depth _int]
[superior _racket]))

 (define root-inspector
   (Scheme_Inspector-superior
((get-ffi-obj 'scheme_get_initial_inspector
  #f
  (_fun - (_gcable _Scheme_Inspector-pointer))

Using `root-inspector`, you can inspect any structure instance.

At Wed, 21 Jan 2015 23:46:10 -0700, Byron Davies wrote:
 Nice parry!  What may be straightforward to you may not be so obvious to
 me.  But I'll take a look.
 
 I'm deep into a project using Racket for weakest precondition analysis.
 Every time I'm debugging it seems like I have to write another
 special-purpose accessor, or export some existing accessor up through
 multiple levels in order to get at the data I need at the top-level.  I
 remember how easy it was with the Lisp Machine to navigate through data no
 matter what it was.
 
 The Lisp Machine offered total transparency, with no real way to protect
 data, to the benefit of the developer.  Racket offers total opacity, to the
 benefit of code security.  I'm hoping there's a middle ground, where
 transparency can be turned on and off.
 
 Byron
 
 On Wed, Jan 21, 2015 at 12:20 PM, Matthias Felleisen matth...@ccs.neu.edu
 wrote:
 
 
  Sounds like a straightforward change to the existing macros. Why don't you
  create a fork and experiment?
 
 
  On Jan 21, 2015, at 1:15 PM, Byron Davies byrondav...@starshine.us
  wrote:
 
   Or, more conservatively, every struct and object in a given package,
  file, or set of files.
  
   On Wed, Jan 21, 2015 at 11:03 AM, Byron Davies byrondav...@starshine.us
  wrote:
   Would it be easy to create a compiler flag that would make every struct
  and object transparent?  This would then make it easy to create a Lisp
  Machine-style Inspector that would be able to roam through every data
  structure during debugging.
  
   Byron
  
  
   _
Racket Developers list:
http://lists.racket-lang.org/dev
 
 
 _
   Racket Developers list:
   http://lists.racket-lang.org/dev
_
  Racket Developers list:
  http://lists.racket-lang.org/dev

Re: [racket-dev] (reposted from users) Noisy compiler at PLTSTDERR=info

2015-01-22 Thread Tony Garnock-Jones

Hi Matthew,

Thanks for those thoughts.

On 01/22/2015 09:11 AM, Matthew Flatt wrote:
 On 1 above: I've been uncertain of the best way to organize logging
 from the start, but the idea of grouping topics hierarchically (such as
 a compilation topic group) doesn't sound promising.

I agree. Better perhaps would be a more relational approach. There are
all sorts of cross-cutting ways one might like to filter log messages:

 - by package author (all the messages in code I wrote)
 - by package
 - by collection
 - by module
 - by specific subroutine?
 - by level (debug, info, warning etc)
 - by phase
 - by place
 - by predicate (e.g. regexp) on log message or log datum

I don't know how to do this yet. Certainly not with the efficiency of
the current logging system!

 I guess there's
 often a mismatch between the producer's original idea of organization
 the and consumer's eventual idea.

Yes, that's a very good point.

 On 2 above: I'm not sure why compilation or phase 1 is special. As more
 and more libraries use logging, it seems like they will generate noise
 (from your perspective) at run time, too.

On reflection, I agree with you. Phase is just one of the many axes
listed above.

 In this sense, the info label is ambiguous. [...]
 My only idea, then, is that we're missing a level somewhere between
 debug and warning.

To me it feels like there is one major divison when it comes to levels:
that between errors/warnings and informational messages. Within each
grouping, less important subdivisions exist.

If I can turn on and off the informational messages as a group, for
individual *subsystems*, I think I'm happy.

So my current workaround works OK for me. Adding an extra gradation
between info and debug wouldn't add much in this example.

I think I'm after finer control of selecting messages on axes *other*
than level/severity.

-- Tony

_
  Racket Developers list:
  http://lists.racket-lang.org/dev

Re: [racket-dev] Full transparency

2015-01-21 Thread Byron Davies

Or, more conservatively, every struct and object in a given package, file,
or set of files.

On Wed, Jan 21, 2015 at 11:03 AM, Byron Davies byrondav...@starshine.us
wrote:

 Would it be easy to create a compiler flag that would make every struct
 and object transparent?  This would then make it easy to create a Lisp
 Machine-style Inspector that would be able to roam through every data
 structure during debugging.

 Byron


_
  Racket Developers list:
  http://lists.racket-lang.org/dev

Re: [racket-dev] Full transparency

2015-01-21 Thread Matthias Felleisen


Sounds like a straightforward change to the existing macros. Why don't you 
create a fork and experiment? 


On Jan 21, 2015, at 1:15 PM, Byron Davies byrondav...@starshine.us wrote:

 Or, more conservatively, every struct and object in a given package, file, or 
 set of files.
 
 On Wed, Jan 21, 2015 at 11:03 AM, Byron Davies byrondav...@starshine.us 
 wrote:
 Would it be easy to create a compiler flag that would make every struct and 
 object transparent?  This would then make it easy to create a Lisp 
 Machine-style Inspector that would be able to roam through every data 
 structure during debugging.
 
 Byron
 
 
 _
  Racket Developers list:
  http://lists.racket-lang.org/dev


_
  Racket Developers list:
  http://lists.racket-lang.org/dev

Re: [racket-dev] Full transparency

2015-01-21 Thread Byron Davies

Nice parry!  What may be straightforward to you may not be so obvious to
me.  But I'll take a look.

I'm deep into a project using Racket for weakest precondition analysis.
Every time I'm debugging it seems like I have to write another
special-purpose accessor, or export some existing accessor up through
multiple levels in order to get at the data I need at the top-level.  I
remember how easy it was with the Lisp Machine to navigate through data no
matter what it was.

The Lisp Machine offered total transparency, with no real way to protect
data, to the benefit of the developer.  Racket offers total opacity, to the
benefit of code security.  I'm hoping there's a middle ground, where
transparency can be turned on and off.

Byron

On Wed, Jan 21, 2015 at 12:20 PM, Matthias Felleisen matth...@ccs.neu.edu
wrote:


 Sounds like a straightforward change to the existing macros. Why don't you
 create a fork and experiment?


 On Jan 21, 2015, at 1:15 PM, Byron Davies byrondav...@starshine.us
 wrote:

  Or, more conservatively, every struct and object in a given package,
 file, or set of files.
 
  On Wed, Jan 21, 2015 at 11:03 AM, Byron Davies byrondav...@starshine.us
 wrote:
  Would it be easy to create a compiler flag that would make every struct
 and object transparent?  This would then make it easy to create a Lisp
 Machine-style Inspector that would be able to roam through every data
 structure during debugging.
 
  Byron
 
 
  _
   Racket Developers list:
   http://lists.racket-lang.org/dev


_
  Racket Developers list:
  http://lists.racket-lang.org/dev

Re: [racket-dev] Compiling a Debuggable Windows Build

2015-01-20 Thread Matthew Flatt

We don't have build products handy on a server, but it shouldn't be
difficult to build yourself using Visual Studio 10. I recommend setting
up the command line using vcvarsall.bat x86_amd64, and then build
from the Git repo using nmake win32-in-place.

That process will give you debugging information in .pdb files, at
least for Racket. It will still build with optimization (so detailed
debugging wouldn't be fun), and there won't be debugging information
for the pre-built graphics and GUI libraries. It might be enough
information to help pinpoint the problem, though.

At Tue, 20 Jan 2015 10:25:04 +0100, Christian Eitner wrote:
 Hello everyone,
 
 I'm trying to analyze bug 14927, which simply states that I cannot
 save any kind of definitions file from DrRacket on Win7 64. The
 message is Racket GUI application has stopped working, i.e., the
 windows crash dialog.
 
 I'm pretty sure the problem is related to my machine only, since on a
 colleague's PC everything works fine.
 
 So I need a Windows build which I can debug. Is there something on the
 build servers which I could use?
 
 I could build locally, having both a Visual Studio (10, 12, 13) and a
 Cygwin 64 environment, or even cross-compile on Ubuntu if that was
 easier/possible.
 
 BTW, how are the provided Windows builds being generated?
 
 Any hints would be welcome.
 
 Thanks for your consideration,
 
 Christian
 _
   Racket Developers list:
   http://lists.racket-lang.org/dev
_
  Racket Developers list:
  http://lists.racket-lang.org/dev

Re: [racket-dev] Compiling a Debuggable Windows Build

2015-01-20 Thread Christian Eitner

Thanks, that should put me on the right track...

The build currently fails because raco is not aware of our mandatory
http proxy, but that is another topic.

Cheers,

Christian

On 20 January 2015 at 15:03, Matthew Flatt mfl...@cs.utah.edu wrote:
 We don't have build products handy on a server, but it shouldn't be
 difficult to build yourself using Visual Studio 10. I recommend setting
 up the command line using vcvarsall.bat x86_amd64, and then build
 from the Git repo using nmake win32-in-place.

 That process will give you debugging information in .pdb files, at
 least for Racket. It will still build with optimization (so detailed
 debugging wouldn't be fun), and there won't be debugging information
 for the pre-built graphics and GUI libraries. It might be enough
 information to help pinpoint the problem, though.

 At Tue, 20 Jan 2015 10:25:04 +0100, Christian Eitner wrote:
 Hello everyone,

 I'm trying to analyze bug 14927, which simply states that I cannot
 save any kind of definitions file from DrRacket on Win7 64. The
 message is Racket GUI application has stopped working, i.e., the
 windows crash dialog.

 I'm pretty sure the problem is related to my machine only, since on a
 colleague's PC everything works fine.

 So I need a Windows build which I can debug. Is there something on the
 build servers which I could use?

 I could build locally, having both a Visual Studio (10, 12, 13) and a
 Cygwin 64 environment, or even cross-compile on Ubuntu if that was
 easier/possible.

 BTW, how are the provided Windows builds being generated?

 Any hints would be welcome.

 Thanks for your consideration,

 Christian
 _
   Racket Developers list:
   http://lists.racket-lang.org/dev
_
  Racket Developers list:
  http://lists.racket-lang.org/dev

Re: [racket-dev] [racket] Implementing contracts for async channels

2015-01-19 Thread Robby Findler

Oh, sorry I missed that.

Robby

On Mon, Jan 19, 2015 at 6:40 PM, Alexis King lexi.lam...@gmail.com wrote:
 I already used blame-add-context, but the message I used wasn’t very good, so 
 I’ve improved it. If everything else looks good, feel free to merge this 
 whenever you get the chance!

 On Jan 19, 2015, at 15:52, Robby Findler ro...@eecs.northwestern.edu wrote:

 Ah: one other note. When you do something like this:

 ((contract (- (list/c (box/c integer?)) any)
   (λ (x) (unbox (car x)))
   'pos 'neg)
 (list (box not an integer)))

 you get an error message that has this text in the middle:

  in: the content of
  the 1st element of
  the 1st argument of
  (- (list/c (box/c integer?)) any)

 This path information is collected in the blame records.

 So, instead of passing along just the blame record you got, call
 blame-add-context so you get some stuff in that portion of the error
 message.

 Maybe a value passed on or something like that would be a good
 phrase? I usually look at a few examples to pick something.

 Otherwise, this looks good to merge to me (but I don't use the
 generics as much as I should so if you wanted to you could try asking
 for someone specifically knowledgeable to look there).

 If you don't, I can push the commit to the appropriate repo. Let me know.

 Robby



 On Mon, Jan 19, 2015 at 5:44 PM, Alexis King lexi.lam...@gmail.com wrote:
 Yes, there are tests, and you can see them here.

 On Jan 19, 2015, at 13:29, Robby Findler ro...@eecs.northwestern.edu
 wrote:

 This seemed okay, but just a quick read of the code. But did I miss
 the test cases? (I just followed the link upthread -- sorry if I need
 to look somewhere else too.)

 Robby


 On Mon, Jan 19, 2015 at 3:15 PM, Alexis King lexi.lam...@gmail.com wrote:

 Any update on this? If there’s anything that still needs to be changed, let
 me know—otherwise, I’ll patiently wait for the process to run its course.
 Just checking in.

 On Jan 16, 2015, at 10:15, Alexis King lexi.lam...@gmail.com wrote:

 Ah, that makes sense, fixed.

 On Jan 16, 2015, at 05:37, Robby Findler ro...@eecs.northwestern.edu
 wrote:

 One comment. The contract combinators are curried so that you can do
 work on the partial applications. So don't write this:

 (define ho-val-first-projection
 impersonate/chaperone-async-channel) ctc) blame) val)

 instead try to do some work earlier, when you first can. (The most
 important thing is to minimize the work done after you get the 'val'
 argument.)

 Robby




 _
 Racket Developers list:
 http://lists.racket-lang.org/dev




_
  Racket Developers list:
  http://lists.racket-lang.org/dev

Re: [racket-dev] [racket] Implementing contracts for async channels

2015-01-19 Thread Alexis King

Yes, there are tests, and you can see them here 
https://github.com/plt/racket/pull/860/files#diff-9383600c097f090324382317068c6187R1.

 On Jan 19, 2015, at 13:29, Robby Findler ro...@eecs.northwestern.edu wrote:
 
 This seemed okay, but just a quick read of the code. But did I miss
 the test cases? (I just followed the link upthread -- sorry if I need
 to look somewhere else too.)
 
 Robby
 
 
 On Mon, Jan 19, 2015 at 3:15 PM, Alexis King lexi.lam...@gmail.com wrote:
 Any update on this? If there’s anything that still needs to be changed, let 
 me know—otherwise, I’ll patiently wait for the process to run its course. 
 Just checking in.
 
 On Jan 16, 2015, at 10:15, Alexis King lexi.lam...@gmail.com wrote:
 
 Ah, that makes sense, fixed.
 
 On Jan 16, 2015, at 05:37, Robby Findler ro...@eecs.northwestern.edu 
 wrote:
 
 One comment. The contract combinators are curried so that you can do
 work on the partial applications. So don't write this:
 
 (define ho-val-first-projection
 impersonate/chaperone-async-channel) ctc) blame) val)
 
 instead try to do some work earlier, when you first can. (The most
 important thing is to minimize the work done after you get the 'val'
 argument.)
 
 Robby
 
 
 
 _
  Racket Developers list:
  http://lists.racket-lang.org/dev

_
  Racket Developers list:
  http://lists.racket-lang.org/dev

Re: [racket-dev] [racket] Implementing contracts for async channels

2015-01-19 Thread Alexis King

Any update on this? If there’s anything that still needs to be changed, let me 
know—otherwise, I’ll patiently wait for the process to run its course. Just 
checking in.

 On Jan 16, 2015, at 10:15, Alexis King lexi.lam...@gmail.com wrote:
 
 Ah, that makes sense, fixed.
 
 On Jan 16, 2015, at 05:37, Robby Findler ro...@eecs.northwestern.edu wrote:
 
 One comment. The contract combinators are curried so that you can do
 work on the partial applications. So don't write this:
 
 (define ho-val-first-projection
 impersonate/chaperone-async-channel) ctc) blame) val)
 
 instead try to do some work earlier, when you first can. (The most
 important thing is to minimize the work done after you get the 'val'
 argument.)
 
 Robby
 


_
  Racket Developers list:
  http://lists.racket-lang.org/dev

Re: [racket-dev] [racket] Implementing contracts for async channels

2015-01-19 Thread Robby Findler

This seemed okay, but just a quick read of the code. But did I miss
the test cases? (I just followed the link upthread -- sorry if I need
to look somewhere else too.)

Robby


On Mon, Jan 19, 2015 at 3:15 PM, Alexis King lexi.lam...@gmail.com wrote:
 Any update on this? If there’s anything that still needs to be changed, let 
 me know—otherwise, I’ll patiently wait for the process to run its course. 
 Just checking in.

 On Jan 16, 2015, at 10:15, Alexis King lexi.lam...@gmail.com wrote:

 Ah, that makes sense, fixed.

 On Jan 16, 2015, at 05:37, Robby Findler ro...@eecs.northwestern.edu 
 wrote:

 One comment. The contract combinators are curried so that you can do
 work on the partial applications. So don't write this:

 (define ho-val-first-projection
 impersonate/chaperone-async-channel) ctc) blame) val)

 instead try to do some work earlier, when you first can. (The most
 important thing is to minimize the work done after you get the 'val'
 argument.)

 Robby



 _
   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

2015-01-18 Thread Benjamin Greenman

On Sun, Jan 18, 2015 at 9:44 AM, Greg Hendershott greghendersh...@gmail.com
 wrote:

 Is there a similarly simple/standard way to disable contracts?


I'd love a #lang like that. Never mind Tony Hoare's metaphor about sailing.
For now, I'm attaching a small patch that'll disable contracts (as far as I
can tell) on the current build; it's adapted from Leif's commits at [1].

;; ---

Please keep the bug reports coming!


It looks like the built-in function expt isn't defined correctly:

(module f racket
  (provide (contract-out [f (integer? . - . integer?)]))
  (define (f n)
(expt n n)))

Contract violation: 'f' violates 'expt'.
Wrong arity
An example module that breaks it:
  (module user racket (require (submid .. f)) (f 0))

  (verification takes 0.035s)

[1] https://github.com/LeifAndersen/racket/tree/no-conracts
From e3a07fa756f47e0eb93be0811f245f1f814f028e Mon Sep 17 00:00:00 2001
From: ben ty...@ccs.neu.edu
Date: Sun, 18 Jan 2015 18:51:48 -0500
Subject: [PATCH] imported leif's no-contract changes

---
 racket/collects/racket/contract/private/base.rkt   |  7 +-
 .../collects/racket/contract/private/provide.rkt   | 80 +++---
 2 files changed, 43 insertions(+), 44 deletions(-)

diff --git a/racket/collects/racket/contract/private/base.rkt b/racket/collects/racket/contract/private/base.rkt
index c7bb61c..cf0ca33 100644
--- a/racket/collects/racket/contract/private/base.rkt
+++ b/racket/collects/racket/contract/private/base.rkt
@@ -35,13 +35,10 @@
 (define-syntax (contract stx)
   (syntax-case stx ()
 [(_ c v pos neg name loc)
- (syntax/loc stx
-   (apply-contract c v pos neg name loc))]
+ (syntax/loc stx v)]
 [(_ c v pos neg)
  (with-syntax ([name (syntax-local-infer-name stx)])
-  (syntax/loc stx
-(apply-contract c v pos neg 'name
-(build-source-location #f]
+  (syntax/loc stx v))]
 [(_ c v pos neg src)
  (raise-syntax-error 'contract
(string-append
diff --git a/racket/collects/racket/contract/private/provide.rkt b/racket/collects/racket/contract/private/provide.rkt
index 5356a64..b020493 100644
--- a/racket/collects/racket/contract/private/provide.rkt
+++ b/racket/collects/racket/contract/private/provide.rkt
@@ -350,42 +350,44 @@
 (raise-syntax-error #f expected an identifier stx #'new-id))
   (unless (identifier? #'orig-id)
 (raise-syntax-error #f expected an identifier stx #'orig-id))
-  (define-values (pos-blame-party-expr srcloc-expr)
-(let loop ([kwd-args (syntax-list #'(kwd-args ...))]
-   [pos-blame-party-expr #'(quote-module-path)]
-   [srcloc-expr #f])
-  (cond
-[(null? kwd-args) (values pos-blame-party-expr
-  (or srcloc-expr (stx-srcloc-expr stx)))]
-[else
- (define kwd (car kwd-args))
- (cond 
-   [(equal? (syntax-e kwd) '#:pos-source)
-(when (null? (cdr kwd-args))
-  (raise-syntax-error #f expected a keyword argument to follow #:pos-source
-  stx))
-(loop (cddr kwd-args)
-  (cadr kwd-args)
-  srcloc-expr)]
-   [(equal? (syntax-e kwd) '#:srcloc)
-(when (null? (cdr kwd-args))
-  (raise-syntax-error #f expected a keyword argument to follow #:srcloc
-  stx))
-(loop (cddr kwd-args)
-  pos-blame-party-expr
-  (cadr kwd-args))]
-   [else
-(raise-syntax-error #f expected either the keyword #:pos-source of #:srcloc
-stx
-(car kwd-args))])])))
-  (internal-function-to-be-figured-out #'ctrct
-   #'orig-id
-   #'orig-id
-   #'new-id
-   #'new-id
-   srcloc-expr
-   'define-module-boundary-contract
-   pos-blame-party-expr))])]))
+  (define new-id orig-id)
+  ;; (define-values (pos-blame-party-expr srcloc-expr)
+  ;;   (let loop ([kwd-args (syntax-list #'(kwd-args ...))]
+  ;;  [pos-blame-party-expr #'(quote-module-path)]
+  ;;  [srcloc-expr #f])
+  ;; (cond
+  ;;   [(null? kwd-args) (values pos-blame-party-expr
+  ;; (or srcloc-expr (stx-srcloc-expr stx)))]
+  ;;   [else
+  ;;(define kwd (car

Re: [racket-dev] Announcing Soft Contract Verification tool

2015-01-18 Thread Greg Hendershott

This looks really exciting!

Imagining using this reminds me of something.

Typed Racket has a simple/standard way to disable type-checking (while
retaining the type declarations for documentation value as well as
potential re-enabling): #lang typed/racket/no-check and #lang
typed/racket/base/no-check.

Is there a similarly simple/standard way to disable contracts?

Last I checked, I couldn't find one. So I think we each write our own
my-define/contract and my-contract-out sort of macros? It's not
difficult. But it's idiosyncratic. Also: tools.

Why not e.g. #lang racket/no-check, and a racket/contract/no-check to
require for use with #lang racket/base?

Although I guess a tool like SCV is more in the business of disabling
individual contracts; not so much whole-file granularity?
_
  Racket Developers list:
  http://lists.racket-lang.org/dev

Re: [racket-dev] Announcing Soft Contract Verification tool

2015-01-16 Thread David Van Horn

On 1/15/15 7:42 PM, Benjamin Greenman wrote:
 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))]))
 
 )


There was a bug causing this to loop which has been fixed.  The server
verifies this program now.

Please keep the bug reports coming!

David



_
  Racket Developers list:
  http://lists.racket-lang.org/dev

Re: [racket-dev] Announcing Soft Contract Verification tool

2015-01-16 Thread David Van Horn

On 1/15/15 2:42 PM, David Van Horn 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).


I misspoke on the issue of boundaries, which we had right, but there
was another bug that's now fixed.  We also fixed the =/c implies
real? bug.

So to summarize, Asumu's program now verifies:

  (module fact racket
(define (factorial x)
  (if (zero? x)
  1
  (* x (factorial (sub1 x)

(provide
  (contract-out
[factorial (- (=/c 0) (=/c 0))])))

A slight variant that uses unsafe contracts will generate
counterexamples causing fact to be blamed:

  (module fact racket
(define (factorial x)
  (if (zero? x)
  1
  (* x (factorial (sub1 x)

(provide
 (contract-out
  [factorial (- (λ (x) (= x 0))
 (λ (x) (= x 0)))])))

The counterexample is:

 (module user racket
   (require (submod .. fact))
   (begin (struct s₃ ()) (factorial (s₃

David


_
  Racket Developers list:
  http://lists.racket-lang.org/dev

Re: [racket-dev] [racket] Implementing contracts for async channels

2015-01-16 Thread Alexis King

Ah, that makes sense, fixed.

 On Jan 16, 2015, at 05:37, Robby Findler ro...@eecs.northwestern.edu wrote:
 
 One comment. The contract combinators are curried so that you can do
 work on the partial applications. So don't write this:
 
 (define ho-val-first-projection
 impersonate/chaperone-async-channel) ctc) blame) val)
 
 instead try to do some work earlier, when you first can. (The most
 important thing is to minimize the work done after you get the 'val'
 argument.)
 
 Robby


_
  Racket Developers list:
  http://lists.racket-lang.org/dev

Re: [racket-dev] Announcing Soft Contract Verification tool

2015-01-15 Thread Matthias Felleisen



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

2015-01-15 Thread Asumu Takikawa

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

2015-01-15 Thread Asumu Takikawa

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

2015-01-15 Thread Alexis King

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

2015-01-15 Thread Alexis King

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

2015-01-15 Thread Sam Tobin-Hochstadt

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

Re: [racket-dev] question, issue(?) with the scope of identifiers passed into define-syntax-rule

2015-01-15 Thread Thomas Lynch

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

2015-01-15 Thread Alexis King

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

2015-01-15 Thread Alexander McLin

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

2015-01-15 Thread Alexander D. Knauth

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