[racket-users] Re: Is there a way to return no value?

2015-12-10 Thread Matthew Butterick
Answer: Yes, if you redefine nothingness. You can exploit the fact that 
appending (or splicing) an empty list will cause it to disappear (meaning, no 
# residue).

#lang racket
(require rackunit)
(define (foo-3 x) (if (eq? x "foo") (list #t) empty))
(check-equal? (append-map foo-3 '(a b "foo" "bar")) '(#t))




On Thursday, December 10, 2015 at 10:16:40 PM UTC-8, David K. Storrs wrote:
> Question: Is there a way to make a function return nothing -- not '() or 
> #void, but actually nothing?
> 
> 
> I'm playing around with HTML parsing as a learning exercise.  The current 
> exercise is writing a look-down function which can be handed an HTML value 
> produced by the html library and a function, run the function across the 
> collect the results, and return them.  I would use this for things like "find 
> every link in the following document" or "capitalize every use of the word 
> 'kumquat'" or etc.
> 
> I would like to have a way to say "this element isn't interesting, just 
> ignore it" so that I don't get spurious return values in the results list.  I 
> can't see a way to do that...I can exclude the values afterwards, but that's 
> not really what I was looking for, and opens the door to false negatives.  
> 
> Here's some simplified test code (removing all the HTML stuff for clarity) to 
> show the point:
> 
> 
> 
> (define (foo-1 x) (if (eq? x "foo") #t '()))
> (define (foo-2 x) (if (eq? x "foo") #t (values)))
> 
> (map foo-1 '(a b "foo" "bar"))
> (filter (lambda (x) (not (null? x))) (map foo-1 '(a b "foo" "bar")))
> (map foo-2 '(a b "foo" "bar"))
> 
> [dstorrs@localhost:~/personal/study/scheme/spider:]$ racket test.rkt
> racket test.rkt
> '(() () #t ())
> '(#t)
> result arity mismatch;
>  expected number of values not received
>   expected: 1
>   received: 0
>   values...:
>   context...:
>/Users/dstorrs/personal/study/scheme/spider/test.rkt: [running body]
> 
> 
> Instead of a 'result arity' crash, I would have liked to get '(#t) back, same 
> a if I'd generated the list and then filtered it.
> 
> Is there a way to do this?
> 
> 
> For the record, here's the actual look-down function:
> 
> (require (prefix-in h: html)
>  (prefix-in x: xml))
> 
> (define (look-down el action)
>   (match el
>  [(struct h:html-full (attributes content))
>   (apply append (map action content))]
> 
>  [(struct h:html-element (attributes))
>   (action el)]
> 
>  [ _ '()]))

-- 
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] Is there a way to return no value?

2015-12-10 Thread David K. Storrs
Question: Is there a way to make a function return nothing -- not '() or #void, 
but actually nothing?


I'm playing around with HTML parsing as a learning exercise.  The current 
exercise is writing a look-down function which can be handed an HTML value 
produced by the html library and a function, run the function across the 
collect the results, and return them.  I would use this for things like "find 
every link in the following document" or "capitalize every use of the word 
'kumquat'" or etc.

I would like to have a way to say "this element isn't interesting, just ignore 
it" so that I don't get spurious return values in the results list.  I can't 
see a way to do that...I can exclude the values afterwards, but that's not 
really what I was looking for, and opens the door to false negatives.  

Here's some simplified test code (removing all the HTML stuff for clarity) to 
show the point:



(define (foo-1 x) (if (eq? x "foo") #t '()))
(define (foo-2 x) (if (eq? x "foo") #t (values)))

(map foo-1 '(a b "foo" "bar"))
(filter (lambda (x) (not (null? x))) (map foo-1 '(a b "foo" "bar")))
(map foo-2 '(a b "foo" "bar"))

[dstorrs@localhost:~/personal/study/scheme/spider:]$ racket test.rkt
racket test.rkt
'(() () #t ())
'(#t)
result arity mismatch;
 expected number of values not received
  expected: 1
  received: 0
  values...:
  context...:
   /Users/dstorrs/personal/study/scheme/spider/test.rkt: [running body]


Instead of a 'result arity' crash, I would have liked to get '(#t) back, same a 
if I'd generated the list and then filtered it.

Is there a way to do this?


For the record, here's the actual look-down function:

(require (prefix-in h: html)
 (prefix-in x: xml))

(define (look-down el action)
  (match el
 [(struct h:html-full (attributes content))
  (apply append (map action content))]

 [(struct h:html-element (attributes))
  (action el)]

 [ _ '()]))

-- 
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] Typed Racket: Is (- 1 1) equivalent to (- 2 2)?

2015-12-10 Thread Matthias Felleisen

You may want to read our papers on Units, Harper/Lillibridge and Leroy both 
from POPL ’94 and chase the citations forward. But perhaps Reynolds’s old 
saying “type structure is a syntactic discipline for enforcing levels of 
abstraction” suffices — Matthias (yes, I have studied all of this too and 
mostly by talking to the people themselves) 





> On Dec 10, 2015, at 5:52 PM, Hendrik Boom  wrote:
> 
> On Thu, Dec 10, 2015 at 08:25:11PM -0500, Matthias Felleisen wrote:
>> 
>> 
>>> On Dec 10, 2015, at 4:47 PM, Hendrik Boom  wrote:
>>> 
>>> On Thu, Dec 10, 2015 at 07:22:40PM -0500, Matthias Felleisen wrote:
 
 On Dec 10, 2015, at 3:04 PM, Klaus Ostermann  wrote:
 
> Thanks for the clarification, Sam. What you write makes sense.
> 
> However, since the default case (without explicit annotations) is that I 
> get these very (too?) precise singleton types, I have the impression that 
> reasoning about (typed) program equivalence is more difficult in TR than 
> in standard statically typed languages. 
> 
> Aren't types supposed to be a device for abstraction and for supporting 
> information hiding? Singleton types seem to be against that spirit by 
> exposing "implementation details" of the terms, such as the difference 
> between (- 1 1) and (- 2 2).
 
 
 I don't think gradual/incremental type systems play this role.
 But it is an open question how we can enrich such type systems with 
 types as abstraction barriers. -- Matthias
>>> 
>>> You don't use types as abstraction barriers.
>>> 
>>> You use modules aas abstraction barriers.
>>> And in your module system you specify explicitly how much  type 
>>> information is exported to be used to type-check the module user.
>>> 
>>> Modules are not types.  But they can contain type definitions.  You an 
>>> export the type definition, or just the type's presence.
>>> 
>>> -- hendrik
>>> 
>> 
>> 
>> Yes sir :-) 
> 
> ;-)
> 
> Maybe that's obvious to you, but there are a lot of people it's not obvious 
> to.
> And a lot of them have been designing programming languages.
> 
> -- 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] Typed Racket: Is (- 1 1) equivalent to (- 2 2)?

2015-12-10 Thread Hendrik Boom
On Thu, Dec 10, 2015 at 08:25:11PM -0500, Matthias Felleisen wrote:
> 
> 
> > On Dec 10, 2015, at 4:47 PM, Hendrik Boom  wrote:
> > 
> > On Thu, Dec 10, 2015 at 07:22:40PM -0500, Matthias Felleisen wrote:
> >> 
> >> On Dec 10, 2015, at 3:04 PM, Klaus Ostermann  wrote:
> >> 
> >>> Thanks for the clarification, Sam. What you write makes sense.
> >>> 
> >>> However, since the default case (without explicit annotations) is that I 
> >>> get these very (too?) precise singleton types, I have the impression that 
> >>> reasoning about (typed) program equivalence is more difficult in TR than 
> >>> in standard statically typed languages. 
> >>> 
> >>> Aren't types supposed to be a device for abstraction and for supporting 
> >>> information hiding? Singleton types seem to be against that spirit by 
> >>> exposing "implementation details" of the terms, such as the difference 
> >>> between (- 1 1) and (- 2 2).
> >> 
> >> 
> >> I don't think gradual/incremental type systems play this role.
> >> But it is an open question how we can enrich such type systems with 
> >> types as abstraction barriers. -- Matthias
> > 
> > You don't use types as abstraction barriers.
> > 
> > You use modules aas abstraction barriers.
> > And in your module system you specify explicitly how much  type 
> > information is exported to be used to type-check the module user.
> > 
> > Modules are not types.  But they can contain type definitions.  You an 
> > export the type definition, or just the type's presence.
> > 
> > -- hendrik
> > 
> 
> 
> Yes sir :-) 

;-)

Maybe that's obvious to you, but there are a lot of people it's not obvious to.
And a lot of them have been designing programming languages.

-- 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] Typed Racket: Is (- 1 1) equivalent to (- 2 2)?

2015-12-10 Thread Matthias Felleisen


> On Dec 10, 2015, at 4:47 PM, Hendrik Boom  wrote:
> 
> On Thu, Dec 10, 2015 at 07:22:40PM -0500, Matthias Felleisen wrote:
>> 
>> On Dec 10, 2015, at 3:04 PM, Klaus Ostermann  wrote:
>> 
>>> Thanks for the clarification, Sam. What you write makes sense.
>>> 
>>> However, since the default case (without explicit annotations) is that I 
>>> get these very (too?) precise singleton types, I have the impression that 
>>> reasoning about (typed) program equivalence is more difficult in TR than in 
>>> standard statically typed languages. 
>>> 
>>> Aren't types supposed to be a device for abstraction and for supporting 
>>> information hiding? Singleton types seem to be against that spirit by 
>>> exposing "implementation details" of the terms, such as the difference 
>>> between (- 1 1) and (- 2 2).
>> 
>> 
>> I don't think gradual/incremental type systems play this role.
>> But it is an open question how we can enrich such type systems with 
>> types as abstraction barriers. -- Matthias
> 
> You don't use types as abstraction barriers.
> 
> You use modules aas abstraction barriers.
> And in your module system you specify explicitly how much  type 
> information is exported to be used to type-check the module user.
> 
> Modules are not types.  But they can contain type definitions.  You an 
> export the type definition, or just the type's presence.
> 
> -- hendrik
> 


Yes sir :-) 


-- 
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] Typed Racket: Is (- 1 1) equivalent to (- 2 2)?

2015-12-10 Thread Hendrik Boom
On Thu, Dec 10, 2015 at 07:22:40PM -0500, Matthias Felleisen wrote:
> 
> On Dec 10, 2015, at 3:04 PM, Klaus Ostermann  wrote:
> 
> > Thanks for the clarification, Sam. What you write makes sense.
> > 
> > However, since the default case (without explicit annotations) is that I 
> > get these very (too?) precise singleton types, I have the impression that 
> > reasoning about (typed) program equivalence is more difficult in TR than in 
> > standard statically typed languages. 
> > 
> > Aren't types supposed to be a device for abstraction and for supporting 
> > information hiding? Singleton types seem to be against that spirit by 
> > exposing "implementation details" of the terms, such as the difference 
> > between (- 1 1) and (- 2 2).
> 
> 
> I don't think gradual/incremental type systems play this role.
> But it is an open question how we can enrich such type systems with 
> types as abstraction barriers. -- Matthias

You don't use types as abstraction barriers.

You use modules aas abstraction barriers.
And in your module system you specify explicitly how much  type 
information is exported to be used to type-check the module user.

Modules are not types.  But they can contain type definitions.  You an 
export the type definition, or just the type's presence.

-- 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] Typed Racket: Is (- 1 1) equivalent to (- 2 2)?

2015-12-10 Thread Hendrik Boom
On Thu, Dec 10, 2015 at 12:04:45PM -0800, Klaus Ostermann wrote:
> Thanks for the clarification, Sam. What you write makes sense.
> 
> However, since the default case (without explicit annotations) is 
> that I get these very (too?) precise singleton types, I have the 
> impression that reasoning about (typed) program equivalence is more 
> difficult in TR than in standard statically typed languages. 

As you go further in setting up more and more powerful type systems, you 
can eventually get to a system that can be used to rigorously prove 
program correctness.  However, when you go this far, type equivalence 
becomes an unsolvable problem.  To be practical, Racket had to walk the 
line between infeasiblity and expressiveness.

Different people can have very different ideas about where to draw this 
line.


> 
> Aren't types supposed to be a device for abstraction and for 
> supporting information hiding?

Types and abstraction are orthogonal concepts, which have too often been 
conflated.  Granted, being orthogonal, they work well together.

Abstraction is the mechanism for information hiding.


-- 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] Typed Racket: Is (- 1 1) equivalent to (- 2 2)?

2015-12-10 Thread Matthias Felleisen

On Dec 10, 2015, at 3:04 PM, Klaus Ostermann  wrote:

> Thanks for the clarification, Sam. What you write makes sense.
> 
> However, since the default case (without explicit annotations) is that I get 
> these very (too?) precise singleton types, I have the impression that 
> reasoning about (typed) program equivalence is more difficult in TR than in 
> standard statically typed languages. 
> 
> Aren't types supposed to be a device for abstraction and for supporting 
> information hiding? Singleton types seem to be against that spirit by 
> exposing "implementation details" of the terms, such as the difference 
> between (- 1 1) and (- 2 2).


I don't think gradual/incremental type systems play this role. But it is an 
open question how we can enrich such type systems with types as abstraction 
barriers. -- Matthias

-- 
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] [Racket] Bug with Abstraction Teachpack, posn and BSL with List Abbreviations

2015-12-10 Thread Matthias Felleisen

Never mind! Write this off to my forgetful old age. This one is supposed to 
work for BSL and BSL+. I had forgotten that I fixed this. 

(There are other parts of 2htdp/abstraction that work only when functions are 
available as values.) 




On Dec 10, 2015, at 5:56 PM, Matthias Felleisen  wrote:

> 
> On Dec 10, 2015, at 1:15 PM, Jonathan Brachthäuser  
> wrote:
> 
>> In DrRacket 6.2.1 when using the `match` construct as defined in the 
>> abstraction teachpack together with posn a strange problem appears.
>> 
>> When choosing BSL as language the following code just works as expected:
>> 
>> ```
>> (require 2htdp/abstraction)
>> (match (make-posn 1 2) [(posn x y) (+ x y)])
>> ```
>> 
>> yields `3`.
>> 
>> However when choosing "BSL with list abbreviation" the above code gives:
>> 
>> ```
>> ... (posn x y) ...
>> function call: expected a function after the open parenthesis, but found a 
>> part
>> ```
>> 
>> We can work around the error by using `my-posn` instead (defined below)
>> 
>> ```
>> (define-struct my-posn (x y))
>> ```
>> 
>> Is there any explanation why this happens? Is the abstraction teachpack not 
>> designed to work with "BSL with list abbrv" ?
> 
> 
> No, 2htdp/abstraction is designed to work with ISL and ISL+. The above 
> problem is precisely why it doesn't work in BSL and BSL+. (There is a second 
> problem, which escapes me right now.) 
> 
> -- 
> 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.


Re: [racket-users] [Racket] Bug with Abstraction Teachpack, posn and BSL with List Abbreviations

2015-12-10 Thread Matthias Felleisen

On Dec 10, 2015, at 1:15 PM, Jonathan Brachthäuser  
wrote:

> In DrRacket 6.2.1 when using the `match` construct as defined in the 
> abstraction teachpack together with posn a strange problem appears.
> 
> When choosing BSL as language the following code just works as expected:
> 
> ```
> (require 2htdp/abstraction)
> (match (make-posn 1 2) [(posn x y) (+ x y)])
> ```
> 
> yields `3`.
> 
> However when choosing "BSL with list abbreviation" the above code gives:
> 
> ```
> ... (posn x y) ...
> function call: expected a function after the open parenthesis, but found a 
> part
> ```
> 
> We can work around the error by using `my-posn` instead (defined below)
> 
> ```
> (define-struct my-posn (x y))
> ```
> 
> Is there any explanation why this happens? Is the abstraction teachpack not 
> designed to work with "BSL with list abbrv" ?


No, 2htdp/abstraction is designed to work with ISL and ISL+. The above problem 
is precisely why it doesn't work in BSL and BSL+. (There is a second problem, 
which escapes me right now.) 

-- 
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] Re: [Racket] Bug with Abstraction Teachpack, posn and BSL with List Abbreviations

2015-12-10 Thread Jonathan Brachthäuser
That was quick. Thanks a lot Paolo and Vincent!

Jonathan

> On 10 Dec 2015, at 22:11, Vincent St-Amour  
> wrote:
> 
> I just merged Paolo's fix. The fix should be in the next release.
> 
> If you want to try it before that, you can either try building from
> source, or using a nightly build tomorrow: pre.racket-lang.org
> 
> Vincent
> 
> 
> 
> On Thu, 10 Dec 2015 12:44:39 -0600,
> Paolo Giarrusso wrote:
>> 
>> On Thursday, December 10, 2015 at 7:15:07 PM UTC+1, Jonathan Brachthäuser 
>> wrote:
>>> In DrRacket 6.2.1 when using the `match` construct as defined in the 
>>> abstraction teachpack together with posn a strange problem appears.
>>> 
>>> When choosing BSL as language the following code just works as expected:
>>> 
>>> ```
>>> (require 2htdp/abstraction)
>>> (match (make-posn 1 2) [(posn x y) (+ x y)])
>>> ```
>>> 
>>> yields `3`.
>>> 
>>> However when choosing "BSL with list abbreviation" the above code gives:
>>> 
>>> ```
>>> ... (posn x y) ...
>>> function call: expected a function after the open parenthesis, but found a 
>>> part
>>> ```
>>> 
>>> We can work around the error by using `my-posn` instead (defined below)
>>> 
>>> ```
>>> (define-struct my-posn (x y))
>>> ```
>>> 
>>> Is there any explanation why this happens? Is the abstraction teachpack not 
>>> designed to work with "BSL with list abbrv" ?
>> 
>> The issue is a missing export in BSL+.
>> 
>> Last time this came up, I submitted a pull request which is still open, so I 
>> suspect this isn't fixed yet: https://github.com/racket/htdp/pull/16. 
>> Apparently I only made a pull request and didn't open a thread on this ML, 
>> which might be part of the problem.
>> 
>> -- 
>> 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.


Re: [racket-users] Re: [Racket] Bug with Abstraction Teachpack, posn and BSL with List Abbreviations

2015-12-10 Thread Vincent St-Amour
I just merged Paolo's fix. The fix should be in the next release.

If you want to try it before that, you can either try building from
source, or using a nightly build tomorrow: pre.racket-lang.org

Vincent



On Thu, 10 Dec 2015 12:44:39 -0600,
Paolo Giarrusso wrote:
> 
> On Thursday, December 10, 2015 at 7:15:07 PM UTC+1, Jonathan Brachthäuser 
> wrote:
> > In DrRacket 6.2.1 when using the `match` construct as defined in the 
> > abstraction teachpack together with posn a strange problem appears.
> > 
> > When choosing BSL as language the following code just works as expected:
> > 
> > ```
> > (require 2htdp/abstraction)
> > (match (make-posn 1 2) [(posn x y) (+ x y)])
> > ```
> > 
> > yields `3`.
> > 
> > However when choosing "BSL with list abbreviation" the above code gives:
> > 
> > ```
> > ... (posn x y) ...
> > function call: expected a function after the open parenthesis, but found a 
> > part
> > ```
> > 
> > We can work around the error by using `my-posn` instead (defined below)
> > 
> > ```
> > (define-struct my-posn (x y))
> > ```
> > 
> > Is there any explanation why this happens? Is the abstraction teachpack not 
> > designed to work with "BSL with list abbrv" ?
> 
> The issue is a missing export in BSL+.
> 
> Last time this came up, I submitted a pull request which is still open, so I 
> suspect this isn't fixed yet: https://github.com/racket/htdp/pull/16. 
> Apparently I only made a pull request and didn't open a thread on this ML, 
> which might be part of the problem.
> 
> -- 
> 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.


Re: [racket-users] Re: Typed Racket: Is (- 1 1) equivalent to (- 2 2)?

2015-12-10 Thread Asumu Takikawa
On 2015-12-10 14:02:55 -0600, Vincent St-Amour wrote:
> My dream is that, instead, the Racket compiler could make its own
> analyses and transformations available as hooks, just as it makes other
> kinds of hooks available. :) Think of it as a "cp0 [1] as a library",
> that #langs and language extensions could reuse.
> 
> [1] After Chez's first compilation pass, which does the usual
> simplification / cleanup optimizations.

BTW, if anyone is interesting in reading more about CP0 you can take a look at
Oscar Waddell's thesis:

  
http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.71.363&rep=rep1&type=pdf

(Chapter 4 describes CP0. The thesis version is nice because it uses Scheme code
 whereas the SAS97 paper uses math.)

Cheers,
Asumu

-- 
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] Re: Typed Racket: Is (- 1 1) equivalent to (- 2 2)?

2015-12-10 Thread Paolo Giarrusso
On Thursday, December 10, 2015 at 9:11:00 PM UTC+1, Vincent St-Amour wrote:
> Right. That's why we've built tools to get information about these types
> more digestible:
> 
> http://docs.racket-lang.org/ts-reference/Exploring_Types.html

Thanks, I'd seen those but forgot the non-verbose option.

> You may be interested in:
> 
> 
> http://andmkent.com/blog/2015/11/22/new-draft-paper-occurrence-typing-modulo-theories/

Thanks, I had forgot SMT altogether. What's good about Presburger arithmetic is 
that it's predictable — it doesn't get multiplication. But that's indeed very 
restrictive.
I've bookmarked that paper and already skimmed the PADL one.

Cheers,
Paolo

-- 
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] Re: Typed Racket: Is (- 1 1) equivalent to (- 2 2)?

2015-12-10 Thread Vincent St-Amour
On Thu, 10 Dec 2015 13:10:04 -0600,
Paolo Giarrusso wrote:
> 
> On Thursday, December 10, 2015 at 6:55:28 PM UTC+1, johnbclements wrote:
> > > On Dec 10, 2015, at 9:50 AM, George Neuner  wrote:
> > > 
> > > On Thu, 10 Dec 2015 12:35:34 -0500, Alex Knauth wrote:
> > > 
> > >> In typed racket (- 1 1) and (- 2 2) are equal at runtime, but the type
> > >> checker doesn't necessarily know that at compile time. It knows that
> > >> (- 1 1) is zero because that's a special case in the type system. But it
> > >> doesn't have a special case for (- 2 2), so it only knows that that's a
> > >> Fixnum. 
> > > 
> > > But in this case the type checker isn't dealing with variables.  Which
> > > begs the question why is (- 1 1) special cased?  Shouldn't there be a
> > > general rule: (- C C) where C is a numeric constant?
> 
> Or conversely, why was the special case added? Maybe there's an
> interesting reason, but this seems _very_ ad-hoc. And this thread IMHO
> shows why some dislike "ad-hoc" solutions: they solve some problem
> magically, but it's rather hard to know when you can rely on them.

I don't remember, off the top of my head, why we added that particular
special case to the type of `-`.

In general, though, those kinds of more precise clauses inside the types
of numeric operations are there to enable closure properties. If you
know that you're operating on, e.g., non-negative floats, then you may
be able to rule out complex-number results in parts of your code.

> Somebody might object that you just need to look at the definition of
> `Number` and at the type of `-`. I think they'd be making my point for
> me. Especially if you care for types for their documentation value.

Right. That's why we've built tools to get information about these types
more digestible:

http://docs.racket-lang.org/ts-reference/Exploring_Types.html

> > The natural extension to all numbers (each number has its own type)
> > leads (IIUC) to a totally intractable type system.
> 
> You're right in the end, but for a subtler reason. Singleton types
> aren't a problem per se ― but expecting (- C C) to have type Zero with
> the current approach, on the other hand, would add to the signature of
> - an entry per number.
> 
> OTOH, there are decision procedures for Presburger arithmetic and
> they've been used in experimental programming languages in the past
> for bound checking; I'm not familiar enough with them to say whether
> using them would be too crazy or just as crazy as a good research
> project.

You may be interested in:


http://andmkent.com/blog/2015/11/22/new-draft-paper-occurrence-typing-modulo-theories/

Vincent

-- 
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] Crash when installing 'boris' package from GitHub URL on OSX 10.6.8

2015-12-10 Thread David K. Storrs
I have to say, the fact that installing a package === using a package is really 
cool.  Go Racket!

-- 
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] Typed Racket: Is (- 1 1) equivalent to (- 2 2)?

2015-12-10 Thread Klaus Ostermann
Thanks for the clarification, Sam. What you write makes sense.

However, since the default case (without explicit annotations) is that I get 
these very (too?) precise singleton types, I have the impression that reasoning 
about (typed) program equivalence is more difficult in TR than in standard 
statically typed languages. 

Aren't types supposed to be a device for abstraction and for supporting 
information hiding? Singleton types seem to be against that spirit by exposing 
"implementation details" of the terms, such as the difference between (- 1 1) 
and (- 2 2).

-- 
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] Re: Typed Racket: Is (- 1 1) equivalent to (- 2 2)?

2015-12-10 Thread Vincent St-Amour
On Thu, 10 Dec 2015 13:18:57 -0600,
Gustavo Massaccesi wrote:
> 
> IIRC, the only numeric type that are singletons are Zero and One, so
> this also typechecks:
> 
> (+ 1 (if (= 0 (- 0 0)) 1 "x"))

There's a few more, actually, like the various floating-point zeroes.

> On a related note, the (untyped)Racket optimizer has constant folding,
> so in (untyped)Racket all these expressions are compiled to 2. I don't
> know if it's possible to add constant folding to Typed Racket.

It would be possible to add constant folding, and other optimizations to
TR. That would essentially involve redoing the same analyses and
transformations that the Racket compiler already does, though, which
would lead to (conceptual) duplication. Instead, TR's MO is to use type
info to arrange code to make the Racket compiler's job easier (e.g.,
make type-dead code obviously dead, so the Racket compiler can DCE it).

My dream is that, instead, the Racket compiler could make its own
analyses and transformations available as hooks, just as it makes other
kinds of hooks available. :) Think of it as a "cp0 [1] as a library",
that #langs and language extensions could reuse.

Vincent


[1] After Chez's first compilation pass, which does the usual
simplification / cleanup optimizations.

> 
> Anyway, other obvious expressions like
> (lambda (x) (+ 1 (if (eq? x x) 1 "x")))
> are not reduced (currently).
> 
> Gustavo
> 
> 
> On Thu, Dec 10, 2015 at 3:12 PM, Vincent St-Amour
>  wrote:
> > Right.
> >
> > The key distinction here is that TR is not so much reasoning about
> > constants, but about a singleton type. So TR is still working in terms
> > of types, not in terms of concrete values.
> >
> > Vincent
> >
> >
> >
> > On Thu, 10 Dec 2015 11:55:24 -0600,
> > 'John Clements' via Racket Users wrote:
> >>
> >>
> >> > On Dec 10, 2015, at 9:50 AM, George Neuner  wrote:
> >> >
> >> > On Thu, 10 Dec 2015 12:35:34 -0500, Alex Knauth
> >> >  wrote:
> >> >
> >> >> In typed racket (- 1 1) and (- 2 2) are equal at runtime, but the type
> >> >> checker doesn't necessarily know that at compile time. It knows that
> >> >> (- 1 1) is zero because that's a special case in the type system. But it
> >> >> doesn't have a special case for (- 2 2), so it only knows that that's a
> >> >> Fixnum.
> >> >
> >> > But in this case the type checker isn't dealing with variables.  Which
> >> > begs the question why is (- 1 1) special cased?  Shouldn't there be a
> >> > general rule: (- C C) where C is a numeric constant?
> >> > [Ok, I know equality is a problem with floating point ... but, still,
> >> > the principle remains.]
> >>
> >> Check out the numeric tower in TR: there’s a type that includes just the 
> >> number 1. The natural extension to all numbers (each number has its own 
> >> type) leads (IIUC) to a totally intractable type system.
> >>
> >> John
> >>
> >> >
> >> > George
> >> >
> >> > --
> >> > 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.
> >
> > --
> > 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.


Re: [racket-users] Typed Racket: Is (- 1 1) equivalent to (- 2 2)?

2015-12-10 Thread Paolo Giarrusso

On Thursday, December 10, 2015 at 8:26:02 PM UTC+1, Klaus Ostermann wrote:
> > I don't think any typed language respects this. For example:
> > 
> >(if (= 1 1) #f "not a boolean")
> > 
> > is equal to #f, but many type systems do not let you replace #f with
> > that expression. 
> 
> But in statically typed languages you usually have a typed equivalence 
> relation like
> 
> \Gamma |- t1 == t2 : T
> 
> Your example would not be well-typed in standard statically typed languages, 
> hence one would not reason that it is equal to #f.
> 
> So I think my argument that usually you can replace "equals by equals" 
> according to the typed equivalence relation holds.
> 
> Presumably the property still holds in Typed Racket, but with regard to a 
> much smaller equality relation in which many equations that one would 
> intuitively expect to be true are not true.

> > In general, if you define "equals" in "replacing equals for equals" by
> > reference to underlying observable equivalence relation induced by an
> > untyped semantics, then you certainly cannot have this design
> > principle.
> 
> I agree that that's not true, but usually I would expect a statically typed 
> language to have a typed equivalence relation |- t1 == t2 : T such that if E 
> is an evaluation context, then E[t1] is welltyped iff E[t2] is welltyped.
> 
> I think you can also define that equivalence relation for Typed Racket, but 
> it would be rather small. 

I guess that typed equivalence is in fact bigger; what's different is a 
different relation. (Please prepend "I guess" to _all_ my claims in this email).

1. I think the results you're quoting (especially the second) are corollaries 
of the substitution lemma; to show that, get E[t1] and E[T2] through 
substitution from E[x], where x is fresh with type T. While Typed Racket is not 
standard, I'm going to assume it has a traditional substitution lemma.

2. Typed Racket has subtyping, so `|- (- 1 1) = (- 2 2) : Number` holds, as it 
would in a usual language. But we can't substitute a Number in the context of 
the original example:

E[x] = (+ 1 (if (= 0 x) 1 "x"))

There we need an instance of Zero, and `|- (- 1 1) = (- 2 2) : Zero` indeed 
fails.

The equivalence which holds usually but not in TR is another one.

Let's define relation R as `e_1 R e_2` iff expressions e_1 and e_2 receive the 
same strongest type (before evaluation) and evaluate to the same value. This 
relation isn't part of the usual presentation of typical type systems, unlike 
typed equivalence; I'm thinking of both Martin-Löf type theory and Barendregt's 
Pure Type Systems (and unlike the rest of this mail, I'm rather confident of 
this). To be fair, typed equivalence is often only introduced for type systems 
with a conversion rule (like dependent ones).

Then (- 1 1) R (- 2 2) holds in most languages and fails in Typed Racket, 
because TR refines the type of (- 1 1) but not the type of (- 2 2).

Cheers,
Paolo

-- 
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] Typed Racket: Is (- 1 1) equivalent to (- 2 2)?

2015-12-10 Thread Sam Tobin-Hochstadt
On Thu, Dec 10, 2015 at 2:26 PM Klaus Ostermann  wrote:

> > I don't think any typed language respects this. For example:
> >
> >(if (= 1 1) #f "not a boolean")
> >
> > is equal to #f, but many type systems do not let you replace #f with
> > that expression.
>
> But in statically typed languages you usually have a typed equivalence
> relation like
>
> \Gamma |- t1 == t2 : T
>
> Your example would not be well-typed in standard statically typed
> languages, hence one would not reason that it is equal to #f.
>
> So I think my argument that usually you can replace "equals by equals"
> according to the typed equivalence relation holds.
>
> Presumably the property still holds in Typed Racket, but with regard to a
> much smaller equality relation in which many equations that one would
> intuitively expect to be true are not true.
>
> > In general, if you define "equals" in "replacing equals for equals" by
> > reference to underlying observable equivalence relation induced by an
> > untyped semantics, then you certainly cannot have this design
> > principle.
>
> I agree that that's not true, but usually I would expect a statically
> typed language to have a typed equivalence relation |- t1 == t2 : T such
> that if E is an evaluation context, then E[t1] is welltyped iff E[t2] is
> welltyped.
>
> I think you can also define that equivalence relation for Typed Racket,
> but it would be rather small.
>

I don't think that's right.  If we consider the equivalence relation you
refer to at `Number`, then it's exactly as large as you expect. However,
neither of the expressions in your first message are well-typed if we treat
`t1` and `t2` as having the type `Number`. You can try this by annotating
them with that type.

What is happening here is that there are some terms from which Typed Racket
derives the type `#false`, and others with type `0`, which _enlarges_ the
set of typable terms to include programs like the ones you began with. Of
course, the equivalence relation at `0` is smaller than at `Number`,
leading to the result you see. As Robby pointed out, neither the set of
terms with type Number, nor the set of terms with type `0`, nor the set of
terms known to evaluate to #false, is closed under evaluation.

As for the rationale for the current design of the numeric types in Typed
Racket, you might be interested in our PADL 2012 paper, here:
http://www.ccs.neu.edu/racket/pubs/padl12-stff.pdf

-- 
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] Typed Racket: Is (- 1 1) equivalent to (- 2 2)?

2015-12-10 Thread Klaus Ostermann
> I don't think any typed language respects this. For example:
> 
>(if (= 1 1) #f "not a boolean")
> 
> is equal to #f, but many type systems do not let you replace #f with
> that expression. 

But in statically typed languages you usually have a typed equivalence relation 
like

\Gamma |- t1 == t2 : T

Your example would not be well-typed in standard statically typed languages, 
hence one would not reason that it is equal to #f.

So I think my argument that usually you can replace "equals by equals" 
according to the typed equivalence relation holds.

Presumably the property still holds in Typed Racket, but with regard to a much 
smaller equality relation in which many equations that one would intuitively 
expect to be true are not true.
 
> In general, if you define "equals" in "replacing equals for equals" by
> reference to underlying observable equivalence relation induced by an
> untyped semantics, then you certainly cannot have this design
> principle.

I agree that that's not true, but usually I would expect a statically typed 
language to have a typed equivalence relation |- t1 == t2 : T such that if E is 
an evaluation context, then E[t1] is welltyped iff E[t2] is welltyped.

I think you can also define that equivalence relation for Typed Racket, but it 
would be rather small. 

So there is a price to be paid for the fancy (singleton and other) types in 
TypedRacket - which is fine if I get something else in return, but it is not 
clear to me right now what it is that is worth this price.

-- 
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] Re: Typed Racket: Is (- 1 1) equivalent to (- 2 2)?

2015-12-10 Thread Gustavo Massaccesi
IIRC, the only numeric type that are singletons are Zero and One, so
this also typechecks:

(+ 1 (if (= 0 (- 0 0)) 1 "x"))

On a related note, the (untyped)Racket optimizer has constant folding,
so in (untyped)Racket all these expressions are compiled to 2. I don't
know if it's possible to add constant folding to Typed Racket.

Anyway, other obvious expressions like
(lambda (x) (+ 1 (if (eq? x x) 1 "x")))
are not reduced (currently).

Gustavo


On Thu, Dec 10, 2015 at 3:12 PM, Vincent St-Amour
 wrote:
> Right.
>
> The key distinction here is that TR is not so much reasoning about
> constants, but about a singleton type. So TR is still working in terms
> of types, not in terms of concrete values.
>
> Vincent
>
>
>
> On Thu, 10 Dec 2015 11:55:24 -0600,
> 'John Clements' via Racket Users wrote:
>>
>>
>> > On Dec 10, 2015, at 9:50 AM, George Neuner  wrote:
>> >
>> > On Thu, 10 Dec 2015 12:35:34 -0500, Alex Knauth
>> >  wrote:
>> >
>> >> In typed racket (- 1 1) and (- 2 2) are equal at runtime, but the type
>> >> checker doesn't necessarily know that at compile time. It knows that
>> >> (- 1 1) is zero because that's a special case in the type system. But it
>> >> doesn't have a special case for (- 2 2), so it only knows that that's a
>> >> Fixnum.
>> >
>> > But in this case the type checker isn't dealing with variables.  Which
>> > begs the question why is (- 1 1) special cased?  Shouldn't there be a
>> > general rule: (- C C) where C is a numeric constant?
>> > [Ok, I know equality is a problem with floating point ... but, still,
>> > the principle remains.]
>>
>> Check out the numeric tower in TR: there’s a type that includes just the 
>> number 1. The natural extension to all numbers (each number has its own 
>> type) leads (IIUC) to a totally intractable type system.
>>
>> John
>>
>> >
>> > George
>> >
>> > --
>> > 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.
>
> --
> 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.


Re: [racket-users] Re: Typed Racket: Is (- 1 1) equivalent to (- 2 2)?

2015-12-10 Thread Paolo Giarrusso
On Thursday, December 10, 2015 at 6:55:28 PM UTC+1, johnbclements wrote:
> > On Dec 10, 2015, at 9:50 AM, George Neuner  wrote:
> > 
> > On Thu, 10 Dec 2015 12:35:34 -0500, Alex Knauth wrote:
> > 
> >> In typed racket (- 1 1) and (- 2 2) are equal at runtime, but the type
> >> checker doesn't necessarily know that at compile time. It knows that
> >> (- 1 1) is zero because that's a special case in the type system. But it
> >> doesn't have a special case for (- 2 2), so it only knows that that's a
> >> Fixnum. 
> > 
> > But in this case the type checker isn't dealing with variables.  Which
> > begs the question why is (- 1 1) special cased?  Shouldn't there be a
> > general rule: (- C C) where C is a numeric constant?

Or conversely, why was the special case added? Maybe there's an interesting 
reason, but this seems _very_ ad-hoc. And this thread IMHO shows why some 
dislike "ad-hoc" solutions: they solve some problem magically, but it's rather 
hard to know when you can rely on them.

Somebody might object that you just need to look at the definition of `Number` 
and at the type of `-`. I think they'd be making my point for me. Especially if 
you care for types for their documentation value.

But I appreciate some of this is inevitable for occurrence typing — if you go 
for regularity, you end up with the typing rules of type theory, which aren't 
adequate.

> The natural extension to all numbers (each number has its own type) leads 
> (IIUC) to a totally intractable type system.

You're right in the end, but for a subtler reason. Singleton types aren't a 
problem per se — but expecting (- C C) to have type Zero with the current 
approach, on the other hand, would add to the signature of - an entry per 
number.

OTOH, there are decision procedures for Presburger arithmetic and they've been 
used in experimental programming languages in the past for bound checking; I'm 
not familiar enough with them to say whether using them would be too crazy or 
just as crazy as a good research project.

Static analysis researchers have used much fancier stuff, but that's even less 
predictable.

Cheers,
Paolo

-- 
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] Crash when installing 'boris' package from GitHub URL on OSX 10.6.8

2015-12-10 Thread Neil Van Dyke



'John Clements' via Racket Users wrote on 12/10/2015 01:04 PM:

However, it could easily be the case that a package (presumably from Neil Van 
Dyke) could contain code that would be installed into the html subdirectory of 
the sxml collection, and I’m guessing that’s what you’re referring to.


Though that's technically possible, I'd strongly prefer that that not 
happen in practice for third-party packages, and at least it's not 
something that I'd likely ever do with my packages.


For decentralized third-party reusable component development, taxonomies 
generally do not get coded in package names themselves. It's much less 
flexible, and easier to mess up in a counterproductive way (even when 
centralized, but especially when decentralized).


And it would be simpler (and also facilitate multiple-version support 
someday), if packages just kept their files compartmentalized to their 
own installation directory.  So I'd discourage third-party package 
developers using the power of the new package system to sprinkle their 
package's files in arbitrary other locations, except when one has a 
really-really good reason.



It appears to me that, for instance, Neil’s html-parsing library is not 
currently available in package form. (ObResearch: quick search for 'neil@ne' 
through pkgs.)


Correct, my `html-parsing` package is still maintained in PLaneT, and I 
have not yet moved it to the new package system.  I do intend to move my 
packages to the new package system, but I've put nothing in the new 
package system catalog yet.


Neil V.

--
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] Re: [Racket] Bug with Abstraction Teachpack, posn and BSL with List Abbreviations

2015-12-10 Thread Paolo Giarrusso
On Thursday, December 10, 2015 at 7:15:07 PM UTC+1, Jonathan Brachthäuser wrote:
> In DrRacket 6.2.1 when using the `match` construct as defined in the 
> abstraction teachpack together with posn a strange problem appears.
> 
> When choosing BSL as language the following code just works as expected:
> 
> ```
> (require 2htdp/abstraction)
> (match (make-posn 1 2) [(posn x y) (+ x y)])
> ```
> 
> yields `3`.
> 
> However when choosing "BSL with list abbreviation" the above code gives:
> 
> ```
> ... (posn x y) ...
> function call: expected a function after the open parenthesis, but found a 
> part
> ```
> 
> We can work around the error by using `my-posn` instead (defined below)
> 
> ```
> (define-struct my-posn (x y))
> ```
> 
> Is there any explanation why this happens? Is the abstraction teachpack not 
> designed to work with "BSL with list abbrv" ?

The issue is a missing export in BSL+.

Last time this came up, I submitted a pull request which is still open, so I 
suspect this isn't fixed yet: https://github.com/racket/htdp/pull/16. 
Apparently I only made a pull request and didn't open a thread on this ML, 
which might be part of the problem.

-- 
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] [Racket] Bug with Abstraction Teachpack, posn and BSL with List Abbreviations

2015-12-10 Thread Jonathan Brachthäuser
In DrRacket 6.2.1 when using the `match` construct as defined in the 
abstraction teachpack together with posn a strange problem appears.

When choosing BSL as language the following code just works as expected:

```
(require 2htdp/abstraction)
(match (make-posn 1 2) [(posn x y) (+ x y)])
```

yields `3`.

However when choosing "BSL with list abbreviation" the above code gives:

```
... (posn x y) ...
function call: expected a function after the open parenthesis, but found a part
```

We can work around the error by using `my-posn` instead (defined below)

```
(define-struct my-posn (x y))
```

Is there any explanation why this happens? Is the abstraction teachpack not 
designed to work with "BSL with list abbrv" ?

-- 
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] Re: Typed Racket: Is (- 1 1) equivalent to (- 2 2)?

2015-12-10 Thread Vincent St-Amour
Right.

The key distinction here is that TR is not so much reasoning about
constants, but about a singleton type. So TR is still working in terms
of types, not in terms of concrete values.

Vincent



On Thu, 10 Dec 2015 11:55:24 -0600,
'John Clements' via Racket Users wrote:
> 
> 
> > On Dec 10, 2015, at 9:50 AM, George Neuner  wrote:
> > 
> > On Thu, 10 Dec 2015 12:35:34 -0500, Alex Knauth
> >  wrote:
> > 
> >> In typed racket (- 1 1) and (- 2 2) are equal at runtime, but the type
> >> checker doesn't necessarily know that at compile time. It knows that
> >> (- 1 1) is zero because that's a special case in the type system. But it
> >> doesn't have a special case for (- 2 2), so it only knows that that's a
> >> Fixnum. 
> > 
> > But in this case the type checker isn't dealing with variables.  Which
> > begs the question why is (- 1 1) special cased?  Shouldn't there be a
> > general rule: (- C C) where C is a numeric constant?
> > [Ok, I know equality is a problem with floating point ... but, still,
> > the principle remains.]
> 
> Check out the numeric tower in TR: there’s a type that includes just the 
> number 1. The natural extension to all numbers (each number has its own type) 
> leads (IIUC) to a totally intractable type system.
> 
> John
> 
> > 
> > George
> > 
> > -- 
> > 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.

-- 
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] Typed Racket: Is (- 1 1) equivalent to (- 2 2)?

