Re: [racket-users] Possible Typed Racket bugs (regarding, separately, for/fold and occurrence typing)

2018-12-02 Thread Sam Tobin-Hochstadt
As John suggested, the difference is all about how they expand. I
recommend taking a look in the macro stepper to see the details, but
roughly, Typed Racket reasons about control flow in a sequence like
`begin`, but writing `(let () (define x 1) (print x) (define y 2)
(print y))` puts the `(print x)` on the right hand side of a `let`
binding which Typed Racket doesn't do anything with. This could
certainly be improved, but that's where the difference comes from.

Sam
On Sat, Dec 1, 2018 at 11:07 PM George Neuner  wrote:
>
>
> On 12/1/2018 7:24 PM, 'John Clements' via Racket Users wrote:
>
> I claim that it’s not quite as simple as that. For instance, consider this 
> program:
>
> #lang typed/racket
>
> ;; this one type-checks as a Number:
> (ann
>  (let ()
>(define num (string->number "aoeu"))
>(unless num
>  (error "Not a number"))
>(* num 2))
>  Number)
>
> ;; this one doesn't type-check at all:
> (ann
>  (let ()
>(define num (string->number "aoeu"))
>(unless num
>  (error "Not a number"))
>(define double (* num 2))
>double)
>  Number)
>
> The first one type-checks fine, the second one doesn’t. The only difference 
> between them is that the first one returns the (* num 2) directly and the 
> second one gives it a name.
>
> Note that the ‘for’ loop is not important, I scrapped it. Also, I wrapped 
> them in a type annotation using ‘ann’, just to show that they both type-check 
> at Number.
>
> Usually when I see something like this I confidently declare that it’s a bug, 
> and then Sam explains that it’s not, because a continuation might jump 
> sideways into the code… or simply that it’s too complicated a piece of code. 
> In this situation, though, I’m not sure how that could be the case.
>
> Finally, in the ‘due diligence’ category, this is DrRacket compiled from 
> head, "version 7.1.0.8--2018-12-01(-/f) [3m]."
>
> John
>
>
> I agree, but it's not simply "giving the value a name" - it has something to 
> do with the internal define.
> E.g., this type checks:
>
> (ann
>  (let ()
>(define num (string->number "aoeu"))
>(unless num
>  (error "Not a number"))
>(let ((double (* num 2)))
>  double))
>  Number)
>
>
> And as I mentioned already, the internal define works inside a COND  [below 
> in the quote].
>
> My (maybe flawed) understanding is that internal define and let both create 
> just a local and not a named binding.
>
> George
>
>
> > On Dec 1, 2018, at 10:40, George Neuner  wrote:
> >
> >
> >
> > On 12/1/2018 12:28 PM, hashim muqtadir wrote:
> >> But this doesn't typecheck:
> >>
> >> > (for ([x (in-list '("123" "432" "234"))])
> >> (define num (string->number x))
> >> (unless num
> >>   (error "Not a number"))
> >> (define double (* num 2))
> >> (display (format "~s" double)))
> >> . Type Checker: type mismatch
> >>   expected: Number
> >>   given: (U Complex False) in: num
> >>
> >> Am I missing something here?
> >
> > That string->number returns #f if it fails - and if num is #f then (* num 
> > 2) is meaningless.
> >
> > The type error is telling you where you will run into the problem:
> >   expected: Number
> >   given: (U Complex False) in: num
> >
> > You know that execution won't reach the multiplication if num is #f, but 
> > the compiler doesn't.
> >
> >
> > I'm not any kind of typed Racket wizard, but the type error goes away if 
> > you explicitly use a conditional:
> >  :
> > (cond
> >   ([false? num]
> >(error "Not a number") )
> >   (else
> >(define double (* num 2))
> >(display (format "~s" double)) ))
> >
> > If you use LET rather than the internal define, you can use IF instead.
> >  :
> > (if num
> >   (let ((double (* num 2)))
> > (display (format "~s" double)))
> >   (error "Not a number")
> >   ))
> >
> >
> > 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.


Re: [racket-users] Possible Typed Racket bugs (regarding, separately, for/fold and occurrence typing)

2018-12-01 Thread George Neuner


On 12/1/2018 7:24 PM, 'John Clements' via Racket Users wrote:

I claim that it’s not quite as simple as that. For instance, consider this 
program:

#lang typed/racket

;; this one type-checks as a Number:
(ann
  (let ()
(define num (string->number "aoeu"))
(unless num
  (error "Not a number"))
(* num 2))
  Number)

;; this one doesn't type-check at all:
(ann
  (let ()
(define num (string->number "aoeu"))
(unless num
  (error "Not a number"))
(define double (* num 2))
double)
  Number)

The first one type-checks fine, the second one doesn’t. The only difference 
between them is that the first one returns the (* num 2) directly and the 
second one gives it a name.

Note that the ‘for’ loop is not important, I scrapped it. Also, I wrapped them 
in a type annotation using ‘ann’, just to show that they both type-check at 
Number.

Usually when I see something like this I confidently declare that it’s a bug, 
and then Sam explains that it’s not, because a continuation might jump sideways 
into the code… or simply that it’s too complicated a piece of code. In this 
situation, though, I’m not sure how that could be the case.

Finally, in the ‘due diligence’ category, this is DrRacket compiled from head, 
"version 7.1.0.8--2018-12-01(-/f) [3m]."

John


I agree, but it's not simply "giving the value a name" - it has 
something to do with the internal define.

E.g., this type checks:

   (ann
 (let ()
   (define num (string->number "aoeu"))
   (unless num
 (error "Not a number"))
   (let ((double (* num 2)))
 double))
 Number)


And as I mentioned already, the internal define works inside a COND 
[below in the quote].


My (maybe flawed) understanding is that internal define and let both 
create just a local and not a named binding.


George



> On Dec 1, 2018, at 10:40, George Neuner  wrote:
> 
> 
> 
> On 12/1/2018 12:28 PM, hashim muqtadir wrote:

>> But this doesn't typecheck:
>> 
>> > (for ([x (in-list '("123" "432" "234"))])

>> (define num (string->number x))
>> (unless num
>>   (error "Not a number"))
>> (define double (* num 2))
>> (display (format "~s" double)))
>> . Type Checker: type mismatch
>>   expected: Number
>>   given: (U Complex False) in: num
>> 
>> Am I missing something here?
> 
> That string->number returns #f if it fails - and if num is #f then (* num 2) is meaningless.
> 
> The type error is telling you where you will run into the problem:

>   expected: Number
>   given: (U Complex False) in: num
> 
> You know that execution won't reach the multiplication if num is #f, but the compiler doesn't.
> 
> 
> I'm not any kind of typed Racket wizard, but the type error goes away if you explicitly use a conditional:

>  :
> (cond
>   ([false? num]
>(error "Not a number") )
>   (else
>(define double (* num 2))
>(display (format "~s" double)) ))
> 
> If you use LET rather than the internal define, you can use IF instead.

>  :
> (if num
>   (let ((double (* num 2)))
> (display (format "~s" double)))
>   (error "Not a number")
>   ))
> 
> 
> 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] Possible Typed Racket bugs (regarding, separately, for/fold and occurrence typing)

2018-12-01 Thread 'John Clements' via Racket Users
I claim that it’s not quite as simple as that. For instance, consider this 
program:

#lang typed/racket

;; this one type-checks as a Number:
(ann  
 (let ()
   (define num (string->number "aoeu"))
   (unless num
 (error "Not a number"))
   (* num 2))
 Number)

;; this one doesn't type-check at all:
(ann
 (let ()
   (define num (string->number "aoeu"))
   (unless num
 (error "Not a number"))
   (define double (* num 2))
   double)
 Number)

The first one type-checks fine, the second one doesn’t. The only difference 
between them is that the first one returns the (* num 2) directly and the 
second one gives it a name.

Note that the ‘for’ loop is not important, I scrapped it. Also, I wrapped them 
in a type annotation using ‘ann’, just to show that they both type-check at 
Number.

Usually when I see something like this I confidently declare that it’s a bug, 
and then Sam explains that it’s not, because a continuation might jump sideways 
into the code… or simply that it’s too complicated a piece of code. In this 
situation, though, I’m not sure how that could be the case.

Finally, in the ‘due diligence’ category, this is DrRacket compiled from head, 
"version 7.1.0.8--2018-12-01(-/f) [3m]."

John




> On Dec 1, 2018, at 10:40, George Neuner  wrote:
> 
> 
> 
> On 12/1/2018 12:28 PM, hashim muqtadir wrote:
>> But this doesn't typecheck:
>> 
>> > (for ([x (in-list '("123" "432" "234"))])
>> (define num (string->number x))
>> (unless num
>>   (error "Not a number"))
>> (define double (* num 2))
>> (display (format "~s" double)))
>> . Type Checker: type mismatch
>>   expected: Number
>>   given: (U Complex False) in: num
>> 
>> Am I missing something here?
> 
> That string->number returns #f if it fails - and if num is #f then (* num 2) 
> is meaningless.
> 
> The type error is telling you where you will run into the problem:
>   expected: Number
>   given: (U Complex False) in: num
> 
> You know that execution won't reach the multiplication if num is #f, but the 
> compiler doesn't.
> 
> 
> I'm not any kind of typed Racket wizard, but the type error goes away if you 
> explicitly use a conditional:
>  :
> (cond
>   ([false? num]
>(error "Not a number") )
>   (else
>(define double (* num 2))
>(display (format "~s" double)) ))
> 
> If you use LET rather than the internal define, you can use IF instead.
>  :
> (if num
>   (let ((double (* num 2)))
> (display (format "~s" double)))
>   (error "Not a number")
>   ))
> 
> 
> 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.


Re: [racket-users] Possible Typed Racket bugs (regarding, separately, for/fold and occurrence typing)

2018-12-01 Thread George Neuner




On 12/1/2018 12:28 PM, hashim muqtadir wrote:

But this doesn't typecheck:

> (for ([x (in-list '("123" "432" "234"))])
    (define num (string->number x))
    (unless num
  (error "Not a number"))
    (define double (* num 2))
    (display (format "~s" double)))
. Type Checker: type mismatch
  expected: Number
  given: (U Complex False) in: num

Am I missing something here?


That string->number returns #f if it fails - and if num is #f then (* 
num 2) is meaningless.


The type error is telling you where you will run into the problem:
  expected: Number
  given: (U Complex False) in: num

You know that execution won't reach the multiplication if num is #f, but 
the compiler doesn't.



I'm not any kind of typed Racket wizard, but the type error goes away if 
you explicitly use a conditional:

 :
    (cond
  ([false? num]
   (error "Not a number") )
  (else
   (define double (* num 2))
   (display (format "~s" double)) ))

If you use LET rather than the internal define, you can use IF instead.
 :
    (if num
  (let ((double (* num 2)))
    (display (format "~s" double)))
  (error "Not a number")
  ))


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.