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

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

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

 On Jan 29, 2015, at 9:25 PM, Alexis King 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:

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

 Thank you,
  Racket Developers list:

   Racket Developers list:

  Racket Developers list:

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

 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)

From e3a07fa756f47e0eb93be0811f245f1f814f028e Mon Sep 17 00:00:00 2001
From: ben
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
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)))]
- (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
-(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-15 Thread Benjamin Greenman
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

(module div racket
  (provide (contract-out [divides? (- positive? positive? boolean?)]))

  (define (positive? x)
(and (integer? x) (= 0 x)))

  (define (divides? a b)
(cond [(= 0 b) #t]
  [( b a) #f]
  [else (divides? a (- b a))]))


On Thu, Jan 15, 2015 at 3:14 PM, David Van Horn wrote:

 On 1/15/15, 2:48 PM, Robby Findler wrote:
  Can you randomly make up programs from your grammar, get example
  errors from the tool, and then run those programs to see if you
  find bugs in the analysis like that one?

 Yes, we're planning to do this.

  That said, I don't see how the bug in =/c is coming in here. Can
  you explain more?

 On further inspection, the counterexample is wrong.  (There are
 counterexamples due to the model of =/c, but the one that reported is
 not an actual one.)  This will be fixed shortly.


   Racket Developers list:

  Racket Developers list:

[racket-dev] managing packages

2014-11-05 Thread Benjamin Greenman
I hear that Racket is having some trouble determining who broke what in
the package ecosystem. I do not know the specifics of this problem, but
there was a recent discussion on the OCaml mailing list about OPAM's method
of tracking package compatibility that may be relevant:

In particular, the second message (of 26) in the thread has a link to a
survey paper on the formal aspects of package systems.
  Racket Developers list: