Re: [racket-users] Re: IO in racket is painful

[Richard Cleis]

"Lurking thresholds" are fun:

I used pre-Racket to read files of numerical data, created by different 
agencies across the country.
The code looked for something that looked like a date (out of about 10 
formats), and moved on from there to read a few hundred lines of gradually 
changing groups of numbers. 

The code was quite good at rummaging beyond various useless headers that were 
created over the years by new programmers attempting to improve the world... 
until one day, when someone actually made a truly useful header with an example 
that contained representative data.

rac


On Mar 24, 2016, at 2:14 PM, Hendrik Boom wrote:

> On Thu, Mar 24, 2016 at 08:59:50PM +0100, Jos Koot wrote:
>> Hi
>> 
>> In all computer languages it is more difficult to read data than to write
>> them, I think.
> 
> Perhaps because when you write data you know what you are writing and 
> are in control.   But when you are reading, who knows what might be 
> lurking at the threshold of the file?
> 
> -- hendrik
> 
> -- 
> You received this message because you are subscribed to the Google Groups 
> "Racket Users" group.
> To unsubscribe from this group and stop receiving emails from it, send an 
> email to racket-users+unsubscr...@googlegroups.com.
> For more options, visit https://groups.google.com/d/optout.

On Mar 24, 2016, at 2:14 PM, Hendrik Boom wrote:

> On Thu, Mar 24, 2016 at 08:59:50PM +0100, Jos Koot wrote:
>> Hi
>> 
>> In all computer languages it is more difficult to read data than to write
>> them, I think.
> 
> Perhaps because when you write data you know what you are writing and 
> are in control.   But when you are reading, who knows what might be 
> lurking at the threshold of the file?
> 
> -- hendrik
> 
> -- 
> You received this message because you are subscribed to the Google Groups 
> "Racket Users" group.
> To unsubscribe from this group and stop receiving emails from it, send an 
> email to racket-users+unsubscr...@googlegroups.com.
> For more options, visit https://groups.google.com/d/optout.

-- 
You received this message because you are subscribed to the Google Groups 
"Racket Users" group.
To unsubscribe from this group and stop receiving emails from it, send an email 
to racket-users+unsubscr...@googlegroups.com.
For more options, visit https://groups.google.com/d/optout.

[racket-users] Slack IRC bridge down again

[Jack Firth]

Slack room shows no new messages since Tuesday, yet IRC archives state the room 
is as active as ever. Messages from the slack side aren't crossing over to IRC 
either.

-- 
You received this message because you are subscribed to the Google Groups 
"Racket Users" group.
To unsubscribe from this group and stop receiving emails from it, send an email 
to racket-users+unsubscr...@googlegroups.com.
For more options, visit https://groups.google.com/d/optout.

Re: [racket-users] Redex pattern for "sequence whose elements match this depth 0 pattern"?

['William J. Bowman' via Racket Users]

On Fri, Mar 25, 2016 at 07:05:52AM -0500, Robby Findler wrote:
> I think the right way to approach such questions is to start from a more
> realistic example and then ask "what do we want the typeset version of this
> to look like?".
I like this advice.
Unfortunate, I think I want the typeset version to look like the same
pattern variable in two places but at different depths.

For real example, I have a model of a dependent type system with
inductive type families.
To check that the declared inductive types are valid, I check that
  a) the declared constructors actually return the declared type
  b) the types of the constructors are strictly positive.

Here is a snippet:

(define-judgment-form tt-typingL
  #:mode (valid I)
  #:contract (valid Δ)

  [ "Valid-Empty"
   (valid ∅)]

  [(valid Δ)
   (type-infer Δ ∅ t_D U_D)
   (type-infer Δ (∅ D : t_D) t_c U_c) ...
   ;; NB: Ugh this should be possible with pattern matching alone 
   (side-condition ,(andmap (curry equal? (term D)) (term (D_0 ...
   ;; positive* should probably be a judgment so I can ... it
   (side-condition (positive* D (t_c ...)))
   - "Valid-Inductive"
   (valid (Δ (D : t_D
   ((c : (name t_c (in-hole Ξ (in-hole Θ D_0
...])

I would prefer to write as this as follows.
Notice the D_0 in the conclusion has changed to a D, and the
side-condition that escapes into Racket disappears.

(define-judgment-form tt-typingL
  #:mode (valid I)
  #:contract (valid Δ)

  [ "Valid-Empty"
   (valid ∅)]

  [(valid Δ)
   (type-infer Δ ∅ t_D U_D)
   (type-infer Δ (∅ D : t_D) t_c U_c) ...
   ;; positive* should probably be a judgment so I can ... it
   (side-condition (positive* D (t_c ...)))
   - "Valid-Inductive"
   (valid (Δ (D : t_D
   ((c : (name t_c (in-hole Ξ (in-hole Θ D
...])

In this instance, I suppose I could create a new judgment or
metafunction that checks each constructor's type separately w.r.t. D.
Since both instances would be at depth 0, this would be fine.
Maybe even easier to read..

--
William J. Bowman

PS: You cannot run this email :(

-- 
You received this message because you are subscribed to the Google Groups 
"Racket Users" group.
To unsubscribe from this group and stop receiving emails from it, send an email 
to racket-users+unsubscr...@googlegroups.com.
For more options, visit https://groups.google.com/d/optout.


signature.asc
Description: PGP signature

Re: [racket-users] Re: IO in racket is painful

[Hendrik Boom]

On Thu, Mar 24, 2016 at 08:59:50PM +0100, Jos Koot wrote:
> Hi
> 
> In all computer languages it is more difficult to read data than to write
> them, I think.

Perhaps because when you write data you know what you are writing and 
are in control.   But when you are reading, who knows what might be 
lurking at the threshold of the file?

-- hendrik

-- 
You received this message because you are subscribed to the Google Groups 
"Racket Users" group.
To unsubscribe from this group and stop receiving emails from it, send an email 
to racket-users+unsubscr...@googlegroups.com.
For more options, visit https://groups.google.com/d/optout.

Re: [racket-users] Redex pattern for "sequence whose elements match this depth 0 pattern"?

[Robby Findler]

I think the right way to approach such questions is to start from a more
realistic example and then ask "what do we want the typeset version of this
to look like?". The answer, when looked at that way is almost never "extend
the pattern language" since additional complexity there is not something
readers of your paper will understand. I find the answer generally takes
the form of an additional meta function that hides some complexity but is
given a nice name.

Robby

On Thursday, March 24, 2016, 'William J. Bowman' via Racket Users <
racket-users@googlegroups.com> wrote:

> #lang scribble/doc Ha, you can run this email!
>
> In Redex, I have on several occasions found myself trying to use a
> pattern to constrain a sequence's member to match that pattern.
> i.e., I want to use a pattern bound at depth 0 to constrain a pattern
> at depth 1.
> Unfortunately, I can't do this, so it seems I must escape into Racket
> and enforce this constraint with andmap and equal?.
> I'm hoping someone can tell me there is a better way.
>
> For example:
>
> @(require
>   redex/reduction-semantics
>   racket/function)
>
> @(define-language testL
>[x ::= variable-not-otherwise-mentioned])
>
> (define-judgment-form testL
>   #:mode (complex-match I)
>   #:contract (complex-match (x (x ...)))
>
>[-
> (complex-match (x (x ...)))])
>
> Gives this error:
> ; : define-judgment-form: found the same binder, x, at different
> depths, 0 and 1
> ;   at: x
> ;   in: (x (x ...))
>
> So, I am forced to write this:
>
> @(define-judgment-form testL
>   #:mode (complex-match_0 I)
>   #:contract (complex-match_0 (x (x ...)))
>
>   [;; NB: Ugh this should be possible with pattern matching alone 
>(side-condition ,(andmap (curry equal? (term x)) (term (x_0 ...
>-
>(complex-match_0 (x (x_0 ...)))])
>
> @(require rackunit)
> @(check-true
>   (judgment-holds (complex-match_0 (x (x)
> @(check-true
>   (judgment-holds (complex-match_0 (foo (foo foo)
> @(check-false
>   (judgment-holds (complex-match_0 (x (y z))
>
>
> This is particularly annoying, since I can easily do almost the
> *opposite*, i.e., use a depth 0 pattern while constraining a sequence's
> members to be distinct.
>
> @(define-judgment-form testL
>   #:mode (complex-not-match I)
>   #:contract (complex-not-match (x (x ...)))
>
>   [-
>(complex-not-match (x_!_0 (x_!_0 ...)))])
>
> @(check-false
>   (judgment-holds (complex-not-match (x (x)
> @(check-false
>   (judgment-holds (complex-not-match (foo (foo foo)
> @(check-true
>   (judgment-holds (complex-not-match (x (y z))
>
>
> If there is no better way, would it be too much to ask for a new
> pattern that does this? E.g., perhaps (x_=_0 (x_=_0 ...))?
>
> --
> William J. Bowman
> Northeastern University
> College of Computer and Information Science
>
> --
> You received this message because you are subscribed to the Google Groups
> "Racket Users" group.
> To unsubscribe from this group and stop receiving emails from it, send an
> email to racket-users+unsubscr...@googlegroups.com .
> For more options, visit https://groups.google.com/d/optout.
>

-- 
You received this message because you are subscribed to the Google Groups 
"Racket Users" group.
To unsubscribe from this group and stop receiving emails from it, send an email 
to racket-users+unsubscr...@googlegroups.com.
For more options, visit https://groups.google.com/d/optout.