[racket] users Digest, Vol 109, Issue 66

Please take me off the list

Thanks

On Sun, Sep 28, 2014 at 11:29 AM,  <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? (Sam Tobin-Hochstadt)
>    2. Re: proof assistants, DrRacket and Bootstrap (Bill Richter)
>    3. Re: proof assistants, DrRacket and Bootstrap (Matthias Felleisen)
>    4. Re: proof assistants, DrRacket and Bootstrap (Bill Richter)
>    5. (fourth RacketCon) videos (Asumu Takikawa)
>    6. Re: proof assistants, DrRacket and Bootstrap (Prabhakar Ragde)
>
>
> ----------------------------------------------------------------------
>
> Message: 1
> Date: Sat, 27 Sep 2014 21:58:14 -0400
> From: Sam Tobin-Hochstadt <samth at cs.indiana.edu>
> To: Anthony Carrico <acarrico at memebeam.org>
> 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:
>         <CAK=HD+aVN_KNXZtf9_9WSFftehQN5m_xb7qGFEgHdpb1EuVXCQ at mail.gmail.com>
> Content-Type: text/plain; charset=UTF-8
>
> On Sat, Sep 27, 2014 at 9:11 PM, Anthony Carrico <acarrico at memebeam.org> wrote:
>> On 09/27/2014 09:49 AM, Alexander D. Knauth wrote:
>>> Like this, I think:  (but for some reason it seems to print it 3 times?)
>>> #lang typed/racket
>>>
>>> (struct foo () #:transparent
>>>   #:property prop:custom-write
>>>   (lambda (this out mode)
>>>     (displayln "whatever")))
>>>
>>> (print (foo))
>>
>> I didn't realize #:property was legal in typed struct. I guess there
>> should be a documentation update here:
>>   http://docs.racket-lang.org/ts-reference/special-forms.html
>
> No, instead we need to change typed racket to reject those programs.
> However, that would break a bunch of code with no easy fix that relies
> on getting away with this, so we'll probably have to wait till we have
> a real story here.
>
>> BTW change your program to use the given port: (displayln "whatever"
>> out) to avoid the double printing problem, although I'm not exactly sure
>> why it would have that effect.
>
> It prints multiple times (to hidden output ports) to detect cycles
> among other things.
>
> Sam
>
>> Thanks!
>>
>> --
>> Anthony Carrico
>>
>>
>>
>> ____________________
>>   Racket Users list:
>>   http://lists.racket-lang.org/users
>>
>
>
> ------------------------------
>
> Message: 2
> Date: Sat, 27 Sep 2014 23:57:12 -0500
> From: Bill Richter <richter at math.northwestern.edu>
> To: Prabhakar Ragde <plragde at uwaterloo.ca>
> Cc: users at racket-lang.org
> Subject: Re: [racket] proof assistants, DrRacket and Bootstrap
> Message-ID:
>         <201409280457.s8S4vCrp000773 at poisson.math.northwestern.edu>
>
>    Translating the gist of suggestions to such posters, I would say:
>    do you really need to execute *any* expression? If not, use
>    OCamllex and/or OCamlyacc (maybe Menhir, or a smaller and cleaner
>    parser combinator library) to write a parser for your language
>    subset, and then write an interpreter for the resulting ASTs.
>
> Thanks, Prabhakar!  I think something like what you're saying is true.  HOL Light is based on quite a lot of the OCaml parser camlp, and I've thought for a long time that I had to learn it myself.
>
>    I don't have enough practice in OCaml to grasp what your code does
>
> I'm making a dialect ofHOL Light with different syntax by interpreting one of my programs as a string and then breaking the string up into the component pieces, but then I need this Toploop/exec hack to evaluate my variables.  That sounds like the Scheme eval, and in Scheme you can solve that problem nicely with the quote feature.
>
> --
> Best,
> Bill
>
>
> ------------------------------
>
> Message: 3
> Date: Sat, 27 Sep 2014 16:00:35 -0600
> From: Matthias Felleisen <matthias 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: <B7FBF0FD-EA70-44BE-BB63-577E2E1B6CFF at ccs.neu.edu>
> Content-Type: text/plain; charset=us-ascii
>
>
> On Sep 27, 2014, at 1:38 AM, Bill Richter wrote:
>
>> 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.
>
> Decouple parsing from interpreting and your ML interpreter for ML won't look too different from your Lisp/Racket/Scheme interpreter for Lisp/Racket/Scheme. Indeed, almost everyone who does the latter actually does some form of decoupling usually.
>
> In general,
>
>  (1) pick a representation for your chosen programming language that is tree-oriented, call it AST
>  (2) pick a representation for the values that your programs may return, call it VAL
>  (3) design a function
>
>         interpreter : AST -> VAL
>
>  (4) for a typed language, also design a function
>
>         type_check : AST -> Boolean
>
> In ML, you might try
>
>   type ast = VAR of String | LAM of String * ast | APP of ast * ast | CONST of int | ADD of ast * ast
>   type val = BASIC of int | FUNCTION of val -> val | ...
>
>
>> 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?
>
>
> 1. HtDP explains the above in a couple of sections.
>
> 2. HtDP is for college freshmen (roughly) and for high school students who have the patience to read. The occasional 7th and 8th grader work their way thru HtDP with adults who understand HtDP or learn to understand HtDP that way. The basic 7th grader will benefit from the material at bootstrap-world.org, which is what we use with many middle school students around the country.
>
> -- Matthias
>
>
>
>
>
>
>
>
> ------------------------------
>
> Message: 4
> Date: Sun, 28 Sep 2014 00:39:20 -0500
> From: Bill Richter <richter at math.northwestern.edu>
> To: Matthias Felleisen <matthias at ccs.neu.edu>
> Cc: users at racket-lang.org
> Subject: Re: [racket] proof assistants, DrRacket and Bootstrap
> Message-ID:
>         <201409280539.s8S5dKcx001372 at poisson.math.northwestern.edu>
> Content-Type: text/plain; charset=utf-8
>
>      type ast = VAR of String | LAM of String * ast | APP of ast * ast | CONST of int | ADD of ast * ast
>      type val = BASIC of int | FUNCTION of val -> val | ...
>
> Thanks, Matthias!  I know this is way off topic, but I think it's the sort of thing only Schemers understand, and I think HOL Light would be a lot better off my problem got solved.  There's a lot I didn't understand with your ML explanation.  Is this written down somewhere?  How to write a ML interpreter in ML using your type ideas?  Are you saying I don't need camlp parsing?  I would find that hard to believe.  Formal proofs in HOL Light are really just OCaml programs where a lot of code has already been evaluated.  Here's a simple Hilbert geometry program in my dialect:
>
> let ExistsPointOffLine = theorem `;
>   ?l. Line l  ?  ?Q. Q ? l
>
>   proof
>     intro_TAC ?l, H1;
>     consider A B C such that
>     ?(A = B) ? ?(A = C) ? ?(B = C) ? ?Collinear A B C     [Distinct] by fol I3;
>     assume (A ? l) ? (B ? l) ? (C ? l)     [all_on] by fol ?;
>     Collinear A B C     [] by fol H1 - Collinear_DEF;
>     fol - Distinct;
>   qed;
> `;;
>
> I think I need the `;[...]` construct, which at present just turns my proof into a string without any backslash or newline problems, which is then passed to my function theorem.  The usual HOL Light style is like this, using instead a function prove:
>
> let MULT_0 = prove
>  (`!m. m * 0 = 0`,
>   INDUCT_TAC THEN ASM_REWRITE_TAC[MULT; ADD_CLAUSES]);;
>
> Notice the related `[...]` construct, which I think sends the ordered pair off to heavy camlp parsing.
>
> Thanks for the 7th and 8th advice.  I think my student is smart and hard-working, and I (finally!) learned how to program reading your book HtDP, so it sounds like you're saying that I should be able to teach it to my student.  I went to bootstrap-world.org and, uh, maybe I didn't look hard enough, but I didn't find anything that looked juicy.
>
> --
> Best,
> Bill
>
>
> ------------------------------
>
> Message: 5
> Date: Sun, 28 Sep 2014 11:17:15 -0400
> From: Asumu Takikawa <asumu at ccs.neu.edu>
> To: Racket Users <users at racket-lang.org>
> Subject: [racket] (fourth RacketCon) videos
> Message-ID: <20140928151714.GH30398 at localhost>
> Content-Type: text/plain; charset=us-ascii
>
> Hi all,
>
> The hi-res talk recordings for (fourth RacketCon) are now up on Youtube.
> You can watch all of them via this playlist:
>
>   https://www.youtube.com/playlist?list=PLXr4KViVC0qI9t3lizitiFJ1cFIeN2Gdh
>
> Let me know if you find any glitches.
>
> Cheers,
> Asumu
>
>
> ------------------------------
>
> Message: 6
> Date: Sun, 28 Sep 2014 11:29:32 -0400
> From: Prabhakar Ragde <plragde at uwaterloo.ca>
> To: Bill Richter <richter at math.northwestern.edu>
> Cc: users at racket-lang.org
> Subject: Re: [racket] proof assistants, DrRacket and Bootstrap
> Message-ID: <5428295C.5050006 at uwaterloo.ca>
> Content-Type: text/plain; charset=ISO-8859-1; format=flowed
>
> On 2014-09-28, 12:57 AM, Bill Richter wrote:
>
>> I'm making a dialect of HOL Light with different syntax by
>> interpreting one of my programs as a string and then breaking the
>> string up into the component pieces, but then I need this
>> Toploop/exec hack to evaluate my variables.  That sounds like the
>> Scheme eval, and in Scheme you can solve that problem nicely with the
>> quote feature.
>
> A Racketeer would probably tell you to use macros to define your
> dialect, instead of using an eval hack. The corresponding tool for OCaml
> is camlp4, and it sounds as if it would be worth your time to learn it
> thoroughly. --PR
>
>
> End of users Digest, Vol 109, Issue 66
> **************************************