2015-12-10 Thread Robby Findler
On Thu, Dec 10, 2015 at 11:26 AM, Klaus Ostermann  wrote:
> This looks a bit strange to me, because usually one would expect 
> well-typedness to be not destroyed by replacing "equals with equals".

I don't think any typed language respects this. For example:

   (if (= 1 1) #f "not a boolean")

is equal to #f, but many type systems do not let you replace #f with
that expression. ML for example. Also, in ocaml, this expression:

let f = fun x -> x in ((f f) 1)

aka this expression:

(let ([f (λ (x) x)])
  ((f f) 1))

type checks, but this one:

(fun f -> ((f f) 1)) (fun x -> x)

aka this one:

((λ (f)
   ((f f) 1))
 (λ (x) x))

does not type check, even tho these are equal to each other.

In general, if you define "equals" in "replacing equals for equals" by
reference to underlying observable equivalence relation induced by an
untyped semantics, then you certainly cannot have this design
principle.

Robby

-- 
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] Crash when installing 'boris' package from GitHub URL on OSX 10.6.8

2015-12-10 Thread 'John Clements' via Racket Users

> On Dec 9, 2015, at 10:59 PM, David K. Storrs  wrote:
> 
> On Wednesday, December 9, 2015 at 6:33:02 PM UTC-8, Neil Van Dyke wrote:
>> David K. Storrs wrote on 12/09/2015 08:50 PM:
>>> 1) Is there a web-spidering package that people recommend?  I could use 
>>> wget and then parse things from disk, but I'd like to have something that's 
>>> easily composable into CLI scripts.
>> 
>> 
>> I've done a lot of Web crawling and scraping successfully with Racket 
>> and Scheme, over the last 14-15 years.  I released an HTML parser 
>> ("http://www.neilvandyke.org/racket-html-parsing/";), which I still use 
>> today.  From that parse, you might then extract the info you need with 
>> `sxml-match` 
>> ("http://planet.racket-lang.org/display.ss?package=sxml-match.plt&owner=jim";)
>>  
>> and/or SXPath.  
> 
> Thank you; I've been rolling through the docs and playing around on thse, and 
> they seem really useful.  One question though -- I stumbled across a mention 
> of the sxml/html module while I was reading, but had no luck installing it.  
> None of the following worked:
> 
> (require sxml/html)
> $ raco pkg install sxml/html
> $ raco pkg install 'sxml/html'  # Maybe the shell was having trouble with '/'?
> 
> I don't know that I need it, but I'd like to know how to deal with modules 
> like this in future.

