[racket] users Digest, Vol 109, Issue 64

Please take me off the list

Thanks

On Sat, Sep 27, 2014 at 5:08 PM,  <users-request at racket-lang.org> wrote:
> Send users mailing list submissions to
>         users at racket-lang.org
>
> To subscribe or unsubscribe via the World Wide Web, visit
>         http://lists.racket-lang.org/users/listinfo
> or, via email, send a message with subject or body 'help' to
>         users-request at racket-lang.org
>
> You can reach the person managing the list at
>         users-owner at racket-lang.org
>
> When replying, please edit your Subject line so it is more specific
> than "Re: Contents of users digest..."
>
>
> [Racket Users list:
>  http://lists.racket-lang.org/users ]
>
>
> Today's Topics:
>
>    1. Re: typed racket and generic interfaces,  is there a
>       workaround using properties? (Alexander D. Knauth)
>    2. Re: proof assistants, DrRacket and Bootstrap (J. Ian Johnson)
>    3. aws/glacier: credential scope (Norman Gray)
>    4. Re: proof assistants, DrRacket and Bootstrap (Bill Richter)
>
>
> ----------------------------------------------------------------------
>
> Message: 1
> Date: Sat, 27 Sep 2014 13:55:12 -0400
> From: "Alexander D. Knauth" <alexander at knauth.org>
> To: Spencer florence <spencerflorence at gmail.com>
> Cc: racket users list <users at racket-lang.org>
> Subject: Re: [racket] typed racket and generic interfaces,      is there a
>         workaround using properties?
> Message-ID: <38E7C628-8FA0-4F07-ABAD-E271E2A66426 at knauth.org>
> Content-Type: text/plain; charset="windows-1252"
>
> Actually using prop:dict works (I hadn?t found prop:dict yet when I first asked this)
> #lang typed/racket
>
> (define-type Dict-Ref ([Dict Any] [Any] . ->* . Any))
> (define-type Dict-Set! (Dict Any Any . -> . Void))
> (define-type Dict-Set (Dict Any Any . -> . Dict))
> (define-type Dict-Remove! (Dict Any . -> . Void))
> (define-type Dict-Remove (Dict Any . -> . Dict))
> (define-type Dict-Iterate-First (Dict . -> . Any))
> (define-type Dict-Iterate-Next (Dict Any . -> . Any))
> (define-type Dict-Iterate-Key (Dict Any . -> . Any))
> (define-type Dict-Iterate-Value (Dict Any . -> . Any))
> (define-type Dict-Count (Dict . -> . Natural))
>
> (require/typed racket/dict
>                [#:opaque Dict dict?]
>                [dict-ref Dict-Ref]
>                [dict-set! Dict-Set!]
>                [dict-set Dict-Set]
>                [dict-remove! Dict-Remove!]
>                [dict-remove Dict-Remove]
>                [dict-iterate-first Dict-Iterate-First]
>                [dict-iterate-next Dict-Iterate-Next]
>                [dict-iterate-key Dict-Iterate-Key]
>                [dict-iterate-value Dict-Iterate-Value]
>                [dict-count Dict-Count]
>                [prop:dict Struct-Type-Property])
>
> (define (make-dict-prop #:dict-ref [dict-ref : Dict-Ref]
>                         #:dict-set! [dict-set! : (U Dict-Set! #f) #f]
>                         #:dict-set [dict-set : (U Dict-Set #f) #f]
>                         #:dict-remove! [dict-remove! : (U Dict-Remove! #f) #f]
>                         #:dict-remove [dict-remove : (U Dict-Remove #f) #f]
>                         #:dict-count [dict-count : Dict-Count]
>                         #:dict-iterate-first [dict-iterate-first : Dict-Iterate-First]
>                         #:dict-iterate-next [dict-iterate-next : Dict-Iterate-Next]
>                         #:dict-iterate-key [dict-iterate-key : Dict-Iterate-Key]
>                         #:dict-iterate-value [dict-iterate-value : Dict-Iterate-Value])
>   (vector-immutable dict-ref
>                     dict-set!
>                     dict-set
>                     dict-remove!
>                     dict-remove
>                     dict-count
>                     dict-iterate-first
>                     dict-iterate-next
>                     dict-iterate-key
>                     dict-iterate-value))
>
> (struct foo () #:transparent
>   #:property prop:dict
>   (make-dict-prop #:dict-ref (lambda (this key [failure #f]) "whatever")
>                   #:dict-count (lambda (this) 0)
>                   #:dict-iterate-first (lambda (this) #f)
>                   #:dict-iterate-next (lambda (this pos) 0)
>                   #:dict-iterate-key (lambda (this pos) pos)
>                   #:dict-iterate-value (lambda (this pos) "whatever")))
>
> (dict-ref (assert (foo) dict?) "idontkare")
>
>
> On Sep 27, 2014, at 1:07 AM, Spencer florence <spencerflorence at gmail.com> wrote:
>
>> I don?t think you can. You would need define the struct in an untyped module then require it via require/typed. This is why dict?s don?t work in typed/racket either.
>>
>>
>>
>> On Sat, May 24, 2014 at 9:39 PM, Alexander D. Knauth <alexander at knauth.org> wrote:
>>
>> Do generic interfaces work using structure type properties, and if they do, is there a way to use generic interfaces through properties so that I can do it in typed racket?
>>
>> Specifically I?m trying to use the gen:custom-write and gen:dict generic interfaces. I can use prop:custom-write for the first one, but I don?t know what to do for gen:dict.
>>
>> Otherwise I?ll just put it in an untyped submodule.
>>
>>
>> ____________________
>> Racket Users list:
>> http://lists.racket-lang.org/users
>>
>>
>
> -------------- next part --------------
> An HTML attachment was scrubbed...
> URL: <http://lists.racket-lang.org/users/archive/attachments/20140927/17fc9f08/attachment-0001.html>
>
> ------------------------------
>
> Message: 2
> Date: Sat, 27 Sep 2014 16:09:09 -0400 (EDT)
> From: "J. Ian Johnson" <ianj at ccs.neu.edu>
> To: Bill Richter <richter at math.northwestern.edu>
> Cc: users at racket-lang.org
> Subject: Re: [racket] proof assistants, DrRacket and Bootstrap
> Message-ID: <28884853.169131411848549503.JavaMail.root at zimbra>
> Content-Type: text/plain; charset=utf-8
>
> To answer the first part of your email, yes. Carl Eastlund developed Dracula for Rackety use of the ACL2 theorem prover.
> -Ian
> ----- Original Message -----
> From: Bill Richter <richter at math.northwestern.edu>
> To: users at racket-lang.org
> Sent: Sat, 27 Sep 2014 03:38:48 -0400 (EDT)
> Subject: [racket] proof assistants, DrRacket and Bootstrap
>
> I have a few questions that might be off-topic.  Are you interested in formal proofs?  Have you considered adapting DrRacket to give an integrated editor for a proof assistant?  The proof assistants Coq and Isabelle use jedit and ProofGeneral, which I think aren't nearly as nice as DrRacket.  I actually use HOL Light, which nobody uses an integrated editor for.  Here are the slides for a talk I gave at the Institut Henri Poincar? in the workshop ``Formalization of mathematics in proof assistants''
> http://www.math.northwestern.edu/~richter/RichterIHPslide.pdf
>
> HOL Light and Coq are written in OCaml, a dialect of ML, which is therefore similar to Scheme, but it has one difference that I wonder if anyone here's knows how to deal with.  Scheme is well-suited for writing a Scheme interpreter, because of the quote feature.  OCaml doesn't have a quote feature, so the question arises how to write an OCaml interpreter inside OCaml.  That's not quite what I want to do, but if anyone could explain how to do it, I'd be grateful.
>
> I have a 7th grade student I'm trying to teach Racket, and I'm a bit confused about Bootstrap and Program By Design.  Is there any reason for my student not to just read HtDP?
>
> --
> Best,
> Bill
> ____________________
>   Racket Users list:
>   http://lists.racket-lang.org/users
>
>
>
>
> ------------------------------
>
> Message: 3
> Date: Sat, 27 Sep 2014 21:14:55 +0100
> From: Norman Gray <norman at astro.gla.ac.uk>
> To: racket users list <users at racket-lang.org>
> Subject: [racket] aws/glacier: credential scope
> Message-ID: <0CA916BA-DD1E-47E9-BFA1-7092EC3F17F5 at astro.gla.ac.uk>
> Content-Type: text/plain; charset=us-ascii
>
>
> Greetings.
>
> I'm trying to use the aws/glacier package, and running into a problem where I'm being told:
>
>     Credential should be scoped to a valid region, not 'eu-west-1'
>
> I'm following the instructions at <https://github.com/greghendershott/aws/blob/master/aws/manual.md>
>
> My test code is:
>
>     % cat glacier.rkt
>     #lang racket/base
>
>     (require aws/glacier
>              aws/keys)
>
>     (define vault "testvault")
>     (region "eu-west-1")
>     (read-keys "aws-zbu-credentials") ; local file
>
>     (module+ main
>       (printf "region=~a~%" (region))
>       (printf "Vaults: ~s~%" (list-vaults))
>       (printf "...specifically: ~s~%" (describe-vault vault)))
>
> Running this produces:
>
>     % racket glacier.rkt
>     region=eu-west-1
>     aws: HTTP/1.1 403 Forbidden
>     x-amzn-RequestId: Un3-L2zlaJBPyrIVKJrWuQcqtMMYQAr34gYUOSScg6Qepc4
>     Content-Type: application/json
>     Content-Length: 129
>     Date: Sat, 27 Sep 2014 18:35:50 GMT
>
>      {"message":"Credential should be scoped to a valid region, not 'eu-west-1'. ","code":"InvalidSignatureException","type":"Client"}
>     HTTP 403 "Forbidden". AWS Code="InvalidSignatureException" Message="Credential should be scoped to a valid region, not 'eu-west-1'. "
>       context...:
>        check-response
>        /Users/norman/Library/Racket/6.1/pkgs/aws/aws/glacier.rkt:97:22: temp68
>        request/redirect/uri
>        (submod /checkouts/me/code/zbu/glacier.rkt main): [running body]
>
> Things I thought of:
>
>   * Printing (public-key)/(private-key) indicates that the credentials are being read correctly.
>   * When I change the argument of (region) to "us-west-1", that's the region that appears in the error message.
>   * My "testvault" vault is in eu-west-1 (and this is indeed one of the valid regions for glacier, reported in <http://docs.aws.amazon.com/general/latest/gr/rande.html> and which does have a host at http://glacier.eu-west-1.amazonaws.com
>   * As far as I can see, credentials are _not_ scoped, but are all at us-east-1.
>   * <http://docs.aws.amazon.com/general/latest/gr/signature-v4-troubleshooting.html> says that "IAM [...] accepts only us-east-1 as its region specification", so I'm taking it that (region) is for setting the _vault_'s region.
>   * I'm not a great AWS expert, so I could have something in my setup broken; but if so, I've no clue what.
>
> If, however, I change the (region) argument to "us-east-1", I get a different error message "User: arn:aws:iam::786725553169:user/zbu is not authorized to perform: glacier:ListVaults on resource: arn:aws:glacier:us-east-1:786725553169:vaults/"  That makes sense, since there's no such vault, but it's interesting that it gets _further_ when the (region) matches the region for the IAM service.
>
> I don't see any other (region) equivalents for the other services supported by the package.  Is that because all of the other services supported by the package are supported by all the AWS regions, or am I missing a configuration?
>
> Thanks for any pointers.
>
> All the best,
>
> Norman
>
>
> --
> Norman Gray  :  http://nxg.me.uk
> SUPA School of Physics and Astronomy, University of Glasgow, UK
>
>
>
>
> ------------------------------
>
> Message: 4
> Date: Sat, 27 Sep 2014 16:08:49 -0500
> From: Bill Richter <richter at math.northwestern.edu>
> To: "J. Ian Johnson" <ianj at ccs.neu.edu>
> Cc: users at racket-lang.org
> Subject: Re: [racket] proof assistants, DrRacket and Bootstrap
> Message-ID:
>         <201409272108.s8RL8nqh030467 at poisson.math.northwestern.edu>
>
>    Carl Eastlund developed Dracula for Rackety use of the ACL2 theorem prover.
>
> Thanks, Ian!  May I suggest that you try to handle Coq, Isabelle or HOL Light?  I believe these are the foremost proof assistants.  The fields medalist Vladimir Voevodsky uses Coq, in which the 4-color theorem and the Feit-Thompson theorem was formalized by Georges Gonthier.  Tom Hales just finished formalizing his proof of Kepler conjecture in HOL Light and Isabelle (which is HOL as well).  I'm no expert, but I think that ACL2 (also Prover9) is an FOL prover, and the bulk of activity in formal proofs uses type theories.  HOL is simple, it's Church's simple types (a version of the Lambda Calculus), and Coq uses a much more complicated type theory.
>
> --
> Best,
> Bill
>
>
> End of users Digest, Vol 109, Issue 64
> **************************************