I don’t believe that package names should contain slashes. 

However, it could easily be the case that a package (presumably from Neil Van 
Dyke) could contain code that would be installed into the html subdirectory of 
the sxml collection, and I’m guessing that’s what you’re referring to.

It’s perhaps also worth mentioning that Racket has an older package system 
(PLaneT), and a newer one (packages), and there’s a certain amount of confusion 
that may result from that transition. When you write ‘raco pkg install …”, 
you’re referring to the new system. It appears to me that, for instance, Neil’s 
html-parsing library is not currently available in package form. (ObResearch: 
quick search for 'neil@ne' through pkgs.)

John Clements



-- 
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] Re: Typed Racket: Is (- 1 1) equivalent to (- 2 2)?

2015-12-10 Thread 'John Clements' via Racket Users

> On Dec 10, 2015, at 9:50 AM, George Neuner  wrote:
> 
> On Thu, 10 Dec 2015 12:35:34 -0500, Alex Knauth
>  wrote:
> 
>> In typed racket (- 1 1) and (- 2 2) are equal at runtime, but the type
>> checker doesn't necessarily know that at compile time. It knows that
>> (- 1 1) is zero because that's a special case in the type system. But it
>> doesn't have a special case for (- 2 2), so it only knows that that's a
>> Fixnum. 
> 
> But in this case the type checker isn't dealing with variables.  Which
> begs the question why is (- 1 1) special cased?  Shouldn't there be a
> general rule: (- C C) where C is a numeric constant?
> [Ok, I know equality is a problem with floating point ... but, still,
> the principle remains.]

Check out the numeric tower in TR: there’s a type that includes just the number 
1. The natural extension to all numbers (each number has its own type) leads 
(IIUC) to a totally intractable type system.

John

> 
> George
> 
> -- 
> 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] Re: Typed Racket: Is (- 1 1) equivalent to (- 2 2)?

2015-12-10 Thread George Neuner
On Thu, 10 Dec 2015 12:35:34 -0500, Alex Knauth
 wrote:

>In typed racket (- 1 1) and (- 2 2) are equal at runtime, but the type
>checker doesn't necessarily know that at compile time. It knows that
>(- 1 1) is zero because that's a special case in the type system. But it
>doesn't have a special case for (- 2 2), so it only knows that that's a
>Fixnum. 

But in this case the type checker isn't dealing with variables.  Which
begs the question why is (- 1 1) special cased?  Shouldn't there be a
general rule: (- C C) where C is a numeric constant?
[Ok, I know equality is a problem with floating point ... but, still,
the principle remains.]

George

-- 
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] Typed Racket: Is (- 1 1) equivalent to (- 2 2)?

2015-12-10 Thread 'John Clements' via Racket Users

> On Dec 10, 2015, at 9:26 AM, Klaus Ostermann  wrote:
> 
> This Typed Racket term is well-typed:
> 
> (+ 1 (if (= 0 (- 1 1)) 1 "x"))
> 
> This one isn't:
> 
> (+ 1 (if (= 0 (- 2 2)) 1 "x"))
> 
> This looks a bit strange to me, because usually one would expect 
> well-typedness to be not destroyed by replacing "equals with equals”.

I think that your quotation marks here are well-placed; specifically, this is 
the crux of the argument: what’s “equal” in the eyes of the type checker? Put 
differently, what kinds of equality does the type checker encompass? In fact, 
there are *very few* type checkers that can reason about the fact that (- 1 1) 
is equal to zero; I’m confident that the type checkers associated with the 20 
most popular languages today would simply discard this expression out of hand.

However, you do point out a very important point about type checkers in 
general: it can be very important that *programmers* understand the system of 
logic associated with a type checker, because when a program fails to type 
check, a programmer must rewrite the program so that the type checker accepts 
it. If the type system is too complex—or “clever”—for the programmer to 
understand, she may be unable to replace the program with an equivalent one 
that the type checker approves of.


John Clements

> 
> I'd like to know the rationale for this design. It would be nice if one of 
> the designers could comment on this.
> 
> -- 
> 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.


Re: [racket-users] Typed Racket: Is (- 1 1) equivalent to (- 2 2)?

2015-12-10 Thread Alex Knauth
In typed racket (- 1 1) and (- 2 2) are equal at runtime, but the type checker 
doesn't necessarily know that at compile time. It knows that (- 1 1) is zero 
because that's a special case in the type system. But it doesn't have a special 
case for (- 2 2), so it only knows that that's a Fixnum. 

Alex Knauth

> On Dec 10, 2015, at 12:26 PM, Klaus Ostermann  wrote:
> 
> This Typed Racket term is well-typed:
> 
> (+ 1 (if (= 0 (- 1 1)) 1 "x"))
> 
> This one isn't:
> 
> (+ 1 (if (= 0 (- 2 2)) 1 "x"))
> 
> This looks a bit strange to me, because usually one would expect 
> well-typedness to be not destroyed by replacing "equals with equals".
> 
> I'd like to know the rationale for this design. It would be nice if one of 
> the designers could comment on this.

-- 
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] Typed Racket: Is (- 1 1) equivalent to (- 2 2)?

2015-12-10 Thread Klaus Ostermann
This Typed Racket term is well-typed:

(+ 1 (if (= 0 (- 1 1)) 1 "x"))

This one isn't:

(+ 1 (if (= 0 (- 2 2)) 1 "x"))

This looks a bit strange to me, because usually one would expect well-typedness 
to be not destroyed by replacing "equals with equals".

I'd like to know the rationale for this design. It would be nice if one of the 
designers could comment on this.

-- 
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] Crash when installing 'boris' package from GitHub URL on OSX 10.6.8

2015-12-10 Thread David K. Storrs
On Thursday, December 10, 2015 at 4:05:02 AM UTC-8, Matthew Flatt wrote:
> I've pushed a repair for the crash, which was due to a bug in the new
> macro expander.
> 
> The "boris/hypertext-browser/http/head.rkt" module creates a pattern of
> binding and shadowing that had never been exercised before --- at least
> not in code saved in bytecode form. (It took me much longer to
> construct a test case that navigates the same path than to fix the
> bug.) I think that `scribble/srcdoc` is a key step in making "head.rkt"
> trigger the expander bug, so if a workaround is needed, probably it
> involves avoiding `scribble/srcdoc`.
> 
> Thanks for the report!

Wow, that was fast!  Thank you.

I didn't actually do anything related to scribble, I just tried to install the 
module -- although presumably that automatically attempted to setup scribble 
docs.

-- 
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] Crash when installing 'boris' package from GitHub URL on OSX 10.6.8

2015-12-10 Thread Matthew Flatt
I've pushed a repair for the crash, which was due to a bug in the new
macro expander.

The "boris/hypertext-browser/http/head.rkt" module creates a pattern of
binding and shadowing that had never been exercised before --- at least
not in code saved in bytecode form. (It took me much longer to
construct a test case that navigates the same path than to fix the
bug.) I think that `scribble/srcdoc` is a key step in making "head.rkt"
trigger the expander bug, so if a workaround is needed, probably it
involves avoiding `scribble/srcdoc`.

Thanks for the report!

At Wed, 9 Dec 2015 17:50:19 -0800 (PST), "David K. Storrs" wrote:
> Hi folks,
> 
> I've done a bit of Scheme in the past (although not a lot) and am just 
> getting 
> started with Racket.  Yesterday I tried installing a package -- 'Boris', a 
> web 
> spider -- and raco crashed with the output shown below.
> 
> Two questions:
> 
> 1) Is there a web-spidering package that people recommend?  I could use wget 
> and then parse things from disk, but I'd like to have something that's easily 
> composable into CLI scripts.
> 
> 2) Given the crash shown below, what happened and how do I keep it from 
> happening again?
> 
> 
> Context:  OSX 10.6.8; Racket 6.3; running in Terminal inside an Emacs 22.1.1 
> *shell* buffer
> 
> 
> $ raco pkg install github://github.com/emdonahu/boris/master
> Querying Git references for boris at github://github.com/emdonahu/boris/master
> Downloading repository github://github.com/emdonahu/boris/master
> raco setup: version: 6.3
> raco setup: platform: x86_64-macosx [3m]
> raco setup: installation name: 6.3
> raco setup: variants: 3m
> raco setup: main collects: /Applications/Racket_v6.3/collects
> raco setup: collects paths:
> raco setup:   /Users/dstorrs/Library/Racket/6.3/collects
> raco setup:   /Applications/Racket_v6.3/collects
> raco setup: main pkgs: /Applications/Racket_v6.3/share/pkgs
> raco setup: pkgs paths:
> raco setup:   /Applications/Racket_v6.3/share/pkgs
> raco setup:   /Users/dstorrs/Library/Racket/6.3/pkgs
> raco setup: links files:
> raco setup:   /Applications/Racket_v6.3/share/links.rktd
> raco setup:   /Users/dstorrs/Library/Racket/6.3/links.rktd
> raco setup: main docs: /Applications/Racket_v6.3/doc
> raco setup: --- updating info-domain tables ---
> raco setup: updating: /Users/dstorrs/Library/Racket/6.3/share/info-cache.rktd
> raco setup: --- pre-installing collections ---
> raco setup: --- installing foreign libraries ---
> raco setup: --- installing shared files ---
> raco setup: --- compiling collections ---
> raco setup: --- parallel build using 8 jobs ---
> raco setup: 7 making: /boris/boris
> raco setup: 6 making: /boris/echo-server
> raco setup: 5 making: /boris/hypertext-browser
> raco setup: 4 making: /boris/persistent
> raco setup: 3 making: /boris/tests
> raco setup: 3 making: /boris/tests/boris
> raco setup: 2 making: /boris/utils
> raco setup: 2 making: /boris/utils/emd
> raco setup: 7 making: /boris/boris/interpreter
> Assertion failed: (((intptr_t)((Scheme_Object *)(scopes))) & 
> 0x1)?(Scheme_Type)scheme_int\
> eger_type:((Scheme_Object *)((Scheme_Object *)(scopes)))->type) >= 
> scheme_hash_tree_type) && \
> (intptr_t)((Scheme_Object *)(scopes))) & 
> 0x1)?(Scheme_Type)scheme_integer_type:((Scheme_O\
> bject *)((Scheme_Object *)(scopes)))->type) <= 
> scheme_hash_tree_indirection_type))), function\
>  add_conditional_as_reachable, file ../../../racket/gc2/../src/syntax.c, line 
> 5337.
> Abort trap
> 
> 
> 
> 
> 
>  
> 
> -- 
> 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.